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



Hi Yuhui,

I had the same answer as Andreas in my pipeline.

Alternatively, it should also be possible to give a lemma that describes forwardcomp in terms of relcomp, and annotate it with the code attribute.

Lukas

On 08/29/2012 12:50 PM, Andreas Lochbihler wrote:
Hi Yuhui,

the problem is the existential quantifier in the definition of forwardcomp. Isabelle provides an executable implementation for types of whose elements it is has a complete list (which is formalised in type class enum). Since lists are finite, nat is not and cannot be an instance. As quickcheck relies on executable implementations for all constants, this explains the error message.

If you want to quickcheck lemmas that depend on forwardcomp, you need to provide an executable implementation yourself. By default, Isabelle2012 implements sets as the list of its elements (or by the list of the set's complement). Hence, you could prove the following code equation by "pattern-matching" on the "implementation constructor" set.

lemma forwardcomp_code [code]:
  "(set ps; set qs) =
set (concat (map (l(x, y). map (l(y', z'). (x, z')) (filter (l(y', z'). y = y') qs)) ps))"
by(fastforce simp add: forwardcomp_def)

Then, you can quickcheck your lemma. Side remark: For a complete implementation, you would probably want to cover all "implementation constructors" for 'a set, which are "set" and "List.coset". But it will be more difficult to find appropriate equations for List.coset.

Hope this helps,
Andreas

Am 29.08.2012 12:09, schrieb Yuhui Lin:
Hi all,

With the change of representation for set, quickcheck can find counter examples for the type like "nat set" now. When I use quickcheck for the following example,

definition
forwardcomp :: "('a * 'b) set ⇒ ('b * 'c) set ⇒ ('a * 'c) set" (infixl ";" 40)
where "p ; q ≡ {(x,y). ∃ z. (x,z) ∈ p ∧ (z,y) ∈ q}"

locale myspec =
fixes
v1 v2 v3 :: "(nat * nat) set"

lemma (in myspec)
"((v1 Un v2) ; v3) = ((v1 ; v3) Un (v2 ; v3))"
quickcheck
oops

it promote  the error message
Wellsortedness error:
Type nat not of sort {enum,equal}
No type arity nat :: enum

What do I miss here ? Many thanks.

Best,
Yuhui Lin








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