author nipkow Wed, 02 Oct 2002 15:26:07 +0200 changeset 13620 61a23a43b783 parent 13619 584291949c23 child 13621 75ae05e894fa
*** empty log message ***
--- a/doc-src/TutorialI/IsarOverview/Isar/Induction.thy	Tue Oct 01 20:54:17 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy	Wed Oct 02 15:26:07 2002 +0200
@@ -147,7 +147,7 @@
case 0 thus ?case by simp
next
case (Suc n)   -- {*\isakeyword{fix} @{term m} \isakeyword{assume} @{text Suc}: @{text[source]"?m < n \<Longrightarrow> P ?m"} @{prop[source]"m < Suc n"}*}
-    show ?case     -- {*@{term ?case}*}
+    show ?case    -- {*@{term ?case}*}
proof cases
assume eq: "m = n"
from Suc and A have "P n" by blast
@@ -165,7 +165,7 @@

The statement of the lemma is interesting because it deviates from the style in
the Tutorial~\cite{LNCS2283}, which suggests to introduce @{text"\<forall>"} or
-@{text"\<longrightarrow>"} into a theorem to strengthen it for induction. In structured Isar
+@{text"\<longrightarrow>"} into a theorem to strengthen it for induction. In Isar
proofs we can use @{text"\<And>"} and @{text"\<Longrightarrow>"} instead. This simplifies the
proof and means we do not have to convert between the two kinds of
connectives.
@@ -174,7 +174,7 @@
subsection{*Rule induction*}

text{* HOL also supports inductively defined sets. See \cite{LNCS2283}
-for details. As an example we define our own version of reflexive
+for details. As an example we define our own version of the reflexive
transitive closure of a relation --- HOL provides a predefined one as well.*}
consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
inductive "r*"
@@ -227,9 +227,9 @@
see very clearly how things fit together and permit ourselves the
obvious forward step @{text"IH[OF B]"}.

-The notation \isakeyword{case}~\isa{(constructor} \emph{vars}\isa{)}
-is also supported for inductive definitions. The constructor is (the
-names of) the rule and the \emph{vars} fix the free variables in the
+The notation \isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}'
+is also supported for inductive definitions. The \emph{constructor} is (the
+name of) the rule and the \emph{vars} fix the free variables in the
rule; the order of the \emph{vars} must correspond to the
\emph{alphabetical order} of the variables as they appear in the rule.
For example, we could start the above detailed proof of the induction
@@ -291,7 +291,7 @@

The third case is only shown in gory detail (see \cite{BauerW-TPHOLs01}
for how to reason with chains of equations) to demonstrate that the
-\isakeyword{case}~\isa{(constructor} \emph{vars}\isa{)} notation also
+\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}' notation also
works for arbitrary induction theorems with numbered cases. The order
of the \emph{vars} corresponds to the order of the
@{text"\<And>"}-quantified variables in each case of the induction
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Tue Oct 01 20:54:17 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Oct 02 15:26:07 2002 +0200
@@ -97,9 +97,9 @@
\end{center}
where \emph{fact} stands for the name of a previously proved
proposition, e.g.\ an assumption, an intermediate result or some global
-theorem, which may also be modified with @{text of}, @{text OF} etc.
+theorem, which may also be modified with @{text OF} etc.
The \emph{fact} is piped'' into the \emph{proof}, which can deal with it
-how it choses. If the \emph{proof} starts with a plain \isakeyword{proof},
+how it chooses. If the \emph{proof} starts with a plain \isakeyword{proof},
an elimination rule (from a predefined list) is applied
whose first premise is solved by the \emph{fact}. Thus the proof above
is equivalent to the following one: *}
@@ -201,7 +201,7 @@
for \isakeyword{from}~@{term A1}~\dots~@{term An}.  This avoids having to
introduce names for all of the sequence elements.  *}

