Examples/hol88.ml

   1 (* ========================================================================= *)
   2 (* HOL88 compatibility: various things missing or different in HOL Light.    *)
   3 (* ========================================================================= *)
   4
   5 let (upto) = (--);;
   6
   7 let is_neg_imp tm =
   8   is_neg tm or is_imp tm;;
   9
  10 let dest_neg_imp tm =
  11   try dest_imp tm with Failure _ ->
  12   try (dest_neg tm,mk_const("F",[]))
  13   with Failure _ -> failwith "dest_neg_imp";;
  14
  15 (* ------------------------------------------------------------------------- *)
  16 (* I removed this recently. Note that it's intuitionistically valid.         *)
  17 (* ------------------------------------------------------------------------- *)
  18
  19 let CONTRAPOS =
  20   let a = `a:bool` and b = `b:bool` in
  21   let pth = ITAUT `(a ==> b) ==> (~b ==> ~a)` in
  22   fun th ->
  23     try let P,Q = dest_imp(concl th) in
  24         MP (INST [P,a; Q,b] pth) th
  25     with Failure _ -> failwith "CONTRAPOS";;
  26
  27 (* ------------------------------------------------------------------------- *)
  28 (* I also got rid of this; it's mainly used inside DISCH_TAC anyway.         *)
  29 (* ------------------------------------------------------------------------- *)
  30
  31 let NEG_DISCH =
  32   let falsity = `F` in
  33   fun t th ->
  34     try if concl th = falsity then NOT_INTRO(DISCH t th) else DISCH t th
  35     with Failure _ -> failwith "NEG_DISCH";;
  36
  37 (* ------------------------------------------------------------------------- *)
  38 (* These were never used (by me).                                            *)
  39 (* ------------------------------------------------------------------------- *)
  40
  41 let SELECT_ELIM th1 (v,th2) =
  42   try let P, SP = dest_comb(concl th1) in
  43       let th3 = DISCH (mk_comb(P,v)) th2 in
  44       MP (INST [SP,v] th3) th1
  45   with Failure _ -> failwith "SELECT_ELIM";;
  46
  47 let SELECT_INTRO =
  48   let P = `P:A->bool` and x = `x:A` in
  49   let pth = SPECL [P; x] SELECT_AX in
  50   fun th ->
  51     try let f,arg = dest_comb(concl th) in
  52         MP (PINST [type_of x,aty] [f,P; arg,x] pth) th
  53     with Failure _ -> failwith "SELECT_INTRO";;
  54
  55 (* ------------------------------------------------------------------------- *)
  56 (* Again, I never use this so I removed it from the core.                    *)
  57 (* ------------------------------------------------------------------------- *)
  58
  59 let EXT =
  60   let f = `f:A->B` and g = `g:A->B` in
  61   let pth = prove
  62    (`(!x. (f:A->B) x = g x) ==> (f = g)`,
  63     MATCH_ACCEPT_TAC EQ_EXT) in
  64   fun th ->
  65     try let x,bod = dest_forall(concl th) in
  66         let l,r = dest_eq bod in
  67         let l',r' = rator l, rator r in
  68         let th1 = PINST [type_of x,aty; type_of l,bty] [l',f; r',g] pth in
  69         MP th1 th
  70     with Failure _ -> failwith "EXT";;
  71
  72 (* ------------------------------------------------------------------------- *)
  73 (* These get overwritten by the subgoal stuff.                               *)
  74 (* ------------------------------------------------------------------------- *)
  75
  76 let PROVE = prove;;
  77
  78 let prove_thm((s:string),g,t) = prove(g,t);;
  79
  80 (* ------------------------------------------------------------------------- *)
  81 (* The quantifier movement conversions.                                      *)
  82 (* ------------------------------------------------------------------------- *)
  83
  84 let (CONV_OF_RCONV: conv -> conv) =
  85   let rec get_bv tm =
  86     if is_abs tm then bndvar tm
  87     else if is_comb tm then
  88          try get_bv (rand tm) with Failure _ -> get_bv (rator tm)
  89     else failwith "" in
  90   fun conv tm ->
  91   let v = get_bv tm in
  92   let th1 = conv tm in
  93   let th2 = ONCE_DEPTH_CONV (GEN_ALPHA_CONV v) (rhs(concl th1)) in
  94   TRANS th1 th2;;
  95
  96 let (CONV_OF_THM: thm -> conv) =
  97   CONV_OF_RCONV o REWR_CONV;;
  98
  99 let (X_FUN_EQ_CONV:term->conv) =
 100   fun v -> (REWR_CONV FUN_EQ_THM) THENC GEN_ALPHA_CONV v;;
 101
 102 let (FUN_EQ_CONV:conv) =
 103   fun tm ->
 104     let vars = frees tm in
 105     let op,[ty1;ty2] = dest_type(type_of (lhs tm)) in
 106     if op = "fun"
 107        then let varnm =
 108                 if (is_vartype ty1) then "x" else
 109                    hd(explode(fst(dest_type ty1))) in
 110             let x = variant vars (mk_var(varnm,ty1)) in
 111             X_FUN_EQ_CONV x tm
 112        else failwith "FUN_EQ_CONV";;
 113
 114 let (SINGLE_DEPTH_CONV:conv->conv) =
 115   let rec SINGLE_DEPTH_CONV conv tm =
 116     try conv tm with Failure _ ->
 117     (SUB_CONV (SINGLE_DEPTH_CONV conv) THENC (TRY_CONV conv)) tm in
 118   SINGLE_DEPTH_CONV;;
 119
 120 let (SKOLEM_CONV:conv) =
 121   SINGLE_DEPTH_CONV (REWR_CONV SKOLEM_THM);;
 122
 123 let (X_SKOLEM_CONV:term->conv) =
 124   fun v -> SKOLEM_CONV THENC GEN_ALPHA_CONV v;;
 125
 126 let EXISTS_UNIQUE_CONV tm =
 127   let v = bndvar(rand tm) in
 128   let th1 = REWR_CONV EXISTS_UNIQUE_THM tm in
 129   let tm1 = rhs(concl th1) in
 130   let vars = frees tm1 in
 131   let v = variant vars v in
 132   let v' = variant (v::vars) v in
 133   let th2 =
 134    (LAND_CONV(GEN_ALPHA_CONV v) THENC
 135     RAND_CONV(BINDER_CONV(GEN_ALPHA_CONV v') THENC
 136               GEN_ALPHA_CONV v)) tm1 in
 137   TRANS th1 th2;;
 138
 139 let NOT_FORALL_CONV = CONV_OF_THM NOT_FORALL_THM;;
 140
 141 let NOT_EXISTS_CONV = CONV_OF_THM NOT_EXISTS_THM;;
 142
 143 let RIGHT_IMP_EXISTS_CONV = CONV_OF_THM RIGHT_IMP_EXISTS_THM;;
 144
 145 let FORALL_IMP_CONV = CONV_OF_RCONV
 146   (REWR_CONV TRIV_FORALL_IMP_THM ORELSEC
 147    REWR_CONV RIGHT_FORALL_IMP_THM ORELSEC
 148    REWR_CONV LEFT_FORALL_IMP_THM);;
 149
 150 let EXISTS_AND_CONV = CONV_OF_RCONV
 151   (REWR_CONV TRIV_EXISTS_AND_THM ORELSEC
 152    REWR_CONV LEFT_EXISTS_AND_THM ORELSEC
 153    REWR_CONV RIGHT_EXISTS_AND_THM);;
 154
 155 let LEFT_IMP_EXISTS_CONV = CONV_OF_THM LEFT_IMP_EXISTS_THM;;
 156
 157 let LEFT_AND_EXISTS_CONV tm =
 158   let v = bndvar(rand(rand(rator tm))) in
 159   (REWR_CONV LEFT_AND_EXISTS_THM THENC TRY_CONV (GEN_ALPHA_CONV v)) tm;;
 160
 161 let RIGHT_AND_EXISTS_CONV =
 162   CONV_OF_THM RIGHT_AND_EXISTS_THM;;
 163
 164 let AND_FORALL_CONV = CONV_OF_THM AND_FORALL_THM;;
 165
 166 (* ------------------------------------------------------------------------- *)
 167 (* Paired beta conversion (now just a special case of GEN_BETA_CONV).        *)
 168 (* ------------------------------------------------------------------------- *)
 169
 170 let PAIRED_BETA_CONV =
 171   let pth = (EQT_ELIM o REWRITE_CONV [EXISTS_THM; GABS_DEF])
 172    `!P:A->bool. (?) P ==> P((GABS) P)`
 173   and pth1 = GSYM PASSOC_DEF and pth2 = GSYM UNCURRY_DEF in
 174   let dest_geq = dest_binary "GEQ" in
 175   let GEQ_RULE = CONV_RULE(REWR_CONV(GSYM GEQ_DEF))
 176   and UNGEQ_RULE = CONV_RULE(REWR_CONV GEQ_DEF) in
 177   let rec UNCURRY_CONV fn vs =
 178     try let l,r = dest_pair vs in
 179         try let r1,r2 = dest_pair r in
 180             let lr = mk_pair(l,r1) in
 181             let th0 = UNCURRY_CONV fn (mk_pair(lr,r2)) in
 182             let th1 = ISPECL [rator(rand(concl th0));l;r1;r2] pth1 in
 183             TRANS th0 th1
 184         with Failure _ ->
 185             let th0 = UNCURRY_CONV fn l in
 186             let fn' = rand(concl th0) in
 187             let th1 = UNCURRY_CONV fn' r in
 188             let th2 = ISPECL [rator fn';l;r] pth2 in
 189             TRANS (TRANS (AP_THM th0 r) th1) th2
 190     with Failure _ -> REFL(mk_comb(fn,vs)) in
 191   fun tm ->
 192     try BETA_CONV tm with Failure _ ->
 193     let gabs,args = dest_comb tm in
 194     let fn,bod = dest_binder "GABS" gabs in
 195     let avs,eqv = strip_forall bod in
 196     let l,r = dest_geq eqv in
 197     let pred = list_mk_abs(avs,r) in
 198     let th0 = rev_itlist
 199       (fun v th -> CONV_RULE(RAND_CONV BETA_CONV) (AP_THM th v))
 200       avs (REFL pred) in
 201     let th1 = TRANS (SYM(UNCURRY_CONV pred (rand l))) th0 in
 202     let th1a = GEQ_RULE th1 in
 203     let etm = list_mk_icomb "?" [rand gabs] in
 204     let th2 = EXISTS(etm,rator (lhand(concl th1a))) (GENL avs th1a) in
 205     let th3 = SPECL (striplist dest_pair args) (BETA_RULE(MATCH_MP pth th2)) in
 206     UNGEQ_RULE th3;;
 207
 208 (* ------------------------------------------------------------------------- *)
 209 (* The slew of named tautologies.                                            *)
 210 (* ------------------------------------------------------------------------- *)
 211
 212 let AND1_THM = TAUT `!t1 t2. t1 /\ t2 ==> t1`;;
 213
 214 let AND2_THM = TAUT `!t1 t2. t1 /\ t2 ==> t2`;;
 215
 216 let AND_IMP_INTRO = TAUT `!t1 t2 t3. t1 ==> t2 ==> t3 <=> t1 /\ t2 ==> t3`;;
 217
 218 let AND_INTRO_THM = TAUT `!t1 t2. t1 ==> t2 ==> t1 /\ t2`;;
 219
 220 let BOOL_EQ_DISTINCT = TAUT `~(T <=> F) /\ ~(F <=> T)`;;
 221
 222 let EQ_EXPAND = TAUT `!t1 t2. (t1 <=> t2) <=> t1 /\ t2 \/ ~t1 /\ ~t2`;;
 223
 224 let EQ_IMP_THM = TAUT `!t1 t2. (t1 <=> t2) <=> (t1 ==> t2) /\ (t2 ==> t1)`;;
 225
 226 let FALSITY = TAUT `!t. F ==> t`;;
 227
 228 let F_IMP = TAUT `!t. ~t ==> t ==> F`;;
 229
 230 let IMP_DISJ_THM = TAUT `!t1 t2. t1 ==> t2 <=> ~t1 \/ t2`;;
 231
 232 let IMP_F = TAUT `!t. (t ==> F) ==> ~t`;;
 233
 234 let IMP_F_EQ_F = TAUT `!t. t ==> F <=> (t <=> F)`;;
 235
 236 let LEFT_AND_OVER_OR = TAUT
 237   `!t1 t2 t3. t1 /\ (t2 \/ t3) <=> t1 /\ t2 \/ t1 /\ t3`;;
 238
 239 let LEFT_OR_OVER_AND = TAUT
 240   `!t1 t2 t3. t1 \/ t2 /\ t3 <=> (t1 \/ t2) /\ (t1 \/ t3)`;;
 241
 242 let NOT_AND = TAUT `~(t /\ ~t)`;;
 243
 244 let NOT_F = TAUT `!t. ~t ==> (t <=> F)`;;
 245
 246 let OR_ELIM_THM = TAUT
 247   `!t t1 t2. t1 \/ t2 ==> (t1 ==> t) ==> (t2 ==> t) ==> t`;;
 248
 249 let OR_IMP_THM = TAUT `!t1 t2. (t1 <=> t2 \/ t1) <=> t2 ==> t1`;;
 250
 251 let OR_INTRO_THM1 = TAUT `!t1 t2. t1 ==> t1 \/ t2`;;
 252
 253 let OR_INTRO_THM2 = TAUT `!t1 t2. t2 ==> t1 \/ t2`;;
 254
 255 let RIGHT_AND_OVER_OR = TAUT
 256   `!t1 t2 t3. (t2 \/ t3) /\ t1 <=> t2 /\ t1 \/ t3 /\ t1`;;
 257
 258 let RIGHT_OR_OVER_AND = TAUT
 259   `!t1 t2 t3. t2 /\ t3 \/ t1 <=> (t2 \/ t1) /\ (t3 \/ t1)`;;
 260
 261 (* ------------------------------------------------------------------------- *)
 262 (* This is an overwrite -- is there any point in what I have?                *)
 263 (* ------------------------------------------------------------------------- *)
 264
 265 let is_type = can get_type_arity;;
 266
 267 (* ------------------------------------------------------------------------- *)
 268 (* I suppose this is also useful.                                            *)
 269 (* ------------------------------------------------------------------------- *)
 270
 271 let is_constant = can get_const_type;;
 272
 273 (* ------------------------------------------------------------------------- *)
 274 (* Misc.                                                                     *)
 275 (* ------------------------------------------------------------------------- *)
 276
 277 let null l = l = [];;
 278
 279 let combine(a,b) = zip a b;;
 280
 281 let split = unzip;;
 282
 283 (* ------------------------------------------------------------------------- *)
 284 (* Syntax.                                                                   *)
 285 (* ------------------------------------------------------------------------- *)
 286
 287 let type_tyvars = type_vars_in_term o curry mk_var "x";;
 288
 289 let find_match u =
 290   let rec find_mt t =
 291     try term_match [] u t with Failure _ ->
 292     try find_mt(rator t) with Failure _ ->
 293     try find_mt(rand  t) with Failure _ ->
 294     try find_mt(snd(dest_abs t))
 295     with Failure _ -> failwith "find_match" in
 296   fun t -> let _,tmin,tyin = find_mt t in
 297            tmin,tyin;;
 298
 299 let rec mk_primed_var(name,ty) =
 300   if can get_const_type name then mk_primed_var(name^"'",ty)
 301   else mk_var(name,ty);;
 302
 303 let subst_occs =
 304   let rec subst_occs slist tm =
 305     let applic,noway = partition (fun (i,(t,x)) -> aconv tm x) slist in
 306     let sposs = map (fun (l,z) -> let l1,l2 = partition ((=) 1) l in
 307                                   (l1,z),(l2,z)) applic in
 308     let racts,rrest = unzip sposs in
 309     let acts = filter (fun t -> not (fst t = [])) racts in
 310     let trest = map (fun (n,t) -> (map (C (-) 1) n,t)) rrest in
 311     let urest = filter (fun t -> not (fst t = [])) trest in
 312     let tlist = urest @ noway in
 313       if acts = [] then
 314       if is_comb tm then
 315         let l,r = dest_comb tm in
 316         let l',s' = subst_occs tlist l in
 317         let r',s'' = subst_occs s' r in
 318         mk_comb(l',r'),s''
 319       else if is_abs tm then
 320         let bv,bod = dest_abs tm in
 321         let gv = genvar(type_of bv) in
 322         let nbod = vsubst[gv,bv] bod in
 323         let tm',s' = subst_occs tlist nbod in
 324         alpha bv (mk_abs(gv,tm')),s'
 325       else
 326         tm,tlist
 327     else
 328       let tm' = (fun (n,(t,x)) -> subst[t,x] tm) (hd acts) in
 329       tm',tlist in
 330   fun ilist slist tm -> fst(subst_occs (zip ilist slist) tm);;
 331
 332 (* ------------------------------------------------------------------------- *)
 333 (* Note that the all-instantiating INST and INST_TYPE are not overwritten.   *)
 334 (* ------------------------------------------------------------------------- *)
 335
 336 let INST_TY_TERM(substl,insttyl) th =
 337   let th' = INST substl (INST_TYPE insttyl th) in
 338   if hyp th' = hyp th then th'
 339   else failwith "INST_TY_TERM: Free term and/or type variables in hypotheses";;
 340
 341 (* ------------------------------------------------------------------------- *)
 342 (* Conversions stuff.                                                        *)
 343 (* ------------------------------------------------------------------------- *)
 344
 345 let RIGHT_CONV_RULE (conv:conv) th =
 346   TRANS th (conv(rhs(concl th)));;
 347
 348 (* ------------------------------------------------------------------------- *)
 349 (* Derived rules.                                                            *)
 350 (* ------------------------------------------------------------------------- *)
 351
 352 let NOT_EQ_SYM =
 353   let pth = GENL [`a:A`; `b:A`]
 354     (CONTRAPOS(DISCH_ALL(SYM(ASSUME`a:A = b`))))
 355   and aty = `:A` in
 356   fun th -> try let l,r = dest_eq(dest_neg(concl th)) in
 357                 MP (SPECL [r; l] (INST_TYPE [type_of l,aty] pth)) th
 358             with Failure _ -> failwith "NOT_EQ_SYM";;
 359
 360 let NOT_MP thi th =
 361   try MP thi th with Failure _ ->
 362   try let t = dest_neg (concl thi) in
 363       MP(MP (SPEC t F_IMP) thi) th
 364   with Failure _ -> failwith "NOT_MP";;
 365
 366 let FORALL_EQ x =
 367   let mkall = AP_TERM (mk_const("!",[type_of x,mk_vartype "A"])) in
 368   fun th -> try mkall (ABS x th)
 369             with Failure _ -> failwith "FORALL_EQ";;
 370
 371 let EXISTS_EQ x =
 372   let mkex = AP_TERM (mk_const("?",[type_of x,mk_vartype "A"])) in
 373   fun th -> try mkex (ABS x th)
 374             with Failure _ -> failwith "EXISTS_EQ";;
 375
 376 let SELECT_EQ x =
 377   let mksel = AP_TERM (mk_const("@",[type_of x,mk_vartype "A"])) in
 378   fun th -> try mksel (ABS x th)
 379             with Failure _ -> failwith "SELECT_EQ";;
 380
 381 let RIGHT_BETA th =
 382   try TRANS th (BETA_CONV(rhs(concl th)))
 383   with Failure _ -> failwith "RIGHT_BETA";;
 384
 385 let rec LIST_BETA_CONV tm =
 386   try let rat,rnd = dest_comb tm in
 387       RIGHT_BETA(AP_THM(LIST_BETA_CONV rat)rnd)
 388   with Failure _ -> REFL tm;;
 389
 390 let RIGHT_LIST_BETA th = TRANS th (LIST_BETA_CONV(snd(dest_eq(concl th))));;
 391
 392 let LIST_CONJ = end_itlist CONJ ;;
 393
 394 let rec CONJ_LIST n th =
 395   try if n=1 then [th] else (CONJUNCT1 th)::(CONJ_LIST (n-1) (CONJUNCT2 th))
 396   with Failure _ -> failwith "CONJ_LIST";;
 397
 398 let rec BODY_CONJUNCTS th =
 399   if is_forall(concl th) then
 400     BODY_CONJUNCTS (SPEC_ALL th) else
 401   if is_conj (concl th) then
 402       BODY_CONJUNCTS (CONJUNCT1 th) @ BODY_CONJUNCTS (CONJUNCT2 th)
 403   else [th];;
 404
 405 let rec IMP_CANON th =
 406     let w = concl th in
 407     if is_conj w then IMP_CANON (CONJUNCT1 th) @ IMP_CANON (CONJUNCT2 th)
 408     else if is_imp w then
 409         let ante,conc = dest_neg_imp w in
 410         if is_conj ante then
 411             let a,b = dest_conj ante in
 412             IMP_CANON
 413             (DISCH a (DISCH b (NOT_MP th (CONJ (ASSUME a) (ASSUME b)))))
 414         else if is_disj ante then
 415             let a,b = dest_disj ante in
 416             IMP_CANON (DISCH a (NOT_MP th (DISJ1 (ASSUME a) b))) @
 417             IMP_CANON (DISCH b (NOT_MP th (DISJ2 a (ASSUME b))))
 418         else if is_exists ante then
 419             let x,body = dest_exists ante in
 420             let x' = variant (thm_frees th) x in
 421             let body' = subst [x',x] body in
 422             IMP_CANON
 423             (DISCH body' (NOT_MP th (EXISTS (ante, x') (ASSUME body'))))
 424         else
 425         map (DISCH ante) (IMP_CANON (UNDISCH th))
 426     else if is_forall w then
 427         IMP_CANON (SPEC_ALL th)
 428     else [th];;
 429
 430 let LIST_MP  = rev_itlist (fun x y -> MP y x);;
 431
 432 let DISJ_IMP =
 433   let pth = TAUT`!t1 t2. t1 \/ t2 ==> ~t1 ==> t2` in
 434   fun th ->
 435     try let a,b = dest_disj(concl th) in MP (SPECL [a;b] pth) th
 436     with Failure _ -> failwith "DISJ_IMP";;
 437
 438 let IMP_ELIM =
 439   let pth = TAUT`!t1 t2. (t1 ==> t2) ==> ~t1 \/ t2` in
 440   fun th ->
 441     try let a,b = dest_imp(concl th) in MP (SPECL [a;b] pth) th
 442     with Failure _ -> failwith "IMP_ELIM";;
 443
 444 let DISJ_CASES_UNION dth ath bth =
 445     DISJ_CASES dth (DISJ1 ath (concl bth)) (DISJ2 (concl ath) bth);;
 446
 447 let MK_ABS qth =
 448   try let ov = bndvar(rand(concl qth)) in
 449       let bv,rth = SPEC_VAR qth in
 450       let sth = ABS bv rth in
 451       let cnv = ALPHA_CONV ov in
 452       CONV_RULE(BINOP_CONV cnv) sth
 453   with Failure _ -> failwith "MK_ABS";;
 454
 455 let HALF_MK_ABS th =
 456   try let th1 = MK_ABS th in
 457       CONV_RULE(LAND_CONV ETA_CONV) th1
 458   with Failure _ -> failwith "HALF_MK_ABS";;
 459
 460 let MK_EXISTS qth =
 461   try let ov = bndvar(rand(concl qth)) in
 462       let bv,rth = SPEC_VAR qth in
 463       let sth = EXISTS_EQ bv rth in
 464       let cnv = GEN_ALPHA_CONV ov in
 465       CONV_RULE(BINOP_CONV cnv) sth
 466   with Failure _ -> failwith "MK_EXISTS";;
 467
 468 let LIST_MK_EXISTS l th = itlist (fun x th -> MK_EXISTS(GEN x th)) l th;;
 469
 470 let IMP_CONJ th1 th2 =
 471   let A1,C1 = dest_imp (concl th1) and A2,C2 = dest_imp (concl th2) in
 472   let a1,a2 = CONJ_PAIR (ASSUME (mk_conj(A1,A2))) in
 473       DISCH (mk_conj(A1,A2)) (CONJ (MP th1 a1) (MP th2 a2));;
 474
 475 let EXISTS_IMP x =
 476   if not (is_var x) then failwith "EXISTS_IMP: first argument not a variable"
 477   else fun th ->
 478          try let ante,cncl = dest_imp(concl th) in
 479              let th1 = EXISTS (mk_exists(x,cncl),x) (UNDISCH th) in
 480              let asm = mk_exists(x,ante) in
 481              DISCH asm (CHOOSE (x,ASSUME asm) th1)
 482          with Failure _ ->
 483                 failwith "EXISTS_IMP: variable free in assumptions";;
 484
 485 let CONJUNCTS_CONV (t1,t2) =
 486   let rec build_conj thl t =
 487     try let l,r = dest_conj t in
 488         CONJ (build_conj thl l) (build_conj thl r)
 489     with Failure _ -> find (fun th -> concl th = t) thl in
 490   try IMP_ANTISYM_RULE
 491      (DISCH t1 (build_conj (CONJUNCTS (ASSUME t1)) t2))
 492      (DISCH t2 (build_conj (CONJUNCTS (ASSUME t2)) t1))
 493   with Failure _ -> failwith "CONJUNCTS_CONV";;
 494
 495 let CONJ_SET_CONV l1 l2 =
 496   try CONJUNCTS_CONV (list_mk_conj l1, list_mk_conj l2)
 497   with Failure _ -> failwith "CONJ_SET_CONV";;
 498
 499 let FRONT_CONJ_CONV tml t =
 500  let rec remove x l =
 501     if hd l = x then tl l else (hd l)::(remove x (tl l)) in
 502  try CONJ_SET_CONV tml (t::(remove t tml))
 503  with Failure _ -> failwith "FRONT_CONJ_CONV";;
 504
 505 let CONJ_DISCH =
 506   let pth = TAUT`!t t1 t2. (t ==> (t1 = t2)) ==> (t /\ t1 <=> t /\ t2)` in
 507   fun t th ->
 508     try let t1,t2 = dest_eq(concl th) in
 509         MP (SPECL [t; t1; t2] pth) (DISCH t th)
 510     with Failure _ -> failwith "CONJ_DISCH";;
 511
 512 let rec CONJ_DISCHL l th =
 513   if l = [] then th else CONJ_DISCH (hd l) (CONJ_DISCHL (tl l) th);;
 514
 515 let rec GSPEC th =
 516   let wl,w = dest_thm th in
 517   if is_forall w then
 518       GSPEC (SPEC (genvar (type_of (fst (dest_forall w)))) th)
 519   else th;;
 520
 521 let ANTE_CONJ_CONV tm =
 522   try let (a1,a2),c = (dest_conj F_F I) (dest_imp tm) in
 523       let imp1 = MP (ASSUME tm) (CONJ (ASSUME a1) (ASSUME a2)) and
 524           imp2 = LIST_MP [CONJUNCT1 (ASSUME (mk_conj(a1,a2)));
 525                           CONJUNCT2 (ASSUME (mk_conj(a1,a2)))]
 526                          (ASSUME (mk_imp(a1,mk_imp(a2,c)))) in
 527       IMP_ANTISYM_RULE (DISCH_ALL (DISCH a1 (DISCH a2 imp1)))
 528                        (DISCH_ALL (DISCH (mk_conj(a1,a2)) imp2))
 529   with Failure _ -> failwith "ANTE_CONJ_CONV";;
 530
 531 let bool_EQ_CONV =
 532   let check = let boolty = `:bool` in check (fun tm -> type_of tm = boolty) in
 533   let clist = map (GEN `b:bool`)
 534                   (CONJUNCTS(SPEC `b:bool` EQ_CLAUSES)) in
 535   let tb = hd clist and bt = hd(tl clist) in
 536   let T = `T` and F = `F` in
 537   fun tm ->
 538     try let l,r = (I F_F check) (dest_eq tm) in
 539         if l = r then EQT_INTRO (REFL l) else
 540         if l = T then SPEC r tb else
 541         if r = T then SPEC l bt else fail()
 542     with Failure _ -> failwith "bool_EQ_CONV";;
 543
 544 let COND_CONV =
 545   let T = `T` and F = `F` and vt = genvar`:A` and vf = genvar `:A` in
 546   let gen = GENL [vt;vf] in
 547   let CT,CF = (gen F_F gen) (CONJ_PAIR (SPECL [vt;vf] COND_CLAUSES)) in
 548   fun tm ->
 549     let P,(u,v) = try dest_cond tm
 550                   with Failure _ -> failwith "COND_CONV: not a conditional" in
 551     let ty = type_of u in
 552     if (P=T) then SPEC v (SPEC u (INST_TYPE [ty,`:A`] CT)) else
 553     if (P=F) then SPEC v (SPEC u (INST_TYPE [ty,`:A`] CF)) else
 554     if (u=v) then SPEC u (SPEC P (INST_TYPE [ty,`:A`] COND_ID)) else
 555     if (aconv u v) then
 556        let cnd = AP_TERM (rator tm) (ALPHA v u) in
 557        let thm = SPEC u (SPEC P (INST_TYPE [ty,`:A`] COND_ID)) in
 558            TRANS cnd thm else
 559   failwith "COND_CONV: can't simplify conditional";;
 560
 561 let SUBST_MATCH eqth th =
 562  let tm_inst,ty_inst = find_match (lhs(concl eqth)) (concl th) in
 563  SUBS [INST tm_inst (INST_TYPE ty_inst eqth)] th;;
 564
 565 let SUBST thl pat th =
 566   let eqs,vs = unzip thl in
 567   let gvs = map (genvar o type_of) vs in
 568   let gpat = subst (zip gvs vs) pat in
 569   let ls,rs = unzip (map (dest_eq o concl) eqs) in
 570   let ths = map (ASSUME o mk_eq) (zip gvs rs) in
 571   let th1 = ASSUME gpat in
 572   let th2 = SUBS ths th1 in
 573   let th3 = itlist DISCH (map concl ths) (DISCH gpat th2) in
 574   let th4 = INST (zip ls gvs) th3 in
 575   MP (rev_itlist (C MP) eqs th4) th;;
 576
 577 (* ------------------------------------------------------------------------- *)
 578 (* A poor thing but my own. The original (bogus) code used mk_thm.           *)
 579 (* I haven't bothered with GSUBS and SUBS_OCCS.                              *)
 580 (* ------------------------------------------------------------------------- *)
 581
 582 let SUBST_CONV thvars template tm =
 583   let thms,vars = unzip thvars in
 584   let gvs = map (genvar o type_of) vars in
 585   let gtemplate = subst (zip gvs vars) template in
 586   SUBST (zip thms gvs) (mk_eq(template,gtemplate)) (REFL tm);;
 587
 588 (* ------------------------------------------------------------------------- *)
 589 (* Filtering rewrites.                                                       *)
 590 (* ------------------------------------------------------------------------- *)
 591
 592 let FILTER_PURE_ASM_REWRITE_RULE f thl th =
 593     PURE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
 594
 595 and FILTER_ASM_REWRITE_RULE f thl th =
 596     REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
 597
 598 and FILTER_PURE_ONCE_ASM_REWRITE_RULE f thl th =
 599     PURE_ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
 600
 601 and FILTER_ONCE_ASM_REWRITE_RULE f thl th =
 602     ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th;;
 603
 604 let (FILTER_PURE_ASM_REWRITE_TAC: (term->bool) -> thm list -> tactic) =
 605   fun f thl (asl,w) ->
 606     PURE_REWRITE_TAC (filter (f o concl) (map snd asl) @ thl) (asl,w)
 607
 608 and (FILTER_ASM_REWRITE_TAC: (term->bool) -> thm list -> tactic) =
 609   fun f thl (asl,w) ->
 610     REWRITE_TAC (filter (f o concl) (map snd asl) @ thl) (asl,w)
 611
 612 and (FILTER_PURE_ONCE_ASM_REWRITE_TAC: (term->bool) -> thm list -> tactic) =
 613   fun f thl (asl,w) ->
 614     PURE_ONCE_REWRITE_TAC (filter (f o concl) (map snd asl) @ thl) (asl,w)
 615
 616 and (FILTER_ONCE_ASM_REWRITE_TAC: (term->bool) -> thm list -> tactic) =
 617   fun f thl (asl,w) ->
 618     ONCE_REWRITE_TAC (filter (f o concl) (map snd asl) @ thl) (asl,w);;
 619
 620 (* ------------------------------------------------------------------------- *)
 621 (* Tacticals.                                                                *)
 622 (* ------------------------------------------------------------------------- *)
 623
 624 let DISJ_CASES_THENL =
 625   end_itlist DISJ_CASES_THEN2;;
 626
 627 let (X_CASES_THENL: term list list -> thm_tactic list -> thm_tactic) =
 628   fun varsl ttacl ->
 629     end_itlist DISJ_CASES_THEN2
 630        (map (fun (vars,ttac) -> EVERY_TCL (map X_CHOOSE_THEN vars) ttac)
 631         (zip varsl ttacl));;
 632
 633 let (X_CASES_THEN: term list list -> thm_tactical) =
 634   fun varsl ttac ->
 635     end_itlist DISJ_CASES_THEN2
 636        (map (fun vars -> EVERY_TCL (map X_CHOOSE_THEN vars) ttac) varsl);;
 637
 638 let (CASES_THENL: thm_tactic list -> thm_tactic) =
 639   fun ttacl -> end_itlist DISJ_CASES_THEN2 (map (REPEAT_TCL CHOOSE_THEN) ttacl);;
 640
 641 (* ------------------------------------------------------------------------- *)
 642 (* Tactics.                                                                  *)
 643 (* ------------------------------------------------------------------------- *)
 644
 645 let (DISCARD_TAC: thm_tactic) =
 646   let truth = `T` in
 647   fun th (asl,w) ->
 648     if exists (aconv (concl th)) (truth::(map (concl o snd) asl))
 649     then ALL_TAC (asl,w)
 650     else failwith "DISCARD_TAC";;
 651
 652 let (GSUBST_TAC:((term * term)list->term->term)->thm list -> tactic) =
 653   fun substfn ths (asl,w) ->
 654   let ls,rs = split (map (dest_eq o concl) ths) in
 655   let vars = map (genvar o type_of) ls in
 656   let base = substfn (combine(vars,ls)) w in
 657   let rfn i thl =
 658     match thl with
 659      [th] -> SUBST (combine(map SYM ths, vars)) base th
 660     | _ -> failwith "" in
 661   null_meta,
 662   [asl,subst (combine(rs,vars)) base],
 663   rfn;;
 664
 665 let SUBST_TAC = GSUBST_TAC subst;;
 666
 667 let SUBST_OCCS_TAC nlths =
 668   let nll,ths = split nlths in GSUBST_TAC (subst_occs nll) ths;;
 669
 670 let (CHECK_ASSUME_TAC: thm_tactic) =
 671   fun gth ->
 672     FIRST [CONTR_TAC gth;  ACCEPT_TAC gth;
 673            DISCARD_TAC gth; ASSUME_TAC gth];;
 674
 675 let (FILTER_GEN_TAC: term -> tactic) =
 676   fun tm (asl,w) ->
 677     if is_forall w & not (tm = fst(dest_forall w)) then
 678         GEN_TAC (asl,w)
 679     else failwith "FILTER_GEN_TAC";;
 680
 681 let (FILTER_DISCH_THEN: thm_tactic -> term -> tactic) =
 682   fun ttac tm (asl,w) ->
 683     if is_neg_imp w & not (free_in tm (fst(dest_neg_imp w))) then
 684       DISCH_THEN ttac (asl,w)
 685     else failwith "FILTER_DISCH_THEN";;
 686
 687 let FILTER_STRIP_THEN ttac tm =
 688   FIRST [FILTER_GEN_TAC tm; FILTER_DISCH_THEN ttac tm; CONJ_TAC];;
 689
 690 let FILTER_DISCH_TAC = FILTER_DISCH_THEN STRIP_ASSUME_TAC;;
 691
 692 let FILTER_STRIP_TAC = FILTER_STRIP_THEN STRIP_ASSUME_TAC;;
 693
 694 (* ------------------------------------------------------------------------- *)
 695 (* Resolution stuff.                                                         *)
 696 (* ------------------------------------------------------------------------- *)
 697
 698 let RES_CANON =
 699     let not_elim th =
 700       if is_neg (concl th) then true,(NOT_ELIM th) else (false,th) in
 701     let rec canon fl th =
 702        let w = concl th in
 703        if (is_conj w) then
 704           let (th1,th2) = CONJ_PAIR th in (canon fl th1) @ (canon fl th2) else
 705        if ((is_imp w) & not(is_neg w)) then
 706           let ante,conc = dest_neg_imp w in
 707           if (is_conj ante) then
 708              let a,b = dest_conj ante in
 709              let cth = NOT_MP th (CONJ (ASSUME a) (ASSUME b)) in
 710              let th1 = DISCH b cth and th2 = DISCH a cth in
 711                  (canon true (DISCH a th1)) @ (canon true (DISCH b th2)) else
 712           if (is_disj ante) then
 713              let a,b = dest_disj ante in
 714              let ath = DISJ1 (ASSUME a) b and bth = DISJ2 a (ASSUME b) in
 715              let th1 = DISCH a (NOT_MP th ath) and
 716                  th2 = DISCH b (NOT_MP th bth) in
 717                  (canon true th1) @ (canon true th2) else
 718           if (is_exists ante) then
 719              let v,body = dest_exists ante in
 720              let newv = variant (thm_frees th) v in
 721              let newa = subst [newv,v] body in
 722              let th1 = NOT_MP th (EXISTS (ante, newv) (ASSUME newa)) in
 723                  canon true (DISCH newa th1) else
 724              map (GEN_ALL o (DISCH ante)) (canon true (UNDISCH th)) else
 725        if (is_eq w & (type_of (rand w) = `:bool`)) then
 726           let (th1,th2) = EQ_IMP_RULE th in
 727           (if fl then [GEN_ALL th] else []) @
 728                        (canon true th1) @ (canon true th2) else
 729        if (is_forall w) then
 730            let vs,body = strip_forall w in
 731            let fvs = thm_frees th in
 732            let vfn = fun l -> variant (l @ fvs) in
 733            let nvs = itlist
 734                    (fun v nv -> let v' = vfn nv v in (v'::nv)) vs [] in
 735                canon fl (SPECL nvs th) else
 736        if fl then [GEN_ALL th] else [] in
 737     fun th -> try let args = map (not_elim o SPEC_ALL)
 738                                  (CONJUNCTS (SPEC_ALL th)) in
 739                   let imps = flat (map (map GEN_ALL o (uncurry canon)) args) in
 740                   check ((not) o (=) []) imps
 741               with Failure _ ->
 742                 failwith
 743                   "RES_CANON: no implication is derivable from input thm.";;
 744
 745 let IMP_RES_THEN,RES_THEN =
 746   let MATCH_MP impth =
 747       let sth = SPEC_ALL impth in
 748       let matchfn = (fun (a,b,c) -> b,c) o
 749                     term_match [] (fst(dest_neg_imp(concl sth))) in
 750          fun th -> NOT_MP (INST_TY_TERM (matchfn (concl th)) sth) th in
 751   let check st l = (if l = [] then failwith st else l) in
 752   let IMP_RES_THEN ttac impth =
 753       let ths = try RES_CANON impth
 754                 with Failure _ -> failwith "IMP_RES_THEN: no implication" in
 755       ASSUM_LIST
 756        (fun asl ->
 757         let l = itlist (fun th -> (@) (mapfilter (MATCH_MP th) asl)) ths [] in
 758         let res = check "IMP_RES_THEN: no resolvents " l in
 759         let tacs = check "IMP_RES_THEN: no tactics" (mapfilter ttac res) in
 760         EVERY tacs) in
 761   let RES_THEN ttac (asl,g) =
 762       let asm = map snd asl in
 763       let ths = itlist (@) (mapfilter RES_CANON asm) [] in
 764       let imps = check "RES_THEN: no implication" ths in
 765       let l = itlist (fun th -> (@) (mapfilter (MATCH_MP th) asm)) imps [] in
 766       let res = check "RES_THEN: no resolvents " l in
 767       let tacs = check "RES_THEN: no tactics" (mapfilter ttac res) in
 768           EVERY tacs (asl,g) in
 769   IMP_RES_THEN,RES_THEN;;
 770
 771 let IMP_RES_TAC th g =
 772   try IMP_RES_THEN (REPEAT_GTCL IMP_RES_THEN STRIP_ASSUME_TAC) th g
 773   with Failure _ -> ALL_TAC g;;
 774
 775 let RES_TAC g =
 776   try RES_THEN (REPEAT_GTCL IMP_RES_THEN STRIP_ASSUME_TAC) g
 777   with Failure _ -> ALL_TAC g;;
 778
 779 (* ------------------------------------------------------------------------- *)
 780 (* Stuff for handling type definitions.                                      *)
 781 (* ------------------------------------------------------------------------- *)
 782
 783 let prove_rep_fn_one_one th =
 784   try let thm = CONJUNCT1 th in
 785       let A,R = (I F_F rator) (dest_comb(lhs(snd(dest_forall(concl thm))))) in
 786       let _,[aty;rty] = dest_type (type_of R) in
 787       let a = mk_primed_var("a",aty) in let a' = variant [a] a in
 788       let a_eq_a' = mk_eq(a,a') and
 789           Ra_eq_Ra' = mk_eq(mk_comb(R,a),mk_comb (R,a')) in
 790       let th1 = AP_TERM A (ASSUME Ra_eq_Ra') in
 791       let ga1 = genvar aty and ga2 = genvar aty in
 792       let th2 = SUBST [SPEC a thm,ga1;SPEC a' thm,ga2] (mk_eq(ga1,ga2)) th1 in
 793       let th3 = DISCH a_eq_a' (AP_TERM R (ASSUME a_eq_a')) in
 794           GEN a (GEN a' (IMP_ANTISYM_RULE (DISCH Ra_eq_Ra' th2) th3))
 795   with Failure _ -> failwith "prove_rep_fn_one_one";;
 796
 797 let prove_rep_fn_onto th =
 798   try let [th1;th2] = CONJUNCTS th in
 799       let r,eq = (I F_F rhs)(dest_forall(concl th2)) in
 800       let RE,ar = dest_comb(lhs eq) and
 801           sr = (mk_eq o (fun (x,y) -> y,x) o dest_eq) eq in
 802       let a = mk_primed_var ("a",type_of ar) in
 803       let sra = mk_eq(r,mk_comb(RE,a)) in
 804       let ex = mk_exists(a,sra) in
 805       let imp1 = EXISTS (ex,ar) (SYM(ASSUME eq)) in
 806       let v = genvar (type_of r) and
 807           A = rator ar and
 808           s' = AP_TERM RE (SPEC a th1) in
 809       let th = SUBST[SYM(ASSUME sra),v](mk_eq(mk_comb(RE,mk_comb(A,v)),v))s' in
 810       let imp2 = CHOOSE (a,ASSUME ex) th in
 811       let swap = IMP_ANTISYM_RULE (DISCH eq imp1) (DISCH ex imp2) in
 812           GEN r (TRANS (SPEC r th2) swap)
 813   with Failure _ -> failwith "prove_rep_fn_onto";;
 814
 815 let prove_abs_fn_onto th =
 816   try let [th1;th2] = CONJUNCTS th in
 817       let a,(A,R) = (I F_F ((I F_F rator)o dest_comb o lhs))
 818         (dest_forall(concl th1)) in
 819       let thm1 = EQT_ELIM(TRANS (SPEC (mk_comb (R,a)) th2)
 820                                 (EQT_INTRO (AP_TERM R (SPEC a th1)))) in
 821       let thm2 = SYM(SPEC a th1) in
 822       let r,P = (I F_F (rator o lhs)) (dest_forall(concl th2)) in
 823       let ex = mk_exists(r,mk_conj(mk_eq(a,mk_comb(A,r)),mk_comb(P,r))) in
 824           GEN a (EXISTS(ex,mk_comb(R,a)) (CONJ thm2 thm1))
 825   with Failure _ -> failwith "prove_abs_fn_onto";;
 826
 827 let prove_abs_fn_one_one th =
 828   try let [th1;th2] = CONJUNCTS th in
 829       let r,P = (I F_F (rator o lhs)) (dest_forall(concl th2)) and
 830           A,R = (I F_F rator) (dest_comb(lhs(snd(dest_forall(concl th1))))) in
 831       let r' = variant [r] r in
 832       let as1 = ASSUME(mk_comb(P,r)) and as2 = ASSUME(mk_comb(P,r')) in
 833       let t1 = EQ_MP (SPEC r th2) as1 and t2 = EQ_MP (SPEC r' th2) as2 in
 834       let eq = (mk_eq(mk_comb(A,r),mk_comb(A,r'))) in
 835       let v1 = genvar(type_of r) and v2 = genvar(type_of r) in
 836       let i1 = DISCH eq
 837                (SUBST [t1,v1;t2,v2] (mk_eq(v1,v2)) (AP_TERM R (ASSUME eq))) and
 838           i2 = DISCH (mk_eq(r,r')) (AP_TERM A (ASSUME (mk_eq(r,r')))) in
 839       let thm = IMP_ANTISYM_RULE i1 i2 in
 840       let disch =  DISCH (mk_comb(P,r)) (DISCH (mk_comb(P,r')) thm) in
 841           GEN r (GEN r' disch)
 842   with Failure _ -> failwith "prove_abs_fn_one_one";;
 843
 844 (* ------------------------------------------------------------------------- *)
 845 (* AC rewriting needs to be wrapped up as a special conversion.              *)
 846 (* ------------------------------------------------------------------------- *)
 847
 848 let AC_CONV(associative,commutative) tm =
 849   try
 850    let op = (rator o rator o lhs o snd o strip_forall o concl) commutative in
 851    let ty = (hd o snd o dest_type o type_of) op in
 852    let x = mk_var("x",ty) and y = mk_var("y",ty) and z = mk_var("z",ty) in
 853    let xy = mk_comb(mk_comb(op,x),y) and yz = mk_comb(mk_comb(op,y),z)
 854    and yx = mk_comb(mk_comb(op,y),x) in
 855    let comm = PART_MATCH I commutative (mk_eq(xy,yx))
 856    and ass = PART_MATCH I (SYM (SPEC_ALL associative))
 857               (mk_eq(mk_comb(mk_comb(op,xy),z),mk_comb(mk_comb(op,x),yz))) in
 858    let asc = TRANS (SUBS [comm] (SYM ass)) (INST[(x,y); (y,x)] ass) in
 859    let init = TOP_DEPTH_CONV (REWR_CONV ass) tm in
 860    let gl = rhs (concl init) in
 861
 862    let rec bubble head expr =
 863      let ((xop,l),r) = (dest_comb F_F I) (dest_comb expr) in
 864      if xop = op then
 865        if l = head then REFL expr else
 866        if r = head then INST [(l,x); (r,y)] comm
 867        else let subb = bubble head r in
 868             let eqv =  AP_TERM (mk_comb(xop,l)) subb
 869             and ((yop,l'),r') = (dest_comb F_F I)
 870                      (dest_comb (snd (dest_eq (concl subb)))) in
 871             TRANS eqv (INST[(l,x); (l',y); (r',z)] asc)
 872      else failwith "" in
 873
 874    let rec asce (l,r) =
 875      if l = r then REFL l
 876      else let ((zop,l'),r') = (dest_comb F_F I) (dest_comb l) in
 877           if zop = op then
 878             let beq = bubble l' r in
 879             let rt = snd (dest_eq (concl beq)) in
 880               TRANS (AP_TERM (mk_comb(op,l'))
 881                       (asce ((snd (dest_comb l)),(snd (dest_comb rt)))))
 882                     (SYM beq)
 883           else failwith "" in
 884
 885    EQT_INTRO (EQ_MP (SYM init) (asce (dest_eq gl)))
 886   with _ -> failwith "AC_CONV";;
 887
 888 let AC_RULE ths = EQT_ELIM o AC_CONV ths;;
 889
 890 (* ------------------------------------------------------------------------- *)
 891 (* The order of picking conditionals is different!                           *)
 892 (* ------------------------------------------------------------------------- *)
 893
 894 let (COND_CASES_TAC :tactic) =
 895     let is_good_cond tm =
 896       try not(is_const(fst(dest_cond tm)))
 897       with Failure _ -> false in
 898     fun (asl,w) ->
 899       let cond = find_term (fun tm -> is_good_cond tm & free_in tm w) w in
 900       let p,(t,u) = dest_cond cond in
 901       let inst = INST_TYPE [type_of t, `:A`] COND_CLAUSES in
 902       let (ct,cf) = CONJ_PAIR (SPEC u (SPEC t inst)) in
 903       DISJ_CASES_THEN2
 904          (fun th -> SUBST1_TAC (EQT_INTRO th) THEN
 905                SUBST1_TAC ct THEN ASSUME_TAC th)
 906          (fun th -> SUBST1_TAC (EQF_INTRO th) THEN
 907                SUBST1_TAC cf THEN ASSUME_TAC th)
 908          (SPEC p EXCLUDED_MIDDLE)
 909          (asl,w) ;;
 910
 911 (* ------------------------------------------------------------------------- *)
 912 (* MATCH_MP_TAC allows universals on the right of implication.               *)
 913 (* Here's a crude hack to allow it.                                          *)
 914 (* ------------------------------------------------------------------------- *)
 915
 916 let MATCH_MP_TAC th =
 917   MATCH_MP_TAC th ORELSE
 918   MATCH_MP_TAC(PURE_REWRITE_RULE[RIGHT_IMP_FORALL_THM] th);;
 919
 920 (* ------------------------------------------------------------------------- *)
 921 (* Various theorems have different names.                                    *)
 922 (* ------------------------------------------------------------------------- *)
 923
 924 let ZERO_LESS_EQ = LE_0;;
 925
 926 let LESS_EQ_MONO = LE_SUC;;
 927
 928 let NOT_LESS = NOT_LT;;
 929
 930 let LESS_0 = LT_0;;
 931
 932 let LESS_EQ_REFL = LE_REFL;;
 933
 934 let LESS_EQUAL_ANTISYM = GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL LE_ANTISYM)));;
 935
 936 let NOT_LESS_0 = GEN_ALL(EQF_ELIM(SPEC_ALL(CONJUNCT1 LT)));;
 937
 938 let LESS_TRANS = LT_TRANS;;
 939
 940 let LESS_LEMMA1 = GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL(CONJUNCT2 LT))));;
 941
 942 let LESS_SUC_REFL = prove(`!n. n < SUC n`,REWRITE_TAC[LT]);;
 943
 944 let FACT_LESS = FACT_LT;;
 945
 946 let LESS_EQ_SUC_REFL = prove(`!n. n <= SUC n`,REWRITE_TAC[LE; LE_REFL]);;
 947
 948 let LESS_EQ_ADD = LE_ADD;;
 949
 950 let GREATER_EQ = GE;;
 951
 952 let LESS_EQUAL_ADD = GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL LE_EXISTS)));;
 953
 954 let LESS_EQ_IMP_LESS_SUC = GEN_ALL(snd(EQ_IMP_RULE(SPEC_ALL LT_SUC_LE)));;
 955
 956 let LESS_IMP_LESS_OR_EQ = LT_IMP_LE;;
 957
 958 let LESS_MONO_ADD = GEN_ALL(snd(EQ_IMP_RULE(SPEC_ALL LT_ADD_RCANCEL)));;
 959
 960 let LESS_SUC = prove(`!m n. m < n ==> m < (SUC n)`,MESON_TAC[LT]);;
 961
 962 let LESS_CASES = LTE_CASES;;
 963
 964 let LESS_EQ = GSYM LE_SUC_LT;;
 965
 966 let LESS_OR_EQ = LE_LT;;
 967
 968 let LESS_ADD_1 = GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL
 969     (REWRITE_RULE[ADD1] LT_EXISTS))));;
 970
 971 let SUC_SUB1 = ARITH_RULE `!m. SUC m - 1 = m`;;
 972
 973 let LESS_MONO_EQ = LT_SUC;;
 974
 975 let LESS_ADD_SUC = ARITH_RULE `!m n. m < m + SUC n`;;
 976
 977 let LESS_REFL = LT_REFL;;
 978
 979 let INV_SUC_EQ = SUC_INJ;;
 980
 981 let LESS_EQ_CASES = LE_CASES;;
 982
 983 let LESS_EQ_TRANS = LE_TRANS;;
 984
 985 let LESS_THM = CONJUNCT2 LT;;
 986
 987 let GREATER = GT;;
 988
 989 let LESS_EQ_0 = CONJUNCT1 LE;;
 990
 991 let OR_LESS = GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL LE_SUC_LT)));;
 992
 993 let SUB_EQUAL_0 = SUB_REFL;;
 994
 995 let SUB_MONO_EQ = SUB_SUC;;
 996
 997 let NOT_SUC_LESS_EQ = ARITH_RULE `!n m. ~(SUC n <= m) <=> m <= n`;;
 998
 999 let SUC_NOT = GSYM NOT_SUC;;
