# HG changeset patch
# User nipkow
# Date 971782137 -7200
# Node ID 7626cb4e14079ce70ce62dcf5d4995f5d802bef4
# Parent  20cf817f3b4ad6effcda7d6117cd1407f6d6a47f
*** empty log message ***

diff -r 20cf817f3b4a -r 7626cb4e1407 doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Tue Oct 17 10:45:51 2000 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Tue Oct 17 13:28:57 2000 +0200
@@ -2,122 +2,307 @@
 
 section{*A context free grammar*}
 
+text{*
+Grammars are nothing but shorthands for inductive definitions of nonterminals
+which represent sets of strings. For example, the production
+$A \to B c$ is short for
+\[ w \in B \Longrightarrow wc \in A \]
+This section demonstrates this idea with a standard example
+\cite[p.\ 81]{HopcroftUllman}, a grammar for generating all words with an
+equal number of $a$'s and $b$'s:
+\begin{eqnarray}
+S &\to& \epsilon \mid b A \mid a B \nonumber\\
+A &\to& a S \mid b A A \nonumber\\
+B &\to& b S \mid a B B \nonumber
+\end{eqnarray}
+At the end we say a few words about the relationship of the formalization
+and the text in the book~\cite[p.\ 81]{HopcroftUllman}.
+
+We start by fixing the alpgabet, which consists only of @{term a}'s
+and @{term b}'s:
+*}
+
 datatype alfa = a | b;
 
-lemma [simp]: "(x ~= a) = (x = b) & (x ~= b) = (x = a)";
+text{*\noindent
+For convenience we includ the following easy lemmas as simplification rules:
+*}
+
+lemma [simp]: "(x \<noteq> a) = (x = b) \<and> (x \<noteq> b) = (x = a)";
 apply(case_tac x);
 by(auto);
 
+text{*\noindent
+Words over this alphabet are of type @{typ"alfa list"}, and
+the three nonterminals are declare as sets of such words:
+*}
+
 consts S :: "alfa list set"
        A :: "alfa list set"
        B :: "alfa list set";
 
+text{*\noindent
+The above productions are recast as a \emph{simultaneous} inductive
+definition of @{term S}, @{term A} and @{term B}:
+*}
+
 inductive S A B
 intros
-"[] : S"
-"w : A ==> b#w : S"
-"w : B ==> a#w : S"
+  "[] \<in> S"
+  "w \<in> A \<Longrightarrow> b#w \<in> S"
+  "w \<in> B \<Longrightarrow> a#w \<in> S"
 
-"w : S ==> a#w : A"
-"[| v:A; w:A |] ==> b#v@w : A"
+  "w \<in> S        \<Longrightarrow> a#w   \<in> A"
+  "\<lbrakk> v\<in>A; w\<in>A \<rbrakk> \<Longrightarrow> b#v@w \<in> A"
+
+  "w \<in> S            \<Longrightarrow> b#w   \<in> B"
+  "\<lbrakk> v \<in> B; w \<in> B \<rbrakk> \<Longrightarrow> a#v@w \<in> B";
 
-"w : S ==> b#w : B"
-"[| v:B; w:B |] ==> a#v@w : B";
+text{*\noindent
+First we show that all words in @{term S} contain the same number of @{term
+a}'s and @{term b}'s. Since the definition of @{term S} is by simultaneous
+induction, so is this 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}.
+*}
 
-thm S_A_B.induct[no_vars];
+lemma correctness:
+  "(w \<in> S \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b])     \<and>
+    (w \<in> A \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1) \<and>
+    (w \<in> B \<longrightarrow> size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1)"
 
