author | wenzelm |
Fri, 17 Dec 2010 13:12:58 +0100 | |
changeset 41224 | 8a104c2a186f |
parent 41194 | 9796e5e01b61 |
child 41280 | a7de9d36f4f2 |
permissions | -rw-r--r-- |
36898 | 1 |
(* Title: HOL/Tools/SMT/smt_normalize.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
4 |
Normalization steps on theorems required by SMT solvers. |
36898 | 5 |
*) |
6 |
||
7 |
signature SMT_NORMALIZE = |
|
8 |
sig |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
9 |
val atomize_conv: Proof.context -> conv |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
10 |
type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
11 |
val add_extra_norm: SMT_Utils.class * extra_norm -> Context.generic -> |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
12 |
Context.generic |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
13 |
val normalize: Proof.context -> (int * (int option * thm)) list -> |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
14 |
(int * thm) list |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
15 |
val setup: theory -> theory |
36898 | 16 |
end |
17 |
||
18 |
structure SMT_Normalize: SMT_NORMALIZE = |
|
19 |
struct |
|
20 |
||
40663 | 21 |
structure U = SMT_Utils |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
22 |
structure B = SMT_Builtin |
40663 | 23 |
|
36898 | 24 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
25 |
(* general theorem normalizations *) |
36898 | 26 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
27 |
(** instantiate elimination rules **) |
40685
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
28 |
|
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
29 |
local |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
30 |
val (cpfalse, cfalse) = `U.mk_cprop (Thm.cterm_of @{theory} @{const False}) |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
31 |
|
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
32 |
fun inst f ct thm = |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
33 |
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
34 |
in Thm.instantiate ([], [(cv, ct)]) thm end |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
35 |
in |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
36 |
|
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
37 |
fun instantiate_elim thm = |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
38 |
(case Thm.concl_of thm of |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
39 |
@{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
40 |
| Var _ => inst I cpfalse thm |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
41 |
| _ => thm) |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
42 |
|
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
43 |
end |
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
44 |
|
dcb27631cb45
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents:
40681
diff
changeset
|
45 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
46 |
(** normalize definitions **) |
36898 | 47 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
48 |
fun norm_def thm = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
49 |
(case Thm.prop_of thm of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
50 |
@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
51 |
norm_def (thm RS @{thm fun_cong}) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
52 |
| Const (@{const_name "=="}, _) $ _ $ Abs _ => |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
53 |
norm_def (thm RS @{thm meta_eq_to_obj_eq}) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
54 |
| _ => thm) |
36898 | 55 |
|
56 |
||
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
57 |
(** atomization **) |
36898 | 58 |
|
59 |
fun atomize_conv ctxt ct = |
|
60 |
(case Thm.term_of ct of |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40424
diff
changeset
|
61 |
@{const "==>"} $ _ $ _ => |
36898 | 62 |
Conv.binop_conv (atomize_conv ctxt) then_conv |
63 |
Conv.rewr_conv @{thm atomize_imp} |
|
64 |
| Const (@{const_name "=="}, _) $ _ $ _ => |
|
65 |
Conv.binop_conv (atomize_conv ctxt) then_conv |
|
66 |
Conv.rewr_conv @{thm atomize_eq} |
|
67 |
| Const (@{const_name all}, _) $ Abs _ => |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset
|
68 |
Conv.binder_conv (atomize_conv o snd) ctxt then_conv |
36898 | 69 |
Conv.rewr_conv @{thm atomize_all} |
70 |
| _ => Conv.all_conv) ct |
|
71 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
72 |
val setup_atomize = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
73 |
fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="}, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
74 |
@{const_name all}, @{const_name Trueprop}] |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
75 |
|
36898 | 76 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
77 |
(** unfold special quantifiers **) |
36898 | 78 |
|
79 |
local |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
80 |
val ex1_def = mk_meta_eq @{lemma |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
81 |
"Ex1 = (%P. EX x. P x & (ALL y. P y --> y = x))" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
82 |
by (rule ext) (simp only: Ex1_def)} |
36898 | 83 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
84 |
val ball_def = mk_meta_eq @{lemma "Ball = (%A P. ALL x. x : A --> P x)" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
85 |
by (rule ext)+ (rule Ball_def)} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
86 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
87 |
val bex_def = mk_meta_eq @{lemma "Bex = (%A P. EX x. x : A & P x)" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
88 |
by (rule ext)+ (rule Bex_def)} |
36898 | 89 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
90 |
val special_quants = [(@{const_name Ex1}, ex1_def), |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
91 |
(@{const_name Ball}, ball_def), (@{const_name Bex}, bex_def)] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
92 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
93 |
fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
94 |
| special_quant _ = NONE |
36898 | 95 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
96 |
fun special_quant_conv _ ct = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
97 |
(case special_quant (Thm.term_of ct) of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
98 |
SOME thm => Conv.rewr_conv thm |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
99 |
| NONE => Conv.all_conv) ct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
100 |
in |
36898 | 101 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
102 |
fun unfold_special_quants_conv ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
103 |
U.if_exists_conv (is_some o special_quant) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
104 |
(Conv.top_conv special_quant_conv ctxt) |
36898 | 105 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
106 |
val setup_unfolded_quants = fold (B.add_builtin_fun_ext'' o fst) special_quants |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
107 |
|
36898 | 108 |
end |
109 |
||
110 |
||
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
111 |
(** trigger inference **) |
36898 | 112 |
|
113 |
local |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
114 |
(*** check trigger syntax ***) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
115 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
116 |
fun dest_trigger (Const (@{const_name pat}, _) $ _) = SOME true |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
117 |
| dest_trigger (Const (@{const_name nopat}, _) $ _) = SOME false |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
118 |
| dest_trigger _ = NONE |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
119 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
120 |
fun eq_list [] = false |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
121 |
| eq_list (b :: bs) = forall (equal b) bs |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
122 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
123 |
fun proper_trigger t = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
124 |
t |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
125 |
|> these o try HOLogic.dest_list |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
126 |
|> map (map_filter dest_trigger o these o try HOLogic.dest_list) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
127 |
|> (fn [] => false | bss => forall eq_list bss) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
128 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
129 |
fun proper_quant inside f t = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
130 |
(case t of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
131 |
Const (@{const_name All}, _) $ Abs (_, _, u) => proper_quant true f u |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
132 |
| Const (@{const_name Ex}, _) $ Abs (_, _, u) => proper_quant true f u |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
133 |
| @{const trigger} $ p $ u => |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
134 |
(if inside then f p else false) andalso proper_quant false f u |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
135 |
| Abs (_, _, u) => proper_quant false f u |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
136 |
| u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2 |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
137 |
| _ => true) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
138 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
139 |
fun check_trigger_error ctxt t = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
140 |
error ("SMT triggers must only occur under quantifier and multipatterns " ^ |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
141 |
"must have the same kind: " ^ Syntax.string_of_term ctxt t) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
142 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
143 |
fun check_trigger_conv ctxt ct = |
41173
7c6178d45cc8
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents:
41126
diff
changeset
|
144 |
if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
145 |
else check_trigger_error ctxt (Thm.term_of ct) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
146 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
147 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
148 |
(*** infer simple triggers ***) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
149 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
150 |
fun dest_cond_eq ct = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
151 |
(case Thm.term_of ct of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
152 |
Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
153 |
| @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
154 |
| _ => raise CTERM ("no equation", [ct])) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
155 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
156 |
fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
157 |
| get_constrs _ _ = [] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
158 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
159 |
fun is_constr thy (n, T) = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
160 |
let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
161 |
in can (the o find_first match o get_constrs thy o Term.body_type) T end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
162 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
163 |
fun is_constr_pat thy t = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
164 |
(case Term.strip_comb t of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
165 |
(Free _, []) => true |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
166 |
| (Const c, ts) => is_constr thy c andalso forall (is_constr_pat thy) ts |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
167 |
| _ => false) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
168 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
169 |
fun is_simp_lhs ctxt t = |
36898 | 170 |
(case Term.strip_comb t of |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
171 |
(Const c, ts as _ :: _) => |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
172 |
not (B.is_builtin_fun_ext ctxt c ts) andalso |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
173 |
forall (is_constr_pat (ProofContext.theory_of ctxt)) ts |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
174 |
| _ => false) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
175 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
176 |
fun has_all_vars vs t = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
177 |
subset (op aconv) (vs, map Free (Term.add_frees t [])) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
178 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
179 |
fun minimal_pats vs ct = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
180 |
if has_all_vars vs (Thm.term_of ct) then |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
181 |
(case Thm.term_of ct of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
182 |
_ $ _ => |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
183 |
(case pairself (minimal_pats vs) (Thm.dest_comb ct) of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
184 |
([], []) => [[ct]] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
185 |
| (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss') |
41174
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41173
diff
changeset
|
186 |
| _ => []) |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
187 |
else [] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
188 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
189 |
fun proper_mpat _ _ _ [] = false |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
190 |
| proper_mpat thy gen u cts = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
191 |
let |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
192 |
val tps = (op ~~) (`gen (map Thm.term_of cts)) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
193 |
fun some_match u = tps |> exists (fn (t', t) => |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
194 |
Pattern.matches thy (t', u) andalso not (t aconv u)) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
195 |
in not (Term.exists_subterm some_match u) end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
196 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
197 |
val pat = U.mk_const_pat @{theory} @{const_name SMT.pat} U.destT1 |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
198 |
fun mk_pat ct = Thm.capply (U.instT' ct pat) ct |
36898 | 199 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
200 |
fun mk_clist T = pairself (Thm.cterm_of @{theory}) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
201 |
(HOLogic.cons_const T, HOLogic.nil_const T) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
202 |
fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
203 |
val mk_pat_list = mk_list (mk_clist @{typ SMT.pattern}) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
204 |
val mk_mpat_list = mk_list (mk_clist @{typ "SMT.pattern list"}) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
205 |
fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
206 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
207 |
val trigger_eq = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
208 |
mk_meta_eq @{lemma "p = SMT.trigger t p" by (simp add: trigger_def)} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
209 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
210 |
fun insert_trigger_conv [] ct = Conv.all_conv ct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
211 |
| insert_trigger_conv ctss ct = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
212 |
let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
213 |
in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
214 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
215 |
fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
216 |
let |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
217 |
val (lhs, rhs) = dest_cond_eq ct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
218 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
219 |
val vs = map Thm.term_of cvs |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
220 |
val thy = ProofContext.theory_of ctxt |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
221 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
222 |
fun get_mpats ct = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
223 |
if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
224 |
else [] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
225 |
val gen = Variable.export_terms ctxt outer_ctxt |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
226 |
val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs)) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
227 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
228 |
in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
229 |
|
41174
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41173
diff
changeset
|
230 |
fun has_trigger (@{const SMT.trigger} $ _ $ _) = true |
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41173
diff
changeset
|
231 |
| has_trigger _ = false |
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41173
diff
changeset
|
232 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
233 |
fun try_trigger_conv cv ct = |
41174
10eb369f8c01
fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents:
41173
diff
changeset
|
234 |
if U.under_quant has_trigger (U.term_of ct) then Conv.all_conv ct |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
235 |
else Conv.try_conv cv ct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
236 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
237 |
fun infer_trigger_conv ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
238 |
if Config.get ctxt SMT_Config.infer_triggers then |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
239 |
try_trigger_conv (U.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
240 |
else Conv.all_conv |
36898 | 241 |
in |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
242 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
243 |
fun trigger_conv ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
244 |
U.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt) |
36898 | 245 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
246 |
val setup_trigger = fold B.add_builtin_fun_ext'' |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
247 |
[@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}] |
36898 | 248 |
|
249 |
end |
|
250 |
||
251 |
||
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
252 |
(** adding quantifier weights **) |
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
253 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
254 |
local |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
255 |
(*** check weight syntax ***) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
256 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
257 |
val has_no_weight = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
258 |
not o Term.exists_subterm (fn @{const SMT.weight} => true | _ => false) |
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
259 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
260 |
fun is_weight (@{const SMT.weight} $ w $ t) = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
261 |
(case try HOLogic.dest_number w of |
41173
7c6178d45cc8
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents:
41126
diff
changeset
|
262 |
SOME (_, i) => i >= 0 andalso has_no_weight t |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
263 |
| _ => false) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
264 |
| is_weight t = has_no_weight t |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
265 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
266 |
fun proper_trigger (@{const SMT.trigger} $ _ $ t) = is_weight t |
41173
7c6178d45cc8
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents:
41126
diff
changeset
|
267 |
| proper_trigger t = is_weight t |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
268 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
269 |
fun check_weight_error ctxt t = |
41173
7c6178d45cc8
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents:
41126
diff
changeset
|
270 |
error ("SMT weight must be a non-negative number and must only occur " ^ |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
271 |
"under the top-most quantifier and an optional trigger: " ^ |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
272 |
Syntax.string_of_term ctxt t) |
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
273 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
274 |
fun check_weight_conv ctxt ct = |
41173
7c6178d45cc8
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents:
41126
diff
changeset
|
275 |
if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
276 |
else check_weight_error ctxt (Thm.term_of ct) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
277 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
278 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
279 |
(*** insertion of weights ***) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
280 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
281 |
fun under_trigger_conv cv ct = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
282 |
(case Thm.term_of ct of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
283 |
@{const SMT.trigger} $ _ $ _ => Conv.arg_conv cv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
284 |
| _ => cv) ct |
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
285 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
286 |
val weight_eq = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
287 |
mk_meta_eq @{lemma "p = SMT.weight i p" by (simp add: weight_def)} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
288 |
fun mk_weight_eq w = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
289 |
let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
290 |
in |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
291 |
Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
292 |
end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
293 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
294 |
fun add_weight_conv NONE _ = Conv.all_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
295 |
| add_weight_conv (SOME weight) ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
296 |
let val cv = Conv.rewr_conv (mk_weight_eq weight) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
297 |
in U.under_quant_conv (K (under_trigger_conv cv)) ctxt end |
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
298 |
in |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
299 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
300 |
fun weight_conv weight ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
301 |
U.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
302 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
303 |
val setup_weight = B.add_builtin_fun_ext'' @{const_name SMT.weight} |
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
304 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
305 |
end |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
306 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
38864
diff
changeset
|
307 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
308 |
(** combined general normalizations **) |
36898 | 309 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
310 |
fun gen_normalize1_conv ctxt weight = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
311 |
atomize_conv ctxt then_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
312 |
unfold_special_quants_conv ctxt then_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
313 |
trigger_conv ctxt then_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
314 |
weight_conv weight ctxt |
36898 | 315 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
316 |
fun gen_normalize1 ctxt weight thm = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
317 |
thm |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
318 |
|> instantiate_elim |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
319 |
|> norm_def |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
320 |
|> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
321 |
|> Drule.forall_intr_vars |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
322 |
|> Conv.fconv_rule (gen_normalize1_conv ctxt weight) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
323 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
324 |
fun drop_fact_warning ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
325 |
let val pre = prefix "Warning: dropping assumption: " |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
326 |
in SMT_Config.verbose_msg ctxt (pre o Display.string_of_thm ctxt) end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
327 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
328 |
fun gen_norm1_safe ctxt (i, (weight, thm)) = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
329 |
if Config.get ctxt SMT_Config.drop_bad_facts then |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
330 |
(case try (gen_normalize1 ctxt weight) thm of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
331 |
SOME thm' => SOME (i, thm') |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
332 |
| NONE => (drop_fact_warning ctxt thm; NONE)) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
333 |
else SOME (i, gen_normalize1 ctxt weight thm) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
334 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
335 |
fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms |
36898 | 336 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
337 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
338 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
339 |
(* unfolding of definitions and theory-specific rewritings *) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
340 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
341 |
(** unfold trivial distincts **) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
342 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
343 |
local |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
344 |
fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
345 |
(case try HOLogic.dest_list t of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
346 |
SOME [] => true |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
347 |
| SOME [_] => true |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
348 |
| _ => false) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
349 |
| is_trivial_distinct _ = false |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
350 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
351 |
val thms = map mk_meta_eq @{lemma |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
352 |
"distinct [] = True" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
353 |
"distinct [x] = True" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
354 |
"distinct [x, y] = (x ~= y)" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
355 |
by simp_all} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
356 |
fun distinct_conv _ = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
357 |
U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
358 |
in |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
359 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
360 |
fun trivial_distinct_conv ctxt = U.if_exists_conv is_trivial_distinct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
361 |
(Conv.top_conv distinct_conv ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
362 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
363 |
end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
364 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
365 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
366 |
(** rewrite bool case expressions as if expressions **) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
367 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
368 |
local |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
369 |
fun is_bool_case (Const (@{const_name "bool.bool_case"}, _)) = true |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
370 |
| is_bool_case _ = false |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
371 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
372 |
val thm = mk_meta_eq @{lemma |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
373 |
"bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
374 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
375 |
fun unfold_conv _ = U.if_true_conv is_bool_case (Conv.rewr_conv thm) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
376 |
in |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
377 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
378 |
fun rewrite_bool_case_conv ctxt = U.if_exists_conv is_bool_case |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
379 |
(Conv.top_conv unfold_conv ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
380 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
381 |
val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
382 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
383 |
end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
384 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
385 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
386 |
(** unfold abs, min and max **) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
387 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
388 |
local |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
389 |
val abs_def = mk_meta_eq @{lemma |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
390 |
"abs = (%a::'a::abs_if. if a < 0 then - a else a)" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
391 |
by (rule ext) (rule abs_if)} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
392 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
393 |
val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
394 |
by (rule ext)+ (rule min_def)} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
395 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
396 |
val max_def = mk_meta_eq @{lemma "max = (%a b. if a <= b then b else a)" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
397 |
by (rule ext)+ (rule max_def)} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
398 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
399 |
val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def), |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
400 |
(@{const_name abs}, abs_def)] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
401 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
402 |
fun is_builtinT ctxt T = B.is_builtin_typ_ext ctxt (Term.domain_type T) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
403 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
404 |
fun abs_min_max ctxt (Const (n, T)) = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
405 |
(case AList.lookup (op =) defs n of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
406 |
NONE => NONE |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
407 |
| SOME thm => if is_builtinT ctxt T then SOME thm else NONE) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
408 |
| abs_min_max _ _ = NONE |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
409 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
410 |
fun unfold_amm_conv ctxt ct = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
411 |
(case abs_min_max ctxt (Thm.term_of ct) of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
412 |
SOME thm => Conv.rewr_conv thm |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
413 |
| NONE => Conv.all_conv) ct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
414 |
in |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
415 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
416 |
fun unfold_abs_min_max_conv ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
417 |
U.if_exists_conv (is_some o abs_min_max ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
418 |
(Conv.top_conv unfold_amm_conv ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
419 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
420 |
val setup_abs_min_max = fold (B.add_builtin_fun_ext'' o fst) defs |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
421 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
422 |
end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
423 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
424 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
425 |
(** embedding of standard natural number operations into integer operations **) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
426 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
427 |
local |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
428 |
val nat_embedding = @{lemma |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
429 |
"ALL n. nat (int n) = n" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
430 |
"ALL i. i >= 0 --> int (nat i) = i" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
431 |
"ALL i. i < 0 --> int (nat i) = 0" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
432 |
by simp_all} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
433 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
434 |
val nat_ops = [ |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
435 |
@{const less (nat)}, @{const less_eq (nat)}, |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
436 |
@{const Suc}, @{const plus (nat)}, @{const minus (nat)}, |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
437 |
@{const times (nat)}, @{const div (nat)}, @{const mod (nat)}] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
438 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
439 |
val nat_consts = nat_ops @ [@{const number_of (nat)}, |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
440 |
@{const zero_class.zero (nat)}, @{const one_class.one (nat)}] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
441 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
442 |
val nat_int_coercions = [@{const of_nat (int)}, @{const nat}] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
443 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
444 |
val nat_ops' = nat_int_coercions @ nat_ops |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
445 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
446 |
val is_nat_const = member (op aconv) nat_consts |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
447 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
448 |
val expands = map mk_meta_eq @{lemma |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
449 |
"0 = nat 0" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
450 |
"1 = nat 1" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
451 |
"(number_of :: int => nat) = (%i. nat (number_of i))" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
452 |
"op < = (%a b. int a < int b)" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
453 |
"op <= = (%a b. int a <= int b)" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
454 |
"Suc = (%a. nat (int a + 1))" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
455 |
"op + = (%a b. nat (int a + int b))" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
456 |
"op - = (%a b. nat (int a - int b))" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
457 |
"op * = (%a b. nat (int a * int b))" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
458 |
"op div = (%a b. nat (int a div int b))" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
459 |
"op mod = (%a b. nat (int a mod int b))" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
460 |
by (auto intro!: ext simp add: nat_mult_distrib nat_div_distrib |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
461 |
nat_mod_distrib)} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
462 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
463 |
val ints = map mk_meta_eq @{lemma |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
464 |
"int 0 = 0" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
465 |
"int 1 = 1" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
466 |
"int (Suc n) = int n + 1" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
467 |
"int (n + m) = int n + int m" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
468 |
"int (n - m) = int (nat (int n - int m))" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
469 |
"int (n * m) = int n * int m" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
470 |
"int (n div m) = int n div int m" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
471 |
"int (n mod m) = int n mod int m" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
472 |
"int (if P then n else m) = (if P then int n else int m)" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
473 |
by (auto simp add: int_mult zdiv_int zmod_int)} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
474 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
475 |
fun mk_number_eq ctxt i lhs = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
476 |
let |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
477 |
val eq = U.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
478 |
val ss = HOL_ss |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
479 |
addsimps [@{thm Nat_Numeral.int_nat_number_of}] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
480 |
addsimps @{thms neg_simps} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
481 |
fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1 |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
482 |
in Goal.norm_result (Goal.prove_internal [] eq tac) end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
483 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
484 |
fun expand_head_conv cv ct = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
485 |
(case Thm.term_of ct of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
486 |
_ $ _ => |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
487 |
Conv.fun_conv (expand_head_conv cv) then_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
488 |
Thm.beta_conversion false |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
489 |
| _ => cv) ct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
490 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
491 |
fun int_conv ctxt ct = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
492 |
(case Thm.term_of ct of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
493 |
@{const of_nat (int)} $ (n as (@{const number_of (nat)} $ _)) => |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
494 |
Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
495 |
| @{const of_nat (int)} $ _ => |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
496 |
(Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
497 |
Conv.top_sweep_conv nat_conv ctxt |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
498 |
| _ => Conv.no_conv) ct |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
499 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
500 |
and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
501 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
502 |
and expand_conv ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
503 |
U.if_conv (not o is_nat_const o Term.head_of) Conv.no_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
504 |
(expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
505 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
506 |
and nat_conv ctxt = U.if_exists_conv is_nat_const |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
507 |
(Conv.top_sweep_conv expand_conv ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
508 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
509 |
val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
510 |
in |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
511 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
512 |
val nat_as_int_conv = nat_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
513 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
514 |
fun add_nat_embedding thms = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
515 |
if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
516 |
else (thms, []) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
517 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
518 |
val setup_nat_as_int = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
519 |
B.add_builtin_typ_ext (@{typ nat}, K true) #> |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
520 |
fold (B.add_builtin_fun_ext' o Term.dest_Const) nat_ops' |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
521 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
522 |
end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
523 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
524 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
525 |
(** normalize numerals **) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
526 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
527 |
local |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
528 |
(* |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
529 |
rewrite negative numerals into positive numerals, |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
530 |
rewrite Numeral0 into 0 |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
531 |
rewrite Numeral1 into 1 |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
532 |
*) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
533 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
534 |
fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) $ _) = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
535 |
(case try HOLogic.dest_number t of |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
536 |
SOME (_, i) => B.is_builtin_num ctxt t andalso i < 2 |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
537 |
| NONE => false) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
538 |
| is_strange_number _ _ = false |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
539 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
540 |
val pos_num_ss = HOL_ss |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
541 |
addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
542 |
addsimps [@{thm Int.number_of_Pls}, @{thm Int.numeral_1_eq_1}] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
543 |
addsimps @{thms Int.pred_bin_simps} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
544 |
addsimps @{thms Int.normalize_bin_simps} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
545 |
addsimps @{lemma |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
546 |
"Int.Min = - Int.Bit1 Int.Pls" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
547 |
"Int.Bit0 (- Int.Pls) = - Int.Pls" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
548 |
"Int.Bit0 (- k) = - Int.Bit0 k" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
549 |
"Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)" |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
550 |
by simp_all (simp add: pred_def)} |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
551 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
552 |
fun norm_num_conv ctxt = U.if_conv (is_strange_number ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
553 |
(Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
554 |
in |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
555 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
556 |
fun normalize_numerals_conv ctxt = U.if_exists_conv (is_strange_number ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
557 |
(Conv.top_sweep_conv norm_num_conv ctxt) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
558 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
559 |
end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
560 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
561 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
562 |
(** combined unfoldings and rewritings **) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
563 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
564 |
fun unfold_conv ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
565 |
trivial_distinct_conv ctxt then_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
566 |
rewrite_bool_case_conv ctxt then_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
567 |
unfold_abs_min_max_conv ctxt then_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
568 |
nat_as_int_conv ctxt then_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
569 |
normalize_numerals_conv ctxt then_conv |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
570 |
Thm.beta_conversion true |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
571 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
572 |
fun burrow_ids f ithms = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
573 |
let |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
574 |
val (is, thms) = split_list ithms |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
575 |
val (thms', extra_thms) = f thms |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
576 |
in (is ~~ thms') @ map (pair ~1) extra_thms end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
577 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
578 |
fun unfold ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
579 |
burrow_ids (map (Conv.fconv_rule (unfold_conv ctxt)) #> add_nat_embedding) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
580 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
581 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
582 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
583 |
(* overall normalization *) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
584 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
585 |
type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
586 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
587 |
structure Extra_Norms = Generic_Data |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
588 |
( |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
589 |
type T = extra_norm U.dict |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
590 |
val empty = [] |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
591 |
val extend = I |
41224 | 592 |
fun merge data = U.dict_merge fst data |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
593 |
) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
594 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
595 |
fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm)) |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
596 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
597 |
fun apply_extra_norms ctxt = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
598 |
let |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
599 |
val cs = SMT_Config.solver_class_of ctxt |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
600 |
val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
601 |
in burrow_ids (fold (fn e => e ctxt) es o rpair []) end |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
602 |
|
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
603 |
fun normalize ctxt iwthms = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
604 |
iwthms |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
605 |
|> gen_normalize ctxt |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
606 |
|> unfold ctxt |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
607 |
|> apply_extra_norms ctxt |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
608 |
|
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
609 |
val setup = Context.theory_map ( |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
610 |
setup_atomize #> |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
611 |
setup_unfolded_quants #> |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
612 |
setup_trigger #> |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
613 |
setup_weight #> |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
614 |
setup_bool_case #> |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
615 |
setup_abs_min_max #> |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41072
diff
changeset
|
616 |
setup_nat_as_int) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40686
diff
changeset
|
617 |
|
36898 | 618 |
end |