src/Sequents/LK0.ML
author paulson
Wed Jul 28 13:55:02 1999 +0200 (1999-07-28)
changeset 7122 87b233b31889
parent 7093 b2ee0e5d1a7f
child 9259 103acc345f75
permissions -rw-r--r--
renamed ...thm_pack... to ...pack...
paulson@7093
     1
(*  Title:      LK/LK0
paulson@7093
     2
    ID:         $Id$
paulson@7093
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7093
     4
    Copyright   1992  University of Cambridge
paulson@7093
     5
paulson@7093
     6
Tactics and lemmas for LK (thanks also to Philippe de Groote)  
paulson@7093
     7
paulson@7093
     8
Structural rules by Soren Heilmann
paulson@7093
     9
*)
paulson@7093
    10
paulson@7093
    11
(** Structural Rules on formulas **)
paulson@7093
    12
paulson@7093
    13
(*contraction*)
paulson@7093
    14
paulson@7093
    15
Goal "$H |- $E, P, P, $F ==> $H |- $E, P, $F";
paulson@7093
    16
by (etac contRS 1);
paulson@7093
    17
qed "contR";
paulson@7093
    18
paulson@7093
    19
Goal "$H, P, P, $G |- $E ==> $H, P, $G |- $E";
paulson@7093
    20
by (etac contLS 1);
paulson@7093
    21
qed "contL";
paulson@7093
    22
paulson@7093
    23
(*thinning*)
paulson@7093
    24
paulson@7093
    25
Goal "$H |- $E, $F ==> $H |- $E, P, $F";
paulson@7093
    26
by (etac thinRS 1);
paulson@7093
    27
qed "thinR";
paulson@7093
    28
paulson@7093
    29
Goal "$H, $G |- $E ==> $H, P, $G |- $E";
paulson@7093
    30
by (etac thinLS 1);
paulson@7093
    31
qed "thinL";
paulson@7093
    32
paulson@7093
    33
(*exchange*)
paulson@7093
    34
paulson@7093
    35
Goal "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F";
paulson@7093
    36
by (etac exchRS 1);
paulson@7093
    37
qed "exchR";
paulson@7093
    38
paulson@7093
    39
Goal "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E";
paulson@7093
    40
by (etac exchLS 1);
paulson@7093
    41
qed "exchL";
paulson@7093
    42
paulson@7093
    43
(*Cut and thin, replacing the right-side formula*)
paulson@7093
    44
fun cutR_tac (sP: string) i = 
paulson@7093
    45
    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
paulson@7093
    46
paulson@7093
    47
(*Cut and thin, replacing the left-side formula*)
paulson@7093
    48
fun cutL_tac (sP: string) i = 
paulson@7093
    49
    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
paulson@7093
    50
paulson@7093
    51
paulson@7093
    52
(** If-and-only-if rules **)
paulson@7122
    53
Goalw [iff_def] 
paulson@7122
    54
    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F";
paulson@7122
    55
by (REPEAT (ares_tac [conjR,impR] 1));
paulson@7122
    56
qed "iffR";
paulson@7122
    57
paulson@7122
    58
Goalw [iff_def] 
paulson@7122
    59
    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E";
paulson@7122
    60
by (REPEAT (ares_tac [conjL,impL,basic] 1));
paulson@7122
    61
qed "iffL";
paulson@7122
    62
paulson@7122
    63
Goal "$H |- $E, (P <-> P), $F";
paulson@7122
    64
by (REPEAT (resolve_tac [iffR,basic] 1));
paulson@7122
    65
qed "iff_refl";
paulson@7093
    66
paulson@7122
    67
Goalw [True_def] "$H |- $E, True, $F";
paulson@7122
    68
by (rtac impR 1);
paulson@7122
    69
by (rtac basic 1);
paulson@7122
    70
qed "TrueR";
paulson@7093
    71
paulson@7122
    72
(*Descriptions*)
paulson@7122
    73
val [p1,p2] = Goal
paulson@7122
    74
    "[| $H |- $E, P(a), $F;  !!x. $H, P(x) |- $E, x=a, $F |] \
paulson@7122
    75
\    ==> $H |- $E, (THE x. P(x)) = a, $F";
paulson@7122
    76
by (rtac cut 1);
paulson@7122
    77
by (rtac p2 2);
paulson@7122
    78
by (rtac The 1 THEN rtac thinR 1 THEN rtac exchRS 1 THEN rtac p1 1);
paulson@7122
    79
by (rtac thinR 1 THEN rtac exchRS 1 THEN rtac p2 1);
paulson@7122
    80
qed "the_equality";
paulson@7093
    81
paulson@7093
    82
