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