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