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