factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML
explicitly introducing combined type clasimpset
--- a/src/FOL/simpdata.ML Wed Feb 25 15:51:24 1998 +0100
+++ b/src/FOL/simpdata.ML Wed Feb 25 20:25:27 1998 +0100
@@ -309,6 +309,10 @@
+
+
+
+
(*** Integration of simplifier with classical reasoner ***)
(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
@@ -324,64 +328,8 @@
if n>0 then rotate_tac n i else no_tac end)
end;
-
-fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN'
- safe_asm_full_simp_tac ss;
-(*an unsatisfactory fix for the incomplete asm_full_simp_tac!
- better: asm_really_full_simp_tac, a yet to be implemented version of
- asm_full_simp_tac that applies all equalities in the
- premises to all the premises *)
-
-(*Add a simpset to a classical set!*)
-infix 4 addSss addss;
-fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
- CHANGED o (safe_asm_more_full_simp_tac ss));
-fun cs addss ss = cs addbefore ("asm_full_simp_tac", asm_full_simp_tac ss);
-
-fun Addss ss = (claset_ref() := claset() addss ss);
-
-(*Designed to be idempotent, except if best_tac instantiates variables
- in some of the subgoals*)
-
-type clasimpset = (claset * simpset);
+use "$ISABELLE_HOME/src/Provers/clasimp.ML";
+open Clasimp;
val FOL_css = (FOL_cs, FOL_ss);
-fun pair_upd1 f ((a,b),x) = (f(a,x), b);
-fun pair_upd2 f ((a,b),x) = (a, f(b,x));
-
-infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
- addsimps2 delsimps2 addcongs2 delcongs2;
-fun op addSIs2 arg = pair_upd1 (op addSIs) arg;
-fun op addSEs2 arg = pair_upd1 (op addSEs) arg;
-fun op addSDs2 arg = pair_upd1 (op addSDs) arg;
-fun op addIs2 arg = pair_upd1 (op addIs ) arg;
-fun op addEs2 arg = pair_upd1 (op addEs ) arg;
-fun op addDs2 arg = pair_upd1 (op addDs ) arg;
-fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
-fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
-fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
-fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
-
-
-fun mk_auto_tac (cs, ss) m n =
- let val cs' = cs addss ss
- val bdt = Blast.depth_tac cs m;
- fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s =>
- (warning ("Blast_tac: " ^ s); Seq.empty);
- val maintac =
- blast_depth_tac (*fast but can't use addss*)
- ORELSE'
- depth_tac cs' n; (*slower but general*)
- in EVERY [ALLGOALS (asm_full_simp_tac ss),
- TRY (safe_tac cs'),
- REPEAT (FIRSTGOAL maintac),
- TRY (safe_tac (cs addSss ss)),
- prune_params_tac]
- end;
-
-fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
-
-fun Auto_tac st = auto_tac (claset(), simpset()) st;
-
-fun auto () = by Auto_tac;
--- a/src/HOL/TLA/cladata.ML Wed Feb 25 15:51:24 1998 +0100
+++ b/src/HOL/TLA/cladata.ML Wed Feb 25 20:25:27 1998 +0100
@@ -51,7 +51,7 @@
AddSIs [actionI,intI];
AddDs [actionD,intD];
-Addss (simpset());
+claset_ref() := claset() addss (simpset());
--- a/src/HOL/simpdata.ML Wed Feb 25 15:51:24 1998 +0100
+++ b/src/HOL/simpdata.ML Wed Feb 25 20:25:27 1998 +0100
@@ -424,6 +424,10 @@
simpset_ref() := HOL_ss;
+
+
+
+
(*** Integration of simplifier with classical reasoner ***)
(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
@@ -438,77 +442,7 @@
if n>0 then rotate_tac n i else no_tac end)
end;
-(*an unsatisfactory fix for the incomplete asm_full_simp_tac!
- better: asm_really_full_simp_tac, a yet to be implemented version of
- asm_full_simp_tac that applies all equalities in the
- premises to all the premises *)
-fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN'
- safe_asm_full_simp_tac ss;
-
-(*Add a simpset to a classical set!*)
-infix 4 addSss addss;
-fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
- CHANGED o (safe_asm_more_full_simp_tac ss));
-fun cs addss ss = cs addbefore ("asm_full_simp_tac", asm_full_simp_tac ss);
-
-fun Addss ss = (claset_ref() := claset() addss ss);
-
-(*Designed to be idempotent, except if best_tac instantiates variables
- in some of the subgoals*)
-
-type clasimpset = (claset * simpset);
+use "$ISABELLE_HOME/src/Provers/clasimp.ML";
+open Clasimp;
val HOL_css = (HOL_cs, HOL_ss);
-
-fun pair_upd1 f ((a,b),x) = (f(a,x), b);
-fun pair_upd2 f ((a,b),x) = (a, f(b,x));
-
-infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
- addsimps2 delsimps2 addcongs2 delcongs2;
-fun op addSIs2 arg = pair_upd1 (op addSIs) arg;
-fun op addSEs2 arg = pair_upd1 (op addSEs) arg;
-fun op addSDs2 arg = pair_upd1 (op addSDs) arg;
-fun op addIs2 arg = pair_upd1 (op addIs ) arg;
-fun op addEs2 arg = pair_upd1 (op addEs ) arg;
-fun op addDs2 arg = pair_upd1 (op addDs ) arg;
-fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
-fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
-fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
-fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
-
-fun mk_auto_tac (cs, ss) m n =
- let val cs' = cs addss ss
- val bdt = Blast.depth_tac cs m;
- fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s =>
- (warning ("Blast_tac: " ^ s); Seq.empty);
-
- (* a variant of depth_tac that avoids interference of the simplifier
- with dup_step_tac when they are combined by auto_tac *)
- fun nodup_depth_tac cs m i state =
- SELECT_GOAL
- (appWrappers cs
- (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
- (safe_step_tac cs i)) THEN_ELSE
- (DEPTH_SOLVE (nodup_depth_tac cs m i),
- inst0_step_tac cs i APPEND
- COND (K(m=0)) no_tac
- ((instp_step_tac cs i APPEND step_tac cs i)
- THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1)
- i state;
-
- val maintac =
- blast_depth_tac (*fast but can't use addss*)
- ORELSE'
- nodup_depth_tac cs' n; (*slower but more general*)
- in EVERY [ALLGOALS (asm_full_simp_tac ss),
- TRY (safe_tac cs'),
- REPEAT (FIRSTGOAL maintac),
- TRY (safe_tac (cs addSss ss)),
- prune_params_tac]
- end;
-
-fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
-
-fun Auto_tac st = auto_tac (claset(), simpset()) st;
-
-fun auto () = by Auto_tac;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/clasimp.ML Wed Feb 25 20:25:27 1998 +0100
@@ -0,0 +1,110 @@
+(* Title: Provers/clasimp.ML
+ ID: $Id$
+ Author: David von Oheimb, TU Muenchen
+
+Combination of classical reasoner and simplifier
+to be used after installing both of them
+*)
+
+infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
+ addsimps2 delsimps2 addcongs2 delcongs2;
+infix 4 addSss addss;
+
+type clasimpset = claset * simpset;
+
+signature CLASIMP =
+sig
+ val addSIs2 : clasimpset * thm list -> clasimpset
+ val addSEs2 : clasimpset * thm list -> clasimpset
+ val addSDs2 : clasimpset * thm list -> clasimpset
+ val addIs2 : clasimpset * thm list -> clasimpset
+ val addEs2 : clasimpset * thm list -> clasimpset
+ val addDs2 : clasimpset * thm list -> clasimpset
+ val addsimps2 : clasimpset * thm list -> clasimpset
+ val delsimps2 : clasimpset * thm list -> clasimpset
+ val addSss : claset * simpset -> claset
+ val addss : claset * simpset -> claset
+ val mk_auto_tac:clasimpset -> int -> int -> tactic
+ val auto_tac : clasimpset -> tactic
+ val Auto_tac : tactic
+ val auto : unit -> unit
+end;
+
+structure Clasimp: CLASIMP =
+struct
+
+local
+ fun pair_upd1 f ((a,b),x) = (f(a,x), b);
+ fun pair_upd2 f ((a,b),x) = (a, f(b,x));
+in
+ fun op addSIs2 arg = pair_upd1 (op addSIs) arg;
+ fun op addSEs2 arg = pair_upd1 (op addSEs) arg;
+ fun op addSDs2 arg = pair_upd1 (op addSDs) arg;
+ fun op addIs2 arg = pair_upd1 (op addIs ) arg;
+ fun op addEs2 arg = pair_upd1 (op addEs ) arg;
+ fun op addDs2 arg = pair_upd1 (op addDs ) arg;
+ fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
+ fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
+ fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
+ fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
+end;
+
+(*an unsatisfactory fix for the incomplete safe_asm_full_simp_tac!
+ better: asm_really_full_simp_tac, a yet to be implemented version of
+ asm_full_simp_tac that applies all equalities in the
+ premises to all the premises *)
+fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN'
+ safe_asm_full_simp_tac ss;
+
+(*Add a simpset to a classical set!*)
+(*Caution: only one simpset added can be added by each of addSss and addss*)
+fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
+ CHANGED o (safe_asm_more_full_simp_tac ss));
+fun cs addss ss = cs addbefore ( "asm_full_simp_tac",
+ asm_full_simp_tac ss);
+
+
+local
+
+ fun blast_depth_tac cs m i thm = Blast.depth_tac cs m i thm
+ handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
+
+ (* a variant of depth_tac that avoids interference of the simplifier
+ with dup_step_tac when they are combined by auto_tac *)
+ fun nodup_depth_tac cs m i state =
+ SELECT_GOAL
+ (appWrappers cs
+ (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
+ (safe_step_tac cs i)) THEN_ELSE
+ (DEPTH_SOLVE (nodup_depth_tac cs m i),
+ inst0_step_tac cs i APPEND
+ COND (K(m=0)) no_tac
+ ((instp_step_tac cs i APPEND step_tac cs i)
+ THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1)
+ i state;
+
+in
+
+(*Designed to be idempotent, except if best_tac instantiates variables
+ in some of the subgoals*)
+fun mk_auto_tac (cs, ss) m n =
+ let val cs' = cs addss ss
+ val maintac =
+ blast_depth_tac cs m (*fast but can't use addss*)
+ ORELSE'
+ nodup_depth_tac cs' n; (*slower but more general*)
+ in EVERY [ALLGOALS (asm_full_simp_tac ss),
+ TRY (safe_tac cs'),
+ REPEAT (FIRSTGOAL maintac),
+ TRY (safe_tac (cs addSss ss)),
+ prune_params_tac]
+ end;
+end;
+
+fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
+
+fun Auto_tac st = auto_tac (claset(), simpset()) st;
+
+fun auto () = by Auto_tac;
+
+end;