src/Sequents/LK0.ML
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 9259 103acc345f75
permissions -rw-r--r--
converted to Isar theory format;
wenzelm@17481
     1
(*  Title:      LK/LK0.ML
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
wenzelm@17481
     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*)
wenzelm@17481
    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*)
wenzelm@17481
    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 **)
wenzelm@17481
    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
wenzelm@17481
    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*)
wenzelm@17481
    96
val prop_pack = empty_pack add_safes
wenzelm@17481
    97
                [basic, refl, TrueR, FalseL,
wenzelm@17481
    98
                 conjL, conjR, disjL, disjR, impL, impR,
paulson@7093
    99
                 notL, notR, iffL, iffR];
paulson@7093
   100
wenzelm@17481
   101
val LK_pack = prop_pack add_safes   [allR, exL]
paulson@7122
   102
                        add_unsafes [allL_thin, exR_thin, the_equality];
paulson@7093
   103
wenzelm@17481
   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
wenzelm@17481
   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
wenzelm@17481
   113
val [major,minor] = goal (the_context ())
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
wenzelm@17481
   120
val [major,minor] = goal (the_context ())
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
wenzelm@17481
   130
val [major,minor] = goal (the_context ())
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
wenzelm@17481
   137
val [major,minor] = goal (the_context ())
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*)
wenzelm@17481
   145
val [prem] = goal (the_context ())
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@9259
   152
Goal "|-P&Q ==> |-P";
paulson@9259
   153
by (etac (thinR RS cut) 1);
wenzelm@17481
   154
by (Fast_tac 1);
paulson@9259
   155
qed "conjunct1";
paulson@7093
   156
paulson@9259
   157
Goal "|-P&Q ==> |-Q";
paulson@9259
   158
by (etac (thinR RS cut) 1);
wenzelm@17481
   159
by (Fast_tac 1);
paulson@9259
   160
qed "conjunct2";
paulson@7093
   161
paulson@9259
   162
Goal "|- (ALL x. P(x)) ==> |- P(x)";
paulson@9259
   163
by (etac (thinR RS cut) 1);
wenzelm@17481
   164
by (Fast_tac 1);
paulson@9259
   165
qed "spec";
paulson@7093
   166
paulson@7093
   167
(** Equality **)
paulson@7093
   168
paulson@7093
   169
Goal "|- a=b --> b=a";
paulson@7093
   170
by (safe_tac (LK_pack add_safes [subst]) 1);
paulson@7093
   171
qed "sym";
paulson@7093
   172
paulson@7093
   173
Goal "|- a=b --> b=c --> a=c";
paulson@7093
   174
by (safe_tac (LK_pack add_safes [subst]) 1);
paulson@7093
   175
qed "trans";
paulson@7093
   176
paulson@7093
   177
(* Symmetry of equality in hypotheses *)
paulson@7093
   178
bind_thm ("symL", sym RS L_of_imp);
paulson@7093
   179
paulson@7093
   180
(* Symmetry of equality in hypotheses *)
paulson@7093
   181
bind_thm ("symR", sym RS R_of_imp);
paulson@7093
   182
paulson@7093
   183
Goal "[| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F";
paulson@7093
   184
by (rtac (trans RS R_of_imp RS mp_R) 1);
paulson@7093
   185
by (ALLGOALS assume_tac);
paulson@7093
   186
qed "transR";
paulson@7122
   187
paulson@7122
   188
paulson@7122
   189
(* Two theorms for rewriting only one instance of a definition:
paulson@7122
   190
   the first for definitions of formulae and the second for terms *)
paulson@7122
   191
wenzelm@17481
   192
val prems = goal (the_context ()) "(A == B) ==> |- A <-> B";
paulson@7122
   193
by (rewrite_goals_tac prems);
paulson@7122
   194
by (rtac iff_refl 1);
paulson@7122
   195
qed "def_imp_iff";
paulson@7122
   196
wenzelm@17481
   197
val prems = goal (the_context ()) "(A == B) ==> |- A = B";
paulson@7122
   198
by (rewrite_goals_tac prems);
paulson@7122
   199
by (rtac refl 1);
paulson@7122
   200
qed "meta_eq_to_obj_eq";