Examples/holby.ml

   1 (* ========================================================================= *)
   2 (* A HOL "by" tactic, doing Mizar-like things, trying something that is      *)
   3 (* sufficient for HOL's basic rules, trying a few other things like          *)
   4 (* arithmetic, and finally if all else fails using MESON_TAC[].              *)
   5 (* ========================================================================= *)
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* More refined net lookup that double-checks conditions like matchability.  *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let matching_enter tm y net =
  12   enter [] (tm,((fun tm' -> can (term_match [] tm) tm'),y)) net;;
  13
  14 let unconditional_enter (tm,y) net =
  15   enter [] (tm,((fun t -> true),y)) net;;
  16
  17 let conditional_enter (tm,condy) net =
  18   enter [] (tm,condy) net;;
  19
  20 let careful_lookup tm net =
  21   map snd (filter (fun (c,y) -> c tm) (lookup tm net));;
  22
  23 (* ------------------------------------------------------------------------- *)
  24 (* Transform theorem list to simplify, eliminate redundant connectives and   *)
  25 (* split the problem into (generally multiple) subproblems. Then, call the   *)
  26 (* prover given as the first argument on each component.                     *)
  27 (* ------------------------------------------------------------------------- *)
  28
  29 let SPLIT_THEN =
  30   let action_false th f oths = th
  31   and action_true th f oths = f oths
  32   and action_conj th f oths =
  33     f (CONJUNCT1 th :: CONJUNCT2 th :: oths)
  34   and action_disj th f oths =
  35     let th1 = f (ASSUME(lhand(concl th)) :: oths)
  36     and th2 = f (ASSUME(rand(concl th)) :: oths) in
  37     DISJ_CASES th th1 th2
  38   and action_taut tm =
  39     let pfun = PART_MATCH lhs (TAUT tm) in
  40     let prule th = EQ_MP (pfun (concl th)) th in
  41     lhand tm,(fun th f oths -> f(prule th :: oths)) in
  42   let enet = itlist unconditional_enter
  43     [`F`,action_false;
  44      `T`,action_true;
  45      `p /\ q`,action_conj;
  46      `p \/ q`,action_disj;
  47      action_taut `(p ==> q) <=> ~p \/ q`;
  48      action_taut `~F <=> T`;
  49      action_taut `~T <=> F`;
  50      action_taut  `~(~p) <=> p`;
  51      action_taut  `~(p /\ q) <=> ~p \/ ~q`;
  52      action_taut  `~(p \/ q) <=> ~p /\ ~q`;
  53      action_taut  `~(p ==> q) <=> p /\ ~q`;
  54      action_taut `p /\ F <=> F`;
  55      action_taut `F /\ p <=> F`;
  56      action_taut `p /\ T <=> p`;
  57      action_taut `T /\ p <=> p`;
  58      action_taut `p \/ F <=> p`;
  59      action_taut `F \/ p <=> p`;
  60      action_taut `p \/ T <=> T`;
  61      action_taut `T \/ p <=> T`]
  62     (let tm,act = action_taut `~(p <=> q) <=> p /\ ~q \/ ~p /\ q` in
  63      let cond tm = type_of(rand(rand tm)) = bool_ty in
  64      conditional_enter (tm,(cond,act))
  65         (let tm,act = action_taut `(p <=> q) <=> p /\ q \/ ~p /\ ~q` in
  66          let cond tm = type_of(rand tm) = bool_ty in
  67          conditional_enter (tm,(cond,act)) empty_net)) in
  68   fun prover ->
  69     let rec splitthen splat tosplit =
  70       match tosplit with
  71         [] -> prover (rev splat)
  72       | th::oths ->
  73           let funs = careful_lookup (concl th) enet in
  74           if funs = [] then splitthen (th::splat) oths
  75           else (hd funs) th (splitthen splat) oths in
  76     splitthen [];;
  77
  78 (* ------------------------------------------------------------------------- *)
  79 (* A similar thing that also introduces Skolem constants (but not functions) *)
  80 (* and does some slight first-order simplification like trivial miniscoping. *)
  81 (* ------------------------------------------------------------------------- *)
  82
  83 let SPLIT_FOL_THEN =
  84   let action_false th f splat oths = th
  85   and action_true th f splat oths = f oths
  86   and action_conj th f splat oths =
  87     f (CONJUNCT1 th :: CONJUNCT2 th :: oths)
  88   and action_disj th f splat oths =
  89     let th1 = f (ASSUME(lhand(concl th)) :: oths)
  90     and th2 = f (ASSUME(rand(concl th)) :: oths) in
  91     DISJ_CASES th th1 th2
  92   and action_exists th f splat oths =
  93     let v,bod = dest_exists(concl th) in
  94     let vars = itlist (union o thm_frees) (oths @ splat) (thm_frees th) in
  95     let v' = variant vars v in
  96     let th' = ASSUME (subst [v',v] bod) in
  97     CHOOSE (v',th) (f (th'::oths))
  98   and action_taut tm =
  99     let pfun = PART_MATCH lhs (TAUT tm) in
 100     let prule th = EQ_MP (pfun (concl th)) th in
 101     lhand tm,(fun th f splat oths -> f(prule th :: oths))
 102   and action_fol tm =
 103     let pfun = PART_MATCH lhs (prove(tm,MESON_TAC[])) in
 104     let prule th = EQ_MP (pfun (concl th)) th in
 105     lhand tm,(fun th f splat oths -> f(prule th :: oths)) in
 106   let enet = itlist unconditional_enter
 107     [`F`,action_false;
 108      `T`,action_true;
 109      `p /\ q`,action_conj;
 110      `p \/ q`,action_disj;
 111      `?x. P x`,action_exists;
 112      action_taut `~(~p) <=> p`;
 113      action_taut `~(p /\ q) <=> ~p \/ ~q`;
 114      action_taut `~(p \/ q) <=> ~p /\ ~q`;
 115      action_fol `~(!x. P x) <=> (?x. ~(P x))`;
 116      action_fol `(!x. P x /\ Q x) <=> (!x. P x) /\ (!x. Q x)`]
 117     empty_net in
 118   fun prover ->
 119     let rec splitthen splat tosplit =
 120       match tosplit with
 121         [] -> prover (rev splat)
 122       | th::oths ->
 123           let funs = careful_lookup (concl th) enet in
 124           if funs = [] then splitthen (th::splat) oths
 125           else (hd funs) th (splitthen splat) splat oths in
 126     splitthen [];;
 127
 128 (* ------------------------------------------------------------------------- *)
 129 (* Do the basic "semantic correlates" stuff.                                 *)
 130 (* This is more like NNF than Mizar's version.                               *)
 131 (* ------------------------------------------------------------------------- *)
 132
 133 let CORRELATE_RULE =
 134   PURE_REWRITE_RULE
 135    [TAUT `(a <=> b) <=> (a ==> b) /\ (b ==> a)`;
 136     TAUT `(a ==> b) <=> ~a \/ b`;
 137     DE_MORGAN_THM;
 138     TAUT `~(~a) <=> a`;
 139     TAUT `~T <=> F`;
 140     TAUT `~F <=> T`;
 141     TAUT `T /\ p <=> p`;
 142     TAUT `p /\ T <=> p`;
 143     TAUT `F /\ p <=> F`;
 144     TAUT `p /\ F <=> F`;
 145     TAUT `T \/ p <=> T`;
 146     TAUT `p \/ T <=> T`;
 147     TAUT `F \/ p <=> p`;
 148     TAUT `p \/ F <=> p`;
 149     GSYM CONJ_ASSOC; GSYM DISJ_ASSOC;
 150     prove(`(?x. P x) <=> ~(!x. ~(P x))`,MESON_TAC[])];;
 151
 152 (* ------------------------------------------------------------------------- *)
 153 (* Look for an immediate contradictory pair of theorems. This is quadratic,  *)
 154 (* but I doubt if that's much of an issue in practice. We could do something *)
 155 (* fancier, but need to be careful over alpha-equivalence if sorting.        *)
 156 (* ------------------------------------------------------------------------- *)
 157
 158 let THMLIST_CONTR_RULE =
 159   let CONTR_PAIR_THM = UNDISCH_ALL(TAUT `p ==> ~p ==> F`)
 160   and p_tm = `p:bool` in
 161   fun ths ->
 162     let ths_n,ths_p = partition (is_neg o concl) ths in
 163     let th_n = find (fun thn -> let tm = rand(concl thn) in
 164                                 exists (aconv tm o concl) ths_p) ths_n in
 165     let tm = rand(concl th_n) in
 166     let th_p = find (aconv tm o concl) ths_p in
 167     itlist PROVE_HYP [th_p; th_n] (INST [tm,p_tm] CONTR_PAIR_THM);;
 168
 169 (* ------------------------------------------------------------------------- *)
 170 (* Hence something similar to Mizar's "prechecker".                          *)
 171 (* ------------------------------------------------------------------------- *)
 172
 173 let PRECHECKER_THEN prover =
 174   SPLIT_THEN (fun ths -> try THMLIST_CONTR_RULE ths
 175                          with Failure _ ->
 176                              SPLIT_FOL_THEN prover (map CORRELATE_RULE ths));;
 177
 178 (* ------------------------------------------------------------------------- *)
 179 (* Lazy equations for use in congruence closure.                             *)
 180 (* ------------------------------------------------------------------------- *)
 181
 182 type lazyeq = Lazy of (term * term) * (unit -> thm);;
 183
 184 let cache f =
 185   let store = ref TRUTH in
 186   fun () -> let th = !store in
 187             if is_eq(concl th) then th else
 188             let th' = f() in
 189             (store := th'; th');;
 190
 191 let lazy_eq th =
 192   Lazy((dest_eq(concl th)),(fun () -> th));;
 193
 194 let lazy_eval (Lazy(_,f)) = f();;
 195
 196 let REFL' t = Lazy((t,t),cache(fun () -> REFL t));;
 197
 198 let SYM' = fun (Lazy((t,t'),f)) -> Lazy((t',t),cache(fun () -> SYM(f ())));;
 199
 200 let TRANS' =
 201   fun (Lazy((s,s'),f)) (Lazy((t,t'),g)) ->
 202      if not(aconv s' t) then failwith "TRANS'"
 203      else Lazy((s,t'),cache(fun () -> TRANS (f ()) (g ())));;
 204
 205 let MK_COMB' =
 206   fun (Lazy((s,s'),f),Lazy((t,t'),g)) ->
 207      Lazy((mk_comb(s,t),mk_comb(s',t')),cache(fun () -> MK_COMB (f (),g ())));;
 208
 209 let concl' = fun (Lazy(tmp,g)) -> tmp;;
 210
 211 (* ------------------------------------------------------------------------- *)
 212 (* Successors of a term, and predecessor function.                           *)
 213 (* ------------------------------------------------------------------------- *)
 214
 215 let successors tm =
 216   try let f,x = dest_comb tm in [f;x]
 217   with Failure _ -> [];;
 218
 219 let predecessor_function tms =
 220   itlist (fun x -> itlist (fun y f -> (y |-> insert x (tryapplyd f y [])) f)
 221                           (successors x))
 222          tms undefined;;
 223
 224 (* ------------------------------------------------------------------------- *)
 225 (* A union-find structure for equivalences, with theorems for edges.         *)
 226 (* ------------------------------------------------------------------------- *)
 227
 228 type termnode = Nonterminal of lazyeq | Terminal of term * term list;;
 229
 230 type termequivalence = Equivalence of (term,termnode)func;;
 231
 232 let rec terminus (Equivalence f as eqv) a =
 233   match (apply f a) with
 234     Nonterminal(th) -> let b = snd(concl' th) in
 235                        let th',n = terminus eqv b in
 236                        TRANS' th th',n
 237   | Terminal(t,n) -> (REFL' t,n);;
 238
 239 let tryterminus eqv a =
 240   try terminus eqv a with Failure _ -> (REFL' a,[a]);;
 241
 242 let canonize eqv a = fst(tryterminus eqv a);;
 243
 244 let equate th (Equivalence f as eqv) =
 245   let a,b = concl' th in
 246   let (ath,na) = tryterminus eqv a
 247   and (bth,nb) = tryterminus eqv b in
 248   let a' = snd(concl' ath) and b' = snd(concl' bth) in
 249   Equivalence
 250    (if a' = b' then f else
 251     if length na <= length nb then
 252       let th' = TRANS' (TRANS' (SYM' ath) th) bth in
 253       (a' |-> Nonterminal th') ((b' |-> Terminal(b',na@nb)) f)
 254     else
 255       let th' = TRANS'(SYM'(TRANS' th bth)) ath in
 256       (b' |-> Nonterminal th') ((a' |-> Terminal(a',na@nb)) f));;
 257
 258 let unequal = Equivalence undefined;;
 259
 260 let equated (Equivalence f) = dom f;;
 261
 262 let prove_equal eqv (s,t) =
 263   let sth = canonize eqv s and tth = canonize eqv t in
 264   TRANS' (canonize eqv s) (SYM'(canonize eqv t));;
 265
 266 let equivalence_class eqv a = snd(tryterminus eqv a);;
 267
 268 (* ------------------------------------------------------------------------- *)
 269 (* Prove composite terms equivalent based on 1-step congruence.              *)
 270 (* ------------------------------------------------------------------------- *)
 271
 272 let provecongruent eqv (tm1,tm2) =
 273   let f1,x1 = dest_comb tm1
 274   and f2,x2 = dest_comb tm2 in
 275   MK_COMB'(prove_equal eqv (f1,f2),prove_equal eqv (x1,x2));;
 276
 277 (* ------------------------------------------------------------------------- *)
 278 (* Merge equivalence classes given equation "th", using congruence closure.  *)
 279 (* ------------------------------------------------------------------------- *)
 280
 281 let rec emerge th (eqv,pfn) =
 282   let s,t = concl' th in
 283   let sth = canonize eqv s and tth = canonize eqv t in
 284   let s' = snd(concl' sth) and t' = snd(concl' tth) in
 285   if s' = t' then (eqv,pfn) else
 286   let sp = tryapplyd pfn s' [] and tp = tryapplyd pfn t' [] in
 287   let eqv' = equate th eqv in
 288   let stth = canonize eqv' s' in
 289   let sttm = snd(concl' stth) in
 290   let pfn' = (sttm |-> union sp tp) pfn in
 291   itlist (fun (u,v) (eqv,pfn as eqp) ->
 292              try let thuv = provecongruent eqv (u,v) in emerge thuv eqp
 293              with Failure _ -> eqp)
 294          (allpairs (fun u v -> (u,v)) sp tp) (eqv',pfn');;
 295
 296 (* ------------------------------------------------------------------------- *)
 297 (* Find subterms of "tm" that contain as a subterm one of the "tms" terms.   *)
 298 (* This is intended to be more efficient than the obvious "find_terms ...".  *)
 299 (* ------------------------------------------------------------------------- *)
 300
 301 let rec supersubterms tms tm =
 302   let ltms,tms' =
 303     if mem tm tms then [tm],filter (fun t -> t <> tm) tms
 304     else [],tms in
 305   if tms' = [] then ltms else
 306   let stms =
 307     try let l,r = dest_comb tm in
 308     union (supersubterms tms' l) (supersubterms tms' r)
 309     with Failure _ -> [] in
 310   if stms = [] then ltms
 311   else tm::stms;;
 312
 313 (* ------------------------------------------------------------------------- *)
 314 (* Find an appropriate term universe for overall terms "tms".                *)
 315 (* ------------------------------------------------------------------------- *)
 316
 317 let term_universe tms =
 318   setify (itlist ((@) o supersubterms tms) tms []);;
 319
 320 (* ------------------------------------------------------------------------- *)
 321 (* Congruence closure of "eqs" over term universe "tms".                     *)
 322 (* ------------------------------------------------------------------------- *)
 323
 324 let congruence_closure tms eqs =
 325   let pfn = predecessor_function tms in
 326   let eqv,_ = itlist emerge eqs (unequal,pfn) in
 327   eqv;;
 328
 329 (* ------------------------------------------------------------------------- *)
 330 (* Prove that "eq" follows from "eqs" by congruence closure.                 *)
 331 (* ------------------------------------------------------------------------- *)
 332
 333 let CCPROVE eqs eq =
 334   let tps = dest_eq eq :: map concl' eqs in
 335   let otms = itlist (fun (x,y) l -> x::y::l) tps [] in
 336   let tms = term_universe(setify otms) in
 337   let eqv = congruence_closure tms eqs in
 338   prove_equal eqv (dest_eq eq);;
 339
 340 (* ------------------------------------------------------------------------- *)
 341 (* Inference rule for `eq1 /\ ... /\ eqn ==> eq`                             *)
 342 (* ------------------------------------------------------------------------- *)
 343
 344 let CONGRUENCE_CLOSURE tm =
 345   if is_imp tm then
 346     let eqs,eq = dest_imp tm in
 347     DISCH eqs (lazy_eval(CCPROVE (map lazy_eq (CONJUNCTS(ASSUME eqs))) eq))
 348   else lazy_eval(CCPROVE [] tm);;
 349
 350 (* ------------------------------------------------------------------------- *)
 351 (* Inference rule for contradictoriness of set of +ve and -ve eqns.          *)
 352 (* ------------------------------------------------------------------------- *)
 353
 354 let CONGRUENCE_CLOSURE_CONTR ths =
 355   let nths,pths = partition (is_neg o concl) ths in
 356   let peqs = filter (is_eq o concl) pths
 357   and neqs = filter (is_eq o rand o concl) nths in
 358   let tps = map (dest_eq o concl) peqs @ map (dest_eq o rand o concl) neqs in
 359   let otms = itlist (fun (x,y) l -> x::y::l) tps [] in
 360   let tms = term_universe(setify otms) in
 361   let eqv = congruence_closure tms (map lazy_eq peqs) in
 362   let prover th =
 363     let eq = dest_eq(rand(concl th)) in
 364     let lth = prove_equal eqv eq in
 365     EQ_MP (EQF_INTRO th) (lazy_eval lth) in
 366   tryfind prover neqs;;
 367
 368 (* ------------------------------------------------------------------------- *)
 369 (* Attempt to prove equality between terms/formulas based on equivalence.    *)
 370 (* Note that ABS sideconditions are only checked at inference-time...        *)
 371 (* ------------------------------------------------------------------------- *)
 372
 373 let ABS' v =
 374   fun (Lazy((s,t),f)) ->
 375         Lazy((mk_abs(v,s),mk_abs(v,t)),
 376         cache(fun () -> ABS v (f ())));;
 377
 378 let ALPHA_EQ' s' t' =
 379   fun (Lazy((s,t),f) as inp) ->
 380         if s' = s & t' = t then inp else
 381         Lazy((s',t'),
 382              cache(fun () -> EQ_MP (ALPHA (mk_eq(s,t)) (mk_eq(s',t')))
 383                                    (f ())));;
 384
 385 let rec PROVE_EQUAL eqv (tm1,tm2 as tmp) =
 386   if tm1 = tm2 then REFL' tm1 else
 387   try prove_equal eqv tmp with Failure _ ->
 388   if is_comb tm1 & is_comb tm2 then
 389     let f1,x1 = dest_comb tm1
 390     and f2,x2 = dest_comb tm2 in
 391     MK_COMB'(PROVE_EQUAL eqv (f1,f2),PROVE_EQUAL eqv (x1,x2))
 392   else if is_abs tm1 & is_abs tm2 then
 393     let x1,bod1 = dest_abs tm1
 394     and x2,bod2 = dest_abs tm2 in
 395     let gv = genvar(type_of x1) in
 396     ALPHA_EQ' tm1 tm2
 397     (ABS' x1 (PROVE_EQUAL eqv (vsubst[gv,x1] bod1,vsubst[gv,x2] bod2)))
 398   else failwith "PROVE_EQUAL";;
 399
 400 let PROVE_EQUIVALENT eqv tm1 tm2 = lazy_eval (PROVE_EQUAL eqv (tm1,tm2));;
 401
 402 (* ------------------------------------------------------------------------- *)
 403 (* Complementary version for formulas.                                       *)
 404 (* ------------------------------------------------------------------------- *)
 405
 406 let PROVE_COMPLEMENTARY eqv th1 th2 =
 407   let tm1 = concl th1 and tm2 = concl th2 in
 408   if is_neg tm1 then
 409     let th = PROVE_EQUIVALENT eqv (rand tm1) tm2 in
 410     EQ_MP (EQF_INTRO th1) (EQ_MP (SYM th) th2)
 411   else if is_neg tm2 then
 412     let th = PROVE_EQUIVALENT eqv (rand tm2) tm1 in
 413     EQ_MP (EQF_INTRO th2) (EQ_MP (SYM th) th1)
 414   else failwith "PROVE_COMPLEMENTARY";;
 415
 416 (* ------------------------------------------------------------------------- *)
 417 (* Check equality under equivalence with "env" mapping for first term.       *)
 418 (* ------------------------------------------------------------------------- *)
 419
 420 let rec test_eq eqv (tm1,tm2) env =
 421   if is_comb tm1 & is_comb tm2 then
 422     let f1,x1 = dest_comb tm1
 423     and f2,x2 = dest_comb tm2 in
 424     test_eq eqv (f1,f2) env & test_eq eqv (x1,x2) env
 425   else if is_abs tm1 & is_abs tm2 then
 426     let x1,bod1 = dest_abs tm1
 427     and x2,bod2 = dest_abs tm2 in
 428     let gv = genvar(type_of x1) in
 429     test_eq eqv (vsubst[gv,x1] bod1,vsubst[gv,x2] bod2) env
 430   else if is_var tm1 & can (rev_assoc tm1) env then
 431     test_eq eqv (rev_assoc tm1 env,tm2) []
 432   else can (prove_equal eqv) (tm1,tm2);;
 433
 434 (* ------------------------------------------------------------------------- *)
 435 (* Map a term to its equivalence class modulo equivalence                    *)
 436 (* ------------------------------------------------------------------------- *)
 437
 438 let rec term_equivs eqv tm =
 439   let l = equivalence_class eqv tm in
 440   if l <> [tm] then l
 441   else if is_comb tm then
 442     let f,x = dest_comb tm in
 443     allpairs (curry mk_comb) (term_equivs eqv f) (term_equivs eqv x)
 444   else if is_abs tm then
 445     let v,bod = dest_abs tm in
 446     let gv = genvar(type_of v) in
 447     map (fun t -> alpha v (mk_abs(gv,t))) (term_equivs eqv (vsubst [gv,v] bod))
 448   else [tm];;
 449
 450 (* ------------------------------------------------------------------------- *)
 451 (* Replace "outer" universal variables with genvars. This is "outer" in the  *)
 452 (* second sense, i.e. universals not in scope of an existential or negation. *)
 453 (* ------------------------------------------------------------------------- *)
 454
 455 let rec GENSPEC th =
 456   let tm = concl th in
 457   if is_forall tm then
 458     let v = bndvar(rand tm) in
 459     let gv = genvar(type_of v) in
 460     GENSPEC(SPEC gv th)
 461   else if is_conj tm then
 462     let th1,th2 = CONJ_PAIR th in
 463     CONJ (GENSPEC th1) (GENSPEC th2)
 464   else if is_disj tm then
 465     let th1 = GENSPEC(ASSUME(lhand tm))
 466     and th2 = GENSPEC(ASSUME(rand tm)) in
 467     let th3 = DISJ1 th1 (concl th2)
 468     and th4 = DISJ2 (concl th1) th2 in
 469     DISJ_CASES th th3 th4
 470   else th;;
 471
 472 (* ------------------------------------------------------------------------- *)
 473 (* Simple first-order matching.                                              *)
 474 (* ------------------------------------------------------------------------- *)
 475
 476 let rec term_fmatch vars vtm ctm env =
 477   if mem vtm vars then
 478     if can (rev_assoc vtm) env then
 479       term_fmatch vars (rev_assoc vtm env) ctm env
 480     else if aconv vtm ctm then env else (ctm,vtm)::env
 481   else if is_comb vtm & is_comb ctm then
 482     let fv,xv = dest_comb vtm
 483     and fc,xc = dest_comb ctm in
 484     term_fmatch vars fv fc (term_fmatch vars xv xc env)
 485   else if is_abs vtm & is_abs ctm then
 486     let xv,bodv = dest_abs vtm
 487     and xc,bodc = dest_abs ctm in
 488     let gv = genvar(type_of xv) and gc = genvar(type_of xc) in
 489     let gbodv = vsubst [gv,xv] bodv
 490     and gbodc = vsubst [gc,xc] bodc in
 491     term_fmatch (gv::vars) gbodv gbodc ((gc,gv)::env)
 492   else if vtm = ctm then env
 493   else failwith "term_fmatch";;
 494
 495 let rec check_consistency env =
 496   match env with
 497     [] -> true
 498   | (c,v)::es -> forall (fun (c',v') -> v' <> v or c' = c) es;;
 499
 500 let separate_insts env =
 501   let tyin = itlist (fun (c,v) -> type_match (type_of v) (type_of c))
 502                     env [] in
 503   let ifn(c,v) = (inst tyin c,inst tyin v) in
 504   let tmin = setify (map ifn env) in
 505   if check_consistency tmin then (tmin,tyin)
 506   else failwith "separate_insts";;
 507
 508 let first_order_match vars vtm ctm env =
 509   let env' = term_fmatch vars vtm ctm env in
 510   if can separate_insts env' then env' else failwith "first_order_match";;
 511
 512 (* ------------------------------------------------------------------------- *)
 513 (* Try to match all leaves to negation of auxiliary propositions.            *)
 514 (* ------------------------------------------------------------------------- *)
 515
 516 let matchleaves =
 517   let rec matchleaves vars vtm ctms env cont =
 518     if is_conj vtm then
 519       try matchleaves vars (rand vtm) ctms env cont
 520       with Failure _ -> matchleaves vars (lhand vtm) ctms env cont
 521     else if is_disj vtm then
 522       matchleaves vars (lhand vtm) ctms env
 523        (fun e -> matchleaves vars (rand vtm) ctms e cont)
 524     else
 525       tryfind (fun ctm -> cont (first_order_match vars vtm ctm env)) ctms in
 526   fun vars vtm ctms env -> matchleaves vars vtm ctms env (fun e -> e);;
 527
 528 (* ------------------------------------------------------------------------- *)
 529 (* Now actually do the refutation once theorem is instantiated.              *)
 530 (* ------------------------------------------------------------------------- *)
 531
 532 let rec REFUTE_LEAVES eqv cths th =
 533   let tm = concl th in
 534   if is_conj tm then
 535     try REFUTE_LEAVES eqv cths (CONJUNCT1 th)
 536     with Failure _ -> REFUTE_LEAVES eqv cths (CONJUNCT2 th)
 537   else if is_disj tm then
 538     let th1 = REFUTE_LEAVES eqv cths (ASSUME(lhand tm))
 539     and th2 = REFUTE_LEAVES eqv cths (ASSUME(rand tm)) in
 540     DISJ_CASES th th1 th2
 541   else
 542     tryfind (PROVE_COMPLEMENTARY eqv th) cths;;
 543
 544 (* ------------------------------------------------------------------------- *)
 545 (* Hence the Mizar "unifier" for given universal formula.                    *)
 546 (* ------------------------------------------------------------------------- *)
 547
 548 let negate tm = if is_neg tm then rand tm else mk_neg tm;;
 549
 550 let MIZAR_UNIFIER eqv ths th =
 551   let gth = GENSPEC th in
 552   let vtm = concl gth in
 553   let vars = subtract (frees vtm) (frees(concl th))
 554   and ctms = map (negate o concl) ths in
 555   let allctms = itlist (union o term_equivs eqv) ctms [] in
 556   let env = matchleaves vars vtm allctms [] in
 557   let tmin,tyin = separate_insts env in
 558   REFUTE_LEAVES eqv ths (PINST tyin tmin gth);;
 559
 560 (* ------------------------------------------------------------------------- *)
 561 (* Deduce disequalities of subterms and add symmetric versions at the end.   *)
 562 (* ------------------------------------------------------------------------- *)
 563
 564 let rec DISEQUALITIES ths =
 565   match ths with
 566     [] -> []
 567   | th::oths ->
 568         let t1,t2 = dest_eq (rand(concl th)) in
 569         let f1,args1 = strip_comb t1
 570         and f2,args2 = strip_comb t2 in
 571         if f1 <> f2 or length args1 <> length args2
 572         then th::(GSYM th)::(DISEQUALITIES oths) else
 573         let zargs = zip args1 args2 in
 574         let diffs = filter (fun (a1,a2) -> a1 <> a2) zargs in
 575         if length diffs <> 1 then th::(GSYM th)::(DISEQUALITIES oths) else
 576         let eths = map (fun (a1,a2) ->
 577           if a1 = a2 then REFL a1 else ASSUME(mk_eq(a1,a2))) zargs in
 578         let th1 = rev_itlist (fun x y -> MK_COMB(y,x)) eths (REFL f1) in
 579         let th2 =
 580           MP (GEN_REWRITE_RULE I [GSYM CONTRAPOS_THM] (DISCH_ALL th1)) th in
 581         th::(GSYM th)::(DISEQUALITIES(th2::oths));;
 582
 583 (* ------------------------------------------------------------------------- *)
 584 (* Get such a starting inequality from complementary literals.               *)
 585 (* ------------------------------------------------------------------------- *)
 586
 587 let ATOMINEQUALITIES th1 th2 =
 588   let t1 = concl th1 and t2' = concl th2 in
 589   let t2 = dest_neg t2' in
 590   let f1,args1 = strip_comb t1
 591   and f2,args2 = strip_comb t2 in
 592   if f1 <> f2 or length args1 <> length args2 then [] else
 593   let zargs = zip args1 args2 in
 594   let diffs = filter (fun (a1,a2) -> a1 <> a2) zargs in
 595   if length diffs <> 1 then [] else
 596   let eths = map (fun (a1,a2) ->
 597     if a1 = a2 then REFL a1 else ASSUME(mk_eq(a1,a2))) zargs in
 598   let th3 = rev_itlist (fun x y -> MK_COMB(y,x)) eths (REFL f1) in
 599   let th4 = EQ_MP (TRANS th3 (EQF_INTRO th2)) th1 in
 600   let th5 = NOT_INTRO(itlist (DISCH o mk_eq) diffs th4) in
 601   [itlist PROVE_HYP [th1; th2] th5];;
 602
 603 (* ------------------------------------------------------------------------- *)
 604 (* Basic prover.                                                             *)
 605 (* ------------------------------------------------------------------------- *)
 606
 607 let BASIC_MIZARBY ths =
 608   try let nths,pths = partition (is_neg o concl) ths in
 609       let peqs,pneqs = partition (is_eq o concl) pths
 610       and neqs,nneqs = partition (is_eq o rand o concl) nths in
 611       let tps = map (dest_eq o concl) peqs @
 612                 map (dest_eq o rand o concl) neqs in
 613       let otms = itlist (fun (x,y) l -> x::y::l) tps [] in
 614       let tms = term_universe(setify otms) in
 615       let eqv = congruence_closure tms (map lazy_eq peqs) in
 616       let eqprover th =
 617         let s,t = dest_eq(rand(concl th)) in
 618         let th' = PROVE_EQUIVALENT eqv s t in
 619         EQ_MP (EQF_INTRO th) th'
 620       and contrprover thp thn =
 621         let th = PROVE_EQUIVALENT eqv (concl thp) (rand(concl thn)) in
 622         EQ_MP (TRANS th (EQF_INTRO thn)) thp in
 623       try tryfind eqprover neqs with Failure _ ->
 624       try tryfind (fun thp -> tryfind (contrprover thp) nneqs) pneqs
 625       with Failure _ ->
 626         let new_neqs = unions(allpairs ATOMINEQUALITIES pneqs nneqs) in
 627         let allths = pneqs @ nneqs @ peqs @ DISEQUALITIES(neqs @ new_neqs) in
 628         tryfind (MIZAR_UNIFIER eqv allths)
 629                 (filter (is_forall o concl) allths)
 630    with Failure _ -> failwith "BASIC_MIZARBY";;
 631
 632 (* ------------------------------------------------------------------------- *)
 633 (* Put it all together.                                                      *)
 634 (* ------------------------------------------------------------------------- *)
 635
 636 let MIZAR_REFUTER ths = PRECHECKER_THEN BASIC_MIZARBY ths;;
 637
 638 (* ------------------------------------------------------------------------- *)
 639 (* The Mizar prover for getting a conclusion from hypotheses.                *)
 640 (* ------------------------------------------------------------------------- *)
 641
 642 let MIZAR_BY =
 643   let pth = TAUT `(~p ==> F) <=> p` and p_tm = `p:bool` in
 644   fun ths tm ->
 645     let tm' = mk_neg tm in
 646     let th0 = ASSUME tm' in
 647     let th1 = MIZAR_REFUTER (th0::ths) in
 648     EQ_MP (INST [tm,p_tm] pth) (DISCH tm' th1);;
 649
 650 (* ------------------------------------------------------------------------- *)
 651 (* As a standalone prover of formulas.                                       *)
 652 (* ------------------------------------------------------------------------- *)
 653
 654 let MIZAR_RULE tm = MIZAR_BY [] tm;;
 655
 656 (* ------------------------------------------------------------------------- *)
 657 (* Some additional stuff for HOL.                                            *)
 658 (* ------------------------------------------------------------------------- *)
 659
 660 let HOL_BY =
 661   let BETASET_CONV =
 662     TOP_DEPTH_CONV GEN_BETA_CONV THENC REWRITE_CONV[IN_ELIM_THM]
 663   and BUILTIN_CONV tm =
 664     try EQT_ELIM(NUM_REDUCE_CONV tm) with Failure _ ->
 665     try EQT_ELIM(REAL_RAT_REDUCE_CONV tm) with Failure _ ->
 666     try ARITH_RULE tm with Failure _ ->
 667     try REAL_ARITH tm with Failure _ ->
 668     failwith "BUILTIN_CONV" in
 669   fun ths tm ->
 670     try MIZAR_BY ths tm with Failure _ ->
 671     try tryfind (fun th -> PART_MATCH I th tm) ths with Failure _ ->
 672     try let avs,bod = strip_forall tm in
 673         let gvs = map (genvar o type_of) avs in
 674         let gtm = vsubst (zip gvs avs) bod in
 675         let th = tryfind (fun th -> PART_MATCH I th gtm) ths in
 676         let gth = GENL gvs th in
 677         EQ_MP (ALPHA (concl gth) tm) gth
 678     with Failure _ -> try
 679        (let ths' = map BETA_RULE ths
 680         and th' = TOP_DEPTH_CONV BETA_CONV tm in
 681         let tm' = rand(concl th') in
 682         try EQ_MP (SYM th') (tryfind (fun th -> PART_MATCH I th tm') ths)
 683         with Failure _ -> try EQ_MP (SYM th') (BUILTIN_CONV tm')
 684         with Failure _ ->
 685           let ths'' = map (CONV_RULE BETASET_CONV) ths'
 686           and th'' = TRANS th' (BETASET_CONV tm') in
 687           EQ_MP (SYM th'') (prove(rand(concl th''),MESON_TAC ths'')))
 688     with Failure _ -> failwith "HOL_BY";;
 689
 690 (* ------------------------------------------------------------------------- *)
 691 (* Standalone prover, breaking down an implication first.                    *)
 692 (* ------------------------------------------------------------------------- *)
 693
 694 let HOL_RULE tm =
 695   try let l,r = dest_imp tm in
 696       DISCH l (HOL_BY (CONJUNCTS(ASSUME l)) r)
 697   with Failure _ -> HOL_BY [] tm;;
 698
 699 (* ------------------------------------------------------------------------- *)
 700 (* Tautology examples (Pelletier problems).                                  *)
 701 (* ------------------------------------------------------------------------- *)
 702
 703 let prop_1 = time HOL_RULE
 704  `p ==> q <=> ~q ==> ~p`;;
 705
 706 let prop_2 = time HOL_RULE
 707  `~ ~p <=> p`;;
 708
 709 let prop_3 = time HOL_RULE
 710  `~(p ==> q) ==> q ==> p`;;
 711
 712 let prop_4 = time HOL_RULE
 713  `~p ==> q <=> ~q ==> p`;;
 714
 715 let prop_5 = time HOL_RULE
 716  `(p \/ q ==> p \/ r) ==> p \/ (q ==> r)`;;
 717
 718 let prop_6 = time HOL_RULE
 719  `p \/ ~p`;;
 720
 721 let prop_7 = time HOL_RULE
 722  `p \/ ~ ~ ~p`;;
 723
 724 let prop_8 = time HOL_RULE
 725  `((p ==> q) ==> p) ==> p`;;
 726
 727 let prop_9 = time HOL_RULE
 728  `(p \/ q) /\ (~p \/ q) /\ (p \/ ~q) ==> ~(~q \/ ~q)`;;
 729
 730 let prop_10 = time HOL_RULE
 731  `(q ==> r) /\ (r ==> p /\ q) /\ (p ==> q /\ r) ==> (p <=> q)`;;
 732
 733 let prop_11 = time HOL_RULE
 734  `p <=> p`;;
 735
 736 let prop_12 = time HOL_RULE
 737  `((p <=> q) <=> r) <=> (p <=> (q <=> r))`;;
 738
 739 let prop_13 = time HOL_RULE
 740  `p \/ q /\ r <=> (p \/ q) /\ (p \/ r)`;;
 741
 742 let prop_14 = time HOL_RULE
 743  `(p <=> q) <=> (q \/ ~p) /\ (~q \/ p)`;;
 744
 745 let prop_15 = time HOL_RULE
 746  `p ==> q <=> ~p \/ q`;;
 747
 748 let prop_16 = time HOL_RULE
 749  `(p ==> q) \/ (q ==> p)`;;
 750
 751 let prop_17 = time HOL_RULE
 752  `p /\ (q ==> r) ==> s <=> (~p \/ q \/ s) /\ (~p \/ ~r \/ s)`;;
 753
 754 (* ------------------------------------------------------------------------- *)
 755 (* Congruence closure examples.                                              *)
 756 (* ------------------------------------------------------------------------- *)
 757
 758 time HOL_RULE
 759  `(f(f(f(f(f(x))))) = x) /\ (f(f(f(x))) = x) ==> (f(x) = x)`;;
 760
 761 time HOL_RULE
 762  `(f(f(f(f(f(f(x)))))) = x) /\ (f(f(f(f(x)))) = x) ==> (f(f(x)) = x)`;;
 763
 764 time HOL_RULE `(f a = a) ==> (f(f a) = a)`;;
 765
 766 time HOL_RULE
 767   `(a = f a) /\ ((g b (f a))=(f (f a))) /\ ((g a b)=(f (g b a)))
 768    ==> (g a b = a)`;;
 769
 770 time HOL_RULE
 771   `((s(s(s(s(s(s(s(s(s(s(s(s(s(s(s a)))))))))))))))=a) /\
 772    ((s (s (s (s (s (s (s (s (s (s a))))))))))=a) /\
 773    ((s (s (s (s (s (s a))))))=a)
 774    ==> (a = s a)`;;
 775
 776 time HOL_RULE `(u = v) ==> (P u <=> P v)`;;
 777
 778 time HOL_RULE
 779   `(b + c + d + e + f + g + h + i + j + k + l + m =
 780     m + l + k + j + i + h + g + f + e + d + c + b)
 781    ==> (a + b + c + d + e + f + g + h + i + j + k + l + m =
 782         a + m + l + k + j + i + h + g + f + e + d + c + b)`;;
 783
 784 time HOL_RULE
 785   `(f(f(f(f(a)))) = a) /\ (f(f(f(f(f(f(a)))))) = a) /\
 786    something(irrelevant) /\ (11 + 12 = 23) /\
 787    (f(f(f(f(b)))) = f(f(f(f(f(f(f(f(f(f(c))))))))))) /\
 788    ~(otherthing) /\ ~(f(a) = a) /\ ~(f(b) = b) /\
 789    P(f(f(f(a)))) ==> P(f(a))`;;
 790
 791 time HOL_RULE
 792   `((a = b) \/ (c = d)) /\ ((a = c) \/ (b = d)) ==> (a = d) \/ (b = c)`;;
 793
 794 (* ------------------------------------------------------------------------- *)
 795 (* Various combined examples.                                                *)
 796 (* ------------------------------------------------------------------------- *)
 797
 798 time HOL_RULE
 799   `(f(f(f(f(a:A)))) = a) /\ (f(f(f(f(f(f(a)))))) = a) /\
 800    something(irrelevant) /\ (11 + 12 = 23) /\
 801    (f(f(f(f(b:A)))) = f(f(f(f(f(f(f(f(f(f(c))))))))))) /\
 802    ~(otherthing) /\ ~(f(a) = a) /\ ~(f(b) = b) /\
 803    P(f(a)) /\ ~(f(f(f(a))) = f(a)) ==> ?x. P(f(f(f(x))))`;;
 804
 805 time HOL_RULE
 806   `(f(f(f(f(a:A)))) = a) /\ (f(f(f(f(f(f(a)))))) = a) /\
 807    something(irrelevant) /\ (11 + 12 = 23) /\
 808    (f(f(f(f(b:A)))) = f(f(f(f(f(f(f(f(f(f(c))))))))))) /\
 809    ~(otherthing) /\ ~(f(a) = a) /\ ~(f(b) = b) /\
 810    P(f(a))
 811    ==> P(f(f(f(a))))`;;
 812
 813 time HOL_RULE
 814   `(f(f(f(f(a:A)))) = a) /\ (f(f(f(f(f(f(a)))))) = a) /\
 815    something(irrelevant) /\ (11 + 12 = 23) /\
 816    (f(f(f(f(b:A)))) = f(f(f(f(f(f(f(f(f(f(c))))))))))) /\
 817    ~(otherthing) /\ ~(f(a) = a) /\ ~(f(b) = b) /\
 818    P(f(a))
 819    ==> ?x. P(f(f(f(x))))`;;
 820
 821 time HOL_RULE
 822   `(a = f a) /\ ((g b (f a))=(f (f a))) /\ ((g a b)=(f (g b a))) /\
 823    (!x y. ~P (g x y))
 824    ==> ~P(a)`;;
 825
 826 time HOL_RULE
 827  `(!x y. x + y = y + x) /\ (1 + 2 = x) /\ (x = 3) ==> (3 = 2 + 1)`;;
 828
 829 time HOL_RULE
 830  `(!x:num y. x + y = y + x) ==> (1 + 2 = 2 + 1)`;;
 831
 832 time HOL_RULE
 833  `(!x:num y. ~(x + y = y + x)) ==> ~(1 + 2 = 2 + 1)`;;
 834
 835 time HOL_RULE
 836  `(1 + 2 = 2 + 1) ==> ?x:num y. x + y = y + x`;;
 837
 838 time HOL_RULE
 839  `(1 + x = x + 1) ==> ?x:num y. x + y = y + x`;;
 840
 841 time (HOL_BY []) `?x. P x ==> !y. P y`;;
 842
 843 (* ------------------------------------------------------------------------- *)
 844 (* Testing the HOL extensions.                                               *)
 845 (* ------------------------------------------------------------------------- *)
 846
 847 time HOL_RULE `1 + 1 = 2`;;
 848
 849 time HOL_RULE `(\x. x + 1) 2 = 2 + 1`;;
 850
 851 time HOL_RULE `!x. x < 2 ==> 2 * x <= 3`;;
 852
 853 time HOL_RULE `y IN {x | x < 2} <=> y < 2`;;
 854
 855 time HOL_RULE `(!x. (x = a) \/ x > a) ==> (1 + x = a) \/ 1 + x > a`;;
 856
 857 time HOL_RULE `(\(x,y). x + y)(1,2) + 5 = (1 + 2) + 5`;;
 858
 859 (* ------------------------------------------------------------------------- *)
 860 (* These and only these should go to MESON.                                  *)
 861 (* ------------------------------------------------------------------------- *)
 862
 863 print_string "***** Now the following (only) should use MESON";
 864 print_newline();;
 865
 866 time HOL_RULE `?x y. x = y`;;
 867
 868 time HOL_RULE `(!Y X Z. p(X,Y) /\ p(Y,Z) ==> p(X,Z)) /\
 869                (!Y X Z. q(X,Y) /\ q(Y,Z) ==> q(X,Z)) /\
 870                (!Y X. q(X,Y) ==> q(Y,X)) /\
 871                (!X Y. p(X,Y) \/ q(X,Y))
 872                ==> p(a,b) \/ q(c,d)`;;
 873
 874 time HOL_BY [PAIR_EQ] `(1,2) IN {(x,y) | x < y} <=> 1 < 2`;;
 875
 876 HOL_BY [] `?x. !y. P x ==> P y`;;