Re: [isabelle] making local definitions programmatically



Florian Haftmann wrote:

> 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 [...]

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

> Example:

> 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

But can I then pass an expanded term, one which mentions the implicit
locale parameters explicitly, to LocalTheory.define?  My experiments
suggest I can't.

If I put this into the locale

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

then I get an error "Illegal application of command "consts" in local
theory mode".  What should t be to make this definition work?  Or
should I be using some other definitional principle?

And is prepending "local." the canonical way to get an acceptable name
for the locale's constants?

Michael.








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