# HG changeset patch # User wenzelm # Date 901818172 -7200 # Node ID 924359415f095dcdd71ba9a37d2d7db7b028d5d9 # Parent 1a49756a2e68a2f202e422554c6214b26d3277fb functorized Clasimp module; diff -r 1a49756a2e68 -r 924359415f09 src/FOL/ROOT.ML --- a/src/FOL/ROOT.ML Thu Jul 30 17:59:57 1998 +0200 +++ b/src/FOL/ROOT.ML Thu Jul 30 19:02:52 1998 +0200 @@ -19,6 +19,7 @@ use "$ISABELLE_HOME/src/Provers/hypsubst.ML"; use "$ISABELLE_HOME/src/Provers/classical.ML"; use "$ISABELLE_HOME/src/Provers/blast.ML"; +use "$ISABELLE_HOME/src/Provers/clasimp.ML"; use "$ISABELLE_HOME/src/Provers/quantifier1.ML"; use_thy "IFOL"; diff -r 1a49756a2e68 -r 924359415f09 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Thu Jul 30 17:59:57 1998 +0200 +++ b/src/FOL/simpdata.ML Thu Jul 30 19:02:52 1998 +0200 @@ -334,11 +334,7 @@ - - - - -(*** Integration of simplifier with classical reasoner ***) +(*** integration of simplifier with classical reasoner ***) (* rot_eq_tac rotates the first equality premise of subgoal i to the front, fails if there is no equaliy or if an equality is already at the front *) @@ -353,8 +349,12 @@ if n>0 then rotate_tac n i else no_tac end) end; -use "$ISABELLE_HOME/src/Provers/clasimp.ML"; + +structure Clasimp = ClasimpFun + (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast + val addcongs = op addcongs and delcongs = op delcongs + and addSaltern = op addSaltern and addbefore = op addbefore); + open Clasimp; val FOL_css = (FOL_cs, FOL_ss); - diff -r 1a49756a2e68 -r 924359415f09 src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Thu Jul 30 17:59:57 1998 +0200 +++ b/src/HOL/ROOT.ML Thu Jul 30 19:02:52 1998 +0200 @@ -21,6 +21,7 @@ use "$ISABELLE_HOME/src/Provers/hypsubst.ML"; use "$ISABELLE_HOME/src/Provers/classical.ML"; use "$ISABELLE_HOME/src/Provers/blast.ML"; +use "$ISABELLE_HOME/src/Provers/clasimp.ML"; use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML"; use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML"; use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML"; diff -r 1a49756a2e68 -r 924359415f09 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Thu Jul 30 17:59:57 1998 +0200 +++ b/src/HOL/simpdata.ML Thu Jul 30 19:02:52 1998 +0200 @@ -457,7 +457,7 @@ -(*** Integration of simplifier with classical reasoner ***) +(*** integration of simplifier with classical reasoner ***) (* rot_eq_tac rotates the first equality premise of subgoal i to the front, fails if there is no equaliy or if an equality is already at the front *) @@ -471,7 +471,12 @@ if n>0 then rotate_tac n i else no_tac end) end; -use "$ISABELLE_HOME/src/Provers/clasimp.ML"; + +structure Clasimp = ClasimpFun + (structure Simplifier = Simplifier and Classical = Classical and Blast = Blast + val addcongs = op addcongs and delcongs = op delcongs + and addSaltern = op addSaltern and addbefore = op addbefore); + open Clasimp; val HOL_css = (HOL_cs, HOL_ss); diff -r 1a49756a2e68 -r 924359415f09 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Thu Jul 30 17:59:57 1998 +0200 +++ b/src/Provers/clasimp.ML Thu Jul 30 19:02:52 1998 +0200 @@ -2,18 +2,32 @@ ID: $Id$ Author: David von Oheimb, TU Muenchen -Combination of classical reasoner and simplifier -to be used after installing both of them +Combination of classical reasoner and simplifier (depends on +simplifier.ML, classical.ML, blast.ML). *) -type clasimpset = claset * simpset; - infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2 addcongs2 delcongs2; infix 4 addSss addss; +signature CLASIMP_DATA = +sig + structure Simplifier: SIMPLIFIER + structure Classical: CLASSICAL + structure Blast: BLAST + sharing type Classical.claset = Blast.claset + val addcongs: Simplifier.simpset * thm list -> Simplifier.simpset + val delcongs: Simplifier.simpset * thm list -> Simplifier.simpset + val addSaltern: Classical.claset * (string * (int -> tactic)) -> Classical.claset + val addbefore: Classical.claset * (string * (int -> tactic)) -> Classical.claset +end + signature CLASIMP = sig + include CLASIMP_DATA + type claset + type simpset + type clasimpset val addSIs2 : clasimpset * thm list -> clasimpset val addSEs2 : clasimpset * thm list -> clasimpset val addSDs2 : clasimpset * thm list -> clasimpset @@ -35,89 +49,101 @@ val force : int -> unit end; -structure Clasimp: CLASIMP = +functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP = struct -(* this interface for updating a clasimpset is rudimentary and just for - convenience for the most common cases. - In other cases a clasimpset may be dealt with componentwise. *) -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; +open Data; + +type claset = Classical.claset; +type simpset = Simplifier.simpset; +type clasimpset = claset * simpset; + + +(* clasimpset operations *) + +(*this interface for updating a clasimpset is rudimentary and just for + convenience for the most common cases*) + +fun pair_upd1 f ((a,b),x) = (f(a,x), b); +fun pair_upd2 f ((a,b),x) = (a, f(b,x)); + +fun op addSIs2 arg = pair_upd1 Classical.addSIs arg; +fun op addSEs2 arg = pair_upd1 Classical.addSEs arg; +fun op addSDs2 arg = pair_upd1 Classical.addSDs arg; +fun op addIs2 arg = pair_upd1 Classical.addIs arg; +fun op addEs2 arg = pair_upd1 Classical.addEs arg; +fun op addDs2 arg = pair_upd1 Classical.addDs arg; +fun op addsimps2 arg = pair_upd2 Simplifier.addsimps arg; +fun op delsimps2 arg = pair_upd2 Simplifier.delsimps arg; +fun op addcongs2 arg = pair_upd2 Data.addcongs arg; +fun op delcongs2 arg = pair_upd2 Data.delcongs arg; (*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_full_simp_tac", - CHANGED o (safe_asm_full_simp_tac ss)); -fun cs addss ss = cs addbefore ( "asm_full_simp_tac", - asm_full_simp_tac ss); + CHANGED o Simplifier.safe_asm_full_simp_tac ss); +fun cs addss ss = cs addbefore ("asm_full_simp_tac", Simplifier.asm_full_simp_tac ss); -fun CLASIMPSET tacf state = CLASET (fn cs => SIMPSET (fn ss => tacf (cs, ss))) state; -fun CLASIMPSET' tacf i state = CLASET (fn cs => SIMPSET (fn ss => tacf (cs, ss) i)) state; +(* tacticals *) + +fun CLASIMPSET tacf state = + Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss))) state; + +fun CLASIMPSET' tacf i state = + Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state; -local +(* auto_tac *) - 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); +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 +(* 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 + (Classical.appWrappers cs + (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac + (Classical.safe_step_tac cs i)) THEN_ELSE + (DEPTH_SOLVE (nodup_depth_tac cs m i), + Classical.inst0_step_tac cs i APPEND + COND (K(m=0)) no_tac + ((Classical.instp_step_tac cs i APPEND Classical.step_tac cs i) + THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1) + i state; (*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 + 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'), + in EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss), + TRY (Classical.safe_tac cs'), REPEAT (FIRSTGOAL maintac), - TRY (safe_tac (cs addSss ss)), + TRY (Classical.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_tac st = auto_tac (Classical.claset(), Simplifier.simpset()) st; fun auto () = by Auto_tac; + +(* force_tac *) + (* aimed to solve the given subgoal totally, using whatever tools possible *) fun force_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [ - clarify_tac cs' 1, - IF_UNSOLVED (asm_full_simp_tac ss 1), - ALLGOALS (best_tac cs')]) end; -fun Force_tac i = force_tac (claset(), simpset()) i; + Classical.clarify_tac cs' 1, + IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1), + ALLGOALS (Classical.best_tac cs')]) end; +fun Force_tac i = force_tac (Classical.claset(), Simplifier.simpset()) i; fun force i = by (Force_tac i); + end;