|
1 (* Title: HOL/Tools/SMT/z3_proof_reconstruction.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Proof reconstruction for proofs found by Z3. |
|
5 *) |
|
6 |
|
7 signature Z3_PROOF_RECONSTRUCTION = |
|
8 sig |
|
9 val trace_assms: bool Config.T |
|
10 val reconstruct: string list * SMT_Translate.recon -> Proof.context -> |
|
11 thm * Proof.context |
|
12 val setup: theory -> theory |
|
13 end |
|
14 |
|
15 structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION = |
|
16 struct |
|
17 |
|
18 structure P = Z3_Proof_Parser |
|
19 structure T = Z3_Proof_Tools |
|
20 structure L = Z3_Proof_Literals |
|
21 |
|
22 fun z3_exn msg = raise SMT_Solver.SMT ("Z3 proof reconstruction: " ^ msg) |
|
23 |
|
24 |
|
25 |
|
26 (** net of schematic rules **) |
|
27 |
|
28 val z3_ruleN = "z3_rule" |
|
29 |
|
30 local |
|
31 val description = "declaration of Z3 proof rules" |
|
32 |
|
33 val eq = Thm.eq_thm |
|
34 |
|
35 structure Z3_Rules = Generic_Data |
|
36 ( |
|
37 type T = thm Net.net |
|
38 val empty = Net.empty |
|
39 val extend = I |
|
40 val merge = Net.merge eq |
|
41 ) |
|
42 |
|
43 val prep = `Thm.prop_of o Simplifier.rewrite_rule [L.rewrite_true] |
|
44 |
|
45 fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net |
|
46 fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net |
|
47 |
|
48 val add = Thm.declaration_attribute (Z3_Rules.map o ins) |
|
49 val del = Thm.declaration_attribute (Z3_Rules.map o del) |
|
50 in |
|
51 |
|
52 fun get_schematic_rules ctxt = Net.content (Z3_Rules.get (Context.Proof ctxt)) |
|
53 |
|
54 fun by_schematic_rule ctxt ct = |
|
55 the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct) |
|
56 |
|
57 val z3_rules_setup = |
|
58 Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #> |
|
59 PureThy.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get) |
|
60 |
|
61 end |
|
62 |
|
63 |
|
64 |
|
65 (** proof tools **) |
|
66 |
|
67 fun named ctxt name prover ct = |
|
68 let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") |
|
69 in prover ct end |
|
70 |
|
71 fun NAMED ctxt name tac i st = |
|
72 let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") |
|
73 in tac i st end |
|
74 |
|
75 fun pretty_goal ctxt thms t = |
|
76 [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]] |
|
77 |> not (null thms) ? cons (Pretty.big_list "assumptions:" |
|
78 (map (Display.pretty_thm ctxt) thms)) |
|
79 |
|
80 fun try_apply ctxt thms = |
|
81 let |
|
82 fun try_apply_err ct = Pretty.string_of (Pretty.chunks [ |
|
83 Pretty.big_list ("Z3 found a proof," ^ |
|
84 " but proof reconstruction failed at the following subgoal:") |
|
85 (pretty_goal ctxt thms (Thm.term_of ct)), |
|
86 Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^ |
|
87 " might solve this problem.")]) |
|
88 |
|
89 fun apply [] ct = error (try_apply_err ct) |
|
90 | apply (prover :: provers) ct = |
|
91 (case try prover ct of |
|
92 SOME thm => (SMT_Solver.trace_msg ctxt I "Z3: succeeded"; thm) |
|
93 | NONE => apply provers ct) |
|
94 |
|
95 in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end |
|
96 |
|
97 |
|
98 |
|
99 (** theorems and proofs **) |
|
100 |
|
101 (* theorem incarnations *) |
|
102 |
|
103 datatype theorem = |
|
104 Thm of thm | (* theorem without special features *) |
|
105 MetaEq of thm | (* meta equality "t == s" *) |
|
106 Literals of thm * L.littab |
|
107 (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *) |
|
108 |
|
109 fun thm_of (Thm thm) = thm |
|
110 | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq} |
|
111 | thm_of (Literals (thm, _)) = thm |
|
112 |
|
113 fun meta_eq_of (MetaEq thm) = thm |
|
114 | meta_eq_of p = mk_meta_eq (thm_of p) |
|
115 |
|
116 fun literals_of (Literals (_, lits)) = lits |
|
117 | literals_of p = L.make_littab [thm_of p] |
|
118 |
|
119 |
|
120 (* proof representation *) |
|
121 |
|
122 datatype proof = Unproved of P.proof_step | Proved of theorem |
|
123 |
|
124 |
|
125 |
|
126 (** core proof rules **) |
|
127 |
|
128 (* assumption *) |
|
129 |
|
130 val (trace_assms, trace_assms_setup) = |
|
131 Attrib.config_bool "z3_trace_assms" (K false) |
|
132 |
|
133 local |
|
134 val remove_trigger = @{lemma "trigger t p == p" |
|
135 by (rule eq_reflection, rule trigger_def)} |
|
136 |
|
137 val prep_rules = [@{thm Let_def}, remove_trigger, L.rewrite_true] |
|
138 |
|
139 fun rewrite_conv ctxt eqs = Simplifier.full_rewrite |
|
140 (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs) |
|
141 |
|
142 fun rewrites ctxt eqs = map (Conv.fconv_rule (rewrite_conv ctxt eqs)) |
|
143 |
|
144 fun trace ctxt thm = |
|
145 if Config.get ctxt trace_assms |
|
146 then tracing (Display.string_of_thm ctxt thm) |
|
147 else () |
|
148 |
|
149 fun lookup_assm ctxt assms ct = |
|
150 (case T.net_instance assms ct of |
|
151 SOME thm => (trace ctxt thm; thm) |
|
152 | _ => z3_exn ("not asserted: " ^ |
|
153 quote (Syntax.string_of_term ctxt (Thm.term_of ct)))) |
|
154 in |
|
155 fun prepare_assms ctxt unfolds assms = |
|
156 let |
|
157 val unfolds' = rewrites ctxt [L.rewrite_true] unfolds |
|
158 val assms' = rewrites ctxt (union Thm.eq_thm unfolds' prep_rules) assms |
|
159 in (unfolds', T.thm_net_of assms') end |
|
160 |
|
161 fun asserted _ NONE ct = Thm (Thm.assume ct) |
|
162 | asserted ctxt (SOME (unfolds, assms)) ct = |
|
163 let val revert_conv = rewrite_conv ctxt unfolds |
|
164 in Thm (T.with_conv revert_conv (lookup_assm ctxt assms) ct) end |
|
165 end |
|
166 |
|
167 |
|
168 |
|
169 (* P = Q ==> P ==> Q or P --> Q ==> P ==> Q *) |
|
170 local |
|
171 val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp} |
|
172 val meta_iffD1_c = T.precompose2 Thm.dest_binop meta_iffD1 |
|
173 |
|
174 val iffD1_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm iffD1} |
|
175 val mp_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm mp} |
|
176 in |
|
177 fun mp (MetaEq thm) p = Thm (Thm.implies_elim (T.compose meta_iffD1_c thm) p) |
|
178 | mp p_q p = |
|
179 let |
|
180 val pq = thm_of p_q |
|
181 val thm = T.compose iffD1_c pq handle THM _ => T.compose mp_c pq |
|
182 in Thm (Thm.implies_elim thm p) end |
|
183 end |
|
184 |
|
185 |
|
186 |
|
187 (* and_elim: P1 & ... & Pn ==> Pi *) |
|
188 (* not_or_elim: ~(P1 | ... | Pn) ==> ~Pi *) |
|
189 local |
|
190 fun is_sublit conj t = L.exists_lit conj (fn u => u aconv t) |
|
191 |
|
192 fun derive conj t lits idx ptab = |
|
193 let |
|
194 val lit = the (L.get_first_lit (is_sublit conj t) lits) |
|
195 val ls = L.explode conj false false [t] lit |
|
196 val lits' = fold L.insert_lit ls (L.delete_lit lit lits) |
|
197 |
|
198 fun upd (Proved thm) = Proved (Literals (thm_of thm, lits')) |
|
199 | upd p = p |
|
200 in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end |
|
201 |
|
202 fun lit_elim conj (p, idx) ct ptab = |
|
203 let val lits = literals_of p |
|
204 in |
|
205 (case L.lookup_lit lits (T.term_of ct) of |
|
206 SOME lit => (Thm lit, ptab) |
|
207 | NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab)) |
|
208 end |
|
209 in |
|
210 val and_elim = lit_elim true |
|
211 val not_or_elim = lit_elim false |
|
212 end |
|
213 |
|
214 |
|
215 |
|
216 (* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *) |
|
217 local |
|
218 fun step lit thm = |
|
219 Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit |
|
220 val explode_disj = L.explode false false false |
|
221 fun intro hyps thm th = fold step (explode_disj hyps th) thm |
|
222 |
|
223 fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))] |
|
224 val ccontr = T.precompose dest_ccontr @{thm ccontr} |
|
225 in |
|
226 fun lemma thm ct = |
|
227 let |
|
228 val cu = Thm.capply @{cterm Not} (Thm.dest_arg ct) |
|
229 val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm)) |
|
230 in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end |
|
231 end |
|
232 |
|
233 |
|
234 |
|
235 (* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *) |
|
236 local |
|
237 val explode_disj = L.explode false true false |
|
238 val join_disj = L.join false |
|
239 fun unit thm thms th = |
|
240 let val t = @{term Not} $ T.prop_of thm and ts = map T.prop_of thms |
|
241 in join_disj (L.make_littab (thms @ explode_disj ts th)) t end |
|
242 |
|
243 fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) |
|
244 fun dest ct = pairself dest_arg2 (Thm.dest_binop ct) |
|
245 val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast} |
|
246 in |
|
247 fun unit_resolution thm thms ct = |
|
248 Thm.capply @{cterm Not} (Thm.dest_arg ct) |
|
249 |> T.under_assumption (unit thm thms) |
|
250 |> Thm o T.discharge thm o T.compose contrapos |
|
251 end |
|
252 |
|
253 |
|
254 |
|
255 (* P ==> P == True or P ==> P == False *) |
|
256 local |
|
257 val iff1 = @{lemma "P ==> P == (~ False)" by simp} |
|
258 val iff2 = @{lemma "~P ==> P == False" by simp} |
|
259 in |
|
260 fun iff_true thm = MetaEq (thm COMP iff1) |
|
261 fun iff_false thm = MetaEq (thm COMP iff2) |
|
262 end |
|
263 |
|
264 |
|
265 |
|
266 (* distributivity of | over & *) |
|
267 fun distributivity ctxt = Thm o try_apply ctxt [] [ |
|
268 named ctxt "fast" (T.by_tac (Classical.best_tac HOL_cs))] |
|
269 (* FIXME: not very well tested *) |
|
270 |
|
271 |
|
272 |
|
273 (* Tseitin-like axioms *) |
|
274 |
|
275 local |
|
276 val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast} |
|
277 val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast} |
|
278 val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast} |
|
279 val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast} |
|
280 |
|
281 fun prove' conj1 conj2 ct2 thm = |
|
282 let val lits = L.true_thm :: L.explode conj1 true (conj1 <> conj2) [] thm |
|
283 in L.join conj2 (L.make_littab lits) (Thm.term_of ct2) end |
|
284 |
|
285 fun prove rule (ct1, conj1) (ct2, conj2) = |
|
286 T.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule |
|
287 |
|
288 fun prove_def_axiom ct = |
|
289 let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct) |
|
290 in |
|
291 (case Thm.term_of ct1 of |
|
292 @{term Not} $ (@{term "op &"} $ _ $ _) => |
|
293 prove disjI1 (Thm.dest_arg ct1, true) (ct2, true) |
|
294 | @{term "op &"} $ _ $ _ => |
|
295 prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true) |
|
296 | @{term Not} $ (@{term "op |"} $ _ $ _) => |
|
297 prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false) |
|
298 | @{term "op |"} $ _ $ _ => |
|
299 prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true) |
|
300 | Const (@{const_name distinct}, _) $ _ => |
|
301 let |
|
302 fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv) |
|
303 fun prv cu = |
|
304 let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) |
|
305 in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end |
|
306 in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end |
|
307 | @{term Not} $ (Const (@{const_name distinct}, _) $ _) => |
|
308 let |
|
309 fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv)) |
|
310 fun prv cu = |
|
311 let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) |
|
312 in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end |
|
313 in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end |
|
314 | _ => raise CTERM ("prove_def_axiom", [ct])) |
|
315 end |
|
316 |
|
317 val rewr_if = |
|
318 @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp} |
|
319 in |
|
320 fun def_axiom ctxt = Thm o try_apply ctxt [] [ |
|
321 named ctxt "conj/disj/distinct" prove_def_axiom, |
|
322 T.by_abstraction ctxt [] (fn ctxt' => |
|
323 named ctxt' "simp+fast" (T.by_tac ( |
|
324 Simplifier.simp_tac (HOL_ss addsimps [rewr_if]) |
|
325 THEN_ALL_NEW Classical.best_tac HOL_cs)))] |
|
326 end |
|
327 |
|
328 |
|
329 |
|
330 (* local definitions *) |
|
331 local |
|
332 val intro_rules = [ |
|
333 @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp}, |
|
334 @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)" |
|
335 by simp}, |
|
336 @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ] |
|
337 |
|
338 val apply_rules = [ |
|
339 @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast}, |
|
340 @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n" |
|
341 by (atomize(full)) fastsimp} ] |
|
342 |
|
343 val inst_rule = T.match_instantiate Thm.dest_arg |
|
344 |
|
345 fun apply_rule ct = |
|
346 (case get_first (try (inst_rule ct)) intro_rules of |
|
347 SOME thm => thm |
|
348 | NONE => raise CTERM ("intro_def", [ct])) |
|
349 in |
|
350 fun intro_def ct = T.make_hyp_def (apply_rule ct) #>> Thm |
|
351 |
|
352 fun apply_def thm = |
|
353 get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules |
|
354 |> the_default (Thm thm) |
|
355 end |
|
356 |
|
357 |
|
358 |
|
359 (* negation normal form *) |
|
360 |
|
361 local |
|
362 val quant_rules1 = ([ |
|
363 @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp}, |
|
364 @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [ |
|
365 @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp}, |
|
366 @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}]) |
|
367 |
|
368 val quant_rules2 = ([ |
|
369 @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp}, |
|
370 @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [ |
|
371 @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp}, |
|
372 @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}]) |
|
373 |
|
374 fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = ( |
|
375 Tactic.rtac thm ORELSE' |
|
376 (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE' |
|
377 (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st |
|
378 |
|
379 fun nnf_quant vars qs p ct = |
|
380 T.as_meta_eq ct |
|
381 |> T.by_tac (nnf_quant_tac (T.varify vars (meta_eq_of p)) qs) |
|
382 |
|
383 fun prove_nnf ctxt = try_apply ctxt [] [ |
|
384 named ctxt "conj/disj" L.prove_conj_disj_eq] |
|
385 in |
|
386 fun nnf ctxt vars ps ct = |
|
387 (case T.term_of ct of |
|
388 _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) => |
|
389 if l aconv r |
|
390 then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) |
|
391 else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct) |
|
392 | _ $ (@{term Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) => |
|
393 MetaEq (nnf_quant vars quant_rules2 (hd ps) ct) |
|
394 | _ => |
|
395 let |
|
396 val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv |
|
397 (T.unfold_eqs ctxt (map (Thm.symmetric o meta_eq_of) ps))) |
|
398 in Thm (T.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end) |
|
399 end |
|
400 |
|
401 |
|
402 |
|
403 (** equality proof rules **) |
|
404 |
|
405 (* |- t = t *) |
|
406 fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) |
|
407 |
|
408 |
|
409 |
|
410 (* s = t ==> t = s *) |
|
411 local |
|
412 val symm_rule = @{lemma "s = t ==> t == s" by simp} |
|
413 in |
|
414 fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm) |
|
415 | symm p = MetaEq (thm_of p COMP symm_rule) |
|
416 end |
|
417 |
|
418 |
|
419 |
|
420 (* s = t ==> t = u ==> s = u *) |
|
421 local |
|
422 val trans1 = @{lemma "s == t ==> t = u ==> s == u" by simp} |
|
423 val trans2 = @{lemma "s = t ==> t == u ==> s == u" by simp} |
|
424 val trans3 = @{lemma "s = t ==> t = u ==> s == u" by simp} |
|
425 in |
|
426 fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2) |
|
427 | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1)) |
|
428 | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2)) |
|
429 | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3)) |
|
430 end |
|
431 |
|
432 |
|
433 |
|
434 (* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn |
|
435 (reflexive antecendents are droppped) *) |
|
436 local |
|
437 exception MONO |
|
438 |
|
439 fun prove_refl (ct, _) = Thm.reflexive ct |
|
440 fun prove_comb f g cp = |
|
441 let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp |
|
442 in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end |
|
443 fun prove_arg f = prove_comb prove_refl f |
|
444 |
|
445 fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp |
|
446 |
|
447 fun prove_nary is_comb f = |
|
448 let |
|
449 fun prove (cp as (ct, _)) = f cp handle MONO => |
|
450 if is_comb (Thm.term_of ct) |
|
451 then prove_comb (prove_arg prove) prove cp |
|
452 else prove_refl cp |
|
453 in prove end |
|
454 |
|
455 fun prove_list f n cp = |
|
456 if n = 0 then prove_refl cp |
|
457 else prove_comb (prove_arg f) (prove_list f (n-1)) cp |
|
458 |
|
459 fun with_length f (cp as (cl, _)) = |
|
460 f (length (HOLogic.dest_list (Thm.term_of cl))) cp |
|
461 |
|
462 fun prove_distinct f = prove_arg (with_length (prove_list f)) |
|
463 |
|
464 fun prove_eq exn lookup cp = |
|
465 (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of |
|
466 SOME eq => eq |
|
467 | NONE => if exn then raise MONO else prove_refl cp) |
|
468 |
|
469 val prove_eq_exn = prove_eq true |
|
470 and prove_eq_safe = prove_eq false |
|
471 |
|
472 fun mono f (cp as (cl, _)) = |
|
473 (case Term.head_of (Thm.term_of cl) of |
|
474 @{term "op &"} => prove_nary L.is_conj (prove_eq_exn f) |
|
475 | @{term "op |"} => prove_nary L.is_disj (prove_eq_exn f) |
|
476 | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f) |
|
477 | _ => prove (prove_eq_safe f)) cp |
|
478 in |
|
479 fun monotonicity eqs ct = |
|
480 let |
|
481 val lookup = AList.lookup (op aconv) (map (`Thm.prop_of o meta_eq_of) eqs) |
|
482 val cp = Thm.dest_binop (Thm.dest_arg ct) |
|
483 in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end |
|
484 end |
|
485 |
|
486 |
|
487 |
|
488 (* |- f a b = f b a (where f is equality) *) |
|
489 local |
|
490 val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)} |
|
491 in |
|
492 fun commutativity ct = MetaEq (T.match_instantiate I (T.as_meta_eq ct) rule) |
|
493 end |
|
494 |
|
495 |
|
496 |
|
497 (** quantifier proof rules **) |
|
498 |
|
499 (* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x) |
|
500 P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x) *) |
|
501 local |
|
502 val rules = [ |
|
503 @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp}, |
|
504 @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}] |
|
505 in |
|
506 fun quant_intro vars p ct = |
|
507 let |
|
508 val thm = meta_eq_of p |
|
509 val rules' = T.varify vars thm :: rules |
|
510 val cu = T.as_meta_eq ct |
|
511 in MetaEq (T.by_tac (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end |
|
512 end |
|
513 |
|
514 |
|
515 |
|
516 (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *) |
|
517 fun pull_quant ctxt = Thm o try_apply ctxt [] [ |
|
518 named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] |
|
519 (* FIXME: not very well tested *) |
|
520 |
|
521 |
|
522 |
|
523 (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *) |
|
524 fun push_quant ctxt = Thm o try_apply ctxt [] [ |
|
525 named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] |
|
526 (* FIXME: not very well tested *) |
|
527 |
|
528 |
|
529 |
|
530 (* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *) |
|
531 local |
|
532 val elim_all = @{lemma "(ALL x. P) == P" by simp} |
|
533 val elim_ex = @{lemma "(EX x. P) == P" by simp} |
|
534 |
|
535 fun elim_unused_conv ctxt = |
|
536 Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv |
|
537 (More_Conv.rewrs_conv [elim_all, elim_ex])))) ctxt |
|
538 |
|
539 fun elim_unused_tac ctxt = |
|
540 REPEAT_ALL_NEW ( |
|
541 Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}] |
|
542 ORELSE' CONVERSION (elim_unused_conv ctxt)) |
|
543 in |
|
544 fun elim_unused_vars ctxt = Thm o T.by_tac (elim_unused_tac ctxt) |
|
545 end |
|
546 |
|
547 |
|
548 |
|
549 (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *) |
|
550 fun dest_eq_res ctxt = Thm o try_apply ctxt [] [ |
|
551 named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] |
|
552 (* FIXME: not very well tested *) |
|
553 |
|
554 |
|
555 |
|
556 (* |- ~(ALL x1...xn. P x1...xn) | P a1...an *) |
|
557 local |
|
558 val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast} |
|
559 in |
|
560 val quant_inst = Thm o T.by_tac ( |
|
561 REPEAT_ALL_NEW (Tactic.match_tac [rule]) |
|
562 THEN' Tactic.rtac @{thm excluded_middle}) |
|
563 end |
|
564 |
|
565 |
|
566 |
|
567 (* c = SOME x. P x |- (EX x. P x) = P c |
|
568 c = SOME x. ~ P x |- ~(ALL x. P x) = ~ P c *) |
|
569 local |
|
570 val elim_ex = @{lemma "EX x. P == P" by simp} |
|
571 val elim_all = @{lemma "~ (ALL x. P) == ~P" by simp} |
|
572 val sk_ex = @{lemma "c == SOME x. P x ==> EX x. P x == P c" |
|
573 by simp (intro eq_reflection some_eq_ex[symmetric])} |
|
574 val sk_all = @{lemma "c == SOME x. ~ P x ==> ~(ALL x. P x) == ~ P c" |
|
575 by (simp only: not_all) (intro eq_reflection some_eq_ex[symmetric])} |
|
576 val sk_ex_rule = ((sk_ex, I), elim_ex) |
|
577 and sk_all_rule = ((sk_all, Thm.dest_arg), elim_all) |
|
578 |
|
579 fun dest f sk_rule = |
|
580 Thm.dest_comb (f (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of sk_rule)))) |
|
581 fun type_of f sk_rule = Thm.ctyp_of_term (snd (dest f sk_rule)) |
|
582 fun pair2 (a, b) (c, d) = [(a, c), (b, d)] |
|
583 fun inst_sk (sk_rule, f) p c = |
|
584 Thm.instantiate ([(type_of f sk_rule, Thm.ctyp_of_term c)], []) sk_rule |
|
585 |> (fn sk' => Thm.instantiate ([], (pair2 (dest f sk') (p, c))) sk') |
|
586 |> Conv.fconv_rule (Thm.beta_conversion true) |
|
587 |
|
588 fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I) |
|
589 | kind (@{term Not} $ (Const (@{const_name All}, _) $ _)) = |
|
590 (sk_all_rule, Thm.dest_arg, Thm.capply @{cterm Not}) |
|
591 | kind t = raise TERM ("skolemize", [t]) |
|
592 |
|
593 fun dest_abs_type (Abs (_, T, _)) = T |
|
594 | dest_abs_type t = raise TERM ("dest_abs_type", [t]) |
|
595 |
|
596 fun bodies_of thy lhs rhs = |
|
597 let |
|
598 val (rule, dest, make) = kind (Thm.term_of lhs) |
|
599 |
|
600 fun dest_body idx cbs ct = |
|
601 let |
|
602 val cb = Thm.dest_arg (dest ct) |
|
603 val T = dest_abs_type (Thm.term_of cb) |
|
604 val cv = Thm.cterm_of thy (Var (("x", idx), T)) |
|
605 val cu = make (Drule.beta_conv cb cv) |
|
606 val cbs' = (cv, cb) :: cbs |
|
607 in |
|
608 (snd (Thm.first_order_match (cu, rhs)), rev cbs') |
|
609 handle Pattern.MATCH => dest_body (idx+1) cbs' cu |
|
610 end |
|
611 in (rule, dest_body 1 [] lhs) end |
|
612 |
|
613 fun transitive f thm = Thm.transitive thm (f (Thm.rhs_of thm)) |
|
614 |
|
615 fun sk_step (rule, elim) (cv, mct, cb) ((is, thm), ctxt) = |
|
616 (case mct of |
|
617 SOME ct => |
|
618 ctxt |
|
619 |> T.make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct) |
|
620 |>> pair ((cv, ct) :: is) o Thm.transitive thm |
|
621 | NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt)) |
|
622 in |
|
623 fun skolemize ct ctxt = |
|
624 let |
|
625 val (lhs, rhs) = Thm.dest_binop (Thm.dest_arg ct) |
|
626 val (rule, (ctab, cbs)) = bodies_of (ProofContext.theory_of ctxt) lhs rhs |
|
627 fun lookup_var (cv, cb) = (cv, AList.lookup (op aconvc) ctab cv, cb) |
|
628 in |
|
629 (([], Thm.reflexive lhs), ctxt) |
|
630 |> fold (sk_step rule) (map lookup_var cbs) |
|
631 |>> MetaEq o snd |
|
632 end |
|
633 end |
|
634 |
|
635 |
|
636 |
|
637 (** theory proof rules **) |
|
638 |
|
639 (* theory lemmas: linear arithmetic, arrays *) |
|
640 |
|
641 fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [ |
|
642 T.by_abstraction ctxt thms (fn ctxt' => T.by_tac ( |
|
643 NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt') |
|
644 ORELSE' NAMED ctxt' "simp+arith" (Simplifier.simp_tac simpset THEN_ALL_NEW |
|
645 Arith_Data.arith_tac ctxt')))] |
|
646 |
|
647 |
|
648 |
|
649 (* rewriting: prove equalities: |
|
650 * ACI of conjunction/disjunction |
|
651 * contradiction, excluded middle |
|
652 * logical rewriting rules (for negation, implication, equivalence, |
|
653 distinct) |
|
654 * normal forms for polynoms (integer/real arithmetic) |
|
655 * quantifier elimination over linear arithmetic |
|
656 * ... ? **) |
|
657 structure Z3_Simps = Named_Thms |
|
658 ( |
|
659 val name = "z3_simp" |
|
660 val description = "simplification rules for Z3 proof reconstruction" |
|
661 ) |
|
662 |
|
663 local |
|
664 fun spec_meta_eq_of thm = |
|
665 (case try (fn th => th RS @{thm spec}) thm of |
|
666 SOME thm' => spec_meta_eq_of thm' |
|
667 | NONE => mk_meta_eq thm) |
|
668 |
|
669 fun prep (Thm thm) = spec_meta_eq_of thm |
|
670 | prep (MetaEq thm) = thm |
|
671 | prep (Literals (thm, _)) = spec_meta_eq_of thm |
|
672 |
|
673 fun unfold_conv ctxt ths = |
|
674 Conv.arg_conv (Conv.binop_conv (T.unfold_eqs ctxt (map prep ths))) |
|
675 |
|
676 fun with_conv _ [] prv = prv |
|
677 | with_conv ctxt ths prv = T.with_conv (unfold_conv ctxt ths) prv |
|
678 |
|
679 val unfold_conv = |
|
680 Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv)) |
|
681 val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq |
|
682 in |
|
683 |
|
684 fun rewrite ctxt simpset ths = Thm o with_conv ctxt ths (try_apply ctxt [] [ |
|
685 named ctxt "conj/disj/distinct" prove_conj_disj_eq, |
|
686 T.by_abstraction ctxt [] (fn ctxt' => T.by_tac ( |
|
687 NAMED ctxt' "simp" (Simplifier.simp_tac simpset) |
|
688 THEN_ALL_NEW ( |
|
689 NAMED ctxt' "fast" (Classical.fast_tac HOL_cs) |
|
690 ORELSE' NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt'))))]) |
|
691 |
|
692 end |
|
693 |
|
694 |
|
695 |
|
696 (** proof reconstruction **) |
|
697 |
|
698 (* tracing and checking *) |
|
699 |
|
700 local |
|
701 fun count_rules ptab = |
|
702 let |
|
703 fun count (_, Unproved _) (solved, total) = (solved, total + 1) |
|
704 | count (_, Proved _) (solved, total) = (solved + 1, total + 1) |
|
705 in Inttab.fold count ptab (0, 0) end |
|
706 |
|
707 fun header idx r (solved, total) = |
|
708 "Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r ^ " (goal " ^ |
|
709 string_of_int (solved + 1) ^ " of " ^ string_of_int total ^ ")" |
|
710 |
|
711 fun check ctxt idx r ps ct p = |
|
712 let val thm = thm_of p |> tap (Thm.join_proofs o single) |
|
713 in |
|
714 if (Thm.cprop_of thm) aconvc ct then () |
|
715 else z3_exn (Pretty.string_of (Pretty.big_list ("proof step failed: " ^ |
|
716 quote (P.string_of_rule r) ^ " (#" ^ string_of_int idx ^ ")") |
|
717 (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @ |
|
718 [Pretty.block [Pretty.str "expected: ", |
|
719 Syntax.pretty_term ctxt (Thm.term_of ct)]]))) |
|
720 end |
|
721 in |
|
722 fun trace_rule idx prove r ps ct (cxp as (ctxt, ptab)) = |
|
723 let |
|
724 val _ = SMT_Solver.trace_msg ctxt (header idx r o count_rules) ptab |
|
725 val result as (p, cxp' as (ctxt', _)) = prove r ps ct cxp |
|
726 val _ = if not (Config.get ctxt' SMT_Solver.trace) then () |
|
727 else check ctxt' idx r ps ct p |
|
728 in result end |
|
729 end |
|
730 |
|
731 |
|
732 (* overall reconstruction procedure *) |
|
733 |
|
734 fun not_supported r = |
|
735 raise Fail ("Z3: proof rule not implemented: " ^ quote (P.string_of_rule r)) |
|
736 |
|
737 fun prove ctxt unfolds assms vars = |
|
738 let |
|
739 val assms' = Option.map (prepare_assms ctxt unfolds) assms |
|
740 val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt) |
|
741 |
|
742 fun step r ps ct (cxp as (cx, ptab)) = |
|
743 (case (r, ps) of |
|
744 (* core rules *) |
|
745 (P.TrueAxiom, _) => (Thm L.true_thm, cxp) |
|
746 | (P.Asserted, _) => (asserted cx assms' ct, cxp) |
|
747 | (P.Goal, _) => (asserted cx assms' ct, cxp) |
|
748 | (P.ModusPonens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp) |
|
749 | (P.ModusPonensOeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp) |
|
750 | (P.AndElim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx |
|
751 | (P.NotOrElim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx |
|
752 | (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp) |
|
753 | (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp) |
|
754 | (P.UnitResolution, (p, _) :: ps) => |
|
755 (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp) |
|
756 | (P.IffTrue, [(p, _)]) => (iff_true (thm_of p), cxp) |
|
757 | (P.IffFalse, [(p, _)]) => (iff_false (thm_of p), cxp) |
|
758 | (P.Distributivity, _) => (distributivity cx ct, cxp) |
|
759 | (P.DefAxiom, _) => (def_axiom cx ct, cxp) |
|
760 | (P.IntroDef, _) => intro_def ct cx ||> rpair ptab |
|
761 | (P.ApplyDef, [(p, _)]) => (apply_def (thm_of p), cxp) |
|
762 | (P.IffOeq, [(p, _)]) => (p, cxp) |
|
763 | (P.NnfPos, _) => (nnf cx vars (map fst ps) ct, cxp) |
|
764 | (P.NnfNeg, _) => (nnf cx vars (map fst ps) ct, cxp) |
|
765 |
|
766 (* equality rules *) |
|
767 | (P.Reflexivity, _) => (refl ct, cxp) |
|
768 | (P.Symmetry, [(p, _)]) => (symm p, cxp) |
|
769 | (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp) |
|
770 | (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp) |
|
771 | (P.Commutativity, _) => (commutativity ct, cxp) |
|
772 |
|
773 (* quantifier rules *) |
|
774 | (P.QuantIntro, [(p, _)]) => (quant_intro vars p ct, cxp) |
|
775 | (P.PullQuant, _) => (pull_quant cx ct, cxp) |
|
776 | (P.PushQuant, _) => (push_quant cx ct, cxp) |
|
777 | (P.ElimUnusedVars, _) => (elim_unused_vars cx ct, cxp) |
|
778 | (P.DestEqRes, _) => (dest_eq_res cx ct, cxp) |
|
779 | (P.QuantInst, _) => (quant_inst ct, cxp) |
|
780 | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab |
|
781 |
|
782 (* theory rules *) |
|
783 | (P.ThLemma, _) => |
|
784 (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp) |
|
785 | (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp) |
|
786 | (P.RewriteStar, ps) => |
|
787 (rewrite cx simpset (map fst ps) ct, cxp) |
|
788 |
|
789 | (P.NnfStar, _) => not_supported r |
|
790 | (P.CnfStar, _) => not_supported r |
|
791 | (P.TransitivityStar, _) => not_supported r |
|
792 | (P.PullQuantStar, _) => not_supported r |
|
793 |
|
794 | _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^ |
|
795 " has an unexpected number of arguments.")) |
|
796 |
|
797 fun conclude idx rule prop (ps, cxp) = |
|
798 trace_rule idx step rule ps prop cxp |
|
799 |-> (fn p => apsnd (Inttab.update (idx, Proved p)) #> pair p) |
|
800 |
|
801 fun lookup idx (cxp as (cx, ptab)) = |
|
802 (case Inttab.lookup ptab idx of |
|
803 SOME (Unproved (P.Proof_Step {rule, prems, prop})) => |
|
804 fold_map lookup prems cxp |
|
805 |>> map2 rpair prems |
|
806 |> conclude idx rule prop |
|
807 | SOME (Proved p) => (p, cxp) |
|
808 | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx))) |
|
809 |
|
810 fun result (p, (cx, _)) = (thm_of p, cx) |
|
811 in |
|
812 (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map Unproved ptab))) |
|
813 end |
|
814 |
|
815 fun reconstruct (output, {typs, terms, unfolds, assms}) ctxt = |
|
816 P.parse ctxt typs terms output |
|
817 |> (fn (idx, (ptab, vars, cx)) => prove cx unfolds assms vars (idx, ptab)) |
|
818 |
|
819 val setup = trace_assms_setup #> z3_rules_setup #> Z3_Simps.setup |
|
820 |
|
821 end |