# HG changeset patch # User wenzelm # Date 967761068 -7200 # Node ID c07777210a693f1ba7e0f4b96f62c787e544241f # Parent 54c6a2c6e5690fc658f366cc317051f54c65729f auto method: opt args; tuned; diff -r 54c6a2c6e569 -r c07777210a69 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Fri Sep 01 00:30:25 2000 +0200 +++ b/src/Provers/clasimp.ML Fri Sep 01 00:31:08 2000 +0200 @@ -1,4 +1,4 @@ -(* Title: Provers/clasimp.ML +(* Title: Provers/clasimp.ML ID: $Id$ Author: David von Oheimb, TU Muenchen @@ -24,33 +24,33 @@ type claset type simpset type clasimpset - 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 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 CLASIMPSET :(clasimpset -> tactic) -> tactic val CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic val clarsimp_tac: clasimpset -> int -> tactic val Clarsimp_tac: int -> tactic val mk_auto_tac : clasimpset -> int -> int -> tactic - val auto_tac : clasimpset -> tactic - val Auto_tac : tactic - val auto : unit -> unit - val force_tac : clasimpset -> int -> tactic - val Force_tac : int -> tactic - val force : int -> unit + val auto_tac : clasimpset -> tactic + val Auto_tac : tactic + val auto : unit -> unit + val force_tac : clasimpset -> int -> tactic + val Force_tac : int -> tactic + val force : int -> unit val fast_simp_tac : clasimpset -> int -> tactic val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute val get_local_clasimpset: Proof.context -> clasimpset val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list - val setup : (theory -> theory) list + val setup : (theory -> theory) list end; functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP = @@ -86,9 +86,9 @@ (*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 = Classical.addSaltern (cs, ("safe_asm_full_simp_tac", - CHANGED o safe_asm_full_simp_tac ss)); -fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac", - CHANGED o Simplifier.asm_full_simp_tac ss)); + CHANGED o safe_asm_full_simp_tac ss)); +fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac", + CHANGED o Simplifier.asm_full_simp_tac ss)); (* tacticals *) @@ -100,26 +100,26 @@ fun clarsimp_tac (cs, ss) = safe_asm_full_simp_tac ss THEN_ALL_NEW - Classical.clarify_tac (cs addSss ss); + Classical.clarify_tac (cs addSss ss); fun Clarsimp_tac i = clarsimp_tac (Classical.claset(), Simplifier.simpset()) i; (* auto_tac *) fun blast_depth_tac cs m i thm = - 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 + +(* a variant of depth_tac that avoids interference of the simplifier with dup_step_tac when they are combined by auto_tac *) local -fun slow_step_tac' cs = Classical.appWrappers cs - (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs); -in fun nodup_depth_tac cs m i state = SELECT_GOAL - (Classical.safe_steps_tac cs 1 THEN_ELSE - (DEPTH_SOLVE (nodup_depth_tac cs m 1), - Classical.inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac - (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) 1)) +fun slow_step_tac' cs = Classical.appWrappers cs + (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs); +in fun nodup_depth_tac cs m i state = SELECT_GOAL + (Classical.safe_steps_tac cs 1 THEN_ELSE + (DEPTH_SOLVE (nodup_depth_tac cs m 1), + Classical.inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac + (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) 1)) )) i state; end; @@ -127,30 +127,31 @@ 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 wrappers *) + val maintac = + blast_depth_tac cs m (* fast but can't use wrappers *) ORELSE' (CHANGED o nodup_depth_tac cs' n); (* slower but more general *) in EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss), - TRY (Classical.safe_tac cs), - REPEAT (FIRSTGOAL maintac), + TRY (Classical.safe_tac cs), + REPEAT (FIRSTGOAL maintac), TRY (Classical.safe_tac (cs addSss ss)), - prune_params_tac] + prune_params_tac] end; -fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2; +fun auto_tac css = mk_auto_tac css 4 2; 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 [ - Classical.clarify_tac cs' 1, - IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1), - ALLGOALS (Classical.first_best_tac cs')]) end; + Classical.clarify_tac cs' 1, + IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1), + ALLGOALS (Classical.first_best_tac cs')]) end; fun Force_tac i = force_tac (Classical.claset(), Simplifier.simpset()) i; fun force i = by (Force_tac i); @@ -160,7 +161,7 @@ fun fast_simp_tac (cs, ss) = let val cs' = cs addss ss in Classical.fast_tac cs' end; -(* attributes *) +(* change clasimpset *) fun change_global_css f (thy, th) = let @@ -199,11 +200,20 @@ val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth'; +fun auto_args m = + Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m; + +fun auto_meth None = clasimp_meth (CHANGED o auto_tac) + | auto_meth (Some (m, n)) = clasimp_meth (CHANGED o (fn css => mk_auto_tac css m n)); + + +(* theory setup *) + val setup = [Method.add_methods [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"), ("force", clasimp_method' force_tac, "force"), - ("auto", clasimp_method (CHANGED o auto_tac), "auto"), + ("auto", auto_args auto_meth, "auto"), ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];