# HG changeset patch
# User nipkow
# Date 1026281375 -7200
# Node ID c9e9b6add7541232249d80d14b465067c3af74bb
# Parent  53c4ec15cae05fb0aa77882e0ab369d80a311345
*** empty log message ***

diff -r 53c4ec15cae0 -r c9e9b6add754 doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Jul 10 07:20:02 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Jul 10 08:09:35 2002 +0200
@@ -60,7 +60,7 @@
 The operational reading: the \isakeyword{assume}-\isakeyword{show} block
 proves @{prop"A \<Longrightarrow> A"},
 which rule @{thm[source]impI} turns into the desired @{prop"A \<longrightarrow> A"}.
-However, this text is much too detailled for comfort. Therefore Isar
+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
@@ -193,7 +193,7 @@
 
 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 nontrival proof where one cannot bridge the gap between 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}.
@@ -247,7 +247,7 @@
 qed
 text{*\noindent Apart from demonstrating the strangeness of classical
 arguments by contradiction, this example also introduces two new
-abbrebviations:
+abbreviations:
 \begin{center}
 \begin{tabular}{lcl}
 \isakeyword{hence} &=& \isakeyword{then} \isakeyword{have} \\
@@ -331,7 +331,7 @@
 \end{center}
 \medskip
 
-Sometimes it is necessary to supress the implicit application of rules in a
+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}: *}
@@ -354,7 +354,7 @@
 (the universal quantifier at the
 meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to
 @{text"\<Longrightarrow>"}. Here is a sample proof, annotated with the rules that are
-applied implictly: *}
+applied implicitly: *}
 lemma assumes P: "\<forall>x. P x" shows "\<forall>x. P(f x)"
 proof  -- "@{thm[source]allI}: @{thm allI[no_vars]}"
   fix a
@@ -602,7 +602,7 @@
 
 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} somewehere.
+but we wanted to use @{term i} somewhere.
 
 Let us now tackle a more ambitious lemma: proving complete induction
 @{prop[display,indent=5]"(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n) \<Longrightarrow> P n"}
@@ -627,7 +627,7 @@
   qed
 qed
 text{* \noindent Let us first examine the statement of the lemma.
-In contrast to the style advertized in the
+In contrast to the style advertised in the
 Tutorial~\cite{LNCS2283}, structured Isar proofs do not need to
 introduce @{text"\<forall>"} or @{text"\<longrightarrow>"} into a theorem to strengthen it
 for induction --- we use @{text"\<And>"} and @{text"\<Longrightarrow>"} instead. This
@@ -645,7 +645,7 @@
 n)"} used above is not the whole truth. The variable names after the case
 name (here: @{term Suc}) are the names of the parameters of that subgoal. So
 far the only parameters where the arguments to the constructor, but now we
-have an additonal parameter coming from the @{text"\<And>m"} in the main
+have an additional parameter coming from the @{text"\<And>m"} in the main
 \isakeyword{shows} clause. Thus @{text"(Suc n m)"} does not mean that
 constructor @{term Suc} is applied to two arguments but that the two
 parameters in the @{term Suc} case are to be named @{text n} and @{text
@@ -701,12 +701,20 @@
 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 chose recursion induction, i.e.\
+induction based on a recursive function definition. The example is an unusual
+definition of rotation of a list: *}
+
 consts rot :: "'a list \<Rightarrow> 'a list"
 recdef rot "measure length"
 "rot [] = []"
 "rot [x] = [x]"
 "rot (x#y#zs) = y # rot(x#zs)"
 
+text{* The proof is trivial: all three cases go through by simplification.*}
 lemma "length(rot xs) = length xs" (is "?P xs")
 proof (induct xs rule: rot.induct)
   show "?P []" by simp
@@ -717,4 +725,11 @@
   thus "?P (x#y#zs)" by simp
 qed
 
+text{*\noindent This schema works for arbitrary induction rules instead of
+@{thm[source]rot.induct}.
+
+Of course the above proof is simple enough that it could be condensed to*}
+(*<*)lemma "length(rot xs) = length xs"(*>*)
+by (induct xs rule: rot.induct, simp_all)
+
 (*<*)end(*>*)
diff -r 53c4ec15cae0 -r c9e9b6add754 doc-src/TutorialI/IsarOverview/Isar/document/root.tex
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Wed Jul 10 07:20:02 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Wed Jul 10 08:09:35 2002 +0200
@@ -18,7 +18,7 @@
 
 \noindent
 This is a very compact introduction to structured proofs in
-Isar/HOL, an extension of Isabelle/HOL~\cite{LNCS2283}. A detailled
+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}.