doc-src/TutorialI/Inductive/AB.thy

 @{thm[display]nat0_intermed_int_val[no_vars]}
 where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
 @{text"\<bar>.\<bar>"} is the absolute value function, and @{term"#1::int"} is the
 integer 1 (see \S\ref{sec:numbers}).
 
-First we show that the our specific function, the difference between the
+First we show that 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.

   \<bar>(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]))\<bar> \<le> #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
+@{text"int :: nat \<Rightarrow> int"}. It is required because @{term size} returns
 a natural number, but subtraction on type~@{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 also need @{term"drop i xs"}, which
 is what remains after that prefix has been dropped from @{term xs}.
 

  apply(erule conjE);
 
 txt{*\noindent
 This yields an index @{prop"i \<le> length v"} such that
 @{prop[display]"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
+With the help of @{thm[source]part2} it follows that
 @{prop[display]"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);

 We conclude this section with a comparison of our proof with 
 Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook
 grammar, for no good reason, excludes the empty word.  That 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.  *}
+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). 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(*>*)