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



on 6/12/10 2:32 PM, Makarius <makarius at sketis.net> wrote:

> There is also a lot of confusion here, because Isabelle2005 features about
> 2 or 3 versions of basic things like syntax layers, goal modules etc.
> The "read" function is an odd leftover from much earlier times.
>
> If you really want to learn about "stone age" Isabelle, I recommend
> something like Isabelle98, or even 89.  If you want to learn about current
> Isabelle, then use the current release Isabelle2009-2.  The
> impracticability of using the raw ML loop in contemporay Isabelle is not
> accidental, but an integral part of the system.  By dropping out of it,
> you won't learn the most important things.

Hmm, not sure whether you're understanding my requirements fully.  When I
say "stone age", I don't mean "early version".  What I mean is "basic ML
toplevel interaction, like what exists in other classic LCF-style theorem
provers, such as HOL90, HOL4, ProofPower HOL, HOL Light".  So can I do this
in Isabelle2005?  If so, I'd like to, because this is closer to the
contemporary system than Isabelle98.

Please understand that I am not coming at this as a normal user - I am
looking to understand the basic Isabelle HOL system itself, rather than to
understand how to use advanced Isabelle HOL most effectively to perform
proofs.  To do this I will be examining Isabelle source code and interacting
with the ML top level, constructing and/or parsing terms and types,
examining how they get pretty printed, applying basic inference rules and
writing my own basic inference rules.  I imagine that interacting with Proof
General, Isar, etc involves various layers of processing.  What I want is to
interact with the basic system, avoiding these layers (but still being able
to parse/print expressions).

By the way, I am getting somewhere on all of this by reading "Isabelle
Logics: HOL" (referred to but not included in the Isabelle2005
documentation), and by using "read" (if there is a more appropriate way to
parse HOL expressions in the ML toplevel, please tell me how).  I have a
description of the syntax in the above document, but there appears to be no
detailed description of the lex.

Mark





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