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