--- a/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Mon Dec 23 12:01:47 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Sun Dec 29 08:56:24 2002 +0100
@@ -12,34 +12,43 @@
text{* We have already met the @{text cases} method for performing
binary case splits. Here is another example: *}
-lemma "P \<or> \<not> P"
+lemma "\<not> A \<or> A"
proof cases
- assume "P" thus ?thesis ..
+ assume "A" thus ?thesis ..
next
- assume "\<not> P" thus ?thesis ..
+ assume "\<not> A" thus ?thesis ..
qed
-text{*\noindent Note that the two cases must come in this order.
-This form is appropriate if @{term P} is textually small. However, if
-@{term P} is large, we do not want to repeat it. This can be avoided by
-the following idiom *}
+text{*\noindent The two cases must come in this order because @{text
+cases} merely abbreviates @{text"(rule case_split_thm)"} where
+@{thm[source] case_split_thm} is @{thm case_split_thm}. If we reverse
+the order of the two cases in the proof, the first case would prove
+@{prop"\<not> A \<Longrightarrow> \<not> A \<or> A"} which would solve the first premise of
+@{thm[source] case_split_thm}, instantiating @{text ?P} with @{term "\<not>
+A"}, thus making the second premise @{prop"\<not> \<not> A \<Longrightarrow> \<not> A \<or> A"}.
+Therefore the order of subgoals is not always completely arbitrary.
-lemma "P \<or> \<not> P"
-proof (cases "P")
+The above proof is appropriate if @{term A} is textually small.
+However, if @{term A} is large, we do not want to repeat it. This can
+be avoided by the following idiom *}
+
+lemma "\<not> A \<or> A"
+proof (cases "A")
case True thus ?thesis ..
next
case False thus ?thesis ..
qed
-text{*\noindent which is simply a shorthand for the previous
-proof. More precisely, the phrase `\isakeyword{case}~@{text True}'
-abbreviates `\isakeyword{assume}~@{text"True: P"}'
-and analogously for @{text"False"} and @{prop"\<not>P"}.
-In contrast to the previous proof we can prove the cases
-in arbitrary order.
+text{*\noindent which is like the previous proof but instantiates
+@{text ?P} right away with @{term A}. Thus we could prove the two
+cases in any order. The phrase `\isakeyword{case}~@{text True}'
+abbreviates `\isakeyword{assume}~@{text"True: A"}' and analogously for
+@{text"False"} and @{prop"\<not>A"}.
-The same game can be played with other datatypes, for example lists:
-\tweakskip
+The same game can be played with other datatypes, for example lists,
+where @{term tl} is the tail of a list, and @{text length} returns a
+natual number:
+\Tweakskip
*}
(*<*)declare length_tl[simp del](*>*)
lemma "length(tl xs) = length xs - 1"
@@ -60,27 +69,15 @@
However, sometimes one may have to. Hence Isar offers a simple scheme for
naming those variables: replace the anonymous @{text Cons} by
@{text"(Cons y ys)"}, which abbreviates `\isakeyword{fix}~@{text"y ys"}
-\isakeyword{assume}~@{text"Cons:"}~@{text"xs = y # ys"}'. Here
-is a (somewhat contrived) example: *}
-
-lemma "length(tl xs) = length xs - 1"
-proof (cases xs)
- case Nil thus ?thesis by simp
-next
- case (Cons y ys)
- hence "length(tl xs) = length ys \<and> length xs = length ys + 1"
- by simp
- thus ?thesis by simp
-qed
-
-text{* Note that in each \isakeyword{case} the assumption can be
+\isakeyword{assume}~@{text"Cons:"}~@{text"xs = y # ys"}'.
+In each \isakeyword{case} the assumption can be
referred to inside the proof by the name of the constructor. In
Section~\ref{sec:full-Ind} below we will come across an example
of this. *}
subsection{*Structural induction*}
-text{* We start with a simple inductive proof where both cases are proved automatically: *}
+text{* We start with an inductive proof where both cases are proved automatically: *}
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
by (induct n, simp_all)
@@ -111,8 +108,8 @@
empty whereas \isakeyword{case}~@{text Suc} assumes @{text"?P n"}. Again we
have the same problem as with case distinctions: we cannot refer to an anonymous @{term n}
in the induction step because it has not been introduced via \isakeyword{fix}
-(in contrast to the previous proof). The solution is the same as above:
-replace @{term Suc} by @{text"(Suc i)"}: *}
+(in contrast to the previous proof). The solution is the one outlined for
+@{text Cons} above: replace @{term Suc} by @{text"(Suc i)"}: *}
lemma fixes n::nat shows "n < n*n + 1"
proof (induct n)
case 0 show ?case by simp
@@ -137,7 +134,7 @@
usual induction hypothesis \emph{and} @{prop"P' x"}.
It should be clear how this generalizes to more complex formulae.
-As a concrete example we will now prove complete induction via
+As an example we will now prove complete induction via
structural induction. *}
lemma assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
@@ -173,7 +170,7 @@
Note that in a nested induction over the same data type, the inner
case labels hide the outer ones of the same name. If you want to refer
-to the outer ones inside, you need to name them on the outside:
+to the outer ones inside, you need to name them on the outside, e.g.\
\isakeyword{note}~@{text"outer_IH = Suc"}. *}
subsection{*Rule induction*}
@@ -293,10 +290,4 @@
(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
by (induct xs rule: rot.induct, simp_all)
-text{*\small
-\paragraph{Acknowledgment}
-I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
-Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer,
-Markus Wenzel and three referees commented on and improved this document.
-*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Mon Dec 23 12:01:47 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Sun Dec 29 08:56:24 2002 +0100
@@ -14,26 +14,27 @@
show "A" by(rule a)
qed
text{*\noindent
-The operational reading: the \isakeyword{assume}-\isakeyword{show} block
-proves @{prop"A \<Longrightarrow> A"},
-which rule @{thm[source]impI} (@{thm impI})
-turns into the desired @{prop"A \<longrightarrow> A"}.
-However, this text is much too detailed for comfort. Therefore Isar
-implements the following principle:
-\begin{quote}\em
-Command \isakeyword{proof} automatically tries to select an introduction rule
-based on the goal and a predefined list of rules.
-\end{quote}
-Here @{thm[source]impI} is applied automatically:
-*}
+The operational reading: the \isakeyword{assume}-\isakeyword{show}
+block proves @{prop"A \<Longrightarrow> A"} (@{term a} is a degenerate rule (no
+assumptions) that proves @{term A} outright), which rule
+@{thm[source]impI} (@{thm impI}) turns into the desired @{prop"A \<longrightarrow>
+A"}. However, this text is much too detailed for comfort. Therefore
+Isar implements the following principle: \begin{quote}\em Command
+\isakeyword{proof} automatically tries to select an introduction rule
+based on the goal and a predefined list of rules. \end{quote} Here
+@{thm[source]impI} is applied automatically: *}
lemma "A \<longrightarrow> A"
proof
- assume a: "A"
- show "A" by(rule a)
+ assume a: A
+ show A by(rule a)
qed
-text{* Trivial proofs, in particular those by assumption, should be trivial
+text{*\noindent Single-identifier formulae such as @{term A} need not
+be enclosed in double quotes. However, we will continue to do so for
+uniformity.
+
+Trivial proofs, in particular those by assumption, should be trivial
to perform. Proof ``.'' does just that (and a bit more). Thus
naming of assumptions is often superfluous: *}
lemma "A \<longrightarrow> A"
@@ -54,10 +55,9 @@
A drawback of implicit proofs by assumption is that it
is no longer obvious where an assumption is used.
-Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"} can be
-abbreviated to ``..''
-if \emph{name} refers to one of the predefined introduction rules:
-*}
+Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"}
+can be abbreviated to ``..'' if \emph{name} refers to one of the
+predefined introduction rules (or elimination rules, see below): *}
lemma "A \<longrightarrow> A \<and> A"
proof
@@ -133,14 +133,13 @@
qed
text{*\noindent Because of the frequency of \isakeyword{from}~@{text
-this} Isar provides two abbreviations:
+this}, Isar provides two abbreviations:
\begin{center}
-\begin{tabular}{rcl}
-\isakeyword{then} &=& \isakeyword{from} @{text this} \\
-\isakeyword{thus} &=& \isakeyword{then} \isakeyword{show}
+\begin{tabular}{r@ {\quad=\quad}l}
+\isakeyword{then} & \isakeyword{from} @{text this} \\
+\isakeyword{thus} & \isakeyword{then} \isakeyword{show}
\end{tabular}
\end{center}
-\medskip
Here is an alternative proof that operates purely by forward reasoning: *}
lemma "A \<and> B \<longrightarrow> B \<and> A"
@@ -150,35 +149,41 @@
from ab have b: "B" ..
from b a show "B \<and> A" ..
qed
-text{*\noindent
-It is worth examining this text in detail because it exhibits a number of new concepts.
-For a start, this is the first time we have proved intermediate propositions
-(\isakeyword{have}) on the way to the final \isakeyword{show}. This is the
-norm in any nontrivial proof where one cannot bridge the gap between the
-assumptions and the conclusion in one step. Both \isakeyword{have}s above are
-proved automatically via @{thm[source]conjE} triggered by
-\isakeyword{from}~@{text ab}.
+text{*\noindent It is worth examining this text in detail because it
+exhibits a number of new concepts. For a start, it is the first time
+we have proved intermediate propositions (\isakeyword{have}) on the
+way to the final \isakeyword{show}. This is the norm in nontrivial
+proofs where one cannot bridge the gap between the assumptions and the
+conclusion in one step. To understand how the proof works we need to
+explain more Isar details.
-The \isakeyword{show} command illustrates two things:
-\begin{itemize}
-\item \isakeyword{from} can be followed by any number of facts.
-Given \isakeyword{from}~@{text f}$_1$~\dots~@{text f}$_n$, the
-\isakeyword{proof} step after \isakeyword{show}
-tries to find an elimination rule whose first $n$ premises can be proved
-by the given facts in the given order.
-\item If there is no matching elimination rule, introduction rules are tried,
-again using the facts to prove the premises.
-\end{itemize}
-In this case, the proof succeeds with @{thm[source]conjI}. Note that the proof
-would fail had we written \isakeyword{from}~@{text"a b"}
-instead of \isakeyword{from}~@{text"b a"}.
+Method @{text rule} can be given a list of rules, in which case
+@{text"(rule"}~\textit{rules}@{text")"} applies the first matching
+rule in the list \textit{rules}. Command \isakeyword{from} can be
+followed by any number of facts. Given \isakeyword{from}~@{text
+f}$_1$~\dots~@{text f}$_n$, the proof step
+@{text"(rule"}~\textit{rules}@{text")"} following a \isakeyword{have}
+or \isakeyword{show} searches \textit{rules} for a rule whose first
+$n$ premises can be proved by @{text f}$_1$~\dots~@{text f}$_n$ in the
+given order. Finally one needs to know that ``..'' is short for
+@{text"by(rule"}~\textit{elim-rules intro-rules}@{text")"} (or
+@{text"by(rule"}~\textit{intro-rules}@{text")"} if there are no facts
+fed into the proof), i.e.\ elimination rules are tried before
+introduction rules.
-This treatment of facts fed into a proof is not restricted to implicit
-application of introduction and elimination rules but applies to explicit
-application of rules as well. Thus you could replace the final ``..'' above
-with \isakeyword{by}@{text"(rule conjI)"}.
-*}
+Thus in the above proof both \isakeyword{have}s are proved via
+@{thm[source]conjE} triggered by \isakeyword{from}~@{text ab} whereas
+in the \isakeyword{show} step no elimination rule is applicable and
+the proof succeeds with @{thm[source]conjI}. The latter would fail had
+we written \isakeyword{from}~@{text"a b"} instead of
+\isakeyword{from}~@{text"b a"}.
+
+Proofs starting with a plain @{text proof} behave the same because the
+latter is short for @{text"proof (rule"}~\textit{elim-rules
+intro-rules}@{text")"} (or @{text"proof
+(rule"}~\textit{intro-rules}@{text")"} if there are no facts fed into
+the proof). *}
subsection{*More constructs*}
@@ -234,9 +239,9 @@
arguments by contradiction, this example also introduces two new
abbreviations:
\begin{center}
-\begin{tabular}{lcl}
-\isakeyword{hence} &=& \isakeyword{then} \isakeyword{have} \\
-\isakeyword{with}~\emph{facts} &=&
+\begin{tabular}{l@ {\quad=\quad}l}
+\isakeyword{hence} & \isakeyword{then} \isakeyword{have} \\
+\isakeyword{with}~\emph{facts} &
\isakeyword{from}~\emph{facts} @{text this}
\end{tabular}
\end{center}
@@ -262,6 +267,11 @@
when showing @{term"A \<and> B"} we need to show both @{term A} and @{term
B}. Each subgoal is proved separately, in \emph{any} order. The
individual proofs are separated by \isakeyword{next}.
+
+Strictly speaking \isakeyword{next} is only required if the subgoals
+are proved in different assumption contexts which need to be
+separated, which is not the case above. For clarity we
+have employed \isakeyword{next} anyway and will continue to do so.
\end{description}
This is all very well as long as formulae are small. Let us now look at some
@@ -315,7 +325,6 @@
\isakeyword{using} \emph{minor-facts}~
\emph{proof}
\end{center}
-\medskip
Sometimes it is necessary to suppress the implicit application of rules in a
\isakeyword{proof}. For example \isakeyword{show}~@{prop"A \<or> B"} would
@@ -379,7 +388,7 @@
the elimination involved.
Here is a proof of a well known tautology.
-Figure out which rule is used where! *}
+Which rule is used where? *}
lemma assumes ex: "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y"
proof
@@ -470,6 +479,7 @@
@{text blast} to achieve bigger proof steps, there may still be the
tendency to use the default introduction and elimination rules to
decompose goals and facts. This can lead to very tedious proofs:
+\Tweakskip
*}
(*<*)ML"set quick_and_dirty"(*>*)
lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
@@ -554,10 +564,10 @@
text{* If you want to remember intermediate fact(s) that cannot be
named directly, use \isakeyword{note}. For example the result of raw
proof block can be named by following it with
-\isakeyword{note}~@{text"note some_name = this"}. As a side effect
+\isakeyword{note}~@{text"some_name = this"}. As a side effect,
@{text this} is set to the list of facts on the right-hand side. You
can also say @{text"note some_fact"}, which simply sets @{text this},
-i.e.\ recalls @{text"some_fact"}. *}
+i.e.\ recalls @{text"some_fact"}, e.g.\ in a \isakeyword{moreover} sequence. *}
subsubsection{*\isakeyword{fixes}*}
@@ -587,7 +597,8 @@
by(simp add: comm mono)
text{*\noindent The concrete syntax is dropped at the end of the proof and the
-theorem becomes @{thm[display,margin=60]comm_mono} *}
+theorem becomes @{thm[display,margin=60]comm_mono}
+\tweakskip *}
subsubsection{*\isakeyword{obtain}*}
--- a/doc-src/TutorialI/IsarOverview/Isar/document/intro.tex Mon Dec 23 12:01:47 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/intro.tex Sun Dec 29 08:56:24 2002 +0100
@@ -1,9 +1,11 @@
\section{Introduction}
-Isar is an extension of Isabelle with structured proofs in a stylized
-language of mathematics. These proofs are readable for both a human
-and a machine. This document is a compact introduction to structured
-proofs in Isar/HOL, an extension of Isabelle/HOL~\cite{LNCS2283}. We
+Isabelle is a generic proof assistant. Isar is an extension of
+Isabelle with structured proofs in a stylised language of mathematics.
+These proofs are readable for both a human and a machine.
+Isabelle/HOL~\cite{LNCS2283} is a specialisation of Isabelle with
+higher-order logic (HOL). This paper is a compact introduction to
+structured proofs in Isar/HOL, an extension of Isabelle/HOL. We
intentionally do not present the full language but concentrate on the
essentials. Neither do we give a formal semantics of Isar. Instead we
introduce Isar by example. We believe that the language ``speaks for
@@ -26,7 +28,7 @@
tactics.
A radically different approach was taken by the Mizar
-system~\cite{Rudnicki92} where proofs are written in a stylized language akin
+system~\cite{Rudnicki92} where proofs are written in a stylised 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
@@ -94,13 +96,16 @@
\subsection{Bits of Isabelle}
-In order to make this paper self-contained we recall some basic
-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$ (named \isa{U}) is written \isa{T[OF U]} and yields theorem $B$.
+We recall some basic notions and notation from Isabelle. For more
+details and for instructions how to run examples see
+elsewhere~\cite{LNCS2283}.
+
+Isabelle's meta-logic comes with a type of \emph{propositions} with
+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$ (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$.
@@ -112,7 +117,12 @@
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
+$\forall$ etc. HOL formulae are propositions, e.g.\ $\forall$ can appear below
+$\Longrightarrow$, but not the other way around. Beware that $\longrightarrow$ binds more
+tightly than $\Longrightarrow$: in $\forall x. P \longrightarrow Q$ the $\forall x$ covers $P \longrightarrow Q$, whereas
+in $\forall x. P \Longrightarrow Q$ it covers only $P$.
+
+Proof methods include \isa{rule} (which performs a backwards
step with a given rule, unifying the conclusion of the rule with the
current subgoal and replacing the subgoal by the premises of the
rule), \isa{simp} (for simplification) and \isa{blast} (for predicate
@@ -146,5 +156,5 @@
%Do not be mislead by the simplicity of the formulae being proved,
%especially in the beginning. Isar has been used very successfully in
-%large applications, for example the formalization of Java, in
+%large applications, for example the formalisation of Java, in
%particular the verification of the bytecode verifier~\cite{KleinN-TCS}.
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Mon Dec 23 12:01:47 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Sun Dec 29 08:56:24 2002 +0100
@@ -13,7 +13,8 @@
\begin{document}
-\title{A Compact Introduction to Structured Proofs in Isar/HOL}
+\title{%A Compact Introduction to
+Structured Proofs in Isar/HOL}
\author{Tobias Nipkow}
\institute{Institut f{\"u}r Informatik, TU M{\"u}nchen\\
{\small\url{http://www.in.tum.de/~nipkow/}}}
@@ -35,7 +36,12 @@
\input{Induction.tex}
\Tweakskip
-\Tweakskip
+\small
+\paragraph{Acknowledgement}
+I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
+Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer,
+Markus Wenzel and Freek Wiedijk commented on and improved this paper.
+
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{root}