1(*  Title:      Provers/clasimp.ML
2    Author:     David von Oheimb, TU Muenchen
3
4Combination of classical reasoner and simplifier (depends on
5splitter.ML, classical.ML, blast.ML).
6*)
7
8signature CLASIMP_DATA =
9sig
10  structure Splitter: SPLITTER
11  structure Classical: CLASSICAL
12  structure Blast: BLAST
13  val notE: thm
14  val iffD1: thm
15  val iffD2: thm
16end;
17
18signature CLASIMP =
19sig
20  val addSss: Proof.context -> Proof.context
21  val addss: Proof.context -> Proof.context
22  val clarsimp_tac: Proof.context -> int -> tactic
23  val mk_auto_tac: Proof.context -> int -> int -> tactic
24  val auto_tac: Proof.context -> tactic
25  val force_tac: Proof.context -> int -> tactic
26  val fast_force_tac: Proof.context -> int -> tactic
27  val slow_simp_tac: Proof.context -> int -> tactic
28  val best_simp_tac: Proof.context -> int -> tactic
29  val iff_add: attribute
30  val iff_add': attribute
31  val iff_del: attribute
32  val iff_modifiers: Method.modifier parser list
33  val clasimp_modifiers: Method.modifier parser list
34end;
35
36functor Clasimp(Data: CLASIMP_DATA): CLASIMP =
37struct
38
39structure Splitter = Data.Splitter;
40structure Classical = Data.Classical;
41structure Blast = Data.Blast;
42
43
44(* simp as classical wrapper *)
45
46(* FIXME !? *)
47fun clasimp f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt));
48
49(*Add a simpset to the claset!*)
50(*Caution: only one simpset added can be added by each of addSss and addss*)
51val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
52val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
53
54
55(* iffs: addition of rules to simpsets and clasets simultaneously *)
56
57local
58
59(*Takes (possibly conditional) theorems of the form A<->B to
60        the Safe Intr     rule B==>A and
61        the Safe Destruct rule A==>B.
62  Also ~A goes to the Safe Elim rule A ==> ?R
63  Failing other cases, A is added as a Safe Intr rule*)
64
65fun add_iff safe unsafe =
66  Thm.declaration_attribute (fn th => fn context =>
67    let
68      val n = Thm.nprems_of th;
69      val (elim, intro) = if n = 0 then safe else unsafe;
70      val zero_rotate = zero_var_indexes o rotate_prems n;
71      val decls =
72        [(intro, zero_rotate (th RS Data.iffD2)),
73         (elim, Tactic.make_elim (zero_rotate (th RS Data.iffD1)))]
74        handle THM _ => [(elim, zero_rotate (th RS Data.notE))]
75        handle THM _ => [(intro, th)];
76    in fold (uncurry Thm.attribute_declaration) decls context end);
77
78fun del_iff del = Thm.declaration_attribute (fn th => fn context =>
79  let
80    val zero_rotate = zero_var_indexes o rotate_prems (Thm.nprems_of th);
81    val rls =
82      [zero_rotate (th RS Data.iffD2), Tactic.make_elim (zero_rotate (th RS Data.iffD1))]
83        handle THM _ => [zero_rotate (th RS Data.notE)]
84        handle THM _ => [th];
85  in fold (Thm.attribute_declaration del) rls context end);
86
87in
88
89val iff_add =
90  Thm.declaration_attribute (fn th =>
91    Thm.attribute_declaration (add_iff
92      (Classical.safe_elim NONE, Classical.safe_intro NONE)
93      (Classical.unsafe_elim NONE, Classical.unsafe_intro NONE)) th
94    #> Thm.attribute_declaration Simplifier.simp_add th);
95
96val iff_add' =
97  add_iff
98    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE)
99    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE);
100
101val iff_del =
102  Thm.declaration_attribute (fn th =>
103    Thm.attribute_declaration (del_iff Classical.rule_del) th #>
104    Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #>
105    Thm.attribute_declaration Simplifier.simp_del th);
106
107end;
108
109
110(* tactics *)
111
112fun clarsimp_tac ctxt =
113  Simplifier.safe_asm_full_simp_tac ctxt THEN_ALL_NEW
114  Classical.clarify_tac (addSss ctxt);
115
116
117(* auto_tac *)
118
119(* a variant of depth_tac that avoids interference of the simplifier
120   with dup_step_tac when they are combined by auto_tac *)
121local
122
123fun slow_step_tac' ctxt =
124  Classical.appWrappers ctxt
125    (Classical.instp_step_tac ctxt APPEND' Classical.unsafe_step_tac ctxt);
126
127in
128
129fun nodup_depth_tac ctxt m i st =
130  SELECT_GOAL
131    (Classical.safe_steps_tac ctxt 1 THEN_ELSE
132      (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
133        Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
134          (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
135
136end;
137
138(*Designed to be idempotent, except if Blast.depth_tac instantiates variables
139  in some of the subgoals*)
140fun mk_auto_tac ctxt m n =
141  let
142    val main_tac =
143      Blast.depth_tac ctxt m  (* fast but can't use wrappers *)
144      ORELSE'
145      (CHANGED o nodup_depth_tac (addss ctxt) n);  (* slower but more general *)
146  in
147    PARALLEL_ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN
148    TRY (Classical.safe_tac ctxt) THEN
149    REPEAT_DETERM (FIRSTGOAL main_tac) THEN
150    TRY (Classical.safe_tac (addSss ctxt)) THEN
151    prune_params_tac ctxt
152  end;
153
154fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
155
156
157(* force_tac *)
158
159(* aimed to solve the given subgoal totally, using whatever tools possible *)
160fun force_tac ctxt =
161  let val ctxt' = addss ctxt in
162    SELECT_GOAL
163     (Classical.clarify_tac ctxt' 1 THEN
164      IF_UNSOLVED (Simplifier.asm_full_simp_tac ctxt 1) THEN
165      ALLGOALS (Classical.first_best_tac ctxt'))
166  end;
167
168
169(* basic combinations *)
170
171val fast_force_tac = Classical.fast_tac o addss;
172val slow_simp_tac = Classical.slow_tac o addss;
173val best_simp_tac = Classical.best_tac o addss;
174
175
176
177(** concrete syntax **)
178
179(* attributes *)
180
181val _ =
182  Theory.setup
183    (Attrib.setup @{binding iff}
184      (Scan.lift
185        (Args.del >> K iff_del ||
186          Scan.option Args.add -- Args.query >> K iff_add' ||
187          Scan.option Args.add >> K iff_add))
188      "declaration of Simplifier / Classical rules");
189
190
191(* method modifiers *)
192
193val iffN = "iff";
194
195val iff_modifiers =
196 [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>),
197  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' \<^here>),
198  Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
199
200val clasimp_modifiers =
201  Simplifier.simp_modifiers @ Splitter.split_modifiers @
202  Classical.cla_modifiers @ iff_modifiers;
203
204
205(* methods *)
206
207fun clasimp_method' tac =
208  Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
209
210val auto_method =
211  Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
212    Method.sections clasimp_modifiers >>
213  (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
214    | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
215
216val _ =
217  Theory.setup
218   (Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
219    Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
220    Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
221    Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
222    Method.setup @{binding auto} auto_method "auto" #>
223    Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
224      "clarify simplified goal");
225
226end;
227