24 the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version. |
26 the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version. |
25 |
27 |
26 We start by fixing the alphabet, which consists only of \isa{a}'s |
28 We start by fixing the alphabet, which consists only of \isa{a}'s |
27 and~\isa{b}'s:% |
29 and~\isa{b}'s:% |
28 \end{isamarkuptext}% |
30 \end{isamarkuptext}% |
29 \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b% |
31 \isamarkuptrue% |
|
32 \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b\isamarkupfalse% |
|
33 % |
30 \begin{isamarkuptext}% |
34 \begin{isamarkuptext}% |
31 \noindent |
35 \noindent |
32 For convenience we include the following easy lemmas as simplification rules:% |
36 For convenience we include the following easy lemmas as simplification rules:% |
33 \end{isamarkuptext}% |
37 \end{isamarkuptext}% |
|
38 \isamarkuptrue% |
34 \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 |
39 \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 |
35 \isacommand{by}\ {\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharcomma}\ auto{\isacharparenright}% |
40 \isamarkupfalse% |
|
41 \isacommand{by}\ {\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% |
|
42 % |
36 \begin{isamarkuptext}% |
43 \begin{isamarkuptext}% |
37 \noindent |
44 \noindent |
38 Words over this alphabet are of type \isa{alfa\ list}, and |
45 Words over this alphabet are of type \isa{alfa\ list}, and |
39 the three nonterminals are declared as sets of such words:% |
46 the three nonterminals are declared as sets of such words:% |
40 \end{isamarkuptext}% |
47 \end{isamarkuptext}% |
|
48 \isamarkuptrue% |
41 \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline |
49 \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline |
42 \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline |
50 \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline |
43 \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}% |
51 \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isamarkupfalse% |
|
52 % |
44 \begin{isamarkuptext}% |
53 \begin{isamarkuptext}% |
45 \noindent |
54 \noindent |
46 The productions above are recast as a \emph{mutual} inductive |
55 The productions above are recast as a \emph{mutual} inductive |
47 definition\index{inductive definition!simultaneous} |
56 definition\index{inductive definition!simultaneous} |
48 of \isa{S}, \isa{A} and~\isa{B}:% |
57 of \isa{S}, \isa{A} and~\isa{B}:% |
49 \end{isamarkuptext}% |
58 \end{isamarkuptext}% |
|
59 \isamarkuptrue% |
50 \isacommand{inductive}\ S\ A\ B\isanewline |
60 \isacommand{inductive}\ S\ A\ B\isanewline |
51 \isakeyword{intros}\isanewline |
61 \isakeyword{intros}\isanewline |
52 \ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline |
62 \ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequote}\isanewline |
53 \ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline |
63 \ \ {\isachardoublequote}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline |
54 \ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline |
64 \ \ {\isachardoublequote}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequote}\isanewline |
55 \isanewline |
65 \isanewline |
56 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline |
66 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequote}\isanewline |
57 \ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline |
67 \ \ {\isachardoublequote}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequote}\isanewline |
58 \isanewline |
68 \isanewline |
59 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline |
69 \ \ {\isachardoublequote}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequote}\isanewline |
60 \ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}% |
70 \ \ {\isachardoublequote}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequote}\isamarkupfalse% |
|
71 % |
61 \begin{isamarkuptext}% |
72 \begin{isamarkuptext}% |
62 \noindent |
73 \noindent |
63 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 mutual |
74 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 mutual |
64 induction, so is the proof: we show at the same time that all words in |
75 induction, so is the proof: we show at the same time that all words in |
65 \isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.% |
76 \isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.% |
66 \end{isamarkuptext}% |
77 \end{isamarkuptext}% |
|
78 \isamarkuptrue% |
67 \isacommand{lemma}\ correctness{\isacharcolon}\isanewline |
79 \isacommand{lemma}\ correctness{\isacharcolon}\isanewline |
68 \ \ {\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 |
80 \ \ {\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 |
69 \ \ \ {\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 |
81 \ \ \ {\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 |
70 \ \ \ {\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}% |
82 \ \ \ {\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}\isamarkupfalse% |
|
83 % |
71 \begin{isamarkuptxt}% |
84 \begin{isamarkuptxt}% |
72 \noindent |
85 \noindent |
73 These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x} |
86 These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x} |
74 holds. Remember that on lists \isa{size} and \isa{length} are synonymous. |
87 holds. Remember that on lists \isa{size} and \isa{length} are synonymous. |
75 |
88 |
76 The proof itself is by rule induction and afterwards automatic:% |
89 The proof itself is by rule induction and afterwards automatic:% |
77 \end{isamarkuptxt}% |
90 \end{isamarkuptxt}% |
78 \isacommand{by}\ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}% |
91 \isamarkuptrue% |
|
92 \isacommand{by}\ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% |
|
93 % |
79 \begin{isamarkuptext}% |
94 \begin{isamarkuptext}% |
80 \noindent |
95 \noindent |
81 This may seem surprising at first, and is indeed an indication of the power |
96 This may seem surprising at first, and is indeed an indication of the power |
82 of inductive definitions. But it is also quite straightforward. For example, |
97 of inductive definitions. But it is also quite straightforward. For example, |
83 consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$ |
98 consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$ |
108 move to the right. At this point we also start generalizing from \isa{a}'s |
123 move to the right. At this point we also start generalizing from \isa{a}'s |
109 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have |
124 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have |
110 to prove the desired lemma twice, once as stated above and once with the |
125 to prove the desired lemma twice, once as stated above and once with the |
111 roles of \isa{a}'s and \isa{b}'s interchanged.% |
126 roles of \isa{a}'s and \isa{b}'s interchanged.% |
112 \end{isamarkuptext}% |
127 \end{isamarkuptext}% |
|
128 \isamarkuptrue% |
113 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline |
129 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline |
114 \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
130 \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
115 \ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ Numeral{\isadigit{1}}{\isachardoublequote}% |
131 \ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ Numeral{\isadigit{1}}{\isachardoublequote}\isamarkupfalse% |
|
132 % |
116 \begin{isamarkuptxt}% |
133 \begin{isamarkuptxt}% |
117 \noindent |
134 \noindent |
118 The lemma is a bit hard to read because of the coercion function |
135 The lemma is a bit hard to read because of the coercion function |
119 \isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns |
136 \isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns |
120 a natural number, but subtraction on type~\isa{nat} will do the wrong thing. |
137 a natural number, but subtraction on type~\isa{nat} will do the wrong thing. |
124 |
141 |
125 The proof is by induction on \isa{w}, with a trivial base case, and a not |
142 The proof is by induction on \isa{w}, with a trivial base case, and a not |
126 so trivial induction step. Since it is essentially just arithmetic, we do not |
143 so trivial induction step. Since it is essentially just arithmetic, we do not |
127 discuss it.% |
144 discuss it.% |
128 \end{isamarkuptxt}% |
145 \end{isamarkuptxt}% |
|
146 \isamarkuptrue% |
129 \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline |
147 \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline |
130 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
148 \ \isamarkupfalse% |
131 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}% |
149 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
150 \isamarkupfalse% |
|
151 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}\isamarkupfalse% |
|
152 % |
132 \begin{isamarkuptext}% |
153 \begin{isamarkuptext}% |
133 Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:% |
154 Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:% |
134 \end{isamarkuptext}% |
155 \end{isamarkuptext}% |
|
156 \isamarkuptrue% |
135 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline |
157 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline |
136 \ {\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 |
158 \ {\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 |
137 \ \ {\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}% |
159 \ \ {\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}\isamarkupfalse% |
|
160 % |
138 \begin{isamarkuptxt}% |
161 \begin{isamarkuptxt}% |
139 \noindent |
162 \noindent |
140 This is proved by \isa{force} with the help of the intermediate value theorem, |
163 This is proved by \isa{force} with the help of the intermediate value theorem, |
141 instantiated appropriately and with its first premise disposed of by lemma |
164 instantiated appropriately and with its first premise disposed of by lemma |
142 \isa{step{\isadigit{1}}}:% |
165 \isa{step{\isadigit{1}}}:% |
143 \end{isamarkuptxt}% |
166 \end{isamarkuptxt}% |
|
167 \isamarkuptrue% |
144 \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}Numeral{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline |
168 \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}Numeral{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline |
145 \isacommand{by}\ force% |
169 \isamarkupfalse% |
|
170 \isacommand{by}\ force\isamarkupfalse% |
|
171 % |
146 \begin{isamarkuptext}% |
172 \begin{isamarkuptext}% |
147 \noindent |
173 \noindent |
148 |
174 |
149 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}. |
175 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}. |
150 An easy lemma deals with the suffix \isa{drop\ i\ w}:% |
176 An easy lemma deals with the suffix \isa{drop\ i\ w}:% |
151 \end{isamarkuptext}% |
177 \end{isamarkuptext}% |
|
178 \isamarkuptrue% |
152 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline |
179 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline |
153 \ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline |
180 \ \ {\isachardoublequote}{\isasymlbrakk}size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\isanewline |
154 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline |
181 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w\ {\isacharat}\ drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline |
155 \ \ \ \ 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 |
182 \ \ \ \ 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 |
156 \ \ \ {\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 |
183 \ \ \ {\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 |
157 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}% |
184 \isamarkupfalse% |
|
185 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isamarkupfalse% |
|
186 % |
158 \begin{isamarkuptext}% |
187 \begin{isamarkuptext}% |
159 \noindent |
188 \noindent |
160 In the proof we have disabled the normally useful lemma |
189 In the proof we have disabled the normally useful lemma |
161 \begin{isabelle} |
190 \begin{isabelle} |
162 \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs} |
191 \isa{take\ n\ xs\ {\isacharat}\ drop\ n\ xs\ {\isacharequal}\ xs} |
168 \end{isabelle} |
197 \end{isabelle} |
169 |
198 |
170 To dispose of trivial cases automatically, the rules of the inductive |
199 To dispose of trivial cases automatically, the rules of the inductive |
171 definition are declared simplification rules:% |
200 definition are declared simplification rules:% |
172 \end{isamarkuptext}% |
201 \end{isamarkuptext}% |
173 \isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}% |
202 \isamarkuptrue% |
|
203 \isacommand{declare}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharbrackleft}simp{\isacharbrackright}\isamarkupfalse% |
|
204 % |
174 \begin{isamarkuptext}% |
205 \begin{isamarkuptext}% |
175 \noindent |
206 \noindent |
176 This could have been done earlier but was not necessary so far. |
207 This could have been done earlier but was not necessary so far. |
177 |
208 |
178 The completeness theorem tells us that if a word has the same number of |
209 The completeness theorem tells us that if a word has the same number of |
179 \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly |
210 \isa{a}'s and \isa{b}'s, then it is in \isa{S}, and similarly |
180 for \isa{A} and \isa{B}:% |
211 for \isa{A} and \isa{B}:% |
181 \end{isamarkuptext}% |
212 \end{isamarkuptext}% |
|
213 \isamarkuptrue% |
182 \isacommand{theorem}\ completeness{\isacharcolon}\isanewline |
214 \isacommand{theorem}\ completeness{\isacharcolon}\isanewline |
183 \ \ {\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 |
215 \ \ {\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 |
184 \ \ \ {\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 |
216 \ \ \ {\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 |
185 \ \ \ {\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}% |
217 \ \ \ {\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}\isamarkupfalse% |
|
218 % |
186 \begin{isamarkuptxt}% |
219 \begin{isamarkuptxt}% |
187 \noindent |
220 \noindent |
188 The proof is by induction on \isa{w}. Structural induction would fail here |
221 The proof is by induction on \isa{w}. Structural induction would fail here |
189 because, as we can see from the grammar, we need to make bigger steps than |
222 because, as we can see from the grammar, we need to make bigger steps than |
190 merely appending a single letter at the front. Hence we induct on the length |
223 merely appending a single letter at the front. Hence we induct on the length |
191 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:% |
224 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:% |
192 \end{isamarkuptxt}% |
225 \end{isamarkuptxt}% |
193 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}% |
226 \isamarkuptrue% |
|
227 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse% |
|
228 \isamarkupfalse% |
|
229 % |
194 \begin{isamarkuptxt}% |
230 \begin{isamarkuptxt}% |
195 \noindent |
231 \noindent |
196 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction |
232 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction |
197 rule to use. For details see \S\ref{sec:complete-ind} below. |
233 rule to use. For details see \S\ref{sec:complete-ind} below. |
198 In this case the result is that we may assume the lemma already |
234 In this case the result is that we may assume the lemma already |
199 holds for all words shorter than \isa{w}. |
235 holds for all words shorter than \isa{w}. |
200 |
236 |
201 The proof continues with a case distinction on \isa{w}, |
237 The proof continues with a case distinction on \isa{w}, |
202 on whether \isa{w} is empty or not.% |
238 on whether \isa{w} is empty or not.% |
203 \end{isamarkuptxt}% |
239 \end{isamarkuptxt}% |
|
240 \isamarkuptrue% |
204 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline |
241 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline |
205 \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}% |
242 \ \isamarkupfalse% |
|
243 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% |
|
244 \isamarkupfalse% |
|
245 % |
206 \begin{isamarkuptxt}% |
246 \begin{isamarkuptxt}% |
207 \noindent |
247 \noindent |
208 Simplification disposes of the base case and leaves only a conjunction |
248 Simplification disposes of the base case and leaves only a conjunction |
209 of two step cases to be proved: |
249 of two step cases to be proved: |
210 if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}% |
250 if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}% |
214 We only consider the first case in detail. |
254 We only consider the first case in detail. |
215 |
255 |
216 After breaking the conjunction up into two cases, we can apply |
256 After breaking the conjunction up into two cases, we can apply |
217 \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.% |
257 \isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.% |
218 \end{isamarkuptxt}% |
258 \end{isamarkuptxt}% |
|
259 \isamarkuptrue% |
219 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline |
260 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline |
220 \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
261 \ \isamarkupfalse% |
221 \ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
262 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
222 \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}% |
263 \ \isamarkupfalse% |
|
264 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
265 \ \isamarkupfalse% |
|
266 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isamarkupfalse% |
|
267 % |
223 \begin{isamarkuptxt}% |
268 \begin{isamarkuptxt}% |
224 \noindent |
269 \noindent |
225 This yields an index \isa{i\ {\isasymle}\ length\ v} such that |
270 This yields an index \isa{i\ {\isasymle}\ length\ v} such that |
226 \begin{isabelle}% |
271 \begin{isabelle}% |
227 \ \ \ \ \ 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}}% |
272 \ \ \ \ \ 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}}% |
229 With the help of \isa{part{\isadigit{2}}} it follows that |
274 With the help of \isa{part{\isadigit{2}}} it follows that |
230 \begin{isabelle}% |
275 \begin{isabelle}% |
231 \ \ \ \ \ 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}}% |
276 \ \ \ \ \ 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}}% |
232 \end{isabelle}% |
277 \end{isabelle}% |
233 \end{isamarkuptxt}% |
278 \end{isamarkuptxt}% |
234 \ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
279 \ \isamarkuptrue% |
235 \ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}% |
280 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
281 \ \ \isamarkupfalse% |
|
282 \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isamarkupfalse% |
|
283 % |
236 \begin{isamarkuptxt}% |
284 \begin{isamarkuptxt}% |
237 \noindent |
285 \noindent |
238 Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A} |
286 Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A} |
239 into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},% |
287 into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},% |
240 \end{isamarkuptxt}% |
288 \end{isamarkuptxt}% |
241 \ \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}% |
289 \ \isamarkuptrue% |
|
290 \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}\isamarkupfalse% |
|
291 % |
242 \begin{isamarkuptxt}% |
292 \begin{isamarkuptxt}% |
243 \noindent |
293 \noindent |
244 (the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the |
294 (the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the |
245 theorems \isa{subst} and \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}) |
295 theorems \isa{subst} and \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}) |
246 after which the appropriate rule of the grammar reduces the goal |
296 after which the appropriate rule of the grammar reduces the goal |
247 to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:% |
297 to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:% |
248 \end{isamarkuptxt}% |
298 \end{isamarkuptxt}% |
249 \ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}% |
299 \ \isamarkuptrue% |
|
300 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isamarkupfalse% |
|
301 % |
250 \begin{isamarkuptxt}% |
302 \begin{isamarkuptxt}% |
251 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:% |
303 Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:% |
252 \end{isamarkuptxt}% |
304 \end{isamarkuptxt}% |
253 \ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
305 \ \ \isamarkuptrue% |
254 \ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}% |
306 \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
|
307 \ \isamarkupfalse% |
|
308 \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse% |
|
309 % |
255 \begin{isamarkuptxt}% |
310 \begin{isamarkuptxt}% |
256 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:% |
311 The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:% |
257 \end{isamarkuptxt}% |
312 \end{isamarkuptxt}% |
|
313 \isamarkuptrue% |
258 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
314 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
315 \isamarkupfalse% |
259 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
316 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
317 \isamarkupfalse% |
260 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
318 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
319 \isamarkupfalse% |
261 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
320 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
262 \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline |
321 \ \isamarkupfalse% |
|
322 \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline |
|
323 \isamarkupfalse% |
263 \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 |
324 \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 |
|
325 \isamarkupfalse% |
264 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline |
326 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline |
265 \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
327 \ \isamarkupfalse% |
266 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}% |
328 \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
|
329 \isamarkupfalse% |
|
330 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse% |
|
331 % |
267 \begin{isamarkuptext}% |
332 \begin{isamarkuptext}% |
268 We conclude this section with a comparison of our proof with |
333 We conclude this section with a comparison of our proof with |
269 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.} |
334 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.} |
270 \cite[p.\ts81]{HopcroftUllman}. |
335 \cite[p.\ts81]{HopcroftUllman}. |
271 For a start, the textbook |
336 For a start, the textbook |