(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
paulson@7093
    83
paulson@7093
    84
Goal "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E";
paulson@7093
    85
by (rtac allL 1);
paulson@7093
    86
by (etac thinL 1);
paulson@7093
    87
qed "allL_thin";
paulson@7093
    88
paulson@7093
    89
Goal "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F";
paulson@7093
    90
by (rtac exR 1);
paulson@7093
    91
by (etac thinR 1);
paulson@7093
    92
qed "exR_thin";
paulson@7093
    93
paulson@7093
    94
paulson@7093
    95
(*The rules of LK*)
paulson@7093
    96
val prop_pack = empty_pack add_safes 
paulson@7093
    97
                [basic, refl, TrueR, FalseL, 
paulson@7093
    98
		 conjL, conjR, disjL, disjR, impL, impR, 
paulson@7093
    99
                 notL, notR, iffL, iffR];
paulson@7093
   100
paulson@7093
   101
val LK_pack = prop_pack add_safes   [allR, exL] 
paulson@7122
   102
                        add_unsafes [allL_thin, exR_thin, the_equality];
paulson@7093
   103
paulson@7093
   104
val LK_dup_pack = prop_pack add_safes   [allR, exL] 
paulson@7122
   105
                            add_unsafes [allL, exR, the_equality];
paulson@7093
   106
paulson@7093
   107
paulson@7122
   108
pack_ref() := LK_pack;
paulson@7093
   109
paulson@7093
   110
fun lemma_tac th i = 
paulson@7093
   111
    rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
paulson@7093
   112
paulson@7093
   113
val [major,minor] = goal thy 
paulson@7093
   114
    "[| $H |- $E, $F, P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
paulson@7093
   115
by (rtac (thinRS RS cut) 1 THEN rtac major 1);
paulson@7093
   116
by (Step_tac 1);
paulson@7093
   117
by (rtac thinR 1 THEN rtac minor 1);
paulson@7093
   118
qed "mp_R";
paulson@7093
   119
paulson@7093
   120
val [major,minor] = goal thy 
paulson@7093
   121
    "[| $H, $G |- $E, P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
paulson@7093
   122
by (rtac (thinL RS cut) 1 THEN rtac major 1);
paulson@7093
   123
by (Step_tac 1);
paulson@7093
   124
by (rtac thinL 1 THEN rtac minor 1);
paulson@7093
   125
qed "mp_L";
paulson@7093
   126
paulson@7093
   127
paulson@7093
   128
(** Two rules to generate left- and right- rules from implications **)
paulson@7093
   129
paulson@7093
   130
val [major,minor] = goal thy 
paulson@7093
   131
    "[| |- P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
paulson@7093
   132
by (rtac mp_R 1);
paulson@7093
   133
by (rtac minor 2);
paulson@7093
   134
by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
paulson@7093
   135
qed "R_of_imp";
paulson@7093
   136
paulson@7093
   137
val [major,minor] = goal thy 
paulson@7093
   138
    "[| |- P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
paulson@7093
   139
by (rtac mp_L 1);
paulson@7093
   140
by (rtac minor 2);
paulson@7093
   141
by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
paulson@7093
   142
qed "L_of_imp";
paulson@7093
   143
paulson@7093
   144
(*Can be used to create implications in a subgoal*)
paulson@7093
   145
val [prem] = goal thy 
paulson@7093
   146
    "[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F";
paulson@7093
   147
by (rtac mp_L 1);
paulson@7093
   148
by (rtac basic 2);
paulson@7093
   149
by (rtac thinR 1 THEN rtac prem 1);
paulson@7093
   150
qed "backwards_impR";
paulson@7093
   151
paulson@7093
   152
 
paulson@7093
   153
qed_goal "conjunct1" thy "|-P&Q ==> |-P"
paulson@7093
   154
    (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
paulson@7093
   155
paulson@7093
   156
qed_goal "conjunct2" thy "|-P&Q ==> |-Q"
paulson@7093
   157
    (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
paulson@7093
   158
paulson@7093
   159
qed_goal "spec" thy "|- (ALL x. P(x)) ==> |- P(x)"
paulson@7093
   160
    (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
paulson@7093
   161
paulson@7093
   162
(** Equality **)
paulson@7093
   163
paulson@7093
   164
Goal "|- a=b --> b=a";
paulson@7093
   165
by (safe_tac (LK_pack add_safes [subst]) 1);
paulson@7093
   166
qed "sym";
paulson@7093
   167
paulson@7093
   168
Goal "|- a=b --> b=c --> a=c";
paulson@7093
   169
by (safe_tac (LK_pack add_safes [subst]) 1);
paulson@7093
   170
qed "trans";
paulson@7093
   171
paulson@7093
   172
(* Symmetry of equality in hypotheses *)
paulson@7093
   173
bind_thm ("symL", sym RS L_of_imp);
paulson@7093
   174
paulson@7093
   175
(* Symmetry of equality in hypotheses *)
paulson@7093
   176
bind_thm ("symR", sym RS R_of_imp);
paulson@7093
   177
paulson@7093
   178
Goal "[| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F";
paulson@7093
   179
by (rtac (trans RS R_of_imp RS mp_R) 1);
paulson@7093
   180
by (ALLGOALS assume_tac);
paulson@7093
   181
qed "transR";
paulson@7122
   182
paulson@7122
   183
paulson@7122
   184
(* Two theorms for rewriting only one instance of a definition:
paulson@7122
   185
   the first for definitions of formulae and the second for terms *)
paulson@7122
   186
paulson@7122
   187
val prems = goal thy "(A == B) ==> |- A <-> B";
paulson@7122
   188
by (rewrite_goals_tac prems);
paulson@7122
   189
by (rtac iff_refl 1);
paulson@7122
   190
qed "def_imp_iff";
paulson@7122
   191
paulson@7122
   192
val prems = goal thy "(A == B) ==> |- A = B";
paulson@7122
   193
by (rewrite_goals_tac prems);
paulson@7122
   194
by (rtac refl 1);
paulson@7122
   195
qed "meta_eq_to_obj_eq";