Re: [isabelle] How do I do stone age interaction?
On Mon, 6 Dec 2010, mark at proof-technologies.com wrote:
on 6/12/10 2:32 PM, Makarius <makarius at sketis.net> wrote:
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).
My understanding was that you want to see the "proof technologies" behind
the Isabelle system :-) I still maintain that the best way to do it is to
use Isabelle/ML through the Isar toplevel, either with Proof General or
the more recent Isabelle/jEdit, which also gives you quick links to the
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.
Above you say "Isabelle HOL" as if that would be the system, but in
reality HOL is a big library within the general Isabelle framework.
Dropping out of the Isar loop, you won't see anything of the HOL name
space, and thus cannot use Isabelle/HOL.
The reason why Larry mentioned Isabelle2005 is because that is the last
release that still happens to have some old layers side-by-side with the
current context management that was originally introduced for the Isar
proof language in 1999. E.g. the "read" function refers to the implicit
"goal context" of the old goal package that has finally been deleted this
year. There is yet another theory context accessed via "the_context()"
which later became a running gag in internal circles, until it was deleted
Isabelle2005 is a rock solid distribution, but also a particularly
confusing one due to many old layers being still in there. This is why I
mentioned the more basic Isabelle98, although it lacks the main concepts
of contempory Isabelle.
Anyway, when I want to understand Linux, I also stay within the normal
user space, instead of booting into single user mode with the init process
running a single instance of bash.
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.
The old HOL manual has hardly ever been maintained in the past 10 years.
The term syntax is defined in library space in the context. The
print_syntax command will tell you some aspects of it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and