Re: [isabelle] making local definitions programmatically



Florian Haftmann wrote:

> Definitions in local theories accumulate a hypothetical proof
> context.  If you want to return to the plain local theory, you can
> leave the hypothetical proof context using LocalTheory.restore and
> export logical entities (theorems, terms, types, ...) using an
> appropriate export morphism which calcuates the difference between
> the hypothetical proof context lthy' and the restored plain local
> theory lthy''.

I need to make definitions inside a locale that I have set up
programmatically.  Within that program, I can't do nice things like
@{term "...localeconst...."}  (as in your example), because the
code doing this is not itself in a locale.

Here's a specific question about check_term.

If I have a theory fragment of the following form:

----------------------------------------------------------------------
theory Scratch
  imports Main
begin

locale L =
  fixes x :: nat
begin
  definition "y = x + 3"
end

term L.y
thm L.y_def

ML {*
  val lthy = TheoryTarget.init (SOME "Scratch.L")
                               (Context.deref @{theory_ref})
  val t = Syntax.check_term lthy (Const(<string>, dummyT))
*}
----------------------------------------------------------------------

The only way I can avoid an "unknown const" error is to have

 <string> = "Scratch.L.y"

I thought the point of check_term was that I could have "local.y"
there, and have it work.  Have I set up my lthy local_theory value
incorrectly?

(In my simple example, I recognise that I could also write

  <string> = @{const_name "L.y"}

This is *no* use in my real circumstances, where the locale L has been
set up in code, so there is no fixed string "L.y" I could provide to
@{const_name}.  Indeed, both the "L" and the "y" are constructed
strings in my code.)

Michael.





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