1(* Copyright (c) 2009-2011 Tjark Weber. All rights reserved. *) 2 3(* Proof reconstruction for Z3: replaying Z3's proofs in HOL *) 4 5structure Z3_ProofReplay = 6struct 7 8local 9 10 fun profile name f x = 11 Profile.profile_with_exn_name name f x 12 13 open Z3_Proof 14 15 val ERR = Feedback.mk_HOL_ERR "Z3_ProofReplay" 16 val WARNING = Feedback.HOL_WARNING "Z3_ProofReplay" 17 18 val ALL_DISTINCT_NIL = HolSmtTheory.ALL_DISTINCT_NIL 19 val ALL_DISTINCT_CONS = HolSmtTheory.ALL_DISTINCT_CONS 20 val NOT_MEM_NIL = HolSmtTheory.NOT_MEM_NIL 21 val NOT_MEM_CONS = HolSmtTheory.NOT_MEM_CONS 22 val AND_T = HolSmtTheory.AND_T 23 val T_AND = HolSmtTheory.T_AND 24 val F_OR = HolSmtTheory.F_OR 25 val CONJ_CONG = HolSmtTheory.CONJ_CONG 26 val NOT_NOT_ELIM = HolSmtTheory.NOT_NOT_ELIM 27 val NOT_FALSE = HolSmtTheory.NOT_FALSE 28 val NNF_CONJ = HolSmtTheory.NNF_CONJ 29 val NNF_DISJ = HolSmtTheory.NNF_DISJ 30 val NNF_NOT_NOT = HolSmtTheory.NNF_NOT_NOT 31 val NEG_IFF_1_1 = HolSmtTheory.NEG_IFF_1_1 32 val NEG_IFF_1_2 = HolSmtTheory.NEG_IFF_1_2 33 val NEG_IFF_2_1 = HolSmtTheory.NEG_IFF_2_1 34 val NEG_IFF_2_2 = HolSmtTheory.NEG_IFF_2_2 35 val DISJ_ELIM_1 = HolSmtTheory.DISJ_ELIM_1 36 val DISJ_ELIM_2 = HolSmtTheory.DISJ_ELIM_2 37 val IMP_DISJ_1 = HolSmtTheory.IMP_DISJ_1 38 val IMP_DISJ_2 = HolSmtTheory.IMP_DISJ_2 39 val IMP_FALSE = HolSmtTheory.IMP_FALSE 40 val AND_IMP_INTRO_SYM = HolSmtTheory.AND_IMP_INTRO_SYM 41 val VALID_IFF_TRUE = HolSmtTheory.VALID_IFF_TRUE 42 43 (* a simplification prover that deals with function (i.e., array) 44 updates when the indices are integer or word literals *) 45 val SIMP_PROVE_UPDATE = simpLib.SIMP_PROVE (simpLib.&& (simpLib.++ 46 (intSimps.int_ss, simpLib.std_conv_ss {name = "word_EQ_CONV", 47 pats = [``(x :'a word) = y``], conv = wordsLib.word_EQ_CONV}), 48 [combinTheory.UPDATE_def, boolTheory.EQ_SYM_EQ])) [] 49 50 (***************************************************************************) 51 (* functions that manipulate/access "global" state *) 52 (***************************************************************************) 53 54 type state = { 55 (* keeps track of assumptions; (only) these may remain in the 56 final theorem *) 57 asserted_hyps : Term.term HOLset.set, 58 (* stores certain theorems (proved by 'rewrite' or 'th_lemma') for 59 later retrieval, to avoid re-reproving them *) 60 thm_cache : Thm.thm Net.net 61 } 62 63 fun state_assert (s : state) (t : Term.term) : state = 64 { 65 asserted_hyps = HOLset.add (#asserted_hyps s, t), 66 thm_cache = #thm_cache s 67 } 68 69 fun state_cache_thm (s : state) (thm : Thm.thm) : state = 70 { 71 asserted_hyps = #asserted_hyps s, 72 thm_cache = Net.insert (Thm.concl thm, thm) (#thm_cache s) 73 } 74 75 fun state_inst_cached_thm (s : state) (t : Term.term) : Thm.thm = 76 Lib.tryfind (* may fail *) 77 (fn thm => Drule.INST_TY_TERM (Term.match_term (Thm.concl thm) t) thm) 78 (Net.match t (#thm_cache s)) 79 80 (***************************************************************************) 81 (* auxiliary functions *) 82 (***************************************************************************) 83 84 (* |- l1 \/ l2 \/ ... \/ ln \/ t |- ~l1 |- ~l2 |- ... |- ~ln 85 ----------------------------------------------------------------- 86 |- t 87 88 The input clause (including "t") is really treated as a set of 89 literals: the resolvents need not be in the correct order, "t" 90 need not be the rightmost disjunct (and if "t" is a disjunction, 91 its disjuncts may even be spread throughout the input clause). 92 Note also that "t" may be F, in which case it need not be present 93 in the input clause. 94 95 We treat all "~li" as atomic, even if they are negated 96 disjunctions. *) 97 fun unit_resolution (thms, t) = 98 let 99 val _ = if List.null thms then 100 raise ERR "unit_resolution" "" 101 else () 102 fun disjuncts dict (disj, thm) = 103 let 104 val (l, r) = boolSyntax.dest_disj disj 105 (* |- l \/ r ==> ... *) 106 val thm = Thm.DISCH disj thm 107 val l_imp_concl = Thm.MP thm (Thm.DISJ1 (Thm.ASSUME l) r) 108 val r_imp_concl = Thm.MP thm (Thm.DISJ2 l (Thm.ASSUME r)) 109 in 110 disjuncts (disjuncts dict (l, l_imp_concl)) (r, r_imp_concl) 111 end 112 handle Feedback.HOL_ERR _ => 113 Redblackmap.insert (dict, disj, thm) 114 fun prove_from_disj dict disj = 115 Redblackmap.find (dict, disj) 116 handle Redblackmap.NotFound => 117 let 118 val (l, r) = boolSyntax.dest_disj disj 119 val l_th = prove_from_disj dict l 120 val r_th = prove_from_disj dict r 121 in 122 Thm.DISJ_CASES (Thm.ASSUME disj) l_th r_th 123 end 124 val dict = disjuncts (Redblackmap.mkDict Term.compare) (t, Thm.ASSUME t) 125 (* derive 't' from each negated resolvent *) 126 val dict = List.foldl (fn (th, dict) => 127 let 128 val lit = Thm.concl th 129 val (is_neg, neg_lit) = (true, boolSyntax.dest_neg lit) 130 handle Feedback.HOL_ERR _ => 131 (false, boolSyntax.mk_neg lit) 132 (* |- neg_lit ==> F *) 133 val th = if is_neg then 134 Thm.NOT_ELIM th 135 else 136 Thm.MP (Thm.SPEC lit NOT_FALSE) th 137 (* neg_lit |- t *) 138 val th = Thm.CCONTR t (Thm.MP th (Thm.ASSUME neg_lit)) 139 in 140 Redblackmap.insert (dict, neg_lit, th) 141 end) dict (List.tl thms) 142 (* derive 't' from ``F`` (just in case ``F`` is a disjunct) *) 143 val dict = Redblackmap.insert 144 (dict, boolSyntax.F, Thm.CCONTR t (Thm.ASSUME boolSyntax.F)) 145 val clause = Thm.concl (List.hd thms) 146 val clause_imp_t = prove_from_disj dict clause 147 in 148 Thm.MP (Thm.DISCH clause clause_imp_t) (List.hd thms) 149 end 150 151 (* e.g., "(A --> B) --> C --> D" acc ==> [A, B, C, D] @ acc *) 152 fun strip_fun_tys ty acc = 153 let 154 val (dom, rng) = Type.dom_rng ty 155 in 156 strip_fun_tys dom (strip_fun_tys rng acc) 157 end 158 handle Feedback.HOL_ERR _ => ty :: acc 159 160 (* approximate: only descends into combination terms and function types *) 161 fun term_contains_real_ty tm = 162 let val (rator, rand) = Term.dest_comb tm 163 in 164 term_contains_real_ty rator orelse term_contains_real_ty rand 165 end 166 handle Feedback.HOL_ERR _ => 167 List.exists (Lib.equal realSyntax.real_ty) 168 (strip_fun_tys (Term.type_of tm) []) 169 170 (* returns "|- l = r", provided 'l' and 'r' are conjunctions that can be 171 obtained from each other using associativity, commutativity and 172 idempotence of conjunction, and identity of "T" wrt. conjunction. 173 174 If 'r' is "F", 'l' must either contain "F" as a conjunct, or 'l' 175 must contain both a literal and its negation. *) 176 fun rewrite_conj (l, r) = 177 let 178 val Tl = boolSyntax.mk_conj (boolSyntax.T, l) 179 val Tr = boolSyntax.mk_conj (boolSyntax.T, r) 180 val Tl_eq_Tr = Drule.CONJUNCTS_AC (Tl, Tr) 181 in 182 Thm.MP (Drule.SPECL [l, r] T_AND) Tl_eq_Tr 183 end 184 handle Feedback.HOL_ERR _ => 185 if r = boolSyntax.F then 186 let 187 val l_imp_F = Thm.DISCH l (Library.gen_contradiction (Thm.ASSUME l)) 188 in 189 Drule.EQF_INTRO (Thm.NOT_INTRO l_imp_F) 190 end 191 else 192 raise ERR "rewrite_conj" "" 193 194 (* returns "|- l = r", provided 'l' and 'r' are disjunctions that can be 195 obtained from each other using associativity, commutativity and 196 idempotence of disjunction, and identity of "F" wrt. disjunction. 197 198 If 'r' is "T", 'l' must contain "T" as a disjunct, or 'l' must contain 199 both a literal and its negation. *) 200 fun rewrite_disj (l, r) = 201 let 202 val Fl = boolSyntax.mk_disj (boolSyntax.F, l) 203 val Fr = boolSyntax.mk_disj (boolSyntax.F, r) 204 val Fl_eq_Fr = Drule.DISJUNCTS_AC (Fl, Fr) 205 in 206 Thm.MP (Drule.SPECL [l, r] F_OR) Fl_eq_Fr 207 end 208 handle Feedback.HOL_ERR _ => 209 if r = boolSyntax.T then 210 Drule.EQT_INTRO (Library.gen_excluded_middle l) 211 else 212 raise ERR "rewrite_disj" "" 213 214 (* |- r1 /\ ... /\ rn = ~(s1 \/ ... \/ sn) 215 216 Note that q <=> p may be negated to p <=> ~q. Also, p <=> ~q may 217 be negated to p <=> q. *) 218 fun rewrite_nnf (l, r) = 219 let 220 val disj = boolSyntax.dest_neg r 221 val conj_ths = Drule.CONJUNCTS (Thm.ASSUME l) 222 (* transform equivalences in 'l' into equivalences as they appear 223 in 'disj' *) 224 val conj_dict = List.foldl (fn (th, dict) => Redblackmap.insert 225 (dict, Thm.concl th, th)) (Redblackmap.mkDict Term.compare) conj_ths 226 (* we map over equivalences in 'disj', possibly obtaining the 227 negation of each one by forward reasoning from a suitable 228 theorem in 'conj_dict' *) 229 val iff_ths = List.mapPartial (Lib.total (fn t => 230 let 231 val (p, q) = boolSyntax.dest_eq t (* may fail *) 232 val neg_q = boolSyntax.mk_neg q (* may fail (because of type) *) 233 in 234 let 235 val th = Redblackmap.find (conj_dict, boolSyntax.mk_eq (p, neg_q)) 236 in 237 (* l |- ~(p <=> q) *) 238 Thm.MP (Drule.SPECL [p, q] NEG_IFF_2_1) th 239 end 240 handle Redblackmap.NotFound => 241 let 242 val q = boolSyntax.dest_neg q (* may fail *) 243 val th = Redblackmap.find (conj_dict, boolSyntax.mk_eq (q, p)) 244 in 245 (* l |- ~(p <=> ~q) *) 246 Thm.MP (Drule.SPECL [p, q] NEG_IFF_1_1) th 247 end 248 end)) (boolSyntax.strip_disj disj) 249 (* [l, disj] |- F *) 250 val F_th = unit_resolution (Thm.ASSUME disj :: conj_ths @ iff_ths, 251 boolSyntax.F) 252 fun disjuncts dict (thmfun, concl) = 253 let 254 val (l, r) = boolSyntax.dest_disj concl (* may fail *) 255 in 256 disjuncts (disjuncts dict (fn th => thmfun (Thm.DISJ1 th r), l)) 257 (fn th => thmfun (Thm.DISJ2 l th), r) 258 end 259 handle Feedback.HOL_ERR _ => (* 'concl' is not a disjunction *) 260 let 261 (* |- concl ==> disjunction *) 262 val th = Thm.DISCH concl (thmfun (Thm.ASSUME concl)) 263 (* ~disjunction |- ~concl *) 264 val th = Drule.UNDISCH (Drule.CONTRAPOS th) 265 val th = Thm.MP (Thm.SPEC (boolSyntax.dest_neg concl) NOT_NOT_ELIM) th 266 handle Feedback.HOL_ERR _ => th 267 val t = Thm.concl th 268 val dict = Redblackmap.insert (dict, t, th) 269 in 270 (* if 't' is a negated equivalence, we check whether it can be 271 transformed into an equivalence that is present in 'l' *) 272 let 273 val (p, q) = boolSyntax.dest_eq (boolSyntax.dest_neg t) (* may fail *) 274 val neg_q = boolSyntax.mk_neg q (* may fail (because of type) *) 275 in 276 let 277 val _ = Redblackmap.find (conj_dict, boolSyntax.mk_eq (p, neg_q)) 278 (* ~disjunction |- p <=> ~q *) 279 val th1 = Thm.MP (Drule.SPECL [p, q] NEG_IFF_2_2) th 280 val dict = Redblackmap.insert (dict, Thm.concl th1, th1) 281 in 282 let 283 val q = boolSyntax.dest_neg q (* may fail *) 284 val _ = Redblackmap.find (conj_dict, boolSyntax.mk_eq (q, p)) 285 (* ~disjunction |- q <=> p *) 286 val th1 = Thm.MP (Drule.SPECL [p, q] NEG_IFF_1_2) th 287 in 288 Redblackmap.insert (dict, Thm.concl th1, th1) 289 end 290 handle Redblackmap.NotFound => dict 291 | Feedback.HOL_ERR _ => dict 292 end 293 handle Redblackmap.NotFound => 294 (* p <=> ~q is not a conjunction in 'l', so we skip 295 deriving it; but we possibly still need to derive 296 q <=> p *) 297 let 298 val q = boolSyntax.dest_neg q (* may fail *) 299 val _ = Redblackmap.find (conj_dict, boolSyntax.mk_eq (q, p)) 300 (* ~disjunction |- q <=> p *) 301 val th1 = Thm.MP (Drule.SPECL [p, q] NEG_IFF_1_2) th 302 in 303 Redblackmap.insert (dict, Thm.concl th1, th1) 304 end 305 handle Redblackmap.NotFound => dict 306 | Feedback.HOL_ERR _ => dict 307 end 308 handle Feedback.HOL_ERR _ => (* 't' is not an equivalence *) 309 dict 310 end (* disjuncts *) 311 val dict = disjuncts (Redblackmap.mkDict Term.compare) (Lib.I, disj) 312 (* derive ``T`` (just in case ``T`` is a conjunct) *) 313 val dict = Redblackmap.insert (dict, boolSyntax.T, boolTheory.TRUTH) 314 (* proves a conjunction 'conj', provided each conjunct is proved 315 in 'dict' *) 316 fun prove_conj dict conj = 317 Redblackmap.find (dict, conj) 318 handle Redblackmap.NotFound => 319 let 320 val (l, r) = boolSyntax.dest_conj conj 321 in 322 Thm.CONJ (prove_conj dict l) (prove_conj dict r) 323 end 324 val r_imp_l = Thm.DISCH r (prove_conj dict l) 325 val l_imp_r = Thm.DISCH l (Thm.NOT_INTRO (Thm.DISCH disj F_th)) 326 in 327 Drule.IMP_ANTISYM_RULE l_imp_r r_imp_l 328 end 329 330 (* returns |- ~MEM x [a; b; c] = x <> a /\ x <> b /\ x <> c; fails 331 if not applied to a term of the form ``~MEM x [a; b; c]`` *) 332 fun NOT_MEM_CONV tm = 333 let 334 val (x, list) = listSyntax.dest_mem (boolSyntax.dest_neg tm) 335 in 336 let 337 val (h, t) = listSyntax.dest_cons list 338 (* |- ~MEM x (h::t) = (x <> h) /\ ~MEM x t *) 339 val th1 = Drule.ISPECL [x, h, t] NOT_MEM_CONS 340 val (neq, notmem) = boolSyntax.dest_conj (boolSyntax.rhs 341 (Thm.concl th1)) 342 (* |- ~MEM x t = rhs *) 343 val th2 = NOT_MEM_CONV notmem 344 (* |- (x <> h) /\ ~MEM x t = (x <> h) /\ rhs *) 345 val th3 = Thm.AP_TERM (Term.mk_comb (boolSyntax.conjunction, neq)) th2 346 (* |- ~MEM x (h::t) = (x <> h) /\ rhs *) 347 val th4 = Thm.TRANS th1 th3 348 in 349 if boolSyntax.rhs (Thm.concl th2) = boolSyntax.T then 350 Thm.TRANS th4 (Thm.SPEC neq AND_T) 351 else 352 th4 353 end 354 handle Feedback.HOL_ERR _ => (* 'list' is not a cons *) 355 if listSyntax.is_nil list then 356 (* |- ~MEM x [] = T *) 357 Drule.ISPEC x NOT_MEM_NIL 358 else 359 raise ERR "NOT_MEM_CONV" "" 360 end 361 362 (* returns "|- ALL_DISTINCT [x; y; z] = (x <> y /\ x <> z) /\ y <> 363 z" (note the parentheses); fails if not applied to a term of the 364 form ``ALL_DISTINCT [x; y; z]`` *) 365 fun ALL_DISTINCT_CONV tm = 366 let 367 val list = listSyntax.dest_all_distinct tm 368 in 369 let 370 val (h, t) = listSyntax.dest_cons list 371 (* |- ALL_DISTINCT (h::t) = ~MEM h t /\ ALL_DISTINCT t *) 372 val th1 = Drule.ISPECL [h, t] ALL_DISTINCT_CONS 373 val (notmem, alldistinct) = boolSyntax.dest_conj 374 (boolSyntax.rhs (Thm.concl th1)) 375 (* |- ~MEM h t = something *) 376 val th2 = NOT_MEM_CONV notmem 377 val something = boolSyntax.rhs (Thm.concl th2) 378 (* |- ALL_DISTINCT t = rhs *) 379 val th3 = ALL_DISTINCT_CONV alldistinct 380 val rhs = boolSyntax.rhs (Thm.concl th3) 381 val th4 = Drule.SPECL [notmem, something, alldistinct, rhs] CONJ_CONG 382 (* |- ~MEM h t /\ ALL_DISTINCT t = something /\ rhs *) 383 val th5 = Thm.MP (Thm.MP th4 th2) th3 384 (* |- ALL_DISTINCT (h::t) = something /\ rhs *) 385 val th6 = Thm.TRANS th1 th5 386 in 387 if rhs = boolSyntax.T then 388 Thm.TRANS th6 (Thm.SPEC something AND_T) 389 else 390 th6 391 end 392 handle Feedback.HOL_ERR _ => (* 'list' is not a cons *) 393 (* |- ALL_DISTINCT [] = T *) 394 Thm.INST_TYPE [{redex = Type.alpha, residue = listSyntax.dest_nil list}] 395 ALL_DISTINCT_NIL 396 end 397 398 (* returns |- (x = y) = (y = x), provided ``y = x`` is LESS than ``x 399 = y`` wrt. Term.compare; fails if applied to a term that is not 400 an equation; may raise Conv.UNCHANGED *) 401 fun REORIENT_SYM_CONV tm = 402 let 403 val tm' = boolSyntax.mk_eq (Lib.swap (boolSyntax.dest_eq tm)) 404 in 405 if Term.compare (tm', tm) = LESS then 406 Conv.SYM_CONV tm 407 else 408 raise Conv.UNCHANGED 409 end 410 411 (* returns |- ALL_DISTINCT ... /\ T = ... *) 412 fun rewrite_all_distinct (l, r) = 413 let 414 fun ALL_DISTINCT_AND_T_CONV t = 415 ALL_DISTINCT_CONV t 416 handle Feedback.HOL_ERR _ => 417 let 418 val all_distinct = Lib.fst (boolSyntax.dest_conj t) 419 val all_distinct_th = ALL_DISTINCT_CONV all_distinct 420 in 421 Thm.TRANS (Thm.SPEC all_distinct AND_T) all_distinct_th 422 end 423 val REORIENT_CONV = Conv.ONCE_DEPTH_CONV REORIENT_SYM_CONV 424 (* since ALL_DISTINCT may be present in both 'l' and 'r', we 425 normalize both 'l' and 'r' *) 426 val l_eq_l' = Conv.THENC (ALL_DISTINCT_AND_T_CONV, REORIENT_CONV) l 427 val r_eq_r' = Conv.THENC (fn t => ALL_DISTINCT_AND_T_CONV t 428 handle Feedback.HOL_ERR _ => raise Conv.UNCHANGED, REORIENT_CONV) r 429 handle Conv.UNCHANGED => Thm.REFL r 430 (* get rid of parentheses *) 431 val l'_eq_r' = Drule.CONJUNCTS_AC (boolSyntax.rhs (Thm.concl l_eq_l'), 432 boolSyntax.rhs (Thm.concl r_eq_r')) 433 in 434 Thm.TRANS (Thm.TRANS l_eq_l' l'_eq_r') (Thm.SYM r_eq_r') 435 end 436 437 (* replaces distinct if-then-else terms by distinct variables; 438 returns the generalized term and a map from ite-subterms to 439 variables (treating anything but combinations as atomic, i.e., 440 this function does NOT descend into lambda-abstractions) *) 441 fun generalize_ite t = 442 let 443 fun aux (dict, t) = 444 if boolSyntax.is_cond t then ( 445 case Redblackmap.peek (dict, t) of 446 SOME var => 447 (dict, var) 448 | NONE => 449 let 450 val var = Term.genvar (Term.type_of t) 451 in 452 (Redblackmap.insert (dict, t, var), var) 453 end 454 ) else ( 455 let 456 val (l, r) = Term.dest_comb t 457 val (dict, l) = aux (dict, l) 458 val (dict, r) = aux (dict, r) 459 in 460 (dict, Term.mk_comb (l, r)) 461 end 462 handle Feedback.HOL_ERR _ => 463 (* 't' is not a combination *) 464 (dict, t) 465 ) 466 in 467 aux (Redblackmap.mkDict Term.compare, t) 468 end 469 470 (***************************************************************************) 471 (* implementation of Z3's inference rules *) 472 (***************************************************************************) 473 474 (* The Z3 documentation is rather outdated (as of version 2.11) and 475 imprecise with respect to the semantics of Z3's inference rules. 476 Ultimately, the most reliable way to determine the semantics is 477 by observation: I applied Z3 to a large collection of SMT-LIB 478 benchmarks, and from the resulting proofs I inferred what each 479 inference rule does. Therefore the implementation below may not 480 cover rare corner cases that were not exercised by any benchmark 481 in the collection. *) 482 483 fun z3_and_elim (state, thm, t) = 484 (state, Library.conj_elim (thm, t)) 485 486 fun z3_asserted (state, t) = 487 (state_assert state t, Thm.ASSUME t) 488 489 fun z3_commutativity (state, t) = 490 let 491 val (x, y) = boolSyntax.dest_eq (boolSyntax.lhs t) 492 in 493 (state, Drule.ISPECL [x, y] boolTheory.EQ_SYM_EQ) 494 end 495 496 (* Instances of Tseitin-style propositional tautologies: 497 (or (not (and p q)) p) 498 (or (not (and p q)) q) 499 (or (and p q) (not p) (not q)) 500 (or (not (or p q)) p q) 501 (or (or p q) (not p)) 502 (or (or p q) (not q)) 503 (or (not (iff p q)) (not p) q) 504 (or (not (iff p q)) p (not q)) 505 (or (iff p q) (not p) (not q)) 506 (or (iff p q) p q) 507 (or (not (ite a b c)) (not a) b) 508 (or (not (ite a b c)) a c) 509 (or (ite a b c) (not a) (not b)) 510 (or (ite a b c) a (not c)) 511 (or (not (not a)) (not a)) 512 (or (not a) a) 513 514 Also 515 (or p (= x (ite p y x))) 516 517 Also 518 ~ALL_DISTINCT [x; y; z] \/ (x <> y /\ x <> z /\ y <> z) 519 ~(ALL_DISTINCT [x; y; z] /\ T) \/ (x <> y /\ x <> z /\ y <> z) 520 521 There is a complication: 't' may contain arbitarily many 522 irrelevant (nested) conjuncts/disjuncts, i.e., 523 conjunction/disjunction in the above tautologies can be of 524 arbitrary arity. 525 526 For the most part, 'z3_def_axiom' could be implemented by a 527 single call to TAUT_PROVE. The (partly less general) 528 implementation below, however, is considerably faster. 529 *) 530 fun z3_def_axiom (state, t) = 531 (state, Z3_ProformaThms.prove Z3_ProformaThms.def_axiom_thms t) 532 handle Feedback.HOL_ERR _ => 533 (* or (or ... p ...) (not p) *) 534 (* or (or ... (not p) ...) p *) 535 (state, Library.gen_excluded_middle t) 536 handle Feedback.HOL_ERR _ => 537 (* (or (not (and ... p ...)) p) *) 538 let 539 val (lhs, rhs) = boolSyntax.dest_disj t 540 val conj = boolSyntax.dest_neg lhs 541 (* conj |- rhs *) 542 val thm = Library.conj_elim (Thm.ASSUME conj, rhs) (* may fail *) 543 in 544 (* |- lhs \/ rhs *) 545 (state, Drule.IMP_ELIM (Thm.DISCH conj thm)) 546 end 547 handle Feedback.HOL_ERR _ => 548 (* ~ALL_DISTINCT [x; y; z] \/ x <> y /\ x <> z /\ y <> z *) 549 (* ~(ALL_DISTINCT [x; y; z] /\ T) \/ x <> y /\ x <> z /\ y <> z *) 550 let 551 val (l, r) = boolSyntax.dest_disj t 552 val all_distinct = boolSyntax.dest_neg l 553 val all_distinct_th = ALL_DISTINCT_CONV all_distinct 554 handle Feedback.HOL_ERR _ => 555 let 556 val all_distinct = Lib.fst (boolSyntax.dest_conj all_distinct) 557 val all_distinct_th = ALL_DISTINCT_CONV all_distinct 558 in 559 Thm.TRANS (Thm.SPEC all_distinct AND_T) all_distinct_th 560 end 561 (* get rid of parentheses *) 562 val l_eq_r = Thm.TRANS all_distinct_th (Drule.CONJUNCTS_AC 563 (boolSyntax.rhs (Thm.concl all_distinct_th), r)) 564 in 565 (state, Drule.IMP_ELIM (Lib.fst (Thm.EQ_IMP_RULE l_eq_r))) 566 end 567 568 (* (!x y z. P) = P *) 569 fun z3_elim_unused (state, t) = 570 let 571 val (lhs, rhs) = boolSyntax.dest_eq t 572 fun strip_some_foralls forall = 573 let 574 val (var, body) = boolSyntax.dest_forall forall 575 val th1 = Thm.DISCH forall (Thm.SPEC var (Thm.ASSUME forall)) 576 val th2 = Thm.DISCH body (Thm.GEN var (Thm.ASSUME body)) 577 val strip_th = Drule.IMP_ANTISYM_RULE th1 th2 578 in 579 if body = rhs then 580 strip_th (* stripped enough quantifiers *) 581 else 582 Thm.TRANS strip_th (strip_some_foralls body) 583 end 584 in 585 (state, strip_some_foralls lhs) 586 end 587 588 (* introduces a local hypothesis (which must be discharged by 589 'z3_lemma' at some later point in the proof) *) 590 fun z3_hypothesis (state, t) = 591 (state, Thm.ASSUME t) 592 593 (* ... |- p 594 ------------ 595 ... |- p = T *) 596 fun z3_iff_true (state, thm, _) = 597 (state, Thm.MP (Thm.SPEC (Thm.concl thm) VALID_IFF_TRUE) thm) 598 599 (* [l1, ..., ln] |- F 600 -------------------- 601 |- ~l1 \/ ... \/ ~ln 602 603 'z3_lemma' could be implemented (essentially) by a single call to 604 'TAUT_PROVE'. The (less general) implementation below, however, 605 is considerably faster. *) 606 fun z3_lemma (state, thm, t) = 607 let 608 fun prove_literal maybe_no_hyp (th, lit) = 609 let 610 val (is_neg, neg_lit) = (true, boolSyntax.dest_neg lit) 611 handle Feedback.HOL_ERR _ => (false, boolSyntax.mk_neg lit) 612 in 613 if maybe_no_hyp orelse HOLset.member (Thm.hypset th, neg_lit) then 614 let 615 val concl = Thm.concl th 616 val th1 = Thm.DISCH neg_lit th 617 in 618 if is_neg then ( 619 if concl = boolSyntax.F then 620 (* [...] |- ~neg_lit *) 621 Thm.NOT_INTRO th1 622 else 623 (* [...] |- ~neg_lit \/ concl *) 624 Thm.MP (Drule.SPECL [neg_lit, concl] IMP_DISJ_1) th1 625 ) else 626 if concl = boolSyntax.F then 627 (* [...] |- lit *) 628 Thm.MP (Thm.SPEC lit IMP_FALSE) th1 629 else 630 (* [...] |- lit \/ concl *) 631 Thm.MP (Drule.SPECL [lit, concl] IMP_DISJ_2) th1 632 end 633 else 634 raise ERR "z3_lemma" "" 635 end 636 fun prove (th, disj) = 637 prove_literal false (th, disj) 638 handle Feedback.HOL_ERR _ => 639 let 640 val (l, r) = boolSyntax.dest_disj disj 641 in 642 (* We do NOT break 'l' apart recursively (because that would be 643 slightly tricky to implement, and require associativity of 644 disjunction). Thus, 't' must be parenthesized to the right 645 (e.g., "l1 \/ (l2 \/ l3)"). *) 646 prove_literal true (prove (th, r), l) 647 end 648 in 649 (state, prove (thm, t)) 650 end 651 652 (* |- l1 = r1 ... |- ln = rn 653 ---------------------------- 654 |- f l1 ... ln = f r1 ... rn *) 655 fun z3_monotonicity (state, thms, t) = 656 let 657 val l_r_thms = List.map 658 (fn thm => (boolSyntax.dest_eq (Thm.concl thm), thm)) thms 659 fun make_equal (l, r) = 660 Thm.ALPHA l r 661 handle Feedback.HOL_ERR _ => 662 Lib.tryfind (fn ((l', r'), thm) => 663 Thm.TRANS (Thm.ALPHA l l') (Thm.TRANS thm (Thm.ALPHA r' r)) 664 handle Feedback.HOL_ERR _ => 665 Thm.TRANS (Thm.ALPHA l r') 666 (Thm.TRANS (Thm.SYM thm) (Thm.ALPHA l' r))) l_r_thms 667 handle Feedback.HOL_ERR _ => 668 let 669 val (l_op, l_arg) = Term.dest_comb l 670 val (r_op, r_arg) = Term.dest_comb r 671 in 672 Thm.MK_COMB (make_equal (l_op, r_op), make_equal (l_arg, r_arg)) 673 end 674 val (l, r) = boolSyntax.dest_eq t 675 val thm = make_equal (l, r) 676 handle Feedback.HOL_ERR _ => 677 (* surprisingly, 'l' is sometimes of the form ``x /\ y ==> z`` 678 and must be transformed into ``x ==> y ==> z`` before any 679 of the theorems in 'thms' can be applied - this is arguably 680 a bug in Z3 (2.11) *) 681 let 682 val (xy, z) = boolSyntax.dest_imp l 683 val (x, y) = boolSyntax.dest_conj xy 684 val th1 = Drule.SPECL [x, y, z] AND_IMP_INTRO_SYM 685 val l' = Lib.snd (boolSyntax.dest_eq (Thm.concl th1)) 686 in 687 Thm.TRANS th1 (make_equal (l', r)) 688 end 689 in 690 (state, thm) 691 end 692 693 fun z3_mp (state, thm1, thm2, t) = 694 (state, Thm.MP thm2 thm1 handle Feedback.HOL_ERR _ => Thm.EQ_MP thm2 thm1) 695 696 (* ~(... \/ p \/ ...) 697 ------------------ 698 ~p *) 699 fun z3_not_or_elim (state, thm, t) = 700 let 701 val (is_neg, neg_t) = (true, boolSyntax.dest_neg t) 702 handle Feedback.HOL_ERR _ => 703 (false, boolSyntax.mk_neg t) 704 val disj = boolSyntax.dest_neg (Thm.concl thm) 705 (* neg_t |- disj *) 706 val th1 = Library.disj_intro (Thm.ASSUME neg_t, disj) 707 (* |- ~disj ==> ~neg_t *) 708 val th1 = Drule.CONTRAPOS (Thm.DISCH neg_t th1) 709 (* |- ~neg_t *) 710 val th1 = Thm.MP th1 thm 711 in 712 (state, if is_neg then th1 else Thm.MP (Thm.SPEC t NOT_NOT_ELIM) th1) 713 end 714 715 (* P = Q 716 --------------------- 717 (!x. P x) = (!y. Q y) *) 718 fun z3_quant_intro (state, thm, t) = 719 let 720 val (lhs, rhs) = boolSyntax.dest_eq t 721 val (bvars, _) = boolSyntax.strip_forall lhs 722 (* P may be a quantified proposition itself; only retain *new* 723 quantifiers *) 724 val (P, _) = boolSyntax.dest_eq (Thm.concl thm) 725 val bvars = List.take (bvars, List.length bvars - 726 List.length (Lib.fst (boolSyntax.strip_forall P))) 727 (* P and Q in the conclusion may require variable renaming to match 728 the premise -- we only look at P and hope Q will come out right *) 729 fun strip_some_foralls 0 term = 730 term 731 | strip_some_foralls n term = 732 strip_some_foralls (n - 1) (Lib.snd (boolSyntax.dest_forall term)) 733 val len = List.length bvars 734 val (tmsubst, _) = Term.match_term P (strip_some_foralls len lhs) 735 val thm = Thm.INST tmsubst thm 736 (* add quantifiers (on both sides) *) 737 val thm = List.foldr (fn (bvar, th) => Drule.FORALL_EQ bvar th) 738 thm bvars 739 (* rename bvars on rhs if necessary *) 740 val (_, intermediate_rhs) = boolSyntax.dest_eq (Thm.concl thm) 741 val thm = Thm.TRANS thm (Thm.ALPHA intermediate_rhs rhs) 742 in 743 (state, thm) 744 end 745 746 fun z3_rewrite (state, t) = 747 let 748 val (l, r) = boolSyntax.dest_eq t 749 in 750 if l = r then 751 (state, Thm.REFL l) 752 else 753 (* proforma theorems *) 754 (state, profile "rewrite(01)(proforma)" 755 (Z3_ProformaThms.prove Z3_ProformaThms.rewrite_thms) t) 756 handle Feedback.HOL_ERR _ => 757 758 (* cached theorems *) 759 (state, profile "rewrite(02)(cache)" (state_inst_cached_thm state) t) 760 handle Feedback.HOL_ERR _ => 761 762 (* re-ordering conjunctions and disjunctions *) 763 profile "rewrite(04)(conj/disj)" (fn () => 764 if boolSyntax.is_conj l then 765 (state, profile "rewrite(04.1)(conj)" rewrite_conj (l, r)) 766 else if boolSyntax.is_disj l then 767 (state, profile "rewrite(04.2)(disj)" rewrite_disj (l, r)) 768 else 769 raise ERR "" "") () 770 handle Feedback.HOL_ERR _ => 771 772 (* |- r1 /\ ... /\ rn = ~(s1 \/ ... \/ sn) *) 773 (state, profile "rewrite(05)(nnf)" rewrite_nnf (l, r)) 774 handle Feedback.HOL_ERR _ => 775 776 (* at this point, we should have dealt with all propositional 777 tautologies (i.e., 'tautLib.TAUT_PROVE t' should fail here) *) 778 779 (* |- ALL_DISTINCT ... /\ T = ... *) 780 (state, profile "rewrite(06)(all_distinct)" rewrite_all_distinct (l, r)) 781 handle Feedback.HOL_ERR _ => 782 783 let 784 val thm = profile "rewrite(07)(SIMP_PROVE_UPDATE)" SIMP_PROVE_UPDATE t 785 handle Feedback.HOL_ERR _ => 786 787 profile "rewrite(08)(WORD_DP)" (wordsLib.WORD_DP 788 (bossLib.SIMP_CONV (bossLib.++ (bossLib.++ (bossLib.arith_ss, 789 wordsLib.WORD_ss), wordsLib.WORD_EXTRACT_ss)) []) 790 (Drule.EQT_ELIM o (bossLib.SIMP_CONV bossLib.arith_ss []))) t 791 handle Feedback.HOL_ERR _ => 792 793 profile "rewrite(09)(WORD_ARITH_CONV)" (fn () => 794 Drule.EQT_ELIM (wordsLib.WORD_ARITH_CONV t) 795 handle Conv.UNCHANGED => raise ERR "" "") () 796 handle Feedback.HOL_ERR _ => 797 798 profile "rewrite(10)(BBLAST)" blastLib.BBLAST_PROVE t 799 handle Feedback.HOL_ERR _ => 800 801 if term_contains_real_ty t then 802 profile "rewrite(11.1)(REAL_ARITH)" realLib.REAL_ARITH t 803 else 804 profile "rewrite(11.2)(ARITH_PROVE)" intLib.ARITH_PROVE t 805 in 806 (state_cache_thm state thm, thm) 807 end 808 end 809 810 fun z3_symm (state, thm, t) = 811 (state, Thm.SYM thm) 812 813 fun th_lemma_wrapper (name : string) 814 (th_lemma_implementation : state * Term.term -> state * Thm.thm) 815 (state, thms, t) : state * Thm.thm = 816 let 817 val t' = boolSyntax.list_mk_imp (List.map Thm.concl thms, t) 818 val (state, thm) = (state, 819 (* proforma theorems *) 820 profile ("th_lemma[" ^ name ^ "](1)(proforma)") 821 (Z3_ProformaThms.prove Z3_ProformaThms.th_lemma_thms) t' 822 handle Feedback.HOL_ERR _ => 823 (* cached theorems *) 824 profile ("th_lemma[" ^ name ^ "](2)(cache)") 825 (state_inst_cached_thm state) t') 826 handle Feedback.HOL_ERR _ => 827 (* do actual work to derive the theorem *) 828 th_lemma_implementation (state, t') 829 in 830 (state, Drule.LIST_MP thms thm) 831 end 832 833 val z3_th_lemma_arith = th_lemma_wrapper "arith" (fn (state, t) => 834 let 835 val (dict, t') = generalize_ite t 836 val thm = if term_contains_real_ty t' then 837 (* this is just a heuristic - it is quite conceivable that a 838 term that contains type real is provable by integer 839 arithmetic *) 840 profile "th_lemma[arith](3.1)(real)" realLib.REAL_ARITH t' 841 else 842 profile "th_lemma[arith](3.2)(int)" intLib.ARITH_PROVE t' 843 val subst = List.map (fn (term, var) => {redex = var, residue = term}) 844 (Redblackmap.listItems dict) 845 in 846 (* cache 'thm', instantiate to undo 'generalize_ite' *) 847 (state_cache_thm state thm, Thm.INST subst thm) 848 end) 849 850 val z3_th_lemma_array = th_lemma_wrapper "array" (fn (state, t) => 851 let 852 val thm = profile "th_lemma[array](3)(SIMP_PROVE_UPDATE)" 853 SIMP_PROVE_UPDATE t 854 in 855 (* cache 'thm' *) 856 (state_cache_thm state thm, thm) 857 end) 858 859 val z3_th_lemma_basic = th_lemma_wrapper "basic" (fn (state, t) => 860 (*TODO: not implemented yet*) 861 raise ERR "" "") 862 863 val z3_th_lemma_bv = 864 let 865 (* TODO: I would like to find out whether PURE_REWRITE_TAC is 866 faster than SIMP_TAC here. However, using the former 867 instead of the latter causes HOL4 to segfault on various 868 SMT-LIB benchmark proofs. So far I do not know the reason 869 for these segfaults. *) 870 val COND_REWRITE_TAC = (*Rewrite.PURE_REWRITE_TAC*) simpLib.SIMP_TAC 871 simpLib.empty_ss [boolTheory.COND_RAND, boolTheory.COND_RATOR] 872 in 873 th_lemma_wrapper "bv" (fn (state, t) => 874 let 875 val thm = profile "th_lemma[bv](3)(WORD_BIT_EQ)" (fn () => 876 Drule.EQT_ELIM (Conv.THENC (simpLib.SIMP_CONV (simpLib.++ 877 (simpLib.++ (bossLib.std_ss, wordsLib.WORD_ss), 878 wordsLib.WORD_BIT_EQ_ss)) [], tautLib.TAUT_CONV) t)) () 879 handle Feedback.HOL_ERR _ => 880 881 profile "th_lemma[bv](4)(COND_BBLAST)" Tactical.prove (t, 882 Tactical.THEN (profile "th_lemma[bv](4.1)(COND_REWRITE_TAC)" 883 COND_REWRITE_TAC, profile "th_lemma[bv](4.2)(BBLAST_TAC)" 884 blastLib.BBLAST_TAC)) 885 in 886 (* cache 'thm' *) 887 (state_cache_thm state thm, thm) 888 end) 889 end 890 891 fun z3_trans (state, thm1, thm2, t) = 892 (state, Thm.TRANS thm1 thm2) 893 894 fun z3_true_axiom (state, t) = 895 (state, boolTheory.TRUTH) 896 897 fun z3_unit_resolution (state, thms, t) = 898 (state, unit_resolution (thms, t)) 899 900 (* end of inference rule implementations *) 901 902 (***************************************************************************) 903 (* proof traversal, turning proofterms into theorems *) 904 (***************************************************************************) 905 906 (* We use a depth-first post-order traversal of the proof, checking 907 each premise of a proofterm (i.e., deriving the corresponding 908 theorem) before checking the proofterm's inference itself. 909 Proofterms that have proof IDs then cause the proof to be updated 910 (at this ID) immediately after they have been checked, so that 911 future uses of the same proof ID merely require a lookup in the 912 proof (rather than a new derivation of the theorem). To achieve 913 a tail-recursive implementation, we use continuation-passing 914 style. *) 915 916 fun check_thm (name, thm, concl) = 917 if Thm.concl thm <> concl then 918 raise ERR "check_thm" (name ^ ": conclusion is " ^ Hol_pp.term_to_string 919 (Thm.concl thm) ^ ", expected: " ^ Hol_pp.term_to_string concl) 920 else if !Library.trace > 2 then 921 Feedback.HOL_MESG 922 ("HolSmtLib: " ^ name ^ " proved: " ^ Hol_pp.thm_to_string thm) 923 else () 924 925 fun zero_prems (state : state, proof : proof) 926 (name : string) 927 (z3_rule_fn : state * Term.term -> state * Thm.thm) 928 (concl : Term.term) 929 (continuation : (state * proof) * Thm.thm -> (state * proof) * Thm.thm) 930 : (state * proof) * Thm.thm = 931 let 932 val (state, thm) = profile name z3_rule_fn (state, concl) 933 handle Feedback.HOL_ERR _ => 934 raise ERR name (Hol_pp.term_to_string concl) 935 val _ = profile "check_thm" check_thm (name, thm, concl) 936 in 937 continuation ((state, proof), thm) 938 end 939 940 fun one_prem (state_proof : state * proof) 941 (name : string) 942 (z3_rule_fn : state * Thm.thm * Term.term -> state * Thm.thm) 943 (pt : proofterm, concl : Term.term) 944 (continuation : (state * proof) * Thm.thm -> (state * proof) * Thm.thm) 945 : (state * proof) * Thm.thm = 946 thm_of_proofterm (state_proof, pt) (continuation o 947 (fn ((state, proof), thm) => 948 let 949 val (state, thm) = profile name z3_rule_fn (state, thm, concl) 950 handle Feedback.HOL_ERR _ => 951 raise ERR name (Hol_pp.thm_to_string thm ^ ", " ^ 952 Hol_pp.term_to_string concl) 953 val _ = profile "check_thm" check_thm (name, thm, concl) 954 in 955 ((state, proof), thm) 956 end)) 957 958 and two_prems (state_proof : state * proof) 959 (name : string) 960 (z3_rule_fn : state * Thm.thm * Thm.thm * Term.term -> state * Thm.thm) 961 (pt1 : proofterm, pt2 : proofterm, concl : Term.term) 962 (continuation : (state * proof) * Thm.thm -> (state * proof) * Thm.thm) 963 : (state * proof) * Thm.thm = 964 thm_of_proofterm (state_proof, pt1) (continuation o 965 (fn (state_proof, thm1) => 966 thm_of_proofterm (state_proof, pt2) (fn ((state, proof), thm2) => 967 let 968 val (state, thm) = profile name z3_rule_fn 969 (state, thm1, thm2, concl) 970 handle Feedback.HOL_ERR _ => 971 raise ERR name (Hol_pp.thm_to_string thm1 ^ ", " ^ 972 Hol_pp.thm_to_string thm2 ^ ", " ^ 973 Hol_pp.term_to_string concl) 974 val _ = profile "check_thm" check_thm (name, thm, concl) 975 in 976 ((state, proof), thm) 977 end))) 978 979 and list_prems (state : state, proof : proof) 980 (name : string) 981 (z3_rule_fn : state * Thm.thm list * Term.term -> state * Thm.thm) 982 ([] : proofterm list, concl : Term.term) 983 (continuation : (state * proof) * Thm.thm -> (state * proof) * Thm.thm) 984 (acc : Thm.thm list) 985 : (state * proof) * Thm.thm = 986 let 987 val acc = List.rev acc 988 val (state, thm) = profile name z3_rule_fn (state, acc, concl) 989 handle Feedback.HOL_ERR _ => 990 raise ERR name ("[" ^ String.concatWith ", " (List.map 991 Hol_pp.thm_to_string acc) ^ "], " ^ Hol_pp.term_to_string concl) 992 val _ = profile "check_thm" check_thm (name, thm, concl) 993 in 994 continuation ((state, proof), thm) 995 end 996 | list_prems (state_proof : state * proof) 997 (name : string) 998 (z3_rule_fn : state * Thm.thm list * Term.term -> state * Thm.thm) 999 (pt :: pts : proofterm list, concl : Term.term) 1000 (continuation : (state * proof) * Thm.thm -> (state * proof) * Thm.thm) 1001 (acc : Thm.thm list) 1002 : (state * proof) * Thm.thm = 1003 thm_of_proofterm (state_proof, pt) (fn (state_proof, thm) => 1004 list_prems state_proof name z3_rule_fn (pts, concl) continuation 1005 (thm :: acc)) 1006 1007 and thm_of_proofterm (state_proof, AND_ELIM x) continuation = 1008 one_prem state_proof "and_elim" z3_and_elim x continuation 1009 | thm_of_proofterm (state_proof, ASSERTED x) continuation = 1010 zero_prems state_proof "asserted" z3_asserted x continuation 1011 | thm_of_proofterm (state_proof, COMMUTATIVITY x) continuation = 1012 zero_prems state_proof "commutativity" z3_commutativity x continuation 1013 | thm_of_proofterm (state_proof, DEF_AXIOM x) continuation = 1014 zero_prems state_proof "def_axiom" z3_def_axiom x continuation 1015 | thm_of_proofterm (state_proof, ELIM_UNUSED x) continuation = 1016 zero_prems state_proof "elim_unused" z3_elim_unused x continuation 1017 | thm_of_proofterm (state_proof, HYPOTHESIS x) continuation = 1018 zero_prems state_proof "hypothesis" z3_hypothesis x continuation 1019 | thm_of_proofterm (state_proof, IFF_TRUE x) continuation = 1020 one_prem state_proof "iff_true" z3_iff_true x continuation 1021 | thm_of_proofterm (state_proof, LEMMA x) continuation = 1022 one_prem state_proof "lemma" z3_lemma x continuation 1023 | thm_of_proofterm (state_proof, MONOTONICITY x) continuation = 1024 list_prems state_proof "monotonicity" z3_monotonicity x continuation [] 1025 | thm_of_proofterm (state_proof, MP x) continuation = 1026 two_prems state_proof "mp" z3_mp x continuation 1027 | thm_of_proofterm (state_proof, NOT_OR_ELIM x) continuation = 1028 one_prem state_proof "not_or_elim" z3_not_or_elim x continuation 1029 | thm_of_proofterm (state_proof, QUANT_INTRO x) continuation = 1030 one_prem state_proof "quant_intro" z3_quant_intro x continuation 1031 | thm_of_proofterm (state_proof, REWRITE x) continuation = 1032 zero_prems state_proof "rewrite" z3_rewrite x continuation 1033 | thm_of_proofterm (state_proof, SYMM x) continuation = 1034 one_prem state_proof "symm" z3_symm x continuation 1035 | thm_of_proofterm (state_proof, TH_LEMMA_ARITH x) continuation = 1036 list_prems state_proof "th_lemma[arith]" z3_th_lemma_arith x 1037 continuation [] 1038 | thm_of_proofterm (state_proof, TH_LEMMA_ARRAY x) continuation = 1039 list_prems state_proof "th_lemma[array]" z3_th_lemma_array x 1040 continuation [] 1041 | thm_of_proofterm (state_proof, TH_LEMMA_BASIC x) continuation = 1042 list_prems state_proof "th_lemma[basic]" z3_th_lemma_basic x 1043 continuation [] 1044 | thm_of_proofterm (state_proof, TH_LEMMA_BV x) continuation = 1045 list_prems state_proof "th_lemma[bv]" z3_th_lemma_bv x continuation [] 1046 | thm_of_proofterm (state_proof, TRANS x) continuation = 1047 two_prems state_proof "trans" z3_trans x continuation 1048 | thm_of_proofterm (state_proof, TRUE_AXIOM x) continuation = 1049 zero_prems state_proof "true_axiom" z3_true_axiom x continuation 1050 | thm_of_proofterm (state_proof, UNIT_RESOLUTION x) continuation = 1051 list_prems state_proof "unit_resolution" z3_unit_resolution x 1052 continuation [] 1053 | thm_of_proofterm ((state, proof), ID id) continuation = 1054 (case Redblackmap.peek (proof, id) of 1055 SOME (THEOREM thm) => 1056 continuation ((state, proof), thm) 1057 | SOME pt => 1058 thm_of_proofterm ((state, proof), pt) (continuation o 1059 (* update the proof, replacing the original proofterm with 1060 the theorem just derived *) 1061 (fn ((state, proof), thm) => 1062 ( 1063 if !Library.trace > 2 then 1064 Feedback.HOL_MESG 1065 ("HolSmtLib: updating proof at ID " ^ Int.toString id) 1066 else (); 1067 ((state, Redblackmap.insert (proof, id, THEOREM thm)), thm) 1068 ))) 1069 | NONE => 1070 raise ERR "thm_of_proofterm" 1071 ("proof has no proofterm for ID " ^ Int.toString id)) 1072 | thm_of_proofterm (state_proof, THEOREM thm) continuation = 1073 continuation (state_proof, thm) 1074 1075in 1076 1077 (* returns a theorem that concludes ``F``, with its hypotheses (a 1078 subset of) those asserted in the proof *) 1079 fun check_proof proof : Thm.thm = 1080 let 1081 val _ = if !Library.trace > 1 then 1082 Feedback.HOL_MESG "HolSmtLib: checking Z3 proof" 1083 else () 1084 1085 (* initial state *) 1086 val state = { 1087 asserted_hyps = Term.empty_tmset, 1088 thm_cache = Net.empty 1089 } 1090 1091 (* ID 0 denotes the proof's root node *) 1092 val ((state, _), thm) = thm_of_proofterm ((state, proof), ID 0) Lib.I 1093 1094 val _ = Thm.concl thm = boolSyntax.F orelse 1095 raise ERR "check_proof" "final conclusion is not 'F'" 1096 1097 (* check that the final theorem contains no hyps other than those 1098 that have been asserted *) 1099 val _ = profile "check_proof(hypcheck)" HOLset.isSubset (Thm.hypset thm, 1100 #asserted_hyps state) orelse 1101 raise ERR "check_proof" "final theorem contains additional hyp(s)" 1102 in 1103 thm 1104 end 1105 1106end (* local *) 1107 1108end 1109