# HG changeset patch
# User paulson
# Date 933094328 -7200
# Node ID d7958f38e9e08e2d4846f0a01b687c62344dc761
# Parent  b76a26835a5cc175d31bcacb8c8436bb6813d8b2
renamed LK0.ML

diff -r b76a26835a5c -r d7958f38e9e0 src/Sequents/LK.ML
--- a/src/Sequents/LK.ML	Tue Jul 27 18:50:14 1999 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-(*  Title:      LK/LK.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Tactics and lemmas for lk.thy (thanks also to Philippe de Groote)  
-*)
-
-open LK;
-
-(*Higher precedence than := facilitates use of references*)
-infix 4 add_safes add_unsafes;
-
-(*Cut and thin, replacing the right-side formula*)
-fun cutR_tac (sP: string) i = 
-    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
-
-(*Cut and thin, replacing the left-side formula*)
-fun cutL_tac (sP: string) i = 
-    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
-
-
-(** If-and-only-if rules **)
-qed_goalw "iffR" LK.thy [iff_def]
-    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
- (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
-
-qed_goalw "iffL" LK.thy [iff_def]
-   "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
- (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
-
-qed_goalw "TrueR" LK.thy [True_def]
-    "$H |- $E, True, $F"
- (fn _=> [ rtac impR 1, rtac basic 1 ]);
-
-
-(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
-
-qed_goal "allL_thin" LK.thy 
-    "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"
- (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);
-
-qed_goal "exR_thin" LK.thy 
-    "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F"
- (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);
-
-(* Symmetry of equality in hypotheses *)
-qed_goal "symL" LK.thy 
-    "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" 
- (fn prems=>
-  [ (rtac cut 1),
-    (rtac thinL 2),
-    (resolve_tac prems 2),
-    (resolve_tac [basic RS sym] 1) ]);
-
-
-
-
-(*The rules of LK*)
-val prop_pack = empty_pack add_safes 
-                [basic, refl, conjL, conjR, disjL, disjR, impL, impR, 
-                 notL, notR, iffL, iffR];
-
-val LK_pack = prop_pack add_safes   [allR, exL] 
-                        add_unsafes [allL_thin, exR_thin];
-
-val LK_dup_pack = prop_pack add_safes   [allR, exL] 
-                            add_unsafes [allL, exR];
-
-
-
-(** Contraction.  Useful since some rules are not complete. **)
-
-qed_goal "conR" LK.thy 
-    "$H |- $E, P, $F, P ==> $H |- $E, P, $F"
- (fn prems=>
-  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
-
-qed_goal "conL" LK.thy 
-    "$H, P, $G, P |- $E ==> $H, P, $G |- $E"
- (fn prems=>
-  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);