*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*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 16 Jun 2016 08:51:44 +0200*In-reply-to*: <7B9CD823-D89D-4F71-A592-45C0356F3276@gmail.com>*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

Dear Mathias,

type_definition Rep Abs {x. inv x}

Andreas On 15/06/16 20:44, Mathias Fleury 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

**Follow-Ups**:**Re: [isabelle] lift_definition in locales***From:*Mathias Fleury

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

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