author nipkow Tue, 17 Apr 2001 19:28:04 +0200 changeset 11257 622331bbdb7f parent 11256 49afcce3bada child 11258 84209fe9fbc9
*** 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}:
*}

-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(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)

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
\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}erule\ exE{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}clarify{\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}