text_formalization/jordan/tactics_jordan.hl

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