*To*: Mathias Fleury <mathias.fleury12 at gmail.com>*Subject*: Re: [isabelle] lift_definition in locales*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Thu, 16 Jun 2016 09:39:55 +0200*Cc*: Isabelle User <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <7B9CD823-D89D-4F71-A592-45C0356F3276@gmail.com>*References*: <7B9CD823-D89D-4F71-A592-45C0356F3276@gmail.com>

Hi Mathias, independently of lift_definition and code generation: a side remark on your locale. A type definition locale already exists. It is called type_definition (the term type_definition is actually a locale predicate; the locale is used by typedef). It assumes only three facts (Rep, Rep_inverse, and Abs_inverse) and derives the rest. There is no need to duplicate those things. Dmitriy > On 15 Jun 2016, at 20:44, Mathias Fleury <mathias.fleury12 at gmail.com> wrote: > > 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 >

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

- Previous by Date: Re: [isabelle] lift_definition in locales
- Next by Date: [isabelle] Operator with Pair sets
- Previous by Thread: Re: [isabelle] lift_definition in locales
- Next by Thread: [isabelle] Proof General as Coq-only front-end
- 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