Re: [isabelle] making local definitions programmatically



Florian Haftmann wrote:

> A further hint I want to add: LocalTheory.define etc. return the
> defined entity as a term.  Normally it is the best to use these
> directly to build up other definitions, lemmas etc.  This saves you
> from referring to suspected names of constants altogether.

It seems I have have apply Context.map_proof_result for this to be
useful.  If I omit this (as below), then the result includes a term
that is a Free (not a Const), with no parameters.

----------------------------------------------------------------------
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 (result, ctxt') = LocalTheory.define Thm.definitionK (("c3",
NoSyn), (("", []), t)) @{context} *}

end
----------------------------------------------------------------------

Michael.





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