1(* Title: HOL/Tools/SMT/z3_replay_methods.ML 2 Author: Sascha Boehme, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4 5Proof methods for replaying Z3 proofs. 6*) 7 8signature Z3_REPLAY_METHODS = 9sig 10 11 (*methods for Z3 proof rules*) 12 type z3_method = Proof.context -> thm list -> term -> thm 13 val true_axiom: z3_method 14 val mp: z3_method 15 val refl: z3_method 16 val symm: z3_method 17 val trans: z3_method 18 val cong: z3_method 19 val quant_intro: z3_method 20 val distrib: z3_method 21 val and_elim: z3_method 22 val not_or_elim: z3_method 23 val rewrite: z3_method 24 val rewrite_star: z3_method 25 val pull_quant: z3_method 26 val push_quant: z3_method 27 val elim_unused: z3_method 28 val dest_eq_res: z3_method 29 val quant_inst: z3_method 30 val lemma: z3_method 31 val unit_res: z3_method 32 val iff_true: z3_method 33 val iff_false: z3_method 34 val comm: z3_method 35 val def_axiom: z3_method 36 val apply_def: z3_method 37 val iff_oeq: z3_method 38 val nnf_pos: z3_method 39 val nnf_neg: z3_method 40 val mp_oeq: z3_method 41 val arith_th_lemma: z3_method 42 val th_lemma: string -> z3_method 43 val method_for: Z3_Proof.z3_rule -> z3_method 44end; 45 46structure Z3_Replay_Methods: Z3_REPLAY_METHODS = 47struct 48 49type z3_method = Proof.context -> thm list -> term -> thm 50 51 52(* utility functions *) 53 54fun replay_error ctxt msg rule thms t = 55 SMT_Replay_Methods.replay_error ctxt msg (Z3_Proof.string_of_rule rule) thms t 56 57fun replay_rule_error ctxt rule thms t = 58 SMT_Replay_Methods.replay_rule_error ctxt (Z3_Proof.string_of_rule rule) thms t 59 60fun trace_goal ctxt rule thms t = 61 SMT_Replay_Methods.trace_goal ctxt (Z3_Proof.string_of_rule rule) thms t 62 63fun as_prop (t as Const (\<^const_name>\<open>Trueprop\<close>, _) $ _) = t 64 | as_prop t = HOLogic.mk_Trueprop t 65 66fun dest_prop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t) = t 67 | dest_prop t = t 68 69fun dest_thm thm = dest_prop (Thm.concl_of thm) 70 71fun prop_tac ctxt prems = 72 Method.insert_tac ctxt prems 73 THEN' SUBGOAL (fn (prop, i) => 74 if Term.size_of_term prop > 100 then SAT.satx_tac ctxt i 75 else (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) i) 76 77fun quant_tac ctxt = Blast.blast_tac ctxt 78 79 80fun apply_rule ctxt t = 81 (case Z3_Replay_Rules.apply ctxt (SMT_Replay_Methods.certify_prop ctxt t) of 82 SOME thm => thm 83 | NONE => raise Fail "apply_rule") 84 85 86(*theory-lemma*) 87 88fun arith_th_lemma_tac ctxt prems = 89 Method.insert_tac ctxt prems 90 THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms z3div_def z3mod_def}) 91 THEN' Arith_Data.arith_tac ctxt 92 93fun arith_th_lemma ctxt thms t = 94 SMT_Replay_Methods.prove_abstract ctxt thms t arith_th_lemma_tac ( 95 fold_map (SMT_Replay_Methods.abstract_arith ctxt o dest_thm) thms ##>> 96 SMT_Replay_Methods.abstract_arith ctxt (dest_prop t)) 97 98val _ = Theory.setup (Context.theory_map ( 99 SMT_Replay_Methods.add_th_lemma_method ("arith", arith_th_lemma))) 100 101fun th_lemma name ctxt thms = 102 (case Symtab.lookup (SMT_Replay_Methods.get_th_lemma_method ctxt) name of 103 SOME method => method ctxt thms 104 | NONE => replay_error ctxt "Bad theory" (Z3_Proof.Th_Lemma name) thms) 105 106 107(* truth axiom *) 108 109fun true_axiom _ _ _ = @{thm TrueI} 110 111 112(* modus ponens *) 113 114fun mp _ [p, p_eq_q] _ = SMT_Replay_Methods.discharge 1 [p_eq_q, p] iffD1 115 | mp ctxt thms t = replay_rule_error ctxt Z3_Proof.Modus_Ponens thms t 116 117val mp_oeq = mp 118 119 120(* reflexivity *) 121 122fun refl ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm refl} 123 124 125(* symmetry *) 126 127fun symm _ [thm] _ = thm RS @{thm sym} 128 | symm ctxt thms t = replay_rule_error ctxt Z3_Proof.Reflexivity thms t 129 130 131(* transitivity *) 132 133fun trans _ [thm1, thm2] _ = thm1 RSN (1, thm2 RSN (2, @{thm trans})) 134 | trans ctxt thms t = replay_rule_error ctxt Z3_Proof.Transitivity thms t 135 136 137(* congruence *) 138 139fun cong ctxt thms = SMT_Replay_Methods.try_provers ctxt 140 (Z3_Proof.string_of_rule Z3_Proof.Monotonicity) [ 141 ("basic", SMT_Replay_Methods.cong_basic ctxt thms), 142 ("full", SMT_Replay_Methods.cong_full ctxt thms)] thms 143 144 145(* quantifier introduction *) 146 147val quant_intro_rules = @{lemma 148 "(\<And>x. P x = Q x) ==> (\<forall>x. P x) = (\<forall>x. Q x)" 149 "(\<And>x. P x = Q x) ==> (\<exists>x. P x) = (\<exists>x. Q x)" 150 "(!!x. (\<not> P x) = Q x) \<Longrightarrow> (\<not>(\<exists>x. P x)) = (\<forall>x. Q x)" 151 "(\<And>x. (\<not> P x) = Q x) ==> (\<not>(\<forall>x. P x)) = (\<exists>x. Q x)" 152 by fast+} 153 154fun quant_intro ctxt [thm] t = 155 SMT_Replay_Methods.prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac ctxt (thm :: quant_intro_rules)))) 156 | quant_intro ctxt thms t = replay_rule_error ctxt Z3_Proof.Quant_Intro thms t 157 158 159(* distributivity of conjunctions and disjunctions *) 160 161(* TODO: there are no tests with this proof rule *) 162fun distrib ctxt _ t = 163 SMT_Replay_Methods.prove_abstract' ctxt t prop_tac 164 (SMT_Replay_Methods.abstract_prop (dest_prop t)) 165 166 167(* elimination of conjunctions *) 168 169fun and_elim ctxt [thm] t = 170 SMT_Replay_Methods.prove_abstract ctxt [thm] t prop_tac ( 171 SMT_Replay_Methods.abstract_lit (dest_prop t) ##>> 172 SMT_Replay_Methods.abstract_conj (dest_thm thm) #>> 173 apfst single o swap) 174 | and_elim ctxt thms t = replay_rule_error ctxt Z3_Proof.And_Elim thms t 175 176 177(* elimination of negated disjunctions *) 178 179fun not_or_elim ctxt [thm] t = 180 SMT_Replay_Methods.prove_abstract ctxt [thm] t prop_tac ( 181 SMT_Replay_Methods.abstract_lit (dest_prop t) ##>> 182 SMT_Replay_Methods.abstract_not SMT_Replay_Methods.abstract_disj (dest_thm thm) #>> 183 apfst single o swap) 184 | not_or_elim ctxt thms t = 185 replay_rule_error ctxt Z3_Proof.Not_Or_Elim thms t 186 187 188(* rewriting *) 189 190local 191 192fun dest_all (Const (\<^const_name>\<open>HOL.All\<close>, _) $ Abs (_, T, t)) nctxt = 193 let 194 val (n, nctxt') = Name.variant "" nctxt 195 val f = Free (n, T) 196 val t' = Term.subst_bound (f, t) 197 in dest_all t' nctxt' |>> cons f end 198 | dest_all t _ = ([], t) 199 200fun dest_alls t = 201 let 202 val nctxt = Name.make_context (Term.add_free_names t []) 203 val (lhs, rhs) = HOLogic.dest_eq (dest_prop t) 204 val (ls, lhs') = dest_all lhs nctxt 205 val (rs, rhs') = dest_all rhs nctxt 206 in 207 if eq_list (op aconv) (ls, rs) then SOME (ls, (HOLogic.mk_eq (lhs', rhs'))) 208 else NONE 209 end 210 211fun forall_intr ctxt t thm = 212 let val ct = Thm.cterm_of ctxt t 213 in Thm.forall_intr ct thm COMP_INCR @{thm iff_allI} end 214 215in 216 217fun focus_eq f ctxt t = 218 (case dest_alls t of 219 NONE => f ctxt t 220 | SOME (vs, t') => fold (forall_intr ctxt) vs (f ctxt t')) 221 222end 223 224fun abstract_eq f (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) = 225 f t1 ##>> f t2 #>> HOLogic.mk_eq 226 | abstract_eq _ t = SMT_Replay_Methods.abstract_term t 227 228fun prove_prop_rewrite ctxt t = 229 SMT_Replay_Methods.prove_abstract' ctxt t prop_tac ( 230 abstract_eq SMT_Replay_Methods.abstract_prop (dest_prop t)) 231 232fun arith_rewrite_tac ctxt _ = 233 let val backup_tac = Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt in 234 (TRY o Simplifier.simp_tac ctxt) THEN_ALL_NEW backup_tac 235 ORELSE' backup_tac 236 end 237 238fun prove_arith_rewrite ctxt t = 239 SMT_Replay_Methods.prove_abstract' ctxt t arith_rewrite_tac ( 240 abstract_eq (SMT_Replay_Methods.abstract_arith ctxt) (dest_prop t)) 241 242val lift_ite_thm = @{thm HOL.if_distrib} RS @{thm eq_reflection} 243 244fun ternary_conv cv = Conv.combination_conv (Conv.binop_conv cv) cv 245 246fun if_context_conv ctxt ct = 247 (case Thm.term_of ct of 248 Const (\<^const_name>\<open>HOL.If\<close>, _) $ _ $ _ $ _ => 249 ternary_conv (if_context_conv ctxt) 250 | _ $ (Const (\<^const_name>\<open>HOL.If\<close>, _) $ _ $ _ $ _) => 251 Conv.rewr_conv lift_ite_thm then_conv ternary_conv (if_context_conv ctxt) 252 | _ => Conv.sub_conv (Conv.top_sweep_conv if_context_conv) ctxt) ct 253 254fun lift_ite_rewrite ctxt t = 255 SMT_Replay_Methods.prove ctxt t (fn ctxt => 256 CONVERSION (HOLogic.Trueprop_conv (Conv.binop_conv (if_context_conv ctxt))) 257 THEN' resolve_tac ctxt @{thms refl}) 258 259fun prove_conj_disj_perm ctxt t = SMT_Replay_Methods.prove ctxt t Conj_Disj_Perm.conj_disj_perm_tac 260 261fun rewrite ctxt _ = SMT_Replay_Methods.try_provers ctxt 262 (Z3_Proof.string_of_rule Z3_Proof.Rewrite) [ 263 ("rules", apply_rule ctxt), 264 ("conj_disj_perm", prove_conj_disj_perm ctxt), 265 ("prop_rewrite", prove_prop_rewrite ctxt), 266 ("arith_rewrite", focus_eq prove_arith_rewrite ctxt), 267 ("if_rewrite", lift_ite_rewrite ctxt)] [] 268 269fun rewrite_star ctxt = rewrite ctxt 270 271 272(* pulling quantifiers *) 273 274fun pull_quant ctxt _ t = SMT_Replay_Methods.prove ctxt t quant_tac 275 276 277(* pushing quantifiers *) 278 279fun push_quant _ _ _ = raise Fail "unsupported" (* FIXME *) 280 281 282(* elimination of unused bound variables *) 283 284val elim_all = @{lemma "P = Q \<Longrightarrow> (\<forall>x. P) = Q" by fast} 285val elim_ex = @{lemma "P = Q \<Longrightarrow> (\<exists>x. P) = Q" by fast} 286 287fun elim_unused_tac ctxt i st = ( 288 match_tac ctxt [@{thm refl}] 289 ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt) 290 ORELSE' ( 291 match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}] 292 THEN' elim_unused_tac ctxt)) i st 293 294fun elim_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t elim_unused_tac 295 296 297(* destructive equality resolution *) 298 299fun dest_eq_res _ _ _ = raise Fail "dest_eq_res" (* FIXME *) 300 301 302(* quantifier instantiation *) 303 304val quant_inst_rule = @{lemma "\<not>P x \<or> Q ==> \<not>(\<forall>x. P x) \<or> Q" by fast} 305 306fun quant_inst ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 307 REPEAT_ALL_NEW (resolve_tac ctxt [quant_inst_rule]) 308 THEN' resolve_tac ctxt @{thms excluded_middle}) 309 310 311(* propositional lemma *) 312 313exception LEMMA of unit 314 315val intro_hyp_rule1 = @{lemma "(\<not>P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q" by fast} 316val intro_hyp_rule2 = @{lemma "(P \<Longrightarrow> Q) \<Longrightarrow> \<not>P \<or> Q" by fast} 317 318fun norm_lemma thm = 319 (thm COMP_INCR intro_hyp_rule1) 320 handle THM _ => thm COMP_INCR intro_hyp_rule2 321 322fun negated_prop (\<^const>\<open>HOL.Not\<close> $ t) = HOLogic.mk_Trueprop t 323 | negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t) 324 325fun intro_hyps tab (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) cx = 326 lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx 327 | intro_hyps tab t cx = 328 lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx 329 330and lookup_intro_hyps tab t f (cx as (thm, terms)) = 331 (case Termtab.lookup tab (negated_prop t) of 332 NONE => f cx 333 | SOME hyp => (norm_lemma (Thm.implies_intr hyp thm), t :: terms)) 334 335fun lemma ctxt (thms as [thm]) t = 336 (let 337 val tab = Termtab.make (map (`Thm.term_of) (Thm.chyps_of thm)) 338 val (thm', terms) = intro_hyps tab (dest_prop t) (thm, []) 339 in 340 SMT_Replay_Methods.prove_abstract ctxt [thm'] t prop_tac ( 341 fold (snd oo SMT_Replay_Methods.abstract_lit) terms #> 342 SMT_Replay_Methods.abstract_disj (dest_thm thm') #>> single ##>> 343 SMT_Replay_Methods.abstract_disj (dest_prop t)) 344 end 345 handle LEMMA () => replay_error ctxt "Bad proof state" Z3_Proof.Lemma thms t) 346 | lemma ctxt thms t = replay_rule_error ctxt Z3_Proof.Lemma thms t 347 348 349(* unit resolution *) 350 351fun unit_res ctxt thms t = 352 SMT_Replay_Methods.prove_abstract ctxt thms t prop_tac ( 353 fold_map (SMT_Replay_Methods.abstract_unit o dest_thm) thms ##>> 354 SMT_Replay_Methods.abstract_unit (dest_prop t) #>> 355 (fn (prems, concl) => (prems, concl))) 356 357 358(* iff-true *) 359 360val iff_true_rule = @{lemma "P ==> P = True" by fast} 361 362fun iff_true _ [thm] _ = thm RS iff_true_rule 363 | iff_true ctxt thms t = replay_rule_error ctxt Z3_Proof.Iff_True thms t 364 365 366(* iff-false *) 367 368val iff_false_rule = @{lemma "\<not>P \<Longrightarrow> P = False" by fast} 369 370fun iff_false _ [thm] _ = thm RS iff_false_rule 371 | iff_false ctxt thms t = replay_rule_error ctxt Z3_Proof.Iff_False thms t 372 373 374(* commutativity *) 375 376fun comm ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm eq_commute} 377 378 379(* definitional axioms *) 380 381fun def_axiom_disj ctxt t = 382 (case dest_prop t of 383 \<^const>\<open>HOL.disj\<close> $ u1 $ u2 => 384 SMT_Replay_Methods.prove_abstract' ctxt t prop_tac ( 385 SMT_Replay_Methods.abstract_prop u2 ##>> SMT_Replay_Methods.abstract_prop u1 #>> 386 HOLogic.mk_disj o swap) 387 | u => SMT_Replay_Methods.prove_abstract' ctxt t prop_tac (SMT_Replay_Methods.abstract_prop u)) 388 389fun def_axiom ctxt _ = SMT_Replay_Methods.try_provers ctxt 390 (Z3_Proof.string_of_rule Z3_Proof.Def_Axiom) [ 391 ("rules", apply_rule ctxt), 392 ("disj", def_axiom_disj ctxt)] [] 393 394 395(* application of definitions *) 396 397fun apply_def _ [thm] _ = thm (* TODO: cover also the missing cases *) 398 | apply_def ctxt thms t = replay_rule_error ctxt Z3_Proof.Apply_Def thms t 399 400 401(* iff-oeq *) 402 403fun iff_oeq _ _ _ = raise Fail "iff_oeq" (* FIXME *) 404 405 406(* negation normal form *) 407 408fun nnf_prop ctxt thms t = 409 SMT_Replay_Methods.prove_abstract ctxt thms t prop_tac ( 410 fold_map (SMT_Replay_Methods.abstract_prop o dest_thm) thms ##>> 411 SMT_Replay_Methods.abstract_prop (dest_prop t)) 412 413fun nnf ctxt rule thms = SMT_Replay_Methods.try_provers ctxt (Z3_Proof.string_of_rule rule) [ 414 ("prop", nnf_prop ctxt thms), 415 ("quant", quant_intro ctxt [hd thms])] thms 416 417fun nnf_pos ctxt = nnf ctxt Z3_Proof.Nnf_Pos 418fun nnf_neg ctxt = nnf ctxt Z3_Proof.Nnf_Neg 419 420 421(* mapping of rules to methods *) 422 423fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule 424fun assumed rule ctxt = replay_error ctxt "Assumed" rule 425 426fun choose Z3_Proof.True_Axiom = true_axiom 427 | choose (r as Z3_Proof.Asserted) = assumed r 428 | choose (r as Z3_Proof.Goal) = assumed r 429 | choose Z3_Proof.Modus_Ponens = mp 430 | choose Z3_Proof.Reflexivity = refl 431 | choose Z3_Proof.Symmetry = symm 432 | choose Z3_Proof.Transitivity = trans 433 | choose (r as Z3_Proof.Transitivity_Star) = unsupported r 434 | choose Z3_Proof.Monotonicity = cong 435 | choose Z3_Proof.Quant_Intro = quant_intro 436 | choose Z3_Proof.Distributivity = distrib 437 | choose Z3_Proof.And_Elim = and_elim 438 | choose Z3_Proof.Not_Or_Elim = not_or_elim 439 | choose Z3_Proof.Rewrite = rewrite 440 | choose Z3_Proof.Rewrite_Star = rewrite_star 441 | choose Z3_Proof.Pull_Quant = pull_quant 442 | choose (r as Z3_Proof.Pull_Quant_Star) = unsupported r 443 | choose Z3_Proof.Push_Quant = push_quant 444 | choose Z3_Proof.Elim_Unused_Vars = elim_unused 445 | choose Z3_Proof.Dest_Eq_Res = dest_eq_res 446 | choose Z3_Proof.Quant_Inst = quant_inst 447 | choose (r as Z3_Proof.Hypothesis) = assumed r 448 | choose Z3_Proof.Lemma = lemma 449 | choose Z3_Proof.Unit_Resolution = unit_res 450 | choose Z3_Proof.Iff_True = iff_true 451 | choose Z3_Proof.Iff_False = iff_false 452 | choose Z3_Proof.Commutativity = comm 453 | choose Z3_Proof.Def_Axiom = def_axiom 454 | choose (r as Z3_Proof.Intro_Def) = assumed r 455 | choose Z3_Proof.Apply_Def = apply_def 456 | choose Z3_Proof.Iff_Oeq = iff_oeq 457 | choose Z3_Proof.Nnf_Pos = nnf_pos 458 | choose Z3_Proof.Nnf_Neg = nnf_neg 459 | choose (r as Z3_Proof.Nnf_Star) = unsupported r 460 | choose (r as Z3_Proof.Cnf_Star) = unsupported r 461 | choose (r as Z3_Proof.Skolemize) = assumed r 462 | choose Z3_Proof.Modus_Ponens_Oeq = mp_oeq 463 | choose (Z3_Proof.Th_Lemma name) = th_lemma name 464 465fun with_tracing rule method ctxt thms t = 466 let val _ = trace_goal ctxt rule thms t 467 in method ctxt thms t end 468 469fun method_for rule = with_tracing rule (choose rule) 470 471end; 472