1(* Title: HOL/Tools/SMT/verit_replay_methods.ML 2 Author: Mathias Fleury, MPII 3 4Proof methods for replaying veriT proofs. 5*) 6 7signature VERIT_REPLAY_METHODS = 8sig 9 10 val is_skolemisation: string -> bool 11 val is_skolemisation_step: VeriT_Proof.veriT_replay_node -> bool 12 13 (* methods for veriT proof rules *) 14 val method_for: string -> Proof.context -> thm list -> term list -> term -> 15 thm 16 17 val veriT_step_requires_subproof_assms : string -> bool 18 val eq_congruent_pred: Proof.context -> 'a -> term -> thm 19end; 20 21 22structure Verit_Replay_Methods: VERIT_REPLAY_METHODS = 23struct 24 25(*Some general comments on the proof format: 26 1. Double negations are not always removed. This means for example that the equivalence rules 27 cannot assume that the double negations have already been removed. Therefore, we match the 28 term, instantiate the theorem, then use simp (to remove double negations), and finally use 29 assumption. 30 2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule 31 is doing much more that is supposed to do. Moreover types can make trivial goals (for the 32 boolean structure) impossible to prove. 33 3. Duplicate literals are sometimes removed, mostly by the SAT solver. We currently do not care 34 about it, since in all cases we have met, a rule like tmp_AC_simp is called to do the 35 simplification. 36 37 Rules unsupported on purpose: 38 * Distinct_Elim, XOR, let (we don't need them). 39 * tmp_skolemize (because it is not clear if veriT still generates using it). 40*) 41 42datatype verit_rule = 43 False | True | 44 45 (* input: a repeated (normalized) assumption of assumption of in a subproof *) 46 Normalized_Input | Local_Input | 47 (* Subproof: *) 48 Subproof | 49 (* Conjunction: *) 50 And | Not_And | And_Pos | And_Neg | 51 (* Disjunction"" *) 52 Or | Or_Pos | Not_Or | Or_Neg | 53 (* Disjunction: *) 54 Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 | 55 (* Equivalence: *) 56 Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 | 57 (* If-then-else: *) 58 ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 | 59 (* Equality: *) 60 Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans | Refl | Cong | 61 (* Arithmetics: *) 62 LA_Disequality | LA_Generic | LA_Tautology | LIA_Generic | LA_Totality | LA_RW_Eq | 63 NLA_Generic | 64 (* Quantifiers: *) 65 Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Qnt_Simplify | Bind | Skolem_Forall | Skolem_Ex | 66 (* Resolution: *) 67 Theory_Resolution | Resolution | 68 (* Various transformation: *) 69 Connective_Equiv | 70 (* Temporary rules, that the veriT developpers want to remove: *) 71 Tmp_AC_Simp | 72 Tmp_Bfun_Elim | 73 (* Unsupported rule *) 74 Unsupported 75 76val is_skolemisation = member (op =) ["sko_forall", "sko_ex"] 77fun is_skolemisation_step (VeriT_Proof.VeriT_Replay_Node {id, ...}) = is_skolemisation id 78 79fun verit_rule_of "bind" = Bind 80 | verit_rule_of "cong" = Cong 81 | verit_rule_of "refl" = Refl 82 | verit_rule_of "equiv1" = Equiv1 83 | verit_rule_of "equiv2" = Equiv2 84 | verit_rule_of "equiv_pos1" = Equiv_pos1 85 | verit_rule_of "equiv_pos2" = Equiv_pos2 86 | verit_rule_of "equiv_neg1" = Equiv_neg1 87 | verit_rule_of "equiv_neg2" = Equiv_neg2 88 | verit_rule_of "sko_forall" = Skolem_Forall 89 | verit_rule_of "sko_ex" = Skolem_Ex 90 | verit_rule_of "eq_reflexive" = Eq_Reflexive 91 | verit_rule_of "th_resolution" = Theory_Resolution 92 | verit_rule_of "forall_inst" = Forall_Inst 93 | verit_rule_of "implies_pos" = Implies_Pos 94 | verit_rule_of "or" = Or 95 | verit_rule_of "not_or" = Not_Or 96 | verit_rule_of "resolution" = Resolution 97 | verit_rule_of "eq_congruent" = Eq_Congruent 98 | verit_rule_of "connective_equiv" = Connective_Equiv 99 | verit_rule_of "trans" = Trans 100 | verit_rule_of "false" = False 101 | verit_rule_of "tmp_AC_simp" = Tmp_AC_Simp 102 | verit_rule_of "and" = And 103 | verit_rule_of "not_and" = Not_And 104 | verit_rule_of "and_pos" = And_Pos 105 | verit_rule_of "and_neg" = And_Neg 106 | verit_rule_of "or_pos" = Or_Pos 107 | verit_rule_of "or_neg" = Or_Neg 108 | verit_rule_of "not_equiv1" = Not_Equiv1 109 | verit_rule_of "not_equiv2" = Not_Equiv2 110 | verit_rule_of "not_implies1" = Not_Implies1 111 | verit_rule_of "not_implies2" = Not_Implies2 112 | verit_rule_of "implies_neg1" = Implies_Neg1 113 | verit_rule_of "implies_neg2" = Implies_Neg2 114 | verit_rule_of "implies" = Implies 115 | verit_rule_of "tmp_bfun_elim" = Tmp_Bfun_Elim 116 | verit_rule_of "ite1" = ITE1 117 | verit_rule_of "ite2" = ITE2 118 | verit_rule_of "not_ite1" = Not_ITE1 119 | verit_rule_of "not_ite2" = Not_ITE2 120 | verit_rule_of "ite_pos1" = ITE_Pos1 121 | verit_rule_of "ite_pos2" = ITE_Pos2 122 | verit_rule_of "ite_neg1" = ITE_Neg1 123 | verit_rule_of "ite_neg2" = ITE_Neg2 124 | verit_rule_of "ite_intro" = ITE_Intro 125 | verit_rule_of "la_disequality" = LA_Disequality 126 | verit_rule_of "lia_generic" = LIA_Generic 127 | verit_rule_of "la_generic" = LA_Generic 128 | verit_rule_of "la_tautology" = LA_Tautology 129 | verit_rule_of "la_totality" = LA_Totality 130 | verit_rule_of "la_rw_eq"= LA_RW_Eq 131 | verit_rule_of "nla_generic"= NLA_Generic 132 | verit_rule_of "eq_transitive" = Eq_Transitive 133 | verit_rule_of "qnt_rm_unused" = Qnt_Rm_Unused 134 | verit_rule_of "qnt_simplify" = Qnt_Simplify 135 | verit_rule_of "qnt_join" = Qnt_Join 136 | verit_rule_of "eq_congruent_pred" = Eq_Congruent_Pred 137 | verit_rule_of "subproof" = Subproof 138 | verit_rule_of r = 139 if r = VeriT_Proof.veriT_normalized_input_rule then Normalized_Input 140 else if r = VeriT_Proof.veriT_local_input_rule then Local_Input 141 else Unsupported 142 143fun string_of_verit_rule Bind = "Bind" 144 | string_of_verit_rule Cong = "Cong" 145 | string_of_verit_rule Refl = "Refl" 146 | string_of_verit_rule Equiv1 = "Equiv1" 147 | string_of_verit_rule Equiv2 = "Equiv2" 148 | string_of_verit_rule Equiv_pos1 = "Equiv_pos1" 149 | string_of_verit_rule Equiv_pos2 = "Equiv_pos2" 150 | string_of_verit_rule Equiv_neg1 = "Equiv_neg1" 151 | string_of_verit_rule Equiv_neg2 = "Equiv_neg2" 152 | string_of_verit_rule Skolem_Forall = "Skolem_Forall" 153 | string_of_verit_rule Skolem_Ex = "Skolem_Ex" 154 | string_of_verit_rule Eq_Reflexive = "Eq_Reflexive" 155 | string_of_verit_rule Theory_Resolution = "Theory_Resolution" 156 | string_of_verit_rule Forall_Inst = "forall_inst" 157 | string_of_verit_rule Or = "Or" 158 | string_of_verit_rule Not_Or = "Not_Or" 159 | string_of_verit_rule Resolution = "Resolution" 160 | string_of_verit_rule Eq_Congruent = "eq_congruent" 161 | string_of_verit_rule Connective_Equiv = "connective_equiv" 162 | string_of_verit_rule Trans = "trans" 163 | string_of_verit_rule False = "false" 164 | string_of_verit_rule And = "and" 165 | string_of_verit_rule And_Pos = "and_pos" 166 | string_of_verit_rule Not_And = "not_and" 167 | string_of_verit_rule And_Neg = "and_neg" 168 | string_of_verit_rule Or_Pos = "or_pos" 169 | string_of_verit_rule Or_Neg = "or_neg" 170 | string_of_verit_rule Tmp_AC_Simp = "tmp_AC_simp" 171 | string_of_verit_rule Not_Equiv1 = "not_equiv1" 172 | string_of_verit_rule Not_Equiv2 = "not_equiv2" 173 | string_of_verit_rule Not_Implies1 = "not_implies1" 174 | string_of_verit_rule Not_Implies2 = "not_implies2" 175 | string_of_verit_rule Implies_Neg1 = "implies_neg1" 176 | string_of_verit_rule Implies_Neg2 = "implies_neg2" 177 | string_of_verit_rule Implies = "implies" 178 | string_of_verit_rule Tmp_Bfun_Elim = "tmp_bfun_elim" 179 | string_of_verit_rule ITE1 = "ite1" 180 | string_of_verit_rule ITE2 = "ite2" 181 | string_of_verit_rule Not_ITE1 = "not_ite1" 182 | string_of_verit_rule Not_ITE2 = "not_ite2" 183 | string_of_verit_rule ITE_Pos1 = "ite_pos1" 184 | string_of_verit_rule ITE_Pos2 = "ite_pos2" 185 | string_of_verit_rule ITE_Neg1 = "ite_neg1" 186 | string_of_verit_rule ITE_Neg2 = "ite_neg2" 187 | string_of_verit_rule ITE_Intro = "ite_intro" 188 | string_of_verit_rule LA_Disequality = "la_disequality" 189 | string_of_verit_rule LA_Generic = "la_generic" 190 | string_of_verit_rule LIA_Generic = "lia_generic" 191 | string_of_verit_rule LA_Tautology = "la_tautology" 192 | string_of_verit_rule LA_RW_Eq = "la_rw_eq" 193 | string_of_verit_rule LA_Totality = "LA_Totality" 194 | string_of_verit_rule NLA_Generic = "nla_generic" 195 | string_of_verit_rule Eq_Transitive = "eq_transitive" 196 | string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused" 197 | string_of_verit_rule Qnt_Simplify = "qnt_simplify" 198 | string_of_verit_rule Qnt_Join = "qnt_join" 199 | string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred" 200 | string_of_verit_rule Normalized_Input = VeriT_Proof.veriT_normalized_input_rule 201 | string_of_verit_rule Local_Input = VeriT_Proof.veriT_normalized_input_rule 202 | string_of_verit_rule Subproof = "subproof" 203 | string_of_verit_rule r = "Unsupported rule: " ^ \<^make_string> r 204 205(*** Methods to Replay Normal steps ***) 206(* sko_forall requires the assumptions to be able to SMT_Replay_Methods.prove the equivalence in case of double 207skolemization. See comment below. *) 208fun veriT_step_requires_subproof_assms t = 209 member (op =) ["refl", "cong", VeriT_Proof.veriT_local_input_rule, "sko_forall", 210 "sko_ex"] t 211 212fun simplify_tac ctxt thms = 213 ctxt 214 |> empty_simpset 215 |> put_simpset HOL_basic_ss 216 |> (fn ctxt => ctxt addsimps @{thms not_not eq_commute} addsimps thms) 217 |> Simplifier.full_simp_tac 218 219val bind_thms = 220 [@{lemma "(\<And>x x'. P x = Q x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)" 221 by blast}, 222 @{lemma "(\<And>x x'. P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)" 223 by blast}, 224 @{lemma "(\<And>x x'. P x = Q x) \<Longrightarrow> (\<exists>x. P x = Q x)" 225 by blast}, 226 @{lemma "(\<And>x x'. P x = Q x) \<Longrightarrow> (\<forall>x. P x = Q x)" 227 by blast}] 228 229fun TRY' tac = fn i => TRY (tac i) 230fun REPEAT' tac = fn i => REPEAT (tac i) 231fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i)) 232 233fun bind ctxt [prems] t = SMT_Replay_Methods.prove ctxt t (fn _ => 234 REPEAT' (resolve_tac ctxt bind_thms) 235 THEN' match_tac ctxt [prems] 236 THEN' simplify_tac ctxt [] 237 THEN' REPEAT' (match_tac ctxt [@{thm refl}])) 238 239 240fun refl ctxt thm t = 241 (case find_first (fn thm => t = Thm.full_prop_of thm) thm of 242 SOME thm => thm 243 | NONE => 244 (case try (Z3_Replay_Methods.refl ctxt thm) t of 245 NONE => 246 ( Z3_Replay_Methods.cong ctxt thm t) 247 | SOME thm => thm)) 248 249local 250 fun equiv_pos_neg_term ctxt thm (\<^term>\<open>Trueprop\<close> $ 251 (\<^term>\<open>HOL.disj\<close> $ (_) $ 252 ((\<^term>\<open>HOL.disj\<close> $ a $ b)))) = 253 Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm 254 255 fun prove_equiv_pos_neg thm ctxt _ t = 256 let val thm = equiv_pos_neg_term ctxt thm t 257 in 258 SMT_Replay_Methods.prove ctxt t (fn _ => 259 Method.insert_tac ctxt [thm] 260 THEN' simplify_tac ctxt []) 261 end 262in 263 264val equiv_pos1_thm = 265 @{lemma "\<not>(a \<longleftrightarrow> ~b) \<or> a \<or> b" 266 by blast+} 267 268val equiv_pos1 = prove_equiv_pos_neg equiv_pos1_thm 269 270val equiv_pos2_thm = 271 @{lemma "\<And>a b. ((\<not>a) \<noteq> b) \<or> a \<or> b" 272 by blast+} 273 274val equiv_pos2 = prove_equiv_pos_neg equiv_pos2_thm 275 276val equiv_neg1_thm = 277 @{lemma "(~a \<longleftrightarrow> ~b) \<or> a \<or> b" 278 by blast} 279 280val equiv_neg1 = prove_equiv_pos_neg equiv_neg1_thm 281 282val equiv_neg2_thm = 283 @{lemma "(a \<longleftrightarrow> b) \<or> a \<or> b" 284 by blast} 285 286val equiv_neg2 = prove_equiv_pos_neg equiv_neg2_thm 287 288end 289 290(* Most of the code below is due to the proof output of veriT: The description of the rule is wrong 291(and according to Pascal Fontaine, it is a bug). Anyway, currently, forall_inst does: 292 1. swapping out the forall quantifiers 293 2. instantiation 294 3. boolean. 295 296However, types can mess-up things: 297 lemma \<open>(0 < degree a) = (0 \<noteq> degree a) \<Longrightarrow> 0 = degree a \<or> 0 < degree a\<close> 298 by fast 299works unlike 300 lemma \<open>((0::nat) < degree a) = (0 \<noteq> degree a) \<Longrightarrow> 0 = degree a \<or> 0 < degree a\<close> 301 by fast. 302Therefore, we use fast and auto as fall-back. 303*) 304fun forall_inst ctxt _ args t = 305 let 306 val instantiate = 307 fold (fn inst => fn tac => 308 let val thm = Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt inst)] @{thm spec} 309 in tac THEN' dmatch_tac ctxt [thm]end) 310 args 311 (K all_tac) 312 in 313 SMT_Replay_Methods.prove ctxt t (fn _ => 314 resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]] 315 THEN' TRY' (Raw_Simplifier.rewrite_goal_tac ctxt @{thms all_simps[symmetric] not_all}) 316 THEN' TRY' instantiate 317 THEN' TRY' (simplify_tac ctxt []) 318 THEN' TRY' (SOLVED' (fn _ => HEADGOAL ( (assume_tac ctxt) 319 ORELSE' 320 TRY' (dresolve_tac ctxt @{thms conjE} 321 THEN_ALL_NEW assume_tac ctxt) 322 ORELSE' 323 TRY' (dresolve_tac ctxt @{thms verit_forall_inst} 324 THEN_ALL_NEW assume_tac ctxt)))) 325 THEN' (TRY' (Classical.fast_tac ctxt)) 326 THEN' (TRY' (K (Clasimp.auto_tac ctxt)))) 327 end 328 329fun or _ [thm] _ = thm 330 331val implies_pos_thm = 332 [@{lemma "\<not>(A \<longrightarrow> B) \<or> \<not>A \<or> B" 333 by blast}, 334 @{lemma "\<not>(\<not>A \<longrightarrow> B) \<or> A \<or> B" 335 by blast}] 336 337fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 338 resolve_tac ctxt implies_pos_thm) 339 340fun extract_rewrite_rule_assumption thms = 341 let 342 fun is_rewrite_rule thm = 343 (case Thm.prop_of thm of 344 \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ Free(_, _) $ _) => true 345 | _ => false) 346 in 347 thms 348 |> filter is_rewrite_rule 349 |> map (fn thm => thm COMP @{thm eq_reflection}) 350 end 351 352(* We need to unfold the assumptions if we are in a subproof: For multiple skolemization, the context 353contains a mapping "verit_vrX \<leadsto> Eps f". The variable "verit_vrX" must be unfolded to "Eps f". 354Otherwise, the proof cannot be done. *) 355fun skolem_forall ctxt (thms) t = 356 let 357 val ts = extract_rewrite_rule_assumption thms 358 in 359 SMT_Replay_Methods.prove ctxt t (fn _ => 360 REPEAT_CHANGED (resolve_tac ctxt @{thms verit_sko_forall'}) 361 THEN' TRY' (simplify_tac ctxt ts) 362 THEN' TRY'(resolve_tac ctxt thms THEN_ALL_NEW resolve_tac ctxt @{thms refl}) 363 THEN' TRY' (resolve_tac ctxt @{thms refl})) 364 end 365 366fun skolem_ex ctxt (thms) t = 367 let 368 val ts = extract_rewrite_rule_assumption thms 369 in 370 SMT_Replay_Methods.prove ctxt t (fn _ => 371 Raw_Simplifier.rewrite_goal_tac ctxt ts 372 THEN' REPEAT_CHANGED (resolve_tac ctxt @{thms verit_sko_ex'}) 373 THEN' REPEAT_CHANGED (resolve_tac ctxt thms THEN_ALL_NEW resolve_tac ctxt @{thms refl}) 374 THEN' TRY' (resolve_tac ctxt @{thms refl})) 375 end 376 377fun eq_reflexive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 378 resolve_tac ctxt [@{thm refl}]) 379 380fun connective_equiv ctxt thms t = SMT_Replay_Methods.prove ctxt t (fn _ => 381 Method.insert_tac ctxt thms 382 THEN' K (Clasimp.auto_tac ctxt)) 383 384 385fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => 386 Method.insert_tac ctxt prems 387 THEN' TRY' (simplify_tac ctxt []) 388 THEN' TRY' (K (Clasimp.auto_tac ctxt))) 389 390val false_rule_thm = @{lemma "\<not>False" by blast} 391 392fun false_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 393 resolve_tac ctxt [false_rule_thm]) 394 395 396(* transitivity *) 397 398val trans_bool_thm = 399 @{lemma "P = Q \<Longrightarrow> Q \<Longrightarrow> P" by blast} 400fun trans _ [thm1, thm2] _ = 401 (case (Thm.full_prop_of thm1, Thm.full_prop_of thm2) of 402 (\<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ t2), 403 \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ _)) => 404 if t2 = t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans})) 405 else thm1 RSN (1, (thm2 RS sym) RSN (2, @{thm trans})) 406 | _ => trans_bool_thm OF [thm1, thm2]) 407 | trans ctxt (thm1 :: thm2 :: thms) t = 408 trans ctxt (trans ctxt [thm1, thm2] t :: thms) t 409 410fun tmp_AC_rule ctxt _ t = 411 let 412 val simplify = 413 ctxt 414 |> empty_simpset 415 |> put_simpset HOL_basic_ss 416 |> (fn ctxt => ctxt addsimps @{thms ac_simps conj_ac}) 417 |> Simplifier.full_simp_tac 418 in SMT_Replay_Methods.prove ctxt t (fn _ => 419 REPEAT_ALL_NEW (simplify_tac ctxt [] 420 THEN' TRY' simplify 421 THEN' TRY' (Classical.fast_tac ctxt))) end 422 423fun and_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => 424 Method.insert_tac ctxt prems 425 THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1))) 426 THEN' TRY' (assume_tac ctxt) 427 THEN' TRY' (simplify_tac ctxt [])) 428 429fun not_and_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => 430 Method.insert_tac ctxt prems THEN' 431 Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) 432 433fun not_or_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => 434 Method.insert_tac ctxt prems THEN' 435 Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) 436 437local 438 fun simplify_and_pos ctxt = 439 ctxt 440 |> empty_simpset 441 |> put_simpset HOL_basic_ss 442 |> (fn ctxt => ctxt addsimps @{thms eq_commute verit_ite_intro_simp if_cancel} 443 addsimps @{thms simp_thms de_Morgan_conj}) 444 |> Simplifier.full_simp_tac 445in 446 447fun and_pos ctxt _ t = 448 SMT_Replay_Methods.prove ctxt t (fn _ => 449 REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos}) 450 THEN' TRY' (simplify_and_pos ctxt) 451 THEN' TRY' (assume_tac ctxt) 452 THEN' TRY' (Classical.fast_tac ctxt)) 453 454end 455 456fun and_neg_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 457 REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_neg}) 458 THEN' simplify_tac ctxt @{thms de_Morgan_conj[symmetric] excluded_middle 459 excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]}) 460 461fun or_pos_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 462 simplify_tac ctxt @{thms simp_thms}) 463 464fun or_neg_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 465 resolve_tac ctxt @{thms verit_or_neg} 466 THEN' (fn i => dresolve_tac ctxt @{thms verit_subst_bool} i 467 THEN assume_tac ctxt (i+1)) 468 THEN' simplify_tac ctxt @{thms simp_thms}) 469 470val not_equiv1_thm = 471 @{lemma "\<not>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> B" 472 by blast} 473 474fun not_equiv1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => 475 Method.insert_tac ctxt [not_equiv1_thm OF [thm]] 476 THEN' simplify_tac ctxt []) 477 478val not_equiv2_thm = 479 @{lemma "\<not>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> \<not>B" 480 by blast} 481 482fun not_equiv2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => 483 Method.insert_tac ctxt [not_equiv2_thm OF [thm]] 484 THEN' simplify_tac ctxt []) 485 486val equiv1_thm = 487 @{lemma "(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> B" 488 by blast} 489 490fun equiv1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => 491 Method.insert_tac ctxt [equiv1_thm OF [thm]] 492 THEN' simplify_tac ctxt []) 493 494val equiv2_thm = 495 @{lemma "(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> \<not>B" 496 by blast} 497 498fun equiv2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => 499 Method.insert_tac ctxt [equiv2_thm OF [thm]] 500 THEN' simplify_tac ctxt []) 501 502 503val not_implies1_thm = 504 @{lemma "\<not>(A \<longrightarrow> B) \<Longrightarrow> A" 505 by blast} 506 507fun not_implies1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => 508 Method.insert_tac ctxt [not_implies1_thm OF [thm]] 509 THEN' simplify_tac ctxt []) 510 511val not_implies2_thm = 512 @{lemma "\<not>(A \<longrightarrow>B) \<Longrightarrow> \<not>B" 513 by blast} 514 515fun not_implies2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => 516 Method.insert_tac ctxt [not_implies2_thm OF [thm]] 517 THEN' simplify_tac ctxt []) 518 519 520local 521 fun implies_pos_neg_term ctxt thm (\<^term>\<open>Trueprop\<close> $ 522 (\<^term>\<open>HOL.disj\<close> $ (\<^term>\<open>HOL.implies\<close> $ a $ b) $ _)) = 523 Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm 524 525 fun prove_implies_pos_neg thm ctxt _ t = 526 let val thm = implies_pos_neg_term ctxt thm t 527 in 528 SMT_Replay_Methods.prove ctxt t (fn _ => 529 Method.insert_tac ctxt [thm] 530 THEN' simplify_tac ctxt []) 531 end 532in 533 534val implies_neg1_thm = 535 @{lemma "(a \<longrightarrow> b) \<or> a" 536 by blast} 537 538val implies_neg1 = prove_implies_pos_neg implies_neg1_thm 539 540val implies_neg2_thm = 541 @{lemma "(a \<longrightarrow> b) \<or> \<not>b" by blast} 542 543val implies_neg2 = prove_implies_pos_neg implies_neg2_thm 544 545end 546 547val implies_thm = 548 @{lemma "(~a \<longrightarrow> b) \<Longrightarrow> a \<or> b" 549 "(a \<longrightarrow> b) \<Longrightarrow> \<not>a \<or> b" 550 by blast+} 551 552fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => 553 Method.insert_tac ctxt prems 554 THEN' resolve_tac ctxt implies_thm 555 THEN' assume_tac ctxt) 556 557 558(* 559Here is a case where force_tac fails, but auto_tac succeeds: 560 Ex (P x) \<noteq> P x c \<Longrightarrow> 561 (\<exists>v0. if x then P True v0 else P False v0) \<noteq> (if x then P True c else P False c) 562 563(this was before we added the eqsubst_tac). Therefore, to be safe, we add the fast, auto, and force. 564*) 565fun tmp_bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => 566 Method.insert_tac ctxt prems 567 THEN' REPEAT_CHANGED (EqSubst.eqsubst_tac ctxt [0] @{thms verit_tmp_bfun_elim}) 568 THEN' TRY' (simplify_tac ctxt []) 569 THEN' (Classical.fast_tac ctxt 570 ORELSE' K (Clasimp.auto_tac ctxt) 571 ORELSE' Clasimp.force_tac ctxt)) 572 573val ite_pos1_thm = 574 @{lemma "\<not>(if x then P else Q) \<or> x \<or> Q" 575 by auto} 576 577fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 578 resolve_tac ctxt [ite_pos1_thm]) 579 580val ite_pos2_thms = 581 @{lemma "\<not>(if x then P else Q) \<or> \<not>x \<or> P" "\<not>(if \<not>x then P else Q) \<or> x \<or> P" 582 by auto} 583 584fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 585 resolve_tac ctxt ite_pos2_thms) 586 587val ite_neg1_thms = 588 @{lemma "(if x then P else Q) \<or> x \<or> \<not>Q" "(if x then P else \<not>Q) \<or> x \<or> Q" 589 by auto} 590 591fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 592 resolve_tac ctxt ite_neg1_thms) 593 594val ite_neg2_thms = 595 @{lemma "(if x then P else Q) \<or> \<not>x \<or> \<not>P" "(if \<not>x then P else Q) \<or> x \<or> \<not>P" 596 "(if x then \<not>P else Q) \<or> \<not>x \<or> P" "(if \<not>x then \<not>P else Q) \<or> x \<or> P" 597 by auto} 598 599fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 600 resolve_tac ctxt ite_neg2_thms) 601 602val ite1_thm = 603 @{lemma "(if x then P else Q) \<Longrightarrow> x \<or> Q" 604 by (auto split: if_splits) } 605 606fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => 607 resolve_tac ctxt [ite1_thm OF [thm]]) 608 609val ite2_thm = 610 @{lemma "(if x then P else Q) \<Longrightarrow> \<not>x \<or> P" 611 by (auto split: if_splits) } 612 613fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => 614 resolve_tac ctxt [ite2_thm OF [thm]]) 615 616 617val not_ite1_thm = 618 @{lemma "\<not>(if x then P else Q) \<Longrightarrow> x \<or> \<not>Q" 619 by (auto split: if_splits) } 620 621fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => 622 resolve_tac ctxt [not_ite1_thm OF [thm]]) 623 624val not_ite2_thm = 625 @{lemma "\<not>(if x then P else Q) \<Longrightarrow> \<not>x \<or> \<not>P" 626 by (auto split: if_splits) } 627 628fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => 629 resolve_tac ctxt [not_ite2_thm OF [thm]]) 630 631 632fun unit_res ctxt thms t = 633 let 634 val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms 635 val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t)) 636 val (_, t2) = Logic.dest_equals (Thm.prop_of t') 637 val thm = Z3_Replay_Methods.unit_res ctxt thms t2 638 in 639 @{thm verit_Pure_trans} OF [t', thm] 640 end 641 642fun ite_intro ctxt _ t = 643 let 644 fun simplify_ite ctxt = 645 ctxt 646 |> empty_simpset 647 |> put_simpset HOL_basic_ss 648 |> (fn ctxt => ctxt addsimps @{thms eq_commute verit_ite_intro_simp if_cancel} 649 addsimps @{thms simp_thms}) 650 |> Simplifier.full_simp_tac 651 in 652 SMT_Replay_Methods.prove ctxt t (fn _ => 653 (simplify_ite ctxt 654 THEN' TRY' (Blast.blast_tac ctxt 655 ORELSE' K (Clasimp.auto_tac ctxt) 656 ORELSE' Clasimp.force_tac ctxt))) 657 end 658 659 660(* Quantifiers *) 661 662fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 663 Classical.fast_tac ctxt) 664 665fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 666 Classical.fast_tac ctxt) 667 668fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 669 Classical.fast_tac ctxt) 670 671 672(* Equality *) 673 674fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 675 REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}]) 676 THEN' REPEAT' (resolve_tac ctxt @{thms impI}) 677 THEN' REPEAT' (eresolve_tac ctxt @{thms conjI}) 678 THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1)) 679 THEN' resolve_tac ctxt @{thms refl}) 680 681local 682 683 (* Rewrite might apply below choice. As we do not want to change them (it can break other 684 rewriting steps), we cannot use Term.lambda *) 685 fun abstract_over_no_choice (v, body) = 686 let 687 fun abs lev tm = 688 if v aconv tm then Bound lev 689 else 690 (case tm of 691 Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) 692 | t as (Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ _) => t 693 | t $ u => 694 (abs lev t $ (abs lev u handle Same.SAME => u) 695 handle Same.SAME => t $ abs lev u) 696 | _ => raise Same.SAME); 697 in abs 0 body handle Same.SAME => body end; 698 699 fun lambda_name (x, v) t = 700 Abs (if x = "" then Term.term_name v else x, fastype_of v, abstract_over_no_choice (v, t)); 701 702 fun lambda v t = lambda_name ("", v) t; 703 704 fun extract_equal_terms (Const(\<^const_name>\<open>Trueprop\<close>, _) $ t) = 705 let fun ext (Const(\<^const_name>\<open>HOL.disj\<close>, _) $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ 706 (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2)) $ t) = 707 apfst (curry (op ::) (t1, t2)) (ext t) 708 | ext t = ([], t) 709 in ext t end 710 fun eq_congruent_tac ctxt t = 711 let 712 val (eqs, g) = extract_equal_terms t 713 fun replace1 (t1, t2) (g, tac) = 714 let 715 val abs_t1 = lambda t2 g 716 val subst = Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [t1, t2, abs_t1]) 717 @{thm subst} 718 in (Term.betapply (abs_t1, t1), 719 tac THEN' resolve_tac ctxt [subst] 720 THEN' TRY' (assume_tac ctxt)) end 721 val (_, tac) = fold replace1 eqs (g, K all_tac) 722 in 723 tac 724 end 725in 726 727fun eq_congruent_pred ctxt _ t = 728 SMT_Replay_Methods.prove ctxt t (fn _ => 729 REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \<open>_ = _\<close>]} RSN (1, @{thm iffD2}) OF @{thms impI}]) 730 THEN' REPEAT' (eresolve_tac ctxt @{thms conjI}) 731 THEN' eq_congruent_tac ctxt t 732 THEN' resolve_tac ctxt @{thms refl excluded_middle 733 excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]}) 734 735end 736 737 738(* subproof *) 739 740fun subproof ctxt [prem] t = 741 SMT_Replay_Methods.prove ctxt t (fn _ => 742 (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}], 743 @{thm disj_not1[of \<open>\<not>_\<close>, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]] 744 THEN' resolve_tac ctxt [prem] 745 THEN_ALL_NEW assume_tac ctxt 746 THEN' TRY' (assume_tac ctxt)) 747 ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt)) 748 749 750(* la_rw_eq *) 751 752val la_rw_eq_thm = @{lemma \<open>(a :: nat) = b \<or> (a \<le> b) \<or> (a \<ge> b)\<close> 753 by auto} 754 755fun la_rw_eq ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => 756 resolve_tac ctxt [la_rw_eq_thm]) 757 758(* congruence *) 759fun cong ctxt thms = SMT_Replay_Methods.try_provers ctxt 760 (string_of_verit_rule Cong) [ 761 ("basic", SMT_Replay_Methods.cong_basic ctxt thms), 762 ("full", SMT_Replay_Methods.cong_full ctxt thms), 763 ("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms)] thms 764 765 766fun unsupported rule ctxt thms _ t = SMT_Replay_Methods.replay_error ctxt "Unsupported verit rule" 767 rule thms t 768 769fun ignore_args f ctxt thm _ t = f ctxt thm t 770 771fun choose Bind = ignore_args bind 772 | choose Refl = ignore_args refl 773 | choose And_Pos = ignore_args and_pos 774 | choose And_Neg = ignore_args and_neg_rule 775 | choose Cong = ignore_args cong 776 | choose Equiv_pos1 = ignore_args equiv_pos1 777 | choose Equiv_pos2 = ignore_args equiv_pos2 778 | choose Equiv_neg1 = ignore_args equiv_neg1 779 | choose Equiv_neg2 = ignore_args equiv_neg2 780 | choose Equiv1 = ignore_args equiv1 781 | choose Equiv2 = ignore_args equiv2 782 | choose Not_Equiv1 = ignore_args not_equiv1 783 | choose Not_Equiv2 = ignore_args not_equiv2 784 | choose Not_Implies1 = ignore_args not_implies1 785 | choose Not_Implies2 = ignore_args not_implies2 786 | choose Implies_Neg1 = ignore_args implies_neg1 787 | choose Implies_Neg2 = ignore_args implies_neg2 788 | choose Implies_Pos = ignore_args implies_pos 789 | choose Implies = ignore_args implies_rules 790 | choose Forall_Inst = forall_inst 791 | choose Skolem_Forall = ignore_args skolem_forall 792 | choose Skolem_Ex = ignore_args skolem_ex 793 | choose Or = ignore_args or 794 | choose Theory_Resolution = ignore_args unit_res 795 | choose Resolution = ignore_args unit_res 796 | choose Eq_Reflexive = ignore_args eq_reflexive 797 | choose Connective_Equiv = ignore_args connective_equiv 798 | choose Trans = ignore_args trans 799 | choose False = ignore_args false_rule 800 | choose Tmp_AC_Simp = ignore_args tmp_AC_rule 801 | choose And = ignore_args and_rule 802 | choose Not_And = ignore_args not_and_rule 803 | choose Not_Or = ignore_args not_or_rule 804 | choose Or_Pos = ignore_args or_pos_rule 805 | choose Or_Neg = ignore_args or_neg_rule 806 | choose Tmp_Bfun_Elim = ignore_args tmp_bfun_elim 807 | choose ITE1 = ignore_args ite1 808 | choose ITE2 = ignore_args ite2 809 | choose Not_ITE1 = ignore_args not_ite1 810 | choose Not_ITE2 = ignore_args not_ite2 811 | choose ITE_Pos1 = ignore_args ite_pos1 812 | choose ITE_Pos2 = ignore_args ite_pos2 813 | choose ITE_Neg1 = ignore_args ite_neg1 814 | choose ITE_Neg2 = ignore_args ite_neg2 815 | choose ITE_Intro = ignore_args ite_intro 816 | choose LA_Disequality = ignore_args Z3_Replay_Methods.arith_th_lemma 817 | choose LIA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma 818 | choose LA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma 819 | choose LA_Totality = ignore_args Z3_Replay_Methods.arith_th_lemma 820 | choose LA_Tautology = ignore_args Z3_Replay_Methods.arith_th_lemma 821 | choose LA_RW_Eq = ignore_args la_rw_eq 822 | choose NLA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma 823 | choose Normalized_Input = ignore_args normalized_input 824 | choose Qnt_Rm_Unused = ignore_args qnt_rm_unused 825 | choose Qnt_Simplify = ignore_args qnt_simplify 826 | choose Qnt_Join = ignore_args qnt_join 827 | choose Eq_Congruent_Pred = ignore_args eq_congruent_pred 828 | choose Eq_Congruent = ignore_args eq_congruent_pred 829 | choose Eq_Transitive = ignore_args eq_transitive 830 | choose Local_Input = ignore_args refl 831 | choose Subproof = ignore_args subproof 832 | choose r = unsupported (string_of_verit_rule r) 833 834type Verit_method = Proof.context -> thm list -> term -> thm 835type abs_context = int * term Termtab.table 836 837fun with_tracing rule method ctxt thms args t = 838 let val _ = SMT_Replay_Methods.trace_goal ctxt rule thms t 839 in method ctxt thms args t end 840 841fun method_for rule = with_tracing rule (choose (verit_rule_of rule)) 842 843end; 844