*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Wellsortedness error by using user defined function in quickcheck*From*: Lukas Bulwahn <bulwahn at in.tum.de>*Date*: Mon, 03 Sep 2012 11:09:06 +0200*Cc*: Yuhui Lin <Y.H.Lin-2 at sms.ed.ac.uk>, isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <50447028.9090206@kit.edu>*References*: <F1E3A26D-18BE-4C61-A01F-E82752F84766@sms.ed.ac.uk> <503DF3E3.30407@kit.edu> <503DFFEF.3080905@in.tum.de> <220D82AA-965A-4D9F-A9E6-DD2DA1811721@sms.ed.ac.uk> <50447028.9090206@kit.edu>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:12.0) Gecko/20120430 Thunderbird/12.0.1

Dear Yuhui, On 09/03/2012 10:54 AM, Andreas Lochbihler wrote:

Dear Yuhui,And I wonder for the following defitnion, "Pow1 R = {S. S ≠ {} ∧ S ⊆ R}" "domres R r = {(x, y) | x y. x ∈ R ∧ (x, y) ∈ r}"there are no quantifiers, and the definitions look simple. I wonderwhy quick check can't execute them directly. More interestingly, if Iunfolder the definition of Pow1, then quick check can work..lemma "(S :: nat set) ~: Pow1 S"lemma "(domres (s0::nat set) (v1:: (nat*nat set))) Un v2 = domres s0(v1 Un v2)"Since sets are represented as the list of their elements, the "Pow1 S"in your first lemma needs to be computed explicitly. Now, Pow1 isdefined as a set comprehension, which is in general not executable.The default code setup computes set comprehensions by taking the listof all elements of the type and filtering each by checking thepredicate of the set comprehension. If you unfold the definition, yourgoal has the form ".. : {S. ...}" and there is a preprocessing step inthe code generator that simplifies this to "... ..", i.e., removes theset comprehension and membership.For domres, there are quantifiers. "{(x, y) | x y. ...}" is ashort-hand for "{u. \exists x y. u = (x, y) & ...}". For tuples, youdon't need to quantify over x and y, so you could simplify thedefinition to"domres R r = {(x, y). x ∈ R ∧ (x, y) ∈ r}"Nevertheless, the trouble with set comprehensions remains, but youcould prove again a custom code equation:lemma domres_code [code]: "domres R (set rs) = set (filter (%(x, y). x : R) rs)" by(auto simp add: domres_def)

You can inspect the code setup with this type of template: definition conjecture where "conjecture S = ((S :: nat set) ~: Pow1 S)" code_thms conjecture

Lukas

Best, Andreas

**References**:**Re: [isabelle] Wellsortedness error by using user defined function in quickcheck***From:*Yuhui Lin

**Re: [isabelle] Wellsortedness error by using user defined function in quickcheck***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Wellsortedness error by using user defined function in quickcheck
- Next by Date: Re: [isabelle] Product types?
- Previous by Thread: Re: [isabelle] Wellsortedness error by using user defined function in quickcheck
- Next by Thread: Re: [isabelle] Wellsortedness error by using user defined function in quickcheck
- Cl-isabelle-users September 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list