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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and