# Re: [isabelle] Wellsortedness error by using user defined function in quickcheck

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 wonder why quick check can't execute them directly. More interestingly, if I unfolder 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 is defined as a set
``comprehension, which is in general not executable. The default code setup
``computes set comprehensions by taking the list of all elements of the type and
``filtering each by checking the predicate of the set comprehension. If you unfold
``the definition, your goal has the form ".. : {S. ...}" and there is a
``preprocessing step in the code generator that simplifies this to "... ..", i.e.,
``removes the set comprehension and membership.
`

`For domres, there are quantifiers. "{(x, y) | x y. ...}" is a short-hand for
``"{u. \exists x y. u = (x, y) & ...}". For tuples, you don't need to quantify
``over x and y, so you could simplify the definition to
`
"domres R r = {(x, y). x ∈ R ∧ (x, y) ∈ r}"

`Nevertheless, the trouble with set comprehensions remains, but you could 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)
Best,
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de

`KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
``in der Helmholtz-Gemeinschaft
`

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*