summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

3 section{*A context free grammar*}

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}.

21 We start by fixing the alpgabet, which consists only of @{term a}'s

22 and @{term b}'s:

23 *}

25 datatype alfa = a | b;

27 text{*\noindent

28 For convenience we includ the following easy lemmas as simplification rules:

29 *}

31 lemma [simp]: "(x \<noteq> a) = (x = b) \<and> (x \<noteq> b) = (x = a)";

32 apply(case_tac x);

33 by(auto);

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 *}

40 consts S :: "alfa list set"

41 A :: "alfa list set"

42 B :: "alfa list set";

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 *}

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"

55 "w \<in> S \<Longrightarrow> a#w \<in> A"

56 "\<lbrakk> v\<in>A; w\<in>A \<rbrakk> \<Longrightarrow> b#v@w \<in> A"

58 "w \<in> S \<Longrightarrow> b#w \<in> B"

59 "\<lbrakk> v \<in> B; w \<in> B \<rbrakk> \<Longrightarrow> a#v@w \<in> B";

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 *}

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)"

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.

80 The proof itself is by rule induction and afterwards automatic:

81 *}

83 apply(rule S_A_B.induct);

84 by(auto);

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.

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}).

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 *}

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";

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}.

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 *}

137 apply(induct w);

138 apply(simp);

139 by(force simp add:zabs_def take_Cons split:nat.split if_splits);

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 *}

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";

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 *}

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]);

160 text{*\noindent

161 The additional lemmas are needed to mediate between @{typ nat} and @{typ int}.

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 *}

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);

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.

179 To dispose of trivial cases automatically, the rules of the inductive

180 definition are declared simplification rules:

181 *}

183 declare S_A_B.intros[simp];

185 text{*\noindent

186 This could have been done earlier but was not necessary so far.

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 *}

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)";

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 *}

205 apply(induct_tac w rule: length_induct);

206 (*<*)apply(rename_tac w)(*>*)

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}.

214 The proof continues with a case distinction on @{term w},

215 i.e.\ if @{term w} is empty or not.

216 *}

218 apply(case_tac w);

219 apply(simp_all);

220 (*<*)apply(rename_tac x v)(*>*)

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.

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 *}

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);

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 *}

247 apply(drule part2[of "\<lambda>x. x=a", simplified]);

248 apply(assumption);

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 *}

257 apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id]);

258 apply(rule S_A_B.intros);

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 *}

265 apply(force simp add: min_less_iff_disj);

266 apply(force split add: nat_diff_split);

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]"}.

273 The case @{prop"w = b#v"} is proved completely analogously:

274 *}

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);

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.

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. *}

307 (*<*)end(*>*)