Re: [isabelle] How do I do stone age interaction?
On 06/12/10 16:19, Makarius wrote:
> 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.
You can certainly do ML interaction effectively in Isabelle2005 - it's
the way I normally use Isabelle.
>> Please understand that I am not coming at this as a normal user - I
>> am looking to understand the basic Isabelle HOL system itself,
I regard, this as pretty normal actually.
>> rather than to understand how to use advanced Isabelle HOL most
>> effectively to perform proofs. To do this I will be examining
The ML layer certainly helps you perform proofs effectively - just by
way of example here is something I wrote this afternoon, which I
understand cannot be done in Isar
fun in_tac sg st = (rtac insertI1 ORELSE' (rtac insertI2 THEN' in_tac))
sg st ;
val _ = qed_goalw "inv_rule_aidps" CI_Rls.thy
(rule_defs @ rule_lists) "inv_rule_set (PC ` aidps)"
(fn _ => [ Simp_tac 1, rewtac inv_rule_set_def, Safe_tac,
(TRYALL (EVERY' [rtac exI, rtac conjI, rtac refl])),
(TRYALL (EVERY' [rtac drl.singleI, in_tac])),
(this last step reduces 13 subgoals to 1)
>> 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.
If "proper context" means something of the type Proof.context, then this
isn't so - the "read" function implicitly uses an old style "theory
> 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.
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.
> 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.
I don't recall from earlier emails in this thread whether you actually
have got Isabelle2005 running. As far as I can see it requires an old
version of PolyML - namely 4.1.4. I don't know whether that is easily
available now, but I can give you a copy (for x86_linux) if required.
> 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