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