Jordan/tactics_ext2.ml

   1
   2 (* ------------------------------------------------------------------ *)
   3 (* MORE RECENT ADDITIONS *)
   4 (* ------------------------------------------------------------------ *)
   5
   6
   7
   8 (* abbrev_type copied from definitions_group.ml *)
   9
  10 let pthm = prove_by_refinement(
  11   `(\ (x:A) .T) (@(x:A). T)`,
  12   [BETA_TAC]);;
  13
  14 let abbrev_type ty s = let (a,b) = new_basic_type_definition s
  15    ("mk_"^s,"dest_"^s)
  16    (INST_TYPE [ty,`:A`] pthm) in
  17    let abst t = list_mk_forall ((frees t), t) in
  18    let a' = abst (concl a) in
  19    let b' = abst (rhs (concl b)) in
  20    (
  21    prove_by_refinement(a',[REWRITE_TAC[a]]),
  22    prove_by_refinement(b',[REWRITE_TAC[GSYM b]]));;
  23
  24
  25 (* ------------------------------------------------------------------ *)
  26 (* KILL IN *)
  27 (* ------------------------------------------------------------------ *)
  28
  29 let un = REWRITE_RULE[IN];;
  30
  31 (* ------------------------------------------------------------------ *)
  32
  33 let SUBCONJ_TAC =
  34   MATCH_MP_TAC (TAUT `A /\ (A ==>B) ==> (A /\ B)`) THEN CONJ_TAC;;
  35
  36 let PROOF_BY_CONTR_TAC =
  37   MATCH_MP_TAC (TAUT `(~A ==> F) ==> A`) THEN DISCH_TAC;;
  38
  39
  40
  41 (* ------------------------------------------------------------------ *)
  42 (* some general tactics *)
  43 (* ------------------------------------------------------------------ *)
  44
  45 (* before adding assumption to hypothesis list, cleanse it
  46    of unnecessary conditions *)
  47
  48
  49 let CLEAN_ASSUME_TAC th =
  50    MP_TAC th THEN ASM_REWRITE_TAC[] THEN DISCH_TAC;;
  51
  52 let CLEAN_THEN th ttac =
  53    MP_TAC th THEN ASM_REWRITE_TAC[] THEN DISCH_THEN ttac;;
  54
  55 (* looks for a hypothesis by matching a subterm *)
  56 let (UNDISCH_FIND_TAC: term -> tactic) =
  57  fun tm (asl,w) ->
  58    let p = can (term_match[] tm)  in
  59    try let sthm,_ = remove
  60      (fun (_,asm) -> can (find_term p) (concl ( asm))) asl in
  61      UNDISCH_TAC (concl (snd sthm)) (asl,w)
  62    with Failure _ -> failwith "UNDISCH_FIND_TAC";;
  63
  64 let (UNDISCH_FIND_THEN: term -> thm_tactic -> tactic) =
  65  fun tm ttac (asl,w) ->
  66    let p = can (term_match[] tm)  in
  67    try let sthm,_ = remove
  68      (fun (_,asm) -> can (find_term p) (concl ( asm))) asl in
  69      UNDISCH_THEN (concl (snd sthm)) ttac (asl,w)
  70    with Failure _ -> failwith "UNDISCH_FIND_TAC";;
  71
  72 (* ------------------------------------------------------------------ *)
  73 (* NAME_CONFLICT_TAC : eliminate name conflicts in a term *)
  74 (* ------------------------------------------------------------------ *)
  75
  76 let relabel_bound_conv tm =
  77  let rec vars_and_constants tm acc =
  78    match tm with
  79     | Var _ -> tm::acc
  80     | Const _ -> tm::acc
  81     | Comb(a,b) -> vars_and_constants b (vars_and_constants a acc)
  82     | Abs(a,b) -> a::(vars_and_constants b acc) in
  83  let relabel_bound tm =
  84    match tm with
  85     | Abs(x,t) ->
  86         let avoids = filter ((!=) x) (vars_and_constants tm []) in
  87         let x' = mk_primed_var avoids x in
  88         if (x=x') then failwith "relabel_bound" else (alpha x' tm)
  89     | _ -> failwith "relabel_bound" in
  90  DEPTH_CONV (fun t -> ALPHA t (relabel_bound t)) tm;;
  91
  92 (* example *)
  93 let _ =
  94   let bad_term = mk_abs (`x:bool`,`(x:num)+1=2`) in
  95   relabel_bound_conv bad_term;;
  96
  97 let NAME_CONFLICT_CONV = relabel_bound_conv;;
  98
  99 let NAME_CONFLICT_TAC =  CONV_TAC (relabel_bound_conv);;
 100
 101 (* renames  given bound variables *)
 102 let alpha_conv env tm = ALPHA tm (deep_alpha env tm);;
 103
 104 (* replaces given alpha-equivalent terms with- the term itself *)
 105 let unify_alpha_tac = SUBST_ALL_TAC o REFL;;
 106
 107 let rec get_abs tm acc = match tm with
 108    Abs(u,v) -> get_abs v (tm::acc)
 109   |Comb(u,v) -> get_abs u (get_abs v acc)
 110   |_ -> acc;;
 111
 112 (* for purposes such as sorting, it helps if ALL ALPHA-equiv
 113    abstractions are replaced by equal abstractions *)
 114 let (alpha_tac:tactic) =
 115   fun  (asl,w' ) ->
 116   EVERY (map unify_alpha_tac (get_abs w' [])) (asl,w');;
 117
 118 (* ------------------------------------------------------------------ *)
 119 (* SELECT ELIMINATION.
 120    SELECT_TAC should work whenever there is a single predicate selected.
 121    Something more sophisticated might be needed when there
 122    is (@)A and (@)B
 123    in the same formula.
 124    Useful for proving statements such as  `1 + (@x. (x=3)) = 4` *)
 125 (* ------------------------------------------------------------------ *)
 126
 127 (* spec form of SELECT_AX *)
 128 let select_thm select_fn select_exist =
 129   BETA_RULE (ISPECL [select_fn;select_exist]
 130              SELECT_AX);;
 131
 132 (* example *)
 133 select_thm
 134     `\m. (X:num->bool) m /\ (!n. X n ==> m <=| n)` `n:num`;;
 135
 136 let SELECT_EXIST = prove_by_refinement(
 137   `!(P:A->bool) Q. (?y. P y) /\ (!t. (P t ==> Q t)) ==> Q ((@) P)`,
 138   (* {{{ proof *)
 139
 140   [
 141   REPEAT GEN_TAC;
 142   DISCH_ALL_TAC;
 143   UNDISCH_FIND_TAC `(?)`;
 144   DISCH_THEN CHOOSE_TAC;
 145   ASSUME_TAC (ISPECL[`P:(A->bool)`;`y:A`] SELECT_AX);
 146   ASM_MESON_TAC[];
 147   ]);;
 148
 149   (* }}} *)
 150
 151 let SELECT_THM = prove_by_refinement(
 152   `!(P:A->bool) Q. (((?y. P y) ==> (!t. (P t ==> Q t))) /\ ((~(?y. P y)) ==>
 153      (!t. Q t))) ==> Q ((@) P)`,
 154   (* {{{ proof *)
 155   [
 156   MESON_TAC[SELECT_EXIST];
 157   ]);;
 158   (* }}} *)
 159
 160 let SELECT_TAC  =
 161   (* explicitly pull apart the clause Q((@) P),
 162      because MATCH_MP_TAC isn't powerful
 163      enough to do this by itself. *)
 164   let unbeta = prove(
 165   `!(P:A->bool) (Q:A->bool). (Q ((@) P)) <=> (\t. Q t) ((@) P)`,MESON_TAC[]) in
 166   let unbeta_tac = CONV_TAC (HIGHER_REWRITE_CONV[unbeta] true) in
 167   unbeta_tac THEN (MATCH_MP_TAC SELECT_THM) THEN BETA_TAC THEN CONJ_TAC
 168    THENL[
 169      (DISCH_THEN (fun t-> ALL_TAC)) THEN GEN_TAC;
 170      DISCH_TAC THEN GEN_TAC];;
 171
 172 (* EXAMPLE:
 173
 174 # g `(R:A->bool) ((@) S)`;;
 175 val it : Core.goalstack = 1 subgoal (1 total)
 176
 177 `R ((@) S)`
 178
 179 # e SELECT_TAC ;;
 180 val it : Core.goalstack = 2 subgoals (2 total)
 181
 182  0 [`~(?y. S y)`]
 183
 184 `R t`
 185
 186 `S t ==> R t`
 187
 188 *)
 189
 190
 191 (* ------------------------------------------------------------------ *)
 192 (* TYPE_THEN and TYPEL_THEN  calculate the types of the terms supplied
 193    in a proof, avoiding the hassle of working them out by hand.
 194    It locates the terms among the free variables in the goal.
 195    Ambiguious if a free variables have name conflicts.
 196
 197    Now TYPE_THEN handles general terms.
 198 *)
 199 (* ------------------------------------------------------------------ *)
 200
 201
 202 let rec type_set: (string*term) list  -> (term list*term) -> (term list*term)=
 203   fun typinfo (acclist,utm) -> match acclist with
 204     | [] -> (acclist,utm)
 205     | (Var(s,_) as a)::rest ->
 206          let a' = (assocd s typinfo a) in
 207            if (a = a') then type_set typinfo (rest,utm)
 208            else let inst = instantiate (term_match [] a a') in
 209              type_set typinfo ((map inst rest),inst utm)
 210     | _ -> failwith "type_set: variable expected"
 211   ;;
 212
 213 let has_stv t =
 214   let typ = (type_vars_in_term t) in
 215   can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;
 216
 217
 218 let TYPE_THEN: term  -> (term -> tactic) -> tactic =
 219   fun t (tac:term->tactic) (asl,w) ->
 220   let avoids = itlist (union o frees o concl o snd) asl
 221                                (frees w) in
 222   let strip  = fun t-> (match t with
 223        |Var(s,_) -> (s,t) | _ -> failwith "TYPE_THEN" ) in
 224   let typinfo = map strip avoids in
 225   let t' = (snd (type_set typinfo ((frees t),t))) in
 226     (warn ((has_stv t')) "TYPE_THEN: unresolved type variables");
 227     tac t' (asl,w);;
 228
 229 (* this version must take variables *)
 230 let TYPEL_THEN: term list -> (term list -> tactic) -> tactic =
 231   fun t (tac:term list->tactic) (asl,w) ->
 232   let avoids = itlist (union o frees o concl o snd) asl
 233                                (frees w) in
 234   let strip  = fun t-> (match t with
 235        |Var(s,_) -> (s,t) | _ -> failwith "TYPE_THEN" ) in
 236   let typinfo = map strip avoids in
 237   let t' = map (fun u -> snd (type_set typinfo ((frees u),u))) t in
 238     (warn ((can (find has_stv) t')) "TYPEL_THEN: unresolved type vars");
 239      tac t' (asl,w);;
 240
 241 (* trivial example *)
 242
 243 let _ = prove_by_refinement(`!y. y:num = y`,
 244  [
 245    GEN_TAC;
 246    TYPE_THEN `y:A` (fun t -> ASSUME_TAC(ISPEC t (TAUT `!x:B. x=x`)));
 247    UNDISCH_TAC `y:num = y`; (* evidence that `y:A` was retyped as `y:num` *)
 248    MESON_TAC[];
 249  ]);;
 250
 251
 252 (* ------------------------------------------------------------------ *)
 253 (* SAVE the goalstate, and retrieve later *)
 254 (* ------------------------------------------------------------------ *)
 255
 256 let (save_goal,get_goal) =
 257   let goal_buffer  = ref [] in
 258   let save_goal s =
 259      goal_buffer := (s,!current_goalstack )::!goal_buffer in
 260   let get_goal (s:string) = (current_goalstack:= assoc s !goal_buffer) in
 261   (save_goal,get_goal);;
 262
 263
 264 (* ------------------------------------------------------------------ *)
 265 (* ordered rewrites with general ord function .
 266    This allows rewrites with an arbitrary condition
 267     -- adapted from simp.ml *)
 268 (* ------------------------------------------------------------------ *)
 269
 270
 271
 272 let net_of_thm_ord ord rep force th =
 273   let t = concl th in
 274   let lconsts = freesl (hyp th) in
 275   let matchable = can o term_match lconsts in
 276   try let l,r = dest_eq t in
 277       if rep & free_in l r then
 278        let th' = EQT_INTRO th in
 279        enter lconsts (l,(1,REWR_CONV th'))
 280       else if rep & matchable l r & matchable r l then
 281         enter lconsts (l,(1,ORDERED_REWR_CONV ord th))
 282       else if force then
 283         enter lconsts (l,(1,ORDERED_REWR_CONV ord th))
 284       else enter lconsts (l,(1,REWR_CONV th))
 285   with Failure _ ->
 286       let l,r = dest_eq(rand t) in
 287       if rep & free_in l r then
 288        let tm = lhand t in
 289        let th' = DISCH tm (EQT_INTRO(UNDISCH th)) in
 290        enter lconsts (l,(3,IMP_REWR_CONV th'))
 291       else if rep &  matchable l r & matchable r l then
 292         enter lconsts (l,(3,ORDERED_IMP_REWR_CONV ord th))
 293       else enter lconsts(l,(3,IMP_REWR_CONV th));;
 294
 295 let GENERAL_REWRITE_ORD_CONV ord rep force (cnvl:conv->conv) (builtin_net:gconv net) thl =
 296   let thl_canon = itlist (mk_rewrites false) thl [] in
 297   let final_net = itlist (net_of_thm_ord ord rep force ) thl_canon builtin_net in
 298   cnvl (REWRITES_CONV final_net);;
 299
 300 let GEN_REWRITE_ORD_CONV ord force (cnvl:conv->conv) thl =
 301   GENERAL_REWRITE_ORD_CONV ord false force cnvl empty_net thl;;
 302
 303 let PURE_REWRITE_ORD_CONV ord force thl =
 304   GENERAL_REWRITE_ORD_CONV ord true force TOP_DEPTH_CONV empty_net thl;;
 305
 306 let REWRITE_ORD_CONV ord force thl =
 307   GENERAL_REWRITE_ORD_CONV ord true force TOP_DEPTH_CONV (basic_net()) thl;;
 308
 309 let PURE_ONCE_REWRITE_ORD_CONV ord force thl =
 310   GENERAL_REWRITE_ORD_CONV ord false force ONCE_DEPTH_CONV empty_net thl;;
 311
 312 let ONCE_REWRITE_ORD_CONV ord force thl =
 313   GENERAL_REWRITE_ORD_CONV ord false force ONCE_DEPTH_CONV (basic_net()) thl;;
 314
 315 let REWRITE_ORD_TAC ord force thl = CONV_TAC(REWRITE_ORD_CONV ord force thl);;
 316
 317
 318
 319
 320 (* ------------------------------------------------------------------ *)
 321 (* poly reduction *)
 322 (* ------------------------------------------------------------------ *)
 323
 324
 325 (* move vars  leftward *)
 326 (* if ord old_lhs new_rhs THEN swap *)
 327
 328
 329 let new_factor_order t1 t2 =
 330   try let t1v = fst(dest_binop `( *. )` t1) in
 331       let t2v = fst(dest_binop `( *. )` t2) in
 332   if (is_var t1v) & (is_var t2v) then term_order t1v t2v
 333   else if (is_var t2v) then true else false
 334   with Failure _  -> false ;;
 335
 336 (* false if it contains a variable or abstraction. *)
 337 let rec is_arith_const tm =
 338   if is_var tm then false else
 339   if is_abs tm then false else
 340   if is_comb tm then
 341      let (a,b) = (dest_comb tm) in
 342      is_arith_const (a) & is_arith_const (b)
 343   else true;;
 344
 345 (* const leftward *)
 346 let new_factor_order2 t1 t2 =
 347   try let t1v = fst(dest_binop `( *. )` t1) in
 348       let t2v = fst(dest_binop `( *. )` t2) in
 349   if (is_var t1v) & (is_var t2v) then term_order t1v t2v
 350   else if (is_arith_const t2v) then true else false
 351   with Failure _  -> false ;;
 352
 353 let rec mon_sz tm =
 354   if is_var tm then
 355     Int (Hashtbl.hash tm)
 356   else
 357   try let (a,b) = dest_binop `( *. )` tm in
 358     (mon_sz a) */ (mon_sz b)
 359   with Failure _ -> Int 1;;
 360
 361 let rec new_summand_order t1 t2 =
 362   try let t1v = fst(dest_binop `( +. )` t1) in
 363       let t2v = fst(dest_binop `( +. )` t2) in
 364   (mon_sz t2v >/ mon_sz t1v)
 365   with Failure _  -> false ;;
 366
 367 let rec new_distrib_order t1 t2 =
 368   try let t2v = fst(dest_binop `( *. )` t2) in
 369   if (is_arith_const t2v) then true else false
 370   with Failure _  ->
 371     try
 372       let t2' = fst(dest_binop `( +. )` t2) in
 373       new_distrib_order t1 t2'
 374     with Failure _ -> false ;;
 375
 376 let real_poly_conv =
 377   (* same side *)
 378   ONCE_REWRITE_CONV [GSYM REAL_SUB_0] THENC
 379   (* expand ALL *)
 380   REWRITE_CONV[real_div;REAL_RDISTRIB;REAL_SUB_RDISTRIB;
 381   pow;
 382   GSYM REAL_MUL_ASSOC;GSYM REAL_ADD_ASSOC;
 383    REAL_ARITH `(x -. (--y) = x + y) /\ (x - y = x + (-- y)) /\
 384                (--(x + y) = --x + (--y)) /\ (--(x - y) = --x + y)`;
 385    REAL_ARITH
 386        `(x*.(-- y) = -- (x*. y)) /\ (--. (--. x) = x) /\
 387        ((--. x)*.y = --.(x*.y))`;
 388          REAL_SUB_LDISTRIB;REAL_LDISTRIB] THENC
 389   (* move constants rightward on monomials *)
 390    REWRITE_ORD_CONV new_factor_order false [REAL_MUL_AC;] THENC
 391    GEN_REWRITE_CONV ONCE_DEPTH_CONV
 392            [REAL_ARITH `-- x = (x*(-- &.1))`] THENC
 393    REWRITE_CONV[GSYM REAL_MUL_ASSOC] THENC
 394    REAL_RAT_REDUCE_CONV THENC
 395    (* collect like monomials *)
 396    REWRITE_ORD_CONV new_summand_order false [REAL_ADD_AC;] THENC
 397    (* move constants leftward AND collect them together *)
 398    REWRITE_ORD_CONV new_factor_order2 false [REAL_MUL_AC;] THENC
 399    REWRITE_ORD_CONV new_distrib_order true [
 400         REAL_ARITH `(a*b +. d*b = (a+d)*b) /\
 401              (a*b + b = (a+ &.1)*b ) /\ ( b + a*b = (a+ &.1)*b) /\
 402              (a*b +. d*b +e = (a+d)*b + e) /\
 403              (a*b + b + e= (a+. &.1)* b +e ) /\
 404              ( b + a*b + e = (a + &.1)*b +e) `;] THENC
 405    REAL_RAT_REDUCE_CONV THENC
 406    REWRITE_CONV[REAL_ARITH `(&.0 * x = &.0) /\ (x + &.0 = x) /\
 407               (&.0 + x = x)`];;
 408
 409 let real_poly_tac = CONV_TAC real_poly_conv;;
 410
 411 let test_real_poly_tac = prove_by_refinement(
 412   `!x y . (x + (&.2)*y)*(x- (&.2)*y) = (x*x -. (&.4)*y*y)`,
 413   (* {{{ proof *)
 414   [
 415   DISCH_ALL_TAC;
 416   real_poly_tac;
 417   ]);;
 418   (* }}} *)
 419
 420
 421
 422
 423 (* ------------------------------------------------------------------ *)
 424 (* REAL INEQUALITIES *)
 425
 426
 427 (* Take inequality certificate A + B1 + B2 +.... + P = C as a term.
 428    Prove it as an inequality.
 429    Reduce to an ineq (A < C) WITH side conditions
 430       0 <= Bi,  0 < P.
 431
 432    If (not strict), write as an ineq (A <= C) WITH side conditions
 433       0 <= Bi.
 434
 435    Expand each Bi (or P) that is a product U*V as 0 <= U /\ 0 <= V.
 436    To prevent expansion of Bi write (U*V) as (&0 + (U*V)).
 437
 438    CALL as
 439    ineq_le_tac `A + B1 + B2 = C`;
 440
 441    *)
 442 (* ------------------------------------------------------------------ *)
 443
 444
 445 let strict_lemma = prove_by_refinement(
 446   `!A B C. (A+B = C) ==> ((&.0 <. B) ==> (A <. C)  )`,
 447   (* {{{ proof *)
 448   [
 449   REAL_ARITH_TAC;
 450   ]);;
 451   (* }}} *)
 452
 453 let weak_lemma = prove_by_refinement(
 454   `!A B C. (A+B = C) ==> ((&.0 <=. B) ==> (A <=. C))`,
 455   (* {{{ proof *)
 456   [
 457   REAL_ARITH_TAC;
 458   ]);;
 459   (* }}} *)
 460
 461 let strip_lt_lemma = prove_by_refinement(
 462   `!B1 B2 C. ((&.0 <. (B1+B2)) ==> C) ==>
 463          ((&.0 <. B2) ==> ((&.0 <=. B1) ==> C))`,
 464   (* {{{ proof *)
 465   [
 466   ASM_MESON_TAC[REAL_LET_ADD];
 467   ]);;
 468   (* }}} *)
 469
 470 let strip_le_lemma = prove_by_refinement(
 471   `!B1 B2 C. ((&.0 <=. (B1+B2)) ==> C) ==>
 472          ((&.0 <=. B2) ==> ((&.0 <=. B1) ==> C))`,
 473   (* {{{ proof *)
 474   [
 475   ASM_MESON_TAC[REAL_LE_ADD];
 476   ]);;
 477   (* }}} *)
 478
 479 let is_x_prod_le tm =
 480   try let hyp = fst(dest_binop `( ==> )` tm) in
 481       let arg = snd(dest_binop `( <=. ) ` hyp) in
 482       let fac = dest_binop `( *. )` arg in
 483   true
 484   with Failure _ -> false;;
 485
 486 let switch_lemma_le_order t1 t2 =
 487   if (is_x_prod_le t1) & (is_x_prod_le t2) then
 488   term_order t1 t2 else
 489   if (is_x_prod_le t2) then true else false;;
 490
 491 let is_x_prod_lt tm =
 492   try let hyp = fst(dest_binop `( ==> )` tm) in
 493       let arg = snd(dest_binop `( <. ) ` hyp) in
 494       let fac = dest_binop `( *. )` arg in
 495   true
 496   with Failure _ -> false;;
 497
 498 let switch_lemma_lt_order t1 t2 =
 499   if (is_x_prod_lt t1) & (is_x_prod_lt t2) then
 500   term_order t1 t2 else
 501   if (is_x_prod_lt t2) then true else false;;
 502
 503 let switch_lemma_le = prove_by_refinement(
 504   `!A B C. ((&.0 <= A) ==> (&.0 <= B) ==> C) =
 505        ((&.0 <=. B) ==> (&.0 <= A) ==> C)`,
 506   (* {{{ proof *)
 507   [
 508   ASM_MESON_TAC[];
 509   ]);;
 510   (* }}} *)
 511
 512 let switch_lemma_let = prove_by_refinement(
 513   `!A B C. ((&.0 < A) ==> (&.0 <= B) ==> C) =
 514        ((&.0 <=. B) ==> (&.0 < A) ==> C)`,
 515   (* {{{ proof *)
 516   [
 517   ASM_MESON_TAC[];
 518   ]);;
 519   (* }}} *)
 520
 521 let switch_lemma_lt = prove_by_refinement(
 522   `!A B C. ((&.0 < A) ==> (&.0 < B) ==> C) =
 523        ((&.0 <. B) ==> (&.0 < A)  ==> C)`,
 524   (* {{{ proof *)
 525   [
 526   ASM_MESON_TAC[];
 527   ]);;
 528   (* }}} *)
 529
 530 let expand_prod_lt = prove_by_refinement(
 531   `!B1 B2 C. (&.0 < B1*B2 ==> C) ==>
 532               ((&.0 <. B1) ==> (&.0 <. B2) ==> C)`,
 533   (* {{{ proof *)
 534   [
 535   ASM_MESON_TAC[REAL_LT_MUL ];
 536   ]);;
 537   (* }}} *)
 538
 539 let expand_prod_le = prove_by_refinement(
 540   `!B1 B2 C. (&.0 <= B1*B2 ==> C) ==>
 541               ((&.0 <=. B1) ==> (&.0 <=. B2) ==> C)`,
 542   (* {{{ proof *)
 543   [
 544   ASM_MESON_TAC[REAL_LE_MUL ];
 545   ]);;
 546   (* }}} *)
 547
 548
 549 let ineq_cert_gen_tac v cert =
 550   let DISCH_RULE f = DISCH_THEN (fun t-> MP_TAC (f t)) in
 551   TYPE_THEN cert
 552      (MP_TAC o (REWRITE_CONV[REAL_POW_2] THENC real_poly_conv)) THEN
 553   REWRITE_TAC[] THEN
 554   DISCH_RULE (MATCH_MP v) THEN
 555   DISCH_RULE (repeat (MATCH_MP strip_lt_lemma)) THEN
 556   DISCH_RULE (repeat (MATCH_MP strip_le_lemma)) THEN
 557   DISCH_RULE (repeat (MATCH_MP expand_prod_lt o
 558         (CONV_RULE
 559    (REWRITE_ORD_CONV switch_lemma_lt_order true[switch_lemma_lt])))) THEN
 560   DISCH_RULE (repeat (MATCH_MP expand_prod_le o
 561         (CONV_RULE (REWRITE_ORD_CONV switch_lemma_le_order true
 562                     [switch_lemma_le])) o
 563       (REWRITE_RULE[switch_lemma_let]))) THEN
 564   DISCH_RULE (repeat (MATCH_MP
 565         (TAUT `(A ==> B==>C) ==> (A /\ B ==> C)`))) THEN
 566   REWRITE_TAC[REAL_MUL_LID] THEN
 567   DISCH_THEN MATCH_MP_TAC THEN
 568   CONV_TAC  REAL_RAT_REDUCE_CONV THEN
 569   ASM_SIMP_TAC[REAL_LE_POW_2;
 570      REAL_ARITH `(&.0 < x ==> &.0 <= x) /\ (&.0 + x = x) /\
 571           (a <= b ==> &.0 <= b - a) /\
 572           (a < b ==> &.0 <= b - a) /\
 573           (~(b < a) ==> &.0 <= b - a) /\
 574           (~(b <= a) ==> &.0 <= b - a) /\
 575           (a < b ==> &.0 < b - a) /\
 576           (~(b <= a) ==> &.0 < b - a)`];;
 577
 578 let ineq_lt_tac = ineq_cert_gen_tac strict_lemma;;
 579 let ineq_le_tac = ineq_cert_gen_tac weak_lemma;;
 580
 581
 582
 583 (* test *)
 584 let test_ineq_tac  = prove_by_refinement(
 585   `!x y z. (&.0 <= x*y) /\ (&.0 <. z) ==>
 586              (x*y)  <. x*x + (&.3)*x*y + &.4 `,
 587   (* {{{ proof *)
 588   [
 589   DISCH_ALL_TAC;
 590   ineq_lt_tac `x * y + x pow 2 + &2 * (&.0 + x * y) + &2 * &2 = x * x + &3 * x * y + &4`;
 591   ]);;
 592   (* }}} *)
 593
 594
 595
 596 (* ------------------------------------------------------------------ *)
 597 (* Move quantifier left. Use class.ml and theorems.ml to bubble
 598    quantifiers towards the head of an expression.  It should move
 599    quantifiers past other quantifiers, past conjunctions, disjunctions,
 600    implications, etc.
 601
 602    val quant_left_CONV : string -> term -> thm = <fun>
 603    Arguments:
 604    var_name:string  -- The name of the variable that is to be shifted.
 605
 606    It tends to return `T` when the conversion fails.
 607
 608    Example:
 609    quant_left_CONV "a" `!b. ?a. a = b*4`;;
 610    val it : thm = |- (!b. ?a. a = b *| 4) <=> (?a. !b. a b = b *| 4)
 611    *)
 612 (* ------------------------------------------------------------------ *)
 613
 614 let tagb = new_definition `TAGB (x:bool) = x`;;
 615
 616 let is_quant tm = (is_forall tm) or (is_exists tm);;
 617
 618 (*** JRH replaced Comb and Abs with abstract type constructors ***)
 619
 620 let rec tag_quant var_name tm =
 621   if (is_forall tm && (fst (dest_var (fst (dest_forall tm))) = var_name))
 622   then mk_comb (`TAGB`,tm)
 623   else if (is_exists tm && (fst (dest_var (fst (dest_exists tm))) = var_name))   then mk_comb (`TAGB`,tm)
 624   else match tm with
 625      | Comb (x,y) -> mk_comb(tag_quant var_name x,tag_quant var_name y)
 626      | Abs (x,y) -> mk_abs(x,tag_quant var_name y)
 627      | _ -> tm;;
 628
 629 let quant_left_CONV  =
 630   (* ~! -> ?~ *)
 631   let iprove f = prove(f,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 632   let NOT_FORALL_TAG = prove(`!P. ~(TAGB(!x. P x)) <=> (?x:A. ~(P x))`,
 633                              REWRITE_TAC[tagb;NOT_FORALL_THM]) in
 634  let SKOLEM_TAG =
 635   prove(`!P. (?y. TAGB (!(x:A). P x ((y:A->B) x))) <=>
 636      ( (!(x:A). ?y. P x ((y:B))))`,REWRITE_TAC[tagb;SKOLEM_THM]) in
 637  let SKOLEM_TAG2 =
 638    prove(`!P. (!x:A. TAGB(?y:B. P x y)) <=> (?y. !x. P x (y x))`,
 639          REWRITE_TAC[tagb;SKOLEM_THM]) in
 640  (* !1 !2 -> !2 !1 *)
 641  let SWAP_FORALL_TAG =
 642   prove(`!P:A->B->bool. (!x. TAGB(! y. P x y)) <=> (!y x. P x y)`,
 643     REWRITE_TAC[SWAP_FORALL_THM;tagb]) in
 644  let SWAP_EXISTS_THM = iprove
 645   `!P:A->B->bool. (?x. TAGB (?y. P x y)) <=> (?y x. P x y)` in
 646  (* ! /\ ! -> ! /\ *)
 647  let AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\ TAGB (!x. Q x) <=>
 648    (!x. P x /\ Q x))`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 649  let LEFT_AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\  Q) <=>
 650    (!x. P x /\ Q )`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 651  let RIGHT_AND_FORALL_TAG = prove(`!P Q. P /\ TAGB (!x. Q x) <=>
 652    (!x. P  /\ Q x)`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 653  let TRIV_OR_FORALL_TAG = prove
 654  (`!P Q. TAGB (!x:A. P) \/ TAGB (!x:A. Q) <=> (!x:A. P \/ Q)`,
 655   REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 656  let RIGHT_IMP_FORALL_TAG = prove
 657  (`!P Q. (P ==> TAGB (!x:A. Q x)) <=> (!x. P ==> Q x)`,
 658   REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 659  let OR_EXISTS_THM = iprove
 660   `!P Q. TAGB (?x. P x) \/ TAGB (?x. Q x) <=> (?x:A. P x \/ Q x)` in
 661  let LEFT_OR_EXISTS_THM = iprove
 662  `!P Q. TAGB (?x. P x) \/ Q <=> (?x:A. P x \/ Q)` in
 663  let RIGHT_OR_EXISTS_THM = iprove
 664  `!P Q. P \/ TAGB (?x. Q x) <=> (?x:A. P \/ Q x)` in
 665  let LEFT_AND_EXISTS_THM = iprove
 666  `!P Q. TAGB (?x:A. P x) /\ Q <=> (?x:A. P x /\ Q)` in
 667  let RIGHT_AND_EXISTS_THM = iprove
 668  `!P Q. P /\ TAGB (?x:A. Q x) <=> (?x:A. P /\ Q x)` in
 669  let TRIV_AND_EXISTS_THM = iprove
 670  `!P Q. TAGB (?x:A. P) /\ TAGB (?x:A. Q) <=> (?x:A. P /\ Q)` in
 671  let LEFT_IMP_EXISTS_THM = iprove
 672  `!P Q. (TAGB (?x:A. P x) ==> Q) <=> (!x. P x ==> Q)` in
 673  let TRIV_FORALL_IMP_THM = iprove
 674  `!P Q. (TAGB (?x:A. P) ==> TAGB (!x:A. Q)) <=> (!x:A. P ==> Q) ` in
 675  let TRIV_EXISTS_IMP_THM = iprove
 676  `!P Q. (TAGB(!x:A. P) ==> TAGB (?x:A. Q)) <=> (?x:A. P ==> Q) ` in
 677  let NOT_EXISTS_TAG = prove(
 678  `!P. ~(TAGB(?x:A. P x)) <=> (!x. ~(P x))`,
 679  REWRITE_TAC[tagb;NOT_EXISTS_THM]) in
 680  let LEFT_OR_FORALL_TAG = prove
 681  (`!P Q. TAGB(!x:A. P x) \/ Q <=> (!x. P x \/ Q)`,
 682  REWRITE_TAC[tagb;LEFT_OR_FORALL_THM]) in
 683  let RIGHT_OR_FORALL_TAG = prove
 684  (`!P Q. P \/ TAGB(!x:A. Q x) <=> (!x. P \/ Q x)`,
 685   REWRITE_TAC[tagb;RIGHT_OR_FORALL_THM]) in
 686  let LEFT_IMP_FORALL_TAG = prove
 687  (`!P Q. (TAGB(!x:A. P x) ==> Q) <=> (?x. P x ==> Q)`,
 688  REWRITE_TAC[tagb;LEFT_IMP_FORALL_THM]) in
 689  let RIGHT_IMP_EXISTS_TAG = prove
 690  (`!P Q. (P ==> TAGB(?x:A. Q x)) <=> (?x:A. P ==> Q x)`,
 691  REWRITE_TAC[tagb;RIGHT_IMP_EXISTS_THM]) in
 692   fun var_name tm ->
 693      REWRITE_RULE [tagb]
 694        (TOP_SWEEP_CONV
 695        (GEN_REWRITE_CONV I
 696          [NOT_FORALL_TAG;SKOLEM_TAG;SKOLEM_TAG2;
 697           SWAP_FORALL_TAG;SWAP_EXISTS_THM;
 698           SWAP_EXISTS_THM;
 699           AND_FORALL_TAG;LEFT_AND_FORALL_TAG;RIGHT_AND_FORALL_TAG;
 700           TRIV_OR_FORALL_TAG;RIGHT_IMP_FORALL_TAG;
 701           OR_EXISTS_THM;LEFT_OR_EXISTS_THM;RIGHT_OR_EXISTS_THM;
 702           LEFT_AND_EXISTS_THM;
 703           RIGHT_AND_EXISTS_THM;
 704           TRIV_AND_EXISTS_THM;LEFT_IMP_EXISTS_THM;TRIV_FORALL_IMP_THM;
 705           TRIV_EXISTS_IMP_THM;NOT_EXISTS_TAG;
 706           LEFT_OR_FORALL_TAG;RIGHT_OR_FORALL_TAG;LEFT_IMP_FORALL_TAG;
 707           RIGHT_IMP_EXISTS_TAG;
 708          ])
 709        (tag_quant var_name tm));;
 710
 711 (* same, but never pass a quantifier past another. No Skolem, etc. *)
 712 let quant_left_noswap_CONV  =
 713   (* ~! -> ?~ *)
 714   let iprove f = prove(f,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 715   let NOT_FORALL_TAG = prove(`!P. ~(TAGB(!x. P x)) <=> (?x:A. ~(P x))`,
 716                              REWRITE_TAC[tagb;NOT_FORALL_THM]) in
 717  let SKOLEM_TAG =
 718   prove(`!P. (?y. TAGB (!(x:A). P x ((y:A->B) x))) <=>
 719      ( (!(x:A). ?y. P x ((y:B))))`,REWRITE_TAC[tagb;SKOLEM_THM]) in
 720  let SKOLEM_TAG2 =
 721    prove(`!P. (!x:A. TAGB(?y:B. P x y)) <=> (?y. !x. P x (y x))`,
 722          REWRITE_TAC[tagb;SKOLEM_THM]) in
 723  (* !1 !2 -> !2 !1 *)
 724  let SWAP_FORALL_TAG =
 725   prove(`!P:A->B->bool. (!x. TAGB(! y. P x y)) <=> (!y x. P x y)`,
 726     REWRITE_TAC[SWAP_FORALL_THM;tagb]) in
 727  let SWAP_EXISTS_THM = iprove
 728   `!P:A->B->bool. (?x. TAGB (?y. P x y)) <=> (?y x. P x y)` in
 729  (* ! /\ ! -> ! /\ *)
 730  let AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\ TAGB (!x. Q x) <=>
 731    (!x. P x /\ Q x))`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 732  let LEFT_AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\  Q) <=>
 733    (!x. P x /\ Q )`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 734  let RIGHT_AND_FORALL_TAG = prove(`!P Q. P /\ TAGB (!x. Q x) <=>
 735    (!x. P  /\ Q x)`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 736  let TRIV_OR_FORALL_TAG = prove
 737  (`!P Q. TAGB (!x:A. P) \/ TAGB (!x:A. Q) <=> (!x:A. P \/ Q)`,
 738   REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 739  let RIGHT_IMP_FORALL_TAG = prove
 740  (`!P Q. (P ==> TAGB (!x:A. Q x)) <=> (!x. P ==> Q x)`,
 741   REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 742  let OR_EXISTS_THM = iprove
 743   `!P Q. TAGB (?x. P x) \/ TAGB (?x. Q x) <=> (?x:A. P x \/ Q x)` in
 744  let LEFT_OR_EXISTS_THM = iprove
 745  `!P Q. TAGB (?x. P x) \/ Q <=> (?x:A. P x \/ Q)` in
 746  let RIGHT_OR_EXISTS_THM = iprove
 747  `!P Q. P \/ TAGB (?x. Q x) <=> (?x:A. P \/ Q x)` in
 748  let LEFT_AND_EXISTS_THM = iprove
 749  `!P Q. TAGB (?x:A. P x) /\ Q <=> (?x:A. P x /\ Q)` in
 750  let RIGHT_AND_EXISTS_THM = iprove
 751  `!P Q. P /\ TAGB (?x:A. Q x) <=> (?x:A. P /\ Q x)` in
 752  let TRIV_AND_EXISTS_THM = iprove
 753  `!P Q. TAGB (?x:A. P) /\ TAGB (?x:A. Q) <=> (?x:A. P /\ Q)` in
 754  let LEFT_IMP_EXISTS_THM = iprove
 755  `!P Q. (TAGB (?x:A. P x) ==> Q) <=> (!x. P x ==> Q)` in
 756  let TRIV_FORALL_IMP_THM = iprove
 757  `!P Q. (TAGB (?x:A. P) ==> TAGB (!x:A. Q)) <=> (!x:A. P ==> Q) ` in
 758  let TRIV_EXISTS_IMP_THM = iprove
 759  `!P Q. (TAGB(!x:A. P) ==> TAGB (?x:A. Q)) <=> (?x:A. P ==> Q) ` in
 760  let NOT_EXISTS_TAG = prove(
 761  `!P. ~(TAGB(?x:A. P x)) <=> (!x. ~(P x))`,
 762  REWRITE_TAC[tagb;NOT_EXISTS_THM]) in
 763  let LEFT_OR_FORALL_TAG = prove
 764  (`!P Q. TAGB(!x:A. P x) \/ Q <=> (!x. P x \/ Q)`,
 765  REWRITE_TAC[tagb;LEFT_OR_FORALL_THM]) in
 766  let RIGHT_OR_FORALL_TAG = prove
 767  (`!P Q. P \/ TAGB(!x:A. Q x) <=> (!x. P \/ Q x)`,
 768   REWRITE_TAC[tagb;RIGHT_OR_FORALL_THM]) in
 769  let LEFT_IMP_FORALL_TAG = prove
 770  (`!P Q. (TAGB(!x:A. P x) ==> Q) <=> (?x. P x ==> Q)`,
 771  REWRITE_TAC[tagb;LEFT_IMP_FORALL_THM]) in
 772  let RIGHT_IMP_EXISTS_TAG = prove
 773  (`!P Q. (P ==> TAGB(?x:A. Q x)) <=> (?x:A. P ==> Q x)`,
 774  REWRITE_TAC[tagb;RIGHT_IMP_EXISTS_THM]) in
 775   fun var_name tm ->
 776      REWRITE_RULE [tagb]
 777        (TOP_SWEEP_CONV
 778        (GEN_REWRITE_CONV I
 779          [NOT_FORALL_TAG; (* SKOLEM_TAG;SKOLEM_TAG2; *)
 780           (* SWAP_FORALL_TAG;SWAP_EXISTS_THM;
 781           SWAP_EXISTS_THM; *)
 782           AND_FORALL_TAG;LEFT_AND_FORALL_TAG;RIGHT_AND_FORALL_TAG;
 783           TRIV_OR_FORALL_TAG;RIGHT_IMP_FORALL_TAG;
 784           OR_EXISTS_THM;LEFT_OR_EXISTS_THM;RIGHT_OR_EXISTS_THM;
 785           LEFT_AND_EXISTS_THM;
 786           RIGHT_AND_EXISTS_THM;
 787           TRIV_AND_EXISTS_THM;LEFT_IMP_EXISTS_THM;TRIV_FORALL_IMP_THM;
 788           TRIV_EXISTS_IMP_THM;NOT_EXISTS_TAG;
 789           LEFT_OR_FORALL_TAG;RIGHT_OR_FORALL_TAG;LEFT_IMP_FORALL_TAG;
 790           RIGHT_IMP_EXISTS_TAG;
 791          ])
 792        (tag_quant var_name tm));;
 793
 794 let quant_right_CONV  =
 795   (* ~! -> ?~ *)
 796   let iprove f = prove(f,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 797   let NOT_FORALL_TAG = prove(`!P. TAGB(?x:A. ~(P x)) <=> ~((!x. P x))`,
 798                              REWRITE_TAC[tagb;GSYM NOT_FORALL_THM]) in
 799  let SKOLEM_TAG =
 800   prove(`!P. ( TAGB(!(x:A). ?y. P x ((y:B)))) <=>
 801    (?y.  (!(x:A). P x ((y:A->B) x)))`,
 802    REWRITE_TAC[tagb;GSYM SKOLEM_THM])
 803    in
 804  let SKOLEM_TAG2 =
 805    prove(`!P. TAGB(?y. !x. P x (y x)) <=> (!x:A. (?y:B. P x y))`,
 806          REWRITE_TAC[tagb;GSYM SKOLEM_THM]) in
 807  (* !1 !2 -> !2 !1.. *)
 808  let SWAP_FORALL_TAG =
 809   prove(`!P:A->B->bool.  TAGB(!y x. P x y) <=> (!x. (! y. P x y))`,
 810     REWRITE_TAC[GSYM SWAP_FORALL_THM;tagb]) in
 811  let SWAP_EXISTS_THM = iprove
 812   `!P:A->B->bool.  TAGB (?y x. P x y) <=> (?x. (?y. P x y))` in
 813  (* ! /\ ! -> ! /\ *)
 814  let AND_FORALL_TAG = iprove`!P Q. TAGB(!x. P x /\ Q x) <=>
 815    ((!x. P x) /\ (!x. Q x))` in
 816  let LEFT_AND_FORALL_TAG = prove(`!P Q.
 817    TAGB(!x. P x /\ Q ) <=> ((!x. P x) /\  Q)`,
 818    REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 819  let RIGHT_AND_FORALL_TAG = prove(`!P Q.
 820    TAGB(!x. P  /\ Q x) <=> P /\  (!x. Q x)`,
 821    REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 822  let TRIV_OR_FORALL_TAG = prove
 823  (`!P Q.   TAGB(!x:A. P \/ Q) <=>(!x:A. P) \/  (!x:A. Q)`,
 824   REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 825  let RIGHT_IMP_FORALL_TAG = prove
 826  (`!P Q. TAGB (!x. P ==> Q x) <=> (P ==>  (!x:A. Q x)) `,
 827   REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 828  let OR_EXISTS_THM = iprove
 829   `!P Q.  TAGB(?x:A. P x \/ Q x) <=> (?x. P x) \/ (?x. Q x) ` in
 830  let LEFT_OR_EXISTS_THM = iprove
 831  `!P Q. TAGB (?x:A. P x \/ Q) <=>  (?x. P x) \/ Q ` in
 832  let RIGHT_OR_EXISTS_THM = iprove
 833  `!P Q.TAGB (?x:A. P \/ Q x) <=>  P \/ (?x. Q x)` in
 834  let LEFT_AND_EXISTS_THM = iprove
 835  `!P Q.TAGB (?x:A. P x /\ Q) <=>  (?x:A. P x) /\ Q` in
 836  let RIGHT_AND_EXISTS_THM = iprove
 837  `!P Q. TAGB (?x:A. P /\ Q x) <=>  P /\ (?x:A. Q x) ` in
 838  let TRIV_AND_EXISTS_THM = iprove
 839  `!P Q. TAGB(?x:A. P /\ Q) <=>  (?x:A. P) /\  (?x:A. Q) ` in (* *)
 840  let LEFT_IMP_EXISTS_THM = iprove
 841  `!P Q. TAGB(!x. P x ==> Q) <=> ( (?x:A. P x) ==> Q) ` in (* *)
 842  let TRIV_FORALL_IMP_THM = iprove
 843  `!P Q. TAGB(!x:A. P ==> Q)  <=> ( (?x:A. P) ==>  (!x:A. Q)) ` in
 844  let TRIV_EXISTS_IMP_THM = iprove
 845  `!P Q. TAGB(?x:A. P ==> Q)  <=> ((!x:A. P) ==>  (?x:A. Q)) ` in
 846  let NOT_EXISTS_TAG = prove(
 847  `!P. TAGB(!x. ~(P x)) <=> ~((?x:A. P x)) `,
 848  REWRITE_TAC[tagb;NOT_EXISTS_THM]) in
 849  let LEFT_OR_FORALL_TAG = prove
 850  (`!P Q. TAGB(!x. P x \/ Q) <=> (!x:A. P x) \/ Q `,
 851  REWRITE_TAC[tagb;LEFT_OR_FORALL_THM]) in
 852  let RIGHT_OR_FORALL_TAG = prove
 853  (`!P Q. TAGB(!x. P \/ Q x) <=> P \/ (!x:A. Q x) `,
 854   REWRITE_TAC[tagb;RIGHT_OR_FORALL_THM]) in
 855  let LEFT_IMP_FORALL_TAG = prove
 856  (`!P Q. TAGB(?x. P x ==> Q) <=> ((!x:A. P x) ==> Q) `,
 857  REWRITE_TAC[tagb;LEFT_IMP_FORALL_THM]) in
 858  let RIGHT_IMP_EXISTS_TAG = prove
 859  (`!P Q. TAGB(?x:A. P ==> Q x) <=> (P ==> (?x:A. Q x)) `,
 860  REWRITE_TAC[tagb;RIGHT_IMP_EXISTS_THM]) in
 861   fun var_name tm ->
 862      REWRITE_RULE [tagb]
 863        (TOP_SWEEP_CONV
 864        (GEN_REWRITE_CONV I
 865          [NOT_FORALL_TAG;SKOLEM_TAG;SKOLEM_TAG2;
 866           SWAP_FORALL_TAG;SWAP_EXISTS_THM;
 867           SWAP_EXISTS_THM;
 868           AND_FORALL_TAG;LEFT_AND_FORALL_TAG;RIGHT_AND_FORALL_TAG;
 869           TRIV_OR_FORALL_TAG;RIGHT_IMP_FORALL_TAG;
 870           OR_EXISTS_THM;LEFT_OR_EXISTS_THM;RIGHT_OR_EXISTS_THM;
 871           LEFT_AND_EXISTS_THM;
 872           RIGHT_AND_EXISTS_THM;
 873           TRIV_AND_EXISTS_THM;LEFT_IMP_EXISTS_THM;TRIV_FORALL_IMP_THM;
 874           TRIV_EXISTS_IMP_THM;NOT_EXISTS_TAG;
 875           LEFT_OR_FORALL_TAG;RIGHT_OR_FORALL_TAG;LEFT_IMP_FORALL_TAG;
 876           RIGHT_IMP_EXISTS_TAG;
 877          ])
 878        (tag_quant var_name tm));;
 879
 880
 881 (* ------------------------------------------------------------------ *)
 882 (* Dropping Superfluous Quantifiers .
 883     Example: ?u. (u = t) /\ ...
 884     We can eliminate the u.
 885  *)
 886 (* ------------------------------------------------------------------ *)
 887
 888 let mark_term = new_definition `mark_term (u:A) = u`;;
 889
 890 (*** JRH replaced Comb and Abs with explicit constructors ***)
 891
 892 let rec markq qname tm =
 893   match tm with
 894    Var (a,b) -> if (a=qname) then mk_icomb (`mark_term:A->A`,tm) else tm
 895   |Const(_,_) -> tm
 896   |Comb(s,b) -> mk_comb(markq qname s,markq qname b)
 897   |Abs (x,t) -> mk_abs(x,markq qname t);;
 898
 899 let rec getquants tm =
 900   if (is_forall tm) then
 901      (fst (dest_var (fst (dest_forall tm))))::
 902         (getquants (snd (dest_forall tm)))
 903   else if (is_exists tm) then
 904      (fst (dest_var (fst (dest_exists tm))))::
 905         (getquants (snd (dest_exists tm)))
 906   else match tm with
 907     Comb(s,b) -> (getquants s) @ (getquants b)
 908   | Abs (x,t) -> (getquants t)
 909   | _ -> [];;
 910
 911 (* can loop if there are TWO *)
 912 let rewrite_conjs = [
 913   prove_by_refinement (`!A B C. (A /\ B) /\ C <=> A /\ B /\ C`,[REWRITE_TAC[CONJ_ACI]]);
 914   prove_by_refinement (`!u. (mark_term (u:A) = mark_term u) <=> T`,[MESON_TAC[]]);
 915   prove_by_refinement (`!u t. (t = mark_term (u:A)) <=> (mark_term u = t)`,[MESON_TAC[]]);
 916   prove_by_refinement (`!u a b. (mark_term (u:A) = a) /\ (mark_term u = b) <=> (mark_term u = a) /\ (a = b)`,[MESON_TAC[]]);
 917   prove_by_refinement (`!u a b B. (mark_term (u:A) = a) /\ (mark_term u = b) /\ B <=> (mark_term u = a) /\ (a = b) /\ B`,[MESON_TAC[]]);
 918   prove_by_refinement (`!u t A C. A /\ (mark_term (u:A) = t) /\ C <=>
 919         (mark_term u = t) /\ A /\ C`,[MESON_TAC[]]);
 920   prove_by_refinement (`!A u t. A /\ (mark_term (u:A) = t)  <=>
 921         (mark_term u = t) /\ A `,[MESON_TAC[]]);
 922   prove_by_refinement (`!u t C D. (((mark_term (u:A) = t) /\ C) ==> D) <=>
 923         ((mark_term (u:A) = t) ==> C ==> D)`,[MESON_TAC[]]);
 924   prove_by_refinement (`!A u t B. (A ==> (mark_term (u:A) = t) ==> B) <=>
 925          ((mark_term (u:A) = t) ==> A ==> B)`,[MESON_TAC[]]);
 926 ];;
 927
 928 let higher_conjs = [
 929   prove_by_refinement (`!C u t. ((mark_term u = t) ==> C (mark_term u)) <=>
 930        ((mark_term u = t) ==> C (t:A))`,[MESON_TAC[mark_term]]);
 931   prove_by_refinement (`!C u t. ((mark_term u = t) /\ C (mark_term u)) <=>
 932          ((mark_term u = t) /\ C (t:A))`,[MESON_TAC[mark_term]]);
 933 ];;
 934
 935
 936 let dropq_conv  =
 937   let drop_exist =
 938     REWRITE_CONV [prove_by_refinement (`!t. ?(u:A). (u = t)`,[MESON_TAC[]])] in
 939   fun qname tm ->
 940   let quanlist =  getquants tm in
 941   let quantleft_CONV = EVERY_CONV
 942       (map (REPEATC o quant_left_noswap_CONV) quanlist) in
 943   let qname_conv tm = prove(mk_eq(tm,markq qname tm),
 944              REWRITE_TAC[mark_term]) in
 945   let conj_conv = REWRITE_CONV rewrite_conjs in
 946   let quantright_CONV = (REPEATC (quant_right_CONV qname)) in
 947   let drop_mark_CONV = REWRITE_CONV [mark_term] in
 948  (quantleft_CONV THENC qname_conv  THENC conj_conv   THENC
 949       (ONCE_REWRITE_CONV higher_conjs)
 950        THENC drop_mark_CONV THENC quantright_CONV THENC
 951        drop_exist  ) tm ;;
 952
 953
 954 (* Examples : *)
 955 dropq_conv "u" `!P Q R . (?(u:B). (?(x:A). (u = P x) /\ (Q x)) /\ (R u))`;;
 956 dropq_conv "t" `!P Q R. (!(t:B). (?(x:A). P x /\ (t = Q x)) ==> R t)`;;
 957
 958 dropq_conv "u" `?u v.
 959      ((t * (a + &1) + (&1 - t) *a = u) /\
 960       (t * (b + &0) + (&1 - t) * b = v)) /\
 961      a < u /\
 962      u < r /\
 963      (v = b)`;;
 964
 965
 966
 967 (* ------------------------------------------------------------------ *)
 968 (*  SOME GENERAL TACTICS FOR THE ASSUMPTION LIST *)
 969 (* ------------------------------------------------------------------ *)
 970
 971 let (%) i = HYP (string_of_int i);;
 972
 973 let WITH i rule = (H_VAL (rule) (HYP (string_of_int i))) ;;
 974
 975 let (UND:int -> tactic) =
 976  fun i (asl,w) ->
 977    let name = "Z-"^(string_of_int i) in
 978    try let thm= assoc name asl in
 979         let tm = concl (thm) in
 980        let (_,asl') = partition (fun t-> ((=) name (fst t))) asl in
 981        null_meta,[asl',mk_imp(tm,w)],
 982        fun i [th] -> MP th (INSTANTIATE_ALL i thm)
 983    with Failure _ -> failwith "UND";;
 984
 985 let KILL i =
 986   (UND i) THEN (DISCH_THEN (fun t -> ALL_TAC));;
 987
 988 let USE i rule = (WITH i rule) THEN (KILL i);;
 989
 990 let CHO i = (UND i) THEN (DISCH_THEN CHOOSE_TAC);;
 991
 992 let X_CHO i t = (UND i) THEN (DISCH_THEN (X_CHOOSE_TAC t));;
 993
 994 let AND i = (UND i) THEN
 995   (DISCH_THEN (fun t-> (ASSUME_TAC (CONJUNCT1 t)
 996                           THEN (ASSUME_TAC (CONJUNCT2 t)))));;
 997
 998 let JOIN i j =
 999    (H_VAL2 CONJ ((%)i) ((%)j)) THEN (KILL i) THEN (KILL j);;
1000
1001 let COPY i = WITH i I;;
1002
1003 let REP n tac = EVERY (replicate tac n);;
1004
1005 let REWR i = (UND i) THEN (ASM_REWRITE_TAC[]) THEN DISCH_TAC;;
1006
1007 let LEFT i t = (USE i (CONV_RULE (quant_left_CONV t)));;
1008
1009 let RIGHT i t =  (USE i (CONV_RULE (quant_right_CONV t)));;
1010
1011 let LEFT_TAC  t = ((CONV_TAC (quant_left_CONV t)));;
1012
1013 let RIGHT_TAC t =  ( (CONV_TAC (quant_right_CONV t)));;
1014
1015 let INR = REWRITE_RULE[IN];;
1016
1017 (*
1018
1019
1020
1021 let rec REP n tac = if (n<=0) then ALL_TAC
1022   else (tac THEN (REP (n-1) tac));;  (* doesn't seem to work? *)
1023
1024
1025 let COPY i = (UNDISCH_WITH i) THEN (DISCH_THEN (fun t->ALL_TAC));;
1026
1027
1028 MANIPULATING ASSUMPTIONS. (MAKE 0= GOAL)
1029
1030 COPY: int -> tactic   Make a copy in adjacent slot.
1031
1032
1033 EXPAND: int -> tactic.
1034     conjunction -> two separate.
1035     exists/goal-forall -> choose.
1036     goal-if-then -> discharge
1037 EXPAND_TERM: int -> term -> tactic.
1038     constant -> expand definition or other rewrites associated.
1039 ADD: term -> tactic.
1040
1041 SIMPLIFY: int -> tactic.  Apply simplification rules.
1042
1043
1044 *)
1045
1046 let CONTRAPOSITIVE_TAC = MATCH_MP_TAC (TAUT `(~q ==> ~p) ==> (p ==> q)`)
1047                            THEN REWRITE_TAC[];;
1048
1049 let REWRT_TAC = (fun t-> REWRITE_TAC[t]);;
1050
1051 let (REDUCE_CONV,REDUCE_TAC) =
1052  let list = [
1053    (* reals *)   REAL_NEG_GE0;
1054    REAL_HALF_DOUBLE;
1055    REAL_SUB_REFL ;
1056    REAL_NEG_NEG;
1057    REAL_LE; LE_0;
1058    REAL_ADD_LINV;REAL_ADD_RINV;
1059    REAL_NEG_0;
1060    REAL_NEG_LE0;
1061    REAL_NEG_GE0;
1062    REAL_LE_NEGL;
1063    REAL_LE_NEGR;
1064    REAL_LE_NEG;
1065    REAL_NEG_EQ_0;
1066    REAL_SUB_RNEG;
1067    REAL_ARITH `!(x:real). (--x = x) <=>  (x = &.0)`;
1068    REAL_ARITH `!(a:real) b. (a - b + b) = a`;
1069    REAL_ADD_LID;
1070    REAL_ADD_RID ;
1071    REAL_INV_0;
1072    REAL_OF_NUM_EQ;
1073    REAL_OF_NUM_LE;
1074    REAL_OF_NUM_LT;
1075    REAL_OF_NUM_ADD;
1076    REAL_OF_NUM_MUL;
1077    REAL_POS;
1078    REAL_MUL_RZERO;
1079    REAL_MUL_LZERO;
1080    REAL_LE_01;
1081    REAL_SUB_RZERO;
1082    REAL_LE_SQUARE;
1083    REAL_MUL_RID;
1084    REAL_MUL_LID;
1085    REAL_ABS_ZERO;
1086    REAL_ABS_NUM;
1087    REAL_ABS_1;
1088    REAL_ABS_NEG;
1089    REAL_ABS_POS;
1090    ABS_ZERO;
1091    ABS_ABS;
1092    REAL_NEG_LT0;
1093    REAL_NEG_GT0;
1094    REAL_LT_NEG;
1095    REAL_NEG_MUL2;
1096    REAL_OF_NUM_POW;
1097    REAL_LT_INV_EQ;
1098    REAL_POW_1;
1099    REAL_INV2;
1100    prove (`(--. (&.n) < (&.m)) <=> (&.0 < (&.n) + (&.m))`,REAL_ARITH_TAC);
1101    prove (`(--. (&.n) <= (&.m)) <=> (&.0 <= (&.n) + (&.m))`,REAL_ARITH_TAC);
1102    prove (`(--. (&.n) = (&.m)) <=> ((&.n) + (&.m) = (&.0))`,REAL_ARITH_TAC);
1103    prove (`((&.n) < --.(&.m)) <=> ((&.n) + (&.m) <. (&.0))`,REAL_ARITH_TAC);
1104    prove (`((&.n) <= --.(&.m)) <=> ((&.n) + (&.m) <=. (&.0))`,REAL_ARITH_TAC);
1105    prove (`((&.n) = --.(&.m)) <=> ((&.n) + (&.m) = (&.0))`,REAL_ARITH_TAC);
1106    prove (`((&.n) < --.(&.m) + &.r) <=> ((&.n) + (&.m) < (&.r))`,REAL_ARITH_TAC);
1107    prove (`(--. x = --. y) <=> (x = y)`,REAL_ARITH_TAC);
1108    prove (`(--(&.n) < --.(&.m) + &.r) <=> ( (&.m) < &.n + (&.r))`,REAL_ARITH_TAC);
1109    prove (`(--. x = --. y) <=> (x = y)`,REAL_ARITH_TAC);
1110    prove (`((--. (&.1))*  x < --. y <=> y < x)`,REAL_ARITH_TAC );
1111    prove (`((--. (&.1))*  x <= --. y <=> y <= x)`,REAL_ARITH_TAC );
1112    (* num *)
1113    EXP_1;
1114    EXP_LT_0;
1115    ADD_0;
1116    ARITH_RULE `0+| m  = m`;
1117    ADD_EQ_0;
1118    prove (`(0 = m +|n) <=> (m = 0)/\ (n=0)`,MESON_TAC[ADD_EQ_0]);
1119    EQ_ADD_LCANCEL_0;
1120    EQ_ADD_RCANCEL_0;
1121    LT_ADD;
1122    LT_ADDR;
1123    ARITH_RULE `(0 = j -| i) <=> (j <=| i)`;
1124    ARITH_RULE `(j -| i = 0) <=> (j <=| i)`;
1125    ARITH_RULE `0 -| i = 0`;
1126    ARITH_RULE `(i<=| j) /\ (j <=| i) <=> (i = j)`;
1127    ARITH_RULE `0 <| 1`;
1128    (* SUC *)
1129    NOT_SUC;
1130    SUC_INJ;
1131    PRE;
1132    ADD_CLAUSES;
1133    MULT;
1134    MULT_CLAUSES;
1135    LE; LT;
1136    ARITH_RULE `SUC b -| 1 = b`;
1137    ARITH_RULE `SUC b -| b = 1`;
1138    prove(`&.(SUC x) - &.x = &.1`,
1139       REWRITE_TAC [REAL_ARITH `(a -. b=c) <=> (a  = b+.c)`;
1140       REAL_OF_NUM_ADD;REAL_OF_NUM_EQ] THEN ARITH_TAC);
1141    (* (o) *)
1142    o_DEF;
1143    (* I *)
1144    I_THM;
1145    I_O_ID;
1146    (* pow *)
1147    REAL_POW_1;
1148    REAL_POW_ONE;
1149    (* INT *)
1150    INT_ADD_LINV;
1151    INT_ADD_RINV;
1152    INT_ADD_SUB2;
1153    INT_EQ_NEG2;
1154    INT_LE_NEG;
1155    INT_LE_NEGL;
1156    INT_LE_NEGR;
1157    INT_LT_NEG;
1158    INT_LT_NEG2;
1159    INT_NEGNEG;
1160    INT_NEG_0;
1161    INT_NEG_EQ_0;
1162    INT_NEG_GE0;
1163    INT_NEG_GT0;
1164    INT_NEG_LE0;
1165    INT_NEG_LT0;
1166    GSYM INT_NEG_MINUS1;
1167    INT_NEG_MUL2;
1168    INT_NEG_NEG;
1169    (* sets *)
1170    ] in
1171 (REWRITE_CONV list,REWRITE_TAC list);;
1172
1173
1174
1175
1176
1177 (* prove by squaring *)
1178 let REAL_POW_2_LE = prove_by_refinement(
1179   `!x y. (&.0 <= x) /\ (&.0 <= y) /\ (x pow 2 <=. y pow 2) ==> (x <=. y)`,
1180   (* {{{ proof *)
1181   [
1182   DISCH_ALL_TAC;
1183   MP_TAC (SPECL[` (x:real) pow 2`;`(y:real)pow 2`] SQRT_MONO_LE);
1184   ASM_REWRITE_TAC[];
1185   ASM_SIMP_TAC[REAL_POW_LE];
1186   ASM_SIMP_TAC[POW_2_SQRT];
1187   ]);;
1188   (* }}} *)
1189
1190 (* prove by squaring *)
1191 let REAL_POW_2_LT = prove_by_refinement(
1192   `!x y. (&.0 <= x) /\ (&.0 <= y) /\ (x pow 2 <. y pow 2) ==> (x <. y)`,
1193   (* {{{ proof *)
1194
1195   [
1196   DISCH_ALL_TAC;
1197   MP_TAC (SPECL[` (x:real) pow 2`;`(y:real)pow 2`] SQRT_MONO_LT);
1198   ASM_REWRITE_TAC[];
1199   ASM_SIMP_TAC[REAL_POW_LE];
1200   ASM_SIMP_TAC[POW_2_SQRT];
1201   ]);;
1202
1203   (* }}} *)
1204
1205 let SQUARE_TAC =
1206     FIRST[
1207       MATCH_MP_TAC REAL_LE_LSQRT;
1208       MATCH_MP_TAC REAL_POW_2_LT;
1209       MATCH_MP_TAC REAL_POW_2_LE
1210     ]
1211     THEN REWRITE_TAC[];;
1212
1213 (****)
1214
1215 let SPEC2_TAC t = SPEC_TAC (t,t);;
1216
1217 let IN_ELIM i = (USE i (REWRITE_RULE[IN]));;
1218
1219 let rec range i n =
1220   if (n>0) then (i::(range (i+1) (n-1))) else [];;
1221
1222
1223 (* in elimination *)
1224
1225 let (IN_OUT_TAC: tactic) =
1226    fun (asl,g) -> (REWRITE_TAC [IN] THEN
1227    (EVERY (map (IN_ELIM) (range 0 (length asl))))) (asl,g);;
1228
1229 let (IWRITE_TAC : thm list -> tactic) =
1230    fun thlist -> REWRITE_TAC (map INR thlist);;
1231
1232 let (IWRITE_RULE : thm list -> thm -> thm) =
1233    fun thlist -> REWRITE_RULE (map INR thlist);;
1234
1235 let IMATCH_MP imp ant = MATCH_MP (INR imp) (INR ant);;
1236
1237 let IMATCH_MP_TAC imp  = MATCH_MP_TAC  (INR imp);;
1238
1239
1240 let GBETA_TAC =   (CONV_TAC (TOP_DEPTH_CONV GEN_BETA_CONV));;
1241 let GBETA_RULE =   (CONV_RULE (TOP_DEPTH_CONV GEN_BETA_CONV));;
1242
1243 (* breaks antecedent into multiple cases *)
1244 let REP_CASES_TAC =
1245   REPEAT (DISCH_THEN (REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC));;
1246
1247 let TSPEC t i  = TYPE_THEN t (USE i o SPEC);;
1248
1249 let IMP_REAL t i = (USE i (MATCH_MP (REAL_ARITH t)));;
1250
1251 (* goes from f = g to fz = gz *)
1252 let TAPP z i  = TYPE_THEN z (fun u -> (USE i(fun t -> AP_THM t u)));;
1253
1254 (* ONE NEW TACTIC -- DOESN'T WORK!! DON'T USE....
1255 let CONCL_TAC t = let co = snd  (dest_imp (concl t)) in
1256   SUBGOAL_TAC co THEN (TRY (IMATCH_MP_TAC  t));;
1257 *)
1258
1259 (* subgoal the antecedent of a THM, in order to USE the conclusion *)
1260 let ANT_TAC t = let (ant,co) =   (dest_imp (concl t)) in
1261   SUBGOAL_TAC ant
1262   THENL [ALL_TAC;DISCH_THEN (fun u-> MP_TAC (MATCH_MP t u))];;
1263
1264
1265 let TH_INTRO_TAC tl th = TYPEL_THEN tl (fun t-> ANT_TAC (ISPECL t th));;
1266
1267 let THM_INTRO_TAC tl th = TYPEL_THEN tl
1268   (fun t->
1269     let s = ISPECL t th in
1270     if is_imp (concl s) then ANT_TAC s else ASSUME_TAC s);;
1271
1272 let (DISCH_THEN_FULL_REWRITE:tactic) =
1273       DISCH_THEN (fun t-> REWRITE_TAC[t] THEN
1274                     (RULE_ASSUM_TAC  (REWRITE_RULE[t])));;
1275
1276 let FULL_REWRITE_TAC t = (REWRITE_TAC t THEN (RULE_ASSUM_TAC (REWRITE_RULE t)));;
1277
1278 (* ------------------------------------------------------------------ *)
1279
1280 let BASIC_TAC  =
1281   [ GEN_TAC;
1282     IMATCH_MP_TAC  (TAUT ` (a ==> b ==> C) ==> ( a /\ b ==> C)`);
1283     DISCH_THEN (CHOOSE_THEN MP_TAC);
1284     FIRST_ASSUM (fun t-> UNDISCH_TAC (concl t) THEN
1285               (DISCH_THEN CHOOSE_TAC));
1286     FIRST_ASSUM (fun t ->
1287         (if (length (CONJUNCTS t) < 2) then failwith "BASIC_TAC"
1288          else UNDISCH_TAC (concl t)));
1289     DISCH_TAC;
1290   ];;
1291
1292 let REP_BASIC_TAC = REPEAT (CHANGED_TAC (FIRST BASIC_TAC));;
1293
1294 (* ------------------------------------------------------------------ *)
1295
1296 let USE_FIRST rule =
1297   FIRST_ASSUM (fun t -> (UNDISCH_TAC (concl t) THEN
1298    (DISCH_THEN (ASSUME_TAC o rule))));;
1299
1300 let WITH_FIRST rule =
1301   FIRST_ASSUM (fun t -> ASSUME_TAC (rule t));;
1302
1303 let UNDF t = (TYPE_THEN t UNDISCH_FIND_TAC );;
1304
1305 let GRABF t ttac = (UNDF t THEN (DISCH_THEN ttac));;
1306
1307 let USEF t rule =
1308     (TYPE_THEN t (fun t' -> UNDISCH_FIND_THEN t'
1309                         (fun u -> ASSUME_TAC (rule u))));;
1310
1311
1312 (* ------------------------------------------------------------------ *)
1313 (* UNIFY_EXISTS_TAC *)
1314 (* ------------------------------------------------------------------ *)
1315
1316 let rec EXISTSL_TAC tml = match tml with
1317   a::tml' -> EXISTS_TAC a THEN EXISTSL_TAC tml' |
1318   [] -> ALL_TAC;;
1319
1320 (*
1321   Goal:  ?x1....xn. P1 /\ ... /\ Pm
1322   Try to pick ALL of x1...xn to unify ONE or more Pi with terms
1323   appearing in the assumption list, trying term_unify on
1324   each Pi with each assumption.
1325 *)
1326 let (UNIFY_EXISTS_TAC:tactic) =
1327   let run_one wc assum (varl,sofar)  =
1328     if varl = [] then (varl,sofar) else
1329       try (
1330         let wc' = instantiate ([],sofar,[]) wc in
1331         let (_,ins,_) = term_unify varl wc' assum in
1332         let insv = map snd ins in
1333           ( subtract varl insv  , union sofar ins    )
1334       ) with failure -> (varl,sofar) in
1335   let run_onel asl wc (varl,sofar)   =
1336     itlist (run_one wc) asl (varl,sofar) in
1337   let run_all varl sofar wcl asl =
1338     itlist (run_onel asl) wcl (varl,sofar) in
1339   let full_unify (asl,w) =
1340     let (varl,ws) = strip_exists w in
1341     let vargl = map genvar (map type_of varl) in
1342     let wg = instantiate ([],zip vargl varl,[]) ws in
1343     let wcg = conjuncts wg in
1344     let (vargl',sofar) = run_all vargl [] wcg ( asl) in
1345       if (vargl' = []) then
1346         map (C rev_assoc sofar) (map (C rev_assoc (zip vargl varl)) varl)
1347       else failwith "full_unify: unification not found " in
1348   fun (asl,w) ->
1349     try(
1350       let asl' = map (concl o snd) asl in
1351       let asl'' = flat (map (conjuncts ) asl') in
1352       let varsub = full_unify (asl'',w) in
1353         EXISTSL_TAC varsub (asl,w)
1354     ) with failure -> failwith "UNIFY_EXIST_TAC: unification not found.";;
1355
1356 (* partial example *)
1357 let unify_exists_tac_example = try(prove_by_refinement(
1358   `!C a b v A R TX U SS. (A v /\ (a = v) /\  (C:num->num->bool) a b /\ R a ==>
1359     ?v v'. TX v' /\ U v v' /\  C v' v /\ SS v)`,
1360   (* {{{ proof *)
1361
1362   [
1363   REP_BASIC_TAC;
1364   UNIFY_EXISTS_TAC; (* v' -> a  and v -> b *)
1365   (* not finished. Here is a variant approach. *)
1366   REP_GEN_TAC;
1367   DISCH_TAC;
1368   UNIFY_EXISTS_TAC;
1369   ])) with failure -> (REFL `T`);;
1370
1371   (* }}} *)
1372
1373 (* ------------------------------------------------------------------ *)
1374 (* UNIFY_EXISTS conversion *)
1375 (* ------------------------------------------------------------------ *)
1376
1377 (*
1378    FIRST argument is the "certificate"
1379    second arg is the goal.
1380    Example:
1381    UNIFY_EXISTS `(f:num->bool) x` `?t. (f:num->bool) t`
1382 *)
1383
1384 let (UNIFY_EXISTS:thm -> term -> thm) =
1385   let run_one wc assum (varl,sofar)  =
1386     if varl = [] then (varl,sofar) else
1387       try (
1388         let wc' = instantiate ([],sofar,[]) wc in
1389         let (_,ins,_) = term_unify varl wc' assum in
1390         let insv = map snd ins in
1391           ( subtract varl insv  , union sofar ins    )
1392       ) with failure -> (varl,sofar) in
1393   let run_onel asl wc (varl,sofar)   =
1394     itlist (run_one wc) asl (varl,sofar) in
1395   let run_all varl sofar wcl asl =
1396     itlist (run_onel asl) wcl (varl,sofar) in
1397   let full_unify (t,w) =
1398     let (varl,ws) = strip_exists w in
1399     let vargl = map genvar (map type_of varl) in
1400     let wg = instantiate ([],zip vargl varl,[]) ws in
1401     let wcg = conjuncts wg in
1402     let (vargl',sofar) = run_all vargl [] wcg ( [concl t]) in
1403       if (vargl' = []) then
1404         map (C rev_assoc sofar) (map (C rev_assoc (zip vargl varl)) varl)
1405       else failwith "full_unify: unification not found " in
1406   fun t w ->
1407     try(
1408       if not(is_exists w) then failwith "UNIFY_EXISTS: not EXISTS" else
1409       let varl' =  (full_unify (t,w)) in
1410       let (varl,ws) = strip_exists w in
1411       let varsub = zip varl' varl in
1412       let varlb = map (fun s->  chop_list s (rev varl))
1413             (range 1 (length varl)) in
1414       let targets = map (fun s-> (instantiate ([],varsub,[])
1415           (list_mk_exists( rev (fst s),  ws)) )) varlb in
1416       let target_zip  = zip (rev targets) varl' in
1417       itlist (fun s th  -> EXISTS s  th) target_zip t
1418     ) with failure -> failwith "UNIFY_EXISTS: unification not found.";;
1419
1420 let unify_exists_example=
1421    UNIFY_EXISTS (ARITH_RULE `2 = 0+2`) `(?x y. ((x:num) = y))`;;
1422
1423 (* now make a prover for it *)
1424
1425
1426 (* ------------------------------------------------------------------ *)
1427
1428 (*
1429 drop_ant_tac replaces
1430   0  A ==>B
1431   1  A
1432 with
1433   0  B
1434   1  A
1435 in hypothesis list
1436 *)
1437 let DROP_ANT_TAC pq  =
1438   UNDISCH_TAC pq THEN (UNDISCH_TAC (fst (dest_imp pq))) THEN
1439   DISCH_THEN (fun pthm -> ASSUME_TAC pthm THEN
1440       DISCH_THEN (fun pqthm -> ASSUME_TAC (MATCH_MP pqthm pthm )));;
1441
1442 let (DROP_ALL_ANT_TAC:tactic) =
1443   fun (asl,w) ->
1444     let imps = filter (is_imp) (map (concl o snd) asl) in
1445     MAP_EVERY (TRY o DROP_ANT_TAC) imps (asl,w);;
1446
1447 let drop_ant_tac_example = prove_by_refinement(
1448   `!A B C D E. (A /\ (A ==> B) /\ (C ==>D) /\ C) ==> (E \/ C \/ B)`,
1449   (* {{{ proof *)
1450   [
1451   REP_BASIC_TAC;
1452   DROP_ALL_ANT_TAC;
1453   ASM_REWRITE_TAC[];
1454   ]);;
1455   (* }}} *)
1456
1457 (* ------------------------------------------------------------------ *)
1458
1459 (* ASSUME tm, then prove it later. almost the same as asm-cases-tac *)
1460 let (BACK_TAC : term -> tactic) =
1461   fun tm (asl,w) ->
1462     let ng = mk_imp (tm,w) in
1463     (SUBGOAL_TAC ng THENL [ALL_TAC;DISCH_THEN  IMATCH_MP_TAC ]) (asl,w);;
1464
1465 (* --- *)
1466 (* Using hash numbers for tactics *)
1467 (* --- *)
1468
1469 let label_of_hash ((asl,g):goal) (h:int) =
1470   let one_label h (s,tm) =
1471     if  (h = hash_of_term (concl tm)) then
1472       let s1 = String.sub s 2 (String.length s - 2) in
1473       int_of_string s1
1474       else failwith "label_of_hash" in
1475   tryfind (one_label h) asl;;
1476
1477 let HASHIFY m h w = m (label_of_hash w h) w;;
1478 let UNDH = HASHIFY UND;;
1479 let REWRH = HASHIFY REWR;;
1480 let KILLH = HASHIFY KILL;;
1481 let COPYH = HASHIFY COPY;;
1482 let HASHIFY1 m h tm w = m (label_of_hash w h) tm w;;
1483 let USEH = HASHIFY1 USE;;
1484 let LEFTH = HASHIFY1 LEFT;;
1485 let RIGHTH = HASHIFY1 RIGHT;;
1486 let TSPECH tm h w = TSPEC tm (label_of_hash w h) w ;;