-lemma "(w : S --> size[x:w. x=a] = size[x:w. x=b]) &
-       (w : A --> size[x:w. x=a] = size[x:w. x=b] + 1) &
-       (w : B --> size[x:w. x=b] = size[x:w. x=a] + 1)";
+txt{*\noindent
+These propositions are expressed with the help of the predefined @{term
+filter} function on lists, which has the convenient syntax @{term"[x\<in>xs. P
+x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
+holds. The length of a list is usually written @{term length}, and @{term
+size} is merely a shorthand.
+
+The proof itself is by rule induction and afterwards automatic:
+*}
+
 apply(rule S_A_B.induct);
 by(auto);
 
-lemma intermed_val[rule_format(no_asm)]:
- "(!i<n. abs(f(i+1) - f i) <= #1) --> 
-  f 0 <= k & k <= f n --> (? i <= n. f i = (k::int))";
-apply(induct n);
- apply(simp);
- apply(arith);
-apply(rule);
-apply(erule impE);
- apply(simp);
-apply(rule);
-apply(erule_tac x = n in allE);
-apply(simp);
-apply(case_tac "k = f(n+1)");
- apply(force);
-apply(erule impE);
- apply(simp add:zabs_def split:split_if_asm);
- apply(arith);
-by(blast intro:le_SucI);
+text{*\noindent
+This may seem surprising at first, and is indeed an indication of the power
+of inductive definitions. But it is also quite straightforward. For example,
+consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
+contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$
+than $b$'s.
+
+As usual, the correctness of syntactic descriptions is easy, but completeness
+is hard: does @{term S} contain \emph{all} words with an equal number of
+@{term a}'s and @{term b}'s? It turns out that this proof requires the
+following little lemma: every string with two more @{term a}'s than @{term
+b}'s can be cut somehwere such that each half has one more @{term a} than
+@{term b}. This is best seen by imagining counting the difference between the
+number of @{term a}'s than @{term b}'s starting at the left end of the
+word. We start at 0 and end (at the right end) with 2. Since each move to the
+right increases or decreases the difference by 1, we must have passed through
+1 on our way from 0 to 2. Formally, we appeal to the following discrete
+intermediate value theorem @{thm[source]nat0_intermed_int_val}
+@{thm[display]nat0_intermed_int_val[no_vars]}
+where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
+@{term abs} is the absolute value function, and @{term"#1::int"} is the
+integer 1 (see \S\ref{sec:int}).
 
-lemma step1: "ALL i < size w.
-  abs((int(size[x:take (i+1) w . P x]) - int(size[x:take (i+1) w . ~P x])) -
-      (int(size[x:take i w . P x]) - int(size[x:take i w . ~P x]))) <= #1";
+First we show that the our specific function, the difference between the
+numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
+move to the right. At this point we also start generalizing from @{term a}'s
+and @{term b}'s to an arbitrary property @{term P}. Otherwise we would have
+to prove the desired lemma twice, once as stated above and once with the
+roles of @{term a}'s and @{term b}'s interchanged.
+*}
+
+lemma step1: "\<forall>i < size w.
+  abs((int(size[x\<in>take (i+1) w.  P x]) -
+       int(size[x\<in>take (i+1) w. \<not>P x]))
+      -
+      (int(size[x\<in>take i w.  P x]) -
+       int(size[x\<in>take i w. \<not>P x]))) <= #1";
+
+txt{*\noindent
+The lemma is a bit hard to read because of the coercion function
+@{term[source]"int::nat \<Rightarrow> int"}. It is required because @{term size} returns
+a natural number, but @{text-} on @{typ nat} will do the wrong thing.
+Function @{term take} is predefined and @{term"take i xs"} is the prefix of
+length @{term i} of @{term xs}; below we als need @{term"drop i xs"}, which
+is what remains after that prefix has been dropped from @{term xs}.
+
+The proof is by induction on @{term w}, with a trivial base case, and a not
+so trivial induction step. Since it is essentially just arithmetic, we do not
+discuss it.
+*}
+
 apply(induct w);
  apply(simp);
-apply(simp add:take_Cons split:nat.split);
-apply(clarsimp);
-apply(rule conjI);
- apply(clarify);
- apply(erule allE);
- apply(erule impE);
-  apply(assumption);
- apply(arith);
-apply(clarify);
-apply(erule allE);
-apply(erule impE);
- apply(assumption);
-by(arith);
+by(force simp add:zabs_def take_Cons split:nat.split if_splits); 
 
