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



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

Andreas is perfectly right with his explanations. It took me also a few minutes to understand what Quickcheck is doing there and what not.

You can inspect the code setup with this type of template:

definition conjecture
where
  "conjecture S = ((S :: nat set) ~: Pow1 S)"

code_thms conjecture

In this case, you see that it requires the constant Collect which uses enum_class.enum. In general, it somehow black magic (known to some wizards here and there) to understand why something is not executable.

For the future, we are developing a rewriting procedure in the code generator that should turn

"domres R r = {(x, y) | x y. x ∈ R ∧ (x, y) ∈ r}" into "(R \times UNIV) \inter r" behind the scenes which can be executed with the code generator (and therefore Quickcheck works).

If you write "Pow1 R = {S. S ≠ {} ∧ S ⊆ R}" as "Pow1 R = Pow R - {{}}" it should also be executable (and Quickcheck works).


Lukas

Best,
Andreas







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