-text{* Although we have only seen a few introduction and elemination rules so
+text{* Although we have only seen a few introduction and elimination rules so
far, Isar's predefined rules include all the usual natural deduction
rules. We conclude our exposition of propositional logic with an extended
example --- which rules are used implicitly where? *}
@@ -278,7 +278,7 @@
text{*\noindent Any formula may be followed by
@{text"("}\isakeyword{is}~\emph{pattern}@{text")"} which causes the pattern
to be matched against the formula, instantiating the @{text"?"}-variables in
-the pattern. Subsequent uses of these variables in other terms simply causes
+the pattern. Subsequent uses of these variables in other terms causes
them to be replaced by the terms they stand for.

We can simplify things even more by stating the theorem by means of the
@@ -440,12 +440,12 @@
assume "y \<in> ?S"
hence "y \<notin> f y"   by simp
hence "y \<notin> ?S"    by(simp add:fy)
-      thus False        by contradiction
+      thus False         by contradiction
next
assume "y \<notin> ?S"
hence "y \<in> f y"   by simp
hence "y \<in> ?S"    by(simp add:fy)
-      thus False        by contradiction
+      thus False         by contradiction
qed
qed
qed
@@ -546,7 +546,7 @@
text{*\noindent You may need to resort to this technique if an
automatic step fails to prove the desired proposition.

-When converting a proof from tactic-style into Isar you can proceeed
+When converting a proof from tactic-style into Isar you can proceed
in a top-down manner: parts of the proof can be left in script form
while to outer structure is already expressed in Isar. *}

--- a/doc-src/TutorialI/IsarOverview/Isar/document/intro.tex	Tue Oct 01 20:54:17 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/intro.tex	Wed Oct 02 15:26:07 2002 +0200
@@ -8,7 +8,7 @@
language but concentrate on the essentials. Neither do we give a
formal semantics of Isar. Instead we introduce Isar by example. Again
this is intentional: we believe that the language speaks for
-itself'' in the same way that traditional mathamtical proofs do, which
+itself'' in the same way that traditional mathematical proofs do, which
are also introduced by example rather than by teaching students logic
first. A detailed exposition of Isar can be found in Markus Wenzel's
PhD thesis~\cite{Wenzel-PhD} and the Isar reference
@@ -27,26 +27,23 @@
tactics.

A radically different approach was taken by the Mizar
-system
-%~\cite{Mizar}
-where proofs are written a stylized language akin to that used in
-ordinary mathematics texts. The most important argument in favour of a
-mathematics-like proof language is communication: as soon as not just
-the theorem but also the proof becomes an object of interest, it
-should be readable.  From a system development point of view there is
-a second important argument against tactic-style proofs: they are much
-harder to maintain when the system is modified. The reason is as
-follows. Since it is usually quite unclear what exactly is proved at
-some point in the middle of a command sequence, updating a failed
-proof often requires executing the proof up to the point of failure
-using the old version of the system.  In contrast, mathematics-like
-proofs contain enough information to tell you what is proved at any
-point.
+system~\cite{Rudnicki92} where proofs are written in a stylized language akin
+to that used in ordinary mathematics texts. The most important argument in
+favour of a mathematics-like proof language is communication: as soon as not
+just the theorem but also the proof becomes an object of interest, it should
+be readable.  From a system development point of view there is a second
+important argument against tactic-style proofs: they are much harder to
+maintain when the system is modified. The reason is as follows. Since it is
+usually quite unclear what exactly is proved at some point in the middle of a
+command sequence, updating a failed proof often requires executing the proof
+up to the point of failure using the old version of the system.  In contrast,
+mathematics-like proofs contain enough information to tell you what is proved
+at any point.

For these reasons the Isabelle system, originally firmly in the
LCF-tradition, was extended with a language for writing structured
proofs in a mathematics-like style. As the name already indicates,
-Isar was certainly inspired by Mizar. However, there are very many
+Isar was certainly inspired by Mizar. However, there are many
differences. For a start, Isar is generic: only a few of the language
constructs described below are specific to HOL; many are generic and
thus available for any logic defined in Isabelle, e.g.\ ZF.
@@ -86,9 +83,8 @@
\end{center}
A proof can be either compound (\isakeyword{proof} --
\isakeyword{qed}) or atomic (\isakeyword{by}). A \emph{method} is a
-proof method offered by the underlying theorem prover, for example
-\isa{rule} or \isa{simp} in Isabelle.  Thus this grammar is
-generic both w.r.t.\ the logic and the theorem prover.
+proof method (tactic) offered by the underlying theorem prover.
+Thus this grammar is generic both w.r.t.\ the logic and the theorem prover.

This is a typical proof skeleton:
\begin{center}
@@ -114,18 +110,18 @@
notions and notation from Isabelle~\cite{LNCS2283}. Isabelle's
meta-logic offers an implication $\Longrightarrow$ and a universal quantifier $\bigwedge$
for expressing inference rules and generality. Iterated implications
-$A_1 \Longrightarrow \dots A_n \Longrightarrow A$ may be abbreviated to $[\!| A_1; \dots; A_n -|\!] \Longrightarrow A$. Applying a theorem $A \Longrightarrow B$ (named \isa{T}) to a theorem
+$A_1 \Longrightarrow \dots A_n \Longrightarrow A$ may be abbreviated to $[\![ A_1; \dots; A_n +]\!] \Longrightarrow A$. Applying a theorem $A \Longrightarrow B$ (named \isa{T}) to a theorem
$A$ (named \isa{U}) is written \isa{T[OF U]} and yields theorem $B$.

Isabelle terms are simply typed. Function types are
written $\tau_1 \Rightarrow \tau_2$.

-Free variables that may be instantiated (logical variables'' in
-Prolog parlance) are prefixed with a \isa{?}. Typically, theorems are
-stated with ordinary free variables but after the proof those are
-replaced by \isa{?}-variables. Thus the theorem can be used with
-arbitrary instances of its free variables.
+Free variables that may be instantiated (logical variables'' in Prolog
+parlance) are prefixed with a \isa{?}. Typically, theorems are stated with
+ordinary free variables but after the proof those are automatically replaced
+by \isa{?}-variables. Thus the theorem can be used with arbitrary instances
+of its free variables.

Isabelle/HOL offers all the usual logical symbols like $\longrightarrow$, $\land$,
$\forall$ etc. Proof methods include \isa{rule} (which performs a backwards
@@ -141,12 +137,11 @@
natural deduction. Section~\ref{sec:Induct} is dedicated to induction,
the key reasoning principle for computer science applications.

-There are at least two further areas where Isar provides specific
-support, but which we do not document here: reasoning by chains of
-(in)equations is described elsewhere~\cite{BauerW-TPHOLs01}, whereas
-reasoning about axiomatically defined structures by means of so called
-locales'' \cite{KWP-TPHOLs99} is only described in a very early
-form and has evolved much since then.
+There are at least two further areas where Isar provides specific support,
+but which we do not document here. Reasoning by chains of (in)equations is
+described elsewhere~\cite{BauerW-TPHOLs01}.  Reasoning about axiomatically
+defined structures by means of so called locales'' was first described in
+\cite{KWP-TPHOLs99} but has evolved much since then.

Do not be mislead by the simplicity of the formulae being proved,
especially in the beginning. Isar has been used very successfully in
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.bib	Tue Oct 01 20:54:17 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.bib	Wed Oct 02 15:26:07 2002 +0200
@@ -6,7 +6,7 @@
title={Calculational Reasoning Revisited --- an {Isabelle/Isar} Experience},
booktitle={Theorem Proving in Higher Order Logics, TPHOLs 2001},
editor={R. Boulton and P. Jackson},
-year=2001,publisher=Springer,series=LNCS,volume=2152}
+year=2001,publisher=Springer,series=LNCS,volume=2152,pages="75--90"}

@book{LCF,author="M.C.J. Gordon and Robin Milner and C.P. Wadsworth",
title="Edinburgh {LCF}: a Mechanised Logic of Computation",
@@ -24,6 +24,15 @@
publisher=Springer,series=LNCS,volume=2283,year=2002,
note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}

+@article{KleinN-TCS,author={Gerwin Klein and Tobias Nipkow},
+title={Verified Bytecode Verifiers},
+journal=TCS,year=2002,note={To appear}}
+
+@InProceedings{Rudnicki92,author={P. Rudnicki},
+title={An Overview of the {Mizar} Project},
+booktitle={Workshop on Types for Proofs and Programs},
+year=1992,organization={Chalmers University of Technology}}
+
@manual{Isar-Ref-Man,author="Markus Wenzel",
title="The Isabelle/Isar Reference Manual",
organization={Technische Universit{\"a}t M{\"u}nchen},year=2002,