+text{*
+Finally we come to the above mentioned lemma about cutting a word with two
+more elements of one sort than of the other sort into two halfs:
+*}
 
 lemma part1:
- "size[x:w. P x] = Suc(Suc(size[x:w. ~P x])) ==>
-  EX i<=size w. size[x:take i w. P x] = size[x:take i w. ~P x]+1";
-apply(insert intermed_val[OF step1, of "P" "w" "#1"]);
-apply(simp);
-apply(erule exE);
-apply(rule_tac x=i in exI);
-apply(simp);
-apply(rule int_int_eq[THEN iffD1]);
-apply(simp);
-by(arith);
+ "size[x\<in>w. P x] = size[x\<in>w. \<not>P x]+2 \<Longrightarrow>
+  \<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1";
+
+txt{*\noindent
+This is proved with the help of the intermediate value theorem, instantiated
+appropriately and with its first premise disposed of by lemma
+@{thm[source]step1}.
+*}
+
+apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "#1"]);
+apply simp;
+by(simp del:int_Suc add:zdiff_eq_eq sym[OF int_Suc]);
+
+text{*\noindent
+The additional lemmas are needed to mediate between @{typ nat} and @{typ int}.
+
+Lemma @{thm[source]part1} tells us only about the prefix @{term"take i w"}.
+The suffix @{term"drop i w"} is dealt with in the following easy lemma:
+*}
+
 
 lemma part2:
-"[| size[x:take i xs @ drop i xs. P x] = size[x:take i xs @ drop i xs. ~P x]+2;
-    size[x:take i xs. P x] = size[x:take i xs. ~P x]+1 |]
- ==> size[x:drop i xs. P x] = size[x:drop i xs. ~P x]+1";
+  "\<lbrakk>size[x\<in>take i w @ drop i w. P x] =
+    size[x\<in>take i w @ drop i w. \<not>P x]+2;
+    size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1\<rbrakk>
+   \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1";
 by(simp del:append_take_drop_id);
 
-lemmas [simp] = S_A_B.intros;
+text{*\noindent
+Lemma @{thm[source]append_take_drop_id}, @{thm append_take_drop_id[no_vars]},
+which is generally useful, needs to be disabled for once.
+
+To dispose of trivial cases automatically, the rules of the inductive
+definition are declared simplification rules:
+*}
+
+declare S_A_B.intros[simp];
+
+text{*\noindent
+This could have been done earlier but was not necessary so far.
+
+The completeness theorem tells us that if a word has the same number of
+@{term a}'s and @{term b}'s, then it is in @{term S}, and similarly and
+simultaneously for @{term A} and @{term B}:
+*}
+
+theorem completeness:
+  "(size[x\<in>w. x=a] = size[x\<in>w. x=b]     \<longrightarrow> w \<in> S) \<and>
+    (size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
+    (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)";
+
+txt{*\noindent
+The proof is by induction on @{term w}. Structural induction would fail here
+because, as we can see from the grammar, we need to make bigger steps than
+merely appending a single letter at the front. Hence we induct on the length
+of @{term w}, using the induction rule @{thm[source]length_induct}:
+*}
 
-lemma "(size[x:w. x=a] = size[x:w. x=b] --> w : S) &
-       (size[x:w. x=a] = size[x:w. x=b] + 1 --> w : A) &
-       (size[x:w. x=b] = size[x:w. x=a] + 1 --> w : B)";
 apply(induct_tac w rule: length_induct);
-apply(case_tac "xs");
- apply(simp);
-apply(simp);
+(*<*)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}.
+
+The proof continues with a case distinction on @{term w},
+i.e.\ if @{term w} is empty or not.
+*}
+
+apply(case_tac w);
+ apply(simp_all);
+(*<*)apply(rename_tac x v)(*>*)
+
+txt{*\noindent
+Simplification disposes of the base case and leaves only two step
+cases to be proved:
+if @{prop"w = a#v"} and @{prop"size[x\<in>v. x=a] = size[x\<in>v. x=b]+2"} then
+@{prop"b#v \<in> A"}, and similarly for @{prop"w = b#v"}.
+We only consider the first case in detail.
+
+After breaking the conjuction up into two cases, we can apply
+@{thm[source]part1} to the assumption that @{term w} contains two more @{term
+a}'s than @{term b}'s.
+*}
+
 apply(rule conjI);
  apply(clarify);
