1 (* Title: Provers/clasimp.ML
3 Author: David von Oheimb, TU Muenchen
5 Combination of classical reasoner and simplifier (depends on
6 simplifier.ML, classical.ML, blast.ML).
9 infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2;
12 signature CLASIMP_DATA =
14 structure Simplifier: SIMPLIFIER
15 structure Classical: CLASSICAL
16 structure Blast: BLAST
17 sharing type Classical.claset = Blast.claset
26 val addSIs2 : clasimpset * thm list -> clasimpset
27 val addSEs2 : clasimpset * thm list -> clasimpset
28 val addSDs2 : clasimpset * thm list -> clasimpset
29 val addIs2 : clasimpset * thm list -> clasimpset
30 val addEs2 : clasimpset * thm list -> clasimpset
31 val addDs2 : clasimpset * thm list -> clasimpset
32 val addsimps2 : clasimpset * thm list -> clasimpset
33 val delsimps2 : clasimpset * thm list -> clasimpset
34 val addSss : claset * simpset -> claset
35 val addss : claset * simpset -> claset
36 val CLASIMPSET :(clasimpset -> tactic) -> tactic
37 val CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic
38 val clarsimp_tac: clasimpset -> int -> tactic
39 val Clarsimp_tac: int -> tactic
40 val mk_auto_tac : clasimpset -> int -> int -> tactic
41 val auto_tac : clasimpset -> tactic
43 val auto : unit -> unit
44 val force_tac : clasimpset -> int -> tactic
45 val Force_tac : int -> tactic
46 val force : int -> unit
49 functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
54 type claset = Classical.claset;
55 type simpset = Simplifier.simpset;
56 type clasimpset = claset * simpset;
59 (* clasimpset operations *)
61 (*this interface for updating a clasimpset is rudimentary and just for
62 convenience for the most common cases*)
64 fun pair_upd1 f ((a,b),x) = (f(a,x), b);
65 fun pair_upd2 f ((a,b),x) = (a, f(b,x));
67 fun op addSIs2 arg = pair_upd1 Classical.addSIs arg;
68 fun op addSEs2 arg = pair_upd1 Classical.addSEs arg;
69 fun op addSDs2 arg = pair_upd1 Classical.addSDs arg;
70 fun op addIs2 arg = pair_upd1 Classical.addIs arg;
71 fun op addEs2 arg = pair_upd1 Classical.addEs arg;
72 fun op addDs2 arg = pair_upd1 Classical.addDs arg;
73 fun op addsimps2 arg = pair_upd2 Simplifier.addsimps arg;
74 fun op delsimps2 arg = pair_upd2 Simplifier.delsimps arg;
76 (*Add a simpset to a classical set!*)
77 (*Caution: only one simpset added can be added by each of addSss and addss*)
78 fun cs addSss ss = op Classical.addSaltern (cs, ("safe_asm_full_simp_tac",
79 CHANGED o Simplifier.safe_asm_full_simp_tac ss));
80 fun cs addss ss = op Classical.addbefore (cs, ("asm_full_simp_tac",
81 CHANGED o Simplifier.asm_full_simp_tac ss));
85 fun CLASIMPSET tacf state =
86 Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss))) state;
88 fun CLASIMPSET' tacf i state =
89 Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state;
92 fun clarsimp_tac (cs, ss) = Simplifier.safe_asm_full_simp_tac ss THEN_MAYBE'
93 Classical.clarify_tac (cs addSss ss);
94 fun Clarsimp_tac i = clarsimp_tac (Classical.claset(), Simplifier.simpset()) i;
99 fun blast_depth_tac cs m i thm =
100 Blast.depth_tac cs m i thm
101 handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
103 (* a variant of depth_tac that avoids interference of the simplifier
104 with dup_step_tac when they are combined by auto_tac *)
105 fun nodup_depth_tac cs m i state = CHANGED (SELECT_GOAL
106 (REPEAT_DETERM1 (COND (has_fewer_prems 1) no_tac
107 (Classical.safe_step_tac cs 1))
108 THEN_ELSE (DEPTH_SOLVE (nodup_depth_tac cs m 1),
109 Classical.appWrappers cs (fn i => Classical.inst0_step_tac cs i APPEND
111 ((Classical.instp_step_tac cs i APPEND Classical.step_tac cs i)
112 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i))) 1))
115 (*Designed to be idempotent, except if best_tac instantiates variables
116 in some of the subgoals*)
117 fun mk_auto_tac (cs, ss) m n =
118 let val cs' = cs addss ss
120 blast_depth_tac cs m (* fast but can't use addss *)
122 nodup_depth_tac cs' n; (* slower but more general *)
123 in EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
124 TRY (Classical.safe_tac cs),
125 REPEAT (FIRSTGOAL maintac),
126 TRY (Classical.safe_tac (cs addSss ss)),
130 fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
132 fun Auto_tac st = auto_tac (Classical.claset(), Simplifier.simpset()) st;
134 fun auto () = by Auto_tac;
139 (* aimed to solve the given subgoal totally, using whatever tools possible *)
140 fun force_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [
141 Classical.clarify_tac cs' 1,
142 IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
143 ALLGOALS (Classical.best_tac cs')]) end;
144 fun Force_tac i = force_tac (Classical.claset(), Simplifier.simpset()) i;
145 fun force i = by (Force_tac i);