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 sources.

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 as well.

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.


	Makarius





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