*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Wellsortedness error by using user defined function in quickcheck*From*: Lukas Bulwahn <bulwahn at in.tum.de>*Date*: Wed, 29 Aug 2012 13:41:35 +0200*Cc*: Yuhui Lin <Y.H.Lin-2 at sms.ed.ac.uk>, isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <503DF3E3.30407@kit.edu>*References*: <F1E3A26D-18BE-4C61-A01F-E82752F84766@sms.ed.ac.uk> <503DF3E3.30407@kit.edu>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:12.0) Gecko/20120430 Thunderbird/12.0.1

Hi Yuhui, I had the same answer as Andreas in my pipeline.

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

Hi Yuhui,the problem is the existential quantifier in the definition offorwardcomp. Isabelle provides an executable implementation for typesof whose elements it is has a complete list (which is formalised intype class enum). Since lists are finite, nat is not and cannot be aninstance. As quickcheck relies on executable implementations for allconstants, this explains the error message.If you want to quickcheck lemmas that depend on forwardcomp, you needto provide an executable implementation yourself. By default,Isabelle2012 implements sets as the list of its elements (or by thelist of the set's complement). Hence, you could prove the followingcode equation by "pattern-matching" on the "implementationconstructor" 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 completeimplementation, you would probably want to cover all "implementationconstructors" for 'a set, which are "set" and "List.coset". But itwill 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 findcounter examples for the type like "nat set" now. When I usequickcheck for the following example,definitionforwardcomp :: "('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

**References**:**[isabelle] Wellsortedness error by using user defined function in quickcheck***From:*Yuhui Lin

**Re: [isabelle] Wellsortedness error by using user defined function in quickcheck***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Wellsortedness error by using user defined function in quickcheck
- Next by Date: [isabelle] Haskell code generation: Datatype Context
- Previous by Thread: Re: [isabelle] Wellsortedness error by using user defined function in quickcheck
- Next by Thread: [isabelle] Haskell code generation: Datatype Context
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list