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 \<noteq> a) = (x = b) \<and> (x \<noteq> 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
  "[] \<in> S"
nipkow@10236
    53
  "w \<in> A \<Longrightarrow> b#w \<in> S"
nipkow@10236
    54
  "w \<in> B \<Longrightarrow> a#w \<in> S"
nipkow@10217
    55
nipkow@10236
    56
  "w \<in> S        \<Longrightarrow> a#w   \<in> A"
nipkow@10236
    57
  "\<lbrakk> v\<in>A; w\<in>A \<rbrakk> \<Longrightarrow> b#v@w \<in> A"
nipkow@10236
    58
nipkow@10236
    59
  "w \<in> S            \<Longrightarrow> b#w   \<in> B"
nipkow@10236
    60
  "\<lbrakk> v \<in> B; w \<in> B \<rbrakk> \<Longrightarrow> a#v@w \<in> 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 \<in> S \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b])     \<and>
nipkow@10237
    72
   (w \<in> A \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1) \<and>
nipkow@10237
    73
   (w \<in> B \<longrightarrow> size[x\<in>w. x=b] = size[x\<in>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\<in>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 \<Rightarrow> int"}, @{typ int} are the integers,
nipkow@10608
   107
@{text"\<bar>.\<bar>"} 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: "\<forall>i < size w.
nipkow@10608
   119
  \<bar>(int(size[x\<in>take (i+1) w. P x])-int(size[x\<in>take (i+1) w. \<not>P x]))
nipkow@10608
   120
   - (int(size[x\<in>take i w. P x])-int(size[x\<in>take i w. \<not>P x]))\<bar> \<le> #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 \<Rightarrow> 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\<in>w. P x] = size[x\<in>w. \<not>P x]+2 \<Longrightarrow>
nipkow@10236
   146
  \<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>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
  "\<lbrakk>size[x\<in>take i w @ drop i w. P x] =
nipkow@10236
   166
    size[x\<in>take i w @ drop i w. \<not>P x]+2;
nipkow@10236
   167
    size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1\<rbrakk>
nipkow@10236
   168
   \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>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\<in>w. x=a] = size[x\<in>w. x=b]     \<longrightarrow> w \<in> S) \<and>
nipkow@10237
   191
   (size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
nipkow@10237
   192
   (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> 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\<in>v. x=a] = size[x\<in>v. x=b]+2"} then
nipkow@10236
   222
@{prop"b#v \<in> 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 "\<lambda>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 \<le> length v"} such that
nipkow@10236
   238
@{prop"length [x\<in>take i v . x = a] = length [x\<in>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\<in>drop i v . x = a] = length [x\<in>drop i v . x = b] + 1"}.
nipkow@10236
   241
*}
nipkow@10236
   242
nipkow@10236
   243
 apply(drule part2[of "\<lambda>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 \<in> 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 \<in> A"} and @{prop"drop i v \<in> 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 "\<lambda>x. x=b", simplified]);
nipkow@10217
   274
apply(erule exE);
nipkow@10217
   275
apply(erule conjE);
nipkow@10236
   276
apply(drule part2[of "\<lambda>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(*>*)