100/ramsey.ml

   1 (* ======================================================================== *)
   2 (* Infinite Ramsey's theorem.                                               *)
   3 (*                                                                          *)
   4 (* Port to HOL Light of a HOL88 proof done on 9th May 1994                  *)
   5 (* ======================================================================== *)
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* HOL88 compatibility.                                                      *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let is_neg_imp tm =
  12   is_neg tm or is_imp tm;;
  13
  14 let dest_neg_imp tm =
  15   try dest_imp tm with Failure _ ->
  16   try (dest_neg tm,mk_const("F",[]))
  17   with Failure _ -> failwith "dest_neg_imp";;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* These get overwritten by the subgoal stuff.                               *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 let PROVE = prove;;
  24
  25 let prove_thm((s:string),g,t) = prove(g,t);;
  26
  27 (* ------------------------------------------------------------------------- *)
  28 (* The quantifier movement conversions.                                      *)
  29 (* ------------------------------------------------------------------------- *)
  30
  31 let (CONV_OF_RCONV: conv -> conv) =
  32   let rec get_bv tm =
  33     if is_abs tm then bndvar tm
  34     else if is_comb tm then try get_bv (rand tm) with Failure _ -> get_bv (rator tm)
  35     else failwith "" in
  36   fun conv tm ->
  37   let v = get_bv tm in
  38   let th1 = conv tm in
  39   let th2 = ONCE_DEPTH_CONV (GEN_ALPHA_CONV v) (rhs(concl th1)) in
  40   TRANS th1 th2;;
  41
  42 let (CONV_OF_THM: thm -> conv) =
  43   CONV_OF_RCONV o REWR_CONV;;
  44
  45 let (X_FUN_EQ_CONV:term->conv) =
  46   fun v -> (REWR_CONV FUN_EQ_THM) THENC GEN_ALPHA_CONV v;;
  47
  48 let (FUN_EQ_CONV:conv) =
  49   fun tm ->
  50     let vars = frees tm in
  51     let op,[ty1;ty2] = dest_type(type_of (lhs tm)) in
  52     if op = "fun"
  53        then let varnm =
  54                 if (is_vartype ty1) then "x" else
  55                    hd(explode(fst(dest_type ty1))) in
  56             let x = variant vars (mk_var(varnm,ty1)) in
  57             X_FUN_EQ_CONV x tm
  58        else failwith "FUN_EQ_CONV";;
  59
  60 let (SINGLE_DEPTH_CONV:conv->conv) =
  61   let rec SINGLE_DEPTH_CONV conv tm =
  62     try conv tm with Failure _ ->
  63     (SUB_CONV (SINGLE_DEPTH_CONV conv) THENC (TRY_CONV conv)) tm in
  64   SINGLE_DEPTH_CONV;;
  65
  66 let (SKOLEM_CONV:conv) =
  67   SINGLE_DEPTH_CONV (REWR_CONV SKOLEM_THM);;
  68
  69 let (X_SKOLEM_CONV:term->conv) =
  70   fun v -> SKOLEM_CONV THENC GEN_ALPHA_CONV v;;
  71
  72 let EXISTS_UNIQUE_CONV tm =
  73   let v = bndvar(rand tm) in
  74   let th1 = REWR_CONV EXISTS_UNIQUE_THM tm in
  75   let tm1 = rhs(concl th1) in
  76   let vars = frees tm1 in
  77   let v = variant vars v in
  78   let v' = variant (v::vars) v in
  79   let th2 =
  80    (LAND_CONV(GEN_ALPHA_CONV v) THENC
  81     RAND_CONV(BINDER_CONV(GEN_ALPHA_CONV v') THENC
  82               GEN_ALPHA_CONV v)) tm1 in
  83   TRANS th1 th2;;
  84
  85 let NOT_FORALL_CONV = CONV_OF_THM NOT_FORALL_THM;;
  86
  87 let NOT_EXISTS_CONV = CONV_OF_THM NOT_EXISTS_THM;;
  88
  89 let RIGHT_IMP_EXISTS_CONV = CONV_OF_THM RIGHT_IMP_EXISTS_THM;;
  90
  91 let FORALL_IMP_CONV = CONV_OF_RCONV
  92   (REWR_CONV TRIV_FORALL_IMP_THM ORELSEC
  93    REWR_CONV RIGHT_FORALL_IMP_THM ORELSEC
  94    REWR_CONV LEFT_FORALL_IMP_THM);;
  95
  96 let EXISTS_AND_CONV = CONV_OF_RCONV
  97   (REWR_CONV TRIV_EXISTS_AND_THM ORELSEC
  98    REWR_CONV LEFT_EXISTS_AND_THM ORELSEC
  99    REWR_CONV RIGHT_EXISTS_AND_THM);;
 100
 101 let LEFT_IMP_EXISTS_CONV = CONV_OF_THM LEFT_IMP_EXISTS_THM;;
 102
 103 let LEFT_AND_EXISTS_CONV tm =
 104   let v = bndvar(rand(rand(rator tm))) in
 105   (REWR_CONV LEFT_AND_EXISTS_THM THENC TRY_CONV (GEN_ALPHA_CONV v)) tm;;
 106
 107 let RIGHT_AND_EXISTS_CONV =
 108   CONV_OF_THM RIGHT_AND_EXISTS_THM;;
 109
 110 let AND_FORALL_CONV = CONV_OF_THM AND_FORALL_THM;;
 111
 112 (* ------------------------------------------------------------------------- *)
 113 (* The slew of named tautologies.                                            *)
 114 (* ------------------------------------------------------------------------- *)
 115
 116 let AND1_THM = TAUT `!t1 t2. t1 /\ t2 ==> t1`;;
 117
 118 let AND2_THM = TAUT `!t1 t2. t1 /\ t2 ==> t2`;;
 119
 120 let AND_IMP_INTRO = TAUT `!t1 t2 t3. t1 ==> t2 ==> t3 = t1 /\ t2 ==> t3`;;
 121
 122 let AND_INTRO_THM = TAUT `!t1 t2. t1 ==> t2 ==> t1 /\ t2`;;
 123
 124 let BOOL_EQ_DISTINCT = TAUT `~(T <=> F) /\ ~(F <=> T)`;;
 125
 126 let EQ_EXPAND = TAUT `!t1 t2. (t1 <=> t2) <=> t1 /\ t2 \/ ~t1 /\ ~t2`;;
 127
 128 let EQ_IMP_THM = TAUT `!t1 t2. (t1 <=> t2) <=> (t1 ==> t2) /\ (t2 ==> t1)`;;
 129
 130 let FALSITY = TAUT `!t. F ==> t`;;
 131
 132 let F_IMP = TAUT `!t. ~t ==> t ==> F`;;
 133
 134 let IMP_DISJ_THM = TAUT `!t1 t2. t1 ==> t2 <=> ~t1 \/ t2`;;
 135
 136 let IMP_F = TAUT `!t. (t ==> F) ==> ~t`;;
 137
 138 let IMP_F_EQ_F = TAUT `!t. t ==> F <=> (t <=> F)`;;
 139
 140 let LEFT_AND_OVER_OR = TAUT
 141   `!t1 t2 t3. t1 /\ (t2 \/ t3) <=> t1 /\ t2 \/ t1 /\ t3`;;
 142
 143 let LEFT_OR_OVER_AND = TAUT
 144   `!t1 t2 t3. t1 \/ t2 /\ t3 <=> (t1 \/ t2) /\ (t1 \/ t3)`;;
 145
 146 let NOT_AND = TAUT `~(t /\ ~t)`;;
 147
 148 let NOT_F = TAUT `!t. ~t ==> (t <=> F)`;;
 149
 150 let OR_ELIM_THM = TAUT
 151   `!t t1 t2. t1 \/ t2 ==> (t1 ==> t) ==> (t2 ==> t) ==> t`;;
 152
 153 let OR_IMP_THM = TAUT `!t1 t2. (t1 <=> t2 \/ t1) <=> t2 ==> t1`;;
 154
 155 let OR_INTRO_THM1 = TAUT `!t1 t2. t1 ==> t1 \/ t2`;;
 156
 157 let OR_INTRO_THM2 = TAUT `!t1 t2. t2 ==> t1 \/ t2`;;
 158
 159 let RIGHT_AND_OVER_OR = TAUT
 160   `!t1 t2 t3. (t2 \/ t3) /\ t1 <=> t2 /\ t1 \/ t3 /\ t1`;;
 161
 162 let RIGHT_OR_OVER_AND = TAUT
 163   `!t1 t2 t3. t2 /\ t3 \/ t1 <=> (t2 \/ t1) /\ (t3 \/ t1)`;;
 164
 165 (* ------------------------------------------------------------------------- *)
 166 (* This is an overwrite -- is there any point in what I have?                *)
 167 (* ------------------------------------------------------------------------- *)
 168
 169 let is_type = can get_type_arity;;
 170
 171 (* ------------------------------------------------------------------------- *)
 172 (* I suppose this is also useful.                                            *)
 173 (* ------------------------------------------------------------------------- *)
 174
 175 let is_constant = can get_const_type;;
 176
 177 (* ------------------------------------------------------------------------- *)
 178 (* Misc.                                                                     *)
 179 (* ------------------------------------------------------------------------- *)
 180
 181 let null l = l = [];;
 182
 183 (* ------------------------------------------------------------------------- *)
 184 (* Syntax.                                                                   *)
 185 (* ------------------------------------------------------------------------- *)
 186
 187 let type_tyvars = type_vars_in_term o curry mk_var "x";;
 188
 189 let find_match u =
 190   let rec find_mt t =
 191     try term_match [] u t with Failure _ ->
 192     try find_mt(rator t) with Failure _ ->
 193     try find_mt(rand  t) with Failure _ ->
 194     try find_mt(snd(dest_abs t))
 195     with Failure _ -> failwith "find_match" in
 196   fun t -> let _,tmin,tyin = find_mt t in
 197            tmin,tyin;;
 198
 199 let rec mk_primed_var(name,ty) =
 200   if can get_const_type name then mk_primed_var(name^"'",ty)
 201   else mk_var(name,ty);;
 202
 203 let subst_occs =
 204   let rec subst_occs slist tm =
 205     let applic,noway = partition (fun (i,(t,x)) -> aconv tm x) slist in
 206     let sposs = map (fun (l,z) -> let l1,l2 = partition ((=) 1) l in
 207                                   (l1,z),(l2,z)) applic in
 208     let racts,rrest = unzip sposs in
 209     let acts = filter (fun t -> not (fst t = [])) racts in
 210     let trest = map (fun (n,t) -> (map (C (-) 1) n,t)) rrest in
 211     let urest = filter (fun t -> not (fst t = [])) trest in
 212     let tlist = urest @ noway in
 213       if acts = [] then
 214       if is_comb tm then
 215         let l,r = dest_comb tm in
 216         let l',s' = subst_occs tlist l in
 217         let r',s'' = subst_occs s' r in
 218         mk_comb(l',r'),s''
 219       else if is_abs tm then
 220         let bv,bod = dest_abs tm in
 221         let gv = genvar(type_of bv) in
 222         let nbod = vsubst[gv,bv] bod in
 223         let tm',s' = subst_occs tlist nbod in
 224         alpha bv (mk_abs(gv,tm')),s'
 225       else
 226         tm,tlist
 227     else
 228       let tm' = (fun (n,(t,x)) -> subst[t,x] tm) (hd acts) in
 229       tm',tlist in
 230   fun ilist slist tm -> fst(subst_occs (zip ilist slist) tm);;
 231
 232 (* ------------------------------------------------------------------------- *)
 233 (* Note that the all-instantiating INST and INST_TYPE are not overwritten.   *)
 234 (* ------------------------------------------------------------------------- *)
 235
 236 let INST_TY_TERM(substl,insttyl) th =
 237   let th' = INST substl (INST_TYPE insttyl th) in
 238   if hyp th' = hyp th then th'
 239   else failwith "INST_TY_TERM: Free term and/or type variables in hypotheses";;
 240
 241 (* ------------------------------------------------------------------------- *)
 242 (* Conversions stuff.                                                        *)
 243 (* ------------------------------------------------------------------------- *)
 244
 245 let RIGHT_CONV_RULE (conv:conv) th =
 246   TRANS th (conv(rhs(concl th)));;
 247
 248 (* ------------------------------------------------------------------------- *)
 249 (* Derived rules.                                                            *)
 250 (* ------------------------------------------------------------------------- *)
 251
 252 let NOT_EQ_SYM =
 253   let pth = GENL [`a:A`; `b:A`]
 254     (GEN_REWRITE_RULE I [GSYM CONTRAPOS_THM] (DISCH_ALL(SYM(ASSUME`a:A = b`))))
 255   and aty = `:A` in
 256   fun th -> try let l,r = dest_eq(dest_neg(concl th)) in
 257                 MP (SPECL [r; l] (INST_TYPE [type_of l,aty] pth)) th
 258             with Failure _ -> failwith "NOT_EQ_SYM";;
 259
 260 let NOT_MP thi th =
 261   try MP thi th with Failure _ ->
 262   try let t = dest_neg (concl thi) in
 263       MP(MP (SPEC t F_IMP) thi) th
 264   with Failure _ -> failwith "NOT_MP";;
 265
 266 let FORALL_EQ x =
 267   let mkall = AP_TERM (mk_const("!",[type_of x,mk_vartype "A"])) in
 268   fun th -> try mkall (ABS x th)
 269             with Failure _ -> failwith "FORALL_EQ";;
 270
 271 let EXISTS_EQ x =
 272   let mkex = AP_TERM (mk_const("?",[type_of x,mk_vartype "A"])) in
 273   fun th -> try mkex (ABS x th)
 274             with Failure _ -> failwith "EXISTS_EQ";;
 275
 276 let SELECT_EQ x =
 277   let mksel = AP_TERM (mk_const("@",[type_of x,mk_vartype "A"])) in
 278   fun th -> try mksel (ABS x th)
 279             with Failure _ -> failwith "SELECT_EQ";;
 280
 281 let RIGHT_BETA th =
 282   try TRANS th (BETA_CONV(rhs(concl th)))
 283   with Failure _ -> failwith "RIGHT_BETA";;
 284
 285 let rec LIST_BETA_CONV tm =
 286   try let rat,rnd = dest_comb tm in
 287       RIGHT_BETA(AP_THM(LIST_BETA_CONV rat)rnd)
 288   with Failure _ -> REFL tm;;
 289
 290 let RIGHT_LIST_BETA th = TRANS th (LIST_BETA_CONV(snd(dest_eq(concl th))));;
 291
 292 let LIST_CONJ = end_itlist CONJ ;;
 293
 294 let rec CONJ_LIST n th =
 295   try if n=1 then [th] else (CONJUNCT1 th)::(CONJ_LIST (n-1) (CONJUNCT2 th))
 296   with Failure _ -> failwith "CONJ_LIST";;
 297
 298 let rec BODY_CONJUNCTS th =
 299   if is_forall(concl th) then
 300     BODY_CONJUNCTS (SPEC_ALL th) else
 301   if is_conj (concl th) then
 302       BODY_CONJUNCTS (CONJUNCT1 th) @ BODY_CONJUNCTS (CONJUNCT2 th)
 303   else [th];;
 304
 305 let rec IMP_CANON th =
 306     let w = concl th in
 307     if is_conj w then IMP_CANON (CONJUNCT1 th) @ IMP_CANON (CONJUNCT2 th)
 308     else if is_imp w then
 309         let ante,conc = dest_neg_imp w in
 310         if is_conj ante then
 311             let a,b = dest_conj ante in
 312             IMP_CANON
 313             (DISCH a (DISCH b (NOT_MP th (CONJ (ASSUME a) (ASSUME b)))))
 314         else if is_disj ante then
 315             let a,b = dest_disj ante in
 316             IMP_CANON (DISCH a (NOT_MP th (DISJ1 (ASSUME a) b))) @
 317             IMP_CANON (DISCH b (NOT_MP th (DISJ2 a (ASSUME b))))
 318         else if is_exists ante then
 319             let x,body = dest_exists ante in
 320             let x' = variant (thm_frees th) x in
 321             let body' = subst [x',x] body in
 322             IMP_CANON
 323             (DISCH body' (NOT_MP th (EXISTS (ante, x') (ASSUME body'))))
 324         else
 325         map (DISCH ante) (IMP_CANON (UNDISCH th))
 326     else if is_forall w then
 327         IMP_CANON (SPEC_ALL th)
 328     else [th];;
 329
 330 let LIST_MP  = rev_itlist (fun x y -> MP y x);;
 331
 332 let DISJ_IMP =
 333   let pth = TAUT`!t1 t2. t1 \/ t2 ==> ~t1 ==> t2` in
 334   fun th ->
 335     try let a,b = dest_disj(concl th) in MP (SPECL [a;b] pth) th
 336     with Failure _ -> failwith "DISJ_IMP";;
 337
 338 let IMP_ELIM =
 339   let pth = TAUT`!t1 t2. (t1 ==> t2) ==> ~t1 \/ t2` in
 340   fun th ->
 341     try let a,b = dest_imp(concl th) in MP (SPECL [a;b] pth) th
 342     with Failure _ -> failwith "IMP_ELIM";;
 343
 344 let DISJ_CASES_UNION dth ath bth =
 345     DISJ_CASES dth (DISJ1 ath (concl bth)) (DISJ2 (concl ath) bth);;
 346
 347 let MK_ABS qth =
 348   try let ov = bndvar(rand(concl qth)) in
 349       let bv,rth = SPEC_VAR qth in
 350       let sth = ABS bv rth in
 351       let cnv = ALPHA_CONV ov in
 352       CONV_RULE(BINOP_CONV cnv) sth
 353   with Failure _ -> failwith "MK_ABS";;
 354
 355 let HALF_MK_ABS th =
 356   try let th1 = MK_ABS th in
 357       CONV_RULE(LAND_CONV ETA_CONV) th1
 358   with Failure _ -> failwith "HALF_MK_ABS";;
 359
 360 let MK_EXISTS qth =
 361   try let ov = bndvar(rand(concl qth)) in
 362       let bv,rth = SPEC_VAR qth in
 363       let sth = EXISTS_EQ bv rth in
 364       let cnv = GEN_ALPHA_CONV ov in
 365       CONV_RULE(BINOP_CONV cnv) sth
 366   with Failure _ -> failwith "MK_EXISTS";;
 367
 368 let LIST_MK_EXISTS l th = itlist (fun x th -> MK_EXISTS(GEN x th)) l th;;
 369
 370 let IMP_CONJ th1 th2 =
 371   let A1,C1 = dest_imp (concl th1) and A2,C2 = dest_imp (concl th2) in
 372   let a1,a2 = CONJ_PAIR (ASSUME (mk_conj(A1,A2))) in
 373       DISCH (mk_conj(A1,A2)) (CONJ (MP th1 a1) (MP th2 a2));;
 374
 375 let EXISTS_IMP x =
 376   if not (is_var x) then failwith "EXISTS_IMP: first argument not a variable"
 377   else fun th ->
 378          try let ante,cncl = dest_imp(concl th) in
 379              let th1 = EXISTS (mk_exists(x,cncl),x) (UNDISCH th) in
 380              let asm = mk_exists(x,ante) in
 381              DISCH asm (CHOOSE (x,ASSUME asm) th1)
 382          with Failure _ -> failwith "EXISTS_IMP: variable free in assumptions";;
 383
 384
 385 let CONJUNCTS_CONV (t1,t2) =
 386   let rec build_conj thl t =
 387     try let l,r = dest_conj t in
 388         CONJ (build_conj thl l) (build_conj thl r)
 389     with Failure _ -> find (fun th -> concl th = t) thl in
 390   try IMP_ANTISYM_RULE
 391      (DISCH t1 (build_conj (CONJUNCTS (ASSUME t1)) t2))
 392      (DISCH t2 (build_conj (CONJUNCTS (ASSUME t2)) t1))
 393   with Failure _ -> failwith "CONJUNCTS_CONV";;
 394
 395 let CONJ_SET_CONV l1 l2 =
 396   try CONJUNCTS_CONV (list_mk_conj l1, list_mk_conj l2)
 397   with Failure _ -> failwith "CONJ_SET_CONV";;
 398
 399 let FRONT_CONJ_CONV tml t =
 400  let rec remove x l =
 401     if hd l = x then tl l else (hd l)::(remove x (tl l)) in
 402  try CONJ_SET_CONV tml (t::(remove t tml))
 403  with Failure _ -> failwith "FRONT_CONJ_CONV";;
 404
 405 let CONJ_DISCH =
 406   let pth = TAUT`!t t1 t2. (t ==> (t1 <=> t2)) ==> (t /\ t1 <=> t /\ t2)` in
 407   fun t th ->
 408     try let t1,t2 = dest_eq(concl th) in
 409         MP (SPECL [t; t1; t2] pth) (DISCH t th)
 410     with Failure _ -> failwith "CONJ_DISCH";;
 411
 412 let rec CONJ_DISCHL l th =
 413   if l = [] then th else CONJ_DISCH (hd l) (CONJ_DISCHL (tl l) th);;
 414
 415 let rec GSPEC th =
 416   let wl,w = dest_thm th in
 417   if is_forall w then
 418       GSPEC (SPEC (genvar (type_of (fst (dest_forall w)))) th)
 419   else th;;
 420
 421 let ANTE_CONJ_CONV tm =
 422   try let (a1,a2),c = (dest_conj F_F I) (dest_imp tm) in
 423       let imp1 = MP (ASSUME tm) (CONJ (ASSUME a1) (ASSUME a2)) and
 424           imp2 = LIST_MP [CONJUNCT1 (ASSUME (mk_conj(a1,a2)));
 425                           CONJUNCT2 (ASSUME (mk_conj(a1,a2)))]
 426                          (ASSUME (mk_imp(a1,mk_imp(a2,c)))) in
 427       IMP_ANTISYM_RULE (DISCH_ALL (DISCH a1 (DISCH a2 imp1)))
 428                        (DISCH_ALL (DISCH (mk_conj(a1,a2)) imp2))
 429   with Failure _ -> failwith "ANTE_CONJ_CONV";;
 430
 431 let bool_EQ_CONV =
 432   let check = let boolty = `:bool` in check (fun tm -> type_of tm = boolty) in
 433   let clist = map (GEN `b:bool`)
 434                   (CONJUNCTS(SPEC `b:bool` EQ_CLAUSES)) in
 435   let tb = hd clist and bt = hd(tl clist) in
 436   let T = `T` and F = `F` in
 437   fun tm ->
 438     try let l,r = (I F_F check) (dest_eq tm) in
 439         if l = r then EQT_INTRO (REFL l) else
 440         if l = T then SPEC r tb else
 441         if r = T then SPEC l bt else fail()
 442     with Failure _ -> failwith "bool_EQ_CONV";;
 443
 444 let COND_CONV =
 445   let T = `T` and F = `F` and vt = genvar`:A` and vf = genvar `:A` in
 446   let gen = GENL [vt;vf] in
 447   let CT,CF = (gen F_F gen) (CONJ_PAIR (SPECL [vt;vf] COND_CLAUSES)) in
 448   fun tm ->
 449     let P,(u,v) = try dest_cond tm
 450                   with Failure _ -> failwith "COND_CONV: not a conditional" in
 451     let ty = type_of u in
 452     if (P=T) then SPEC v (SPEC u (INST_TYPE [ty,`:A`] CT)) else
 453     if (P=F) then SPEC v (SPEC u (INST_TYPE [ty,`:A`] CF)) else
 454     if (u=v) then SPEC u (SPEC P (INST_TYPE [ty,`:A`] COND_ID)) else
 455     if (aconv u v) then
 456        let cnd = AP_TERM (rator tm) (ALPHA v u) in
 457        let thm = SPEC u (SPEC P (INST_TYPE [ty,`:A`] COND_ID)) in
 458            TRANS cnd thm else
 459   failwith "COND_CONV: can't simplify conditional";;
 460
 461 let SUBST_MATCH eqth th =
 462  let tm_inst,ty_inst = find_match (lhs(concl eqth)) (concl th) in
 463  SUBS [INST tm_inst (INST_TYPE ty_inst eqth)] th;;
 464
 465 let SUBST thl pat th =
 466   let eqs,vs = unzip thl in
 467   let gvs = map (genvar o type_of) vs in
 468   let gpat = subst (zip gvs vs) pat in
 469   let ls,rs = unzip (map (dest_eq o concl) eqs) in
 470   let ths = map (ASSUME o mk_eq) (zip gvs rs) in
 471   let th1 = ASSUME gpat in
 472   let th2 = SUBS ths th1 in
 473   let th3 = itlist DISCH (map concl ths) (DISCH gpat th2) in
 474   let th4 = INST (zip ls gvs) th3 in
 475   MP (rev_itlist (C MP) eqs th4) th;;
 476
 477 (* let GSUBS = ...                                                           *)
 478 (* let SUBS_OCCS = ...                                                       *)
 479
 480 (* A poor thing but mine own. The old ones use mk_thm and the commented
 481    out functions are bogus. *)
 482
 483 let SUBST_CONV thvars template tm =
 484   let thms,vars = unzip thvars in
 485   let gvs = map (genvar o type_of) vars in
 486   let gtemplate = subst (zip gvs vars) template in
 487   SUBST (zip thms gvs) (mk_eq(template,gtemplate)) (REFL tm);;
 488
 489 (* ------------------------------------------------------------------------- *)
 490 (* Filtering rewrites.                                                       *)
 491 (* ------------------------------------------------------------------------- *)
 492
 493 let FILTER_PURE_ASM_REWRITE_RULE f thl th =
 494     PURE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
 495
 496 and FILTER_ASM_REWRITE_RULE f thl th =
 497     REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
 498
 499 and FILTER_PURE_ONCE_ASM_REWRITE_RULE f thl th =
 500     PURE_ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
 501
 502 and FILTER_ONCE_ASM_REWRITE_RULE f thl th =
 503     ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th;;
 504
 505 let (FILTER_PURE_ASM_REWRITE_TAC: (term->bool) -> thm list -> tactic) =
 506   fun f thl (asl,w) ->
 507     PURE_REWRITE_TAC (filter (f o concl) (map snd asl) @ thl) (asl,w)
 508
 509 and (FILTER_ASM_REWRITE_TAC: (term->bool) -> thm list -> tactic) =
 510   fun f thl (asl,w) ->
 511     REWRITE_TAC (filter (f o concl) (map snd asl) @ thl) (asl,w)
 512
 513 and (FILTER_PURE_ONCE_ASM_REWRITE_TAC: (term->bool) -> thm list -> tactic) =
 514   fun f thl (asl,w) ->
 515     PURE_ONCE_REWRITE_TAC (filter (f o concl) (map snd asl) @ thl) (asl,w)
 516
 517 and (FILTER_ONCE_ASM_REWRITE_TAC: (term->bool) -> thm list -> tactic) =
 518   fun f thl (asl,w) ->
 519     ONCE_REWRITE_TAC (filter (f o concl) (map snd asl) @ thl) (asl,w);;
 520
 521 (* ------------------------------------------------------------------------- *)
 522 (* Tacticals.                                                                *)
 523 (* ------------------------------------------------------------------------- *)
 524
 525 let (X_CASES_THENL: term list list -> thm_tactic list -> thm_tactic) =
 526   fun varsl ttacl ->
 527     end_itlist DISJ_CASES_THEN2
 528        (map (fun (vars,ttac) -> EVERY_TCL (map X_CHOOSE_THEN vars) ttac)
 529         (zip varsl ttacl));;
 530
 531 let (X_CASES_THEN: term list list -> thm_tactical) =
 532   fun varsl ttac ->
 533     end_itlist DISJ_CASES_THEN2
 534        (map (fun vars -> EVERY_TCL (map X_CHOOSE_THEN vars) ttac) varsl);;
 535
 536 let (CASES_THENL: thm_tactic list -> thm_tactic) =
 537   fun ttacl -> end_itlist DISJ_CASES_THEN2 (map (REPEAT_TCL CHOOSE_THEN) ttacl);;
 538
 539 (* ------------------------------------------------------------------------- *)
 540 (* Tactics.                                                                  *)
 541 (* ------------------------------------------------------------------------- *)
 542
 543 let (DISCARD_TAC: thm_tactic) =
 544   let truth = `T` in
 545   fun th (asl,w) ->
 546     if exists (aconv (concl th)) (truth::(map (concl o snd) asl))
 547     then ALL_TAC (asl,w)
 548     else failwith "DISCARD_TAC";;
 549
 550 let (CHECK_ASSUME_TAC: thm_tactic) =
 551   fun gth ->
 552     FIRST [CONTR_TAC gth;  ACCEPT_TAC gth;
 553            DISCARD_TAC gth; ASSUME_TAC gth];;
 554
 555 let (FILTER_GEN_TAC: term -> tactic) =
 556   fun tm (asl,w) ->
 557     if is_forall w & not (tm = fst(dest_forall w)) then
 558         GEN_TAC (asl,w)
 559     else failwith "FILTER_GEN_TAC";;
 560
 561 let (FILTER_DISCH_THEN: thm_tactic -> term -> tactic) =
 562   fun ttac tm (asl,w) ->
 563     if is_neg_imp w & not (free_in tm (fst(dest_neg_imp w))) then
 564       DISCH_THEN ttac (asl,w)
 565     else failwith "FILTER_DISCH_THEN";;
 566
 567 let FILTER_STRIP_THEN ttac tm =
 568   FIRST [FILTER_GEN_TAC tm; FILTER_DISCH_THEN ttac tm; CONJ_TAC];;
 569
 570 let FILTER_DISCH_TAC = FILTER_DISCH_THEN STRIP_ASSUME_TAC;;
 571
 572 let FILTER_STRIP_TAC = FILTER_STRIP_THEN STRIP_ASSUME_TAC;;
 573
 574 (* ------------------------------------------------------------------------- *)
 575 (* Conversions for quantifier movement using proforma theorems.              *)
 576 (* ------------------------------------------------------------------------- *)
 577
 578 (* let ....... *)
 579
 580 (* ------------------------------------------------------------------------- *)
 581 (* Resolution stuff.                                                         *)
 582 (* ------------------------------------------------------------------------- *)
 583
 584 let RES_CANON =
 585     let not_elim th =
 586       if is_neg (concl th) then true,(NOT_ELIM th) else (false,th) in
 587     let rec canon fl th =
 588        let w = concl th in
 589        if (is_conj w) then
 590           let (th1,th2) = CONJ_PAIR th in (canon fl th1) @ (canon fl th2) else
 591        if ((is_imp w) & not(is_neg w)) then
 592           let ante,conc = dest_neg_imp w in
 593           if (is_conj ante) then
 594              let a,b = dest_conj ante in
 595              let cth = NOT_MP th (CONJ (ASSUME a) (ASSUME b)) in
 596              let th1 = DISCH b cth and th2 = DISCH a cth in
 597                  (canon true (DISCH a th1)) @ (canon true (DISCH b th2)) else
 598           if (is_disj ante) then
 599              let a,b = dest_disj ante in
 600              let ath = DISJ1 (ASSUME a) b and bth = DISJ2 a (ASSUME b) in
 601              let th1 = DISCH a (NOT_MP th ath) and
 602                  th2 = DISCH b (NOT_MP th bth) in
 603                  (canon true th1) @ (canon true th2) else
 604           if (is_exists ante) then
 605              let v,body = dest_exists ante in
 606              let newv = variant (thm_frees th) v in
 607              let newa = subst [newv,v] body in
 608              let th1 = NOT_MP th (EXISTS (ante, newv) (ASSUME newa)) in
 609                  canon true (DISCH newa th1) else
 610              map (GEN_ALL o (DISCH ante)) (canon true (UNDISCH th)) else
 611        if (is_eq w & (type_of (rand w) = `:bool`)) then
 612           let (th1,th2) = EQ_IMP_RULE th in
 613           (if fl then [GEN_ALL th] else []) @ (canon true th1) @ (canon true th2) else
 614        if (is_forall w) then
 615            let vs,body = strip_forall w in
 616            let fvs = thm_frees th in
 617            let vfn = fun l -> variant (l @ fvs) in
 618            let nvs = itlist (fun v nv -> let v' = vfn nv v in (v'::nv)) vs [] in
 619                canon fl (SPECL nvs th) else
 620        if fl then [GEN_ALL th] else [] in
 621     fun th -> try let args = map (not_elim o SPEC_ALL) (CONJUNCTS (SPEC_ALL th)) in
 622                   let imps = flat (map (map GEN_ALL o (uncurry canon)) args) in
 623                   check (fun l -> l <> []) imps
 624               with Failure _ ->
 625                 failwith "RES_CANON: no implication is derivable from input thm.";;
 626
 627 let IMP_RES_THEN,RES_THEN =
 628   let MATCH_MP impth =
 629       let sth = SPEC_ALL impth in
 630       let matchfn = (fun (a,b,c) -> b,c) o
 631                     term_match [] (fst(dest_neg_imp(concl sth))) in
 632          fun th -> NOT_MP (INST_TY_TERM (matchfn (concl th)) sth) th in
 633   let check st l = (if l = [] then failwith st else l) in
 634   let IMP_RES_THEN ttac impth =
 635       let ths = try RES_CANON impth with Failure _ -> failwith "IMP_RES_THEN: no implication" in
 636       ASSUM_LIST
 637        (fun asl ->
 638         let l = itlist (fun th -> (@) (mapfilter (MATCH_MP th) asl)) ths [] in
 639         let res = check "IMP_RES_THEN: no resolvents " l in
 640         let tacs = check "IMP_RES_THEN: no tactics" (mapfilter ttac res) in
 641         EVERY tacs) in
 642   let RES_THEN ttac (asl,g) =
 643       let asm = map snd asl in
 644       let ths = itlist (@) (mapfilter RES_CANON asm) [] in
 645       let imps = check "RES_THEN: no implication" ths in
 646       let l = itlist (fun th -> (@) (mapfilter (MATCH_MP th) asm)) imps [] in
 647       let res = check "RES_THEN: no resolvents " l in
 648       let tacs = check "RES_THEN: no tactics" (mapfilter ttac res) in
 649           EVERY tacs (asl,g) in
 650   IMP_RES_THEN,RES_THEN;;
 651
 652 let IMP_RES_TAC th g =
 653   try IMP_RES_THEN (REPEAT_GTCL IMP_RES_THEN STRIP_ASSUME_TAC) th g
 654   with Failure _ -> ALL_TAC g;;
 655
 656 let RES_TAC g =
 657   try RES_THEN (REPEAT_GTCL IMP_RES_THEN STRIP_ASSUME_TAC) g
 658   with Failure _ -> ALL_TAC g;;
 659
 660 (* ------------------------------------------------------------------------- *)
 661 (* Stuff for handling type definitions.                                      *)
 662 (* ------------------------------------------------------------------------- *)
 663
 664 let prove_rep_fn_one_one th =
 665   try let thm = CONJUNCT1 th in
 666       let A,R = (I F_F rator) (dest_comb(lhs(snd(dest_forall(concl thm))))) in
 667       let _,[aty;rty] = dest_type (type_of R) in
 668       let a = mk_primed_var("a",aty) in let a' = variant [a] a in
 669       let a_eq_a' = mk_eq(a,a') and
 670           Ra_eq_Ra' = mk_eq(mk_comb(R,a),mk_comb (R,a')) in
 671       let th1 = AP_TERM A (ASSUME Ra_eq_Ra') in
 672       let ga1 = genvar aty and ga2 = genvar aty in
 673       let th2 = SUBST [SPEC a thm,ga1;SPEC a' thm,ga2] (mk_eq(ga1,ga2)) th1 in
 674       let th3 = DISCH a_eq_a' (AP_TERM R (ASSUME a_eq_a')) in
 675           GEN a (GEN a' (IMP_ANTISYM_RULE (DISCH Ra_eq_Ra' th2) th3))
 676   with Failure _ -> failwith "prove_rep_fn_one_one";;
 677
 678 let prove_rep_fn_onto th =
 679   try let [th1;th2] = CONJUNCTS th in
 680       let r,eq = (I F_F rhs)(dest_forall(concl th2)) in
 681       let RE,ar = dest_comb(lhs eq) and
 682           sr = (mk_eq o (fun (x,y) -> y,x) o dest_eq) eq in
 683       let a = mk_primed_var ("a",type_of ar) in
 684       let sra = mk_eq(r,mk_comb(RE,a)) in
 685       let ex = mk_exists(a,sra) in
 686       let imp1 = EXISTS (ex,ar) (SYM(ASSUME eq)) in
 687       let v = genvar (type_of r) and
 688           A = rator ar and
 689           s' = AP_TERM RE (SPEC a th1) in
 690       let th = SUBST[SYM(ASSUME sra),v](mk_eq(mk_comb(RE,mk_comb(A,v)),v))s' in
 691       let imp2 = CHOOSE (a,ASSUME ex) th in
 692       let swap = IMP_ANTISYM_RULE (DISCH eq imp1) (DISCH ex imp2) in
 693           GEN r (TRANS (SPEC r th2) swap)
 694   with Failure _ -> failwith "prove_rep_fn_onto";;
 695
 696 let prove_abs_fn_onto th =
 697   try let [th1;th2] = CONJUNCTS th in
 698       let a,(A,R) = (I F_F ((I F_F rator)o dest_comb o lhs))
 699         (dest_forall(concl th1)) in
 700       let thm1 = EQT_ELIM(TRANS (SPEC (mk_comb (R,a)) th2)
 701                                 (EQT_INTRO (AP_TERM R (SPEC a th1)))) in
 702       let thm2 = SYM(SPEC a th1) in
 703       let r,P = (I F_F (rator o lhs)) (dest_forall(concl th2)) in
 704       let ex = mk_exists(r,mk_conj(mk_eq(a,mk_comb(A,r)),mk_comb(P,r))) in
 705           GEN a (EXISTS(ex,mk_comb(R,a)) (CONJ thm2 thm1))
 706   with Failure _ -> failwith "prove_abs_fn_onto";;
 707
 708 let prove_abs_fn_one_one th =
 709   try let [th1;th2] = CONJUNCTS th in
 710       let r,P = (I F_F (rator o lhs)) (dest_forall(concl th2)) and
 711           A,R = (I F_F rator) (dest_comb(lhs(snd(dest_forall(concl th1))))) in
 712       let r' = variant [r] r in
 713       let as1 = ASSUME(mk_comb(P,r)) and as2 = ASSUME(mk_comb(P,r')) in
 714       let t1 = EQ_MP (SPEC r th2) as1 and t2 = EQ_MP (SPEC r' th2) as2 in
 715       let eq = (mk_eq(mk_comb(A,r),mk_comb(A,r'))) in
 716       let v1 = genvar(type_of r) and v2 = genvar(type_of r) in
 717       let i1 = DISCH eq
 718                (SUBST [t1,v1;t2,v2] (mk_eq(v1,v2)) (AP_TERM R (ASSUME eq))) and
 719           i2 = DISCH (mk_eq(r,r')) (AP_TERM A (ASSUME (mk_eq(r,r')))) in
 720       let thm = IMP_ANTISYM_RULE i1 i2 in
 721       let disch =  DISCH (mk_comb(P,r)) (DISCH (mk_comb(P,r')) thm) in
 722           GEN r (GEN r' disch)
 723   with Failure _ -> failwith "prove_abs_fn_one_one";;
 724
 725 (* ------------------------------------------------------------------------- *)
 726 (* AC rewriting needs to be wrapped up as a special conversion.              *)
 727 (* ------------------------------------------------------------------------- *)
 728
 729 let AC_CONV(assoc,sym) =
 730   let th1 = SPEC_ALL assoc
 731   and th2 = SPEC_ALL sym in
 732   let th3 = GEN_REWRITE_RULE (RAND_CONV o LAND_CONV) [th2] th1 in
 733   let th4 = SYM th1 in
 734   let th5 = GEN_REWRITE_RULE RAND_CONV [th4] th3 in
 735   EQT_INTRO o AC(end_itlist CONJ [th2; th4; th5]);;
 736
 737 let AC_RULE ths = EQT_ELIM o AC_CONV ths;;
 738
 739 (* ------------------------------------------------------------------------- *)
 740 (* The order of picking conditionals is different!                           *)
 741 (* ------------------------------------------------------------------------- *)
 742
 743 let (COND_CASES_TAC :tactic) =
 744     let is_good_cond tm =
 745       try not(is_const(fst(dest_cond tm)))
 746       with Failure _ -> false in
 747     fun (asl,w) ->
 748       let cond = find_term (fun tm -> is_good_cond tm & free_in tm w) w in
 749       let p,(t,u) = dest_cond cond in
 750       let inst = INST_TYPE [type_of t, `:A`] COND_CLAUSES in
 751       let (ct,cf) = CONJ_PAIR (SPEC u (SPEC t inst)) in
 752       DISJ_CASES_THEN2
 753          (fun th -> SUBST1_TAC (EQT_INTRO th) THEN
 754                SUBST1_TAC ct THEN ASSUME_TAC th)
 755          (fun th -> SUBST1_TAC (EQF_INTRO th) THEN
 756                SUBST1_TAC cf THEN ASSUME_TAC th)
 757          (SPEC p EXCLUDED_MIDDLE)
 758          (asl,w) ;;
 759
 760 (* ------------------------------------------------------------------------- *)
 761 (* MATCH_MP_TAC allows universals on the right of implication.               *)
 762 (* Here's a crude hack to allow it.                                          *)
 763 (* ------------------------------------------------------------------------- *)
 764
 765 let MATCH_MP_TAC th =
 766   MATCH_MP_TAC th ORELSE
 767   MATCH_MP_TAC(PURE_REWRITE_RULE[RIGHT_IMP_FORALL_THM] th);;
 768
 769 (* ------------------------------------------------------------------------- *)
 770 (* Various theorems have different names.                                    *)
 771 (* ------------------------------------------------------------------------- *)
 772
 773 let ZERO_LESS_EQ = LE_0;;
 774
 775 let LESS_EQ_MONO = LE_SUC;;
 776
 777 let NOT_LESS = NOT_LT;;
 778
 779 let LESS_0 = LT_0;;
 780
 781 let LESS_EQ_REFL = LE_REFL;;
 782
 783 let LESS_EQUAL_ANTISYM = GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL LE_ANTISYM)));;
 784
 785 let NOT_LESS_0 = GEN_ALL(EQF_ELIM(SPEC_ALL(CONJUNCT1 LT)));;
 786
 787 let LESS_TRANS = LT_TRANS;;
 788
 789 let LESS_LEMMA1 = GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL(CONJUNCT2 LT))));;
 790
 791 let LESS_SUC_REFL = prove(`!n. n < SUC n`,REWRITE_TAC[LT]);;
 792
 793 let FACT_LESS = FACT_LT;;
 794
 795 let LESS_EQ_SUC_REFL = prove(`!n. n <= SUC n`,REWRITE_TAC[LE; LE_REFL]);;
 796
 797 let LESS_EQ_ADD = LE_ADD;;
 798
 799 let GREATER_EQ = GE;;
 800
 801 let LESS_EQUAL_ADD = GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL LE_EXISTS)));;
 802
 803 let LESS_EQ_IMP_LESS_SUC = GEN_ALL(snd(EQ_IMP_RULE(SPEC_ALL LT_SUC_LE)));;
 804
 805 let LESS_IMP_LESS_OR_EQ = LT_IMP_LE;;
 806
 807 let LESS_MONO_ADD = GEN_ALL(snd(EQ_IMP_RULE(SPEC_ALL LT_ADD_RCANCEL)));;
 808
 809 let LESS_SUC = prove(`!m n. m < n ==> m < (SUC n)`,MESON_TAC[LT]);;
 810
 811 let LESS_CASES = LTE_CASES;;
 812
 813 let LESS_EQ = GSYM LE_SUC_LT;;
 814
 815 let LESS_OR_EQ = LE_LT;;
 816
 817 let LESS_ADD_1 = GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL
 818     (REWRITE_RULE[ADD1] LT_EXISTS))));;
 819
 820 let SUC_SUB1 = prove(`!m. SUC m - 1 = m`,
 821                      REWRITE_TAC[num_CONV `1`; SUB_SUC; SUB_0]);;
 822
 823 let LESS_MONO_EQ = LT_SUC;;
 824
 825 let LESS_ADD_SUC = prove (`!m n. m < m + SUC n`,
 826                           REWRITE_TAC[ADD_CLAUSES; LT_SUC_LE; LE_ADD]);;
 827
 828 let LESS_REFL = LT_REFL;;
 829
 830 let INV_SUC_EQ = SUC_INJ;;
 831
 832 let LESS_EQ_CASES = LE_CASES;;
 833
 834 let LESS_EQ_TRANS = LE_TRANS;;
 835
 836 let LESS_THM = CONJUNCT2 LT;;
 837
 838 let GREATER = GT;;
 839
 840 let LESS_EQ_0 = CONJUNCT1 LE;;
 841
 842 let OR_LESS = GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL LE_SUC_LT)));;
 843
 844 let SUB_EQUAL_0 = SUB_REFL;;
 845
 846 let SUB_MONO_EQ = SUB_SUC;;
 847
 848 let NOT_SUC_LESS_EQ = prove (`!n m. ~(SUC n <= m) <=> m <= n`,
 849                              REWRITE_TAC[NOT_LE; LT] THEN
 850                              MESON_TAC[LE_LT]);;
 851
 852 let SUC_NOT = GSYM NOT_SUC;;
 853
 854 let LESS_LESS_CASES = prove(`!m n:num. (m = n) \/ m < n \/ n < m`,
 855                             MESON_TAC[LT_CASES]);;
 856
 857 let NOT_LESS_EQUAL = NOT_LE;;
 858
 859 let LESS_EQ_EXISTS = LE_EXISTS;;
 860
 861 let LESS_MONO_ADD_EQ = LT_ADD_RCANCEL;;
 862
 863 let LESS_LESS_EQ_TRANS = LTE_TRANS;;
 864
 865 let SUB_SUB = ARITH_RULE
 866   `!b c. c <= b ==> (!a:num. a - (b - c) = (a + c) - b)`;;
 867
 868 let LESS_CASES_IMP = ARITH_RULE
 869   `!m n:num. ~(m < n) /\ ~(m = n) ==> n < m`;;
 870
 871 let SUB_LESS_EQ = ARITH_RULE
 872   `!n m:num. (n - m) <= n`;;
 873
 874 let SUB_EQ_EQ_0 = ARITH_RULE
 875  `!m n:num. (m - n = m) <=> (m = 0) \/ (n = 0)`;;
 876
 877 let SUB_LEFT_LESS_EQ = ARITH_RULE
 878   `!m n p:num. m <= (n - p) <=> (m + p) <= n \/ m <= 0`;;
 879
 880 let SUB_LEFT_GREATER_EQ =
 881   ARITH_RULE `!m n p:num. m >= (n - p) <=> (m + p) >= n`;;
 882
 883 let LESS_EQ_LESS_TRANS = LET_TRANS;;
 884
 885 let LESS_0_CASES = ARITH_RULE `!m. (0 = m) \/ 0 < m`;;
 886
 887 let LESS_OR = ARITH_RULE `!m n. m < n ==> (SUC m) <= n`;;
 888
 889 let SUB = ARITH_RULE
 890   `(!m. 0 - m = 0) /\
 891    (!m n. (SUC m) - n = (if m < n then 0 else SUC(m - n)))`;;
 892
 893 let LESS_MULT_MONO = prove
 894  (`!m i n. ((SUC n) * m) < ((SUC n) * i) <=> m < i`,
 895   REWRITE_TAC[LT_MULT_LCANCEL; NOT_SUC]);;
 896
 897 let LESS_MONO_MULT = prove
 898  (`!m n p. m <= n ==> (m * p) <= (n * p)`,
 899   SIMP_TAC[LE_MULT_RCANCEL]);;
 900
 901 let LESS_MULT2 = prove
 902  (`!m n. 0 < m /\ 0 < n ==> 0 < (m * n)`,
 903   REWRITE_TAC[LT_MULT]);;
 904
 905 let SUBSET_FINITE = prove
 906  (`!s. FINITE s ==> (!t. t SUBSET s ==> FINITE t)`,
 907   MESON_TAC[FINITE_SUBSET]);;
 908
 909 let LESS_EQ_SUC = prove
 910  (`!n. m <= SUC n <=> (m = SUC n) \/ m <= n`,
 911   REWRITE_TAC[LE]);;
 912
 913 let ANTE_RES_THEN ttac th = FIRST_ASSUM(fun t -> ttac (MATCH_MP t th));;
 914
 915 let IMP_RES_THEN ttac th = FIRST_ASSUM(fun t -> ttac (MATCH_MP th t));;
 916
 917 (* ------------------------------------------------------------------------ *)
 918 (* Set theory lemmas.                                                       *)
 919 (* ------------------------------------------------------------------------ *)
 920
 921 let INFINITE_MEMBER = prove(
 922   `!s. INFINITE(s:A->bool) ==> ?x. x IN s`,
 923   GEN_TAC THEN DISCH_TAC THEN
 924   SUBGOAL_THEN `~(s:A->bool = {})` MP_TAC THENL
 925    [UNDISCH_TAC `INFINITE (s:A->bool)` THEN
 926     CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN
 927     DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[INFINITE; FINITE_EMPTY];
 928     REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN
 929     PURE_ONCE_REWRITE_TAC[NOT_FORALL_THM] THEN
 930     REWRITE_TAC[]]);;
 931
 932 let INFINITE_CHOOSE = prove(
 933   `!s:A->bool. INFINITE(s) ==> ((@) s) IN s`,
 934   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP INFINITE_MEMBER) THEN
 935   DISCH_THEN(MP_TAC o SELECT_RULE) THEN REWRITE_TAC[IN] THEN
 936   CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[]);;
 937
 938 let INFINITE_DELETE = prove(
 939   `!(t:A->bool) x. INFINITE (t DELETE x) = INFINITE(t)`,
 940   REWRITE_TAC[INFINITE; FINITE_DELETE]);;
 941
 942 let INFINITE_INSERT = prove(
 943   `!(x:A) t. INFINITE(x INSERT t) = INFINITE(t)`,
 944   REWRITE_TAC[INFINITE; FINITE_INSERT]);;
 945
 946 let SIZE_INSERT = prove(
 947   `!(x:A) t. ~(x IN t) /\ t HAS_SIZE n ==> (x INSERT t) HAS_SIZE (SUC n)`,
 948   SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_RULES]);;
 949
 950 let SIZE_DELETE = prove(
 951   `!(x:A) t. x IN t /\ t HAS_SIZE (SUC n) ==> (t DELETE x) HAS_SIZE n`,
 952   SIMP_TAC[HAS_SIZE_SUC]);;
 953
 954 let SIZE_EXISTS = prove(
 955   `!s N. s HAS_SIZE (SUC N) ==> ?x:A. x IN s`,
 956   SIMP_TAC[HAS_SIZE_SUC; GSYM MEMBER_NOT_EMPTY]);;
 957
 958 let SUBSET_DELETE = prove(
 959   `!s t (x:A). s SUBSET t ==> (s DELETE x) SUBSET t`,
 960   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_TRANS THEN
 961   EXISTS_TAC `s:A->bool` THEN ASM_REWRITE_TAC[DELETE_SUBSET]);;
 962
 963 let INFINITE_FINITE_CHOICE = prove(
 964   `!n (s:A->bool). INFINITE(s) ==> ?t. t SUBSET s /\ t HAS_SIZE n`,
 965   INDUCT_TAC THEN GEN_TAC THEN DISCH_TAC THENL
 966    [EXISTS_TAC `{}:A->bool` THEN
 967     REWRITE_TAC[HAS_SIZE; EMPTY_SUBSET; HAS_SIZE_0];
 968     FIRST_ASSUM(UNDISCH_TAC o check is_forall o concl) THEN
 969     DISCH_THEN(MP_TAC o SPEC `s DELETE ((@) s :A)`) THEN
 970     ASM_REWRITE_TAC[INFINITE_DELETE] THEN
 971     DISCH_THEN(X_CHOOSE_THEN `t:A->bool` STRIP_ASSUME_TAC) THEN
 972     EXISTS_TAC `((@) s :A) INSERT t` THEN CONJ_TAC THENL
 973      [REWRITE_TAC[INSERT_SUBSET] THEN CONJ_TAC THENL
 974        [MATCH_MP_TAC INFINITE_CHOOSE THEN ASM_REWRITE_TAC[];
 975         REWRITE_TAC[SUBSET] THEN
 976         RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN
 977         GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
 978         REWRITE_TAC[IN_DELETE] THEN CONV_TAC(EQT_INTRO o TAUT)];
 979         MATCH_MP_TAC SIZE_INSERT THEN ASM_REWRITE_TAC[] THEN
 980         DISCH_TAC THEN UNDISCH_TAC `t SUBSET (s DELETE ((@) s:A))` THEN
 981         REWRITE_TAC[SUBSET; IN_DELETE] THEN
 982         DISCH_THEN(IMP_RES_THEN MP_TAC) THEN REWRITE_TAC[]]]);;
 983
 984 let IMAGE_WOP_LEMMA = prove(
 985   `!N (t:num->bool) (u:A->bool).
 986         u SUBSET (IMAGE f t) /\ u HAS_SIZE (SUC N) ==>
 987         ?n v. (u = (f n) INSERT v) /\
 988               !y. y IN v ==> ?m. (y = f m) /\ n < m`,
 989   REPEAT STRIP_TAC THEN
 990   MP_TAC(SPEC `\n:num. ?y:A. y IN u /\ (y = f n)` num_WOP) THEN BETA_TAC THEN
 991   DISCH_THEN(MP_TAC o fst o EQ_IMP_RULE) THEN
 992   FIRST_ASSUM(X_CHOOSE_TAC `y:A` o MATCH_MP SIZE_EXISTS) THEN
 993   FIRST_ASSUM(MP_TAC o SPEC `y:A` o REWRITE_RULE[SUBSET]) THEN
 994   ASM_REWRITE_TAC[IN_IMAGE] THEN
 995   DISCH_THEN(X_CHOOSE_THEN `n:num` STRIP_ASSUME_TAC) THEN
 996   W(C SUBGOAL_THEN (fun t ->REWRITE_TAC[t]) o
 997        funpow 2 (fst o dest_imp) o snd) THENL
 998    [MAP_EVERY EXISTS_TAC [`n:num`; `y:A`] THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
 999   DISCH_THEN(X_CHOOSE_THEN `m:num` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
1000   DISCH_THEN(X_CHOOSE_THEN `x:A` STRIP_ASSUME_TAC) THEN
1001   MAP_EVERY EXISTS_TAC [`m:num`; `u DELETE (x:A)`] THEN CONJ_TAC THENL
1002    [ASM_REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN
1003     MATCH_MP_TAC INSERT_DELETE THEN FIRST_ASSUM(SUBST1_TAC o SYM) THEN
1004     FIRST_ASSUM MATCH_ACCEPT_TAC;
1005     X_GEN_TAC `z:A` THEN REWRITE_TAC[IN_DELETE] THEN STRIP_TAC THEN
1006     FIRST_ASSUM(MP_TAC o SPEC `z:A` o REWRITE_RULE[SUBSET]) THEN
1007     ASM_REWRITE_TAC[IN_IMAGE] THEN
1008     DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
1009     EXISTS_TAC `k:num` THEN ASM_REWRITE_TAC[GSYM NOT_LESS_EQUAL] THEN
1010     REWRITE_TAC[LESS_OR_EQ; DE_MORGAN_THM] THEN CONJ_TAC THENL
1011      [DISCH_THEN(ANTE_RES_THEN (MP_TAC o CONV_RULE NOT_EXISTS_CONV)) THEN
1012       DISCH_THEN(MP_TAC o SPEC `z:A`) THEN REWRITE_TAC[] THEN
1013       CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC;
1014       DISCH_THEN SUBST_ALL_TAC THEN
1015       UNDISCH_TAC `~(z:A = x)` THEN ASM_REWRITE_TAC[]]]);;
1016
1017 (* ------------------------------------------------------------------------ *)
1018 (* Lemma about finite colouring of natural numbers.                         *)
1019 (* ------------------------------------------------------------------------ *)
1020
1021 let COLOURING_LEMMA = prove(
1022   `!M col s. (INFINITE(s) /\ !n:A. n IN s ==> col(n) <= M) ==>
1023           ?c t. t SUBSET s /\ INFINITE(t) /\ !n:A. n IN t ==> (col(n) = c)`,
1024   INDUCT_TAC THENL
1025    [REWRITE_TAC[LESS_EQ_0] THEN REPEAT STRIP_TAC THEN
1026     MAP_EVERY EXISTS_TAC [`0`; `s:A->bool`] THEN
1027     ASM_REWRITE_TAC[SUBSET_REFL];
1028     REPEAT STRIP_TAC THEN SUBGOAL_THEN
1029      `INFINITE { x:A | x IN s /\ (col x = SUC M) } \/
1030       INFINITE { x:A | x IN s /\ col x <= M}`
1031     DISJ_CASES_TAC THENL
1032      [UNDISCH_TAC `INFINITE(s:A->bool)` THEN
1033       REWRITE_TAC[INFINITE; GSYM DE_MORGAN_THM; GSYM FINITE_UNION] THEN
1034       CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN
1035       DISCH_THEN(MATCH_MP_TAC o MATCH_MP SUBSET_FINITE) THEN
1036       REWRITE_TAC[SUBSET; IN_UNION] THEN
1037       REWRITE_TAC[IN_ELIM_THM] THEN
1038       GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[GSYM LESS_EQ_SUC] THEN
1039       FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1040       MAP_EVERY EXISTS_TAC [`SUC M`; `{ x:A | x IN s /\ (col x = SUC M)}`] THEN
1041       ASM_REWRITE_TAC[SUBSET] THEN REWRITE_TAC[IN_ELIM_THM] THEN
1042       REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
1043       SUBGOAL_THEN `!n:A. n IN { x | x IN s /\ col x <= M } ==> col(n) <= M`
1044       MP_TAC THENL
1045        [GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN
1046         DISCH_THEN(MATCH_ACCEPT_TAC o CONJUNCT2);
1047         FIRST_X_ASSUM(MP_TAC o SPECL [`col:A->num`;
1048                                         `{ x:A | x IN s /\ col x <= M}`]) THEN
1049         ASM_SIMP_TAC[] THEN
1050         MATCH_MP_TAC(TAUT `(c ==> d) ==> (b ==> c) ==> b ==> d`) THEN
1051         DISCH_THEN(X_CHOOSE_THEN `c:num` (X_CHOOSE_TAC `t:A->bool`)) THEN
1052         MAP_EVERY EXISTS_TAC [`c:num`; `t:A->bool`] THEN
1053         ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUBSET_TRANS THEN
1054         EXISTS_TAC `{ x:A | x IN s /\ col x <= M }` THEN ASM_REWRITE_TAC[] THEN
1055         REWRITE_TAC[SUBSET] THEN REWRITE_TAC[IN_ELIM_THM] THEN
1056         REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]]]]);;
1057
1058 let COLOURING_THM = prove(
1059   `!M col. (!n. col n <= M) ==>
1060            ?c s. INFINITE(s) /\ !n:num. n IN s ==> (col(n) = c)`,
1061   REPEAT STRIP_TAC THEN MP_TAC
1062    (ISPECL [`M:num`; `col:num->num`; `UNIV:num->bool`] COLOURING_LEMMA) THEN
1063   ASM_REWRITE_TAC[num_INFINITE] THEN
1064   DISCH_THEN(X_CHOOSE_THEN `c:num` (X_CHOOSE_TAC `t:num->bool`)) THEN
1065   MAP_EVERY EXISTS_TAC [`c:num`; `t:num->bool`] THEN ASM_REWRITE_TAC[]);;
1066
1067 (* ------------------------------------------------------------------------ *)
1068 (* Simple approach via lemmas then induction over size of coloured sets.    *)
1069 (* ------------------------------------------------------------------------ *)
1070
1071 let RAMSEY_LEMMA1 = prove(
1072  `(!C s. INFINITE(s:A->bool) /\
1073          (!t. t SUBSET s /\ t HAS_SIZE N ==> C(t) <= M)
1074          ==> ?t c. INFINITE(t) /\ t SUBSET s /\
1075                    (!u. u SUBSET t /\ u HAS_SIZE N ==> (C(u) = c)))
1076   ==> !C s. INFINITE(s:A->bool) /\
1077             (!t. t SUBSET s /\ t HAS_SIZE (SUC N) ==> C(t) <= M)
1078             ==> ?t c. INFINITE(t) /\ t SUBSET s /\ ~(((@) s) IN t) /\
1079                       (!u. u SUBSET t /\ u HAS_SIZE N
1080                            ==> (C(((@) s) INSERT u) = c))`,
1081   DISCH_THEN((THEN) (REPEAT STRIP_TAC) o MP_TAC) THEN
1082   DISCH_THEN(MP_TAC o SPEC `\u. C (((@) s :A) INSERT u):num`) THEN
1083   DISCH_THEN(MP_TAC o SPEC `s DELETE ((@)s:A)`) THEN BETA_TAC THEN
1084   ASM_REWRITE_TAC[INFINITE_DELETE] THEN
1085   W(C SUBGOAL_THEN (fun t ->REWRITE_TAC[t]) o
1086         funpow 2 (fst o dest_imp) o snd) THENL
1087    [REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN CONJ_TAC THENL
1088      [UNDISCH_TAC `t SUBSET (s DELETE ((@) s :A))` THEN
1089       REWRITE_TAC[SUBSET; IN_INSERT; IN_DELETE; NOT_IN_EMPTY] THEN
1090       DISCH_TAC THEN GEN_TAC THEN DISCH_THEN DISJ_CASES_TAC THEN
1091       ASM_REWRITE_TAC[] THENL
1092        [MATCH_MP_TAC INFINITE_CHOOSE;
1093         FIRST_ASSUM(ANTE_RES_THEN ASSUME_TAC)] THEN
1094       ASM_REWRITE_TAC[];
1095       MATCH_MP_TAC SIZE_INSERT THEN ASM_REWRITE_TAC[] THEN
1096       DISCH_TAC THEN UNDISCH_TAC `t SUBSET (s DELETE ((@) s :A))` THEN
1097       ASM_REWRITE_TAC[SUBSET; IN_DELETE] THEN
1098       DISCH_THEN(MP_TAC o SPEC `(@)s:A`) THEN ASM_REWRITE_TAC[]];
1099     DISCH_THEN(X_CHOOSE_THEN `t:A->bool` MP_TAC) THEN
1100     DISCH_THEN(X_CHOOSE_THEN `c:num` STRIP_ASSUME_TAC) THEN
1101     MAP_EVERY EXISTS_TAC [`t:A->bool`; `c:num`] THEN ASM_REWRITE_TAC[] THEN
1102     RULE_ASSUM_TAC(REWRITE_RULE[SUBSET; IN_DELETE]) THEN CONJ_TAC THENL
1103      [REWRITE_TAC[SUBSET] THEN
1104       GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN(fun th -> REWRITE_TAC[th]));
1105       DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN REWRITE_TAC[]]]);;
1106
1107 let RAMSEY_LEMMA2 = prove(
1108  `(!C s. INFINITE(s:A->bool) /\
1109          (!t. t SUBSET s /\ t HAS_SIZE (SUC N) ==> C(t) <= M)
1110         ==> ?t c. INFINITE(t) /\ t SUBSET s /\ ~(((@) s) IN t) /\
1111                   (!u. u SUBSET t /\ u HAS_SIZE N
1112                        ==> (C(((@) s) INSERT u) = c)))
1113   ==> !C s. INFINITE(s:A->bool) /\
1114             (!t. t SUBSET s /\ t HAS_SIZE (SUC N) ==> C(t) <= M)
1115             ==> ?t x col. (!n. col n <= M) /\
1116                           (!n. (t n) SUBSET s) /\
1117                           (!n. t(SUC n) SUBSET (t n)) /\
1118                           (!n. ~((x n) IN (t n))) /\
1119                           (!n. x(SUC n) IN (t n)) /\
1120                           (!n. (x n) IN s) /\
1121                           (!n u. u SUBSET (t n) /\ u HAS_SIZE N
1122                                  ==> (C((x n) INSERT u) = col n))`,
1123   REPEAT STRIP_TAC THEN
1124   MP_TAC(ISPECL [`s:A->bool`; `\s (n:num). @t:A->bool. ?c:num.
1125       INFINITE(t) /\
1126       t SUBSET s /\
1127       ~(((@) s) IN t) /\
1128       !u. u SUBSET t /\ u HAS_SIZE N ==> (C(((@) s) INSERT u) = c)`]
1129     num_Axiom) THEN DISCH_THEN(MP_TAC o BETA_RULE o EXISTENCE) THEN
1130   DISCH_THEN(X_CHOOSE_THEN `f:num->(A->bool)` STRIP_ASSUME_TAC) THEN
1131   SUBGOAL_THEN
1132    `!n:num. (f n) SUBSET (s:A->bool) /\
1133     ?c. INFINITE(f(SUC n)) /\ f(SUC n) SUBSET (f n) /\
1134         ~(((@)(f n)) IN (f(SUC n))) /\
1135         !u. u SUBSET (f(SUC n)) /\ u HAS_SIZE N ==>
1136           (C(((@)(f n)) INSERT u) = c:num)`
1137   MP_TAC THENL
1138    [MATCH_MP_TAC num_INDUCTION THEN REPEAT STRIP_TAC THENL
1139      [ASM_REWRITE_TAC[SUBSET_REFL];
1140       FIRST_ASSUM(SUBST1_TAC o SPEC `0`) THEN CONV_TAC SELECT_CONV THEN
1141       FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1142       MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `f(n:num):A->bool` THEN
1143       CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC;
1144       FIRST_ASSUM(SUBST1_TAC o SPEC `SUC n`) THEN CONV_TAC SELECT_CONV THEN
1145       FIRST_ASSUM MATCH_MP_TAC THEN CONJ_TAC THEN
1146       TRY(FIRST_ASSUM MATCH_ACCEPT_TAC) THEN REPEAT STRIP_TAC THEN
1147       FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1148       REPEAT(MATCH_MP_TAC SUBSET_TRANS THEN
1149         FIRST_ASSUM(fun th -> EXISTS_TAC(rand(concl th)) THEN
1150         CONJ_TAC THENL [FIRST_ASSUM MATCH_ACCEPT_TAC; ALL_TAC])) THEN
1151       MATCH_ACCEPT_TAC SUBSET_REFL];
1152     PURE_REWRITE_TAC[LEFT_EXISTS_AND_THM; RIGHT_EXISTS_AND_THM;
1153                      FORALL_AND_THM] THEN
1154     DISCH_THEN(REPEAT_TCL (CONJUNCTS_THEN2 ASSUME_TAC) MP_TAC) THEN
1155     DISCH_THEN(X_CHOOSE_TAC `col:num->num` o CONV_RULE SKOLEM_CONV) THEN
1156     MAP_EVERY EXISTS_TAC
1157       [`\n:num. f(SUC n):A->bool`; `\n:num. (@)(f n):A`] THEN
1158     BETA_TAC THEN EXISTS_TAC `col:num->num` THEN CONJ_TAC THENL
1159      [X_GEN_TAC `n:num` THEN
1160       FIRST_ASSUM(MP_TAC o MATCH_MP INFINITE_FINITE_CHOICE o SPEC `n:num`) THEN
1161       DISCH_THEN(CHOOSE_THEN MP_TAC o SPEC `N:num`) THEN
1162       DISCH_THEN(fun th -> STRIP_ASSUME_TAC th THEN
1163           ANTE_RES_THEN MP_TAC th) THEN
1164       DISCH_THEN(SUBST1_TAC o SYM) THEN FIRST_ASSUM MATCH_MP_TAC THEN
1165       CONJ_TAC THENL
1166        [REWRITE_TAC[INSERT_SUBSET] THEN CONJ_TAC THENL
1167          [FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[SUBSET]) THEN
1168           EXISTS_TAC `n:num` THEN MATCH_MP_TAC INFINITE_CHOOSE THEN
1169           SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
1170           TRY(FIRST_ASSUM MATCH_ACCEPT_TAC) THEN ASM_REWRITE_TAC[];
1171           MATCH_MP_TAC SUBSET_TRANS THEN
1172           EXISTS_TAC `f(SUC n):A->bool` THEN ASM_REWRITE_TAC[]];
1173         MATCH_MP_TAC SIZE_INSERT THEN ASM_REWRITE_TAC[] THEN
1174         UNDISCH_TAC `!n:num. ~(((@)(f n):A) IN (f(SUC n)))` THEN
1175         DISCH_THEN(MP_TAC o SPEC `n:num`) THEN CONV_TAC CONTRAPOS_CONV THEN
1176         REWRITE_TAC[] THEN
1177         FIRST_ASSUM(MATCH_ACCEPT_TAC o REWRITE_RULE[SUBSET])];
1178       REPEAT CONJ_TAC THEN TRY (FIRST_ASSUM MATCH_ACCEPT_TAC) THENL
1179        [GEN_TAC; INDUCT_TAC THENL
1180          [ASM_REWRITE_TAC[];
1181           FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[SUBSET]) THEN
1182           EXISTS_TAC `SUC n`]] THEN
1183       MATCH_MP_TAC INFINITE_CHOOSE THEN ASM_REWRITE_TAC[]]]);;
1184
1185 let RAMSEY_LEMMA3 = prove(
1186  `(!C s. INFINITE(s:A->bool) /\
1187              (!t. t SUBSET s /\ t HAS_SIZE (SUC N) ==> C(t) <= M)
1188              ==> ?t x col. (!n. col n <= M) /\
1189                            (!n. (t n) SUBSET s) /\
1190                            (!n. t(SUC n) SUBSET (t n)) /\
1191                            (!n. ~((x n) IN (t n))) /\
1192                            (!n. x(SUC n) IN (t n)) /\
1193                            (!n. (x n) IN s) /\
1194                            (!n u. u SUBSET (t n) /\ u HAS_SIZE N
1195                                   ==> (C((x n) INSERT u) = col n)))
1196   ==> !C s. INFINITE(s:A->bool) /\
1197             (!t. t SUBSET s /\ t HAS_SIZE (SUC N) ==> C(t) <= M)
1198             ==> ?t c. INFINITE(t) /\ t SUBSET s /\
1199                       (!u. u SUBSET t /\ u HAS_SIZE (SUC N) ==> (C(u) = c))`,
1200   DISCH_THEN((THEN) (REPEAT STRIP_TAC) o MP_TAC) THEN
1201   DISCH_THEN(MP_TAC o SPECL [`C:(A->bool)->num`; `s:A->bool`]) THEN
1202   ASM_REWRITE_TAC[] THEN
1203   DISCH_THEN(X_CHOOSE_THEN `t:num->(A->bool)` MP_TAC) THEN
1204   DISCH_THEN(X_CHOOSE_THEN `x:num->A` MP_TAC) THEN
1205   DISCH_THEN(X_CHOOSE_THEN `col:num->num` STRIP_ASSUME_TAC) THEN
1206   MP_TAC(ISPECL [`M:num`; `col:num->num`; `UNIV:num->bool`]
1207     COLOURING_LEMMA) THEN ASM_REWRITE_TAC[num_INFINITE] THEN
1208   DISCH_THEN(X_CHOOSE_THEN `c:num` MP_TAC) THEN
1209   DISCH_THEN(X_CHOOSE_THEN `t:num->bool` STRIP_ASSUME_TAC) THEN
1210   MAP_EVERY EXISTS_TAC [`IMAGE (x:num->A) t`; `c:num`] THEN
1211   SUBGOAL_THEN `!m n. m <= n ==> (t n:A->bool) SUBSET (t m)` ASSUME_TAC THENL
1212    [REPEAT GEN_TAC THEN REWRITE_TAC[LESS_EQ_EXISTS] THEN
1213     DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
1214     SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THEN
1215     ASM_REWRITE_TAC[ADD_CLAUSES; SUBSET_REFL] THEN
1216     MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `t(m + d):A->bool` THEN
1217     ASM_REWRITE_TAC[]; ALL_TAC] THEN
1218   SUBGOAL_THEN `!m n. m < n ==> (x n:A) IN (t m)` ASSUME_TAC THENL
1219    [REPEAT GEN_TAC THEN
1220     DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN
1221     FIRST_ASSUM(MP_TAC o SPECL [`m:num`; `m + d`]) THEN
1222     REWRITE_TAC[LESS_EQ_ADD; SUBSET] THEN DISCH_THEN MATCH_MP_TAC THEN
1223     ASM_REWRITE_TAC[GSYM ADD1; ADD_CLAUSES]; ALL_TAC] THEN
1224   SUBGOAL_THEN `!m n. ((x:num->A) m = x n) <=> (m = n)` ASSUME_TAC THENL
1225    [REPEAT GEN_TAC THEN EQ_TAC THENL
1226      [REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
1227        (SPECL [`m:num`; `n:num`] LESS_LESS_CASES) THEN
1228       ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN
1229       FIRST_ASSUM(ANTE_RES_THEN MP_TAC) THEN ASM_REWRITE_TAC[] THEN
1230       FIRST_ASSUM(UNDISCH_TAC o check is_eq o concl) THEN
1231       DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[];
1232       DISCH_THEN SUBST1_TAC THEN REFL_TAC]; ALL_TAC] THEN
1233   REPEAT CONJ_TAC THENL
1234    [UNDISCH_TAC `INFINITE(t:num->bool)` THEN
1235     MATCH_MP_TAC INFINITE_IMAGE_INJ THEN ASM_REWRITE_TAC[];
1236     REWRITE_TAC[SUBSET; IN_IMAGE] THEN GEN_TAC THEN
1237     DISCH_THEN(CHOOSE_THEN (SUBST1_TAC o CONJUNCT1)) THEN ASM_REWRITE_TAC[];
1238     GEN_TAC THEN DISCH_THEN(fun th -> STRIP_ASSUME_TAC th THEN MP_TAC th) THEN
1239     DISCH_THEN(MP_TAC o MATCH_MP IMAGE_WOP_LEMMA) THEN
1240     DISCH_THEN(X_CHOOSE_THEN `n:num` (X_CHOOSE_THEN `v:A->bool` MP_TAC)) THEN
1241     DISCH_THEN STRIP_ASSUME_TAC THEN ASM_REWRITE_TAC[] THEN
1242     SUBGOAL_THEN `c = (col:num->num) n` SUBST1_TAC THENL
1243      [CONV_TAC SYM_CONV THEN FIRST_ASSUM MATCH_MP_TAC THEN
1244       UNDISCH_TAC `u SUBSET (IMAGE (x:num->A) t)` THEN
1245       REWRITE_TAC[SUBSET; IN_IMAGE] THEN
1246       DISCH_THEN(MP_TAC o SPEC `(x:num->A) n`) THEN
1247       ASM_REWRITE_TAC[IN_INSERT] THEN
1248       DISCH_THEN(CHOOSE_THEN STRIP_ASSUME_TAC) THEN ASM_REWRITE_TAC[];
1249       FIRST_ASSUM MATCH_MP_TAC THEN CONJ_TAC THENL
1250        [REWRITE_TAC[SUBSET] THEN GEN_TAC THEN
1251         DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1252         DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
1253         ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1254         SUBGOAL_THEN `v = u DELETE ((x:num->A) n)` SUBST1_TAC THENL
1255          [ASM_REWRITE_TAC[] THEN REWRITE_TAC[DELETE_INSERT] THEN
1256           REWRITE_TAC[EXTENSION; IN_DELETE;
1257             TAUT `(a <=> a /\ b) <=> a ==> b`] THEN
1258           GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN
1259           DISCH_THEN SUBST1_TAC THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1260           ASM_REWRITE_TAC[] THEN
1261           DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1262           ASM_REWRITE_TAC[LESS_REFL];
1263           MATCH_MP_TAC SIZE_DELETE THEN CONJ_TAC THENL
1264            [ASM_REWRITE_TAC[IN_INSERT]; FIRST_ASSUM MATCH_ACCEPT_TAC]]]]]);;
1265
1266 let RAMSEY = prove(
1267   `!M N C s.
1268         INFINITE(s:A->bool) /\
1269         (!t. t SUBSET s /\ t HAS_SIZE N ==> C(t) <= M)
1270         ==> ?t c. INFINITE(t) /\ t SUBSET s /\
1271                   (!u. u SUBSET t /\ u HAS_SIZE N ==> (C(u) = c))`,
1272   GEN_TAC THEN INDUCT_TAC THENL
1273    [REPEAT STRIP_TAC THEN
1274     MAP_EVERY EXISTS_TAC [`s:A->bool`; `(C:(A->bool)->num) {}`] THEN
1275     ASM_REWRITE_TAC[HAS_SIZE_0] THEN
1276     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[SUBSET_REFL];
1277     MAP_EVERY MATCH_MP_TAC [RAMSEY_LEMMA3; RAMSEY_LEMMA2; RAMSEY_LEMMA1] THEN
1278     POP_ASSUM MATCH_ACCEPT_TAC]);;