- apply(frule part1[of "%x. x=a", simplified]);
+ apply(frule part1[of "\<lambda>x. x=a", simplified]);
  apply(erule exE);
  apply(erule conjE);
- apply(drule part2[of "%x. x=a", simplified]);
+
+txt{*\noindent
+This yields an index @{prop"i \<le> length v"} such that
+@{prop"length [x\<in>take i v . x = a] = length [x\<in>take i v . x = b] + 1"}.
+With the help of @{thm[source]part1} it follows that
+@{prop"length [x\<in>drop i v . x = a] = length [x\<in>drop i v . x = b] + 1"}.
+*}
+
+ apply(drule part2[of "\<lambda>x. x=a", simplified]);
   apply(assumption);
- apply(rule_tac n1=i and t=list in subst[OF append_take_drop_id]);
+
+txt{*\noindent
+Now it is time to decompose @{term v} in the conclusion @{prop"b#v \<in> A"}
+into @{term"take i v @ drop i v"},
+after which the appropriate rule of the grammar reduces the goal
+to the two subgoals @{prop"take i v \<in> A"} and @{prop"drop i v \<in> A"}:
+*}
+
+ apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id]);
  apply(rule S_A_B.intros);
-  apply(force simp add:min_less_iff_disj);
+
+txt{*\noindent
+Both subgoals follow from the induction hypothesis because both @{term"take i
+v"} and @{term"drop i v"} are shorter than @{term w}:
+*}
+
+  apply(force simp add: min_less_iff_disj);
  apply(force split add: nat_diff_split);
+
+txt{*\noindent
+Note that the variables @{term n1} and @{term t} referred to in the
+substitution step above come from the derived theorem @{text"subst[OF
+append_take_drop_id]"}.
+
+The case @{prop"w = b#v"} is proved completely analogously:
+*}
+
 apply(clarify);
-apply(frule part1[of "%x. x=b", simplified]);
+apply(frule part1[of "\<lambda>x. x=b", simplified]);
 apply(erule exE);
 apply(erule conjE);
-apply(drule part2[of "%x. x=b", simplified]);
+apply(drule part2[of "\<lambda>x. x=b", simplified]);
  apply(assumption);
-apply(rule_tac n1=i and t=list in subst[OF append_take_drop_id]);
+apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id]);
 apply(rule S_A_B.intros);
  apply(force simp add:min_less_iff_disj);
 by(force simp add:min_less_iff_disj split add: nat_diff_split);
 
+text{*
+We conclude this section with a comparison of the above proof and the one
+in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook
+grammar, for no good reason, excludes the empty word, which complicates
+matters just a little bit because we now have 8 instead of our 7 productions.
+
+More importantly, the proof itself is different: rather than separating the
+two directions, they perform one induction on the length of a word. This
+deprives them of the beauty of rule induction and in the easy direction
+(correctness) their reasoning is more detailed than our @{text auto}. For the
+hard part (completeness), they consider just one of the cases that our @{text
+simp_all} disposes of automatically. Then they conclude the proof by saying
+about the remaining cases: ``We do this in a manner similar to our method of
+proof for part (1); this part is left to the reader''. But this is precisely
+the part that requires the intermediate value theorem and thus is not at all
+similar to the other cases (which are automatic in Isabelle). We conclude
+that the authors are at least cavalier about this point and may even have
+overlooked the slight difficulty lurking in the omitted cases. This is not
+atypical for pen-and-paper proofs, once analysed in detail.  *}
+
 (*<*)end(*>*)
