src/FOL/FOL.ML
changeset 7355 4c43090659ca
parent 5159 8fc4fb20d70f
child 7529 fa534e4f7e49
     1.1 --- a/src/FOL/FOL.ML	Wed Aug 25 20:42:01 1999 +0200
     1.2 +++ b/src/FOL/FOL.ML	Wed Aug 25 20:45:19 1999 +0200
     1.3 @@ -1,94 +1,8 @@
     1.4 -(*  Title:      FOL/FOL.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8  
     1.9 -Tactics and lemmas for FOL.thy (classical First-Order Logic)
    1.10 -*)
    1.11 +structure FOL =
    1.12 +struct
    1.13 +  val thy = the_context ();
    1.14 +  val classical = classical;
    1.15 +end;
    1.16  
    1.17  open FOL;
    1.18 -
    1.19 -
    1.20 -val ccontr = FalseE RS classical;
    1.21 -
    1.22 -(*** Classical introduction rules for | and EX ***)
    1.23 -
    1.24 -qed_goal "disjCI" FOL.thy 
    1.25 -   "(~Q ==> P) ==> P|Q"
    1.26 - (fn prems=>
    1.27 -  [ (rtac classical 1),
    1.28 -    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    1.29 -    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
    1.30 -
    1.31 -(*introduction rule involving only EX*)
    1.32 -qed_goal "ex_classical" FOL.thy 
    1.33 -   "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
    1.34 - (fn prems=>
    1.35 -  [ (rtac classical 1),
    1.36 -    (eresolve_tac (prems RL [exI]) 1) ]);
    1.37 -
    1.38 -(*version of above, simplifying ~EX to ALL~ *)
    1.39 -qed_goal "exCI" FOL.thy 
    1.40 -   "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
    1.41 - (fn [prem]=>
    1.42 -  [ (rtac ex_classical 1),
    1.43 -    (resolve_tac [notI RS allI RS prem] 1),
    1.44 -    (etac notE 1),
    1.45 -    (etac exI 1) ]);
    1.46 -
    1.47 -qed_goal "excluded_middle" FOL.thy "~P | P"
    1.48 - (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    1.49 -
    1.50 -(*For disjunctive case analysis*)
    1.51 -fun excluded_middle_tac sP =
    1.52 -    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
    1.53 -
    1.54 -qed_goal "case_split_thm" FOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
    1.55 -  (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
    1.56 -                  etac p2 1, etac p1 1]);
    1.57 -
    1.58 -(*HOL's more natural case analysis tactic*)
    1.59 -fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
    1.60 -
    1.61 -
    1.62 -(*** Special elimination rules *)
    1.63 -
    1.64 -
    1.65 -(*Classical implies (-->) elimination. *)
    1.66 -qed_goal "impCE" FOL.thy 
    1.67 -    "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
    1.68 - (fn major::prems=>
    1.69 -  [ (resolve_tac [excluded_middle RS disjE] 1),
    1.70 -    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    1.71 -
    1.72 -(*This version of --> elimination works on Q before P.  It works best for
    1.73 -  those cases in which P holds "almost everywhere".  Can't install as
    1.74 -  default: would break old proofs.*)
    1.75 -qed_goal "impCE'" thy 
    1.76 -    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
    1.77 - (fn major::prems=>
    1.78 -  [ (resolve_tac [excluded_middle RS disjE] 1),
    1.79 -    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    1.80 -
    1.81 -(*Double negation law*)
    1.82 -qed_goal "notnotD" FOL.thy "~~P ==> P"
    1.83 - (fn [major]=>
    1.84 -  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
    1.85 -
    1.86 -qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
    1.87 -        rtac classical 1,
    1.88 -        dtac p2 1,
    1.89 -        etac notE 1,
    1.90 -        rtac p1 1]);
    1.91 -
    1.92 -(*** Tactics for implication and contradiction ***)
    1.93 -
    1.94 -(*Classical <-> elimination.  Proof substitutes P=Q in 
    1.95 -    ~P ==> ~Q    and    P ==> Q  *)
    1.96 -qed_goalw "iffCE" FOL.thy [iff_def]
    1.97 -    "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
    1.98 - (fn prems =>
    1.99 -  [ (rtac conjE 1),
   1.100 -    (REPEAT (DEPTH_SOLVE_1 
   1.101 -        (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
   1.102 -