|
1 (* Title: HOL/Library/Old_SMT/old_smt_normalize.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Normalization steps on theorems required by SMT solvers. |
|
5 *) |
|
6 |
|
7 signature OLD_SMT_NORMALIZE = |
|
8 sig |
|
9 val drop_fact_warning: Proof.context -> thm -> unit |
|
10 val atomize_conv: Proof.context -> conv |
|
11 type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list |
|
12 val add_extra_norm: Old_SMT_Utils.class * extra_norm -> Context.generic -> |
|
13 Context.generic |
|
14 val normalize: (int * (int option * thm)) list -> Proof.context -> |
|
15 (int * thm) list * Proof.context |
|
16 val setup: theory -> theory |
|
17 end |
|
18 |
|
19 structure Old_SMT_Normalize: OLD_SMT_NORMALIZE = |
|
20 struct |
|
21 |
|
22 fun drop_fact_warning ctxt = |
|
23 Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o |
|
24 Display.string_of_thm ctxt) |
|
25 |
|
26 |
|
27 (* general theorem normalizations *) |
|
28 |
|
29 (** instantiate elimination rules **) |
|
30 |
|
31 local |
|
32 val (cpfalse, cfalse) = |
|
33 `Old_SMT_Utils.mk_cprop (Thm.cterm_of @{theory} @{const False}) |
|
34 |
|
35 fun inst f ct thm = |
|
36 let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) |
|
37 in Thm.instantiate ([], [(cv, ct)]) thm end |
|
38 in |
|
39 |
|
40 fun instantiate_elim thm = |
|
41 (case Thm.concl_of thm of |
|
42 @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm |
|
43 | Var _ => inst I cpfalse thm |
|
44 | _ => thm) |
|
45 |
|
46 end |
|
47 |
|
48 |
|
49 (** normalize definitions **) |
|
50 |
|
51 fun norm_def thm = |
|
52 (case Thm.prop_of thm of |
|
53 @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => |
|
54 norm_def (thm RS @{thm fun_cong}) |
|
55 | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => |
|
56 norm_def (thm RS @{thm meta_eq_to_obj_eq}) |
|
57 | _ => thm) |
|
58 |
|
59 |
|
60 (** atomization **) |
|
61 |
|
62 fun atomize_conv ctxt ct = |
|
63 (case Thm.term_of ct of |
|
64 @{const Pure.imp} $ _ $ _ => |
|
65 Conv.binop_conv (atomize_conv ctxt) then_conv |
|
66 Conv.rewr_conv @{thm atomize_imp} |
|
67 | Const (@{const_name Pure.eq}, _) $ _ $ _ => |
|
68 Conv.binop_conv (atomize_conv ctxt) then_conv |
|
69 Conv.rewr_conv @{thm atomize_eq} |
|
70 | Const (@{const_name Pure.all}, _) $ Abs _ => |
|
71 Conv.binder_conv (atomize_conv o snd) ctxt then_conv |
|
72 Conv.rewr_conv @{thm atomize_all} |
|
73 | _ => Conv.all_conv) ct |
|
74 |
|
75 val setup_atomize = |
|
76 fold Old_SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, |
|
77 @{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}] |
|
78 |
|
79 |
|
80 (** unfold special quantifiers **) |
|
81 |
|
82 local |
|
83 val ex1_def = mk_meta_eq @{lemma |
|
84 "Ex1 = (%P. EX x. P x & (ALL y. P y --> y = x))" |
|
85 by (rule ext) (simp only: Ex1_def)} |
|
86 |
|
87 val ball_def = mk_meta_eq @{lemma "Ball = (%A P. ALL x. x : A --> P x)" |
|
88 by (rule ext)+ (rule Ball_def)} |
|
89 |
|
90 val bex_def = mk_meta_eq @{lemma "Bex = (%A P. EX x. x : A & P x)" |
|
91 by (rule ext)+ (rule Bex_def)} |
|
92 |
|
93 val special_quants = [(@{const_name Ex1}, ex1_def), |
|
94 (@{const_name Ball}, ball_def), (@{const_name Bex}, bex_def)] |
|
95 |
|
96 fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n |
|
97 | special_quant _ = NONE |
|
98 |
|
99 fun special_quant_conv _ ct = |
|
100 (case special_quant (Thm.term_of ct) of |
|
101 SOME thm => Conv.rewr_conv thm |
|
102 | NONE => Conv.all_conv) ct |
|
103 in |
|
104 |
|
105 fun unfold_special_quants_conv ctxt = |
|
106 Old_SMT_Utils.if_exists_conv (is_some o special_quant) |
|
107 (Conv.top_conv special_quant_conv ctxt) |
|
108 |
|
109 val setup_unfolded_quants = |
|
110 fold (Old_SMT_Builtin.add_builtin_fun_ext'' o fst) special_quants |
|
111 |
|
112 end |
|
113 |
|
114 |
|
115 (** trigger inference **) |
|
116 |
|
117 local |
|
118 (*** check trigger syntax ***) |
|
119 |
|
120 fun dest_trigger (Const (@{const_name pat}, _) $ _) = SOME true |
|
121 | dest_trigger (Const (@{const_name nopat}, _) $ _) = SOME false |
|
122 | dest_trigger _ = NONE |
|
123 |
|
124 fun eq_list [] = false |
|
125 | eq_list (b :: bs) = forall (equal b) bs |
|
126 |
|
127 fun proper_trigger t = |
|
128 t |
|
129 |> these o try HOLogic.dest_list |
|
130 |> map (map_filter dest_trigger o these o try HOLogic.dest_list) |
|
131 |> (fn [] => false | bss => forall eq_list bss) |
|
132 |
|
133 fun proper_quant inside f t = |
|
134 (case t of |
|
135 Const (@{const_name All}, _) $ Abs (_, _, u) => proper_quant true f u |
|
136 | Const (@{const_name Ex}, _) $ Abs (_, _, u) => proper_quant true f u |
|
137 | @{const trigger} $ p $ u => |
|
138 (if inside then f p else false) andalso proper_quant false f u |
|
139 | Abs (_, _, u) => proper_quant false f u |
|
140 | u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2 |
|
141 | _ => true) |
|
142 |
|
143 fun check_trigger_error ctxt t = |
|
144 error ("SMT triggers must only occur under quantifier and multipatterns " ^ |
|
145 "must have the same kind: " ^ Syntax.string_of_term ctxt t) |
|
146 |
|
147 fun check_trigger_conv ctxt ct = |
|
148 if proper_quant false proper_trigger (Old_SMT_Utils.term_of ct) then |
|
149 Conv.all_conv ct |
|
150 else check_trigger_error ctxt (Thm.term_of ct) |
|
151 |
|
152 |
|
153 (*** infer simple triggers ***) |
|
154 |
|
155 fun dest_cond_eq ct = |
|
156 (case Thm.term_of ct of |
|
157 Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct |
|
158 | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct) |
|
159 | _ => raise CTERM ("no equation", [ct])) |
|
160 |
|
161 fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n) |
|
162 | get_constrs _ _ = [] |
|
163 |
|
164 fun is_constr thy (n, T) = |
|
165 let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U) |
|
166 in can (the o find_first match o get_constrs thy o Term.body_type) T end |
|
167 |
|
168 fun is_constr_pat thy t = |
|
169 (case Term.strip_comb t of |
|
170 (Free _, []) => true |
|
171 | (Const c, ts) => is_constr thy c andalso forall (is_constr_pat thy) ts |
|
172 | _ => false) |
|
173 |
|
174 fun is_simp_lhs ctxt t = |
|
175 (case Term.strip_comb t of |
|
176 (Const c, ts as _ :: _) => |
|
177 not (Old_SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso |
|
178 forall (is_constr_pat (Proof_Context.theory_of ctxt)) ts |
|
179 | _ => false) |
|
180 |
|
181 fun has_all_vars vs t = |
|
182 subset (op aconv) (vs, map Free (Term.add_frees t [])) |
|
183 |
|
184 fun minimal_pats vs ct = |
|
185 if has_all_vars vs (Thm.term_of ct) then |
|
186 (case Thm.term_of ct of |
|
187 _ $ _ => |
|
188 (case pairself (minimal_pats vs) (Thm.dest_comb ct) of |
|
189 ([], []) => [[ct]] |
|
190 | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss') |
|
191 | _ => []) |
|
192 else [] |
|
193 |
|
194 fun proper_mpat _ _ _ [] = false |
|
195 | proper_mpat thy gen u cts = |
|
196 let |
|
197 val tps = (op ~~) (`gen (map Thm.term_of cts)) |
|
198 fun some_match u = tps |> exists (fn (t', t) => |
|
199 Pattern.matches thy (t', u) andalso not (t aconv u)) |
|
200 in not (Term.exists_subterm some_match u) end |
|
201 |
|
202 val pat = |
|
203 Old_SMT_Utils.mk_const_pat @{theory} @{const_name pat} Old_SMT_Utils.destT1 |
|
204 fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct |
|
205 |
|
206 fun mk_clist T = pairself (Thm.cterm_of @{theory}) |
|
207 (HOLogic.cons_const T, HOLogic.nil_const T) |
|
208 fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil |
|
209 val mk_pat_list = mk_list (mk_clist @{typ pattern}) |
|
210 val mk_mpat_list = mk_list (mk_clist @{typ "pattern list"}) |
|
211 fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss |
|
212 |
|
213 val trigger_eq = |
|
214 mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)} |
|
215 |
|
216 fun insert_trigger_conv [] ct = Conv.all_conv ct |
|
217 | insert_trigger_conv ctss ct = |
|
218 let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct |
|
219 in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end |
|
220 |
|
221 fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = |
|
222 let |
|
223 val (lhs, rhs) = dest_cond_eq ct |
|
224 |
|
225 val vs = map Thm.term_of cvs |
|
226 val thy = Proof_Context.theory_of ctxt |
|
227 |
|
228 fun get_mpats ct = |
|
229 if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct |
|
230 else [] |
|
231 val gen = Variable.export_terms ctxt outer_ctxt |
|
232 val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs)) |
|
233 |
|
234 in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end |
|
235 |
|
236 fun has_trigger (@{const trigger} $ _ $ _) = true |
|
237 | has_trigger _ = false |
|
238 |
|
239 fun try_trigger_conv cv ct = |
|
240 if Old_SMT_Utils.under_quant has_trigger (Old_SMT_Utils.term_of ct) then |
|
241 Conv.all_conv ct |
|
242 else Conv.try_conv cv ct |
|
243 |
|
244 fun infer_trigger_conv ctxt = |
|
245 if Config.get ctxt Old_SMT_Config.infer_triggers then |
|
246 try_trigger_conv |
|
247 (Old_SMT_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt) |
|
248 else Conv.all_conv |
|
249 in |
|
250 |
|
251 fun trigger_conv ctxt = |
|
252 Old_SMT_Utils.prop_conv |
|
253 (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt) |
|
254 |
|
255 val setup_trigger = |
|
256 fold Old_SMT_Builtin.add_builtin_fun_ext'' |
|
257 [@{const_name pat}, @{const_name nopat}, @{const_name trigger}] |
|
258 |
|
259 end |
|
260 |
|
261 |
|
262 (** adding quantifier weights **) |
|
263 |
|
264 local |
|
265 (*** check weight syntax ***) |
|
266 |
|
267 val has_no_weight = |
|
268 not o Term.exists_subterm (fn @{const weight} => true | _ => false) |
|
269 |
|
270 fun is_weight (@{const weight} $ w $ t) = |
|
271 (case try HOLogic.dest_number w of |
|
272 SOME (_, i) => i >= 0 andalso has_no_weight t |
|
273 | _ => false) |
|
274 | is_weight t = has_no_weight t |
|
275 |
|
276 fun proper_trigger (@{const trigger} $ _ $ t) = is_weight t |
|
277 | proper_trigger t = is_weight t |
|
278 |
|
279 fun check_weight_error ctxt t = |
|
280 error ("SMT weight must be a non-negative number and must only occur " ^ |
|
281 "under the top-most quantifier and an optional trigger: " ^ |
|
282 Syntax.string_of_term ctxt t) |
|
283 |
|
284 fun check_weight_conv ctxt ct = |
|
285 if Old_SMT_Utils.under_quant proper_trigger (Old_SMT_Utils.term_of ct) then |
|
286 Conv.all_conv ct |
|
287 else check_weight_error ctxt (Thm.term_of ct) |
|
288 |
|
289 |
|
290 (*** insertion of weights ***) |
|
291 |
|
292 fun under_trigger_conv cv ct = |
|
293 (case Thm.term_of ct of |
|
294 @{const trigger} $ _ $ _ => Conv.arg_conv cv |
|
295 | _ => cv) ct |
|
296 |
|
297 val weight_eq = |
|
298 mk_meta_eq @{lemma "p = weight i p" by (simp add: weight_def)} |
|
299 fun mk_weight_eq w = |
|
300 let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq) |
|
301 in |
|
302 Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq |
|
303 end |
|
304 |
|
305 fun add_weight_conv NONE _ = Conv.all_conv |
|
306 | add_weight_conv (SOME weight) ctxt = |
|
307 let val cv = Conv.rewr_conv (mk_weight_eq weight) |
|
308 in Old_SMT_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end |
|
309 in |
|
310 |
|
311 fun weight_conv weight ctxt = |
|
312 Old_SMT_Utils.prop_conv |
|
313 (check_weight_conv ctxt then_conv add_weight_conv weight ctxt) |
|
314 |
|
315 val setup_weight = Old_SMT_Builtin.add_builtin_fun_ext'' @{const_name weight} |
|
316 |
|
317 end |
|
318 |
|
319 |
|
320 (** combined general normalizations **) |
|
321 |
|
322 fun gen_normalize1_conv ctxt weight = |
|
323 atomize_conv ctxt then_conv |
|
324 unfold_special_quants_conv ctxt then_conv |
|
325 Thm.beta_conversion true then_conv |
|
326 trigger_conv ctxt then_conv |
|
327 weight_conv weight ctxt |
|
328 |
|
329 fun gen_normalize1 ctxt weight thm = |
|
330 thm |
|
331 |> instantiate_elim |
|
332 |> norm_def |
|
333 |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) |
|
334 |> Drule.forall_intr_vars |
|
335 |> Conv.fconv_rule (gen_normalize1_conv ctxt weight) |
|
336 |
|
337 fun gen_norm1_safe ctxt (i, (weight, thm)) = |
|
338 (case try (gen_normalize1 ctxt weight) thm of |
|
339 SOME thm' => SOME (i, thm') |
|
340 | NONE => (drop_fact_warning ctxt thm; NONE)) |
|
341 |
|
342 fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms |
|
343 |
|
344 |
|
345 |
|
346 (* unfolding of definitions and theory-specific rewritings *) |
|
347 |
|
348 fun expand_head_conv cv ct = |
|
349 (case Thm.term_of ct of |
|
350 _ $ _ => |
|
351 Conv.fun_conv (expand_head_conv cv) then_conv |
|
352 Conv.try_conv (Thm.beta_conversion false) |
|
353 | _ => cv) ct |
|
354 |
|
355 |
|
356 (** rewrite bool case expressions as if expressions **) |
|
357 |
|
358 local |
|
359 fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true |
|
360 | is_case_bool _ = false |
|
361 |
|
362 val thm = mk_meta_eq @{lemma |
|
363 "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp} |
|
364 |
|
365 fun unfold_conv _ = |
|
366 Old_SMT_Utils.if_true_conv (is_case_bool o Term.head_of) |
|
367 (expand_head_conv (Conv.rewr_conv thm)) |
|
368 in |
|
369 |
|
370 fun rewrite_case_bool_conv ctxt = |
|
371 Old_SMT_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt) |
|
372 |
|
373 val setup_case_bool = |
|
374 Old_SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"} |
|
375 |
|
376 end |
|
377 |
|
378 |
|
379 (** unfold abs, min and max **) |
|
380 |
|
381 local |
|
382 val abs_def = mk_meta_eq @{lemma |
|
383 "abs = (%a::'a::abs_if. if a < 0 then - a else a)" |
|
384 by (rule ext) (rule abs_if)} |
|
385 |
|
386 val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)" |
|
387 by (rule ext)+ (rule min_def)} |
|
388 |
|
389 val max_def = mk_meta_eq @{lemma "max = (%a b. if a <= b then b else a)" |
|
390 by (rule ext)+ (rule max_def)} |
|
391 |
|
392 val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def), |
|
393 (@{const_name abs}, abs_def)] |
|
394 |
|
395 fun is_builtinT ctxt T = |
|
396 Old_SMT_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T) |
|
397 |
|
398 fun abs_min_max ctxt (Const (n, T)) = |
|
399 (case AList.lookup (op =) defs n of |
|
400 NONE => NONE |
|
401 | SOME thm => if is_builtinT ctxt T then SOME thm else NONE) |
|
402 | abs_min_max _ _ = NONE |
|
403 |
|
404 fun unfold_amm_conv ctxt ct = |
|
405 (case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of |
|
406 SOME thm => expand_head_conv (Conv.rewr_conv thm) |
|
407 | NONE => Conv.all_conv) ct |
|
408 in |
|
409 |
|
410 fun unfold_abs_min_max_conv ctxt = |
|
411 Old_SMT_Utils.if_exists_conv (is_some o abs_min_max ctxt) |
|
412 (Conv.top_conv unfold_amm_conv ctxt) |
|
413 |
|
414 val setup_abs_min_max = fold (Old_SMT_Builtin.add_builtin_fun_ext'' o fst) defs |
|
415 |
|
416 end |
|
417 |
|
418 |
|
419 (** embedding of standard natural number operations into integer operations **) |
|
420 |
|
421 local |
|
422 val nat_embedding = @{lemma |
|
423 "ALL n. nat (int n) = n" |
|
424 "ALL i. i >= 0 --> int (nat i) = i" |
|
425 "ALL i. i < 0 --> int (nat i) = 0" |
|
426 by simp_all} |
|
427 |
|
428 val simple_nat_ops = [ |
|
429 @{const less (nat)}, @{const less_eq (nat)}, |
|
430 @{const Suc}, @{const plus (nat)}, @{const minus (nat)}] |
|
431 |
|
432 val mult_nat_ops = |
|
433 [@{const times (nat)}, @{const div (nat)}, @{const mod (nat)}] |
|
434 |
|
435 val nat_ops = simple_nat_ops @ mult_nat_ops |
|
436 |
|
437 val nat_consts = nat_ops @ [@{const numeral (nat)}, |
|
438 @{const zero_class.zero (nat)}, @{const one_class.one (nat)}] |
|
439 |
|
440 val nat_int_coercions = [@{const of_nat (int)}, @{const nat}] |
|
441 |
|
442 val builtin_nat_ops = nat_int_coercions @ simple_nat_ops |
|
443 |
|
444 val is_nat_const = member (op aconv) nat_consts |
|
445 |
|
446 fun is_nat_const' @{const of_nat (int)} = true |
|
447 | is_nat_const' t = is_nat_const t |
|
448 |
|
449 val expands = map mk_meta_eq @{lemma |
|
450 "0 = nat 0" |
|
451 "1 = nat 1" |
|
452 "(numeral :: num => nat) = (%i. nat (numeral i))" |
|
453 "op < = (%a b. int a < int b)" |
|
454 "op <= = (%a b. int a <= int b)" |
|
455 "Suc = (%a. nat (int a + 1))" |
|
456 "op + = (%a b. nat (int a + int b))" |
|
457 "op - = (%a b. nat (int a - int b))" |
|
458 "op * = (%a b. nat (int a * int b))" |
|
459 "op div = (%a b. nat (int a div int b))" |
|
460 "op mod = (%a b. nat (int a mod int b))" |
|
461 by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+} |
|
462 |
|
463 val ints = map mk_meta_eq @{lemma |
|
464 "int 0 = 0" |
|
465 "int 1 = 1" |
|
466 "int (Suc n) = int n + 1" |
|
467 "int (n + m) = int n + int m" |
|
468 "int (n - m) = int (nat (int n - int m))" |
|
469 "int (n * m) = int n * int m" |
|
470 "int (n div m) = int n div int m" |
|
471 "int (n mod m) = int n mod int m" |
|
472 by (auto simp add: int_mult zdiv_int zmod_int)} |
|
473 |
|
474 val int_if = mk_meta_eq @{lemma |
|
475 "int (if P then n else m) = (if P then int n else int m)" |
|
476 by simp} |
|
477 |
|
478 fun mk_number_eq ctxt i lhs = |
|
479 let |
|
480 val eq = Old_SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i) |
|
481 val tac = |
|
482 Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm Int.int_numeral}]) 1 |
|
483 in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end |
|
484 |
|
485 fun ite_conv cv1 cv2 = |
|
486 Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2 |
|
487 |
|
488 fun int_conv ctxt ct = |
|
489 (case Thm.term_of ct of |
|
490 @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) => |
|
491 Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct) |
|
492 | @{const of_nat (int)} $ _ => |
|
493 (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv |
|
494 (Conv.rewr_conv int_if then_conv |
|
495 ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv |
|
496 Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt |
|
497 | _ => Conv.no_conv) ct |
|
498 |
|
499 and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt |
|
500 |
|
501 and expand_conv ctxt = |
|
502 Old_SMT_Utils.if_conv (is_nat_const o Term.head_of) |
|
503 (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) |
|
504 (int_conv ctxt) |
|
505 |
|
506 and nat_conv ctxt = Old_SMT_Utils.if_exists_conv is_nat_const' |
|
507 (Conv.top_sweep_conv expand_conv ctxt) |
|
508 |
|
509 val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions) |
|
510 in |
|
511 |
|
512 val nat_as_int_conv = nat_conv |
|
513 |
|
514 fun add_nat_embedding thms = |
|
515 if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) |
|
516 else (thms, []) |
|
517 |
|
518 val setup_nat_as_int = |
|
519 Old_SMT_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #> |
|
520 fold (Old_SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops |
|
521 |
|
522 end |
|
523 |
|
524 |
|
525 (** normalize numerals **) |
|
526 |
|
527 local |
|
528 (* |
|
529 rewrite Numeral1 into 1 |
|
530 rewrite - 0 into 0 |
|
531 *) |
|
532 |
|
533 fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) = |
|
534 true |
|
535 | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) = |
|
536 true |
|
537 | is_irregular_number _ = |
|
538 false; |
|
539 |
|
540 fun is_strange_number ctxt t = is_irregular_number t andalso Old_SMT_Builtin.is_builtin_num ctxt t; |
|
541 |
|
542 val proper_num_ss = |
|
543 simpset_of (put_simpset HOL_ss @{context} |
|
544 addsimps @{thms Num.numeral_One minus_zero}) |
|
545 |
|
546 fun norm_num_conv ctxt = |
|
547 Old_SMT_Utils.if_conv (is_strange_number ctxt) |
|
548 (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv |
|
549 in |
|
550 |
|
551 fun normalize_numerals_conv ctxt = |
|
552 Old_SMT_Utils.if_exists_conv (is_strange_number ctxt) |
|
553 (Conv.top_sweep_conv norm_num_conv ctxt) |
|
554 |
|
555 end |
|
556 |
|
557 |
|
558 (** combined unfoldings and rewritings **) |
|
559 |
|
560 fun unfold_conv ctxt = |
|
561 rewrite_case_bool_conv ctxt then_conv |
|
562 unfold_abs_min_max_conv ctxt then_conv |
|
563 nat_as_int_conv ctxt then_conv |
|
564 Thm.beta_conversion true |
|
565 |
|
566 fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt))) |
|
567 |
|
568 fun burrow_ids f ithms = |
|
569 let |
|
570 val (is, thms) = split_list ithms |
|
571 val (thms', extra_thms) = f thms |
|
572 in (is ~~ thms') @ map (pair ~1) extra_thms end |
|
573 |
|
574 fun unfold2 ctxt ithms = |
|
575 ithms |
|
576 |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) |
|
577 |> burrow_ids add_nat_embedding |
|
578 |
|
579 |
|
580 |
|
581 (* overall normalization *) |
|
582 |
|
583 type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list |
|
584 |
|
585 structure Extra_Norms = Generic_Data |
|
586 ( |
|
587 type T = extra_norm Old_SMT_Utils.dict |
|
588 val empty = [] |
|
589 val extend = I |
|
590 fun merge data = Old_SMT_Utils.dict_merge fst data |
|
591 ) |
|
592 |
|
593 fun add_extra_norm (cs, norm) = |
|
594 Extra_Norms.map (Old_SMT_Utils.dict_update (cs, norm)) |
|
595 |
|
596 fun apply_extra_norms ctxt ithms = |
|
597 let |
|
598 val cs = Old_SMT_Config.solver_class_of ctxt |
|
599 val es = Old_SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs |
|
600 in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end |
|
601 |
|
602 local |
|
603 val ignored = member (op =) [@{const_name All}, @{const_name Ex}, |
|
604 @{const_name Let}, @{const_name If}, @{const_name HOL.eq}] |
|
605 |
|
606 val schematic_consts_of = |
|
607 let |
|
608 fun collect (@{const trigger} $ p $ t) = |
|
609 collect_trigger p #> collect t |
|
610 | collect (t $ u) = collect t #> collect u |
|
611 | collect (Abs (_, _, t)) = collect t |
|
612 | collect (t as Const (n, _)) = |
|
613 if not (ignored n) then Monomorph.add_schematic_consts_of t else I |
|
614 | collect _ = I |
|
615 and collect_trigger t = |
|
616 let val dest = these o try HOLogic.dest_list |
|
617 in fold (fold collect_pat o dest) (dest t) end |
|
618 and collect_pat (Const (@{const_name pat}, _) $ t) = collect t |
|
619 | collect_pat (Const (@{const_name nopat}, _) $ t) = collect t |
|
620 | collect_pat _ = I |
|
621 in (fn t => collect t Symtab.empty) end |
|
622 in |
|
623 |
|
624 fun monomorph ctxt xthms = |
|
625 let val (xs, thms) = split_list xthms |
|
626 in |
|
627 map (pair 1) thms |
|
628 |> Monomorph.monomorph schematic_consts_of ctxt |
|
629 |> maps (uncurry (map o pair)) o map2 pair xs o map (map snd) |
|
630 end |
|
631 |
|
632 end |
|
633 |
|
634 fun normalize iwthms ctxt = |
|
635 iwthms |
|
636 |> gen_normalize ctxt |
|
637 |> unfold1 ctxt |
|
638 |> monomorph ctxt |
|
639 |> unfold2 ctxt |
|
640 |> apply_extra_norms ctxt |
|
641 |> rpair ctxt |
|
642 |
|
643 val setup = Context.theory_map ( |
|
644 setup_atomize #> |
|
645 setup_unfolded_quants #> |
|
646 setup_trigger #> |
|
647 setup_weight #> |
|
648 setup_case_bool #> |
|
649 setup_abs_min_max #> |
|
650 setup_nat_as_int) |
|
651 |
|
652 end |