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



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.