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)


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 - 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.