[isabelle] lift_definition in locales



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.