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