diff -r 20cf817f3b4a -r 7626cb4e1407 doc-src/TutorialI/Inductive/document/AB.tex
--- a/doc-src/TutorialI/Inductive/document/AB.tex	Tue Oct 17 10:45:51 2000 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Tue Oct 17 13:28:57 2000 +0200
@@ -3,123 +3,278 @@
 \def\isabellecontext{AB}%
 %
 \isamarkupsection{A context free grammar}
-\isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b\isanewline
-\isanewline
-\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isacharampersand}\ {\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline
+%
+\begin{isamarkuptext}%
+Grammars are nothing but shorthands for inductive definitions of nonterminals
+which represent sets of strings. For example, the production
+$A \to B c$ is short for
+\[ w \in B \Longrightarrow wc \in A \]
+This section demonstrates this idea with a standard example
+\cite[p.\ 81]{HopcroftUllman}, a grammar for generating all words with an
+equal number of $a$'s and $b$'s:
+\begin{eqnarray}
+S &\to& \epsilon \mid b A \mid a B \nonumber\\
+A &\to& a S \mid b A A \nonumber\\
+B &\to& b S \mid a B B \nonumber
+\end{eqnarray}
+At the end we say a few words about the relationship of the formalization
+and the text in the book~\cite[p.\ 81]{HopcroftUllman}.
+
+We start by fixing the alpgabet, which consists only of \isa{a}'s
+and \isa{b}'s:%
+\end{isamarkuptext}%
+\isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
+\begin{isamarkuptext}%
+\noindent
+For convenience we includ the following easy lemmas as simplification rules:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}x\ {\isasymnoteq}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
-\isanewline
+\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+Words over this alphabet are of type \isa{alfa\ list}, and
+the three nonterminals are declare as sets of such words:%
+\end{isamarkuptext}%
 \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
 \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline
-\isanewline
+\ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+The above productions are recast as a \emph{simultaneous} inductive
+definition of \isa{S}, \isa{A} and \isa{B}:%
+\end{isamarkuptext}%
 \isacommand{inductive}\ S\ A\ B\isanewline
 \isakeyword{intros}\isanewline
-{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}\ S{\isachardoublequote}\isanewline
-{\isachardoublequote}w\ {\isacharcolon}\ A\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}w\ {\isacharcolon}\ S{\isachardoublequote}\isanewline
-{\isachardoublequote}w\ {\isacharcolon}\ B\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}w\ {\isacharcolon}\ S{\isachardoublequote}\isanewline
-\isanewline
-{\isachardoublequote}w\ {\isacharcolon}\ S\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}w\ {\isacharcolon}\ A{\isachardoublequote}\isanewline
-{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ v{\isacharcolon}A{\isacharsemicolon}\ w{\isacharcolon}A\ {\isacharbar}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}v{\isacharat}w\ {\isacharcolon}\ A{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline
 \isanewline
-{\isachardoublequote}w\ {\isacharcolon}\ S\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}w\ {\isacharcolon}\ B{\isachardoublequote}\isanewline
-{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ v{\isacharcolon}B{\isacharsemicolon}\ w{\isacharcolon}B\ {\isacharbar}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}v{\isacharat}w\ {\isacharcolon}\ B{\isachardoublequote}\isanewline
-\isanewline
-\isacommand{thm}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}\isanewline
-\isanewline
-\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}w\ {\isacharcolon}\ S\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ {\isacharampersand}\isanewline
-\ \ \ \ \ \ \ {\isacharparenleft}w\ {\isacharcolon}\ A\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharampersand}\isanewline
-\ \ \ \ \ \ \ {\isacharparenleft}w\ {\isacharcolon}\ B\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
+\ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline
 \isanewline
