Email Gateway (Aug 22 2022 at 13:32): Email Gateway (Aug 22 2022 at 13:32):From: Mark Adams <mark@proof-technologies.com>
Dear list,
Is there an equivalent to turnstile in Isabelle? In good old
mathematics and in other HOL systems, the turnstile (|-) has two roles:
to indicate that a theorem has been proved, and to separate any
assumptions of the theorem from its conclusion.
In Isabelle2005, if you return a theorem in the read-eval-print-loop,
then if it has one assumption 'P' and conclusion 'Q' then it gets
printed as "Q [P]" (if the flag for showing hypotheses is set), but just
as "Q" if there are no assumptions, and so this corresponds to the
second role.
But what about in more recent Isabelles? I know that there's no
read-eval-print-loop as such, and that in Isar scripts you write
"theorem" before a formula, which is a bit like the first role but not
quite because until the proof is complete it states the intention that
the formula will be proved rather than that it has been proved. Are
there ways of displaying lists of theorems, and if so how are these
presented? I note that the printer for "Q [P]" is still there in the
Isabelle Pure source. If anyone could shed any light on all of this
then I'd be most grateful.
Mark.
Email Gateway (Aug 22 2022 at 13:33):From: Peter Lammich <lammich@in.tum.de>
On Di, 2016-06-07 at 00:51 +0100, Mark Adams wrote:
Dear list,
Is there an equivalent to turnstile in Isabelle? In good old
mathematics and in other HOL systems, the turnstile (|-) has two roles:
to indicate that a theorem has been proved, and to separate any
assumptions of the theorem from its conclusion.In Isabelle2005, if you return a theorem in the read-eval-print-loop,
then if it has one assumption 'P' and conclusion 'Q' then it gets
printed as "Q [P]" (if the flag for showing hypotheses is set), but just
as "Q" if there are no assumptions, and so this corresponds to the
second role.But what about in more recent Isabelles? I know that there's no
read-eval-print-loop as such, and that in Isar scripts you write
"theorem" before a formula, which is a bit like the first role but not
quite because until the proof is complete it states the intention that
the formula will be proved rather than that it has been proved. Are
there ways of displaying lists of theorems, and if so how are these
presented? I note that the printer for "Q [P]" is still there in the
Isabelle Pure source. If anyone could shed any light on all of this
then I'd be most grateful.
The hypothesis are used in Isabelle merely internally, and the
standard-user should not see them. Theorems are presented as
meta-implications "P1==>...==>Pn==>Q", or, syntax-sugared "[| P1;...;Pn
|] ==> Q". This is also the way they are printed.
In Isar, you can use the "thm" command to print (a list of) theorems.
To state a theorem, you can either use meta-implications, or the
"long-goal" format:
lemma foo:
assumes P1 and ... and Pn
shows Q
By the very design of Isabelle, every theorem has been proved (or has a
pending future proof attached [Makarius, correct me if I'm wrong
here ;)])
Email Gateway (Aug 22 2022 at 13:33):From: Makarius <makarius@sketis.net>
On 07/06/16 01:51, Mark Adams wrote:
Is there an equivalent to turnstile in Isabelle? In good old
mathematics and in other HOL systems, the turnstile (|-) has two roles:
to indicate that a theorem has been proved, and to separate any
assumptions of the theorem from its conclusion.
See also chapter 2 about "Primitive logic" of the "implementation"
manual. It explains the role of the Pure logic as framework for
higher-order natural deduction in various object-logics, where HOL is
the main example.
The turnstile is there, but it belongs to the system infrastructure for
local context management, and thus is hardly ever encountered in user
tools and applications.
In Isabelle2005, if you return a theorem in the read-eval-print-loop,
then if it has one assumption 'P' and conclusion 'Q' then it gets
printed as "Q [P]" (if the flag for showing hypotheses is set), but just
as "Q" if there are no assumptions, and so this corresponds to the
second role.
Isabelle2005 is mainly of historic interest and no longer used in
serious applications. It is remarkable in being the last version of
Isabelle that still has remains from the 1990s, so it is possible to
pretend that it resembles "other HOL systems".
Note that the Isar concepts have already taken over the lead in Isabelle
around 2002. Thus Isabelle2005 is just for prolonged nostalgy: one needs
to go back to Isabelle98 to be authentic.
Anyway, Q [P] is just Larry Paulson's notation for P |- Q. The context P
is only informative when there is something wrong in the internal
context management, so it is not printed by default, and when printed it
is done in non-intrusive postfix notation.
But what about in more recent Isabelles? I know that there's no
read-eval-print-loop as such, and that in Isar scripts
Isar is about structured proof documents or proof texts, not
"scripts". It is important to use the proper terminology to get some
idea how things work.
Isabelle is a document-oriented proof composition tool, with timeless
and stateless continuous checking.
"theorem" before a formula, which is a bit like the first role but not
quite because until the proof is complete it states the intention that
the formula will be proved rather than that it has been proved.
The 'theorem' command is more than an old-fashioned "goal" statement. It
builds up a context and states conclusions from that context: the result
is a Pure rule.
This is ubiquitious in the Isabelle/Isar documentation, e.g. "isar-ref"
or "implementation" manual.
Are there ways of displaying lists of theorems, and if so how are these
presented? I note that the printer for "Q [P]" is still there in the
Isabelle Pure source. If anyone could shed any light on all of this
then I'd be most grateful.
Here is an example for current Isabelle2016:
theorem test:
fixes x y z :: 'a
assumes "x = y" and "y = z"
shows "x = z" and "z = x"
using assms by simp_all
ML ‹
val thms = @{thms test};
map (fn thm => (Thm.hyps_of thm, Thm.prop_of thm)) thms;
›
The hyps are empty, because the result lives in a global context.
Here is an example with a local context:
context
fixes x y z :: 'a
assumes asms: "x = y" "y = z"
begin
theorem test': "x = z" and "z = x"
using asms by simp_all
ML ‹
val thms = @{thms test'};
map (fn thm => (Thm.hyps_of thm, Thm.prop_of thm)) thms;
›
end
ML ‹
val thms = @{thms test'};
map (fn thm => (Thm.hyps_of thm, Thm.prop_of thm)) thms;
›
Hyps are potentially non-empty in the local context, and empty outside
of it. Note that hyps record aspects of the proof in the thm object.
This is also the reason why in recent years, hyps are hardly ever
printed: this would lead to non-determinism, depending on the the
accidental state of a future proof process that might fail or finish
only later.
Makarius
Email Gateway (Aug 22 2022 at 13:33):From: Makarius <makarius@sketis.net>
A thm value is indeed only a promise to finish a proof eventually. For
fully authentic results, one needs to do a batch run with "isabelle
build", which forms a global join on all open ends in the very end, and
potential errors are exposed.
This reform of thm-ness goes back to 2007/2008, when parallel proof
construction in Isabelle emerged for the first time.
Makarius
Last updated: Apr 19 2024 at 16:20 UTC