1 (* Title: HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Proof reconstruction for proofs found by Z3. |
|
5 *) |
|
6 |
|
7 signature OLD_Z3_PROOF_RECONSTRUCTION = |
|
8 sig |
|
9 val add_z3_rule: thm -> Context.generic -> Context.generic |
|
10 val reconstruct: Proof.context -> Old_SMT_Translate.recon -> string list -> int list * thm |
|
11 end |
|
12 |
|
13 structure Old_Z3_Proof_Reconstruction: OLD_Z3_PROOF_RECONSTRUCTION = |
|
14 struct |
|
15 |
|
16 |
|
17 fun z3_exn msg = raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure |
|
18 ("Z3 proof reconstruction: " ^ msg)) |
|
19 |
|
20 |
|
21 |
|
22 (* net of schematic rules *) |
|
23 |
|
24 local |
|
25 val description = "declaration of Z3 proof rules" |
|
26 |
|
27 val eq = Thm.eq_thm |
|
28 |
|
29 structure Old_Z3_Rules = Generic_Data |
|
30 ( |
|
31 type T = thm Net.net |
|
32 val empty = Net.empty |
|
33 val extend = I |
|
34 val merge = Net.merge eq |
|
35 ) |
|
36 |
|
37 fun prep context = |
|
38 `Thm.prop_of o rewrite_rule (Context.proof_of context) [Old_Z3_Proof_Literals.rewrite_true] |
|
39 |
|
40 fun ins thm context = |
|
41 context |> Old_Z3_Rules.map (fn net => Net.insert_term eq (prep context thm) net handle Net.INSERT => net) |
|
42 fun rem thm context = |
|
43 context |> Old_Z3_Rules.map (fn net => Net.delete_term eq (prep context thm) net handle Net.DELETE => net) |
|
44 |
|
45 val add = Thm.declaration_attribute ins |
|
46 val del = Thm.declaration_attribute rem |
|
47 in |
|
48 |
|
49 val add_z3_rule = ins |
|
50 |
|
51 fun by_schematic_rule ctxt ct = |
|
52 the (Old_Z3_Proof_Tools.net_instance (Old_Z3_Rules.get (Context.Proof ctxt)) ct) |
|
53 |
|
54 val _ = Theory.setup |
|
55 (Attrib.setup @{binding old_z3_rule} (Attrib.add_del add del) description #> |
|
56 Global_Theory.add_thms_dynamic (@{binding old_z3_rule}, Net.content o Old_Z3_Rules.get)) |
|
57 |
|
58 end |
|
59 |
|
60 |
|
61 |
|
62 (* proof tools *) |
|
63 |
|
64 fun named ctxt name prover ct = |
|
65 let val _ = Old_SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") |
|
66 in prover ct end |
|
67 |
|
68 fun NAMED ctxt name tac i st = |
|
69 let val _ = Old_SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") |
|
70 in tac i st end |
|
71 |
|
72 fun pretty_goal ctxt thms t = |
|
73 [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]] |
|
74 |> not (null thms) ? cons (Pretty.big_list "assumptions:" |
|
75 (map (Thm.pretty_thm ctxt) thms)) |
|
76 |
|
77 fun try_apply ctxt thms = |
|
78 let |
|
79 fun try_apply_err ct = Pretty.string_of (Pretty.chunks [ |
|
80 Pretty.big_list ("Z3 found a proof," ^ |
|
81 " but proof reconstruction failed at the following subgoal:") |
|
82 (pretty_goal ctxt thms (Thm.term_of ct)), |
|
83 Pretty.str ("Declaring a rule as [old_z3_rule] might solve this problem.")]) |
|
84 |
|
85 fun apply [] ct = error (try_apply_err ct) |
|
86 | apply (prover :: provers) ct = |
|
87 (case try prover ct of |
|
88 SOME thm => (Old_SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm) |
|
89 | NONE => apply provers ct) |
|
90 |
|
91 fun schematic_label full = "schematic rules" |> full ? suffix " (full)" |
|
92 fun schematic ctxt full ct = |
|
93 ct |
|
94 |> full ? fold_rev (curry Drule.mk_implies o Thm.cprop_of) thms |
|
95 |> named ctxt (schematic_label full) (by_schematic_rule ctxt) |
|
96 |> fold Thm.elim_implies thms |
|
97 |
|
98 in apply o cons (schematic ctxt false) o cons (schematic ctxt true) end |
|
99 |
|
100 local |
|
101 val rewr_if = |
|
102 @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp} |
|
103 in |
|
104 |
|
105 fun HOL_fast_tac ctxt = |
|
106 Classical.fast_tac (put_claset HOL_cs ctxt) |
|
107 |
|
108 fun simp_fast_tac ctxt = |
|
109 Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [rewr_if]) |
|
110 THEN_ALL_NEW HOL_fast_tac ctxt |
|
111 |
|
112 end |
|
113 |
|
114 |
|
115 |
|
116 (* theorems and proofs *) |
|
117 |
|
118 (** theorem incarnations **) |
|
119 |
|
120 datatype theorem = |
|
121 Thm of thm | (* theorem without special features *) |
|
122 MetaEq of thm | (* meta equality "t == s" *) |
|
123 Literals of thm * Old_Z3_Proof_Literals.littab |
|
124 (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *) |
|
125 |
|
126 fun thm_of (Thm thm) = thm |
|
127 | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq} |
|
128 | thm_of (Literals (thm, _)) = thm |
|
129 |
|
130 fun meta_eq_of (MetaEq thm) = thm |
|
131 | meta_eq_of p = mk_meta_eq (thm_of p) |
|
132 |
|
133 fun literals_of (Literals (_, lits)) = lits |
|
134 | literals_of p = Old_Z3_Proof_Literals.make_littab [thm_of p] |
|
135 |
|
136 |
|
137 |
|
138 (** core proof rules **) |
|
139 |
|
140 (* assumption *) |
|
141 |
|
142 local |
|
143 val remove_trigger = mk_meta_eq @{thm trigger_def} |
|
144 val remove_weight = mk_meta_eq @{thm weight_def} |
|
145 val remove_fun_app = mk_meta_eq @{thm fun_app_def} |
|
146 |
|
147 fun rewrite_conv _ [] = Conv.all_conv |
|
148 | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs) |
|
149 |
|
150 val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight, |
|
151 remove_fun_app, Old_Z3_Proof_Literals.rewrite_true] |
|
152 |
|
153 fun rewrite _ [] = I |
|
154 | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs) |
|
155 |
|
156 fun lookup_assm assms_net ct = |
|
157 Old_Z3_Proof_Tools.net_instances assms_net ct |
|
158 |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct)) |
|
159 in |
|
160 |
|
161 fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt = |
|
162 let |
|
163 val eqs = map (rewrite ctxt [Old_Z3_Proof_Literals.rewrite_true]) rewrite_rules |
|
164 val eqs' = union Thm.eq_thm eqs prep_rules |
|
165 |
|
166 val assms_net = |
|
167 assms |
|
168 |> map (apsnd (rewrite ctxt eqs')) |
|
169 |> map (apsnd (Conv.fconv_rule Thm.eta_conversion)) |
|
170 |> Old_Z3_Proof_Tools.thm_net_of snd |
|
171 |
|
172 fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion |
|
173 |
|
174 fun assume thm ctxt = |
|
175 let |
|
176 val ct = Thm.cprem_of thm 1 |
|
177 val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt |
|
178 in (Thm.implies_elim thm thm', ctxt') end |
|
179 |
|
180 fun add1 idx thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) = |
|
181 let |
|
182 val (thm, ctxt') = |
|
183 if exact then (Thm.implies_elim thm1 th, ctxt) |
|
184 else assume thm1 ctxt |
|
185 val thms' = if exact then thms else th :: thms |
|
186 in |
|
187 ((insert (op =) i is, thms'), |
|
188 (ctxt', Inttab.update (idx, Thm thm) ptab)) |
|
189 end |
|
190 |
|
191 fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) = |
|
192 let |
|
193 val thm1 = |
|
194 Thm.trivial ct |
|
195 |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt)) |
|
196 val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1 |
|
197 in |
|
198 (case lookup_assm assms_net (Thm.cprem_of thm2 1) of |
|
199 [] => |
|
200 let val (thm, ctxt') = assume thm1 ctxt |
|
201 in ((is, thms), (ctxt', Inttab.update (idx, Thm thm) ptab)) end |
|
202 | ithms => fold (add1 idx thm1) ithms cx) |
|
203 end |
|
204 in fold add asserted (([], []), (ctxt, Inttab.empty)) end |
|
205 |
|
206 end |
|
207 |
|
208 |
|
209 (* P = Q ==> P ==> Q or P --> Q ==> P ==> Q *) |
|
210 local |
|
211 val precomp = Old_Z3_Proof_Tools.precompose2 |
|
212 val comp = Old_Z3_Proof_Tools.compose |
|
213 |
|
214 val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp} |
|
215 val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1 |
|
216 |
|
217 val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1} |
|
218 val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp} |
|
219 in |
|
220 fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p) |
|
221 | mp p_q p = |
|
222 let |
|
223 val pq = thm_of p_q |
|
224 val thm = comp iffD1_c pq handle THM _ => comp mp_c pq |
|
225 in Thm (Thm.implies_elim thm p) end |
|
226 end |
|
227 |
|
228 |
|
229 (* and_elim: P1 & ... & Pn ==> Pi *) |
|
230 (* not_or_elim: ~(P1 | ... | Pn) ==> ~Pi *) |
|
231 local |
|
232 fun is_sublit conj t = Old_Z3_Proof_Literals.exists_lit conj (fn u => u aconv t) |
|
233 |
|
234 fun derive conj t lits idx ptab = |
|
235 let |
|
236 val lit = the (Old_Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits) |
|
237 val ls = Old_Z3_Proof_Literals.explode conj false false [t] lit |
|
238 val lits' = fold Old_Z3_Proof_Literals.insert_lit ls |
|
239 (Old_Z3_Proof_Literals.delete_lit lit lits) |
|
240 |
|
241 fun upd thm = Literals (thm_of thm, lits') |
|
242 val ptab' = Inttab.map_entry idx upd ptab |
|
243 in (the (Old_Z3_Proof_Literals.lookup_lit lits' t), ptab') end |
|
244 |
|
245 fun lit_elim conj (p, idx) ct ptab = |
|
246 let val lits = literals_of p |
|
247 in |
|
248 (case Old_Z3_Proof_Literals.lookup_lit lits (Old_SMT_Utils.term_of ct) of |
|
249 SOME lit => (Thm lit, ptab) |
|
250 | NONE => apfst Thm (derive conj (Old_SMT_Utils.term_of ct) lits idx ptab)) |
|
251 end |
|
252 in |
|
253 val and_elim = lit_elim true |
|
254 val not_or_elim = lit_elim false |
|
255 end |
|
256 |
|
257 |
|
258 (* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *) |
|
259 local |
|
260 fun step lit thm = |
|
261 Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit |
|
262 val explode_disj = Old_Z3_Proof_Literals.explode false false false |
|
263 fun intro hyps thm th = fold step (explode_disj hyps th) thm |
|
264 |
|
265 fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))] |
|
266 val ccontr = Old_Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr} |
|
267 in |
|
268 fun lemma thm ct = |
|
269 let |
|
270 val cu = Old_Z3_Proof_Literals.negate (Thm.dest_arg ct) |
|
271 val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm) |
|
272 val th = Old_Z3_Proof_Tools.under_assumption (intro hyps thm) cu |
|
273 in Thm (Old_Z3_Proof_Tools.compose ccontr th) end |
|
274 end |
|
275 |
|
276 |
|
277 (* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *) |
|
278 local |
|
279 val explode_disj = Old_Z3_Proof_Literals.explode false true false |
|
280 val join_disj = Old_Z3_Proof_Literals.join false |
|
281 fun unit thm thms th = |
|
282 let |
|
283 val t = @{const Not} $ Old_SMT_Utils.prop_of thm |
|
284 val ts = map Old_SMT_Utils.prop_of thms |
|
285 in |
|
286 join_disj (Old_Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t |
|
287 end |
|
288 |
|
289 fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) |
|
290 fun dest ct = apply2 dest_arg2 (Thm.dest_binop ct) |
|
291 val contrapos = |
|
292 Old_Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast} |
|
293 in |
|
294 fun unit_resolution thm thms ct = |
|
295 Old_Z3_Proof_Literals.negate (Thm.dest_arg ct) |
|
296 |> Old_Z3_Proof_Tools.under_assumption (unit thm thms) |
|
297 |> Thm o Old_Z3_Proof_Tools.discharge thm o Old_Z3_Proof_Tools.compose contrapos |
|
298 end |
|
299 |
|
300 |
|
301 (* P ==> P == True or P ==> P == False *) |
|
302 local |
|
303 val iff1 = @{lemma "P ==> P == (~ False)" by simp} |
|
304 val iff2 = @{lemma "~P ==> P == False" by simp} |
|
305 in |
|
306 fun iff_true thm = MetaEq (thm COMP iff1) |
|
307 fun iff_false thm = MetaEq (thm COMP iff2) |
|
308 end |
|
309 |
|
310 |
|
311 (* distributivity of | over & *) |
|
312 fun distributivity ctxt = Thm o try_apply ctxt [] [ |
|
313 named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] |
|
314 (* FIXME: not very well tested *) |
|
315 |
|
316 |
|
317 (* Tseitin-like axioms *) |
|
318 local |
|
319 val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast} |
|
320 val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast} |
|
321 val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast} |
|
322 val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast} |
|
323 |
|
324 fun prove' conj1 conj2 ct2 thm = |
|
325 let |
|
326 val littab = |
|
327 Old_Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm |
|
328 |> cons Old_Z3_Proof_Literals.true_thm |
|
329 |> Old_Z3_Proof_Literals.make_littab |
|
330 in Old_Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end |
|
331 |
|
332 fun prove rule (ct1, conj1) (ct2, conj2) = |
|
333 Old_Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule |
|
334 |
|
335 fun prove_def_axiom ct = |
|
336 let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct) |
|
337 in |
|
338 (case Thm.term_of ct1 of |
|
339 @{const Not} $ (@{const HOL.conj} $ _ $ _) => |
|
340 prove disjI1 (Thm.dest_arg ct1, true) (ct2, true) |
|
341 | @{const HOL.conj} $ _ $ _ => |
|
342 prove disjI3 (Old_Z3_Proof_Literals.negate ct2, false) (ct1, true) |
|
343 | @{const Not} $ (@{const HOL.disj} $ _ $ _) => |
|
344 prove disjI3 (Old_Z3_Proof_Literals.negate ct2, false) (ct1, false) |
|
345 | @{const HOL.disj} $ _ $ _ => |
|
346 prove disjI2 (Old_Z3_Proof_Literals.negate ct1, false) (ct2, true) |
|
347 | Const (@{const_name distinct}, _) $ _ => |
|
348 let |
|
349 fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv) |
|
350 val unfold_dis_conv = dis_conv Old_Z3_Proof_Tools.unfold_distinct_conv |
|
351 fun prv cu = |
|
352 let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) |
|
353 in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end |
|
354 in Old_Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end |
|
355 | @{const Not} $ (Const (@{const_name distinct}, _) $ _) => |
|
356 let |
|
357 fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv)) |
|
358 val unfold_dis_conv = dis_conv Old_Z3_Proof_Tools.unfold_distinct_conv |
|
359 fun prv cu = |
|
360 let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) |
|
361 in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end |
|
362 in Old_Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end |
|
363 | _ => raise CTERM ("prove_def_axiom", [ct])) |
|
364 end |
|
365 in |
|
366 fun def_axiom ctxt = Thm o try_apply ctxt [] [ |
|
367 named ctxt "conj/disj/distinct" prove_def_axiom, |
|
368 Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => |
|
369 named ctxt' "simp+fast" (Old_Z3_Proof_Tools.by_tac ctxt (simp_fast_tac ctxt')))] |
|
370 end |
|
371 |
|
372 |
|
373 (* local definitions *) |
|
374 local |
|
375 val intro_rules = [ |
|
376 @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp}, |
|
377 @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)" |
|
378 by simp}, |
|
379 @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ] |
|
380 |
|
381 val apply_rules = [ |
|
382 @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast}, |
|
383 @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n" |
|
384 by (atomize(full)) fastforce} ] |
|
385 |
|
386 val inst_rule = Old_Z3_Proof_Tools.match_instantiate Thm.dest_arg |
|
387 |
|
388 fun apply_rule ct = |
|
389 (case get_first (try (inst_rule ct)) intro_rules of |
|
390 SOME thm => thm |
|
391 | NONE => raise CTERM ("intro_def", [ct])) |
|
392 in |
|
393 fun intro_def ct = Old_Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm |
|
394 |
|
395 fun apply_def thm = |
|
396 get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules |
|
397 |> the_default (Thm thm) |
|
398 end |
|
399 |
|
400 |
|
401 (* negation normal form *) |
|
402 local |
|
403 val quant_rules1 = ([ |
|
404 @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp}, |
|
405 @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [ |
|
406 @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp}, |
|
407 @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}]) |
|
408 |
|
409 val quant_rules2 = ([ |
|
410 @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp}, |
|
411 @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [ |
|
412 @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp}, |
|
413 @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}]) |
|
414 |
|
415 fun nnf_quant_tac ctxt thm (qs as (qs1, qs2)) i st = ( |
|
416 resolve_tac ctxt [thm] ORELSE' |
|
417 (match_tac ctxt qs1 THEN' nnf_quant_tac ctxt thm qs) ORELSE' |
|
418 (match_tac ctxt qs2 THEN' nnf_quant_tac ctxt thm qs)) i st |
|
419 |
|
420 fun nnf_quant_tac_varified ctxt vars eq = |
|
421 nnf_quant_tac ctxt (Old_Z3_Proof_Tools.varify vars eq) |
|
422 |
|
423 fun nnf_quant ctxt vars qs p ct = |
|
424 Old_Z3_Proof_Tools.as_meta_eq ct |
|
425 |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified ctxt vars (meta_eq_of p) qs) |
|
426 |
|
427 fun prove_nnf ctxt = try_apply ctxt [] [ |
|
428 named ctxt "conj/disj" Old_Z3_Proof_Literals.prove_conj_disj_eq, |
|
429 Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => |
|
430 named ctxt' "simp+fast" (Old_Z3_Proof_Tools.by_tac ctxt' (simp_fast_tac ctxt')))] |
|
431 in |
|
432 fun nnf ctxt vars ps ct = |
|
433 (case Old_SMT_Utils.term_of ct of |
|
434 _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) => |
|
435 if l aconv r |
|
436 then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) |
|
437 else MetaEq (nnf_quant ctxt vars quant_rules1 (hd ps) ct) |
|
438 | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) => |
|
439 MetaEq (nnf_quant ctxt vars quant_rules2 (hd ps) ct) |
|
440 | _ => |
|
441 let |
|
442 val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv |
|
443 (Old_Z3_Proof_Tools.unfold_eqs ctxt |
|
444 (map (Thm.symmetric o meta_eq_of) ps))) |
|
445 in Thm (Old_Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end) |
|
446 end |
|
447 |
|
448 |
|
449 |
|
450 (** equality proof rules **) |
|
451 |
|
452 (* |- t = t *) |
|
453 fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) |
|
454 |
|
455 |
|
456 (* s = t ==> t = s *) |
|
457 local |
|
458 val symm_rule = @{lemma "s = t ==> t == s" by simp} |
|
459 in |
|
460 fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm) |
|
461 | symm p = MetaEq (thm_of p COMP symm_rule) |
|
462 end |
|
463 |
|
464 |
|
465 (* s = t ==> t = u ==> s = u *) |
|
466 local |
|
467 val trans1 = @{lemma "s == t ==> t = u ==> s == u" by simp} |
|
468 val trans2 = @{lemma "s = t ==> t == u ==> s == u" by simp} |
|
469 val trans3 = @{lemma "s = t ==> t = u ==> s == u" by simp} |
|
470 in |
|
471 fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2) |
|
472 | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1)) |
|
473 | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2)) |
|
474 | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3)) |
|
475 end |
|
476 |
|
477 |
|
478 (* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn |
|
479 (reflexive antecendents are droppped) *) |
|
480 local |
|
481 exception MONO |
|
482 |
|
483 fun prove_refl (ct, _) = Thm.reflexive ct |
|
484 fun prove_comb f g cp = |
|
485 let val ((ct1, ct2), (cu1, cu2)) = apply2 Thm.dest_comb cp |
|
486 in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end |
|
487 fun prove_arg f = prove_comb prove_refl f |
|
488 |
|
489 fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp |
|
490 |
|
491 fun prove_nary is_comb f = |
|
492 let |
|
493 fun prove (cp as (ct, _)) = f cp handle MONO => |
|
494 if is_comb (Thm.term_of ct) |
|
495 then prove_comb (prove_arg prove) prove cp |
|
496 else prove_refl cp |
|
497 in prove end |
|
498 |
|
499 fun prove_list f n cp = |
|
500 if n = 0 then prove_refl cp |
|
501 else prove_comb (prove_arg f) (prove_list f (n-1)) cp |
|
502 |
|
503 fun with_length f (cp as (cl, _)) = |
|
504 f (length (HOLogic.dest_list (Thm.term_of cl))) cp |
|
505 |
|
506 fun prove_distinct f = prove_arg (with_length (prove_list f)) |
|
507 |
|
508 fun prove_eq exn lookup cp = |
|
509 (case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of |
|
510 SOME eq => eq |
|
511 | NONE => if exn then raise MONO else prove_refl cp) |
|
512 |
|
513 val prove_exn = prove_eq true |
|
514 and prove_safe = prove_eq false |
|
515 |
|
516 fun mono f (cp as (cl, _)) = |
|
517 (case Term.head_of (Thm.term_of cl) of |
|
518 @{const HOL.conj} => prove_nary Old_Z3_Proof_Literals.is_conj (prove_exn f) |
|
519 | @{const HOL.disj} => prove_nary Old_Z3_Proof_Literals.is_disj (prove_exn f) |
|
520 | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f) |
|
521 | _ => prove (prove_safe f)) cp |
|
522 in |
|
523 fun monotonicity eqs ct = |
|
524 let |
|
525 fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)] |
|
526 val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs |
|
527 val lookup = AList.lookup (op aconv) teqs |
|
528 val cp = Thm.dest_binop (Thm.dest_arg ct) |
|
529 in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end |
|
530 end |
|
531 |
|
532 |
|
533 (* |- f a b = f b a (where f is equality) *) |
|
534 local |
|
535 val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)} |
|
536 in |
|
537 fun commutativity ct = |
|
538 MetaEq (Old_Z3_Proof_Tools.match_instantiate I |
|
539 (Old_Z3_Proof_Tools.as_meta_eq ct) rule) |
|
540 end |
|
541 |
|
542 |
|
543 |
|
544 (** quantifier proof rules **) |
|
545 |
|
546 (* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x) |
|
547 P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x) *) |
|
548 local |
|
549 val rules = [ |
|
550 @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp}, |
|
551 @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}] |
|
552 in |
|
553 fun quant_intro ctxt vars p ct = |
|
554 let |
|
555 val thm = meta_eq_of p |
|
556 val rules' = Old_Z3_Proof_Tools.varify vars thm :: rules |
|
557 val cu = Old_Z3_Proof_Tools.as_meta_eq ct |
|
558 val tac = REPEAT_ALL_NEW (match_tac ctxt rules') |
|
559 in MetaEq (Old_Z3_Proof_Tools.by_tac ctxt tac cu) end |
|
560 end |
|
561 |
|
562 |
|
563 (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *) |
|
564 fun pull_quant ctxt = Thm o try_apply ctxt [] [ |
|
565 named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] |
|
566 (* FIXME: not very well tested *) |
|
567 |
|
568 |
|
569 (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *) |
|
570 fun push_quant ctxt = Thm o try_apply ctxt [] [ |
|
571 named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] |
|
572 (* FIXME: not very well tested *) |
|
573 |
|
574 |
|
575 (* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *) |
|
576 local |
|
577 val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast} |
|
578 val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast} |
|
579 |
|
580 fun elim_unused_tac ctxt i st = ( |
|
581 match_tac ctxt [@{thm refl}] |
|
582 ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt) |
|
583 ORELSE' ( |
|
584 match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}] |
|
585 THEN' elim_unused_tac ctxt)) i st |
|
586 in |
|
587 |
|
588 fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (elim_unused_tac ctxt) |
|
589 |
|
590 end |
|
591 |
|
592 |
|
593 (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *) |
|
594 fun dest_eq_res ctxt = Thm o try_apply ctxt [] [ |
|
595 named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] |
|
596 (* FIXME: not very well tested *) |
|
597 |
|
598 |
|
599 (* |- ~(ALL x1...xn. P x1...xn) | P a1...an *) |
|
600 local |
|
601 val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast} |
|
602 in |
|
603 fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt ( |
|
604 REPEAT_ALL_NEW (match_tac ctxt [rule]) |
|
605 THEN' resolve_tac ctxt @{thms excluded_middle}) |
|
606 end |
|
607 |
|
608 |
|
609 (* |- (EX x. P x) = P c |- ~(ALL x. P x) = ~ P c *) |
|
610 local |
|
611 val forall = |
|
612 Old_SMT_Utils.mk_const_pat @{theory} @{const_name Pure.all} |
|
613 (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1) |
|
614 fun mk_forall cv ct = |
|
615 Thm.apply (Old_SMT_Utils.instT' cv forall) (Thm.lambda cv ct) |
|
616 |
|
617 fun get_vars f mk pred ctxt t = |
|
618 Term.fold_aterms f t [] |
|
619 |> map_filter (fn v => |
|
620 if pred v then SOME (Thm.cterm_of ctxt (mk v)) else NONE) |
|
621 |
|
622 fun close vars f ct ctxt = |
|
623 let |
|
624 val frees_of = get_vars Term.add_frees Free (member (op =) vars o fst) |
|
625 val vs = frees_of ctxt (Thm.term_of ct) |
|
626 val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt |
|
627 val vars_of = get_vars Term.add_vars Var (K true) ctxt' |
|
628 in |
|
629 (Thm.instantiate ([], map (dest_Var o Thm.term_of) (vars_of (Thm.prop_of thm)) ~~ vs) thm, |
|
630 ctxt') |
|
631 end |
|
632 |
|
633 val sk_rules = @{lemma |
|
634 "c = (SOME x. P x) ==> (EX x. P x) = P c" |
|
635 "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)" |
|
636 by (metis someI_ex)+} |
|
637 in |
|
638 |
|
639 fun skolemize vars = |
|
640 apfst Thm oo close vars (yield_singleton Assumption.add_assumes) |
|
641 |
|
642 fun discharge_sk_tac ctxt i st = ( |
|
643 resolve_tac ctxt @{thms trans} i |
|
644 THEN resolve_tac ctxt sk_rules i |
|
645 THEN (resolve_tac ctxt @{thms refl} ORELSE' discharge_sk_tac ctxt) (i+1) |
|
646 THEN resolve_tac ctxt @{thms refl} i) st |
|
647 |
|
648 end |
|
649 |
|
650 |
|
651 |
|
652 (** theory proof rules **) |
|
653 |
|
654 (* theory lemmas: linear arithmetic, arrays *) |
|
655 fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [ |
|
656 Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' => |
|
657 Old_Z3_Proof_Tools.by_tac ctxt' ( |
|
658 NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt') |
|
659 ORELSE' NAMED ctxt' "simp+arith" ( |
|
660 Simplifier.asm_full_simp_tac (put_simpset simpset ctxt') |
|
661 THEN_ALL_NEW Arith_Data.arith_tac ctxt')))] |
|
662 |
|
663 |
|
664 (* rewriting: prove equalities: |
|
665 * ACI of conjunction/disjunction |
|
666 * contradiction, excluded middle |
|
667 * logical rewriting rules (for negation, implication, equivalence, |
|
668 distinct) |
|
669 * normal forms for polynoms (integer/real arithmetic) |
|
670 * quantifier elimination over linear arithmetic |
|
671 * ... ? **) |
|
672 local |
|
673 fun spec_meta_eq_of thm = |
|
674 (case try (fn th => th RS @{thm spec}) thm of |
|
675 SOME thm' => spec_meta_eq_of thm' |
|
676 | NONE => mk_meta_eq thm) |
|
677 |
|
678 fun prep (Thm thm) = spec_meta_eq_of thm |
|
679 | prep (MetaEq thm) = thm |
|
680 | prep (Literals (thm, _)) = spec_meta_eq_of thm |
|
681 |
|
682 fun unfold_conv ctxt ths = |
|
683 Conv.arg_conv (Conv.binop_conv (Old_Z3_Proof_Tools.unfold_eqs ctxt |
|
684 (map prep ths))) |
|
685 |
|
686 fun with_conv _ [] prv = prv |
|
687 | with_conv ctxt ths prv = |
|
688 Old_Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv |
|
689 |
|
690 val unfold_conv = |
|
691 Conv.arg_conv (Conv.binop_conv |
|
692 (Conv.try_conv Old_Z3_Proof_Tools.unfold_distinct_conv)) |
|
693 val prove_conj_disj_eq = |
|
694 Old_Z3_Proof_Tools.with_conv unfold_conv Old_Z3_Proof_Literals.prove_conj_disj_eq |
|
695 |
|
696 fun declare_hyps ctxt thm = |
|
697 (thm, snd (Assumption.add_assumes (Thm.chyps_of thm) ctxt)) |
|
698 in |
|
699 |
|
700 val abstraction_depth = 3 |
|
701 (* |
|
702 This value was chosen large enough to potentially catch exceptions, |
|
703 yet small enough to not cause too much harm. The value might be |
|
704 increased in the future, if reconstructing 'rewrite' fails on problems |
|
705 that get too much abstracted to be reconstructable. |
|
706 *) |
|
707 |
|
708 fun rewrite simpset ths ct ctxt = |
|
709 apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [ |
|
710 named ctxt "conj/disj/distinct" prove_conj_disj_eq, |
|
711 named ctxt "pull-ite" Old_Z3_Proof_Methods.prove_ite ctxt, |
|
712 Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => |
|
713 Old_Z3_Proof_Tools.by_tac ctxt' ( |
|
714 NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt')) |
|
715 THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))), |
|
716 Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' => |
|
717 Old_Z3_Proof_Tools.by_tac ctxt' ( |
|
718 (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac) |
|
719 THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt')) |
|
720 THEN_ALL_NEW ( |
|
721 NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt') |
|
722 ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))), |
|
723 Old_Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' => |
|
724 Old_Z3_Proof_Tools.by_tac ctxt' ( |
|
725 (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac) |
|
726 THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt')) |
|
727 THEN_ALL_NEW ( |
|
728 NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt') |
|
729 ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))), |
|
730 named ctxt "injectivity" (Old_Z3_Proof_Methods.prove_injectivity ctxt), |
|
731 Old_Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt [] |
|
732 (fn ctxt' => |
|
733 Old_Z3_Proof_Tools.by_tac ctxt' ( |
|
734 (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac) |
|
735 THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt')) |
|
736 THEN_ALL_NEW ( |
|
737 NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt') |
|
738 ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac |
|
739 ctxt'))))]) ct)) |
|
740 |
|
741 end |
|
742 |
|
743 |
|
744 |
|
745 (* proof reconstruction *) |
|
746 |
|
747 (** tracing and checking **) |
|
748 |
|
749 fun trace_before ctxt idx = Old_SMT_Config.trace_msg ctxt (fn r => |
|
750 "Z3: #" ^ string_of_int idx ^ ": " ^ Old_Z3_Proof_Parser.string_of_rule r) |
|
751 |
|
752 fun check_after idx r ps ct (p, (ctxt, _)) = |
|
753 if not (Config.get ctxt Old_SMT_Config.trace) then () |
|
754 else |
|
755 let |
|
756 val thm = thm_of p |
|
757 val _ = Thm.consolidate thm |
|
758 in |
|
759 if (Thm.cprop_of thm) aconvc ct then () |
|
760 else |
|
761 z3_exn (Pretty.string_of (Pretty.big_list |
|
762 ("proof step failed: " ^ quote (Old_Z3_Proof_Parser.string_of_rule r) ^ |
|
763 " (#" ^ string_of_int idx ^ ")") |
|
764 (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @ |
|
765 [Pretty.block [Pretty.str "expected: ", |
|
766 Syntax.pretty_term ctxt (Thm.term_of ct)]]))) |
|
767 end |
|
768 |
|
769 |
|
770 (** overall reconstruction procedure **) |
|
771 |
|
772 local |
|
773 fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^ |
|
774 quote (Old_Z3_Proof_Parser.string_of_rule r)) |
|
775 |
|
776 fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) = |
|
777 (case (r, ps) of |
|
778 (* core rules *) |
|
779 (Old_Z3_Proof_Parser.True_Axiom, _) => (Thm Old_Z3_Proof_Literals.true_thm, cxp) |
|
780 | (Old_Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion" |
|
781 | (Old_Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion" |
|
782 | (Old_Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) => |
|
783 (mp q (thm_of p), cxp) |
|
784 | (Old_Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) => |
|
785 (mp q (thm_of p), cxp) |
|
786 | (Old_Z3_Proof_Parser.And_Elim, [(p, i)]) => |
|
787 and_elim (p, i) ct ptab ||> pair cx |
|
788 | (Old_Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) => |
|
789 not_or_elim (p, i) ct ptab ||> pair cx |
|
790 | (Old_Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp) |
|
791 | (Old_Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp) |
|
792 | (Old_Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) => |
|
793 (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp) |
|
794 | (Old_Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp) |
|
795 | (Old_Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp) |
|
796 | (Old_Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp) |
|
797 | (Old_Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp) |
|
798 | (Old_Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab |
|
799 | (Old_Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp) |
|
800 | (Old_Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp) |
|
801 | (Old_Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp) |
|
802 | (Old_Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp) |
|
803 |
|
804 (* equality rules *) |
|
805 | (Old_Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp) |
|
806 | (Old_Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp) |
|
807 | (Old_Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp) |
|
808 | (Old_Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp) |
|
809 | (Old_Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp) |
|
810 |
|
811 (* quantifier rules *) |
|
812 | (Old_Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro cx vars p ct, cxp) |
|
813 | (Old_Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp) |
|
814 | (Old_Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp) |
|
815 | (Old_Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp) |
|
816 | (Old_Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp) |
|
817 | (Old_Z3_Proof_Parser.Quant_Inst, _) => (quant_inst cx ct, cxp) |
|
818 | (Old_Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab |
|
819 |
|
820 (* theory rules *) |
|
821 | (Old_Z3_Proof_Parser.Th_Lemma _, _) => (* FIXME: use arguments *) |
|
822 (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp) |
|
823 | (Old_Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab |
|
824 | (Old_Z3_Proof_Parser.Rewrite_Star, ps) => |
|
825 rewrite simpset (map fst ps) ct cx ||> rpair ptab |
|
826 |
|
827 | (Old_Z3_Proof_Parser.Nnf_Star, _) => not_supported r |
|
828 | (Old_Z3_Proof_Parser.Cnf_Star, _) => not_supported r |
|
829 | (Old_Z3_Proof_Parser.Transitivity_Star, _) => not_supported r |
|
830 | (Old_Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r |
|
831 |
|
832 | _ => raise Fail ("Z3: proof rule " ^ |
|
833 quote (Old_Z3_Proof_Parser.string_of_rule r) ^ |
|
834 " has an unexpected number of arguments.")) |
|
835 |
|
836 fun lookup_proof ptab idx = |
|
837 (case Inttab.lookup ptab idx of |
|
838 SOME p => (p, idx) |
|
839 | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx))) |
|
840 |
|
841 fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) = |
|
842 let |
|
843 val Old_Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step |
|
844 val ps = map (lookup_proof ptab) prems |
|
845 val _ = trace_before ctxt idx r |
|
846 val (thm, (ctxt', ptab')) = |
|
847 cxp |
|
848 |> prove_step simpset vars r ps prop |
|
849 |> tap (check_after idx r ps prop) |
|
850 in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end |
|
851 |
|
852 fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl}, |
|
853 @{thm reflexive}, Old_Z3_Proof_Literals.true_thm] |
|
854 |
|
855 fun discharge_assms_tac ctxt rules = |
|
856 REPEAT (HEADGOAL (resolve_tac ctxt rules ORELSE' SOLVED' (discharge_sk_tac ctxt))) |
|
857 |
|
858 fun discharge_assms ctxt rules thm = |
|
859 if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm |
|
860 else |
|
861 (case Seq.pull (discharge_assms_tac ctxt rules thm) of |
|
862 SOME (thm', _) => Goal.norm_result ctxt thm' |
|
863 | NONE => raise THM ("failed to discharge premise", 1, [thm])) |
|
864 |
|
865 fun discharge rules outer_ctxt (p, (inner_ctxt, _)) = |
|
866 thm_of p |
|
867 |> singleton (Proof_Context.export inner_ctxt outer_ctxt) |
|
868 |> discharge_assms outer_ctxt (make_discharge_rules rules) |
|
869 in |
|
870 |
|
871 fun reconstruct outer_ctxt recon output = |
|
872 let |
|
873 val {context=ctxt, typs, terms, rewrite_rules, assms} = recon |
|
874 val (asserted, steps, vars, ctxt1) = |
|
875 Old_Z3_Proof_Parser.parse ctxt typs terms output |
|
876 |
|
877 val simpset = |
|
878 Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems old_z3_simp}) |
|
879 |
|
880 val ((is, rules), cxp as (ctxt2, _)) = |
|
881 add_asserted outer_ctxt rewrite_rules assms asserted ctxt1 |
|
882 in |
|
883 if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI}) |
|
884 else |
|
885 (Thm @{thm TrueI}, cxp) |
|
886 |> fold (prove simpset vars) steps |
|
887 |> discharge rules outer_ctxt |
|
888 |> pair [] |
|
889 end |
|
890 |
|
891 end |
|
892 |
|
893 end |
|