development/thales/chaff/tactics.hl

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