Re: [isabelle] making local definitions programmatically

Dear Michael,

> locale L =
>   fixes c0 :: "'a \<Rightarrow> 'a"
> begin
> ML {*
> fun def lthy =
>   let
>     val ((t, _), lthy') = LocalTheory.define Thm.definitionK
>       (("c1", NoSyn), (("", []), @{term "\<lambda>x. c0 (c0 x)"})) lthy;
>     val lthy'' = LocalTheory.restore lthy';
>     val t' = Morphism.term (ProofContext.export_morphism lthy' lthy'') t;
>   in (t', lthy'') end;
> *}
> ML {*
> Context.>>> (Context.map_proof_result def)
> *}

Definitions in local theories accumulate a hypothetical proof context.
If you want to return to the plain local theory, you can leave the
hypothetical proof context using LocalTheory.restore and export logical
entities (theorems, terms, types, ...) using an appropriate export
morphism which calcuates the difference between the hypothetical proof
context lthy' and the restored plain local theory lthy''.

Anyway, it is also possible (and most times more convenient) to
*continue* within the hypothetical context with defines, notes etc.
These are exported into the local theory context implicitly without
further ado.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.