Re: [isabelle] making local definitions programmatically



Dear Michael,

> As for this last point, I thought that I would do as you suggest (keep
> track of what is returned by LocalTheory.define), but if you check
> what it does, you don't actually get a Const back.  Instead, the term
> returned is a Free, with an unqualified name.

Concerning this, recall the following:

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

This approach refrains from assuming anything about a particular naming
policy.

Hope this helps,

	Florian

begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature



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