-\isacommand{lemma}\ intermed{\isacharunderscore}val{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
-\ {\isachardoublequote}{\isacharparenleft}{\isacharbang}i{\isacharless}n{\isachardot}\ abs{\isacharparenleft}f{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isacharparenright}\ {\isacharminus}{\isacharminus}{\isachargreater}\ \isanewline
-\ \ f\ {\isadigit{0}}\ {\isacharless}{\isacharequal}\ k\ {\isacharampersand}\ k\ {\isacharless}{\isacharequal}\ f\ n\ {\isacharminus}{\isacharminus}{\isachargreater}\ {\isacharparenleft}{\isacharquery}\ i\ {\isacharless}{\isacharequal}\ n{\isachardot}\ f\ i\ {\isacharequal}\ {\isacharparenleft}k{\isacharcolon}{\isacharcolon}int{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ n\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequote}k\ {\isacharequal}\ f{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}force{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ split{\isacharcolon}split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}le{\isacharunderscore}SucI{\isacharparenright}\isanewline
-\isanewline
-\isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}ALL\ i\ {\isacharless}\ size\ w{\isachardot}\isanewline
-\ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w\ {\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\ int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w\ {\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharminus}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ i\ w\ {\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\ int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ i\ w\ {\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}%
+\begin{isamarkuptext}%
+\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 simultaneous
+induction, so is this 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}.%
+\end{isamarkuptext}%
+\isacommand{lemma}\ correctness{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline
+\ \ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline
+\ \ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{filter\ P\ xs}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x}
+holds. The length of a list is usually written \isa{size}, and \isa{size} is merely a shorthand.
+
+The proof itself is by rule induction and afterwards automatic:%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline
+\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+This may seem surprising at first, and is indeed an indication of the power
+of inductive definitions. But it is also quite straightforward. For example,
+consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$
+contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$
+than $b$'s.
+
+As usual, the correctness of syntactic descriptions is easy, but completeness
+is hard: does \isa{S} contain \emph{all} words with an equal number of
+\isa{a}'s and \isa{b}'s? It turns out that this proof requires the
+following little lemma: every string with two more \isa{a}'s than \isa{b}'s can be cut somehwere such that each half has one more \isa{a} than
+\isa{b}. This is best seen by imagining counting the difference between the
+number of \isa{a}'s than \isa{b}'s starting at the left end of the
+word. We start at 0 and end (at the right end) with 2. Since each move to the
+right increases or decreases the difference by 1, we must have passed through
+1 on our way from 0 to 2. Formally, we appeal to the following discrete
+intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
+\begin{isabelle}%
+\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ abs\ {\isacharparenleft}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
+\ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
+\end{isabelle}
+where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
+\isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
+integer 1 (see \S\ref{sec:int}).
+
+First we show that the our specific function, the difference between the
+numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
+move to the right. At this point we also start generalizing from \isa{a}'s
+and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have
+to prove the desired lemma twice, once as stated above and once with the
+roles of \isa{a}'s and \isa{b}'s interchanged.%
+\end{isamarkuptext}%
+\isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
+\ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
+\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
+\ \ \ \ \ \ {\isacharminus}\isanewline
+\ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
+\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+The lemma is a bit hard to read because of the coercion function
+\isa{{\isachardoublequote}int{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
+a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing.
+Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
+length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which
+is what remains after that prefix has been dropped from \isa{xs}.
+
+The proof is by induction on \isa{w}, with a trivial base case, and a not
+so trivial induction step. Since it is essentially just arithmetic, we do not
+discuss it.%
+\end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline
 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline
+\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
+\begin{isamarkuptext}%
+Finally we come to the above mentioned lemma about cutting a word with two
+more elements of one sort than of the other sort into two halfs:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
+\ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline
+\ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+This is proved with the help of the intermediate value theorem, instantiated
+appropriately and with its first premise disposed of by lemma
+\isa{step{\isadigit{1}}}.%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline
+\isacommand{apply}\ simp\isanewline
+\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}int{\isacharunderscore}Suc\ add{\isacharcolon}zdiff{\isacharunderscore}eq{\isacharunderscore}eq\ sym{\isacharbrackleft}OF\ int{\isacharunderscore}Suc{\isacharbrackright}{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+The additional lemmas are needed to mediate between \isa{nat} and \isa{int}.
+
+Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
+The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline
+\ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
+\ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isasymrbrakk}\isanewline
+\ \ \ {\isasymLongrightarrow}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+Lemma \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}, \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs},
+which is generally useful, needs to be disabled for once.
+
+To dispose of trivial cases automatically, the rules of the inductive
+definition are declared simplification rules:%
+\end{isamarkuptext}%
+\isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}%
+\begin{isamarkuptext}%
+\noindent
+This could have been done earlier but was not necessary so far.
+
+The completeness theorem tells us that if a word has the same number of
+\isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly and
+simultaneously for \isa{A} and \isa{B}:%
+\end{isamarkuptext}%
+\isacommand{theorem}\ completeness{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline
+\ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline
+\ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+The proof is by induction on \isa{w}. Structural induction would fail here
+because, as we can see from the grammar, we need to make bigger steps than
+merely appending a single letter at the front. Hence we induct on the length
+of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\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}.
+
+The proof continues with a case distinction on \isa{w},
+i.e.\ if \isa{w} is empty or not.%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+Simplification disposes of the base case and leaves only two step
+cases to be proved:
+if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \isa{length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}} then
+\isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}.
+We only consider the first case in detail.
+
+After breaking the conjuction up into two cases, we can apply
+\isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.%
+\end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
 \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}erule\ allE{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
-\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+This yields an index \isa{i\ {\isasymle}\ length\ v} such that
+\isa{length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}}.
+With the help of \isa{part{\isadigit{1}}} it follows that
+\isa{length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}}.%
+\end{isamarkuptxt}%
+\ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}
+into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},
+after which the appropriate rule of the grammar reduces the goal
+to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:%
+\end{isamarkuptxt}%
+\ \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:%
+\end{isamarkuptxt}%
+\ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+Note that the variables \isa{n{\isadigit{1}}} and \isa{t} referred to in the
+substitution step above come from the derived theorem \isa{subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}}.
+
+The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved completely analogously:%
+\end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ allE{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
-\isanewline
-\isanewline
-\isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
-\ {\isachardoublequote}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ Suc{\isacharparenleft}Suc{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}{\isacharequal}{\isachargreater}\isanewline
-\ \ EX\ i{\isacharless}{\isacharequal}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ w{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}insert\ intermed{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}i\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule\ int{\isacharunderscore}int{\isacharunderscore}eq{\isacharbrackleft}THEN\ iffD{\isadigit{1}}{\isacharbrackright}{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
-\isanewline
-\isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline
-{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs\ {\isacharat}\ drop\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs\ {\isacharat}\ drop\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline
-\ \ \ \ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}\ {\isacharbar}{\isacharbrackright}\isanewline
-\ {\isacharequal}{\isacharequal}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}drop\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}drop\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isanewline
-\isanewline
-\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros\isanewline
-\isanewline
-\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ S{\isacharparenright}\ {\isacharampersand}\isanewline
-\ \ \ \ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ A{\isacharparenright}\ {\isacharampersand}\isanewline
-\ \ \ \ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ B{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequote}xs{\isachardoublequote}{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
-\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}list\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
-\ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline
 \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}list\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
 \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
