--- a/NEWS Mon Sep 30 16:48:15 2002 +0200
+++ b/NEWS Mon Sep 30 16:50:39 2002 +0200
@@ -74,6 +74,9 @@
* the simplifier trace now shows the names of the applied rewrite rules
+* induct over a !!-quantified statement (say !!x1..xn):
+ each "case" automatically performs "fix x1 .. xn" with exactly those names.
+
* GroupTheory: converted to Isar theories, using locales with implicit structures;
* Real/HahnBanach: updated and adapted to locales;
--- a/doc-src/TutorialI/IsarOverview/Isar/Calc.thy Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Calc.thy Mon Sep 30 16:50:39 2002 +0200
@@ -1,5 +1,7 @@
theory Calc = Main:
+subsection{* Chains of equalities *}
+
axclass
group < zero, plus, minus
assoc: "(x + y) + z = x + (y + z)"
@@ -17,6 +19,23 @@
finally show ?thesis .
qed
+subsection{* Inequalities and substitution *}
+
+lemmas distrib = zadd_zmult_distrib zadd_zmult_distrib2
+ zdiff_zmult_distrib zdiff_zmult_distrib2
+declare numeral_2_eq_2[simp]
+
+
+lemma fixes a :: int shows "(a+b)\<twosuperior> \<le> 2*(a\<twosuperior> + b\<twosuperior>)"
+proof -
+ have "(a+b)\<twosuperior> \<le> (a+b)\<twosuperior> + (a-b)\<twosuperior>" by simp
+ also have "(a+b)\<twosuperior> \<le> a\<twosuperior> + b\<twosuperior> + 2*a*b" by(simp add:distrib)
+ also have "(a-b)\<twosuperior> = a\<twosuperior> + b\<twosuperior> - 2*a*b" by(simp add:distrib)
+ finally show ?thesis by simp
+qed
+
+
+subsection{* More transitivity *}
lemma assumes R: "(a,b) \<in> R" "(b,c) \<in> R" "(c,d) \<in> R"
shows "(a,d) \<in> R\<^sup>*"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Mon Sep 30 16:50:39 2002 +0200
@@ -0,0 +1,262 @@
+(*<*)theory Induction = Main:(*>*)
+
+section{*Case distinction and induction \label{sec:Induct}*}
+
+
+subsection{*Case distinction*}
+
+text{* We have already met the @{text cases} method for performing
+binary case splits. Here is another example: *}
+lemma "P \<or> \<not> P"
+proof cases
+ assume "P" thus ?thesis ..
+next
+ assume "\<not> P" 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 don't want to repeat it. This can be avoided by
+the following idiom *}
+
+lemma "P \<or> \<not> P"
+proof (cases "P")
+ case True thus ?thesis ..
+next
+ case False thus ?thesis ..
+qed
+text{*\noindent which is simply a shorthand for the previous
+proof. More precisely, the phrases \isakeyword{case}~@{prop
+True}/@{prop False} abbreviate the corresponding assumptions @{prop P}
+and @{prop"\<not>P"}. In contrast to the previous proof we can prove the cases
+in arbitrary order.
+
+The same game can be played with other datatypes, for example lists:
+*}
+(*<*)declare length_tl[simp del](*>*)
+lemma "length(tl xs) = length xs - 1"
+proof (cases xs)
+ case Nil thus ?thesis by simp
+next
+ case Cons thus ?thesis by simp
+qed
+text{*\noindent Here \isakeyword{case}~@{text Nil} abbreviates
+\isakeyword{assume}~@{prop"xs = []"} and \isakeyword{case}~@{text Cons}
+abbreviates \isakeyword{fix}~@{text"? ??"}
+\isakeyword{assume}~@{text"xs = ? # ??"} where @{text"?"} and @{text"??"}
+stand for variable names that have been chosen by the system.
+Therefore we cannot
+refer to them (this would lead to obscure proofs) and have not even shown
+them. Luckily, this proof is simple enough we do not need to refer to them.
+However, sometimes one may have to. Hence Isar offers a simple scheme for
+naming those variables: replace the anonymous @{text Cons} by, for example,
+@{text"(Cons y ys)"}, which abbreviates \isakeyword{fix}~@{text"y ys"}
+\isakeyword{assume}~@{text"xs = Cons y ys"}, i.e.\ @{prop"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
+
+
+subsection{*Structural induction*}
+
+text{* We start with a simple inductive proof where both cases are proved automatically: *}
+lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
+by (induct n, simp_all)
+
+text{*\noindent If we want to expose more of the structure of the
+proof, we can use pattern matching to avoid having to repeat the goal
+statement: *}
+lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)" (is "?P n")
+proof (induct n)
+ show "?P 0" by simp
+next
+ fix n assume "?P n"
+ thus "?P(Suc n)" by simp
+qed
+
+text{* \noindent We could refine this further to show more of the equational
+proof. Instead we explore the same avenue as for case distinctions:
+introducing context via the \isakeyword{case} command: *}
+lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
+proof (induct n)
+ case 0 show ?case by simp
+next
+ case Suc thus ?case by simp
+qed
+
+text{* \noindent The implicitly defined @{text ?case} refers to the
+corresponding case to be proved, i.e.\ @{text"?P 0"} in the first case and
+@{text"?P(Suc n)"} in the second case. Context \isakeyword{case}~@{text 0} is
+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)"}: *}
+lemma fixes n::nat shows "n < n*n + 1"
+proof (induct n)
+ case 0 show ?case by simp
+next
+ case (Suc i) thus "Suc i < Suc i * Suc i + 1" by simp
+qed
+
+text{* \noindent Of course we could again have written
+\isakeyword{thus}~@{text ?case} instead of giving the term explicitly
+but we wanted to use @{term i} somewhere. *}
+
+subsection{*Induction formulae involving @{text"\<And>"} or @{text"\<Longrightarrow>"}*}
+
+text{* Let us now consider the situation where the goal to be proved contains
+@{text"\<And>"} or @{text"\<Longrightarrow>"}, say @{prop"\<And>x. P x \<Longrightarrow> Q x"} --- motivation and a
+real example follow shortly. This means that in each case of the induction,
+@{text ?case} would be of the same form @{prop"\<And>x. P' x \<Longrightarrow> Q' x"}. Thus the
+first proof steps will be the canonical ones, fixing @{text x} and assuming
+@{prop"P' x"}. To avoid this tedium, induction performs these steps
+automatically: for example in case @{text"(Suc n)"}, @{text ?case} is only
+@{prop"Q' x"} whereas the assumptions (named @{term Suc}) contain both the
+usual induction hypothesis \emph{and} @{prop"P' x"}. To fix the name of the
+bound variable @{term x} you may write @{text"(Suc n x)"}, thus abbreviating
+\isakeyword{fix}~@{term x}.
+It should be clear how this example generalizes to more complex formulae.
+
+As a concrete 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)"
+ shows "P(n::nat)"
+proof (rule A)
+ show "\<And>m. m < n \<Longrightarrow> P m"
+ proof (induct n)
+ case 0 thus ?case by simp
+ next
+ case (Suc n m) -- {*@{text"?m < n \<Longrightarrow> P ?m"} and @{prop"m < Suc n"}*}
+ show ?case -- {*@{term ?case}*}
+ proof cases
+ assume eq: "m = n"
+ from Suc A have "P n" by blast
+ with eq show "P m" by simp
+ next
+ assume "m \<noteq> n"
+ with Suc have "m < n" by arith
+ thus "P m" by(rule Suc)
+ qed
+ qed
+qed
+text{* \noindent Given the explanations above and the comments in
+the proof text, the proof should be quite readable.
+
+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
+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.
+*}
+
+subsection{*Rule induction*}
+
+text{* We define our own version of reflexive transitive closure of a
+relation *}
+consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
+inductive "r*"
+intros
+refl: "(x,x) \<in> r*"
+step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
+
+text{* \noindent and prove that @{term"r*"} is indeed transitive: *}
+lemma assumes A: "(x,y) \<in> r*" shows "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*"
+using A
+proof induct
+ case refl thus ?case .
+next
+ case step thus ?case by(blast intro: rtc.step)
+qed
+text{*\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n)
+\in R$ piped into the proof, here \isakeyword{using}~@{text A}. The
+proof itself follows the inductive definition very
+closely: there is one case for each rule, and it has the same name as
+the rule, analogous to structural induction.
+
+However, this proof is rather terse. Here is a more readable version:
+*}
+
+lemma assumes A: "(x,y) \<in> r*" and B: "(y,z) \<in> r*"
+ shows "(x,z) \<in> r*"
+proof -
+ from A B show ?thesis
+ proof induct
+ fix x assume "(x,z) \<in> r*" -- {*@{text B}[@{text y} := @{text x}]*}
+ thus "(x,z) \<in> r*" .
+ next
+ fix x' x y
+ assume 1: "(x',x) \<in> r" and
+ IH: "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*" and
+ B: "(y,z) \<in> r*"
+ from 1 IH[OF B] show "(x',z) \<in> r*" by(rule rtc.step)
+ qed
+qed
+text{*\noindent We start the proof with \isakeyword{from}~@{text"A
+B"}. Only @{text A} is ``consumed'' by the induction step.
+Since @{text B} is left over we don't just prove @{text
+?thesis} but @{text"B \<Longrightarrow> ?thesis"}, just as in the previous proof. The
+base case is trivial. In the assumptions for the induction step we can
+see very clearly how things fit together and permit ourselves the
+obvious forward step @{text"IH[OF B]"}. *}
+
+subsection{*More induction*}
+
+text{* We close the section by demonstrating how arbitrary induction rules
+are applied. As a simple example we have chosen recursion induction, i.e.\
+induction based on a recursive function definition. The example is an unusual
+definition of rotation: *}
+
+consts rot :: "'a list \<Rightarrow> 'a list"
+recdef rot "measure length"
+"rot [] = []"
+"rot [x] = [x]"
+"rot (x#y#zs) = y # rot(x#zs)"
+
+text{* In the first proof we set up each case explicitly, merely using
+pattern matching to abbreviate the statement: *}
+
+lemma "length(rot xs) = length xs" (is "?P xs")
+proof (induct xs rule: rot.induct)
+ show "?P []" by simp
+next
+ fix x show "?P [x]" by simp
+next
+ fix x y zs assume "?P (x#zs)"
+ thus "?P (x#y#zs)" by simp
+qed
+text{*\noindent
+This proof skeleton works for arbitrary induction rules, not just
+@{thm[source]rot.induct}.
+
+In the following proof we rely on a default naming scheme for cases: they are
+called 1, 2, etc, unless they have been named explicitly. The latter happens
+only with datatypes and inductively defined sets, but not with recursive
+functions. *}
+
+lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"
+proof (induct xs rule: rot.induct)
+ case 1 thus ?case by simp
+next
+ case 2 show ?case by simp
+next
+ case 3 thus ?case by simp
+qed
+
+text{*\noindent Why can case 2 get away with \isakeyword{show} instead of
+\isakeyword{thus}?
+
+Of course both proofs are so simple that they can be condensed to*}
+(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
+by (induct xs rule: rot.induct, simp_all)
+(*<*)end(*>*)
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Mon Sep 30 16:50:39 2002 +0200
@@ -1,50 +1,6 @@
(*<*)theory Logic = Main:(*>*)
-text{* We begin by looking at a simplified grammar for Isar proofs
-where parentheses are used for grouping and $^?$ indicates an optional item:
-\begin{center}
-\begin{tabular}{lrl}
-\emph{proof} & ::= & \isakeyword{proof} \emph{method}$^?$
- \emph{statement}*
- \isakeyword{qed} \\
- &$\mid$& \isakeyword{by} \emph{method}\\[1ex]
-\emph{statement} &::= & \isakeyword{fix} \emph{variables} \\
- &$\mid$& \isakeyword{assume} \emph{propositions} \\
- &$\mid$& (\isakeyword{from} \emph{facts})$^?$
- (\isakeyword{show} $\mid$ \isakeyword{have})
- \emph{propositions} \emph{proof} \\[1ex]
-\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} \\[1ex]
-\emph{fact} &::=& \emph{label}
-\end{tabular}
-\end{center}
-This is a typical proof skeleton:
-\begin{center}
-\begin{tabular}{@ {}ll}
-\isakeyword{proof}\\
-\hspace*{3ex}\isakeyword{assume} @{text"\""}\emph{the-assm}@{text"\""}\\
-\hspace*{3ex}\isakeyword{have} @{text"\""}\dots@{text"\""} & --- intermediate result\\
-\hspace*{3ex}\vdots\\
-\hspace*{3ex}\isakeyword{have} @{text"\""}\dots@{text"\""} & --- intermediate result\\
-\hspace*{3ex}\isakeyword{show} @{text"\""}\emph{the-concl}@{text"\""}\\
-\isakeyword{qed}
-\end{tabular}
-\end{center}
-It proves \emph{the-assm}~@{text"\<Longrightarrow>"}~\emph{the-concl}.
-Text starting with ``---'' is a comment.
-
-Note that \emph{propositions} (following \isakeyword{assume} etc)
-may but need not be
-separated by \isakeyword{and}, whose purpose is to structure them
-into possibly named blocks. For example in
-\begin{center}
-\isakeyword{assume} @{text"A:"} $A_1$ $A_2$ \isakeyword{and} @{text"B:"} $A_3$
-\isakeyword{and} $A_4$
-\end{center}
-label @{text A} refers to the list of propositions $A_1$ $A_2$ and
-label @{text B} to $A_3$.
-*}
-
-section{*Logic*}
+section{*Logic \label{sec:Logic}*}
subsection{*Propositional logic*}
@@ -90,7 +46,7 @@
by assumption: *}
lemma "A \<longrightarrow> A \<and> A"
proof
- assume A
+ assume "A"
show "A \<and> A" by(rule conjI)
qed
text{*\noindent A drawback of these implicit proofs by assumption is that it
@@ -103,7 +59,7 @@
lemma "A \<longrightarrow> A \<and> A"
proof
- assume A
+ assume "A"
show "A \<and> A" ..
qed
text{*\noindent
@@ -122,7 +78,7 @@
assume AB: "A \<and> B"
show "B \<and> A"
proof (rule conjE[OF AB]) -- {*@{text"conjE[OF AB]"}: @{thm conjE[OF AB]} *}
- assume A and B
+ assume "A" "B"
show ?thesis ..
qed
qed
@@ -151,7 +107,7 @@
assume AB: "A \<and> B"
from AB show "B \<and> A"
proof
- assume A and B
+ assume "A" "B"
show ?thesis ..
qed
qed
@@ -169,7 +125,7 @@
assume "A \<and> B"
from this show "B \<and> A"
proof
- assume A and B
+ assume "A" "B"
show ?thesis ..
qed
qed
@@ -188,8 +144,8 @@
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
assume ab: "A \<and> B"
- from ab have a: A ..
- from ab have b: B ..
+ from ab have a: "A" ..
+ from ab have b: "B" ..
from b a show "B \<and> A" ..
qed
text{*\noindent
@@ -232,9 +188,9 @@
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
assume ab: "A \<and> B"
- from ab have B ..
+ from ab have "B" ..
moreover
- from ab have A ..
+ from ab have "A" ..
ultimately show "B \<and> A" ..
qed
text{*\noindent You can combine any number of facts @{term A1} \dots\ @{term
@@ -255,10 +211,10 @@
assume nn: "\<not> (\<not> A \<or> \<not> B)"
have "\<not> A"
proof
- assume A
+ assume "A"
have "\<not> B"
proof
- assume B
+ assume "B"
have "A \<and> B" ..
with n show False ..
qed
@@ -279,7 +235,7 @@
\begin{tabular}{lcl}
\isakeyword{hence} &=& \isakeyword{then} \isakeyword{have} \\
\isakeyword{with}~\emph{facts} &=&
-\isakeyword{from}~\emph{facts} \isakeyword{and} @{text this}
+\isakeyword{from}~\emph{facts} @{text this}
\end{tabular}
\end{center}
*}
@@ -313,9 +269,9 @@
lemma "large_A \<and> large_B \<Longrightarrow> large_B \<and> large_A"
(is "?AB \<Longrightarrow> ?B \<and> ?A")
proof
- assume ?AB thus ?B ..
+ assume "?AB" thus "?B" ..
next
- assume ?AB thus ?A ..
+ assume "?AB" thus "?A" ..
qed
text{*\noindent Any formula may be followed by
@{text"("}\isakeyword{is}~\emph{pattern}@{text")"} which causes the pattern
@@ -330,9 +286,9 @@
lemma assumes AB: "large_A \<and> large_B"
shows "large_B \<and> large_A" (is "?B \<and> ?A")
proof
- from AB show ?B ..
+ from AB show "?B" ..
next
- from AB show ?A ..
+ from AB show "?A" ..
qed
text{*\noindent Note the difference between @{text ?AB}, a term, and
@{text AB}, a fact.
@@ -345,7 +301,7 @@
shows "large_B \<and> large_A" (is "?B \<and> ?A")
using AB
proof
- assume ?A and ?B show ?thesis ..
+ assume "?A" "?B" show ?thesis ..
qed
text{*\noindent Command \isakeyword{using} can appear before a proof
and adds further facts to those piped into the proof. Here @{text AB}
@@ -361,7 +317,7 @@
Sometimes it is necessary to suppress the implicit application of rules in a
\isakeyword{proof}. For example \isakeyword{show}~@{prop"A \<or> B"} would
trigger $\lor$-introduction, requiring us to prove @{prop A}. A simple
-``@{text"-"}'' prevents this \emph{faut pas}: *}
+``@{text"-"}'' prevents this \emph{faux pas}: *}
lemma assumes AB: "A \<or> B" shows "B \<or> A"
proof -
@@ -509,7 +465,7 @@
lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B"
proof
- assume a: A
+ assume a: "A"
show "(A \<longrightarrow>B) \<longrightarrow> B"
apply(rule impI)
apply(erule impE)
@@ -520,263 +476,4 @@
text{*\noindent You may need to resort to this technique if an automatic step
fails to prove the desired proposition. *}
-section{*Case distinction and induction*}
-
-
-subsection{*Case distinction*}
-
-text{* We have already met the @{text cases} method for performing
-binary case splits. Here is another example: *}
-lemma "P \<or> \<not> P"
-proof cases
- assume "P" thus ?thesis ..
-next
- assume "\<not> P" 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 don't want to repeat it. This can be avoided by
-the following idiom *}
-
-lemma "P \<or> \<not> P"
-proof (cases "P")
- case True thus ?thesis ..
-next
- case False thus ?thesis ..
-qed
-text{*\noindent which is simply a shorthand for the previous
-proof. More precisely, the phrases \isakeyword{case}~@{prop
-True}/@{prop False} abbreviate the corresponding assumptions @{prop P}
-and @{prop"\<not>P"}. In contrast to the previous proof we can prove the cases
-in arbitrary order.
-
-The same game can be played with other datatypes, for example lists:
-*}
-(*<*)declare length_tl[simp del](*>*)
-lemma "length(tl xs) = length xs - 1"
-proof (cases xs)
- case Nil thus ?thesis by simp
-next
- case Cons thus ?thesis by simp
-qed
-text{*\noindent Here \isakeyword{case}~@{text Nil} abbreviates
-\isakeyword{assume}~@{prop"xs = []"} and \isakeyword{case}~@{text Cons}
-abbreviates \isakeyword{fix}~@{text"? ??"}
-\isakeyword{assume}~@{text"xs = ? # ??"} where @{text"?"} and @{text"??"}
-stand for variable names that have been chosen by the system.
-Therefore we cannot
-refer to them (this would lead to obscure proofs) and have not even shown
-them. Luckily, this proof is simple enough we do not need to refer to them.
-However, sometimes one may have to. Hence Isar offers a simple scheme for
-naming those variables: replace the anonymous @{text Cons} by, for example,
-@{text"(Cons y ys)"}, which abbreviates \isakeyword{fix}~@{text"y ys"}
-\isakeyword{assume}~@{text"xs = Cons y ys"}, i.e.\ @{prop"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
-
-
-subsection{*Structural induction*}
-
-text{* We start with a simple inductive proof where both cases are proved automatically: *}
-lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
-by (induct n, simp_all)
-
-text{*\noindent If we want to expose more of the structure of the
-proof, we can use pattern matching to avoid having to repeat the goal
-statement: *}
-lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)" (is "?P n")
-proof (induct n)
- show "?P 0" by simp
-next
- fix n assume "?P n"
- thus "?P(Suc n)" by simp
-qed
-
-text{* \noindent We could refine this further to show more of the equational
-proof. Instead we explore the same avenue as for case distinctions:
-introducing context via the \isakeyword{case} command: *}
-lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
-proof (induct n)
- case 0 show ?case by simp
-next
- case Suc thus ?case by simp
-qed
-
-text{* \noindent The implicitly defined @{text ?case} refers to the
-corresponding case to be proved, i.e.\ @{text"?P 0"} in the first case and
-@{text"?P(Suc n)"} in the second case. Context \isakeyword{case}~@{text 0} is
-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)"}: *}
-lemma fixes n::nat shows "n < n*n + 1"
-proof (induct n)
- case 0 show ?case by simp
-next
- case (Suc i) thus "Suc i < Suc i * Suc i + 1" by simp
-qed
-
-text{* \noindent Of course we could again have written
-\isakeyword{thus}~@{text ?case} instead of giving the term explicitly
-but we wanted to use @{term i} somewhere. *}
-
-subsection{*Induction formulae involving @{text"\<And>"} or @{text"\<Longrightarrow>"}*}
-
-text{* Let us now consider the situation where the goal to be proved contains
-@{text"\<And>"} or @{text"\<Longrightarrow>"}, say @{prop"\<And>x. P x \<Longrightarrow> Q x"} --- motivation and a
-real example follow shortly. This means that in each case of the induction,
-@{text ?case} would be of the same form @{prop"\<And>x. P' x \<Longrightarrow> Q' x"}. Thus the
-first proof steps will be the canonical ones, fixing @{text x} and assuming
-@{prop"P' x"}. To avoid this tedium, induction performs these steps
-automatically: for example in case @{text"(Suc n)"}, @{text ?case} is only
-@{prop"Q' x"} whereas the assumptions (named @{term Suc}) contain both the
-usual induction hypothesis \emph{and} @{prop"P' x"}. To fix the name of the
-bound variable @{term x} you may write @{text"(Suc n x)"}, thus abbreviating
-\isakeyword{fix}~@{term x}.
-It should be clear how this example generalizes to more complex formulae.
-
-As a concrete 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)"
- shows "P(n::nat)"
-proof (rule A)
- show "\<And>m. m < n \<Longrightarrow> P m"
- proof (induct n)
- case 0 thus ?case by simp
- next
- case (Suc n m) -- {*@{text"?m < n \<Longrightarrow> P ?m"} and @{prop"m < Suc n"}*}
- show ?case -- {*@{term ?case}*}
- proof cases
- assume eq: "m = n"
- from Suc A have "P n" by blast
- with eq show "P m" by simp
- next
- assume "m \<noteq> n"
- with Suc have "m < n" by arith
- thus "P m" by(rule Suc)
- qed
- qed
-qed
-text{* \noindent Given the explanations above and the comments in
-the proof text, the proof should be quite readable.
-
-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
-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.
-*}
-
-subsection{*Rule induction*}
-
-text{* We define our own version of reflexive transitive closure of a
-relation *}
-consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
-inductive "r*"
-intros
-refl: "(x,x) \<in> r*"
-step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
-
-text{* \noindent and prove that @{term"r*"} is indeed transitive: *}
-lemma assumes A: "(x,y) \<in> r*" shows "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*"
-using A
-proof induct
- case refl thus ?case .
-next
- case step thus ?case by(blast intro: rtc.step)
-qed
-text{*\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n)
-\in R$ piped into the proof, here \isakeyword{using}~@{text A}. The
-proof itself follows the inductive definition very
-closely: there is one case for each rule, and it has the same name as
-the rule, analogous to structural induction.
-
-However, this proof is rather terse. Here is a more readable version:
-*}
-
-lemma assumes A: "(x,y) \<in> r*" and B: "(y,z) \<in> r*"
- shows "(x,z) \<in> r*"
-proof -
- from A B show ?thesis
- proof induct
- fix x assume "(x,z) \<in> r*" -- {*@{text B}[@{text y} := @{text x}]*}
- thus "(x,z) \<in> r*" .
- next
- fix x' x y
- assume 1: "(x',x) \<in> r" and
- IH: "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*" and
- B: "(y,z) \<in> r*"
- from 1 IH[OF B] show "(x',z) \<in> r*" by(rule rtc.step)
- qed
-qed
-text{*\noindent We start the proof with \isakeyword{from}~@{text"A
-B"}. Only @{text A} is ``consumed'' by the induction step.
-Since @{text B} is left over we don't just prove @{text
-?thesis} but @{text"B \<Longrightarrow> ?thesis"}, just as in the previous proof. The
-base case is trivial. In the assumptions for the induction step we can
-see very clearly how things fit together and permit ourselves the
-obvious forward step @{text"IH[OF B]"}. *}
-
-subsection{*More induction*}
-
-text{* We close the section by demonstrating how arbitrary induction rules
-are applied. As a simple example we have chosen recursion induction, i.e.\
-induction based on a recursive function definition. The example is an unusual
-definition of rotation: *}
-
-consts rot :: "'a list \<Rightarrow> 'a list"
-recdef rot "measure length"
-"rot [] = []"
-"rot [x] = [x]"
-"rot (x#y#zs) = y # rot(x#zs)"
-
-text{* In the first proof we set up each case explicitly, merely using
-pattern matching to abbreviate the statement: *}
-
-lemma "length(rot xs) = length xs" (is "?P xs")
-proof (induct xs rule: rot.induct)
- show "?P []" by simp
-next
- fix x show "?P [x]" by simp
-next
- fix x y zs assume "?P (x#zs)"
- thus "?P (x#y#zs)" by simp
-qed
-text{*\noindent
-This proof skeleton works for arbitrary induction rules, not just
-@{thm[source]rot.induct}.
-
-In the following proof we rely on a default naming scheme for cases: they are
-called 1, 2, etc, unless they have been named explicitly. The latter happens
-only with datatypes and inductively defined sets, but not with recursive
-functions. *}
-
-lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"
-proof (induct xs rule: rot.induct)
- case 1 thus ?case by simp
-next
- case 2 show ?case by simp
-next
- case 3 thus ?case by simp
-qed
-
-text{*\noindent Why can case 2 get away with \isakeyword{show} instead of
-\isakeyword{thus}?
-
-Of course both proofs are so simple that they can be condensed to*}
-(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
-by (induct xs rule: rot.induct, simp_all)
(*<*)end(*>*)
--- a/doc-src/TutorialI/IsarOverview/Isar/ROOT.ML Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/ROOT.ML Mon Sep 30 16:50:39 2002 +0200
@@ -1,1 +1,2 @@
-use_thy "Logic"
+use_thy "Logic";
+use_thy "Induction"
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.bib Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.bib Mon Sep 30 16:50:39 2002 +0200
@@ -1,6 +1,10 @@
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
@string{Springer="Springer-Verlag"}
+@book{LCF,author="M.C.J. Gordon and Robin Milner and C.P. Wadsworth",
+title="Edinburgh {LCF}: a Mechanised Logic of Computation",
+publisher=Springer,series=LNCS,volume=78,year=1979}
+
@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
publisher=Springer,series=LNCS,volume=2283,year=2002,
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Mon Sep 30 16:50:39 2002 +0200
@@ -10,23 +10,162 @@
\begin{document}
-\title{A Compact Overview of Structured Proofs in Isar/HOL}
+\title{A Compact Introduction to Structured Proofs in Isar/HOL}
\author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\
{\small\url{http://www.in.tum.de/~nipkow/}}}
\date{}
\maketitle
-\noindent
-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.
+\begin{abstract}
+ Isar is an extension of the theorem prover Isabelle with a language
+ for writing human-readable structured proofs. This paper is an
+ introduction to the basic constructs of this language. It is aimed
+ at potential users of Isar but also discusses the design rationals
+ behind the language and its constructs.
+\end{abstract}
+
+\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 very compact introduction to
+structured proofs in Isar/HOL, an extension of
+Isabelle/HOL~\cite{LNCS2283}. 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. Again
+this is intentional: we believe that the language ``speaks for
+itself'' in the same way that traditional mathamtical 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
+manual~\cite{Isar-Ref-Man}.
+
+\subsection{Background}
+
+Interactive theorem proving has been dominated by a model of proof
+that goes back to the LCF system~\cite{LCF}: a proof is a more or less
+structured sequence of commands that manipulate an implicit proof
+state. Thus the proof proof text is only suitable for the machine; for
+a human, the proof only comes alive when he can see the state changes
+caused by the stepwise execution of the commands. Such a proof is like
+an uncommented assembly language program. We call them
+\emph{tactic-style} proofs because LCF proof-commands were called
+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 as it is. 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
+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.
+Furthermore, we have Isabelle's powerful automatic proof procedures
+(e.g.\ simplification and a tableau-style prover) at our disposal.
+A closer comparison of Isar and Mizar can be found
+elsewhere~\cite{Isar-Mizar}.
-This document is a very compact introduction to structured proofs in
-Isar/HOL, an extension of Isabelle/HOL~\cite{LNCS2283}. A detailed
-exposition of this material can be found in Markus Wenzel's PhD
-thesis~\cite{Wenzel-PhD} and the Isar reference manual~\cite{Isar-Ref-Man}.
+Finally, a word of warning for potential writers of structured Isar
+proofs. It has always been easier to write obscure rather than
+readable texts. Similarly, tactic-based proofs are often (though by no
+means always!) easier to write than readable ones: structure does not
+emerge automatically but needs to be understood and imposed. If the
+precise structure of the proof is not clear from the beginning, it can
+be useful to start in a tactic-based style for exploratory purposes
+until one has found a proof which can then be converted into a
+structured text in a second step. Top down conversion is possible
+because Isar allows tactic-based proofs as components of structured
+ones.
+
+\subsection{An overview of the Isar syntax}
+
+We begin by looking at a simplified grammar for Isar proofs
+where parentheses are used for grouping and $^?$ indicates an optional item:
+\begin{center}
+\begin{tabular}{lrl}
+\emph{proof} & ::= & \isakeyword{proof} \emph{method}$^?$
+ \emph{statement}*
+ \isakeyword{qed} \\
+ &$\mid$& \isakeyword{by} \emph{method}\\[1ex]
+\emph{statement} &::= & \isakeyword{fix} \emph{variables} \\
+ &$\mid$& \isakeyword{assume} \emph{propositions} \\
+ &$\mid$& (\isakeyword{from} \emph{facts})$^?$
+ (\isakeyword{show} $\mid$ \isakeyword{have})
+ \emph{propositions} \emph{proof} \\[1ex]
+\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} \\[1ex]
+\emph{fact} &::=& \emph{label}
+\end{tabular}
+\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.
+
+This is a typical proof skeleton:
+\begin{center}
+\begin{tabular}{@{}ll}
+\isakeyword{proof}\\
+\hspace*{3ex}\isakeyword{assume} \isa{"}\emph{the-assm}\isa{"}\\
+\hspace*{3ex}\isakeyword{have} \isa{"}\dots\isa{"} & --- intermediate result\\
+\hspace*{3ex}\vdots\\
+\hspace*{3ex}\isakeyword{have} \isa{"}\dots\isa{"} & --- intermediate result\\
+\hspace*{3ex}\isakeyword{show} \isa{"}\emph{the-concl}\isa{"}\\
+\isakeyword{qed}
+\end{tabular}
+\end{center}
+It proves \emph{the-assm}~$\Longrightarrow$~\emph{the-concl}. Text starting with
+``---'' is a comment. The intermediate \isakeyword{have}s are only
+there to bridge the gap between the assumption and the conclusion and
+do not contribute to the theorem being proved. In contrast,
+\isakeyword{show} establishes the conclusion of the theorem.
+
+As a final bit of syntax note that \emph{propositions} (following
+\isakeyword{assume} etc) may but need not be separated by
+\isakeyword{and}, whose purpose is to structure them into possibly
+named blocks. For example in
+\begin{center}
+\isakeyword{assume} \isa{A:} $A_1$ $A_2$ \isakeyword{and} \isa{B:} $A_3$
+\isakeyword{and} $A_4$
+\end{center}
+label \isa{A} refers to the list of propositions $A_1$ $A_2$ and
+label \isa{B} to $A_3$.
+
+\subsection{Overview of the paper}
+
+The rest of the paper is divided into two parts.
+Section~\ref{sec:Logic} introduces proofs in pure logic based on
+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-TPHOL}, whereas
+reasoning about axiomatically defined structures by means of so called
+``locales'' \cite{BallarinPW-TPHOL} is only described in a very early
+form and 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
+large applications, for example the formalization of Java, in
+particular the verification of the bytecode verifier~\cite{KleinN-TCS}.
\input{Logic.tex}
+\input{Induction.tex}
%\input{Isar.tex}
--- a/doc-src/TutorialI/IsarOverview/Isar/makeDemo Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/makeDemo Mon Sep 30 16:50:39 2002 +0200
@@ -13,6 +13,8 @@
s/text\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here
s/\(\*<\*\)//sg;
s/\(\*>\*\)//sg;
+ s/--(\ )*"([^"])*"//sg;
+ s/--(\ )*\{\*([^*]|\*[^}])*\*\}//sg;
$result = $_;