|
1 (* Title: HOL/Proofs/Extraction/Higman.thy |
|
2 Author: Stefan Berghofer, TU Muenchen |
|
3 Author: Monika Seisenberger, LMU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Higman's lemma *} |
|
7 |
|
8 theory Higman |
|
9 imports Main "~~/src/HOL/Library/State_Monad" Random |
|
10 begin |
|
11 |
|
12 text {* |
|
13 Formalization by Stefan Berghofer and Monika Seisenberger, |
|
14 based on Coquand and Fridlender \cite{Coquand93}. |
|
15 *} |
|
16 |
|
17 datatype letter = A | B |
|
18 |
|
19 inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool" |
|
20 where |
|
21 emb0 [Pure.intro]: "emb [] bs" |
|
22 | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)" |
|
23 | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)" |
|
24 |
|
25 inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool" |
|
26 for v :: "letter list" |
|
27 where |
|
28 L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)" |
|
29 | L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)" |
|
30 |
|
31 inductive good :: "letter list list \<Rightarrow> bool" |
|
32 where |
|
33 good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)" |
|
34 | good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)" |
|
35 |
|
36 inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool" |
|
37 for a :: letter |
|
38 where |
|
39 R0 [Pure.intro]: "R a [] []" |
|
40 | R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)" |
|
41 |
|
42 inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool" |
|
43 for a :: letter |
|
44 where |
|
45 T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)" |
|
46 | T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)" |
|
47 | T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)" |
|
48 |
|
49 inductive bar :: "letter list list \<Rightarrow> bool" |
|
50 where |
|
51 bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws" |
|
52 | bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws" |
|
53 |
|
54 theorem prop1: "bar ([] # ws)" by iprover |
|
55 |
|
56 theorem lemma1: "L as ws \<Longrightarrow> L (a # as) ws" |
|
57 by (erule L.induct, iprover+) |
|
58 |
|
59 lemma lemma2': "R a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws" |
|
60 apply (induct set: R) |
|
61 apply (erule L.cases) |
|
62 apply simp+ |
|
63 apply (erule L.cases) |
|
64 apply simp_all |
|
65 apply (rule L0) |
|
66 apply (erule emb2) |
|
67 apply (erule L1) |
|
68 done |
|
69 |
|
70 lemma lemma2: "R a vs ws \<Longrightarrow> good vs \<Longrightarrow> good ws" |
|
71 apply (induct set: R) |
|
72 apply iprover |
|
73 apply (erule good.cases) |
|
74 apply simp_all |
|
75 apply (rule good0) |
|
76 apply (erule lemma2') |
|
77 apply assumption |
|
78 apply (erule good1) |
|
79 done |
|
80 |
|
81 lemma lemma3': "T a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws" |
|
82 apply (induct set: T) |
|
83 apply (erule L.cases) |
|
84 apply simp_all |
|
85 apply (rule L0) |
|
86 apply (erule emb2) |
|
87 apply (rule L1) |
|
88 apply (erule lemma1) |
|
89 apply (erule L.cases) |
|
90 apply simp_all |
|
91 apply iprover+ |
|
92 done |
|
93 |
|
94 lemma lemma3: "T a ws zs \<Longrightarrow> good ws \<Longrightarrow> good zs" |
|
95 apply (induct set: T) |
|
96 apply (erule good.cases) |
|
97 apply simp_all |
|
98 apply (rule good0) |
|
99 apply (erule lemma1) |
|
100 apply (erule good1) |
|
101 apply (erule good.cases) |
|
102 apply simp_all |
|
103 apply (rule good0) |
|
104 apply (erule lemma3') |
|
105 apply iprover+ |
|
106 done |
|
107 |
|
108 lemma lemma4: "R a ws zs \<Longrightarrow> ws \<noteq> [] \<Longrightarrow> T a ws zs" |
|
109 apply (induct set: R) |
|
110 apply iprover |
|
111 apply (case_tac vs) |
|
112 apply (erule R.cases) |
|
113 apply simp |
|
114 apply (case_tac a) |
|
115 apply (rule_tac b=B in T0) |
|
116 apply simp |
|
117 apply (rule R0) |
|
118 apply (rule_tac b=A in T0) |
|
119 apply simp |
|
120 apply (rule R0) |
|
121 apply simp |
|
122 apply (rule T1) |
|
123 apply simp |
|
124 done |
|
125 |
|
126 lemma letter_neq: "(a::letter) \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b" |
|
127 apply (case_tac a) |
|
128 apply (case_tac b) |
|
129 apply (case_tac c, simp, simp) |
|
130 apply (case_tac c, simp, simp) |
|
131 apply (case_tac b) |
|
132 apply (case_tac c, simp, simp) |
|
133 apply (case_tac c, simp, simp) |
|
134 done |
|
135 |
|
136 lemma letter_eq_dec: "(a::letter) = b \<or> a \<noteq> b" |
|
137 apply (case_tac a) |
|
138 apply (case_tac b) |
|
139 apply simp |
|
140 apply simp |
|
141 apply (case_tac b) |
|
142 apply simp |
|
143 apply simp |
|
144 done |
|
145 |
|
146 theorem prop2: |
|
147 assumes ab: "a \<noteq> b" and bar: "bar xs" |
|
148 shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar |
|
149 proof induct |
|
150 fix xs zs assume "T a xs zs" and "good xs" |
|
151 hence "good zs" by (rule lemma3) |
|
152 then show "bar zs" by (rule bar1) |
|
153 next |
|
154 fix xs ys |
|
155 assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" |
|
156 assume "bar ys" |
|
157 thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" |
|
158 proof induct |
|
159 fix ys zs assume "T b ys zs" and "good ys" |
|
160 then have "good zs" by (rule lemma3) |
|
161 then show "bar zs" by (rule bar1) |
|
162 next |
|
163 fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs" |
|
164 and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs" |
|
165 show "bar zs" |
|
166 proof (rule bar2) |
|
167 fix w |
|
168 show "bar (w # zs)" |
|
169 proof (cases w) |
|
170 case Nil |
|
171 thus ?thesis by simp (rule prop1) |
|
172 next |
|
173 case (Cons c cs) |
|
174 from letter_eq_dec show ?thesis |
|
175 proof |
|
176 assume ca: "c = a" |
|
177 from ab have "bar ((a # cs) # zs)" by (iprover intro: I ys Ta Tb) |
|
178 thus ?thesis by (simp add: Cons ca) |
|
179 next |
|
180 assume "c \<noteq> a" |
|
181 with ab have cb: "c = b" by (rule letter_neq) |
|
182 from ab have "bar ((b # cs) # zs)" by (iprover intro: I' Ta Tb) |
|
183 thus ?thesis by (simp add: Cons cb) |
|
184 qed |
|
185 qed |
|
186 qed |
|
187 qed |
|
188 qed |
|
189 |
|
190 theorem prop3: |
|
191 assumes bar: "bar xs" |
|
192 shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar |
|
193 proof induct |
|
194 fix xs zs |
|
195 assume "R a xs zs" and "good xs" |
|
196 then have "good zs" by (rule lemma2) |
|
197 then show "bar zs" by (rule bar1) |
|
198 next |
|
199 fix xs zs |
|
200 assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs" |
|
201 and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs" |
|
202 show "bar zs" |
|
203 proof (rule bar2) |
|
204 fix w |
|
205 show "bar (w # zs)" |
|
206 proof (induct w) |
|
207 case Nil |
|
208 show ?case by (rule prop1) |
|
209 next |
|
210 case (Cons c cs) |
|
211 from letter_eq_dec show ?case |
|
212 proof |
|
213 assume "c = a" |
|
214 thus ?thesis by (iprover intro: I [simplified] R) |
|
215 next |
|
216 from R xsn have T: "T a xs zs" by (rule lemma4) |
|
217 assume "c \<noteq> a" |
|
218 thus ?thesis by (iprover intro: prop2 Cons xsb xsn R T) |
|
219 qed |
|
220 qed |
|
221 qed |
|
222 qed |
|
223 |
|
224 theorem higman: "bar []" |
|
225 proof (rule bar2) |
|
226 fix w |
|
227 show "bar [w]" |
|
228 proof (induct w) |
|
229 show "bar [[]]" by (rule prop1) |
|
230 next |
|
231 fix c cs assume "bar [cs]" |
|
232 thus "bar [c # cs]" by (rule prop3) (simp, iprover) |
|
233 qed |
|
234 qed |
|
235 |
|
236 primrec |
|
237 is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool" |
|
238 where |
|
239 "is_prefix [] f = True" |
|
240 | "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)" |
|
241 |
|
242 theorem L_idx: |
|
243 assumes L: "L w ws" |
|
244 shows "is_prefix ws f \<Longrightarrow> \<exists>i. emb (f i) w \<and> i < length ws" using L |
|
245 proof induct |
|
246 case (L0 v ws) |
|
247 hence "emb (f (length ws)) w" by simp |
|
248 moreover have "length ws < length (v # ws)" by simp |
|
249 ultimately show ?case by iprover |
|
250 next |
|
251 case (L1 ws v) |
|
252 then obtain i where emb: "emb (f i) w" and "i < length ws" |
|
253 by simp iprover |
|
254 hence "i < length (v # ws)" by simp |
|
255 with emb show ?case by iprover |
|
256 qed |
|
257 |
|
258 theorem good_idx: |
|
259 assumes good: "good ws" |
|
260 shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using good |
|
261 proof induct |
|
262 case (good0 w ws) |
|
263 hence "w = f (length ws)" and "is_prefix ws f" by simp_all |
|
264 with good0 show ?case by (iprover dest: L_idx) |
|
265 next |
|
266 case (good1 ws w) |
|
267 thus ?case by simp |
|
268 qed |
|
269 |
|
270 theorem bar_idx: |
|
271 assumes bar: "bar ws" |
|
272 shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using bar |
|
273 proof induct |
|
274 case (bar1 ws) |
|
275 thus ?case by (rule good_idx) |
|
276 next |
|
277 case (bar2 ws) |
|
278 hence "is_prefix (f (length ws) # ws) f" by simp |
|
279 thus ?case by (rule bar2) |
|
280 qed |
|
281 |
|
282 text {* |
|
283 Strong version: yields indices of words that can be embedded into each other. |
|
284 *} |
|
285 |
|
286 theorem higman_idx: "\<exists>(i::nat) j. emb (f i) (f j) \<and> i < j" |
|
287 proof (rule bar_idx) |
|
288 show "bar []" by (rule higman) |
|
289 show "is_prefix [] f" by simp |
|
290 qed |
|
291 |
|
292 text {* |
|
293 Weak version: only yield sequence containing words |
|
294 that can be embedded into each other. |
|
295 *} |
|
296 |
|
297 theorem good_prefix_lemma: |
|
298 assumes bar: "bar ws" |
|
299 shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> good vs" using bar |
|
300 proof induct |
|
301 case bar1 |
|
302 thus ?case by iprover |
|
303 next |
|
304 case (bar2 ws) |
|
305 from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp |
|
306 thus ?case by (iprover intro: bar2) |
|
307 qed |
|
308 |
|
309 theorem good_prefix: "\<exists>vs. is_prefix vs f \<and> good vs" |
|
310 using higman |
|
311 by (rule good_prefix_lemma) simp+ |
|
312 |
|
313 |
|
314 end |