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(*>*)