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



Dear Jeremy & Co,

May I kindly suggest to make this a private thread among stone age
users? Probably only a handful of people know what you are talking about
and even fewer are interested in the details of ML level interaction. If
anybody else, apart from the participants of this thread, is interested
in the details, they should speak up now and I take back what I wrote.

Thanks
Tobias

Jeremy Dawson schrieb:
> 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.