Email Gateway (Aug 18 2022 at 16:19): Email Gateway (Aug 18 2022 at 16:19):From: mark@proof-technologies.com
Hello all,
(I am a newcomer to Isabelle, so apologies for asking what is probably
an incredibly trivial question. I have installed Isabelle 2009 from
source, and have already tried looking at bundled documents such as
'intro.dvi', 'main.dvi', 'system.dvi' and 'tutorial.dvi', but to no
avail.)
Is it possible to do basic ML top level interactive forward proofs in
Isabelle HOL, in a style similar to basic forward proof in HOL Light,
HOL4 and ProofPower? I don't want to use Isar or Proof General, just
the basic ML top level. Starting Isabelle using 'isabelle tty',
followed by entering 'exit' to drop out of Isar sounds promising, but
what do I do then? Just some examples of basic proofs (e.g. "Socrates
is mortal") would be so helpful. I'm not convinced that there is even
the concept of term quotations in Isabelle's basic ML top level. Am I
right? And what are the ML constructor functions for types and terms?
So here is my basic HOL4 forward proof:
(* First some declarations and definitions *)
new_type ("Person",0);
new_constant ("Socrates", :Person);
new_constant ("Man", :Person->bool);
new_constant ("Mortal", :Person->bool);
val ax1 = new_axiom ("Socrates Axiom 1", Man Socrates);
val ax2 = new_axiom ("Socrates Axiom 2", ! p. Man p ==> Mortal
p);
(* Now the proof itself *)
MP (SPEC Socrates ax2) ax1;
This gives me:
val it = |- Mortal Socrates : thm
Can anyone translate this into Isabelle HOL top level commands for me?
Thanks,
Mark Adams
Email Gateway (Aug 18 2022 at 16:19):From: Makarius <makarius@sketis.net>
On Sat, 27 Nov 2010, mark@proof-technologies.com wrote:
Is it possible to do basic ML top level interactive forward proofs in
Isabelle HOL, in a style similar to basic forward proof in HOL Light,
HOL4 and ProofPower? I don't want to use Isar or Proof General, just
the basic ML top level.
You can hardly do anything on the raw ML toplevel, since everything is
managed by the Isar infrastructure theses days, notably the theory context
and the ML toplevel environment.
Starting Isabelle using 'isabelle tty'
Fine.
followed by entering 'exit' to drop out of Isar sounds promising
Bad move. No ML bindings coming after the Pure bootstrap will be
available, because the connection to the formal context is lost.
I'm not convinced that there is even the concept of term quotations in
Isabelle's basic ML top level. Am I right?
Isabelle/ML antiquotations are quite advanced, but you need to do things
in the proper order: quote ML inside Isar, antiquote logical entities
inside ML. See also chapter 0 of
http://www4.in.tum.de/~wenzelm/test/implementation.pdf which will be part
of the next official release.
So here is my basic HOL4 forward proof:
(* First some declarations and definitions *)
new_type ("Person",0);
new_constant ("Socrates",:Person);
new_constant ("Man",:Person->bool);
new_constant ("Mortal",:Person->bool);
val ax1 = new_axiom ("Socrates Axiom 1",Man Socrates);
val ax2 = new_axiom ("Socrates Axiom 2",! p. Man p ==> Mortal p);(* Now the proof itself *)
MP (SPECSocratesax2) ax1;This gives me:
val it = |- Mortal Socrates : thm
Can anyone translate this into Isabelle HOL top level commands for me?
Here is my version for Isabelle2009-2:
theory A imports Main begin;
example_proof;
fix socrates :: 'person;
fix man :: "'person => bool";
fix mortal :: "'person => bool";
assume ax1: "man socrates";
assume ax2: "!!p. man p ==> mortal p";
ML_val {*
val th = @{thm ax2} OF [@{thm ax1}];
writeln (Display.string_of_thm @{context} th);
*};
end;
The old-fashioned semicolons are there for your convenience in the tty.
Myself I composed this quickly with Isabelle/jEdit and than pasted it into
the terminal.
The th result above is pretty-printed without a proper context, unlike the
full version with writeln and Display.string_of_thm.
In order to be productive with Isabelle/ML you should build up your
context in Isar source notation and the experiment with it via small ML
snippets. What is your application anyway? Serious use of Isabelle
outside the Isar system infrastructure is hard to imagine.
Makarius
Email Gateway (Aug 18 2022 at 16:19):From: Lawrence Paulson <lp15@cam.ac.uk>
You might consider downloading an older version from here: http://www.cl.cam.ac.uk/~lp15/archive/
Until around 2005, ML level interaction was still supported.
Larry Paulson
Email Gateway (Aug 18 2022 at 16:20):From: mark@proof-technologies.com
on 27/11/10 11:25 AM, Makarius <makarius@sketis.net> wrote:
In order to be productive with Isabelle/ML you should build up your
context in Isar source notation and the experiment with it via small ML
snippets. What is your application anyway? Serious use of Isabelle
outside the Isar system infrastructure is hard to imagine.
Unlike other users, I'm not aiming to use Isabelle for performing proofs as
such. Rather I'm looking to gain a deep understanding of how Isabelle
works. But thanks for the Isar example for Socrates, which will help me
understand Isar.
on 27/11/10 11:55 AM, Lawrence Paulson <lp15@cam.ac.uk> wrote:
You might consider downloading an older version from here:
http://www.cl.cam.ac.uk/~lp15/archive/Until around 2005, ML level interaction was still supported.
Thanks. I've got Isabelle 2005 with HOL up and running now (curiously, this
required a handful of changes to the Isabelle ML source code to get it
through what purports to be Poly/ML 4.1.4). But how do I enter HOL term and
type quotations into the session? And what are the HOL term and type
constructor functions?
Mark.
Email Gateway (Aug 18 2022 at 16:20):From: Makarius <makarius@sketis.net>
The you should study the "implementation" manual, although it is still
only half through the main concepts. Again see
http://www4.in.tum.de/~wenzelm/test/implementation.pdf
It also tells you about datatypes for types and terms etc.
Makarius
Email Gateway (Aug 18 2022 at 16:20):From: Lawrence Paulson <lp15@cam.ac.uk>
Probably you should look at the papers at http://www.cl.cam.ac.uk/~lp15/papers/isabelle.html
Look particularly at the papers under the tab “of historical interest".
Larry
Email Gateway (Aug 18 2022 at 16:21):From: mark@proof-technologies.com
These documents I'm sure will be very useful, and Makarius's implementation
manual looks especially useful for my purposes. But I also want to carry
out basic interaction - this is just the way I go about learning about the
innards of a system - I like to construct my own terms and experiment. So
can I enter HOL term quotations in Isabelle 2005? And can I use ML
constructor functions to create HOL terms?
Mark.
on 28/11/10 1:26 PM, Makarius <makarius@sketis.net> wrote:
The you should study the "implementation" manual, although it is still
only half through the main concepts. Again see
http://www4.in.tum.de/~wenzelm/test/implementation.pdfIt also tells you about datatypes for types and terms etc.
Makarius
on 28/11/10 1:42 PM, Lawrence Paulson <lp15@cam.ac.uk> wrote:
Probably you should look at the papers at
http://www.cl.cam.ac.uk/~lp15/papers/isabelle.htmlLook particularly at the papers under the tab “of historical interest".
Larry
Email Gateway (Aug 18 2022 at 16:21):From: Makarius <makarius@sketis.net>
The most productive way to do this is to use Isabelle2009-2 with
Isabelle/jEdit, which happens to be part of that distribution as sneak
preview. You can then use it as simple "IDE" for ML: it provides tooltips
for inferred ML types and hyperlinks to the sources (using CONTROL/COMMAND
with mouse hovering).
In the next release this mode of interaction will work even more smoothly.
At some later stage I might also provide a raw ML console for the
low-level tinkering below Isabelle itself, but that is a different story.
Makarius
Email Gateway (Aug 18 2022 at 16:22):From: Lawrence Paulson <lp15@cam.ac.uk>
Note that in the early days, there was no form of antiquotation. You could create a term by parsing the corresponding string or (painfully) using constructor functions.
Larry
Email Gateway (Aug 18 2022 at 16:22):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Not so - my own TPHOLs papers in 2002, 2007 and 2009, plus my track B
presentations in 2002 and 2007, and several other papers presented
elsewhere, all describe work proving things in different areas, all
using Isabelle, none using Isar.
Jeremy
Email Gateway (Aug 18 2022 at 16:22):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Mark,
If I understand the question in your last sentence correctly, the
information you want is in the reference manual, sections 6.5 (terms)
and 6.8 (types, which are contained in terms). (this is applies to the
Isabelle2005 reference manual - it may have been changed since).
../Isabelle2005/doc/ref.dvi
Jeremy
Email Gateway (Aug 18 2022 at 16:22):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear Larry,
Am 29.11.2010 um 12:49 schrieb Lawrence Paulson:
I must give this a try sometime. Does even the standard version of jEdit have this ML mode?
What do you mean exactly ?
You certainly know the ML-environment in Default-ISAR:
ML{*
fun fac x = if x = 0 then 1 else x * fac(x-1)
*}
If you use jEdit, and press the shift- button while hovering,
for example, over the "x" in the ML code, you get directly
type "int" in the display. Makarius demonstrated this already
in the Isabelle developper days in Cambridge, but it may well
be that you missed this session.
It is planned that future versions of jEdit (which we will call Pide
in the future because thats the project that finances Makarius
work here) will do that for any part of inner syntax.
Hhm, I intended to send my mail to Isabelle-users - in case I
adressed this only to you, could you please forward it ?
bu
Larry
On 29 Nov 2010, at 08:25, Burkhart Wolff wrote:
Hmm, i'm one of these dinosaurs that program Isabelle on the ml - level myself. These days, I'll do that inside isar in the ML{} environment which is, I believe, now the best ml environment out there - in jEdit, you can even hover over ml expressions and get the type information. It speeds up ml development even if you do not even target isabelle. You can even try to program without antiquotations, sometimes this is instructive to see what they actually do. However, since they offer a certain infra-structure and discipline to handle proof and theory contexts, they help to avoid the common error to reuse a stale context, which the kernel must avoid in order to become a purely functional transaction machine.
Email Gateway (Aug 18 2022 at 16:22):From: Makarius <makarius@sketis.net>
You can try the jEdit-based Prover IDE (PIDE) in Isabelle2009-2 (from the
Isabelle download website) by invoking "isabelle jedit" on the command
line. Their is also a newer (totally adhoc) snapshot at
http://www.lri.fr/~wenzel/Isar2010-Orsay/download.html which makes
"Isabelle" start the IDE immediately, without Proof General legacy.
In the next official release we will have both side-by side, but Proof
General still the default. It will take quite some time to get such a
substantial change from TTY-based proving to full-scale IDE support into
everyday practice.
Makarius
Email Gateway (Aug 18 2022 at 16:22):From: Makarius <makarius@sketis.net>
The following file might help with the quickstart:
http://www.lri.fr/~wenzel/Isar2010-Orsay/Editor.thy
jEdit is able to open the URL directly, but you cannot save it back in the
same place for obvious reasons.
Makarius
Email Gateway (Aug 18 2022 at 16:33):From: Lawrence Paulson <lp15@cam.ac.uk>
For Isabelle 2005, just use the included documentation. I hope that it is reasonably complete.
You will find lots of useful “read" functions in the files sign.ML and thm.ML.
Larry
Email Gateway (Aug 18 2022 at 16:35):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 18 2022 at 16:36):From: mark@proof-technologies.com
on 6/12/10 2:32 PM, Makarius <makarius@sketis.net> wrote:
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.
Mark
Email Gateway (Aug 18 2022 at 16:36):From: Makarius <makarius@sketis.net>
On Mon, 6 Dec 2010, mark@proof-technologies.com wrote:
on 6/12/10 2:32 PM, Makarius <makarius@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
Email Gateway (Aug 18 2022 at 16:37):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
On 06/12/10 16:19, Makarius wrote:
On Mon, 6 Dec 2010, mark@proof-technologies.com wrote:
on 6/12/10 2:32 PM, Makarius <makarius@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.Mark,
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
context" onlyAbove 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.
Jeremy
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
Email Gateway (Aug 18 2022 at 16:37):From: mark@proof-technologies.com
Thanks for you replies everyone. It sounds like I need to take a look at
Isar in Isabelle2009 then. I'll also be looking at Isabelle98.
on 6/12/10 4:20 PM, Makarius <makarius@sketis.net> wrote:
My understanding was that you want to see the "proof technologies" behind
the Isabelle system :-)
Aha I see! :)
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'll be taking a look at Isabelle98 then. Basic stone age is what I need.
Thanks.
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.
Therein lies the difference between us. To understand HOL4 I first look at
HOL90 in detail!
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.
In which document can I find a comprehensive description of the (presumably
ASCII) lex (any version of Isabelle will do for starters)? And does the
lex vary between logics?
Mark.
Email Gateway (Aug 18 2022 at 16:37):From: mark@proof-technologies.com
Jeremy, thanks for the reply.
on 6/12/10 6:10 PM, Jeremy Dawson <jeremy@rsise.anu.edu.au> wrote:
On 06/12/10 16:19, Makarius wrote:
On Mon, 6 Dec 2010, mark@proof-technologies.com wrote:
You can certainly do ML interaction effectively in Isabelle2005 - it's
the way I normally use Isabelle.
Hmm. I'll carry on looking into Isabelle2005 too then.
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 Isarfun in_tac sg st = (rtac insertI1 ORELSE' (rtac insertI2 THEN' in_tac))
sg st ;....
Excellent, thanks.
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.
Yes, so do I... Maybe they are talking about Isabelle2009-2?
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.
Thanks for the offer, but I have already managed to install Isabelle2005
(with Poly/ML 4.1.4) and Isabelle2009 (with Poly/ML 5.2.1) from source. I'm
now building Isabelle 2009-2 (with Poly/ML 5.2.1) from source.
Incidentally, Isabelle2005 required a few source code changes to get it
through Poly/ML 4.1.4. This seems strange to me, and sounds like a
configuration management problem with either the precise version of
Isabelle2005 or the precise version of Poly/ML 4.1.4 source code that
appears on the web. I can provide details of the changes required if anyone
is interested..
Mark.
Email Gateway (Aug 18 2022 at 16:37):From: Makarius <makarius@sketis.net>
If "lex" means the lexical syntax here, see the two sections called
"Lexical matters" in the isar-ref manual. There are two, since Isabelle
has outer and inner syntax layers.
Isabelle does not use ASCII code, but "Isabelle symbol" notation which
provides an infinite alphabet of basic text entities. See the section
"Strings of symbols" in the implementation manual.
This refers both to the current official release Isabelle2009-2. If you
want to hear a longer story over 10-20 years of history, I can also do
that.
Makarius
Email Gateway (Aug 18 2022 at 16:37):From: Makarius <makarius@sketis.net>
On Mon, 6 Dec 2010, Jeremy Dawson wrote:
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 Isarfun 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])),
As a general rule of thumb, you can do always do more in Isar than in the
stone age -- in the same way, you can do more with a computer that runs
Linux or Mac OS X, compared to the bare metal. This does not mean that
Linus Torvalds or Apple will let you poke around in hardware registers,
though.
See the "tactic" proof method in the isar-ref manual how to embed ML
tactic expressions into Isar source text.
BTW, old Simp_tac and Safe_tac refer to "the_context()" which is not
always the same as your goal context, i.e. CI_Rls.thy above. This is why
I have called it a running gag from many years ago.
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
context" only
An old style "theory context" is not a proper context. You are also
subject to "the_context()" confusion here, i.e. you can never be quite
sure what you get. Good that we got rid of the "read" function long ago.
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.
Hardly anybody on the mailing list will remember "old-style" theories.
This is just historical cruft, even in Isabelle2005. Gladly this has been
deleted long ago.
Makarius
Email Gateway (Aug 18 2022 at 16:38):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
On 06/12/10 20:17, Makarius wrote:
On Mon, 6 Dec 2010, Jeremy Dawson wrote:
See the "tactic" proof method in the isar-ref manual how to embed ML
tactic expressions into Isar source text.A warning, though - this often doesn't work. One of the reasons is
described in the following paragraph.BTW, old Simp_tac and Safe_tac refer to "the_context()" which is not
always the same as your goal context, i.e. CI_Rls.thy above. This is
why I have called it a running gag from many years ago.I think this is a legitimate criticism, but that the sensible solution
would have been to change these tactics so that they use the theory
context of the theorem representing the proof underway.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
context" onlyAn old style "theory context" is not a proper context. You are also
subject to "the_context()" confusion here, i.e. you can never be quite
sure what you get. Good that we got rid of the "read" function long ago.
As for the general issue of using an implicit, rather than explicit,
context, well, it isn't so long ago that someone thought it was a _good_
idea to introduce the "Goal" command as an alternative to "goal" (for
this discussion, Goal = goal (the_context ())). That is, different
people have different opinions on this sort of issue.
Anyway what I mean is that "read", as I understand it, uses only a
"theory context", not a "proper context" (which, as I understand it,
doesn't exist unless you're using Isar).
I think that another legitimate criticism of the ML interface is that
"read" and "prin" refer to the context of the most recent interactive
proof, rather than the_context (), but that fixing this doesn't require
chucking out the entire ML interface.
as for never being quite sure of what [theory context] you get, I found
this problem a good deal worse using Isar, because (I think) the theory
context keeps changing while an Isar file is being processed
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.Hardly anybody on the mailing list will remember "old-style" theories.
This is just historical cruft, even in Isabelle2005. Gladly this has
been deleted long ago.whatever the relative merits of new-style theories versus old-style
theories, the fact is that massive amounts of proofs using old-style
theories exist, and people are currently developing further proofs build
upon them. So what make you glad makes recent versions of Isabelle
unusable for other people
Jeremy
Makarius
Email Gateway (Aug 18 2022 at 16:38):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Jeremy & Co,
May I kindly suggest to make this a private thread among stone age
users? Probably only a handful of people know what you are talking about
and even fewer are interested in the details of ML level interaction. If
anybody else, apart from the participants of this thread, is interested
in the details, they should speak up now and I take back what I wrote.
Thanks
Tobias
Jeremy Dawson schrieb:
Email Gateway (Aug 18 2022 at 16:38):From: Brian Huffman <brianh@cs.pdx.edu>
I, for one, would be interested in hearing the rest of this discussion.
Email Gateway (Aug 18 2022 at 16:38):From: Michael Norrish <Michael.Norrish@nicta.com.au>
I'm quite interested in the details.
Michael
Email Gateway (Aug 18 2022 at 16:38):From: Alexander Krauss <krauss@in.tum.de>
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 'Isabelle architecture'. 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
Email Gateway (Aug 18 2022 at 16:38):From: Steven Obua <steven.obua@googlemail.com>
On 08.12.2010, at 10:19, Alexander Krauss wrote:
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.
I think that this point is a good one and deserves special attention.
a) You need to pass contexts around in purely functional programming.
b) Most of the time, you don't want to deal with this passing around explicitly.
A purely functional programming language should deal with this in a natural and pretty way
(nope, monads are not natural; and they are ugly). If there just were such a language ...
I think that much confusion comes from confusing (1) and (4). Maybe
reimlementing (1) in LISP (as in Edinburgh LCF) could solve this
problem :-)).
Why not try Babel-17 instead of LISP? A new and much refined version of it will come out this Friday, together with a Netbeans plugin :-)
Email Gateway (Aug 18 2022 at 16:38):From: Makarius <makarius@sketis.net>
Very nice explanation -- including all your other text from above that I
have suppressed for brevity. I did not know the wording of Isar as
Isabelle architecture' so far.
There is little left to add, apart from (5) Isabelle/Scala and (6) Prover
IDE. The latter already helps a lot in exploring Isabelle/ML right now,
and at a later stage raw ML access will return for bare bones system
maintenance, but that is not very signifant compared to many other things
that are still missing.
Makarius
Email Gateway (Aug 18 2022 at 16:39):From: Lawrence Paulson <lp15@cam.ac.uk>
Historically, I see it like this. By 1989, we had the basics: higher-order unification as the inference mechanism and higher-order logic as the logical framework. A couple of years later, we had order-sorted polymorphism. By around 2000, with innovations such as axiomatic type classes, inductive and datatype definitions and the classical reasoner, classic Isabelle could be described as mature. Isar represents a new departure, but what is particularly nice is how well it fits on the old logical framework infrastructure. One might imagine that everything had been foreseen at the start, but this isn't true at all. All this is to say that “to understand Isabelle" could refer to many very different things.
Larry
Email Gateway (Aug 18 2022 at 16:41):From: mark@proof-technologies.com
(apologies for a week of absence...)
on 28/11/10 8:54 PM, Lawrence Paulson <lp15@cam.ac.uk> wrote:
Note that in the early days, there was no form of antiquotation. You could
create a term by parsing the corresponding string or (painfully) using
constructor functions.
Larry
I see, so would I be right in saying that the "read" function is the
appropriate ML function for parsing a string into a HOL term? Is there a
corresponding function for HOL types? And where is the best place to find a
complete description of the lex/syntax of Isabelle HOL terms and types (for
Isabelle 2005)?
on 29/11/10 10:24 AM, Jeremy Dawson <jeremy@rsise.anu.edu.au> wrote:
If I understand the question in your last sentence correctly, the
information you want is in the reference manual, sections 6.5 (terms)
and 6.8 (types, which are contained in terms). (this is applies to the
Isabelle2005 reference manual - it may have been changed since).
That's one of the two things I was looking for. Thanks that helps.
Mark.
On 28/11/10 14:32, mark@proof-technologies.com wrote:
But I also want to carry out basic interaction - this is just the way I
go
about learning about the innards of a system - I like to construct my
own terms and experiment. So can I enter HOL term quotations in
Isabelle 2005? And can I use ML constructor functions to create
HOL terms?Mark.
Last updated: Apr 26 2024 at 04:17 UTC