Re: [isabelle] making local definitions programmatically



Dear Michael,

> ML {* val t = Syntax.check_term @{context} (Const("local.c1", dummyT))
>       val ctxt' = LocalTheory.define Thm.definitionK
>                                      (("c3", NoSyn), (("", []), t))
>                                      @{context}
> *}

Which Isabelle version are you using?  The following works fine with
Isabelle2007:

locale L =
  fixes c0 :: "'a � 'a"
begin

definition
  "c1 x = c0 (c0 x)"

definition
  "c2 x = c1 (c1 x)"

ML {*
val t = Syntax.check_term @{context} (Const ("local.c1", dummyT))
*}

ML {* val (_, ctxt') = LocalTheory.define Thm.definitionK (("c3",
NoSyn), (("", []), t)) @{context} *}


Recently it is now also possible to transform a local context (a local
theory) with ML, using the Context.>> and Context.>>> combinators within
ML sections:

locale L =
  fixes c0 :: "'a \<Rightarrow> 'a"
begin

definition
  "c1 x = c0 (c0 x)"

definition
  "c2 x = c1 (c1 x)"

ML_val {*
val t = Syntax.check_term @{context} (Const ("local.c1", dummyT))
*}

ML {*
Context.>>> (Context.map_proof_result (
  LocalTheory.define Thm.definitionK (("c3", NoSyn), (("", []), t))
  ##> LocalTheory.restore
))
*}

ML {* @{term c3} *}
thm c3_def

end


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.