src/Provers/classical.ML
changeset 26412 0918f5c0bbca
parent 24867 e5b55d7be9bb
child 26425 6561665c5cb1
     1.1 --- a/src/Provers/classical.ML	Wed Mar 26 22:40:01 2008 +0100
     1.2 +++ b/src/Provers/classical.ML	Wed Mar 26 22:40:02 2008 +0100
     1.3 @@ -27,9 +27,10 @@
     1.4  
     1.5  signature CLASSICAL_DATA =
     1.6  sig
     1.7 -  val mp        : thm           (* [| P-->Q;  P |] ==> Q *)
     1.8 -  val not_elim  : thm           (* [| ~P;  P |] ==> R *)
     1.9 -  val classical : thm           (* (~P ==> P) ==> P *)
    1.10 +  val imp_elim  : thm           (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
    1.11 +  val not_elim  : thm           (* ~P ==> P ==> R *)
    1.12 +  val swap      : thm           (* ~ P ==> (~ R ==> P) ==> R *)
    1.13 +  val classical : thm           (* (~ P ==> P) ==> P *)
    1.14    val sizef     : thm -> int    (* size function for BEST_FIRST *)
    1.15    val hyp_subst_tacs: (int -> tactic) list
    1.16  end;
    1.17 @@ -133,7 +134,6 @@
    1.18  signature CLASSICAL =
    1.19  sig
    1.20    include BASIC_CLASSICAL
    1.21 -  val swap: thm  (* ~P ==> (~Q ==> P) ==> Q *)
    1.22    val classical_rule: thm -> thm
    1.23    val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
    1.24    val del_context_safe_wrapper: string -> theory -> theory
    1.25 @@ -206,9 +206,6 @@
    1.26  
    1.27  (*** Useful tactics for classical reasoning ***)
    1.28  
    1.29 -val imp_elim = (*cannot use bind_thm within a structure!*)
    1.30 -  store_thm ("imp_elim", Thm.transfer (the_context ()) (classical_rule (Tactic.make_elim mp)));
    1.31 -
    1.32  (*Prove goal that assumes both P and ~P.
    1.33    No backtracking if it finds an equal assumption.  Perhaps should call
    1.34    ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
    1.35 @@ -217,23 +214,19 @@
    1.36  
    1.37  (*Finds P-->Q and P in the assumptions, replaces implication by Q.
    1.38    Could do the same thing for P<->Q and P... *)
    1.39 -fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;
    1.40 +fun mp_tac i = eresolve_tac [not_elim, Data.imp_elim] i  THEN  assume_tac i;
    1.41  
    1.42  (*Like mp_tac but instantiates no variables*)
    1.43 -fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
    1.44 -
    1.45 -val swap =
    1.46 -  store_thm ("swap", Thm.transfer (the_context ())
    1.47 -    (rule_by_tactic (etac thin_rl 1) (not_elim RS classical)));
    1.48 +fun eq_mp_tac i = ematch_tac [not_elim, Data.imp_elim] i  THEN  eq_assume_tac i;
    1.49  
    1.50  (*Creates rules to eliminate ~A, from rules to introduce A*)
    1.51 -fun swapify intrs = intrs RLN (2, [swap]);
    1.52 -fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, swap))) x;
    1.53 +fun swapify intrs = intrs RLN (2, [Data.swap]);
    1.54 +fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, Data.swap))) x;
    1.55  
    1.56  (*Uses introduction rules in the normal way, or on negated assumptions,
    1.57    trying rules in order. *)
    1.58  fun swap_res_tac rls =
    1.59 -    let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
    1.60 +    let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
    1.61      in  assume_tac      ORELSE'
    1.62          contr_tac       ORELSE'
    1.63          biresolve_tac (foldr addrl [] rls)