src/FOL/FOL.ML
author wenzelm
Mon, 16 Nov 1998 11:33:42 +0100
changeset 5896 4a75d89e2818
parent 5159 8fc4fb20d70f
child 7355 4c43090659ca
permissions -rw-r--r--
thm, thms;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1459
d12da312eff4 expanded tabs
clasohm
parents: 1280
diff changeset
     1
(*  Title:      FOL/FOL.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 1280
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
1280
909079af97b7 corrected spelling of title
clasohm
parents: 779
diff changeset
     6
Tactics and lemmas for FOL.thy (classical First-Order Logic)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open FOL;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
2576
390c9fb786b5 Declaration of ccontr (classical contradiction) for HOL compatibility
paulson
parents: 2469
diff changeset
    12
val ccontr = FalseE RS classical;
390c9fb786b5 Declaration of ccontr (classical contradiction) for HOL compatibility
paulson
parents: 2469
diff changeset
    13
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
(*** Classical introduction rules for | and EX ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
779
4ab9176b45b7 removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
clasohm
parents: 677
diff changeset
    16
qed_goal "disjCI" FOL.thy 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
   "(~Q ==> P) ==> P|Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
 (fn prems=>
1459
d12da312eff4 expanded tabs
clasohm
parents: 1280
diff changeset
    19
  [ (rtac classical 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
(*introduction rule involving only EX*)
779
4ab9176b45b7 removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
clasohm
parents: 677
diff changeset
    24
qed_goal "ex_classical" FOL.thy 
3835
9a5a4e123859 fixed dots;
wenzelm
parents: 2576
diff changeset
    25
   "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
 (fn prems=>
1459
d12da312eff4 expanded tabs
clasohm
parents: 1280
diff changeset
    27
  [ (rtac classical 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
    (eresolve_tac (prems RL [exI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
(*version of above, simplifying ~EX to ALL~ *)
779
4ab9176b45b7 removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
clasohm
parents: 677
diff changeset
    31
qed_goal "exCI" FOL.thy 
3835
9a5a4e123859 fixed dots;
wenzelm
parents: 2576
diff changeset
    32
   "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
 (fn [prem]=>
1459
d12da312eff4 expanded tabs
clasohm
parents: 1280
diff changeset
    34
  [ (rtac ex_classical 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
    (resolve_tac [notI RS allI RS prem] 1),
1459
d12da312eff4 expanded tabs
clasohm
parents: 1280
diff changeset
    36
    (etac notE 1),
d12da312eff4 expanded tabs
clasohm
parents: 1280
diff changeset
    37
    (etac exI 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
779
4ab9176b45b7 removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
clasohm
parents: 677
diff changeset
    39
qed_goal "excluded_middle" FOL.thy "~P | P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
 (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
440
1577cbcd0936 FOL/FOL.ML/excluded_middle_tac: new
lcp
parents: 0
diff changeset
    42
(*For disjunctive case analysis*)
1577cbcd0936 FOL/FOL.ML/excluded_middle_tac: new
lcp
parents: 0
diff changeset
    43
fun excluded_middle_tac sP =
1577cbcd0936 FOL/FOL.ML/excluded_middle_tac: new
lcp
parents: 0
diff changeset
    44
    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
5159
8fc4fb20d70f added case_tac to be like HOL
paulson
parents: 4308
diff changeset
    46
qed_goal "case_split_thm" FOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
8fc4fb20d70f added case_tac to be like HOL
paulson
parents: 4308
diff changeset
    47
  (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
8fc4fb20d70f added case_tac to be like HOL
paulson
parents: 4308
diff changeset
    48
                  etac p2 1, etac p1 1]);
8fc4fb20d70f added case_tac to be like HOL
paulson
parents: 4308
diff changeset
    49
8fc4fb20d70f added case_tac to be like HOL
paulson
parents: 4308
diff changeset
    50
(*HOL's more natural case analysis tactic*)
8fc4fb20d70f added case_tac to be like HOL
paulson
parents: 4308
diff changeset
    51
fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
8fc4fb20d70f added case_tac to be like HOL
paulson
parents: 4308
diff changeset
    52
8fc4fb20d70f added case_tac to be like HOL
paulson
parents: 4308
diff changeset
    53
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
(*** Special elimination rules *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
(*Classical implies (-->) elimination. *)
779
4ab9176b45b7 removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
clasohm
parents: 677
diff changeset
    58
qed_goal "impCE" FOL.thy 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
    "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
  [ (resolve_tac [excluded_middle RS disjE] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
4308
9abce31cc764 Added rule impCE'
paulson
parents: 4186
diff changeset
    64
(*This version of --> elimination works on Q before P.  It works best for
9abce31cc764 Added rule impCE'
paulson
parents: 4186
diff changeset
    65
  those cases in which P holds "almost everywhere".  Can't install as
9abce31cc764 Added rule impCE'
paulson
parents: 4186
diff changeset
    66
  default: would break old proofs.*)
9abce31cc764 Added rule impCE'
paulson
parents: 4186
diff changeset
    67
qed_goal "impCE'" thy 
9abce31cc764 Added rule impCE'
paulson
parents: 4186
diff changeset
    68
    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
9abce31cc764 Added rule impCE'
paulson
parents: 4186
diff changeset
    69
 (fn major::prems=>
9abce31cc764 Added rule impCE'
paulson
parents: 4186
diff changeset
    70
  [ (resolve_tac [excluded_middle RS disjE] 1),
9abce31cc764 Added rule impCE'
paulson
parents: 4186
diff changeset
    71
    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
9abce31cc764 Added rule impCE'
paulson
parents: 4186
diff changeset
    72
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
(*Double negation law*)
779
4ab9176b45b7 removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
clasohm
parents: 677
diff changeset
    74
qed_goal "notnotD" FOL.thy "~~P ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
 (fn [major]=>
1459
d12da312eff4 expanded tabs
clasohm
parents: 1280
diff changeset
    76
  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
4186
e39f28f94cf8 added contrapos2
oheimb
parents: 4096
diff changeset
    78
qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
e39f28f94cf8 added contrapos2
oheimb
parents: 4096
diff changeset
    79
        rtac classical 1,
e39f28f94cf8 added contrapos2
oheimb
parents: 4096
diff changeset
    80
        dtac p2 1,
e39f28f94cf8 added contrapos2
oheimb
parents: 4096
diff changeset
    81
        etac notE 1,
e39f28f94cf8 added contrapos2
oheimb
parents: 4096
diff changeset
    82
        rtac p1 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
(*** Tactics for implication and contradiction ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
(*Classical <-> elimination.  Proof substitutes P=Q in 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
    ~P ==> ~Q    and    P ==> Q  *)
779
4ab9176b45b7 removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
clasohm
parents: 677
diff changeset
    88
qed_goalw "iffCE" FOL.thy [iff_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
    "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
 (fn prems =>
1459
d12da312eff4 expanded tabs
clasohm
parents: 1280
diff changeset
    91
  [ (rtac conjE 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
    (REPEAT (DEPTH_SOLVE_1 
1459
d12da312eff4 expanded tabs
clasohm
parents: 1280
diff changeset
    93
        (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1459
diff changeset
    94