--- 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";
--- 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;