[isabelle] lift_definition in locales

[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

[Andreas Lochbihler]

Dear Mathias,

The Lifting package manages the registered quotients in a map with the name of the type
constructor as a key. So even if you could trick setup_lifting into accepting a theorem of
the form

type_definition Rep Abs {x. inv x}

the lift_definition command would not be able to find the setup, because it constructs the
lifting relation based on the type constructors that appear in the types of the raw term
and the lifted constant. One would have to extend the implementation of
Lifting_Term.prove_schematic_quot_thm accordingly to also support TFree.

Moreover, you'd have to make sure that the quotient theorem setup does not leak into any
interpretation, in which the type variables get instantiated or generalised. Otherwise,
the internal data structures of the Lifting package would be messed up.

Finally, I am not sure that your approach will actually work for code generation. The
steps of lift_definition for a subtype copy are fairly limited except when it comes to
code generation for compound return types. For example, if your function returns something
like 'inv list (rather than a plain 'inv), then lift_definition internally generates a
number of types and auxiliary constants and lifts the invariant to those types such that
the code generator can handle them. I cannot see how this construction would work for an
unspecified 'inv (otherwise, we could have done the construction once and for all for such
an arbitrary 'inv and then just reused everything).

Andreas

[Dmitriy Traytel]

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

[Mathias Fleury]

Dear Andreas and Florian,

Thanks for your comments.


> 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.


I am not in that case: I wanted to abstract the concrete representation of two watched literals scheme (allowing to instantiate the locale with arrays or red-black trees).

> Finally, I am not sure that your approach will actually work for code generation. The steps of lift_definition for a subtype copy are fairly limited except when it comes to code generation for compound return types.

I am mostly interested in the steps of lift_definition for a subtype. I wanted to avoid writing the theorems by hand each time, but it does not matter so much. That seems also easier than changing the Lifting package.



Thanks for your help,
Mathias