--- a/doc-src/TutorialI/Fun/document/fun0.tex Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Fun/document/fun0.tex Thu Jun 12 14:20:25 2008 +0200
@@ -322,7 +322,7 @@
\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
\end{quote}\index{*induct_tac (method)}%
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
-name of a function that takes an $n$ arguments. Usually the subgoal will
+name of a function that takes $n$ arguments. Usually the subgoal will
contain the term $f x@1 \dots x@n$ but this need not be the case. The
induction rules do not mention $f$ at all. Here is \isa{sep{\isachardot}induct}:
\begin{isabelle}
--- a/doc-src/TutorialI/Fun/fun0.thy Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Fun/fun0.thy Thu Jun 12 14:20:25 2008 +0200
@@ -239,7 +239,7 @@
\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
\end{quote}\index{*induct_tac (method)}%
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
-name of a function that takes an $n$ arguments. Usually the subgoal will
+name of a function that takes $n$ arguments. Usually the subgoal will
contain the term $f x@1 \dots x@n$ but this need not be the case. The
induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:
\begin{isabelle}
--- a/doc-src/TutorialI/Inductive/AB.thy Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy Thu Jun 12 14:20:25 2008 +0200
@@ -60,7 +60,7 @@
a}'s and @{term b}'s. Since the definition of @{term S} is by mutual
induction, so is the proof: we show at the same time that all words in
@{term A} contain one more @{term a} than @{term b} and all words in @{term
-B} contains one more @{term b} than @{term a}.
+B} contain one more @{term b} than @{term a}.
*}
lemma correctness:
@@ -199,13 +199,14 @@
*}
apply(induct_tac w rule: length_induct)
-(*<*)apply(rename_tac w)(*>*)
+apply(rename_tac w)
txt{*\noindent
The @{text rule} parameter tells @{text induct_tac} explicitly which induction
rule to use. For details see \S\ref{sec:complete-ind} below.
In this case the result is that we may assume the lemma already
-holds for all words shorter than @{term w}.
+holds for all words shorter than @{term w}. Because the induction step renames
+the induction variable we rename it back to @{text w}.
The proof continues with a case distinction on @{term w},
on whether @{term w} is empty or not.
--- a/doc-src/TutorialI/Inductive/Advanced.thy Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Inductive/Advanced.thy Thu Jun 12 14:20:25 2008 +0200
@@ -234,8 +234,8 @@
apply (erule well_formed_gterm'.induct)
(*>*)
txt {*
-The proof script is identical, but the subgoal after applying induction may
-be surprising:
+The proof script is virtually identical,
+but the subgoal after applying induction may be surprising:
@{subgoals[display,indent=0,margin=65]}
The induction hypothesis contains an application of @{term lists}. Using a
monotone function in the inductive definition always has this effect. The
--- a/doc-src/TutorialI/Inductive/document/AB.tex Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Thu Jun 12 14:20:25 2008 +0200
@@ -93,7 +93,7 @@
\noindent
First we show that all words in \isa{S} contain the same number of \isa{a}'s and \isa{b}'s. Since the definition of \isa{S} is by mutual
induction, so is the proof: we show at the same time that all words in
-\isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.%
+\isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contain one more \isa{b} than \isa{a}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
@@ -303,13 +303,16 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
+{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isacharparenleft}rename{\isacharunderscore}tac\ w{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
rule to use. For details see \S\ref{sec:complete-ind} below.
In this case the result is that we may assume the lemma already
-holds for all words shorter than \isa{w}.
+holds for all words shorter than \isa{w}. Because the induction step renames
+the induction variable we rename it back to \isa{w}.
The proof continues with a case distinction on \isa{w},
on whether \isa{w} is empty or not.%
--- a/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Jun 12 14:20:25 2008 +0200
@@ -346,8 +346,8 @@
\isatagproof
%
\begin{isamarkuptxt}%
-The proof script is identical, but the subgoal after applying induction may
-be surprising:
+The proof script is virtually identical,
+but the subgoal after applying induction may be surprising:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline
--- a/doc-src/TutorialI/Rules/rules.tex Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Jun 12 14:20:25 2008 +0200
@@ -220,7 +220,7 @@
The result of this proof is a new inference rule \isa{disj_swap}, which is neither
an introduction nor an elimination rule, but which might
be useful. We can use it to replace any goal of the form $Q\disj P$
-by a one of the form $P\disj Q$.%
+by one of the form $P\disj Q$.%
\index{elimination rules|)}
@@ -515,16 +515,15 @@
\begin{isabelle}
\isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\
\isasymLongrightarrow\ P\ \isasymor\ (Q\ \isasymand\ R)"\isanewline
-\isacommand{apply}\ (intro\ disjCI\ conjI)\isanewline
+\isacommand{apply}\ (rule\ disjCI)\isanewline
\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline
\ \isacommand{apply}\ assumption
\isanewline
\isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI)
\end{isabelle}
%
-The first proof step uses \isa{intro} to apply
-the introduction rules \isa{disjCI} and \isa{conjI}. The resulting
-subgoal has the negative assumption
+The first proof step to applies the introduction rules \isa{disjCI}.
+The resulting subgoal has the negative assumption
\hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}.
\begin{isabelle}
@@ -901,11 +900,11 @@
arbitrary, since it has not been assumed to satisfy any special conditions.
Isabelle's underlying formalism, called the
\bfindex{meta-logic}, eliminates the need for English. It provides its own
-universal quantifier (\isasymAnd) to express the notion of an arbitrary value. We
-have already seen another symbol of the meta-logic, namely
-\isa\isasymLongrightarrow, which expresses inference rules and the treatment of
-assumptions. The only other symbol in the meta-logic is \isa\isasymequiv, which
-can be used to define constants.
+universal quantifier (\isasymAnd) to express the notion of an arbitrary value.
+We have already seen another operator of the meta-logic, namely
+\isa\isasymLongrightarrow, which expresses inference rules and the treatment
+of assumptions. The only other operator in the meta-logic is \isa\isasymequiv,
+which can be used to define constants.
\subsection{The Universal Introduction Rule}