src/Sequents/LK0.ML
changeset 17481 75166ebb619b
parent 9259 103acc345f75
     1.1 --- a/src/Sequents/LK0.ML	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/LK0.ML	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -1,9 +1,9 @@
     1.4 -(*  Title:      LK/LK0
     1.5 +(*  Title:      LK/LK0.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1992  University of Cambridge
     1.9  
    1.10 -Tactics and lemmas for LK (thanks also to Philippe de Groote)  
    1.11 +Tactics and lemmas for LK (thanks also to Philippe de Groote)
    1.12  
    1.13  Structural rules by Soren Heilmann
    1.14  *)
    1.15 @@ -41,21 +41,21 @@
    1.16  qed "exchL";
    1.17  
    1.18  (*Cut and thin, replacing the right-side formula*)
    1.19 -fun cutR_tac (sP: string) i = 
    1.20 +fun cutR_tac (sP: string) i =
    1.21      res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
    1.22  
    1.23  (*Cut and thin, replacing the left-side formula*)
    1.24 -fun cutL_tac (sP: string) i = 
    1.25 +fun cutL_tac (sP: string) i =
    1.26      res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
    1.27  
    1.28  
    1.29  (** If-and-only-if rules **)
    1.30 -Goalw [iff_def] 
    1.31 +Goalw [iff_def]
    1.32      "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F";
    1.33  by (REPEAT (ares_tac [conjR,impR] 1));
    1.34  qed "iffR";
    1.35  
    1.36 -Goalw [iff_def] 
    1.37 +Goalw [iff_def]
    1.38      "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E";
    1.39  by (REPEAT (ares_tac [conjL,impL,basic] 1));
    1.40  qed "iffL";
    1.41 @@ -93,31 +93,31 @@
    1.42  
    1.43  
    1.44  (*The rules of LK*)
    1.45 -val prop_pack = empty_pack add_safes 
    1.46 -                [basic, refl, TrueR, FalseL, 
    1.47 -		 conjL, conjR, disjL, disjR, impL, impR, 
    1.48 +val prop_pack = empty_pack add_safes
    1.49 +                [basic, refl, TrueR, FalseL,
    1.50 +                 conjL, conjR, disjL, disjR, impL, impR,
    1.51                   notL, notR, iffL, iffR];
    1.52  
    1.53 -val LK_pack = prop_pack add_safes   [allR, exL] 
    1.54 +val LK_pack = prop_pack add_safes   [allR, exL]
    1.55                          add_unsafes [allL_thin, exR_thin, the_equality];
    1.56  
    1.57 -val LK_dup_pack = prop_pack add_safes   [allR, exL] 
    1.58 +val LK_dup_pack = prop_pack add_safes   [allR, exL]
    1.59                              add_unsafes [allL, exR, the_equality];
    1.60  
    1.61  
    1.62  pack_ref() := LK_pack;
    1.63  
    1.64 -fun lemma_tac th i = 
    1.65 +fun lemma_tac th i =
    1.66      rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
    1.67  
    1.68 -val [major,minor] = goal thy 
    1.69 +val [major,minor] = goal (the_context ())
    1.70      "[| $H |- $E, $F, P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
    1.71  by (rtac (thinRS RS cut) 1 THEN rtac major 1);
    1.72  by (Step_tac 1);
    1.73  by (rtac thinR 1 THEN rtac minor 1);
    1.74  qed "mp_R";
    1.75  
    1.76 -val [major,minor] = goal thy 
    1.77 +val [major,minor] = goal (the_context ())
    1.78      "[| $H, $G |- $E, P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
    1.79  by (rtac (thinL RS cut) 1 THEN rtac major 1);
    1.80  by (Step_tac 1);
    1.81 @@ -127,14 +127,14 @@
    1.82  
    1.83  (** Two rules to generate left- and right- rules from implications **)
    1.84  
    1.85 -val [major,minor] = goal thy 
    1.86 +val [major,minor] = goal (the_context ())
    1.87      "[| |- P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
    1.88  by (rtac mp_R 1);
    1.89  by (rtac minor 2);
    1.90  by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
    1.91  qed "R_of_imp";
    1.92  
    1.93 -val [major,minor] = goal thy 
    1.94 +val [major,minor] = goal (the_context ())
    1.95      "[| |- P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
    1.96  by (rtac mp_L 1);
    1.97  by (rtac minor 2);
    1.98 @@ -142,7 +142,7 @@
    1.99  qed "L_of_imp";
   1.100  
   1.101  (*Can be used to create implications in a subgoal*)
   1.102 -val [prem] = goal thy 
   1.103 +val [prem] = goal (the_context ())
   1.104      "[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F";
   1.105  by (rtac mp_L 1);
   1.106  by (rtac basic 2);
   1.107 @@ -151,17 +151,17 @@
   1.108  
   1.109  Goal "|-P&Q ==> |-P";
   1.110  by (etac (thinR RS cut) 1);
   1.111 -by (Fast_tac 1);		
   1.112 +by (Fast_tac 1);
   1.113  qed "conjunct1";
   1.114  
   1.115  Goal "|-P&Q ==> |-Q";
   1.116  by (etac (thinR RS cut) 1);
   1.117 -by (Fast_tac 1);		
   1.118 +by (Fast_tac 1);
   1.119  qed "conjunct2";
   1.120  
   1.121  Goal "|- (ALL x. P(x)) ==> |- P(x)";
   1.122  by (etac (thinR RS cut) 1);
   1.123 -by (Fast_tac 1);		
   1.124 +by (Fast_tac 1);
   1.125  qed "spec";
   1.126  
   1.127  (** Equality **)
   1.128 @@ -189,12 +189,12 @@
   1.129  (* Two theorms for rewriting only one instance of a definition:
   1.130     the first for definitions of formulae and the second for terms *)
   1.131  
   1.132 -val prems = goal thy "(A == B) ==> |- A <-> B";
   1.133 +val prems = goal (the_context ()) "(A == B) ==> |- A <-> B";
   1.134  by (rewrite_goals_tac prems);
   1.135  by (rtac iff_refl 1);
   1.136  qed "def_imp_iff";
   1.137  
   1.138 -val prems = goal thy "(A == B) ==> |- A = B";
   1.139 +val prems = goal (the_context ()) "(A == B) ==> |- A = B";
   1.140  by (rewrite_goals_tac prems);
   1.141  by (rtac refl 1);
   1.142  qed "meta_eq_to_obj_eq";