1 (* Title: HOL/SMT/Tools/z3_proof_tools.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Helper functions required for Z3 proof reconstruction. |
|
5 *) |
|
6 |
|
7 signature Z3_PROOF_TOOLS = |
|
8 sig |
|
9 (* accessing and modifying terms *) |
|
10 val term_of: cterm -> term |
|
11 val prop_of: thm -> term |
|
12 val mk_prop: cterm -> cterm |
|
13 val as_meta_eq: cterm -> cterm |
|
14 |
|
15 (* theorem nets *) |
|
16 val thm_net_of: thm list -> thm Net.net |
|
17 val net_instance: thm Net.net -> cterm -> thm option |
|
18 |
|
19 (* proof combinators *) |
|
20 val under_assumption: (thm -> thm) -> cterm -> thm |
|
21 val with_conv: conv -> (cterm -> thm) -> cterm -> thm |
|
22 val discharge: thm -> thm -> thm |
|
23 val varify: string list -> thm -> thm |
|
24 val unfold_eqs: Proof.context -> thm list -> conv |
|
25 val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm |
|
26 val by_tac: (int -> tactic) -> cterm -> thm |
|
27 val make_hyp_def: thm -> Proof.context -> thm * Proof.context |
|
28 val by_abstraction: Proof.context -> thm list -> (Proof.context -> cterm -> |
|
29 thm) -> cterm -> thm |
|
30 |
|
31 (* a faster COMP *) |
|
32 type compose_data |
|
33 val precompose: (cterm -> cterm list) -> thm -> compose_data |
|
34 val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data |
|
35 val compose: compose_data -> thm -> thm |
|
36 |
|
37 (* unfolding of 'distinct' *) |
|
38 val unfold_distinct_conv: conv |
|
39 |
|
40 (* simpset *) |
|
41 val make_simpset: Proof.context -> thm list -> simpset |
|
42 end |
|
43 |
|
44 structure Z3_Proof_Tools: Z3_PROOF_TOOLS = |
|
45 struct |
|
46 |
|
47 |
|
48 |
|
49 (* accessing terms *) |
|
50 |
|
51 val dest_prop = (fn @{term Trueprop} $ t => t | t => t) |
|
52 |
|
53 fun term_of ct = dest_prop (Thm.term_of ct) |
|
54 fun prop_of thm = dest_prop (Thm.prop_of thm) |
|
55 |
|
56 val mk_prop = Thm.capply @{cterm Trueprop} |
|
57 |
|
58 val (eqT, eq) = `(hd o Thm.dest_ctyp o Thm.ctyp_of_term) @{cpat "op =="} |
|
59 fun mk_meta_eq_cterm ct cu = |
|
60 let val inst = ([(eqT, Thm.ctyp_of_term ct)], []) |
|
61 in Thm.mk_binop (Thm.instantiate_cterm inst eq) ct cu end |
|
62 |
|
63 fun as_meta_eq ct = uncurry mk_meta_eq_cterm (Thm.dest_binop (Thm.dest_arg ct)) |
|
64 |
|
65 |
|
66 |
|
67 (* theorem nets *) |
|
68 |
|
69 fun thm_net_of thms = |
|
70 let fun insert thm = Net.insert_term (K false) (Thm.prop_of thm, thm) |
|
71 in fold insert thms Net.empty end |
|
72 |
|
73 fun maybe_instantiate ct thm = |
|
74 try Thm.first_order_match (Thm.cprop_of thm, ct) |
|
75 |> Option.map (fn inst => Thm.instantiate inst thm) |
|
76 |
|
77 fun first_of thms ct = get_first (maybe_instantiate ct) thms |
|
78 fun net_instance net ct = first_of (Net.match_term net (Thm.term_of ct)) ct |
|
79 |
|
80 |
|
81 |
|
82 (* proof combinators *) |
|
83 |
|
84 fun under_assumption f ct = |
|
85 let val ct' = mk_prop ct |
|
86 in Thm.implies_intr ct' (f (Thm.assume ct')) end |
|
87 |
|
88 fun with_conv conv prove ct = |
|
89 let val eq = Thm.symmetric (conv ct) |
|
90 in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end |
|
91 |
|
92 fun discharge p pq = Thm.implies_elim pq p |
|
93 |
|
94 fun varify vars = Drule.generalize ([], vars) |
|
95 |
|
96 fun unfold_eqs _ [] = Conv.all_conv |
|
97 | unfold_eqs ctxt eqs = |
|
98 More_Conv.top_sweep_conv (K (More_Conv.rewrs_conv eqs)) ctxt |
|
99 |
|
100 fun match_instantiate f ct thm = |
|
101 Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm |
|
102 |
|
103 fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1))) |
|
104 |
|
105 (* |- c x == t x ==> P (c x) ~~> c == t |- P (c x) *) |
|
106 fun make_hyp_def thm ctxt = |
|
107 let |
|
108 val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1) |
|
109 val (cf, cvs) = Drule.strip_comb lhs |
|
110 val eq = mk_meta_eq_cterm cf (fold_rev Thm.cabs cvs rhs) |
|
111 fun apply cv th = |
|
112 Thm.combination th (Thm.reflexive cv) |
|
113 |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false)) |
|
114 in |
|
115 yield_singleton Assumption.add_assumes eq ctxt |
|
116 |>> Thm.implies_elim thm o fold apply cvs |
|
117 end |
|
118 |
|
119 |
|
120 |
|
121 (* abstraction *) |
|
122 |
|
123 local |
|
124 |
|
125 fun typ_of ct = #T (Thm.rep_cterm ct) |
|
126 fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) |
|
127 |
|
128 fun abs_context ctxt = (ctxt, Termtab.empty, 1, false) |
|
129 |
|
130 fun context_of (ctxt, _, _, _) = ctxt |
|
131 |
|
132 fun replace (cv, ct) = Thm.forall_elim ct o Thm.forall_intr cv |
|
133 |
|
134 fun abs_instantiate (_, tab, _, beta_norm) = |
|
135 fold replace (map snd (Termtab.dest tab)) #> |
|
136 beta_norm ? Conv.fconv_rule (Thm.beta_conversion true) |
|
137 |
|
138 fun generalize cvs = |
|
139 let |
|
140 val no_name = "" |
|
141 |
|
142 fun dest (Free (n, _)) = n |
|
143 | dest _ = no_name |
|
144 |
|
145 fun gen vs (t as Free (n, _)) = |
|
146 let val i = find_index (equal n) vs |
|
147 in |
|
148 if i >= 0 then insert (op aconvc) (nth cvs i) #> pair (Bound i) |
|
149 else pair t |
|
150 end |
|
151 | gen vs (t $ u) = gen vs t ##>> gen vs u #>> (op $) |
|
152 | gen vs (Abs (n, T, t)) = |
|
153 gen (no_name :: vs) t #>> (fn u => Abs (n, T, u)) |
|
154 | gen _ t = pair t |
|
155 |
|
156 in (fn ct => gen (map (dest o Thm.term_of) cvs) (Thm.term_of ct) []) end |
|
157 |
|
158 fun fresh_abstraction cvs ct (cx as (ctxt, tab, idx, beta_norm)) = |
|
159 let val (t, cvs') = generalize cvs ct |
|
160 in |
|
161 (case Termtab.lookup tab t of |
|
162 SOME (cv, _) => (cv, cx) |
|
163 | NONE => |
|
164 let |
|
165 val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt |
|
166 val cv = certify ctxt (Free (n, map typ_of cvs' ---> typ_of ct)) |
|
167 val cv' = Drule.list_comb (cv, cvs') |
|
168 val e = (t, (cv, fold_rev Thm.cabs cvs' ct)) |
|
169 val beta_norm' = beta_norm orelse not (null cvs') |
|
170 in (cv', (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end) |
|
171 end |
|
172 |
|
173 fun abs_arg f cvs ct = |
|
174 let val (cf, cu) = Thm.dest_comb ct |
|
175 in f cvs cu #>> Thm.capply cf end |
|
176 |
|
177 fun abs_comb f g cvs ct = |
|
178 let val (cf, cu) = Thm.dest_comb ct |
|
179 in f cvs cf ##>> g cvs cu #>> uncurry Thm.capply end |
|
180 |
|
181 fun abs_list f g cvs ct = |
|
182 (case Thm.term_of ct of |
|
183 Const (@{const_name Nil}, _) => pair ct |
|
184 | Const (@{const_name Cons}, _) $ _ $ _ => |
|
185 abs_comb (abs_arg f) (abs_list f g) cvs ct |
|
186 | _ => g cvs ct) |
|
187 |
|
188 fun abs_abs f cvs ct = |
|
189 let val (cv, cu) = Thm.dest_abs NONE ct |
|
190 in f (cv :: cvs) cu #>> Thm.cabs cv end |
|
191 |
|
192 val is_atomic = (fn _ $ _ => false | Abs _ => false | _ => true) |
|
193 val is_arithT = (fn @{typ int} => true | @{typ real} => true | _ => false) |
|
194 fun is_number t = |
|
195 (case try HOLogic.dest_number t of |
|
196 SOME (T, _) => is_arithT T |
|
197 | NONE => false) |
|
198 |
|
199 val abstract = |
|
200 let (* FIXME: provide an option to avoid abstraction of If/distinct/All/Ex *) |
|
201 fun abstr1 cvs ct = abs_arg abstr cvs ct |
|
202 and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct |
|
203 and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct |
|
204 and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct |
|
205 |
|
206 and abstr cvs ct = |
|
207 (case Thm.term_of ct of |
|
208 @{term Trueprop} $ _ => abstr1 cvs ct |
|
209 | @{term "op ==>"} $ _ $ _ => abstr2 cvs ct |
|
210 | @{term True} => pair ct |
|
211 | @{term False} => pair ct |
|
212 | @{term Not} $ _ => abstr1 cvs ct |
|
213 | @{term "op &"} $ _ $ _ => abstr2 cvs ct |
|
214 | @{term "op |"} $ _ $ _ => abstr2 cvs ct |
|
215 | @{term "op -->"} $ _ $ _ => abstr2 cvs ct |
|
216 | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct |
|
217 | Const (@{const_name distinct}, _) $ _ => |
|
218 abs_arg (abs_list abstr fresh_abstraction) cvs ct |
|
219 | Const (@{const_name If}, _) $ _ $ _ $ _ => abstr3 cvs ct |
|
220 | Const (@{const_name All}, _) $ _ => abstr_abs cvs ct |
|
221 | Const (@{const_name Ex}, _) $ _ => abstr_abs cvs ct |
|
222 | @{term "uminus :: int => _"} $ _ => abstr1 cvs ct |
|
223 | @{term "uminus :: real => _"} $ _ => abstr1 cvs ct |
|
224 | @{term "op + :: int => _"} $ _ $ _ => abstr2 cvs ct |
|
225 | @{term "op + :: real => _"} $ _ $ _ => abstr2 cvs ct |
|
226 | @{term "op - :: int => _"} $ _ $ _ => abstr2 cvs ct |
|
227 | @{term "op - :: real => _"} $ _ $ _ => abstr2 cvs ct |
|
228 | @{term "op * :: int => _"} $ _ $ _ => abstr2 cvs ct |
|
229 | @{term "op * :: real => _"} $ _ $ _ => abstr2 cvs ct |
|
230 | @{term "op div :: int => _"} $ _ $ _ => abstr2 cvs ct |
|
231 | @{term "op mod :: int => _"} $ _ $ _ => abstr2 cvs ct |
|
232 | @{term "op / :: real => _"} $ _ $ _ => abstr2 cvs ct |
|
233 | @{term "op < :: int => _"} $ _ $ _ => abstr2 cvs ct |
|
234 | @{term "op < :: real => _"} $ _ $ _ => abstr2 cvs ct |
|
235 | @{term "op <= :: int => _"} $ _ $ _ => abstr2 cvs ct |
|
236 | @{term "op <= :: real => _"} $ _ $ _ => abstr2 cvs ct |
|
237 | Const (@{const_name apply}, _) $ _ $ _ => abstr2 cvs ct |
|
238 | Const (@{const_name fun_upd}, _) $ _ $ _ $ _ => abstr3 cvs ct |
|
239 | t => |
|
240 if is_atomic t orelse is_number t then pair ct |
|
241 else fresh_abstraction cvs ct) |
|
242 in abstr [] end |
|
243 |
|
244 fun with_prems thms f ct = |
|
245 fold_rev (Thm.mk_binop @{cterm "op ==>"} o Thm.cprop_of) thms ct |
|
246 |> f |
|
247 |> fold (fn prem => fn th => Thm.implies_elim th prem) thms |
|
248 |
|
249 in |
|
250 |
|
251 fun by_abstraction ctxt thms prove = with_prems thms (fn ct => |
|
252 let val (cu, cx) = abstract ct (abs_context ctxt) |
|
253 in abs_instantiate cx (prove (context_of cx) cu) end) |
|
254 |
|
255 end |
|
256 |
|
257 |
|
258 |
|
259 (* a faster COMP *) |
|
260 |
|
261 type compose_data = cterm list * (cterm -> cterm list) * thm |
|
262 |
|
263 fun list2 (x, y) = [x, y] |
|
264 |
|
265 fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule) |
|
266 fun precompose2 f rule = precompose (list2 o f) rule |
|
267 |
|
268 fun compose (cvs, f, rule) thm = |
|
269 discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule) |
|
270 |
|
271 |
|
272 |
|
273 (* unfolding of 'distinct' *) |
|
274 |
|
275 local |
|
276 val set1 = @{lemma "x ~: set [] == ~False" by simp} |
|
277 val set2 = @{lemma "x ~: set [x] == False" by simp} |
|
278 val set3 = @{lemma "x ~: set [y] == x ~= y" by simp} |
|
279 val set4 = @{lemma "x ~: set (x # ys) == False" by simp} |
|
280 val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp} |
|
281 |
|
282 fun set_conv ct = |
|
283 (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv |
|
284 (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct |
|
285 |
|
286 val dist1 = @{lemma "distinct [] == ~False" by simp} |
|
287 val dist2 = @{lemma "distinct [x] == ~False" by simp} |
|
288 val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs" |
|
289 by simp} |
|
290 |
|
291 fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 |
|
292 in |
|
293 fun unfold_distinct_conv ct = |
|
294 (More_Conv.rewrs_conv [dist1, dist2] else_conv |
|
295 (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct |
|
296 end |
|
297 |
|
298 |
|
299 |
|
300 (* simpset *) |
|
301 |
|
302 local |
|
303 val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv} |
|
304 val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2} |
|
305 val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1} |
|
306 val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3} |
|
307 |
|
308 fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm |
|
309 fun dest_binop ((c as Const _) $ t $ u) = (c, t, u) |
|
310 | dest_binop t = raise TERM ("dest_binop", [t]) |
|
311 |
|
312 fun prove_antisym_le ss t = |
|
313 let |
|
314 val (le, r, s) = dest_binop t |
|
315 val less = Const (@{const_name less}, Term.fastype_of le) |
|
316 val prems = Simplifier.prems_of_ss ss |
|
317 in |
|
318 (case find_first (eq_prop (le $ s $ r)) prems of |
|
319 NONE => |
|
320 find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems |
|
321 |> Option.map (fn thm => thm RS antisym_less1) |
|
322 | SOME thm => SOME (thm RS antisym_le1)) |
|
323 end |
|
324 handle THM _ => NONE |
|
325 |
|
326 fun prove_antisym_less ss t = |
|
327 let |
|
328 val (less, r, s) = dest_binop (HOLogic.dest_not t) |
|
329 val le = Const (@{const_name less_eq}, Term.fastype_of less) |
|
330 val prems = prems_of_ss ss |
|
331 in |
|
332 (case find_first (eq_prop (le $ r $ s)) prems of |
|
333 NONE => |
|
334 find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems |
|
335 |> Option.map (fn thm => thm RS antisym_less2) |
|
336 | SOME thm => SOME (thm RS antisym_le2)) |
|
337 end |
|
338 handle THM _ => NONE |
|
339 in |
|
340 |
|
341 fun make_simpset ctxt rules = Simplifier.context ctxt (HOL_ss |
|
342 addsimps @{thms field_simps} |
|
343 addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}] |
|
344 addsimps @{thms arith_special} addsimps @{thms less_bin_simps} |
|
345 addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps} |
|
346 addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps} |
|
347 addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps} |
|
348 addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps} |
|
349 addsimps @{thms array_rules} |
|
350 addsimprocs [ |
|
351 Simplifier.simproc @{theory} "fast_int_arith" [ |
|
352 "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc), |
|
353 Simplifier.simproc @{theory} "fast_real_arith" [ |
|
354 "(m::real) < n", "(m::real) <= n", "(m::real) = n"] |
|
355 (K Lin_Arith.simproc), |
|
356 Simplifier.simproc @{theory} "antisym_le" ["(x::'a::order) <= y"] |
|
357 (K prove_antisym_le), |
|
358 Simplifier.simproc @{theory} "antisym_less" ["~ (x::'a::linorder) < y"] |
|
359 (K prove_antisym_less)] |
|
360 addsimps rules) |
|
361 |
|
362 end |
|
363 |
|
364 end |
|