1.1 --- a/src/Provers/clasimp.ML Fri Sep 01 00:30:25 2000 +0200
1.2 +++ b/src/Provers/clasimp.ML Fri Sep 01 00:31:08 2000 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -(* Title: Provers/clasimp.ML
1.5 +(* Title: Provers/clasimp.ML
1.6 ID: $Id$
1.7 Author: David von Oheimb, TU Muenchen
1.8
1.9 @@ -24,33 +24,33 @@
1.10 type claset
1.11 type simpset
1.12 type clasimpset
1.13 - val addSIs2 : clasimpset * thm list -> clasimpset
1.14 - val addSEs2 : clasimpset * thm list -> clasimpset
1.15 - val addSDs2 : clasimpset * thm list -> clasimpset
1.16 - val addIs2 : clasimpset * thm list -> clasimpset
1.17 - val addEs2 : clasimpset * thm list -> clasimpset
1.18 - val addDs2 : clasimpset * thm list -> clasimpset
1.19 - val addsimps2 : clasimpset * thm list -> clasimpset
1.20 - val delsimps2 : clasimpset * thm list -> clasimpset
1.21 - val addSss : claset * simpset -> claset
1.22 - val addss : claset * simpset -> claset
1.23 + val addSIs2 : clasimpset * thm list -> clasimpset
1.24 + val addSEs2 : clasimpset * thm list -> clasimpset
1.25 + val addSDs2 : clasimpset * thm list -> clasimpset
1.26 + val addIs2 : clasimpset * thm list -> clasimpset
1.27 + val addEs2 : clasimpset * thm list -> clasimpset
1.28 + val addDs2 : clasimpset * thm list -> clasimpset
1.29 + val addsimps2 : clasimpset * thm list -> clasimpset
1.30 + val delsimps2 : clasimpset * thm list -> clasimpset
1.31 + val addSss : claset * simpset -> claset
1.32 + val addss : claset * simpset -> claset
1.33 val CLASIMPSET :(clasimpset -> tactic) -> tactic
1.34 val CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic
1.35 val clarsimp_tac: clasimpset -> int -> tactic
1.36 val Clarsimp_tac: int -> tactic
1.37 val mk_auto_tac : clasimpset -> int -> int -> tactic
1.38 - val auto_tac : clasimpset -> tactic
1.39 - val Auto_tac : tactic
1.40 - val auto : unit -> unit
1.41 - val force_tac : clasimpset -> int -> tactic
1.42 - val Force_tac : int -> tactic
1.43 - val force : int -> unit
1.44 + val auto_tac : clasimpset -> tactic
1.45 + val Auto_tac : tactic
1.46 + val auto : unit -> unit
1.47 + val force_tac : clasimpset -> int -> tactic
1.48 + val Force_tac : int -> tactic
1.49 + val force : int -> unit
1.50 val fast_simp_tac : clasimpset -> int -> tactic
1.51 val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
1.52 val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
1.53 val get_local_clasimpset: Proof.context -> clasimpset
1.54 val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
1.55 - val setup : (theory -> theory) list
1.56 + val setup : (theory -> theory) list
1.57 end;
1.58
1.59 functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
1.60 @@ -86,9 +86,9 @@
1.61 (*Add a simpset to a classical set!*)
1.62 (*Caution: only one simpset added can be added by each of addSss and addss*)
1.63 fun cs addSss ss = Classical.addSaltern (cs, ("safe_asm_full_simp_tac",
1.64 - CHANGED o safe_asm_full_simp_tac ss));
1.65 -fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac",
1.66 - CHANGED o Simplifier.asm_full_simp_tac ss));
1.67 + CHANGED o safe_asm_full_simp_tac ss));
1.68 +fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac",
1.69 + CHANGED o Simplifier.asm_full_simp_tac ss));
1.70
1.71 (* tacticals *)
1.72
1.73 @@ -100,26 +100,26 @@
1.74
1.75
1.76 fun clarsimp_tac (cs, ss) = safe_asm_full_simp_tac ss THEN_ALL_NEW
1.77 - Classical.clarify_tac (cs addSss ss);
1.78 + Classical.clarify_tac (cs addSss ss);
1.79 fun Clarsimp_tac i = clarsimp_tac (Classical.claset(), Simplifier.simpset()) i;
1.80
1.81
1.82 (* auto_tac *)
1.83
1.84 fun blast_depth_tac cs m i thm =
1.85 - Blast.depth_tac cs m i thm
1.86 + Blast.depth_tac cs m i thm
1.87 handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
1.88 -
1.89 -(* a variant of depth_tac that avoids interference of the simplifier
1.90 +
1.91 +(* a variant of depth_tac that avoids interference of the simplifier
1.92 with dup_step_tac when they are combined by auto_tac *)
1.93 local
1.94 -fun slow_step_tac' cs = Classical.appWrappers cs
1.95 - (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs);
1.96 -in fun nodup_depth_tac cs m i state = SELECT_GOAL
1.97 - (Classical.safe_steps_tac cs 1 THEN_ELSE
1.98 - (DEPTH_SOLVE (nodup_depth_tac cs m 1),
1.99 - Classical.inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
1.100 - (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) 1))
1.101 +fun slow_step_tac' cs = Classical.appWrappers cs
1.102 + (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs);
1.103 +in fun nodup_depth_tac cs m i state = SELECT_GOAL
1.104 + (Classical.safe_steps_tac cs 1 THEN_ELSE
1.105 + (DEPTH_SOLVE (nodup_depth_tac cs m 1),
1.106 + Classical.inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
1.107 + (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) 1))
1.108 )) i state;
1.109 end;
1.110
1.111 @@ -127,30 +127,31 @@
1.112 in some of the subgoals*)
1.113 fun mk_auto_tac (cs, ss) m n =
1.114 let val cs' = cs addss ss
1.115 - val maintac =
1.116 - blast_depth_tac cs m (* fast but can't use wrappers *)
1.117 + val maintac =
1.118 + blast_depth_tac cs m (* fast but can't use wrappers *)
1.119 ORELSE'
1.120 (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
1.121 in EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
1.122 - TRY (Classical.safe_tac cs),
1.123 - REPEAT (FIRSTGOAL maintac),
1.124 + TRY (Classical.safe_tac cs),
1.125 + REPEAT (FIRSTGOAL maintac),
1.126 TRY (Classical.safe_tac (cs addSss ss)),
1.127 - prune_params_tac]
1.128 + prune_params_tac]
1.129 end;
1.130
1.131 -fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
1.132 +fun auto_tac css = mk_auto_tac css 4 2;
1.133
1.134 fun Auto_tac st = auto_tac (Classical.claset(), Simplifier.simpset()) st;
1.135
1.136 fun auto () = by Auto_tac;
1.137
1.138 +
1.139 (* force_tac *)
1.140
1.141 (* aimed to solve the given subgoal totally, using whatever tools possible *)
1.142 fun force_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [
1.143 - Classical.clarify_tac cs' 1,
1.144 - IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
1.145 - ALLGOALS (Classical.first_best_tac cs')]) end;
1.146 + Classical.clarify_tac cs' 1,
1.147 + IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
1.148 + ALLGOALS (Classical.first_best_tac cs')]) end;
1.149 fun Force_tac i = force_tac (Classical.claset(), Simplifier.simpset()) i;
1.150 fun force i = by (Force_tac i);
1.151
1.152 @@ -160,7 +161,7 @@
1.153 fun fast_simp_tac (cs, ss) = let val cs' = cs addss ss in Classical.fast_tac cs' end;
1.154
1.155
1.156 -(* attributes *)
1.157 +(* change clasimpset *)
1.158
1.159 fun change_global_css f (thy, th) =
1.160 let
1.161 @@ -199,11 +200,20 @@
1.162 val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
1.163
1.164
1.165 +fun auto_args m =
1.166 + Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m;
1.167 +
1.168 +fun auto_meth None = clasimp_meth (CHANGED o auto_tac)
1.169 + | auto_meth (Some (m, n)) = clasimp_meth (CHANGED o (fn css => mk_auto_tac css m n));
1.170 +
1.171 +
1.172 +(* theory setup *)
1.173 +
1.174 val setup =
1.175 [Method.add_methods
1.176 [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
1.177 ("force", clasimp_method' force_tac, "force"),
1.178 - ("auto", clasimp_method (CHANGED o auto_tac), "auto"),
1.179 + ("auto", auto_args auto_meth, "auto"),
1.180 ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];
1.181
1.182