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.

Example:

theory Scratch
imports Main
begin

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

definition
  "c1 x = c0 (c0 x)"

definition
  "c2 x = c1 (c1 x)"

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

end

Hope this helps
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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