# HG changeset patch # User nipkow # Date 987528484 -7200 # Node ID 622331bbdb7f0f8987e3fc730113f5be6c140c92 # Parent 49afcce3bada3f423ce676bd0e87d286ade6271f *** empty log message *** diff -r 49afcce3bada -r 622331bbdb7f doc-src/TutorialI/Inductive/AB.thy --- 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\xs@ys. P x] = [x\xs. P x] @ [x\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\v. x=a] = size[x\v. x=b]+2"} then @{prop"b#v \ 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 "\x. x=a", simplified]); - apply(erule exE); - apply(erule conjE); - +apply(rule conjI) + apply(clarify) + apply(frule part1[of "\x. x=a", simplified]) + apply(clarify) txt{*\noindent This yields an index @{prop"i \ length v"} such that @{prop[display]"length [x\take i v . x = a] = length [x\take i v . x = b] + 1"} @@ -241,51 +241,52 @@ @{prop[display]"length [x\drop i v . x = a] = length [x\drop i v . x = b] + 1"} *} - apply(drule part2[of "\x. x=a", simplified]); - apply(assumption); + apply(drule part2[of "\x. x=a", simplified]) + apply(assumption) txt{*\noindent Now it is time to decompose @{term v} in the conclusion @{prop"b#v \ 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 \ A"} and @{prop"drop i v \ 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 "\x. x=b", simplified]); -apply(erule exE); -apply(erule conjE); -apply(drule part2[of "\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 "\x. x=b", simplified]) +apply(clarify) +apply(drule part2[of "\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 diff -r 49afcce3bada -r 622331bbdb7f doc-src/TutorialI/Inductive/Star.thy --- 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} diff -r 49afcce3bada -r 622331bbdb7f doc-src/TutorialI/Inductive/document/AB.tex --- 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 diff -r 49afcce3bada -r 622331bbdb7f doc-src/TutorialI/Inductive/document/Star.tex --- 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}