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