1 (* Title: Pure/meta_simplifier.ML |
|
2 Author: Tobias Nipkow and Stefan Berghofer, TU Muenchen |
|
3 |
|
4 Meta-level Simplification. |
|
5 *) |
|
6 |
|
7 infix 4 |
|
8 addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs |
|
9 setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler |
|
10 setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver; |
|
11 |
|
12 signature BASIC_META_SIMPLIFIER = |
|
13 sig |
|
14 val simp_debug: bool Config.T |
|
15 val simp_debug_raw: Config.raw |
|
16 val simp_trace: bool Config.T |
|
17 val simp_trace_raw: Config.raw |
|
18 val simp_trace_default: bool Unsynchronized.ref |
|
19 val simp_trace_depth_limit: int Config.T |
|
20 val simp_trace_depth_limit_raw: Config.raw |
|
21 val simp_trace_depth_limit_default: int Unsynchronized.ref |
|
22 type rrule |
|
23 val eq_rrule: rrule * rrule -> bool |
|
24 type simpset |
|
25 type proc |
|
26 type solver |
|
27 val mk_solver': string -> (simpset -> int -> tactic) -> solver |
|
28 val mk_solver: string -> (thm list -> int -> tactic) -> solver |
|
29 val empty_ss: simpset |
|
30 val merge_ss: simpset * simpset -> simpset |
|
31 val dest_ss: simpset -> |
|
32 {simps: (string * thm) list, |
|
33 procs: (string * cterm list) list, |
|
34 congs: (string * thm) list, |
|
35 weak_congs: string list, |
|
36 loopers: string list, |
|
37 unsafe_solvers: string list, |
|
38 safe_solvers: string list} |
|
39 type simproc |
|
40 val eq_simproc: simproc * simproc -> bool |
|
41 val morph_simproc: morphism -> simproc -> simproc |
|
42 val make_simproc: {name: string, lhss: cterm list, |
|
43 proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc |
|
44 val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc |
|
45 val add_prems: thm list -> simpset -> simpset |
|
46 val prems_of_ss: simpset -> thm list |
|
47 val addsimps: simpset * thm list -> simpset |
|
48 val delsimps: simpset * thm list -> simpset |
|
49 val addeqcongs: simpset * thm list -> simpset |
|
50 val deleqcongs: simpset * thm list -> simpset |
|
51 val addcongs: simpset * thm list -> simpset |
|
52 val delcongs: simpset * thm list -> simpset |
|
53 val addsimprocs: simpset * simproc list -> simpset |
|
54 val delsimprocs: simpset * simproc list -> simpset |
|
55 val mksimps: simpset -> thm -> thm list |
|
56 val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset |
|
57 val setmkcong: simpset * (simpset -> thm -> thm) -> simpset |
|
58 val setmksym: simpset * (simpset -> thm -> thm option) -> simpset |
|
59 val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset |
|
60 val settermless: simpset * (term * term -> bool) -> simpset |
|
61 val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset |
|
62 val setloop': simpset * (simpset -> int -> tactic) -> simpset |
|
63 val setloop: simpset * (int -> tactic) -> simpset |
|
64 val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset |
|
65 val addloop: simpset * (string * (int -> tactic)) -> simpset |
|
66 val delloop: simpset * string -> simpset |
|
67 val setSSolver: simpset * solver -> simpset |
|
68 val addSSolver: simpset * solver -> simpset |
|
69 val setSolver: simpset * solver -> simpset |
|
70 val addSolver: simpset * solver -> simpset |
|
71 |
|
72 val rewrite_rule: thm list -> thm -> thm |
|
73 val rewrite_goals_rule: thm list -> thm -> thm |
|
74 val rewrite_goals_tac: thm list -> tactic |
|
75 val rewrite_goal_tac: thm list -> int -> tactic |
|
76 val rewtac: thm -> tactic |
|
77 val prune_params_tac: tactic |
|
78 val fold_rule: thm list -> thm -> thm |
|
79 val fold_goals_tac: thm list -> tactic |
|
80 val norm_hhf: thm -> thm |
|
81 val norm_hhf_protect: thm -> thm |
|
82 end; |
|
83 |
|
84 signature META_SIMPLIFIER = |
|
85 sig |
|
86 include BASIC_META_SIMPLIFIER |
|
87 exception SIMPLIFIER of string * thm |
|
88 val internal_ss: simpset -> |
|
89 {rules: rrule Net.net, |
|
90 prems: thm list, |
|
91 bounds: int * ((string * typ) * string) list, |
|
92 depth: int * bool Unsynchronized.ref, |
|
93 context: Proof.context option} * |
|
94 {congs: (string * thm) list * string list, |
|
95 procs: proc Net.net, |
|
96 mk_rews: |
|
97 {mk: simpset -> thm -> thm list, |
|
98 mk_cong: simpset -> thm -> thm, |
|
99 mk_sym: simpset -> thm -> thm option, |
|
100 mk_eq_True: simpset -> thm -> thm option, |
|
101 reorient: theory -> term list -> term -> term -> bool}, |
|
102 termless: term * term -> bool, |
|
103 subgoal_tac: simpset -> int -> tactic, |
|
104 loop_tacs: (string * (simpset -> int -> tactic)) list, |
|
105 solvers: solver list * solver list} |
|
106 val add_simp: thm -> simpset -> simpset |
|
107 val del_simp: thm -> simpset -> simpset |
|
108 val solver: simpset -> solver -> int -> tactic |
|
109 val simp_depth_limit_raw: Config.raw |
|
110 val simp_depth_limit: int Config.T |
|
111 val clear_ss: simpset -> simpset |
|
112 val simproc_global_i: theory -> string -> term list |
|
113 -> (theory -> simpset -> term -> thm option) -> simproc |
|
114 val simproc_global: theory -> string -> string list |
|
115 -> (theory -> simpset -> term -> thm option) -> simproc |
|
116 val inherit_context: simpset -> simpset -> simpset |
|
117 val the_context: simpset -> Proof.context |
|
118 val context: Proof.context -> simpset -> simpset |
|
119 val global_context: theory -> simpset -> simpset |
|
120 val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset |
|
121 val debug_bounds: bool Unsynchronized.ref |
|
122 val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset |
|
123 val set_solvers: solver list -> simpset -> simpset |
|
124 val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv |
|
125 val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term |
|
126 val rewrite_thm: bool * bool * bool -> |
|
127 (simpset -> thm -> thm option) -> simpset -> thm -> thm |
|
128 val rewrite_goal_rule: bool * bool * bool -> |
|
129 (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm |
|
130 val asm_rewrite_goal_tac: bool * bool * bool -> |
|
131 (simpset -> tactic) -> simpset -> int -> tactic |
|
132 val rewrite: bool -> thm list -> conv |
|
133 val simplify: bool -> thm list -> thm -> thm |
|
134 end; |
|
135 |
|
136 structure MetaSimplifier: META_SIMPLIFIER = |
|
137 struct |
|
138 |
|
139 (** datatype simpset **) |
|
140 |
|
141 (* rewrite rules *) |
|
142 |
|
143 type rrule = |
|
144 {thm: thm, (*the rewrite rule*) |
|
145 name: string, (*name of theorem from which rewrite rule was extracted*) |
|
146 lhs: term, (*the left-hand side*) |
|
147 elhs: cterm, (*the etac-contracted lhs*) |
|
148 extra: bool, (*extra variables outside of elhs*) |
|
149 fo: bool, (*use first-order matching*) |
|
150 perm: bool}; (*the rewrite rule is permutative*) |
|
151 |
|
152 (* |
|
153 Remarks: |
|
154 - elhs is used for matching, |
|
155 lhs only for preservation of bound variable names; |
|
156 - fo is set iff |
|
157 either elhs is first-order (no Var is applied), |
|
158 in which case fo-matching is complete, |
|
159 or elhs is not a pattern, |
|
160 in which case there is nothing better to do; |
|
161 *) |
|
162 |
|
163 fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) = |
|
164 Thm.eq_thm_prop (thm1, thm2); |
|
165 |
|
166 |
|
167 (* simplification sets, procedures, and solvers *) |
|
168 |
|
169 (*A simpset contains data required during conversion: |
|
170 rules: discrimination net of rewrite rules; |
|
171 prems: current premises; |
|
172 bounds: maximal index of bound variables already used |
|
173 (for generating new names when rewriting under lambda abstractions); |
|
174 depth: simp_depth and exceeded flag; |
|
175 congs: association list of congruence rules and |
|
176 a list of `weak' congruence constants. |
|
177 A congruence is `weak' if it avoids normalization of some argument. |
|
178 procs: discrimination net of simplification procedures |
|
179 (functions that prove rewrite rules on the fly); |
|
180 mk_rews: |
|
181 mk: turn simplification thms into rewrite rules; |
|
182 mk_cong: prepare congruence rules; |
|
183 mk_sym: turn == around; |
|
184 mk_eq_True: turn P into P == True; |
|
185 termless: relation for ordered rewriting;*) |
|
186 |
|
187 datatype simpset = |
|
188 Simpset of |
|
189 {rules: rrule Net.net, |
|
190 prems: thm list, |
|
191 bounds: int * ((string * typ) * string) list, |
|
192 depth: int * bool Unsynchronized.ref, |
|
193 context: Proof.context option} * |
|
194 {congs: (string * thm) list * string list, |
|
195 procs: proc Net.net, |
|
196 mk_rews: |
|
197 {mk: simpset -> thm -> thm list, |
|
198 mk_cong: simpset -> thm -> thm, |
|
199 mk_sym: simpset -> thm -> thm option, |
|
200 mk_eq_True: simpset -> thm -> thm option, |
|
201 reorient: theory -> term list -> term -> term -> bool}, |
|
202 termless: term * term -> bool, |
|
203 subgoal_tac: simpset -> int -> tactic, |
|
204 loop_tacs: (string * (simpset -> int -> tactic)) list, |
|
205 solvers: solver list * solver list} |
|
206 and proc = |
|
207 Proc of |
|
208 {name: string, |
|
209 lhs: cterm, |
|
210 proc: simpset -> cterm -> thm option, |
|
211 id: stamp * thm list} |
|
212 and solver = |
|
213 Solver of |
|
214 {name: string, |
|
215 solver: simpset -> int -> tactic, |
|
216 id: stamp}; |
|
217 |
|
218 |
|
219 fun internal_ss (Simpset args) = args; |
|
220 |
|
221 fun make_ss1 (rules, prems, bounds, depth, context) = |
|
222 {rules = rules, prems = prems, bounds = bounds, depth = depth, context = context}; |
|
223 |
|
224 fun map_ss1 f {rules, prems, bounds, depth, context} = |
|
225 make_ss1 (f (rules, prems, bounds, depth, context)); |
|
226 |
|
227 fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) = |
|
228 {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless, |
|
229 subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers}; |
|
230 |
|
231 fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} = |
|
232 make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); |
|
233 |
|
234 fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2); |
|
235 |
|
236 fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2); |
|
237 fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2); |
|
238 |
|
239 fun prems_of_ss (Simpset ({prems, ...}, _)) = prems; |
|
240 |
|
241 fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) = |
|
242 s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2); |
|
243 fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2); |
|
244 |
|
245 fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()}; |
|
246 fun mk_solver name solver = mk_solver' name (solver o prems_of_ss); |
|
247 |
|
248 fun solver_name (Solver {name, ...}) = name; |
|
249 fun solver ss (Solver {solver = tac, ...}) = tac ss; |
|
250 fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2); |
|
251 |
|
252 |
|
253 (* simp depth *) |
|
254 |
|
255 val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100)); |
|
256 val simp_depth_limit = Config.int simp_depth_limit_raw; |
|
257 |
|
258 val simp_trace_depth_limit_default = Unsynchronized.ref 1; |
|
259 val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit" |
|
260 (fn _ => Config.Int (! simp_trace_depth_limit_default)); |
|
261 val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw; |
|
262 |
|
263 fun simp_trace_depth_limit_of NONE = ! simp_trace_depth_limit_default |
|
264 | simp_trace_depth_limit_of (SOME ctxt) = Config.get ctxt simp_trace_depth_limit; |
|
265 |
|
266 fun trace_depth (Simpset ({depth = (depth, exceeded), context, ...}, _)) msg = |
|
267 if depth > simp_trace_depth_limit_of context then |
|
268 if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true) |
|
269 else |
|
270 (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false); |
|
271 |
|
272 val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) => |
|
273 (rules, prems, bounds, |
|
274 (depth + 1, |
|
275 if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context)); |
|
276 |
|
277 fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth; |
|
278 |
|
279 |
|
280 (* diagnostics *) |
|
281 |
|
282 exception SIMPLIFIER of string * thm; |
|
283 |
|
284 val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false)); |
|
285 val simp_debug = Config.bool simp_debug_raw; |
|
286 |
|
287 val simp_trace_default = Unsynchronized.ref false; |
|
288 val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default)); |
|
289 val simp_trace = Config.bool simp_trace_raw; |
|
290 |
|
291 fun if_enabled (Simpset ({context, ...}, _)) flag f = |
|
292 (case context of |
|
293 SOME ctxt => if Config.get ctxt flag then f ctxt else () |
|
294 | NONE => ()) |
|
295 |
|
296 fun if_visible (Simpset ({context, ...}, _)) f x = |
|
297 (case context of |
|
298 SOME ctxt => if Context_Position.is_visible ctxt then f x else () |
|
299 | NONE => ()); |
|
300 |
|
301 local |
|
302 |
|
303 fun prnt ss warn a = if warn then warning a else trace_depth ss a; |
|
304 |
|
305 fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t = |
|
306 let |
|
307 val names = Term.declare_term_names t Name.context; |
|
308 val xs = rev (#1 (Name.variants (rev (map #2 bs)) names)); |
|
309 fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T)); |
|
310 in Term.subst_atomic (ListPair.map subst (bs, xs)) t end; |
|
311 |
|
312 fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^ |
|
313 Syntax.string_of_term ctxt |
|
314 (if Config.get ctxt simp_debug then t else show_bounds ss t)); |
|
315 |
|
316 in |
|
317 |
|
318 fun print_term_global ss warn a thy t = |
|
319 print_term ss warn (K a) t (ProofContext.init_global thy); |
|
320 |
|
321 fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ())); |
|
322 fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ())); |
|
323 |
|
324 fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t); |
|
325 fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t); |
|
326 |
|
327 fun trace_cterm warn a ss ct = |
|
328 if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct)); |
|
329 |
|
330 fun trace_thm a ss th = |
|
331 if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th)); |
|
332 |
|
333 fun trace_named_thm a ss (th, name) = |
|
334 if_enabled ss simp_trace (print_term ss false |
|
335 (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":") |
|
336 (Thm.full_prop_of th)); |
|
337 |
|
338 fun warn_thm a ss th = |
|
339 print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th); |
|
340 |
|
341 fun cond_warn_thm a ss th = if_visible ss (fn () => warn_thm a ss th) (); |
|
342 |
|
343 end; |
|
344 |
|
345 |
|
346 |
|
347 (** simpset operations **) |
|
348 |
|
349 (* context *) |
|
350 |
|
351 fun eq_bound (x: string, (y, _)) = x = y; |
|
352 |
|
353 fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds), depth, context) => |
|
354 (rules, prems, (count + 1, bound :: bounds), depth, context)); |
|
355 |
|
356 fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth, context) => |
|
357 (rules, ths @ prems, bounds, depth, context)); |
|
358 |
|
359 fun inherit_context (Simpset ({bounds, depth, context, ...}, _)) = |
|
360 map_simpset1 (fn (rules, prems, _, _, _) => (rules, prems, bounds, depth, context)); |
|
361 |
|
362 fun the_context (Simpset ({context = SOME ctxt, ...}, _)) = ctxt |
|
363 | the_context _ = raise Fail "Simplifier: no proof context in simpset"; |
|
364 |
|
365 fun context ctxt = |
|
366 map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt)); |
|
367 |
|
368 val global_context = context o ProofContext.init_global; |
|
369 |
|
370 fun activate_context thy ss = |
|
371 let |
|
372 val ctxt = the_context ss; |
|
373 val ctxt' = ctxt |
|
374 |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt)) |
|
375 |> Context_Position.set_visible false; |
|
376 in context ctxt' ss end; |
|
377 |
|
378 fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss)); |
|
379 |
|
380 |
|
381 (* maintain simp rules *) |
|
382 |
|
383 (* FIXME: it seems that the conditions on extra variables are too liberal if |
|
384 prems are nonempty: does solving the prems really guarantee instantiation of |
|
385 all its Vars? Better: a dynamic check each time a rule is applied. |
|
386 *) |
|
387 fun rewrite_rule_extra_vars prems elhs erhs = |
|
388 let |
|
389 val elhss = elhs :: prems; |
|
390 val tvars = fold Term.add_tvars elhss []; |
|
391 val vars = fold Term.add_vars elhss []; |
|
392 in |
|
393 erhs |> Term.exists_type (Term.exists_subtype |
|
394 (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse |
|
395 erhs |> Term.exists_subterm |
|
396 (fn Var v => not (member (op =) vars v) | _ => false) |
|
397 end; |
|
398 |
|
399 fun rrule_extra_vars elhs thm = |
|
400 rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm); |
|
401 |
|
402 fun mk_rrule2 {thm, name, lhs, elhs, perm} = |
|
403 let |
|
404 val t = term_of elhs; |
|
405 val fo = Pattern.first_order t orelse not (Pattern.pattern t); |
|
406 val extra = rrule_extra_vars elhs thm; |
|
407 in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end; |
|
408 |
|
409 fun del_rrule (rrule as {thm, elhs, ...}) ss = |
|
410 ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) => |
|
411 (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context)) |
|
412 handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss); |
|
413 |
|
414 fun insert_rrule (rrule as {thm, name, ...}) ss = |
|
415 (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name); |
|
416 ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) => |
|
417 let |
|
418 val rrule2 as {elhs, ...} = mk_rrule2 rrule; |
|
419 val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules; |
|
420 in (rules', prems, bounds, depth, context) end) |
|
421 handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss)); |
|
422 |
|
423 fun vperm (Var _, Var _) = true |
|
424 | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) |
|
425 | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) |
|
426 | vperm (t, u) = (t = u); |
|
427 |
|
428 fun var_perm (t, u) = |
|
429 vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []); |
|
430 |
|
431 (*simple test for looping rewrite rules and stupid orientations*) |
|
432 fun default_reorient thy prems lhs rhs = |
|
433 rewrite_rule_extra_vars prems lhs rhs |
|
434 orelse |
|
435 is_Var (head_of lhs) |
|
436 orelse |
|
437 (* turns t = x around, which causes a headache if x is a local variable - |
|
438 usually it is very useful :-( |
|
439 is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs)) |
|
440 andalso not(exists_subterm is_Var lhs) |
|
441 orelse |
|
442 *) |
|
443 exists (fn t => Logic.occs (lhs, t)) (rhs :: prems) |
|
444 orelse |
|
445 null prems andalso Pattern.matches thy (lhs, rhs) |
|
446 (*the condition "null prems" is necessary because conditional rewrites |
|
447 with extra variables in the conditions may terminate although |
|
448 the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*) |
|
449 orelse |
|
450 is_Const lhs andalso not (is_Const rhs); |
|
451 |
|
452 fun decomp_simp thm = |
|
453 let |
|
454 val thy = Thm.theory_of_thm thm; |
|
455 val prop = Thm.prop_of thm; |
|
456 val prems = Logic.strip_imp_prems prop; |
|
457 val concl = Drule.strip_imp_concl (Thm.cprop_of thm); |
|
458 val (lhs, rhs) = Thm.dest_equals concl handle TERM _ => |
|
459 raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm); |
|
460 val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs)); |
|
461 val elhs = if term_of elhs aconv term_of lhs then lhs else elhs; (*share identical copies*) |
|
462 val erhs = Envir.eta_contract (term_of rhs); |
|
463 val perm = |
|
464 var_perm (term_of elhs, erhs) andalso |
|
465 not (term_of elhs aconv erhs) andalso |
|
466 not (is_Var (term_of elhs)); |
|
467 in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end; |
|
468 |
|
469 fun decomp_simp' thm = |
|
470 let val (_, _, lhs, _, rhs, _) = decomp_simp thm in |
|
471 if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm) |
|
472 else (lhs, rhs) |
|
473 end; |
|
474 |
|
475 fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) = |
|
476 (case mk_eq_True ss thm of |
|
477 NONE => [] |
|
478 | SOME eq_True => |
|
479 let |
|
480 val (_, _, lhs, elhs, _, _) = decomp_simp eq_True; |
|
481 in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end); |
|
482 |
|
483 (*create the rewrite rule and possibly also the eq_True variant, |
|
484 in case there are extra vars on the rhs*) |
|
485 fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) = |
|
486 let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in |
|
487 if rewrite_rule_extra_vars [] lhs rhs then |
|
488 mk_eq_True ss (thm2, name) @ [rrule] |
|
489 else [rrule] |
|
490 end; |
|
491 |
|
492 fun mk_rrule ss (thm, name) = |
|
493 let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in |
|
494 if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] |
|
495 else |
|
496 (*weak test for loops*) |
|
497 if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs) |
|
498 then mk_eq_True ss (thm, name) |
|
499 else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm) |
|
500 end; |
|
501 |
|
502 fun orient_rrule ss (thm, name) = |
|
503 let |
|
504 val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm; |
|
505 val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss; |
|
506 in |
|
507 if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] |
|
508 else if reorient thy prems lhs rhs then |
|
509 if reorient thy prems rhs lhs |
|
510 then mk_eq_True ss (thm, name) |
|
511 else |
|
512 (case mk_sym ss thm of |
|
513 NONE => [] |
|
514 | SOME thm' => |
|
515 let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm' |
|
516 in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end) |
|
517 else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm) |
|
518 end; |
|
519 |
|
520 fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) = |
|
521 maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms; |
|
522 |
|
523 fun extract_safe_rrules (ss, thm) = |
|
524 maps (orient_rrule ss) (extract_rews (ss, [thm])); |
|
525 |
|
526 |
|
527 (* add/del rules explicitly *) |
|
528 |
|
529 fun comb_simps comb mk_rrule (ss, thms) = |
|
530 let |
|
531 val rews = extract_rews (ss, thms); |
|
532 in fold (fold comb o mk_rrule) rews ss end; |
|
533 |
|
534 fun ss addsimps thms = |
|
535 comb_simps insert_rrule (mk_rrule ss) (ss, thms); |
|
536 |
|
537 fun ss delsimps thms = |
|
538 comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms); |
|
539 |
|
540 fun add_simp thm ss = ss addsimps [thm]; |
|
541 fun del_simp thm ss = ss delsimps [thm]; |
|
542 |
|
543 |
|
544 (* congs *) |
|
545 |
|
546 fun cong_name (Const (a, _)) = SOME a |
|
547 | cong_name (Free (a, _)) = SOME ("Free: " ^ a) |
|
548 | cong_name _ = NONE; |
|
549 |
|
550 local |
|
551 |
|
552 fun is_full_cong_prems [] [] = true |
|
553 | is_full_cong_prems [] _ = false |
|
554 | is_full_cong_prems (p :: prems) varpairs = |
|
555 (case Logic.strip_assums_concl p of |
|
556 Const ("==", _) $ lhs $ rhs => |
|
557 let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in |
|
558 is_Var x andalso forall is_Bound xs andalso |
|
559 not (has_duplicates (op =) xs) andalso xs = ys andalso |
|
560 member (op =) varpairs (x, y) andalso |
|
561 is_full_cong_prems prems (remove (op =) (x, y) varpairs) |
|
562 end |
|
563 | _ => false); |
|
564 |
|
565 fun is_full_cong thm = |
|
566 let |
|
567 val prems = prems_of thm and concl = concl_of thm; |
|
568 val (lhs, rhs) = Logic.dest_equals concl; |
|
569 val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs; |
|
570 in |
|
571 f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso |
|
572 is_full_cong_prems prems (xs ~~ ys) |
|
573 end; |
|
574 |
|
575 fun add_cong (ss, thm) = ss |> |
|
576 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
577 let |
|
578 val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm)) |
|
579 handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
|
580 (*val lhs = Envir.eta_contract lhs;*) |
|
581 val a = the (cong_name (head_of (term_of lhs))) handle Option.Option => |
|
582 raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm); |
|
583 val (xs, weak) = congs; |
|
584 val _ = |
|
585 if AList.defined (op =) xs a |
|
586 then if_visible ss warning ("Overwriting congruence rule for " ^ quote a) |
|
587 else (); |
|
588 val xs' = AList.update (op =) (a, thm) xs; |
|
589 val weak' = if is_full_cong thm then weak else a :: weak; |
|
590 in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); |
|
591 |
|
592 fun del_cong (ss, thm) = ss |> |
|
593 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
594 let |
|
595 val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ => |
|
596 raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
|
597 (*val lhs = Envir.eta_contract lhs;*) |
|
598 val a = the (cong_name (head_of lhs)) handle Option.Option => |
|
599 raise SIMPLIFIER ("Congruence must start with a constant", thm); |
|
600 val (xs, _) = congs; |
|
601 val xs' = filter_out (fn (x : string, _) => x = a) xs; |
|
602 val weak' = xs' |> map_filter (fn (a, thm) => |
|
603 if is_full_cong thm then NONE else SOME a); |
|
604 in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); |
|
605 |
|
606 fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss; |
|
607 |
|
608 in |
|
609 |
|
610 val (op addeqcongs) = Library.foldl add_cong; |
|
611 val (op deleqcongs) = Library.foldl del_cong; |
|
612 |
|
613 fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs; |
|
614 fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs; |
|
615 |
|
616 end; |
|
617 |
|
618 |
|
619 (* simprocs *) |
|
620 |
|
621 datatype simproc = |
|
622 Simproc of |
|
623 {name: string, |
|
624 lhss: cterm list, |
|
625 proc: morphism -> simpset -> cterm -> thm option, |
|
626 id: stamp * thm list}; |
|
627 |
|
628 fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2); |
|
629 |
|
630 fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) = |
|
631 Simproc |
|
632 {name = name, |
|
633 lhss = map (Morphism.cterm phi) lhss, |
|
634 proc = Morphism.transform phi proc, |
|
635 id = (s, Morphism.fact phi ths)}; |
|
636 |
|
637 fun make_simproc {name, lhss, proc, identifier} = |
|
638 Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)}; |
|
639 |
|
640 fun mk_simproc name lhss proc = |
|
641 make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct => |
|
642 proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []}; |
|
643 |
|
644 (* FIXME avoid global thy and Logic.varify_global *) |
|
645 fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global); |
|
646 fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy); |
|
647 |
|
648 |
|
649 local |
|
650 |
|
651 fun add_proc (proc as Proc {name, lhs, ...}) ss = |
|
652 (trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs; |
|
653 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
654 (congs, Net.insert_term eq_proc (term_of lhs, proc) procs, |
|
655 mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss |
|
656 handle Net.INSERT => |
|
657 (if_visible ss warning ("Ignoring duplicate simplification procedure " ^ quote name); ss)); |
|
658 |
|
659 fun del_proc (proc as Proc {name, lhs, ...}) ss = |
|
660 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
661 (congs, Net.delete_term eq_proc (term_of lhs, proc) procs, |
|
662 mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss |
|
663 handle Net.DELETE => |
|
664 (if_visible ss warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss); |
|
665 |
|
666 fun prep_procs (Simproc {name, lhss, proc, id}) = |
|
667 lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id}); |
|
668 |
|
669 in |
|
670 |
|
671 fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss; |
|
672 fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss; |
|
673 |
|
674 end; |
|
675 |
|
676 |
|
677 (* mk_rews *) |
|
678 |
|
679 local |
|
680 |
|
681 fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient}, |
|
682 termless, subgoal_tac, loop_tacs, solvers) => |
|
683 let |
|
684 val (mk', mk_cong', mk_sym', mk_eq_True', reorient') = |
|
685 f (mk, mk_cong, mk_sym, mk_eq_True, reorient); |
|
686 val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True', |
|
687 reorient = reorient'}; |
|
688 in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end); |
|
689 |
|
690 in |
|
691 |
|
692 fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss; |
|
693 |
|
694 fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => |
|
695 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); |
|
696 |
|
697 fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) => |
|
698 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); |
|
699 |
|
700 fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) => |
|
701 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); |
|
702 |
|
703 fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) => |
|
704 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); |
|
705 |
|
706 fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) => |
|
707 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); |
|
708 |
|
709 end; |
|
710 |
|
711 |
|
712 (* termless *) |
|
713 |
|
714 fun ss settermless termless = ss |> |
|
715 map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) => |
|
716 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); |
|
717 |
|
718 |
|
719 (* tactics *) |
|
720 |
|
721 fun ss setsubgoaler subgoal_tac = ss |> |
|
722 map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) => |
|
723 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); |
|
724 |
|
725 fun ss setloop' tac = ss |> |
|
726 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) => |
|
727 (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers)); |
|
728 |
|
729 fun ss setloop tac = ss setloop' (K tac); |
|
730 |
|
731 fun ss addloop' (name, tac) = ss |> |
|
732 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
733 (congs, procs, mk_rews, termless, subgoal_tac, |
|
734 (if AList.defined (op =) loop_tacs name |
|
735 then if_visible ss warning ("Overwriting looper " ^ quote name) |
|
736 else (); AList.update (op =) (name, tac) loop_tacs), solvers)); |
|
737 |
|
738 fun ss addloop (name, tac) = ss addloop' (name, K tac); |
|
739 |
|
740 fun ss delloop name = ss |> |
|
741 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
742 (congs, procs, mk_rews, termless, subgoal_tac, |
|
743 (if AList.defined (op =) loop_tacs name then () |
|
744 else if_visible ss warning ("No such looper in simpset: " ^ quote name); |
|
745 AList.delete (op =) name loop_tacs), solvers)); |
|
746 |
|
747 fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
|
748 subgoal_tac, loop_tacs, (unsafe_solvers, _)) => |
|
749 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]))); |
|
750 |
|
751 fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
|
752 subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, |
|
753 subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers))); |
|
754 |
|
755 fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
|
756 subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless, |
|
757 subgoal_tac, loop_tacs, ([solver], solvers))); |
|
758 |
|
759 fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
|
760 subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, |
|
761 subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers))); |
|
762 |
|
763 fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless, |
|
764 subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless, |
|
765 subgoal_tac, loop_tacs, (solvers, solvers))); |
|
766 |
|
767 |
|
768 (* empty *) |
|
769 |
|
770 fun init_ss mk_rews termless subgoal_tac solvers = |
|
771 make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE), |
|
772 (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers)); |
|
773 |
|
774 fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) = |
|
775 init_ss mk_rews termless subgoal_tac solvers |
|
776 |> inherit_context ss; |
|
777 |
|
778 val empty_ss = |
|
779 init_ss |
|
780 {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], |
|
781 mk_cong = K I, |
|
782 mk_sym = K (SOME o Drule.symmetric_fun), |
|
783 mk_eq_True = K (K NONE), |
|
784 reorient = default_reorient} |
|
785 Term_Ord.termless (K (K no_tac)) ([], []); |
|
786 |
|
787 |
|
788 (* merge *) (*NOTE: ignores some fields of 2nd simpset*) |
|
789 |
|
790 fun merge_ss (ss1, ss2) = |
|
791 if pointer_eq (ss1, ss2) then ss1 |
|
792 else |
|
793 let |
|
794 val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _}, |
|
795 {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, |
|
796 loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; |
|
797 val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _}, |
|
798 {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, |
|
799 loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; |
|
800 |
|
801 val rules' = Net.merge eq_rrule (rules1, rules2); |
|
802 val prems' = Thm.merge_thms (prems1, prems2); |
|
803 val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; |
|
804 val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; |
|
805 val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2); |
|
806 val weak' = merge (op =) (weak1, weak2); |
|
807 val procs' = Net.merge eq_proc (procs1, procs2); |
|
808 val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2); |
|
809 val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2); |
|
810 val solvers' = merge eq_solver (solvers1, solvers2); |
|
811 in |
|
812 make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs', |
|
813 mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'))) |
|
814 end; |
|
815 |
|
816 |
|
817 (* dest_ss *) |
|
818 |
|
819 fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) = |
|
820 {simps = Net.entries rules |
|
821 |> map (fn {name, thm, ...} => (name, thm)), |
|
822 procs = Net.entries procs |
|
823 |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id)) |
|
824 |> partition_eq (eq_snd eq_procid) |
|
825 |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)), |
|
826 congs = #1 congs, |
|
827 weak_congs = #2 congs, |
|
828 loopers = map fst loop_tacs, |
|
829 unsafe_solvers = map solver_name (#1 solvers), |
|
830 safe_solvers = map solver_name (#2 solvers)}; |
|
831 |
|
832 |
|
833 |
|
834 (** rewriting **) |
|
835 |
|
836 (* |
|
837 Uses conversions, see: |
|
838 L C Paulson, A higher-order implementation of rewriting, |
|
839 Science of Computer Programming 3 (1983), pages 119-149. |
|
840 *) |
|
841 |
|
842 fun check_conv msg ss thm thm' = |
|
843 let |
|
844 val thm'' = Thm.transitive thm thm' handle THM _ => |
|
845 Thm.transitive thm (Thm.transitive |
|
846 (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm') |
|
847 in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end |
|
848 handle THM _ => |
|
849 let |
|
850 val _ $ _ $ prop0 = Thm.prop_of thm; |
|
851 in |
|
852 trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm'; |
|
853 trace_term false (fn () => "Should have proved:") ss prop0; |
|
854 NONE |
|
855 end; |
|
856 |
|
857 |
|
858 (* mk_procrule *) |
|
859 |
|
860 fun mk_procrule ss thm = |
|
861 let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in |
|
862 if rewrite_rule_extra_vars prems lhs rhs |
|
863 then (cond_warn_thm "Extra vars on rhs:" ss thm; []) |
|
864 else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}] |
|
865 end; |
|
866 |
|
867 |
|
868 (* rewritec: conversion to apply the meta simpset to a term *) |
|
869 |
|
870 (*Since the rewriting strategy is bottom-up, we avoid re-normalizing already |
|
871 normalized terms by carrying around the rhs of the rewrite rule just |
|
872 applied. This is called the `skeleton'. It is decomposed in parallel |
|
873 with the term. Once a Var is encountered, the corresponding term is |
|
874 already in normal form. |
|
875 skel0 is a dummy skeleton that is to enforce complete normalization.*) |
|
876 |
|
877 val skel0 = Bound 0; |
|
878 |
|
879 (*Use rhs as skeleton only if the lhs does not contain unnormalized bits. |
|
880 The latter may happen iff there are weak congruence rules for constants |
|
881 in the lhs.*) |
|
882 |
|
883 fun uncond_skel ((_, weak), (lhs, rhs)) = |
|
884 if null weak then rhs (*optimization*) |
|
885 else if exists_Const (member (op =) weak o #1) lhs then skel0 |
|
886 else rhs; |
|
887 |
|
888 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs. |
|
889 Otherwise those vars may become instantiated with unnormalized terms |
|
890 while the premises are solved.*) |
|
891 |
|
892 fun cond_skel (args as (_, (lhs, rhs))) = |
|
893 if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args |
|
894 else skel0; |
|
895 |
|
896 (* |
|
897 Rewriting -- we try in order: |
|
898 (1) beta reduction |
|
899 (2) unconditional rewrite rules |
|
900 (3) conditional rewrite rules |
|
901 (4) simplification procedures |
|
902 |
|
903 IMPORTANT: rewrite rules must not introduce new Vars or TVars! |
|
904 *) |
|
905 |
|
906 fun rewritec (prover, thyt, maxt) ss t = |
|
907 let |
|
908 val ctxt = the_context ss; |
|
909 val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss; |
|
910 val eta_thm = Thm.eta_conversion t; |
|
911 val eta_t' = Thm.rhs_of eta_thm; |
|
912 val eta_t = term_of eta_t'; |
|
913 fun rew {thm, name, lhs, elhs, extra, fo, perm} = |
|
914 let |
|
915 val prop = Thm.prop_of thm; |
|
916 val (rthm, elhs') = |
|
917 if maxt = ~1 orelse not extra then (thm, elhs) |
|
918 else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs); |
|
919 val insts = |
|
920 if fo then Thm.first_order_match (elhs', eta_t') |
|
921 else Thm.match (elhs', eta_t'); |
|
922 val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); |
|
923 val prop' = Thm.prop_of thm'; |
|
924 val unconditional = (Logic.count_prems prop' = 0); |
|
925 val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop') |
|
926 in |
|
927 if perm andalso not (termless (rhs', lhs')) |
|
928 then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name); |
|
929 trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE) |
|
930 else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name); |
|
931 if unconditional |
|
932 then |
|
933 (trace_thm (fn () => "Rewriting:") ss thm'; |
|
934 let |
|
935 val lr = Logic.dest_equals prop; |
|
936 val SOME thm'' = check_conv false ss eta_thm thm'; |
|
937 in SOME (thm'', uncond_skel (congs, lr)) end) |
|
938 else |
|
939 (trace_thm (fn () => "Trying to rewrite:") ss thm'; |
|
940 if simp_depth ss > Config.get ctxt simp_depth_limit |
|
941 then |
|
942 let |
|
943 val s = "simp_depth_limit exceeded - giving up"; |
|
944 val _ = trace false (fn () => s) ss; |
|
945 val _ = if_visible ss warning s; |
|
946 in NONE end |
|
947 else |
|
948 case prover ss thm' of |
|
949 NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE) |
|
950 | SOME thm2 => |
|
951 (case check_conv true ss eta_thm thm2 of |
|
952 NONE => NONE | |
|
953 SOME thm2' => |
|
954 let val concl = Logic.strip_imp_concl prop |
|
955 val lr = Logic.dest_equals concl |
|
956 in SOME (thm2', cond_skel (congs, lr)) end))) |
|
957 end |
|
958 |
|
959 fun rews [] = NONE |
|
960 | rews (rrule :: rrules) = |
|
961 let val opt = rew rrule handle Pattern.MATCH => NONE |
|
962 in case opt of NONE => rews rrules | some => some end; |
|
963 |
|
964 fun sort_rrules rrs = |
|
965 let |
|
966 fun is_simple ({thm, ...}: rrule) = |
|
967 (case Thm.prop_of thm of |
|
968 Const ("==", _) $ _ $ _ => true |
|
969 | _ => false); |
|
970 fun sort [] (re1, re2) = re1 @ re2 |
|
971 | sort (rr :: rrs) (re1, re2) = |
|
972 if is_simple rr |
|
973 then sort rrs (rr :: re1, re2) |
|
974 else sort rrs (re1, rr :: re2); |
|
975 in sort rrs ([], []) end; |
|
976 |
|
977 fun proc_rews [] = NONE |
|
978 | proc_rews (Proc {name, proc, lhs, ...} :: ps) = |
|
979 if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then |
|
980 (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t; |
|
981 case proc ss eta_t' of |
|
982 NONE => (debug false (fn () => "FAILED") ss; proc_rews ps) |
|
983 | SOME raw_thm => |
|
984 (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:") |
|
985 ss raw_thm; |
|
986 (case rews (mk_procrule ss raw_thm) of |
|
987 NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^ |
|
988 " -- does not match") ss t; proc_rews ps) |
|
989 | some => some))) |
|
990 else proc_rews ps; |
|
991 in |
|
992 (case eta_t of |
|
993 Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0) |
|
994 | _ => |
|
995 (case rews (sort_rrules (Net.match_term rules eta_t)) of |
|
996 NONE => proc_rews (Net.match_term procs eta_t) |
|
997 | some => some)) |
|
998 end; |
|
999 |
|
1000 |
|
1001 (* conversion to apply a congruence rule to a term *) |
|
1002 |
|
1003 fun congc prover ss maxt cong t = |
|
1004 let val rthm = Thm.incr_indexes (maxt + 1) cong; |
|
1005 val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm))); |
|
1006 val insts = Thm.match (rlhs, t) |
|
1007 (* Thm.match can raise Pattern.MATCH; |
|
1008 is handled when congc is called *) |
|
1009 val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm); |
|
1010 val _ = trace_thm (fn () => "Applying congruence rule:") ss thm'; |
|
1011 fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE) |
|
1012 in |
|
1013 (case prover thm' of |
|
1014 NONE => err ("Congruence proof failed. Could not prove", thm') |
|
1015 | SOME thm2 => |
|
1016 (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of |
|
1017 NONE => err ("Congruence proof failed. Should not have proved", thm2) |
|
1018 | SOME thm2' => |
|
1019 if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2'))) |
|
1020 then NONE else SOME thm2')) |
|
1021 end; |
|
1022 |
|
1023 val (cA, (cB, cC)) = |
|
1024 apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong))); |
|
1025 |
|
1026 fun transitive1 NONE NONE = NONE |
|
1027 | transitive1 (SOME thm1) NONE = SOME thm1 |
|
1028 | transitive1 NONE (SOME thm2) = SOME thm2 |
|
1029 | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2) |
|
1030 |
|
1031 fun transitive2 thm = transitive1 (SOME thm); |
|
1032 fun transitive3 thm = transitive1 thm o SOME; |
|
1033 |
|
1034 fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) = |
|
1035 let |
|
1036 fun botc skel ss t = |
|
1037 if is_Var skel then NONE |
|
1038 else |
|
1039 (case subc skel ss t of |
|
1040 some as SOME thm1 => |
|
1041 (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of |
|
1042 SOME (thm2, skel2) => |
|
1043 transitive2 (Thm.transitive thm1 thm2) |
|
1044 (botc skel2 ss (Thm.rhs_of thm2)) |
|
1045 | NONE => some) |
|
1046 | NONE => |
|
1047 (case rewritec (prover, thy, maxidx) ss t of |
|
1048 SOME (thm2, skel2) => transitive2 thm2 |
|
1049 (botc skel2 ss (Thm.rhs_of thm2)) |
|
1050 | NONE => NONE)) |
|
1051 |
|
1052 and try_botc ss t = |
|
1053 (case botc skel0 ss t of |
|
1054 SOME trec1 => trec1 | NONE => (Thm.reflexive t)) |
|
1055 |
|
1056 and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 = |
|
1057 (case term_of t0 of |
|
1058 Abs (a, T, _) => |
|
1059 let |
|
1060 val b = Name.bound (#1 bounds); |
|
1061 val (v, t') = Thm.dest_abs (SOME b) t0; |
|
1062 val b' = #1 (Term.dest_Free (Thm.term_of v)); |
|
1063 val _ = |
|
1064 if b <> b' then |
|
1065 warning ("Simplifier: renamed bound variable " ^ |
|
1066 quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ())) |
|
1067 else (); |
|
1068 val ss' = add_bound ((b', T), a) ss; |
|
1069 val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0; |
|
1070 in case botc skel' ss' t' of |
|
1071 SOME thm => SOME (Thm.abstract_rule a v thm) |
|
1072 | NONE => NONE |
|
1073 end |
|
1074 | t $ _ => (case t of |
|
1075 Const ("==>", _) $ _ => impc t0 ss |
|
1076 | Abs _ => |
|
1077 let val thm = Thm.beta_conversion false t0 |
|
1078 in case subc skel0 ss (Thm.rhs_of thm) of |
|
1079 NONE => SOME thm |
|
1080 | SOME thm' => SOME (Thm.transitive thm thm') |
|
1081 end |
|
1082 | _ => |
|
1083 let fun appc () = |
|
1084 let |
|
1085 val (tskel, uskel) = case skel of |
|
1086 tskel $ uskel => (tskel, uskel) |
|
1087 | _ => (skel0, skel0); |
|
1088 val (ct, cu) = Thm.dest_comb t0 |
|
1089 in |
|
1090 (case botc tskel ss ct of |
|
1091 SOME thm1 => |
|
1092 (case botc uskel ss cu of |
|
1093 SOME thm2 => SOME (Thm.combination thm1 thm2) |
|
1094 | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu))) |
|
1095 | NONE => |
|
1096 (case botc uskel ss cu of |
|
1097 SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1) |
|
1098 | NONE => NONE)) |
|
1099 end |
|
1100 val (h, ts) = strip_comb t |
|
1101 in case cong_name h of |
|
1102 SOME a => |
|
1103 (case AList.lookup (op =) (fst congs) a of |
|
1104 NONE => appc () |
|
1105 | SOME cong => |
|
1106 (*post processing: some partial applications h t1 ... tj, j <= length ts, |
|
1107 may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*) |
|
1108 (let |
|
1109 val thm = congc (prover ss) ss maxidx cong t0; |
|
1110 val t = the_default t0 (Option.map Thm.rhs_of thm); |
|
1111 val (cl, cr) = Thm.dest_comb t |
|
1112 val dVar = Var(("", 0), dummyT) |
|
1113 val skel = |
|
1114 list_comb (h, replicate (length ts) dVar) |
|
1115 in case botc skel ss cl of |
|
1116 NONE => thm |
|
1117 | SOME thm' => transitive3 thm |
|
1118 (Thm.combination thm' (Thm.reflexive cr)) |
|
1119 end handle Pattern.MATCH => appc ())) |
|
1120 | _ => appc () |
|
1121 end) |
|
1122 | _ => NONE) |
|
1123 |
|
1124 and impc ct ss = |
|
1125 if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss |
|
1126 |
|
1127 and rules_of_prem ss prem = |
|
1128 if maxidx_of_term (term_of prem) <> ~1 |
|
1129 then (trace_cterm true |
|
1130 (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:") |
|
1131 ss prem; ([], NONE)) |
|
1132 else |
|
1133 let val asm = Thm.assume prem |
|
1134 in (extract_safe_rrules (ss, asm), SOME asm) end |
|
1135 |
|
1136 and add_rrules (rrss, asms) ss = |
|
1137 (fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms) |
|
1138 |
|
1139 and disch r prem eq = |
|
1140 let |
|
1141 val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq); |
|
1142 val eq' = Thm.implies_elim (Thm.instantiate |
|
1143 ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) |
|
1144 (Thm.implies_intr prem eq) |
|
1145 in if not r then eq' else |
|
1146 let |
|
1147 val (prem', concl) = Thm.dest_implies lhs; |
|
1148 val (prem'', _) = Thm.dest_implies rhs |
|
1149 in Thm.transitive (Thm.transitive |
|
1150 (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) |
|
1151 Drule.swap_prems_eq) eq') |
|
1152 (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) |
|
1153 Drule.swap_prems_eq) |
|
1154 end |
|
1155 end |
|
1156 |
|
1157 and rebuild [] _ _ _ _ eq = eq |
|
1158 | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq = |
|
1159 let |
|
1160 val ss' = add_rrules (rev rrss, rev asms) ss; |
|
1161 val concl' = |
|
1162 Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq)); |
|
1163 val dprem = Option.map (disch false prem) |
|
1164 in |
|
1165 (case rewritec (prover, thy, maxidx) ss' concl' of |
|
1166 NONE => rebuild prems concl' rrss asms ss (dprem eq) |
|
1167 | SOME (eq', _) => transitive2 (fold (disch false) |
|
1168 prems (the (transitive3 (dprem eq) eq'))) |
|
1169 (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss)) |
|
1170 end |
|
1171 |
|
1172 and mut_impc0 prems concl rrss asms ss = |
|
1173 let |
|
1174 val prems' = strip_imp_prems concl; |
|
1175 val (rrss', asms') = split_list (map (rules_of_prem ss) prems') |
|
1176 in |
|
1177 mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss') |
|
1178 (asms @ asms') [] [] [] [] ss ~1 ~1 |
|
1179 end |
|
1180 |
|
1181 and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k = |
|
1182 transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1 |
|
1183 (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE) |
|
1184 (if changed > 0 then |
|
1185 mut_impc (rev prems') concl (rev rrss') (rev asms') |
|
1186 [] [] [] [] ss ~1 changed |
|
1187 else rebuild prems' concl rrss' asms' ss |
|
1188 (botc skel0 (add_rrules (rev rrss', rev asms') ss) concl)) |
|
1189 |
|
1190 | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms) |
|
1191 prems' rrss' asms' eqns ss changed k = |
|
1192 case (if k = 0 then NONE else botc skel0 (add_rrules |
|
1193 (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of |
|
1194 NONE => mut_impc prems concl rrss asms (prem :: prems') |
|
1195 (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed |
|
1196 (if k = 0 then 0 else k - 1) |
|
1197 | SOME eqn => |
|
1198 let |
|
1199 val prem' = Thm.rhs_of eqn; |
|
1200 val tprems = map term_of prems; |
|
1201 val i = 1 + fold Integer.max (map (fn p => |
|
1202 find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1; |
|
1203 val (rrs', asm') = rules_of_prem ss prem' |
|
1204 in mut_impc prems concl rrss asms (prem' :: prems') |
|
1205 (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true) |
|
1206 (take i prems) |
|
1207 (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies |
|
1208 (drop i prems, concl))))) :: eqns) |
|
1209 ss (length prems') ~1 |
|
1210 end |
|
1211 |
|
1212 (*legacy code - only for backwards compatibility*) |
|
1213 and nonmut_impc ct ss = |
|
1214 let |
|
1215 val (prem, conc) = Thm.dest_implies ct; |
|
1216 val thm1 = if simprem then botc skel0 ss prem else NONE; |
|
1217 val prem1 = the_default prem (Option.map Thm.rhs_of thm1); |
|
1218 val ss1 = |
|
1219 if not useprem then ss |
|
1220 else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss |
|
1221 in |
|
1222 (case botc skel0 ss1 conc of |
|
1223 NONE => |
|
1224 (case thm1 of |
|
1225 NONE => NONE |
|
1226 | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc))) |
|
1227 | SOME thm2 => |
|
1228 let val thm2' = disch false prem1 thm2 in |
|
1229 (case thm1 of |
|
1230 NONE => SOME thm2' |
|
1231 | SOME thm1' => |
|
1232 SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2')) |
|
1233 end) |
|
1234 end |
|
1235 |
|
1236 in try_botc end; |
|
1237 |
|
1238 |
|
1239 (* Meta-rewriting: rewrites t to u and returns the theorem t==u *) |
|
1240 |
|
1241 (* |
|
1242 Parameters: |
|
1243 mode = (simplify A, |
|
1244 use A in simplifying B, |
|
1245 use prems of B (if B is again a meta-impl.) to simplify A) |
|
1246 when simplifying A ==> B |
|
1247 prover: how to solve premises in conditional rewrites and congruences |
|
1248 *) |
|
1249 |
|
1250 val debug_bounds = Unsynchronized.ref false; |
|
1251 |
|
1252 fun check_bounds ss ct = |
|
1253 if ! debug_bounds then |
|
1254 let |
|
1255 val Simpset ({bounds = (_, bounds), ...}, _) = ss; |
|
1256 val bs = fold_aterms (fn Free (x, _) => |
|
1257 if Name.is_bound x andalso not (AList.defined eq_bound bounds x) |
|
1258 then insert (op =) x else I |
|
1259 | _ => I) (term_of ct) []; |
|
1260 in |
|
1261 if null bs then () |
|
1262 else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) |
|
1263 (Thm.theory_of_cterm ct) (Thm.term_of ct) |
|
1264 end |
|
1265 else (); |
|
1266 |
|
1267 fun rewrite_cterm mode prover raw_ss raw_ct = |
|
1268 let |
|
1269 val thy = Thm.theory_of_cterm raw_ct; |
|
1270 val ct = Thm.adjust_maxidx_cterm ~1 raw_ct; |
|
1271 val {maxidx, ...} = Thm.rep_cterm ct; |
|
1272 val ss = inc_simp_depth (activate_context thy raw_ss); |
|
1273 val depth = simp_depth ss; |
|
1274 val _ = |
|
1275 if depth mod 20 = 0 then |
|
1276 if_visible ss warning ("Simplification depth " ^ string_of_int depth) |
|
1277 else (); |
|
1278 val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct; |
|
1279 val _ = check_bounds ss ct; |
|
1280 in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end; |
|
1281 |
|
1282 val simple_prover = |
|
1283 SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss))); |
|
1284 |
|
1285 fun rewrite _ [] ct = Thm.reflexive ct |
|
1286 | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover |
|
1287 (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct; |
|
1288 |
|
1289 fun simplify full thms = Conv.fconv_rule (rewrite full thms); |
|
1290 val rewrite_rule = simplify true; |
|
1291 |
|
1292 (*simple term rewriting -- no proof*) |
|
1293 fun rewrite_term thy rules procs = |
|
1294 Pattern.rewrite_term thy (map decomp_simp' rules) procs; |
|
1295 |
|
1296 fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss); |
|
1297 |
|
1298 (*Rewrite the subgoals of a proof state (represented by a theorem)*) |
|
1299 fun rewrite_goals_rule thms th = |
|
1300 Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover |
|
1301 (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th; |
|
1302 |
|
1303 (*Rewrite the subgoal of a proof state (represented by a theorem)*) |
|
1304 fun rewrite_goal_rule mode prover ss i thm = |
|
1305 if 0 < i andalso i <= Thm.nprems_of thm |
|
1306 then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm |
|
1307 else raise THM ("rewrite_goal_rule", i, [thm]); |
|
1308 |
|
1309 |
|
1310 (** meta-rewriting tactics **) |
|
1311 |
|
1312 (*Rewrite all subgoals*) |
|
1313 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); |
|
1314 fun rewtac def = rewrite_goals_tac [def]; |
|
1315 |
|
1316 (*Rewrite one subgoal*) |
|
1317 fun asm_rewrite_goal_tac mode prover_tac ss i thm = |
|
1318 if 0 < i andalso i <= Thm.nprems_of thm then |
|
1319 Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm) |
|
1320 else Seq.empty; |
|
1321 |
|
1322 fun rewrite_goal_tac rews = |
|
1323 let val ss = empty_ss addsimps rews in |
|
1324 fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac) |
|
1325 (global_context (Thm.theory_of_thm st) ss) i st |
|
1326 end; |
|
1327 |
|
1328 (*Prunes all redundant parameters from the proof state by rewriting. |
|
1329 DOES NOT rewrite main goal, where quantification over an unused bound |
|
1330 variable is sometimes done to avoid the need for cut_facts_tac.*) |
|
1331 val prune_params_tac = rewrite_goals_tac [triv_forall_equality]; |
|
1332 |
|
1333 |
|
1334 (* for folding definitions, handling critical pairs *) |
|
1335 |
|
1336 (*The depth of nesting in a term*) |
|
1337 fun term_depth (Abs (_, _, t)) = 1 + term_depth t |
|
1338 | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t) |
|
1339 | term_depth _ = 0; |
|
1340 |
|
1341 val lhs_of_thm = #1 o Logic.dest_equals o prop_of; |
|
1342 |
|
1343 (*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0)) |
|
1344 Returns longest lhs first to avoid folding its subexpressions.*) |
|
1345 fun sort_lhs_depths defs = |
|
1346 let val keylist = AList.make (term_depth o lhs_of_thm) defs |
|
1347 val keys = sort_distinct (rev_order o int_ord) (map #2 keylist) |
|
1348 in map (AList.find (op =) keylist) keys end; |
|
1349 |
|
1350 val rev_defs = sort_lhs_depths o map Thm.symmetric; |
|
1351 |
|
1352 fun fold_rule defs = fold rewrite_rule (rev_defs defs); |
|
1353 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs)); |
|
1354 |
|
1355 |
|
1356 (* HHF normal form: !! before ==>, outermost !! generalized *) |
|
1357 |
|
1358 local |
|
1359 |
|
1360 fun gen_norm_hhf ss th = |
|
1361 (if Drule.is_norm_hhf (Thm.prop_of th) then th |
|
1362 else Conv.fconv_rule |
|
1363 (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th) |
|
1364 |> Thm.adjust_maxidx_thm ~1 |
|
1365 |> Drule.gen_all; |
|
1366 |
|
1367 val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs; |
|
1368 |
|
1369 in |
|
1370 |
|
1371 val norm_hhf = gen_norm_hhf hhf_ss; |
|
1372 val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]); |
|
1373 |
|
1374 end; |
|
1375 |
|
1376 end; |
|
1377 |
|
1378 structure Basic_Meta_Simplifier: BASIC_META_SIMPLIFIER = MetaSimplifier; |
|
1379 open Basic_Meta_Simplifier; |
|