# HG changeset patch # User oheimb # Date 888434727 -3600 # Node ID d24cca140eebbf71f5ae476b4ab732bebcf42344 # Parent 70dd492a1698619920326ead8056ede901782d7b 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 diff -r 70dd492a1698 -r d24cca140eeb src/FOL/simpdata.ML --- 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; diff -r 70dd492a1698 -r d24cca140eeb src/HOL/TLA/cladata.ML --- 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()); diff -r 70dd492a1698 -r d24cca140eeb src/HOL/simpdata.ML --- 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; diff -r 70dd492a1698 -r d24cca140eeb src/Provers/clasimp.ML --- /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;