+\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
+\begin{isamarkuptext}%
+We conclude this section with a comparison of the above proof and the one
+in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook
+grammar, for no good reason, excludes the empty word, which complicates
+matters just a little bit because we now have 8 instead of our 7 productions.
+
+More importantly, the proof itself is different: rather than separating the
+two directions, they perform one induction on the length of a word. This
+deprives them of the beauty of rule induction and in the easy direction
+(correctness) their reasoning is more detailed than our \isa{auto}. For the
+hard part (completeness), they consider just one of the cases that our \isa{simp{\isacharunderscore}all} disposes of automatically. Then they conclude the proof by saying
+about the remaining cases: ``We do this in a manner similar to our method of
+proof for part (1); this part is left to the reader''. But this is precisely
+the part that requires the intermediate value theorem and thus is not at all
+similar to the other cases (which are automatic in Isabelle). We conclude
+that the authors are at least cavalier about this point and may even have
+overlooked the slight difficulty lurking in the omitted cases. This is not
+atypical for pen-and-paper proofs, once analysed in detail.%
+\end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 20cf817f3b4a -r 7626cb4e1407 doc-src/TutorialI/Misc/AdvancedInd.thy
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Oct 17 10:45:51 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Oct 17 13:28:57 2000 +0200
@@ -231,13 +231,17 @@
 identity.
 \end{exercise}
 
