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


Now I've got a new problem to give a code attribute for the following function.
	"funimage r x = (THE y. (x, y) ∈ r)"

I give a weaker version of code definition, i.e  
	(funimage (set ss) x) = snd (hd (filter (λ (x0, y0). x = x0) ss))

but I don't know how to represent it equivalently in list, because it addresses that y is unique and x : r, which returns boolean type. 

I wonder if there is undefined value for list to represent the invalid case, e.g. return the invalid value when y is not unique. Also I'm trying to giving assumptions for the the code attribute, which is 
"x : Domain (set ss) ==> functional (set ss) ==> (funimage (set ss) x) = snd (hd (filter (λ (x0, y0). x = x0) ss))"
Then I receive a warning "Not a equation". 

How can I deal with it ? Thanks for helps.


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.