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