-In general, @{text"induct_tac"} can be applied with any rule $r$
+In general, @{text induct_tac} can be applied with any rule $r$
 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
 format is
 \begin{quote}
 \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
 \end{quote}\index{*induct_tac}%
 where $y@1, \dots, y@n$ are variables in the first subgoal.
+A further example of a useful induction rule is @{thm[source]length_induct},
+induction on the length of a list:\indexbold{*length_induct}
+@{thm[display]length_induct[no_vars]}
+
 In fact, @{text"induct_tac"} even allows the conclusion of
 $r$ to be an (iterated) conjunction of formulae of the above form, in
 which case the application is
diff -r 20cf817f3b4a -r 7626cb4e1407 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Oct 17 10:45:51 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Oct 17 13:28:57 2000 +0200
@@ -216,6 +216,12 @@
 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
 \end{quote}\index{*induct_tac}%
 where $y@1, \dots, y@n$ are variables in the first subgoal.
+A further example of a useful induction rule is \isa{length{\isacharunderscore}induct},
+induction on the length of a list:\indexbold{*length_induct}
+\begin{isabelle}%
+\ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs%
+\end{isabelle}
+
 In fact, \isa{induct{\isacharunderscore}tac} even allows the conclusion of
 $r$ to be an (iterated) conjunction of formulae of the above form, in
 which case the application is
diff -r 20cf817f3b4a -r 7626cb4e1407 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Tue Oct 17 10:45:51 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Oct 17 13:28:57 2000 +0200
@@ -40,8 +40,8 @@
 Next, two functions @{text"app"} and \isaindexbold{rev} are declared:
 *}
 
-consts app :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list"   (infixr "@" 65)
-       rev :: "'a list \\<Rightarrow> 'a list";
+consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"   (infixr "@" 65)
+       rev :: "'a list \<Rightarrow> 'a list";
 
 text{*
 \noindent
@@ -100,7 +100,7 @@
 dropped, unless the identifier happens to be a keyword, as in
 *}
 
-consts "end" :: "'a list \\<Rightarrow> 'a"
+consts "end" :: "'a list \<Rightarrow> 'a"
 
 text{*\noindent
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
@@ -188,7 +188,7 @@
 \end{isabelle}
 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
 ignored most of the time, or simply treated as a list of variables local to
-this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
+this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}.
 The {\it assumptions} are the local assumptions for this subgoal and {\it
   conclusion} is the actual proposition to be proved. Typical proof steps
 that add new assumptions are induction or case distinction. In our example
diff -r 20cf817f3b4a -r 7626cb4e1407 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Oct 17 10:45:51 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Oct 17 13:28:57 2000 +0200
@@ -183,7 +183,7 @@
 \end{isabelle}
 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
 ignored most of the time, or simply treated as a list of variables local to
-this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
+this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}.
 The {\it assumptions} are the local assumptions for this subgoal and {\it
   conclusion} is the actual proposition to be proved. Typical proof steps
 that add new assumptions are induction or case distinction. In our example
diff -r 20cf817f3b4a -r 7626cb4e1407 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Tue Oct 17 10:45:51 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias	Tue Oct 17 13:28:57 2000 +0200
@@ -36,6 +36,8 @@
 
 it would be nice if one could get id to the enclosing quotes in the [source] option.
 
+arithmetic: allow mixed nat/int formulae
+-> simplify proof of part1 in Inductive/AB.thy
 
 Minor fixes in the tutorial
 ===========================
diff -r 20cf817f3b4a -r 7626cb4e1407 doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Tue Oct 17 10:45:51 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Tue Oct 17 13:28:57 2000 +0200
@@ -66,6 +66,7 @@
 \input{basics}
 \input{fp}
 \chapter{The Rules of the Game}
+\label{ch:Rules}
 \input{sets}
 \input{Inductive/inductive}
 \input{Advanced/advanced}