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



Many thanks for the solution. I can run quick check on these user-defined operations code attributes.  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)"

Best,
Yuhui

On 29 Aug 2012, at 12:41, Lukas Bulwahn <bulwahn at in.tum.de> wrote:

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

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.


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