Re: [isabelle] How do I do stone age interaction?



On 06/12/10 20:17, Makarius wrote:
> On Mon, 6 Dec 2010, Jeremy Dawson wrote:
>

> See the "tactic" proof method in the isar-ref manual how to embed ML
> tactic expressions into Isar source text.
>
A warning, though - this often doesn't work.  One of the reasons is
described in the following paragraph.
>
> BTW, old Simp_tac and Safe_tac refer to "the_context()" which is not
> always the same as your goal context, i.e. CI_Rls.thy above.  This is
> why I have called it a running gag from many years ago.
>
I think this is a legitimate criticism, but that the sensible solution
would have been to change these tactics so that they use the theory
context of the theorem representing the proof underway.
>
>>> The naked ML toplevel lacks the formal Isabelle context, which means
>>> you can hardly do anything useful, e.g. being able to parse/print
>>> expressions always requires a proper context.
>> If "proper context" means something of the type Proof.context, then this
>> isn't so - the "read" function implicitly uses an old style "theory
>> context" only
>
> An old style "theory context" is not a proper context.  You are also
> subject to "the_context()" confusion here, i.e. you can never be quite
> sure what you get.  Good that we got rid of the "read" function long ago.

As for the general issue of using an implicit, rather than explicit,
context, well, it isn't so long ago that someone thought it was a _good_
idea to introduce the "Goal" command as an alternative to "goal" (for
this discussion, Goal = goal (the_context ())).  That is, different
people have different opinions on this sort of issue.

Anyway what I mean is that "read", as I understand it, uses only a
"theory context", not a "proper context" (which, as I understand it,
doesn't exist unless you're using Isar).

I think that another legitimate criticism of the ML interface is that
"read" and "prin" refer to the context of the most recent interactive
proof, rather than the_context (), but that fixing this doesn't require
chucking out the entire ML interface.

as for never being quite sure of what [theory context] you get, I found
this problem a good deal worse using Isar, because (I think) the theory
context keeps changing while an Isar file is being processed
>
>> I'm not sure if I understand this right, but at the ML level I
>> certainly get all the HOL syntax and theorems - note, though, if
>> you're using "new-style" theory files, then to get theorems derived
>> from the theory file as ML identifiers you need to use the
>> "use_legacy_bindings" function.
>
> Hardly anybody on the mailing list will remember "old-style" theories.
> This is just historical cruft, even in Isabelle2005.  Gladly this has
> been deleted long ago.
>
whatever the relative merits of new-style theories versus old-style
theories, the fact is that massive amounts of proofs using old-style
theories exist, and people are currently developing further proofs build
upon them.  So what make you glad makes recent versions of Isabelle
unusable for other people

Jeremy
>     Makarius






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