# HG changeset patch
# User paulson
# Date 933162902 -7200
# Node ID 87b233b31889dc5ef586f9c5c389fcf1dc200fe4
# Parent  0e3d09451b7a54a738190097f8ae2ab9ba41f80e
renamed ...thm_pack... to ...pack...

diff -r 0e3d09451b7a -r 87b233b31889 src/Sequents/LK0.ML
--- a/src/Sequents/LK0.ML	Wed Jul 28 13:52:59 1999 +0200
+++ b/src/Sequents/LK0.ML	Wed Jul 28 13:55:02 1999 +0200
@@ -50,18 +50,34 @@
 
 
 (** If-and-only-if rules **)
-qed_goalw "iffR" 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)) ]);
+Goalw [iff_def] 
+    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F";
+by (REPEAT (ares_tac [conjR,impR] 1));
+qed "iffR";
+
+Goalw [iff_def] 
+    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E";
+by (REPEAT (ares_tac [conjL,impL,basic] 1));
+qed "iffL";
+
+Goal "$H |- $E, (P <-> P), $F";
+by (REPEAT (resolve_tac [iffR,basic] 1));
+qed "iff_refl";
 
-qed_goalw "iffL" 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)) ]);
+Goalw [True_def] "$H |- $E, True, $F";
+by (rtac impR 1);
+by (rtac basic 1);
+qed "TrueR";
 
-qed_goalw "TrueR" thy [True_def]
-    "$H |- $E, True, $F"
- (fn _=> [ rtac impR 1, rtac basic 1 ]);
-
+(*Descriptions*)
+val [p1,p2] = Goal
+    "[| $H |- $E, P(a), $F;  !!x. $H, P(x) |- $E, x=a, $F |] \
+\    ==> $H |- $E, (THE x. P(x)) = a, $F";
+by (rtac cut 1);
+by (rtac p2 2);
+by (rtac The 1 THEN rtac thinR 1 THEN rtac exchRS 1 THEN rtac p1 1);
+by (rtac thinR 1 THEN rtac exchRS 1 THEN rtac p2 1);
+qed "the_equality";
 
 (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
 
@@ -83,17 +99,13 @@
                  notL, notR, iffL, iffR];
 
 val LK_pack = prop_pack add_safes   [allR, exL] 
-                        add_unsafes [allL_thin, exR_thin];
+                        add_unsafes [allL_thin, exR_thin, the_equality];
 
 val LK_dup_pack = prop_pack add_safes   [allR, exL] 
-                            add_unsafes [allL, exR];
+                            add_unsafes [allL, exR, the_equality];
 
 
-thm_pack_ref() := LK_pack;
-
-fun Fast_tac st = fast_tac (thm_pack()) st;
-fun Step_tac st = step_tac (thm_pack()) st;
-fun Safe_tac st = safe_tac (thm_pack()) st;
+pack_ref() := LK_pack;
 
 fun lemma_tac th i = 
     rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
@@ -167,3 +179,17 @@
 by (rtac (trans RS R_of_imp RS mp_R) 1);
 by (ALLGOALS assume_tac);
 qed "transR";
