Re: [isabelle] lift_definition in locales



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


> On 16 Jun 2016, at 08:51, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
> 
> 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.