*** empty log message ***

--- a/doc-src/TutorialI/Inductive/AB.thy	Tue Apr 17 16:54:38 2001 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Tue Apr 17 19:28:04 2001 +0200
@@ -167,11 +167,13 @@
 by(simp del:append_take_drop_id);
 
 text{*\noindent
-In the proof, we have had to disable a normally useful lemma:
+In the proof we have disabled the normally useful lemma
 \begin{isabelle}
 @{thm append_take_drop_id[no_vars]}
 \rulename{append_take_drop_id}
 \end{isabelle}
+to allow the simplifier to apply the following lemma instead:
+@{text[display]"[x\<in>xs@ys. P x] = [x\<in>xs. P x] @ [x\<in>ys. P x]"}
 
 To dispose of trivial cases automatically, the rules of the inductive
 definition are declared simplification rules:
@@ -217,23 +219,21 @@
 (*<*)apply(rename_tac x v)(*>*)
 
 txt{*\noindent
-Simplification disposes of the base case and leaves only two step
-cases to be proved:
+Simplification disposes of the base case and leaves only a conjunction
+of two step cases to be proved:
 if @{prop"w = a#v"} and @{prop[display]"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
+After breaking the conjunction 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 "\<lambda>x. x=a", simplified]);
- apply(erule exE);
- apply(erule conjE);
-
+apply(rule conjI)
+ apply(clarify)
+ apply(frule part1[of "\<lambda>x. x=a", simplified])
+ apply(clarify)
 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"}
@@ -241,51 +241,52 @@
 @{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);
+ apply(drule part2[of "\<lambda>x. x=a", simplified])
+  apply(assumption)
 
 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"},
+*}
+
+ apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id])
+
+txt{*\noindent
+(the variables @{term n1} and @{term t} are the result of composing the
+theorems @{thm[source]subst} and @{thm[source]append_take_drop_id})
 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(rule S_A_B.intros)
 
-txt{*\noindent
+txt{*
 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);
+  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]"}.
-
+txt{*
 The case @{prop"w = b#v"} is proved analogously:
 *}
 
-apply(clarify);
-apply(frule part1[of "\<lambda>x. x=b", simplified]);
-apply(erule exE);
-apply(erule conjE);
-apply(drule part2[of "\<lambda>x. x=b", simplified]);
- apply(assumption);
-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);
+apply(clarify)
+apply(frule part1[of "\<lambda>x. x=b", simplified])
+apply(clarify)
+apply(drule part2[of "\<lambda>x. x=b", simplified])
+ apply(assumption)
+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 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.
+grammar, for no good reason, excludes the empty word, thus complicating
+matters just a little bit: they 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

--- a/doc-src/TutorialI/Inductive/Star.thy	Tue Apr 17 16:54:38 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy	Tue Apr 17 19:28:04 2001 +0200
@@ -91,7 +91,7 @@
 txt{*\noindent
 This is not an obscure trick but a generally applicable heuristic:
 \begin{quote}\em
-Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
+When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
 pull all other premises containing any of the $x@i$ into the conclusion
 using $\longrightarrow$.
 \end{quote}

--- a/doc-src/TutorialI/Inductive/document/AB.tex	Tue Apr 17 16:54:38 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Tue Apr 17 19:28:04 2001 +0200
@@ -156,11 +156,15 @@
 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
-In the proof, we have had to disable a normally useful lemma:
+In the proof we have disabled the normally useful lemma
 \begin{isabelle}
 \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs}
 \rulename{append_take_drop_id}
 \end{isabelle}
+to allow the simplifier to apply the following lemma instead:
+\begin{isabelle}%
+\ \ \ \ \ {\isacharbrackleft}x{\isasymin}xs{\isacharat}ys{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}x{\isasymin}ys{\isachardot}\ P\ x{\isacharbrackright}%
+\end{isabelle}
 
 To dispose of trivial cases automatically, the rules of the inductive
 definition are declared simplification rules:%
@@ -200,22 +204,21 @@
 \ \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:
+Simplification disposes of the base case and leaves only a conjunction
+of two step cases to be proved:
 if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}%
 \ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}%
 \end{isabelle} 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
+After breaking the conjunction 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}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}%
+\ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 This yields an index \isa{i\ {\isasymle}\ length\ v} such that
@@ -232,29 +235,28 @@
 \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},
+into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},%
+\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}%
+\begin{isamarkuptxt}%
+\noindent
+(the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the
+theorems \isa{subst} and \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id})
 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 analogously:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}clarify{\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}clarify{\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}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline
@@ -264,8 +266,8 @@
 \begin{isamarkuptext}%
 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.
+grammar, for no good reason, excludes the empty word, thus complicating
+matters just a little bit: they 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

--- a/doc-src/TutorialI/Inductive/document/Star.tex	Tue Apr 17 16:54:38 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex	Tue Apr 17 19:28:04 2001 +0200
@@ -96,7 +96,7 @@
 \noindent
 This is not an obscure trick but a generally applicable heuristic:
 \begin{quote}\em
-Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
+When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
 pull all other premises containing any of the $x@i$ into the conclusion
 using $\longrightarrow$.
 \end{quote}