+
+
+(* Two theorms for rewriting only one instance of a definition:
+   the first for definitions of formulae and the second for terms *)
+
+val prems = goal thy "(A == B) ==> |- A <-> B";
+by (rewrite_goals_tac prems);
+by (rtac iff_refl 1);
+qed "def_imp_iff";
+
+val prems = goal thy "(A == B) ==> |- A = B";
+by (rewrite_goals_tac prems);
+by (rtac refl 1);
+qed "meta_eq_to_obj_eq";
diff -r 0e3d09451b7a -r 87b233b31889 src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Wed Jul 28 13:52:59 1999 +0200
+++ b/src/Sequents/prover.ML	Wed Jul 28 13:55:02 1999 +0200
@@ -1,4 +1,4 @@
-(*  Title:      LK/LK.ML
+(*  Title:      Sequents/prover
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
@@ -7,12 +7,17 @@
 *)
 
 
-
 (*Higher precedence than := facilitates use of references*)
 infix 4 add_safes add_unsafes;
 
+structure Cla =
+
+struct
+
 datatype pack = Pack of thm list * thm list;
 
+val trace = ref false;
+
 (*A theorem pack has the form  (safe rules, unsafe rules)
   An unsafe rule is incomplete or introduces variables in subgoals,
   and is tried only when the safe rules are not applicable.  *)
@@ -129,7 +134,9 @@
   let val restac  =    RESOLVE_THEN safes
       and lastrestac = RESOLVE_THEN unsafes;
       fun gtac i = restac gtac i  
-	           ORELSE  (print_tac "" THEN lastrestac gtac i)
+	           ORELSE  (if !trace then
+				(print_tac "" THEN lastrestac gtac i)
+			    else lastrestac gtac i)
   in  gtac  end; 
 
 
@@ -139,8 +146,8 @@
 val safe_goal_tac = safe_tac;   (*backwards compatibility*)
 
 (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
-fun step_tac (thm_pack as Pack(safes,unsafes)) =
-    safe_tac thm_pack  ORELSE'
+fun step_tac (pack as Pack(safes,unsafes)) =
+    safe_tac pack  ORELSE'
     filseq_resolve_tac unsafes 9999;
 
 
@@ -148,17 +155,17 @@
    A decision procedure for Propositional Calculus, it is incomplete
    for Predicate-Calculus because of allL_thin and exR_thin.  
    Fails if it can do nothing.      *)
-fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1));
+fun pc_tac pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac pack 1));
 
 
 (*The following two tactics are analogous to those provided by 
   Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
-fun fast_tac thm_pack =
-  SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1));
+fun fast_tac pack =
+  SELECT_GOAL (DEPTH_SOLVE (step_tac pack 1));
 
-fun best_tac thm_pack  = 
+fun best_tac pack  = 
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
-	       (step_tac thm_pack 1));
+	       (step_tac pack 1));
 
 
 
@@ -177,23 +184,33 @@
 
 val prover_setup = [ProverData.init];
 
-val print_thm_pack = ProverData.print;
-val thm_pack_ref_of_sg = ProverData.get_sg;
-val thm_pack_ref_of = ProverData.get;
+val print_pack = ProverData.print;
+val pack_ref_of_sg = ProverData.get_sg;
+val pack_ref_of = ProverData.get;
 
-(* access global thm_pack *)
+(* access global pack *)
 
-val thm_pack_of_sg = ! o thm_pack_ref_of_sg;
-val thm_pack_of = thm_pack_of_sg o sign_of;
+val pack_of_sg = ! o pack_ref_of_sg;
+val pack_of = pack_of_sg o sign_of;
 
-val thm_pack = thm_pack_of o Context.the_context;
-val thm_pack_ref = thm_pack_ref_of_sg o sign_of o Context.the_context;
+val pack = pack_of o Context.the_context;
+val pack_ref = pack_ref_of_sg o sign_of o Context.the_context;
 
 
-(* change global thm_pack *)
+(* change global pack *)
+
+fun change_pack f x = pack_ref () := (f (pack (), x));
 
-fun change_thm_pack f x = thm_pack_ref () := (f (thm_pack (), x));
+val Add_safes = change_pack (op add_safes);
+val Add_unsafes = change_pack (op add_unsafes);
+
 
-val Add_safes = change_thm_pack (op add_safes);
-val Add_unsafes = change_thm_pack (op add_unsafes);
+fun Fast_tac st = fast_tac (pack()) st;
+fun Step_tac st = step_tac (pack()) st;
+fun Safe_tac st = safe_tac (pack()) st;
+fun Pc_tac st   = pc_tac (pack()) st;
 
+end;
+
+
+open Cla;