src/Sequents/LK0.ML
author paulson
Tue Jul 27 18:52:23 1999 +0200 (1999-07-27)
changeset 7093 b2ee0e5d1a7f
child 7122 87b233b31889
permissions -rw-r--r--
renamed theory LK to LK0
     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 qed_goalw "iffR" thy [iff_def]
    54     "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    55  (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
    56 
    57 qed_goalw "iffL" thy [iff_def]
    58    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    59  (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
    60 
    61 qed_goalw "TrueR" thy [True_def]
    62     "$H |- $E, True, $F"
    63  (fn _=> [ rtac impR 1, rtac basic 1 ]);
    64 
    65 
    66 (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
    67 
    68 Goal "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E";
    69 by (rtac allL 1);
    70 by (etac thinL 1);
    71 qed "allL_thin";
    72 
    73 Goal "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F";
    74 by (rtac exR 1);
    75 by (etac thinR 1);
    76 qed "exR_thin";
    77 
    78 
    79 (*The rules of LK*)
    80 val prop_pack = empty_pack add_safes 
    81                 [basic, refl, TrueR, FalseL, 
    82 		 conjL, conjR, disjL, disjR, impL, impR, 
    83                  notL, notR, iffL, iffR];
    84 
    85 val LK_pack = prop_pack add_safes   [allR, exL] 
    86                         add_unsafes [allL_thin, exR_thin];
    87 
    88 val LK_dup_pack = prop_pack add_safes   [allR, exL] 
    89                             add_unsafes [allL, exR];
    90 
    91 
    92 thm_pack_ref() := LK_pack;
    93 
    94 fun Fast_tac st = fast_tac (thm_pack()) st;
    95 fun Step_tac st = step_tac (thm_pack()) st;
    96 fun Safe_tac st = safe_tac (thm_pack()) st;
    97 
    98 fun lemma_tac th i = 
    99     rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
   100 
   101 val [major,minor] = goal thy 
   102     "[| $H |- $E, $F, P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
   103 by (rtac (thinRS RS cut) 1 THEN rtac major 1);
   104 by (Step_tac 1);
   105 by (rtac thinR 1 THEN rtac minor 1);
   106 qed "mp_R";
   107 
   108 val [major,minor] = goal thy 
   109     "[| $H, $G |- $E, P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
   110 by (rtac (thinL RS cut) 1 THEN rtac major 1);
   111 by (Step_tac 1);
   112 by (rtac thinL 1 THEN rtac minor 1);
   113 qed "mp_L";
   114 
   115 
   116 (** Two rules to generate left- and right- rules from implications **)
   117 
   118 val [major,minor] = goal thy 
   119     "[| |- P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
   120 by (rtac mp_R 1);
   121 by (rtac minor 2);
   122 by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
   123 qed "R_of_imp";
   124 
   125 val [major,minor] = goal thy 
   126     "[| |- P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
   127 by (rtac mp_L 1);
   128 by (rtac minor 2);
   129 by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
   130 qed "L_of_imp";
   131 
   132 (*Can be used to create implications in a subgoal*)
   133 val [prem] = goal thy 
   134     "[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F";
   135 by (rtac mp_L 1);
   136 by (rtac basic 2);
   137 by (rtac thinR 1 THEN rtac prem 1);
   138 qed "backwards_impR";
   139 
   140  
   141 qed_goal "conjunct1" thy "|-P&Q ==> |-P"
   142     (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
   143 
   144 qed_goal "conjunct2" thy "|-P&Q ==> |-Q"
   145     (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
   146 
   147 qed_goal "spec" thy "|- (ALL x. P(x)) ==> |- P(x)"
   148     (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
   149 
   150 (** Equality **)
   151 
   152 Goal "|- a=b --> b=a";
   153 by (safe_tac (LK_pack add_safes [subst]) 1);
   154 qed "sym";
   155 
   156 Goal "|- a=b --> b=c --> a=c";
   157 by (safe_tac (LK_pack add_safes [subst]) 1);
   158 qed "trans";
   159 
   160 (* Symmetry of equality in hypotheses *)
   161 bind_thm ("symL", sym RS L_of_imp);
   162 
   163 (* Symmetry of equality in hypotheses *)
   164 bind_thm ("symR", sym RS R_of_imp);
   165 
   166 Goal "[| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F";
   167 by (rtac (trans RS R_of_imp RS mp_R) 1);
   168 by (ALLGOALS assume_tac);
   169 qed "transR";