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