1000
1001 let LESS_LESS_CASES = ARITH_RULE `!m n:num. (m = n) \/ m < n \/ n < m`;;
1002
1003 let NOT_LESS_EQUAL = NOT_LE;;
1004
1005 let LESS_EQ_EXISTS = LE_EXISTS;;
1006
1007 let LESS_MONO_ADD_EQ = LT_ADD_RCANCEL;;
1008
1009 let LESS_LESS_EQ_TRANS = LTE_TRANS;;
1010
1011 let SUB_SUB = ARITH_RULE
1012   `!b c. c <= b ==> (!a:num. a - (b - c) = (a + c) - b)`;;
1013
1014 let LESS_CASES_IMP = ARITH_RULE
1015  `!m n:num. ~(m < n) /\ ~(m = n) ==> n < m`;;
1016
1017 let SUB_LESS_EQ = ARITH_RULE `!n m:num. (n - m) <= n`;;
1018
1019 let SUB_EQ_EQ_0 = ARITH_RULE `!m n:num. (m - n = m) = (m = 0) \/ (n = 0)`;;
1020
1021 let SUB_LEFT_LESS_EQ = ARITH_RULE
1022  `!m n p:num. m <= (n - p) <=> (m + p) <= n \/ m <= 0`;;
1023
1024 let SUB_LEFT_GREATER_EQ =
1025    ARITH_RULE `!m n p:num. m >= (n - p) <=> (m + p) >= n`;;
1026
1027 let LESS_EQ_LESS_TRANS = LET_TRANS;;
1028
1029 let LESS_0_CASES = ARITH_RULE `!m. (0 = m) \/ 0 < m`;;
1030
1031 let LESS_OR = ARITH_RULE `!m n. m < n ==> (SUC m) <= n`;;
1032
1033 let SUB = ARITH_RULE
1034    `(!m. 0 - m = 0) /\
1035     (!m n. (SUC m) - n = (if m < n then 0 else SUC(m - n)))`;;
1036
1037 let LESS_MULT_MONO = prove
1038  (`!m i n. ((SUC n) * m) < ((SUC n) * i) <=> m < i`,
1039   REWRITE_TAC[LT_MULT_LCANCEL; NOT_SUC]);;
1040
1041 let LESS_MONO_MULT = prove
1042  (`!m n p. m <= n ==> (m * p) <= (n * p)`,
1043   SIMP_TAC[LE_MULT_RCANCEL]);;
1044
1045 let LESS_MULT2 = prove
1046  (`!m n. 0 < m /\ 0 < n ==> 0 < (m * n)`,
1047   REWRITE_TAC[LT_MULT]);;
1048
1049 let SUBSET_FINITE = prove
1050  (`!s. FINITE s ==> (!t. t SUBSET s ==> FINITE t)`,
1051   MESON_TAC[FINITE_SUBSET]);;
1052
1053 let LESS_EQ_SUC = prove
1054  (`!n. m <= SUC n <=> (m = SUC n) \/ m <= n`,
1055   REWRITE_TAC[LE]);;
1056
1057 (* ------------------------------------------------------------------------- *)
1058 (* Restore traditional (low) parse status of "=".                            *)
1059 (* ------------------------------------------------------------------------- *)
1060
1061 parse_as_infix("=",(2,"right"));;