<commit_before>(*  Title:      FOL/FOL.ML
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Tactics and lemmas for FOL.thy (classical First-Order Logic)
*)

open FOL;


val ccontr = FalseE RS classical;

(*** Classical introduction rules for | and EX ***)

qed_goal "disjCI" FOL.thy 
   "(~Q ==> P) ==> P|Q"
 (fn prems=>
  [ (rtac classical 1),
    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);

(*introduction rule involving only EX*)
qed_goal "ex_classical" FOL.thy 
   "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
 (fn prems=>
  [ (rtac classical 1),
    (eresolve_tac (prems RL [exI]) 1) ]);

(*version of above, simplifying ~EX to ALL~ *)
qed_goal "exCI" FOL.thy 
   "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
 (fn [prem]=>
  [ (rtac ex_classical 1),
    (resolve_tac [notI RS allI RS prem] 1),
    (etac notE 1),
    (etac exI 1) ]);

qed_goal "excluded_middle" FOL.thy "~P | P"
 (fn _=> [ rtac disjCI 1, assume_tac 1 ]);

(*For disjunctive case analysis*)
fun excluded_middle_tac sP =
    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);

(*** Special elimination rules *)


(*Classical implies (-->) elimination. *)
qed_goal "impCE" FOL.thy 
    "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
 (fn major::prems=>
  [ (resolve_tac [excluded_middle RS disjE] 1),
    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);

(*Double negation law*)
qed_goal "notnotD" FOL.thy "~~P ==> P"
 (fn [major]=>
  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);

qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
        rtac classical 1,
        dtac p2 1,
        etac notE 1,
        rtac p1 1]);

(*** Tactics for implication and contradiction ***)

(*Classical <-> elimination.  Proof substitutes P=Q in 
    ~P ==> ~Q    and    P ==> Q  *)
qed_goalw "iffCE" FOL.thy [iff_def]
    "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
 (fn prems =>
  [ (rtac conjE 1),
    (REPEAT (DEPTH_SOLVE_1 
        (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);

<commit_msg>Added rule impCE'<commit_after>(*  Title:      FOL/FOL.ML
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Tactics and lemmas for FOL.thy (classical First-Order Logic)
*)

open FOL;


val ccontr = FalseE RS classical;

(*** Classical introduction rules for | and EX ***)

qed_goal "disjCI" FOL.thy 
   "(~Q ==> P) ==> P|Q"
 (fn prems=>
  [ (rtac classical 1),
    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);

(*introduction rule involving only EX*)
qed_goal "ex_classical" FOL.thy 
   "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
 (fn prems=>
  [ (rtac classical 1),
    (eresolve_tac (prems RL [exI]) 1) ]);

(*version of above, simplifying ~EX to ALL~ *)
qed_goal "exCI" FOL.thy 
   "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
 (fn [prem]=>
  [ (rtac ex_classical 1),
    (resolve_tac [notI RS allI RS prem] 1),
    (etac notE 1),
    (etac exI 1) ]);

qed_goal "excluded_middle" FOL.thy "~P | P"
 (fn _=> [ rtac disjCI 1, assume_tac 1 ]);

(*For disjunctive case analysis*)
fun excluded_middle_tac sP =
    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);

(*** Special elimination rules *)


(*Classical implies (-->) elimination. *)
qed_goal "impCE" FOL.thy 
    "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
 (fn major::prems=>
  [ (resolve_tac [excluded_middle RS disjE] 1),
    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);

(*This version of --> elimination works on Q before P.  It works best for
  those cases in which P holds "almost everywhere".  Can't install as
  default: would break old proofs.*)
qed_goal "impCE'" thy 
    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
 (fn major::prems=>
  [ (resolve_tac [excluded_middle RS disjE] 1),
    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);

(*Double negation law*)
qed_goal "notnotD" FOL.thy "~~P ==> P"
 (fn [major]=>
  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);

qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
        rtac classical 1,
        dtac p2 1,
        etac notE 1,
        rtac p1 1]);

(*** Tactics for implication and contradiction ***)

(*Classical <-> elimination.  Proof substitutes P=Q in 
    ~P ==> ~Q    and    P ==> Q  *)
qed_goalw "iffCE" FOL.thy [iff_def]
    "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
 (fn prems =>
  [ (rtac conjE 1),
    (REPEAT (DEPTH_SOLVE_1 
        (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);


{'fraction_non_alphanumeric': 0.18671224097415082, 'fraction_numerical': 0.015381328775902585, 'mean_word_length': 3.0855148342059335, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 69, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2828588', 'n_tokens_mistral': 2060, 'n_tokens_neox': 1941, 'n_words': 555}