doc-src/TutorialI/Inductive/AB.thy
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10520 bb9dfcc87951 child 10884 2995639c6a09 permissions -rw-r--r--
*** empty log message ***
 nipkow@10225  1 (*<*)theory AB = Main:(*>*)  nipkow@10225  2 nipkow@10242  3 section{*Case study: A context free grammar*}  nipkow@10217  4 nipkow@10242  5 text{*\label{sec:CFG}  nipkow@10236  6 Grammars are nothing but shorthands for inductive definitions of nonterminals  nipkow@10236  7 which represent sets of strings. For example, the production  nipkow@10236  8 $A \to B c$ is short for  nipkow@10236  9 $w \in B \Longrightarrow wc \in A$  nipkow@10236  10 This section demonstrates this idea with a standard example  nipkow@10236  11 \cite[p.\ 81]{HopcroftUllman}, a grammar for generating all words with an  nipkow@10236  12 equal number of $a$'s and $b$'s:  nipkow@10236  13 \begin{eqnarray}  nipkow@10236  14 S &\to& \epsilon \mid b A \mid a B \nonumber\\  nipkow@10236  15 A &\to& a S \mid b A A \nonumber\\  nipkow@10236  16 B &\to& b S \mid a B B \nonumber  nipkow@10236  17 \end{eqnarray}  nipkow@10236  18 At the end we say a few words about the relationship of the formalization  nipkow@10236  19 and the text in the book~\cite[p.\ 81]{HopcroftUllman}.  nipkow@10236  20 paulson@10287  21 We start by fixing the alphabet, which consists only of @{term a}'s  nipkow@10236  22 and @{term b}'s:  nipkow@10236  23 *}  nipkow@10236  24 nipkow@10217  25 datatype alfa = a | b;  nipkow@10217  26 nipkow@10236  27 text{*\noindent  paulson@10287  28 For convenience we include the following easy lemmas as simplification rules:  nipkow@10236  29 *}  nipkow@10236  30 nipkow@10236  31 lemma [simp]: "(x \ a) = (x = b) \ (x \ b) = (x = a)";  nipkow@10217  32 apply(case_tac x);  nipkow@10217  33 by(auto);  nipkow@10217  34 nipkow@10236  35 text{*\noindent  nipkow@10236  36 Words over this alphabet are of type @{typ"alfa list"}, and  nipkow@10236  37 the three nonterminals are declare as sets of such words:  nipkow@10236  38 *}  nipkow@10236  39 nipkow@10217  40 consts S :: "alfa list set"  nipkow@10217  41  A :: "alfa list set"  nipkow@10217  42  B :: "alfa list set";  nipkow@10217  43 nipkow@10236  44 text{*\noindent  nipkow@10236  45 The above productions are recast as a \emph{simultaneous} inductive  nipkow@10242  46 definition\index{inductive definition!simultaneous}  nipkow@10242  47 of @{term S}, @{term A} and @{term B}:  nipkow@10236  48 *}  nipkow@10236  49 nipkow@10217  50 inductive S A B  nipkow@10217  51 intros  nipkow@10236  52  "[] \ S"  nipkow@10236  53  "w \ A \ b#w \ S"  nipkow@10236  54  "w \ B \ a#w \ S"  nipkow@10217  55 nipkow@10236  56  "w \ S \ a#w \ A"  nipkow@10236  57  "\ v\A; w\A \ \ b#v@w \ A"  nipkow@10236  58 nipkow@10236  59  "w \ S \ b#w \ B"  nipkow@10236  60  "\ v \ B; w \ B \ \ a#v@w \ B";  nipkow@10217  61 nipkow@10236  62 text{*\noindent  nipkow@10236  63 First we show that all words in @{term S} contain the same number of @{term  nipkow@10236  64 a}'s and @{term b}'s. Since the definition of @{term S} is by simultaneous  nipkow@10236  65 induction, so is this proof: we show at the same time that all words in  nipkow@10236  66 @{term A} contain one more @{term a} than @{term b} and all words in @{term  nipkow@10236  67 B} contains one more @{term b} than @{term a}.  nipkow@10236  68 *}  nipkow@10217  69 nipkow@10236  70 lemma correctness:  nipkow@10236  71  "(w \ S \ size[x\w. x=a] = size[x\w. x=b]) \  nipkow@10237  72  (w \ A \ size[x\w. x=a] = size[x\w. x=b] + 1) \  nipkow@10237  73  (w \ B \ size[x\w. x=b] = size[x\w. x=a] + 1)"  nipkow@10217  74 nipkow@10236  75 txt{*\noindent  nipkow@10236  76 These propositions are expressed with the help of the predefined @{term  nipkow@10283  77 filter} function on lists, which has the convenient syntax @{text"[x\xs. P  nipkow@10236  78 x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}  nipkow@10237  79 holds. Remember that on lists @{term size} and @{term length} are synonymous.  nipkow@10236  80 nipkow@10236  81 The proof itself is by rule induction and afterwards automatic:  nipkow@10236  82 *}  nipkow@10236  83 nipkow@10217  84 apply(rule S_A_B.induct);  nipkow@10217  85 by(auto);  nipkow@10217  86 nipkow@10236  87 text{*\noindent  nipkow@10236  88 This may seem surprising at first, and is indeed an indication of the power  nipkow@10236  89 of inductive definitions. But it is also quite straightforward. For example,  nipkow@10236  90 consider the production $A \to b A A$: if $v,w \in A$ and the elements of $A$  nipkow@10236  91 contain one more $a$ than $b$'s, then $bvw$ must again contain one more $a$  nipkow@10236  92 than $b$'s.  nipkow@10236  93 nipkow@10236  94 As usual, the correctness of syntactic descriptions is easy, but completeness  nipkow@10236  95 is hard: does @{term S} contain \emph{all} words with an equal number of  nipkow@10236  96 @{term a}'s and @{term b}'s? It turns out that this proof requires the  nipkow@10236  97 following little lemma: every string with two more @{term a}'s than @{term  nipkow@10236  98 b}'s can be cut somehwere such that each half has one more @{term a} than  nipkow@10236  99 @{term b}. This is best seen by imagining counting the difference between the  nipkow@10283  100 number of @{term a}'s and @{term b}'s starting at the left end of the  nipkow@10283  101 word. We start with 0 and end (at the right end) with 2. Since each move to the  nipkow@10236  102 right increases or decreases the difference by 1, we must have passed through  nipkow@10236  103 1 on our way from 0 to 2. Formally, we appeal to the following discrete  nipkow@10236  104 intermediate value theorem @{thm[source]nat0_intermed_int_val}  nipkow@10236  105 @{thm[display]nat0_intermed_int_val[no_vars]}  nipkow@10236  106 where @{term f} is of type @{typ"nat \ int"}, @{typ int} are the integers,  nipkow@10608  107 @{text"\.\"} is the absolute value function, and @{term"#1::int"} is the  nipkow@10420  108 integer 1 (see \S\ref{sec:numbers}).  nipkow@10217  109 nipkow@10236  110 First we show that the our specific function, the difference between the  nipkow@10236  111 numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every  nipkow@10236  112 move to the right. At this point we also start generalizing from @{term a}'s  nipkow@10236  113 and @{term b}'s to an arbitrary property @{term P}. Otherwise we would have  nipkow@10236  114 to prove the desired lemma twice, once as stated above and once with the  nipkow@10236  115 roles of @{term a}'s and @{term b}'s interchanged.  nipkow@10236  116 *}  nipkow@10236  117 nipkow@10236  118 lemma step1: "\i < size w.  nipkow@10608  119  \(int(size[x\take (i+1) w. P x])-int(size[x\take (i+1) w. \P x]))  nipkow@10608  120  - (int(size[x\take i w. P x])-int(size[x\take i w. \P x]))\ \ #1"  nipkow@10236  121 nipkow@10236  122 txt{*\noindent  nipkow@10236  123 The lemma is a bit hard to read because of the coercion function  nipkow@10608  124 @{term[source]"int :: nat \ int"}. It is required because @{term size} returns  nipkow@10236  125 a natural number, but @{text-} on @{typ nat} will do the wrong thing.  nipkow@10236  126 Function @{term take} is predefined and @{term"take i xs"} is the prefix of  nipkow@10236  127 length @{term i} of @{term xs}; below we als need @{term"drop i xs"}, which  nipkow@10236  128 is what remains after that prefix has been dropped from @{term xs}.  nipkow@10236  129 nipkow@10236  130 The proof is by induction on @{term w}, with a trivial base case, and a not  nipkow@10236  131 so trivial induction step. Since it is essentially just arithmetic, we do not  nipkow@10236  132 discuss it.  nipkow@10236  133 *}  nipkow@10236  134 nipkow@10217  135 apply(induct w);  nipkow@10217  136  apply(simp);  nipkow@10236  137 by(force simp add:zabs_def take_Cons split:nat.split if_splits);  nipkow@10217  138 nipkow@10236  139 text{*  nipkow@10236  140 Finally we come to the above mentioned lemma about cutting a word with two  nipkow@10283  141 more elements of one sort than of the other sort into two halves:  nipkow@10236  142 *}  nipkow@10217  143 nipkow@10217  144 lemma part1:  nipkow@10236  145  "size[x\w. P x] = size[x\w. \P x]+2 \  nipkow@10236  146  \i\size w. size[x\take i w. P x] = size[x\take i w. \P x]+1";  nipkow@10236  147 nipkow@10236  148 txt{*\noindent  nipkow@10608  149 This is proved by force with the help of the intermediate value theorem,  nipkow@10608  150 instantiated appropriately and with its first premise disposed of by lemma  nipkow@10608  151 @{thm[source]step1}:  nipkow@10236  152 *}  nipkow@10236  153 nipkow@10236  154 apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "#1"]);  nipkow@10608  155 by force;  nipkow@10236  156 nipkow@10236  157 text{*\noindent  nipkow@10236  158 nipkow@10236  159 Lemma @{thm[source]part1} tells us only about the prefix @{term"take i w"}.  nipkow@10236  160 The suffix @{term"drop i w"} is dealt with in the following easy lemma:  nipkow@10236  161 *}  nipkow@10236  162 nipkow@10217  163 nipkow@10217  164 lemma part2:  nipkow@10236  165  "\size[x\take i w @ drop i w. P x] =  nipkow@10236  166  size[x\take i w @ drop i w. \P x]+2;  nipkow@10236  167  size[x\take i w. P x] = size[x\take i w. \P x]+1\  nipkow@10236  168  \ size[x\drop i w. P x] = size[x\drop i w. \P x]+1";  nipkow@10217  169 by(simp del:append_take_drop_id);  nipkow@10217  170 nipkow@10236  171 text{*\noindent  nipkow@10236  172 Lemma @{thm[source]append_take_drop_id}, @{thm append_take_drop_id[no_vars]},  nipkow@10236  173 which is generally useful, needs to be disabled for once.  nipkow@10236  174 nipkow@10236  175 To dispose of trivial cases automatically, the rules of the inductive  nipkow@10236  176 definition are declared simplification rules:  nipkow@10236  177 *}  nipkow@10236  178 nipkow@10236  179 declare S_A_B.intros[simp];  nipkow@10236  180 nipkow@10236  181 text{*\noindent  nipkow@10236  182 This could have been done earlier but was not necessary so far.  nipkow@10236  183 nipkow@10236  184 The completeness theorem tells us that if a word has the same number of  nipkow@10236  185 @{term a}'s and @{term b}'s, then it is in @{term S}, and similarly and  nipkow@10236  186 simultaneously for @{term A} and @{term B}:  nipkow@10236  187 *}  nipkow@10236  188 nipkow@10236  189 theorem completeness:  nipkow@10236  190  "(size[x\w. x=a] = size[x\w. x=b] \ w \ S) \  nipkow@10237  191  (size[x\w. x=a] = size[x\w. x=b] + 1 \ w \ A) \  nipkow@10237  192  (size[x\w. x=b] = size[x\w. x=a] + 1 \ w \ B)";  nipkow@10236  193 nipkow@10236  194 txt{*\noindent  nipkow@10236  195 The proof is by induction on @{term w}. Structural induction would fail here  nipkow@10236  196 because, as we can see from the grammar, we need to make bigger steps than  nipkow@10236  197 merely appending a single letter at the front. Hence we induct on the length  nipkow@10236  198 of @{term w}, using the induction rule @{thm[source]length_induct}:  nipkow@10236  199 *}  nipkow@10217  200 nipkow@10217  201 apply(induct_tac w rule: length_induct);  nipkow@10236  202 (*<*)apply(rename_tac w)(*>*)  nipkow@10236  203 nipkow@10236  204 txt{*\noindent  nipkow@10236  205 The @{text rule} parameter tells @{text induct_tac} explicitly which induction  nipkow@10236  206 rule to use. For details see \S\ref{sec:complete-ind} below.  nipkow@10236  207 In this case the result is that we may assume the lemma already  nipkow@10236  208 holds for all words shorter than @{term w}.  nipkow@10236  209 nipkow@10236  210 The proof continues with a case distinction on @{term w},  nipkow@10236  211 i.e.\ if @{term w} is empty or not.  nipkow@10236  212 *}  nipkow@10236  213 nipkow@10236  214 apply(case_tac w);  nipkow@10236  215  apply(simp_all);  nipkow@10236  216 (*<*)apply(rename_tac x v)(*>*)  nipkow@10236  217 nipkow@10236  218 txt{*\noindent  nipkow@10236  219 Simplification disposes of the base case and leaves only two step  nipkow@10236  220 cases to be proved:  nipkow@10236  221 if @{prop"w = a#v"} and @{prop"size[x\v. x=a] = size[x\v. x=b]+2"} then  nipkow@10236  222 @{prop"b#v \ A"}, and similarly for @{prop"w = b#v"}.  nipkow@10236  223 We only consider the first case in detail.  nipkow@10236  224 nipkow@10236  225 After breaking the conjuction up into two cases, we can apply  nipkow@10236  226 @{thm[source]part1} to the assumption that @{term w} contains two more @{term  nipkow@10236  227 a}'s than @{term b}'s.  nipkow@10236  228 *}  nipkow@10236  229 nipkow@10217  230 apply(rule conjI);  nipkow@10217  231  apply(clarify);  nipkow@10236  232  apply(frule part1[of "\x. x=a", simplified]);  nipkow@10217  233  apply(erule exE);  nipkow@10217  234  apply(erule conjE);  nipkow@10236  235 nipkow@10236  236 txt{*\noindent  nipkow@10236  237 This yields an index @{prop"i \ length v"} such that  nipkow@10236  238 @{prop"length [x\take i v . x = a] = length [x\take i v . x = b] + 1"}.  nipkow@10236  239 With the help of @{thm[source]part1} it follows that  nipkow@10236  240 @{prop"length [x\drop i v . x = a] = length [x\drop i v . x = b] + 1"}.  nipkow@10236  241 *}  nipkow@10236  242 nipkow@10236  243  apply(drule part2[of "\x. x=a", simplified]);  nipkow@10217  244  apply(assumption);  nipkow@10236  245 nipkow@10236  246 txt{*\noindent  nipkow@10236  247 Now it is time to decompose @{term v} in the conclusion @{prop"b#v \ A"}  nipkow@10236  248 into @{term"take i v @ drop i v"},  nipkow@10236  249 after which the appropriate rule of the grammar reduces the goal  nipkow@10236  250 to the two subgoals @{prop"take i v \ A"} and @{prop"drop i v \ A"}:  nipkow@10236  251 *}  nipkow@10236  252 nipkow@10236  253  apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id]);  nipkow@10217  254  apply(rule S_A_B.intros);  nipkow@10236  255 nipkow@10236  256 txt{*\noindent  nipkow@10236  257 Both subgoals follow from the induction hypothesis because both @{term"take i  nipkow@10236  258 v"} and @{term"drop i v"} are shorter than @{term w}:  nipkow@10236  259 *}  nipkow@10236  260 nipkow@10236  261  apply(force simp add: min_less_iff_disj);  nipkow@10217  262  apply(force split add: nat_diff_split);  nipkow@10236  263 nipkow@10236  264 txt{*\noindent  nipkow@10236  265 Note that the variables @{term n1} and @{term t} referred to in the  nipkow@10236  266 substitution step above come from the derived theorem @{text"subst[OF  nipkow@10236  267 append_take_drop_id]"}.  nipkow@10236  268 nipkow@10236  269 The case @{prop"w = b#v"} is proved completely analogously:  nipkow@10236  270 *}  nipkow@10236  271 nipkow@10217  272 apply(clarify);  nipkow@10236  273 apply(frule part1[of "\x. x=b", simplified]);  nipkow@10217  274 apply(erule exE);  nipkow@10217  275 apply(erule conjE);  nipkow@10236  276 apply(drule part2[of "\x. x=b", simplified]);  nipkow@10217  277  apply(assumption);  nipkow@10236  278 apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id]);  nipkow@10217  279 apply(rule S_A_B.intros);  nipkow@10217  280  apply(force simp add:min_less_iff_disj);  nipkow@10217  281 by(force simp add:min_less_iff_disj split add: nat_diff_split);  nipkow@10217  282 nipkow@10236  283 text{*  nipkow@10236  284 We conclude this section with a comparison of the above proof and the one  nipkow@10236  285 in the textbook \cite[p.\ 81]{HopcroftUllman}. For a start, the texbook  nipkow@10236  286 grammar, for no good reason, excludes the empty word, which complicates  nipkow@10236  287 matters just a little bit because we now have 8 instead of our 7 productions.  nipkow@10236  288 nipkow@10236  289 More importantly, the proof itself is different: rather than separating the  nipkow@10236  290 two directions, they perform one induction on the length of a word. This  nipkow@10236  291 deprives them of the beauty of rule induction and in the easy direction  nipkow@10236  292 (correctness) their reasoning is more detailed than our @{text auto}. For the  nipkow@10236  293 hard part (completeness), they consider just one of the cases that our @{text  nipkow@10236  294 simp_all} disposes of automatically. Then they conclude the proof by saying  nipkow@10236  295 about the remaining cases: We do this in a manner similar to our method of  nipkow@10236  296 proof for part (1); this part is left to the reader''. But this is precisely  nipkow@10236  297 the part that requires the intermediate value theorem and thus is not at all  nipkow@10236  298 similar to the other cases (which are automatic in Isabelle). We conclude  nipkow@10236  299 that the authors are at least cavalier about this point and may even have  nipkow@10236  300 overlooked the slight difficulty lurking in the omitted cases. This is not  nipkow@10520  301 atypical for pen-and-paper proofs, once analysed in detail. *}  nipkow@10236  302 nipkow@10225  303 (*<*)end(*>*)