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



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


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