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



Dear stone age enthusiasts and others,

In the present discussions, there seem to be some misunderstandings
due to conflating two meanings of the word 'Isar'. It means two
things: a) the language in which most users write specifications and
proofs, and b) the management layer that interprets the above
language, but also deals with contexts, data management, system state
and transactions, theory management etc. Maybe for the latter meaning
one could read 'Isar' as '*Is*abelle *ar*chitecture'. It was initially
introduced to support the language, but it is now central to the whole
system.

While it is perfectly reasonable not to use Isar-the-language (in fact
automated proof tools typically don't, yet they produce specifications
and proofs similar to the ones written by users), in recent Isabelle
versions (starting with ca. 2007/8) there is no way of circumventing
Isar-the-architecture. Like every architecture, it has its pros and
cons, but there is no way of ignoring its existence.

Isar-the-architecture provides the full SML programming language,
extended with antiquotations to refer to logical entities from static
(compile time) contexts. To use this, ML code must obey some
structuring principles, and the most important one is that contexts
(i.e. values of type Proof.context, theory, or local_theory, depending
on the application) must be passed around explicitly. Anyone familiar
with the notion of pure functional programming should find this very
natural. For example, a theorem declaration (in the global theory) is
a function of type "theory -> theory", and most tactics that do
something interesting must depend on a context. So does parsing and
pretty printing. Jeremy's example looks like it is very easy to port
to current Isabelle by using explicit context passing. Many people on
this list will be happy to demonstrate this on self-contained
examples. Implicit context passing is only provided by
Isar-the-language.

As it was said, Isabelle 2005 still supported unmanaged interaction to
some extent, and this is what Jeremy is using. I personally don't know
of any other (active) user of this model, but I would be curious to
hear about any.

In other words, the current model is roughly

(4) Isabelle/ML embedded into Isar
 --------------------------------------
(3) Isar language
 --------------------------------------
(2) Isar infrastructure
 --------------------------------------
(1) Raw ML toplevel (provided by compiler)


(4) is where you actually work in when interacting in ML, and if you
want to ignore (3), you can do so by using the embedded language only.
From (1) you hardly get anything useful. From what Mark wrote, I
assume that he is more interested in the logical part of the
internals, not so much the management part. IMHO the easiest way to
explore this in Isabelle2009-2 is using (4). In Isabelle2005, you can
still use (1), but what you get is, of course, an impression of how
Isabelle2005 worked.

I think that much confusion comes from confusing (1) and (4). Maybe
reimlementing (1) in LISP (as in Edinburgh LCF) could solve this
problem :-)).

Alex





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