Re: [isabelle] making local definitions programmatically

Dear Michael,

> It would be nice if I could just write
>   Const("C1", nat)

the best thing is to use the "check" interface which does the job for you:

Syntax.check_term @{context} (Const ("local.C1", dummyT))

yield a completely inferred and expanded term representing the local
constant C1.  This saves you from educated guesses what the expanded
foundation term of a local constant actually is.  Note that "check" is a
part of the canonical interface for reading terms:

a) "parse" transforms a string to an abstract term representation
(without further steps like type inference, expanding local constants etc)
b) "check" does the rest

This allows to aggregate "skeleton terms" with dummy types and check
them to get complete internal terms.


theory Scratch
imports Main

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

  "c1 x = c0 (c0 x)"

  "c2 x = c1 (c1 x)"

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


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.