# [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?