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

  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 =
v1 v2 v3 :: "(nat * nat) set"

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

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.

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.