*Subject*: Re: [isabelle] Problem with sort constraints*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Mon, 11 Jun 2012 09:15:43 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <372BA9A1-16F5-4812-BAA5-F2AFBCFED674@uibk.ac.at>*References*: <372BA9A1-16F5-4812-BAA5-F2AFBCFED674@uibk.ac.at>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.27) Gecko/20120216 Thunderbird/3.1.19

Dear René, > So my question is, whether this is also possible for class-constraints?

> I.e., if I just > fix some function (emb in the example below) without making any assumptions > about it, can one get rid of the sort constraint (i.e., replace the > "('a :: embed)list by ('a list)"). > > In the proof below, I just require the exakt definition of emb for lists, but > it does not matter how emb is defined on type 'a for the elements of the list.

function len :: "'a list => nat" where "len [] = 0" | "len (x # xs) = Suc (len xs)" by pat_completeness auto termination len (* goal: All len_dom *) proof def emb == "list_rec 0 (%x xs res. undefined + 2 * res + 1) :: 'a list => nat" let ?r = "inv_image ({(x,y). x < y}) emb" show "wf ?r" by (rule wf_inv_image[OF wf_less]) fix x xs show "(xs, x # xs) : ?r" by(simp add: emb_def) qed

(* not tested *) consts emb :: "'a => nat" defs (overloaded) emb_list_def: "emb = list_rec 0 (%x xs res. emb x + 2 * res + 1)" class emb_code = fixes emb_code :: "'a => nat" assumes emb_code: "emb = emb_code" declare emb_code[code] instantiation list :: (emb) emb begin definition "emb_code :: 'a list => nat == emb" instance by(intro_locales)(simp add: emb_code_def) end 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

**Follow-Ups**:**Re: [isabelle] Problem with sort constraints***From:*René Thiemann

**References**:**[isabelle] Problem with sort constraints***From:*René Thiemann

- Previous by Date: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- Next by Date: Re: [isabelle] Problem with sort constraints
- Previous by Thread: [isabelle] Problem with sort constraints
- Next by Thread: Re: [isabelle] Problem with sort constraints
- Cl-isabelle-users June 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