src/FOL/FOL.ML
changeset 7355 4c43090659ca
parent 5159 8fc4fb20d70f
child 7529 fa534e4f7e49
equal deleted inserted replaced
7354:358b1c5391f0 7355:4c43090659ca
     1 (*  Title:      FOL/FOL.ML
       
     2     ID:         $Id$
       
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
       
     4     Copyright   1991  University of Cambridge
       
     5 
     1 
     6 Tactics and lemmas for FOL.thy (classical First-Order Logic)
     2 structure FOL =
     7 *)
     3 struct
       
     4   val thy = the_context ();
       
     5   val classical = classical;
       
     6 end;
     8 
     7 
     9 open FOL;
     8 open FOL;
    10 
       
    11 
       
    12 val ccontr = FalseE RS classical;
       
    13 
       
    14 (*** Classical introduction rules for | and EX ***)
       
    15 
       
    16 qed_goal "disjCI" FOL.thy 
       
    17    "(~Q ==> P) ==> P|Q"
       
    18  (fn prems=>
       
    19   [ (rtac classical 1),
       
    20     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
       
    21     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
       
    22 
       
    23 (*introduction rule involving only EX*)
       
    24 qed_goal "ex_classical" FOL.thy 
       
    25    "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
       
    26  (fn prems=>
       
    27   [ (rtac classical 1),
       
    28     (eresolve_tac (prems RL [exI]) 1) ]);
       
    29 
       
    30 (*version of above, simplifying ~EX to ALL~ *)
       
    31 qed_goal "exCI" FOL.thy 
       
    32    "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
       
    33  (fn [prem]=>
       
    34   [ (rtac ex_classical 1),
       
    35     (resolve_tac [notI RS allI RS prem] 1),
       
    36     (etac notE 1),
       
    37     (etac exI 1) ]);
       
    38 
       
    39 qed_goal "excluded_middle" FOL.thy "~P | P"
       
    40  (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
       
    41 
       
    42 (*For disjunctive case analysis*)
       
    43 fun excluded_middle_tac sP =
       
    44     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
       
    45 
       
    46 qed_goal "case_split_thm" FOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
       
    47   (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
       
    48                   etac p2 1, etac p1 1]);
       
    49 
       
    50 (*HOL's more natural case analysis tactic*)
       
    51 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
       
    52 
       
    53 
       
    54 (*** Special elimination rules *)
       
    55 
       
    56 
       
    57 (*Classical implies (-->) elimination. *)
       
    58 qed_goal "impCE" FOL.thy 
       
    59     "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
       
    60  (fn major::prems=>
       
    61   [ (resolve_tac [excluded_middle RS disjE] 1),
       
    62     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
       
    63 
       
    64 (*This version of --> elimination works on Q before P.  It works best for
       
    65   those cases in which P holds "almost everywhere".  Can't install as
       
    66   default: would break old proofs.*)
       
    67 qed_goal "impCE'" thy 
       
    68     "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
       
    69  (fn major::prems=>
       
    70   [ (resolve_tac [excluded_middle RS disjE] 1),
       
    71     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
       
    72 
       
    73 (*Double negation law*)
       
    74 qed_goal "notnotD" FOL.thy "~~P ==> P"
       
    75  (fn [major]=>
       
    76   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
       
    77 
       
    78 qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
       
    79         rtac classical 1,
       
    80         dtac p2 1,
       
    81         etac notE 1,
       
    82         rtac p1 1]);
       
    83 
       
    84 (*** Tactics for implication and contradiction ***)
       
    85 
       
    86 (*Classical <-> elimination.  Proof substitutes P=Q in 
       
    87     ~P ==> ~Q    and    P ==> Q  *)
       
    88 qed_goalw "iffCE" FOL.thy [iff_def]
       
    89     "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
       
    90  (fn prems =>
       
    91   [ (rtac conjE 1),
       
    92     (REPEAT (DEPTH_SOLVE_1 
       
    93         (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
       
    94