*To*: Mathias Fleury <mathias.fleury12 at gmail.com>, Isabelle User <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] lift_definition in locales*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 16 Jun 2016 08:59:28 +0200*In-reply-to*: <7B9CD823-D89D-4F71-A592-45C0356F3276@gmail.com>*Organization*: TU Munich*References*: <7B9CD823-D89D-4F71-A592-45C0356F3276@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

Hi Mathias, quoting NEWS for Isabelle2099-2: > * Command 'typedef' now works within a local theory context -- without > introducing dependencies on parameters or assumptions, which is not > possible in Isabelle/Pure/HOL. Note that the logical environment may > contain multiple interpretations of local typedefs (with different > non-emptiness proofs), even in a global theory context. I do not know whether your typedef specification satisfy the precondition that no dependencies on parameters or assumptions are introduced, but you may want to try this and see how far you can get. Hope this helps, Florian Am 15.06.2016 um 20:44 schrieb Mathias Fleury: > Hello list, > > I would like to prepare code exportation within a locale, in such a way that I only have to instantiate the locale to generate code later. However, my functions do not unconditionally terminate and I need an invariant (called inv in the following email) to prove termination and correctness. Therefore, I wanted to define a typedef within the locale. > > But as there cannot be a typedef inside a locale, I axiomatised it (via the theorem that typedef generates) with the idea that I could instantiate it later, while still using the theorems and lift definitions: > > locale type_definition_locale = > fixes Abs :: "'a â 'inv" and Rep :: "'inv â 'a" and inv :: "'a â bool" > assumes > Rep_inverse: "Abs (Rep x) = x" and > Rep: "Rep x â {a. inv a}" and > Rep_inject: "Rep x = Rep y â x = y" and > Abs_inverse: "z â {a. inv a} â Rep (Abs z) = z" and > Abs_induct: "(ây. y â {a. inv a} â P (Abs y)) â P y" and > Rep_induct: "z â {a. inv a} â (âz. P' (Rep z)) â P' z" and > Abs_cases: "(ây. x = Abs y â y â {a. inv a} â Q) â Q" and > Rep_cases: "z â {a. inv a} â (ây. z = Rep y â Q) â Q" and > Abs_inject: "z â {a. inv a} â z' â {a. inv a} â Abs z = Abs z' â z = z'" > > > Now my question is the following: is there a way to use lift_definition within the previous locale? For now, an error is produced: > > context type_definition_locale > begin > > definition raw_K :: "'a â 'a â 'a" where > "raw_K a _ = a" > > lift_definition refined_K :: "'inv â 'inv â 'inv" is raw_K > > (* Fails with: > Lifting failed for the following term: > Term: raw_K > Type: 'a â 'a â 'a > > Reason: > The type of the term cannot be instantiated to > "'inv â 'inv â âinvâ. > *) > end > > I tried using setup_lifting, but this does not work either. The error message was not very precise ("The abstract type must be a type constructor.â), but I think that the error comes from: > > fun is_Type (Type _) = true > | is_Type _ = false > > Types passed as parameters in locales use the constructor TFree instead of Type. > > > Is there a way to avoid doing the lifting by hand? Would it be safe to extend the function is_Type to accept TFree? > > > Thanks in advance, > Mathias > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] lift_definition in locales***From:*Mathias Fleury

- Previous by Date: Re: [isabelle] lift_definition in locales
- Next by Date: Re: [isabelle] lift_definition in locales
- Previous by Thread: Re: [isabelle] lift_definition in locales
- Next by Thread: Re: [isabelle] lift_definition in locales
- Cl-isabelle-users June 2016 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