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