*To*: Yuhui Lin <Y.H.Lin-2 at sms.ed.ac.uk>*Subject*: Re: [isabelle] Wellsortedness error by using user defined function in quickcheck*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Wed, 19 Sep 2012 08:34:04 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <B1442E3B-B04D-4712-965F-0AAC25B48441@sms.ed.ac.uk>*References*: <F1E3A26D-18BE-4C61-A01F-E82752F84766@sms.ed.ac.uk> <503DF3E3.30407@kit.edu> <503DFFEF.3080905@in.tum.de> <220D82AA-965A-4D9F-A9E6-DD2DA1811721@sms.ed.ac.uk> <504855A6.3060002@informatik.tu-muenchen.de> <B1442E3B-B04D-4712-965F-0AAC25B48441@sms.ed.ac.uk>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.27) Gecko/20120216 Thunderbird/3.1.19

Hi Yuhui,

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

"0 = funimage (set [(0, 0), (0, 1)]) 0 = funimage (set [(0, 1), (0, 0)]) 0 = 1"

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

lemma [code]: "funimage (set ss) x = (if x : Domain (set ss) & functional (set ss) then snd (hd (filter (λ (x0, y0). x = x0) ss)) else funimage (set ss) x)"

definition funimage_not_unique :: "(unit => 'a) => 'a" where [simp]: "funimage_not_unique f = f ()" code_abort funimage_not_unique lemma [code]: "funimage (set ss) x = (if x : Domain (set ss) & functional (set ss) then snd (hd (filter (λ (x0, y0). x = x0) ss)) else funimage_not_unique (%_. funimage (set ss) x))" code_abort funimage_not_unique

lemma "funimage (set ss) x = Predicate.the (pred_of_set (set (filter (λ (x0, y0). x = x0) ss)))" Hope this helps, Andreas

-- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Am Fasanengarten 5, Geb. 50.34, Raum 025 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**References**:

- Previous by Date: Re: [isabelle] Wellsortedness error by using user defined function in quickcheck
- Next by Date: Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround)
- Previous by Thread: Re: [isabelle] Wellsortedness error by using user defined function in quickcheck
- Next by Thread: Re: [isabelle] Product types?
- Cl-isabelle-users September 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