Re: [isabelle] making local definitions programmatically



       This works for me:

ML {*
   val lthy = TheoryTarget.init (SOME "Scratch.L") (Context.deref @{theory_ref})  
   val t = Syntax.check_term lthy (Const(LocalTheory.full_name lthy "y", dummyT))
*}

	I guess that check_term doesn't expand the name it is given.  
That first line is ugly, better (IMHO) is:

     val lthy = TheoryTarget.context "L" @{theory}

     Simon

At Tue, 29 Apr 2008 16:39:39 +1000,
Michael Norrish wrote:
> 
> Florian Haftmann wrote:
[...]
> 
> 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.