author | boehmes |
Wed, 24 Nov 2010 10:39:58 +0100 | |
changeset 40681 | 872b08416fb4 |
parent 40663 | e080c9e68752 |
child 40685 | dcb27631cb45 |
permissions | -rw-r--r-- |
36898 | 1 |
(* Title: HOL/Tools/SMT/smt_normalize.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Normalization steps on theorems required by SMT solvers: |
|
5 |
* simplify trivial distincts (those with less than three elements), |
|
6 |
* rewrite bool case expressions as if expressions, |
|
7 |
* normalize numerals (e.g. replace negative numerals by negated positive |
|
8 |
numerals), |
|
9 |
* embed natural numbers into integers, |
|
10 |
* add extra rules specifying types and constants which occur frequently, |
|
11 |
* fully translate into object logic, add universal closure, |
|
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
|
12 |
* monomorphize (create instances of schematic rules), |
36898 | 13 |
* lift lambda terms, |
14 |
* make applications explicit for functions with varying number of arguments. |
|
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
|
15 |
* add (hypothetical definitions for) missing datatype selectors, |
36898 | 16 |
*) |
17 |
||
18 |
signature SMT_NORMALIZE = |
|
19 |
sig |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
20 |
type extra_norm = bool -> (int * thm) list -> Proof.context -> |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
21 |
(int * thm) list * Proof.context |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40279
diff
changeset
|
22 |
val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context -> |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
23 |
(int * thm) list * Proof.context |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
24 |
val atomize_conv: Proof.context -> conv |
36898 | 25 |
val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv |
26 |
end |
|
27 |
||
28 |
structure SMT_Normalize: SMT_NORMALIZE = |
|
29 |
struct |
|
30 |
||
40663 | 31 |
structure U = SMT_Utils |
32 |
||
36898 | 33 |
infix 2 ?? |
34 |
fun (test ?? f) x = if test x then f x else x |
|
35 |
||
36 |
||
37 |
||
38 |
(* simplification of trivial distincts (distinct should have at least |
|
39 |
three elements in the argument list) *) |
|
40 |
||
41 |
local |
|
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
42 |
fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) = |
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
43 |
(case try HOLogic.dest_list t of |
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
44 |
SOME [] => true |
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
45 |
| SOME [_] => true |
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
46 |
| _ => false) |
36898 | 47 |
| is_trivial_distinct _ = false |
48 |
||
37786
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents:
37153
diff
changeset
|
49 |
val thms = map mk_meta_eq @{lemma |
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
50 |
"distinct [] = True" |
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
51 |
"distinct [x] = True" |
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
52 |
"distinct [x, y] = (x ~= y)" |
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40663
diff
changeset
|
53 |
by simp_all} |
36898 | 54 |
fun distinct_conv _ = |
40663 | 55 |
U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms) |
36898 | 56 |
in |
57 |
fun trivial_distinct ctxt = |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
58 |
map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ?? |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
59 |
Conv.fconv_rule (Conv.top_conv distinct_conv ctxt))) |
36898 | 60 |
end |
61 |
||
62 |
||
63 |
||
64 |
(* rewrite bool case expressions as if expressions *) |
|
65 |
||
66 |
local |
|
67 |
val is_bool_case = (fn |
|
68 |
Const (@{const_name "bool.bool_case"}, _) $ _ $ _ $ _ => true |
|
69 |
| _ => false) |
|
70 |
||
40275 | 71 |
val thm = mk_meta_eq @{lemma |
72 |
"(case P of True => x | False => y) = (if P then x else y)" by simp} |
|
40663 | 73 |
val unfold_conv = U.if_true_conv is_bool_case (Conv.rewr_conv thm) |
36898 | 74 |
in |
75 |
fun rewrite_bool_cases ctxt = |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
76 |
map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ?? |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
77 |
Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt))) |
36898 | 78 |
end |
79 |
||
80 |
||
81 |
||
82 |
(* normalization of numerals: rewriting of negative integer numerals into |
|
83 |
positive numerals, Numeral0 into 0, Numeral1 into 1 *) |
|
84 |
||
85 |
local |
|
86 |
fun is_number_sort ctxt T = |
|
87 |
Sign.of_sort (ProofContext.theory_of ctxt) (T, @{sort number_ring}) |
|
88 |
||
89 |
fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) $ _) = |
|
90 |
(case try HOLogic.dest_number t of |
|
91 |
SOME (T, i) => is_number_sort ctxt T andalso i < 2 |
|
92 |
| NONE => false) |
|
93 |
| is_strange_number _ _ = false |
|
94 |
||
95 |
val pos_numeral_ss = HOL_ss |
|
96 |
addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}] |
|
97 |
addsimps [@{thm Int.number_of_Pls}, @{thm Int.numeral_1_eq_1}] |
|
98 |
addsimps @{thms Int.pred_bin_simps} |
|
99 |
addsimps @{thms Int.normalize_bin_simps} |
|
100 |
addsimps @{lemma |
|
101 |
"Int.Min = - Int.Bit1 Int.Pls" |
|
102 |
"Int.Bit0 (- Int.Pls) = - Int.Pls" |
|
103 |
"Int.Bit0 (- k) = - Int.Bit0 k" |
|
104 |
"Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)" |
|
105 |
by simp_all (simp add: pred_def)} |
|
106 |
||
40663 | 107 |
fun pos_conv ctxt = U.if_conv (is_strange_number ctxt) |
36898 | 108 |
(Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss)) |
109 |
Conv.no_conv |
|
110 |
in |
|
111 |
fun normalize_numerals ctxt = |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
112 |
map (apsnd ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ?? |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
113 |
Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt))) |
36898 | 114 |
end |
115 |
||
116 |
||
117 |
||
118 |
(* embedding of standard natural number operations into integer operations *) |
|
119 |
||
120 |
local |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
121 |
val nat_embedding = map (pair ~1) @{lemma |
36898 | 122 |
"nat (int n) = n" |
123 |
"i >= 0 --> int (nat i) = i" |
|
124 |
"i < 0 --> int (nat i) = 0" |
|
125 |
by simp_all} |
|
126 |
||
127 |
val nat_rewriting = @{lemma |
|
128 |
"0 = nat 0" |
|
129 |
"1 = nat 1" |
|
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
130 |
"(number_of :: int => nat) = (%i. nat (number_of i))" |
36898 | 131 |
"int (nat 0) = 0" |
132 |
"int (nat 1) = 1" |
|
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
133 |
"op < = (%a b. int a < int b)" |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
134 |
"op <= = (%a b. int a <= int b)" |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
135 |
"Suc = (%a. nat (int a + 1))" |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
136 |
"op + = (%a b. nat (int a + int b))" |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
137 |
"op - = (%a b. nat (int a - int b))" |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
138 |
"op * = (%a b. nat (int a * int b))" |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
139 |
"op div = (%a b. nat (int a div int b))" |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
140 |
"op mod = (%a b. nat (int a mod int b))" |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
141 |
"min = (%a b. nat (min (int a) (int b)))" |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
142 |
"max = (%a b. nat (max (int a) (int b)))" |
36898 | 143 |
"int (nat (int a + int b)) = int a + int b" |
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
144 |
"int (nat (int a + 1)) = int a + 1" (* special rule due to Suc above *) |
36898 | 145 |
"int (nat (int a * int b)) = int a * int b" |
146 |
"int (nat (int a div int b)) = int a div int b" |
|
147 |
"int (nat (int a mod int b)) = int a mod int b" |
|
148 |
"int (nat (min (int a) (int b))) = min (int a) (int b)" |
|
149 |
"int (nat (max (int a) (int b))) = max (int a) (int b)" |
|
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
150 |
by (auto intro!: ext simp add: nat_mult_distrib nat_div_distrib |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
151 |
nat_mod_distrib int_mult[symmetric] zdiv_int[symmetric] |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
152 |
zmod_int[symmetric])} |
36898 | 153 |
|
154 |
fun on_positive num f x = |
|
155 |
(case try HOLogic.dest_number (Thm.term_of num) of |
|
156 |
SOME (_, i) => if i >= 0 then SOME (f x) else NONE |
|
157 |
| NONE => NONE) |
|
158 |
||
159 |
val cancel_int_nat_ss = HOL_ss |
|
160 |
addsimps [@{thm Nat_Numeral.nat_number_of}] |
|
161 |
addsimps [@{thm Nat_Numeral.int_nat_number_of}] |
|
162 |
addsimps @{thms neg_simps} |
|
163 |
||
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
|
164 |
val int_eq = Thm.cterm_of @{theory} @{const "==" (int)} |
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
|
165 |
|
36898 | 166 |
fun cancel_int_nat_simproc _ ss ct = |
167 |
let |
|
168 |
val num = Thm.dest_arg (Thm.dest_arg ct) |
|
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
|
169 |
val goal = Thm.mk_binop int_eq ct num |
36898 | 170 |
val simpset = Simplifier.inherit_context ss cancel_int_nat_ss |
171 |
fun tac _ = Simplifier.simp_tac simpset 1 |
|
172 |
in on_positive num (Goal.prove_internal [] goal) tac end |
|
173 |
||
174 |
val nat_ss = HOL_ss |
|
175 |
addsimps nat_rewriting |
|
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
176 |
addsimprocs [ |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
177 |
Simplifier.make_simproc { |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
178 |
name = "cancel_int_nat_num", lhss = [@{cpat "int (nat _)"}], |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
179 |
proc = cancel_int_nat_simproc, identifier = [] }] |
36898 | 180 |
|
181 |
fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss) |
|
182 |
||
183 |
val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat})) |
|
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
|
184 |
val uses_nat_int = Term.exists_subterm (member (op aconv) |
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
|
185 |
[@{const of_nat (int)}, @{const nat}]) |
36898 | 186 |
in |
187 |
fun nat_as_int ctxt = |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
188 |
map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #> |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
189 |
exists (uses_nat_int o Thm.prop_of o snd) ?? append nat_embedding |
36898 | 190 |
end |
191 |
||
192 |
||
193 |
||
194 |
(* further normalizations: beta/eta, universal closure, atomize *) |
|
195 |
||
196 |
val eta_expand_eq = @{lemma "f == (%x. f x)" by (rule reflexive)} |
|
197 |
||
198 |
fun eta_expand_conv cv ctxt = |
|
199 |
Conv.rewr_conv eta_expand_eq then_conv Conv.abs_conv (cv o snd) ctxt |
|
200 |
||
201 |
local |
|
202 |
val eta_conv = eta_expand_conv |
|
203 |
||
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
204 |
fun args_conv cv ct = |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
205 |
(case Thm.term_of ct of |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
206 |
_ $ _ => Conv.combination_conv (args_conv cv) cv |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
207 |
| _ => Conv.all_conv) ct |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
208 |
|
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
209 |
fun eta_args_conv cv 0 = args_conv o cv |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
210 |
| eta_args_conv cv i = eta_conv (eta_args_conv cv (i-1)) |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
211 |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset
|
212 |
fun keep_conv ctxt = Conv.binder_conv (norm_conv o snd) ctxt |
36898 | 213 |
and eta_binder_conv ctxt = Conv.arg_conv (eta_conv norm_conv ctxt) |
214 |
and keep_let_conv ctxt = Conv.combination_conv |
|
215 |
(Conv.arg_conv (norm_conv ctxt)) (Conv.abs_conv (norm_conv o snd) ctxt) |
|
216 |
and unfold_let_conv ctxt = Conv.combination_conv |
|
217 |
(Conv.arg_conv (norm_conv ctxt)) (eta_conv norm_conv ctxt) |
|
218 |
and unfold_conv thm ctxt = Conv.rewr_conv thm then_conv keep_conv ctxt |
|
219 |
and unfold_ex1_conv ctxt = unfold_conv @{thm Ex1_def} ctxt |
|
37786
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents:
37153
diff
changeset
|
220 |
and unfold_ball_conv ctxt = unfold_conv (mk_meta_eq @{thm Ball_def}) ctxt |
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents:
37153
diff
changeset
|
221 |
and unfold_bex_conv ctxt = unfold_conv (mk_meta_eq @{thm Bex_def}) ctxt |
36898 | 222 |
and norm_conv ctxt ct = |
223 |
(case Thm.term_of ct of |
|
224 |
Const (@{const_name All}, _) $ Abs _ => keep_conv |
|
225 |
| Const (@{const_name All}, _) $ _ => eta_binder_conv |
|
226 |
| Const (@{const_name All}, _) => eta_conv eta_binder_conv |
|
227 |
| Const (@{const_name Ex}, _) $ Abs _ => keep_conv |
|
228 |
| Const (@{const_name Ex}, _) $ _ => eta_binder_conv |
|
229 |
| Const (@{const_name Ex}, _) => eta_conv eta_binder_conv |
|
230 |
| Const (@{const_name Let}, _) $ _ $ Abs _ => keep_let_conv |
|
231 |
| Const (@{const_name Let}, _) $ _ $ _ => unfold_let_conv |
|
232 |
| Const (@{const_name Let}, _) $ _ => eta_conv unfold_let_conv |
|
233 |
| Const (@{const_name Let}, _) => eta_conv (eta_conv unfold_let_conv) |
|
234 |
| Const (@{const_name Ex1}, _) $ _ => unfold_ex1_conv |
|
235 |
| Const (@{const_name Ex1}, _) => eta_conv unfold_ex1_conv |
|
236 |
| Const (@{const_name Ball}, _) $ _ $ _ => unfold_ball_conv |
|
237 |
| Const (@{const_name Ball}, _) $ _ => eta_conv unfold_ball_conv |
|
238 |
| Const (@{const_name Ball}, _) => eta_conv (eta_conv unfold_ball_conv) |
|
239 |
| Const (@{const_name Bex}, _) $ _ $ _ => unfold_bex_conv |
|
240 |
| Const (@{const_name Bex}, _) $ _ => eta_conv unfold_bex_conv |
|
241 |
| Const (@{const_name Bex}, _) => eta_conv (eta_conv unfold_bex_conv) |
|
242 |
| Abs _ => Conv.abs_conv (norm_conv o snd) |
|
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
243 |
| _ => |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
244 |
(case Term.strip_comb (Thm.term_of ct) of |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
245 |
(Const (c as (_, T)), ts) => |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
246 |
if SMT_Builtin.is_builtin ctxt c |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
247 |
then eta_args_conv norm_conv |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
248 |
(length (Term.binder_types T) - length ts) |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
249 |
else args_conv o norm_conv |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40279
diff
changeset
|
250 |
| _ => args_conv o norm_conv)) ctxt ct |
36898 | 251 |
|
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
252 |
fun is_normed ctxt t = |
36898 | 253 |
(case t of |
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
254 |
Const (@{const_name All}, _) $ Abs (_, _, u) => is_normed ctxt u |
36898 | 255 |
| Const (@{const_name All}, _) $ _ => false |
256 |
| Const (@{const_name All}, _) => false |
|
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
257 |
| Const (@{const_name Ex}, _) $ Abs (_, _, u) => is_normed ctxt u |
36898 | 258 |
| Const (@{const_name Ex}, _) $ _ => false |
259 |
| Const (@{const_name Ex}, _) => false |
|
260 |
| Const (@{const_name Let}, _) $ u1 $ Abs (_, _, u2) => |
|
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
261 |
is_normed ctxt u1 andalso is_normed ctxt u2 |
36898 | 262 |
| Const (@{const_name Let}, _) $ _ $ _ => false |
263 |
| Const (@{const_name Let}, _) $ _ => false |
|
264 |
| Const (@{const_name Let}, _) => false |
|
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
265 |
| Const (@{const_name Ex1}, _) $ _ => false |
36898 | 266 |
| Const (@{const_name Ex1}, _) => false |
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
267 |
| Const (@{const_name Ball}, _) $ _ $ _ => false |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
268 |
| Const (@{const_name Ball}, _) $ _ => false |
36898 | 269 |
| Const (@{const_name Ball}, _) => false |
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
270 |
| Const (@{const_name Bex}, _) $ _ $ _ => false |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
271 |
| Const (@{const_name Bex}, _) $ _ => false |
36898 | 272 |
| Const (@{const_name Bex}, _) => false |
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
273 |
| Abs (_, _, u) => is_normed ctxt u |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
274 |
| _ => |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
275 |
(case Term.strip_comb t of |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
276 |
(Const (c as (_, T)), ts) => |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
277 |
if SMT_Builtin.is_builtin ctxt c |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
278 |
then length (Term.binder_types T) = length ts andalso |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
279 |
forall (is_normed ctxt) ts |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
280 |
else forall (is_normed ctxt) ts |
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
281 |
| (_, ts) => forall (is_normed ctxt) ts)) |
36898 | 282 |
in |
40279
96365b4ae7b6
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes
parents:
40278
diff
changeset
|
283 |
fun norm_binder_conv ctxt = |
40663 | 284 |
U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt) |
36898 | 285 |
end |
286 |
||
287 |
fun norm_def ctxt thm = |
|
288 |
(case Thm.prop_of thm 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
|
289 |
@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => |
36898 | 290 |
norm_def ctxt (thm RS @{thm fun_cong}) |
291 |
| Const (@{const_name "=="}, _) $ _ $ Abs _ => |
|
292 |
norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq}) |
|
293 |
| _ => thm) |
|
294 |
||
295 |
fun atomize_conv ctxt ct = |
|
296 |
(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
|
297 |
@{const "==>"} $ _ $ _ => |
36898 | 298 |
Conv.binop_conv (atomize_conv ctxt) then_conv |
299 |
Conv.rewr_conv @{thm atomize_imp} |
|
300 |
| Const (@{const_name "=="}, _) $ _ $ _ => |
|
301 |
Conv.binop_conv (atomize_conv ctxt) then_conv |
|
302 |
Conv.rewr_conv @{thm atomize_eq} |
|
303 |
| Const (@{const_name all}, _) $ Abs _ => |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset
|
304 |
Conv.binder_conv (atomize_conv o snd) ctxt then_conv |
36898 | 305 |
Conv.rewr_conv @{thm atomize_all} |
306 |
| _ => Conv.all_conv) ct |
|
307 |
||
308 |
fun normalize_rule ctxt = |
|
309 |
Conv.fconv_rule ( |
|
310 |
(* reduce lambda abstractions, except at known binders: *) |
|
311 |
Thm.beta_conversion true then_conv |
|
312 |
Thm.eta_conversion then_conv |
|
313 |
norm_binder_conv ctxt) #> |
|
314 |
norm_def ctxt #> |
|
315 |
Drule.forall_intr_vars #> |
|
316 |
Conv.fconv_rule (atomize_conv ctxt) |
|
317 |
||
318 |
||
319 |
||
320 |
(* lift lambda terms into additional rules *) |
|
321 |
||
322 |
local |
|
323 |
fun used_vars cvs ct = |
|
324 |
let |
|
325 |
val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs) |
|
326 |
val add = (fn SOME ct => insert (op aconvc) ct | _ => I) |
|
327 |
in Term.fold_aterms (add o lookup) (Thm.term_of ct) [] end |
|
328 |
||
329 |
fun apply cv thm = |
|
330 |
let val thm' = Thm.combination thm (Thm.reflexive cv) |
|
331 |
in Thm.transitive thm' (Thm.beta_conversion false (Thm.rhs_of thm')) end |
|
332 |
fun apply_def cvs eq = Thm.symmetric (fold apply cvs eq) |
|
333 |
||
334 |
fun replace_lambda cvs ct (cx as (ctxt, defs)) = |
|
335 |
let |
|
336 |
val cvs' = used_vars cvs ct |
|
337 |
val ct' = fold_rev Thm.cabs cvs' ct |
|
338 |
in |
|
339 |
(case Termtab.lookup defs (Thm.term_of ct') of |
|
340 |
SOME eq => (apply_def cvs' eq, cx) |
|
341 |
| NONE => |
|
342 |
let |
|
343 |
val {T, ...} = Thm.rep_cterm ct' and n = Name.uu |
|
344 |
val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt |
|
40663 | 345 |
val cu = U.mk_cequals (U.certify ctxt (Free (n', T))) ct' |
36898 | 346 |
val (eq, ctxt'') = yield_singleton Assumption.add_assumes cu ctxt' |
347 |
val defs' = Termtab.update (Thm.term_of ct', eq) defs |
|
348 |
in (apply_def cvs' eq, (ctxt'', defs')) end) |
|
349 |
end |
|
350 |
||
351 |
fun none ct cx = (Thm.reflexive ct, cx) |
|
352 |
fun in_comb f g ct cx = |
|
353 |
let val (cu1, cu2) = Thm.dest_comb ct |
|
354 |
in cx |> f cu1 ||>> g cu2 |>> uncurry Thm.combination end |
|
355 |
fun in_arg f = in_comb none f |
|
356 |
fun in_abs f cvs ct (ctxt, defs) = |
|
357 |
let |
|
358 |
val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt |
|
359 |
val (cv, cu) = Thm.dest_abs (SOME n) ct |
|
360 |
in (ctxt', defs) |> f (cv :: cvs) cu |>> Thm.abstract_rule n cv end |
|
361 |
||
362 |
fun traverse cvs ct = |
|
363 |
(case Thm.term_of ct of |
|
364 |
Const (@{const_name All}, _) $ Abs _ => in_arg (in_abs traverse cvs) |
|
365 |
| Const (@{const_name Ex}, _) $ Abs _ => in_arg (in_abs traverse cvs) |
|
366 |
| Const (@{const_name Let}, _) $ _ $ Abs _ => |
|
367 |
in_comb (in_arg (traverse cvs)) (in_abs traverse cvs) |
|
368 |
| Abs _ => at_lambda cvs |
|
369 |
| _ $ _ => in_comb (traverse cvs) (traverse cvs) |
|
370 |
| _ => none) ct |
|
371 |
||
372 |
and at_lambda cvs ct = |
|
373 |
in_abs traverse cvs ct #-> (fn thm => |
|
374 |
replace_lambda cvs (Thm.rhs_of thm) #>> Thm.transitive thm) |
|
375 |
||
376 |
fun has_free_lambdas t = |
|
377 |
(case t of |
|
378 |
Const (@{const_name All}, _) $ Abs (_, _, u) => has_free_lambdas u |
|
379 |
| Const (@{const_name Ex}, _) $ Abs (_, _, u) => has_free_lambdas u |
|
380 |
| Const (@{const_name Let}, _) $ u1 $ Abs (_, _, u2) => |
|
381 |
has_free_lambdas u1 orelse has_free_lambdas u2 |
|
382 |
| Abs _ => true |
|
383 |
| u1 $ u2 => has_free_lambdas u1 orelse has_free_lambdas u2 |
|
384 |
| _ => false) |
|
385 |
||
386 |
fun lift_lm f thm cx = |
|
387 |
if not (has_free_lambdas (Thm.prop_of thm)) then (thm, cx) |
|
388 |
else cx |> f (Thm.cprop_of thm) |>> (fn thm' => Thm.equal_elim thm' thm) |
|
389 |
in |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
390 |
fun lift_lambdas irules ctxt = |
36898 | 391 |
let |
392 |
val cx = (ctxt, Termtab.empty) |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
393 |
val (idxs, thms) = split_list irules |
36898 | 394 |
val (thms', (ctxt', defs)) = fold_map (lift_lm (traverse [])) thms cx |
395 |
val eqs = Termtab.fold (cons o normalize_rule ctxt' o snd) defs [] |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
396 |
in (map (pair ~1) eqs @ (idxs ~~ thms'), ctxt') end |
36898 | 397 |
end |
398 |
||
399 |
||
400 |
||
401 |
(* make application explicit for functions with varying number of arguments *) |
|
402 |
||
403 |
local |
|
404 |
val const = prefix "c" and free = prefix "f" |
|
405 |
fun min i (e as (_, j)) = if i <> j then (true, Int.min (i, j)) else e |
|
406 |
fun add t i = Symtab.map_default (t, (false, i)) (min i) |
|
407 |
fun traverse t = |
|
408 |
(case Term.strip_comb t of |
|
409 |
(Const (n, _), ts) => add (const n) (length ts) #> fold traverse ts |
|
410 |
| (Free (n, _), ts) => add (free n) (length ts) #> fold traverse ts |
|
411 |
| (Abs (_, _, u), ts) => fold traverse (u :: ts) |
|
412 |
| (_, ts) => fold traverse ts) |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
413 |
fun prune tab = Symtab.fold (fn (n, (true, i)) => |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
414 |
Symtab.update (n, i) | _ => I) tab Symtab.empty |
36898 | 415 |
|
416 |
fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 |
|
417 |
fun nary_conv conv1 conv2 ct = |
|
418 |
(Conv.combination_conv (nary_conv conv1 conv2) conv2 else_conv conv1) ct |
|
419 |
fun abs_conv conv tb = Conv.abs_conv (fn (cv, cx) => |
|
420 |
let val n = fst (Term.dest_Free (Thm.term_of cv)) |
|
421 |
in conv (Symtab.update (free n, 0) tb) cx end) |
|
37153
8feed34275ce
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents:
36936
diff
changeset
|
422 |
val fun_app_rule = @{lemma "f x == fun_app f x" by (simp add: fun_app_def)} |
36898 | 423 |
in |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
424 |
fun explicit_application ctxt irules = |
36898 | 425 |
let |
426 |
fun sub_conv tb ctxt ct = |
|
427 |
(case Term.strip_comb (Thm.term_of ct) of |
|
428 |
(Const (n, _), ts) => app_conv tb (const n) (length ts) ctxt |
|
429 |
| (Free (n, _), ts) => app_conv tb (free n) (length ts) ctxt |
|
430 |
| (Abs _, _) => nary_conv (abs_conv sub_conv tb ctxt) (sub_conv tb ctxt) |
|
431 |
| (_, _) => nary_conv Conv.all_conv (sub_conv tb ctxt)) ct |
|
432 |
and app_conv tb n i ctxt = |
|
433 |
(case Symtab.lookup tb n of |
|
434 |
NONE => nary_conv Conv.all_conv (sub_conv tb ctxt) |
|
37153
8feed34275ce
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents:
36936
diff
changeset
|
435 |
| SOME j => fun_app_conv tb ctxt (i - j)) |
8feed34275ce
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents:
36936
diff
changeset
|
436 |
and fun_app_conv tb ctxt i ct = ( |
36898 | 437 |
if i = 0 then nary_conv Conv.all_conv (sub_conv tb ctxt) |
438 |
else |
|
37153
8feed34275ce
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents:
36936
diff
changeset
|
439 |
Conv.rewr_conv fun_app_rule then_conv |
8feed34275ce
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents:
36936
diff
changeset
|
440 |
binop_conv (fun_app_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct |
36898 | 441 |
|
442 |
fun needs_exp_app tab = Term.exists_subterm (fn |
|
443 |
Bound _ $ _ => true |
|
444 |
| Const (n, _) => Symtab.defined tab (const n) |
|
445 |
| Free (n, _) => Symtab.defined tab (free n) |
|
446 |
| _ => false) |
|
447 |
||
448 |
fun rewrite tab ctxt thm = |
|
449 |
if not (needs_exp_app tab (Thm.prop_of thm)) then thm |
|
450 |
else Conv.fconv_rule (sub_conv tab ctxt) thm |
|
451 |
||
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
452 |
val tab = prune (fold (traverse o Thm.prop_of o snd) irules Symtab.empty) |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
453 |
in map (apsnd (rewrite tab ctxt)) irules end |
36898 | 454 |
end |
455 |
||
456 |
||
457 |
||
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
|
458 |
(* add missing datatype selectors via hypothetical definitions *) |
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
|
459 |
|
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
|
460 |
local |
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
|
461 |
val add = (fn Type (n, _) => Symtab.update (n, ()) | _ => I) |
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
|
462 |
|
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
|
463 |
fun collect t = |
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
|
464 |
(case Term.strip_comb t of |
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
|
465 |
(Abs (_, T, t), _) => add T #> collect t |
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
|
466 |
| (Const (_, T), ts) => collects T ts |
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
|
467 |
| (Free (_, T), ts) => collects T ts |
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
|
468 |
| _ => I) |
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
|
469 |
and collects T ts = |
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
|
470 |
let val ((Ts, Us), U) = Term.strip_type T |> apfst (chop (length ts)) |
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
|
471 |
in fold add Ts #> add (Us ---> U) #> fold collect ts 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
|
472 |
|
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
|
473 |
fun add_constructors thy n = |
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
|
474 |
(case Datatype.get_info thy n of |
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
|
475 |
NONE => I |
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
|
476 |
| SOME {descr, ...} => fold (fn (_, (_, _, cs)) => fold (fn (n, ds) => |
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
|
477 |
fold (insert (op =) o pair n) (1 upto length ds)) cs) descr) |
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
|
478 |
|
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
|
479 |
fun add_selector (c as (n, i)) ctxt = |
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
|
480 |
(case Datatype_Selectors.lookup_selector ctxt c of |
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
|
481 |
SOME _ => ctxt |
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
|
482 |
| NONE => |
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
|
483 |
let |
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
|
484 |
val T = Sign.the_const_type (ProofContext.theory_of ctxt) n |
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
|
485 |
val U = Term.body_type T --> nth (Term.binder_types T) (i-1) |
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
|
486 |
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
|
487 |
ctxt |
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
|
488 |
|> yield_singleton Variable.variant_fixes Name.uu |
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
|
489 |
|>> pair ((n, T), i) o rpair U |
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
|
490 |
|-> Context.proof_map o Datatype_Selectors.add_selector |
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
|
491 |
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
|
492 |
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
|
493 |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
494 |
fun datatype_selectors irules ctxt = |
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
|
495 |
let |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
496 |
val ns = Symtab.keys (fold (collect o Thm.prop_of o snd) irules Symtab.empty) |
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
|
497 |
val cs = fold (add_constructors (ProofContext.theory_of ctxt)) ns [] |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
498 |
in (irules, fold add_selector cs 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
|
499 |
(* FIXME: also generate hypothetical definitions for the selectors *) |
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
|
500 |
|
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
|
501 |
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
|
502 |
|
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
|
503 |
|
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
|
504 |
|
36898 | 505 |
(* combined normalization *) |
506 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
507 |
type extra_norm = bool -> (int * thm) list -> Proof.context -> |
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
508 |
(int * thm) list * Proof.context |
36898 | 509 |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39483
diff
changeset
|
510 |
fun with_context f irules ctxt = (f ctxt irules, ctxt) |
36898 | 511 |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40279
diff
changeset
|
512 |
fun normalize extra_norm with_datatypes irules ctxt = |
40278
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
513 |
let |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
514 |
fun norm f ctxt' (i, thm) = |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40279
diff
changeset
|
515 |
if Config.get ctxt' SMT_Config.drop_bad_facts then |
40278
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
516 |
(case try (f ctxt') thm of |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
517 |
SOME thm' => SOME (i, thm') |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40279
diff
changeset
|
518 |
| NONE => (SMT_Config.verbose_msg ctxt' (prefix ("Warning: " ^ |
40278
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
519 |
"dropping assumption: ") o Display.string_of_thm ctxt') thm; NONE)) |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40279
diff
changeset
|
520 |
else SOME (i, f ctxt' thm) |
40278
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
521 |
in |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
522 |
irules |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
523 |
|> trivial_distinct ctxt |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
524 |
|> rewrite_bool_cases ctxt |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
525 |
|> normalize_numerals ctxt |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
526 |
|> nat_as_int ctxt |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
527 |
|> rpair ctxt |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
528 |
|-> extra_norm with_datatypes |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
529 |
|-> with_context (map_filter o norm normalize_rule) |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
530 |
|-> SMT_Monomorph.monomorph |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
531 |
|-> lift_lambdas |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
532 |
|-> with_context explicit_application |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
533 |
|-> (if with_datatypes then datatype_selectors else pair) |
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40275
diff
changeset
|
534 |
end |
36898 | 535 |
|
536 |
end |