Re: [isabelle] lift_definition in locales



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

On 15/06/16 20:44, Mathias Fleury 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.