Re: [isabelle] lift_definition in locales



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
Description: OpenPGP digital signature



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