Re: [isabelle] lift_definition in locales



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
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.