Added rule impCE'
authorpaulson
Wed Nov 26 17:23:18 1997 +0100 (1997-11-26)
changeset 43022c99775d953f
parent 4301 ed343192de45
child 4303 c872cc541db2
Added rule impCE'
src/HOL/HOL.ML
     1.1 --- a/src/HOL/HOL.ML	Wed Nov 26 17:16:48 1997 +0100
     1.2 +++ b/src/HOL/HOL.ML	Wed Nov 26 17:23:18 1997 +0100
     1.3 @@ -321,6 +321,15 @@
     1.4    [ rtac (excluded_middle RS disjE) 1,
     1.5      REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
     1.6  
     1.7 +(*This version of --> elimination works on Q before P.  It works best for
     1.8 +  those cases in which P holds "almost everywhere".  Can't install as
     1.9 +  default: would break old proofs.*)
    1.10 +qed_goal "impCE'" thy 
    1.11 +    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
    1.12 + (fn major::prems=>
    1.13 +  [ (resolve_tac [excluded_middle RS disjE] 1),
    1.14 +    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    1.15 +
    1.16  (*Classical <-> elimination. *)
    1.17  qed_goal "iffCE" HOL.thy
    1.18      "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"