diff --git a/src/HOL/SMT.thy b/src/HOL/SMT.thy --- a/src/HOL/SMT.thy +++ b/src/HOL/SMT.thy @@ -1,895 +1,896 @@ (* Title: HOL/SMT.thy Author: Sascha Boehme, TU Muenchen Author: Jasmin Blanchette, VU Amsterdam *) section \Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\ theory SMT imports Divides Numeral_Simprocs keywords "smt_status" :: diag begin subsection \A skolemization tactic and proof method\ lemma choices: "\Q. \x. \y ya. Q x y ya \ \f fa. \x. Q x (f x) (fa x)" "\Q. \x. \y ya yb. Q x y ya yb \ \f fa fb. \x. Q x (f x) (fa x) (fb x)" "\Q. \x. \y ya yb yc. Q x y ya yb yc \ \f fa fb fc. \x. Q x (f x) (fa x) (fb x) (fc x)" "\Q. \x. \y ya yb yc yd. Q x y ya yb yc yd \ \f fa fb fc fd. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x)" "\Q. \x. \y ya yb yc yd ye. Q x y ya yb yc yd ye \ \f fa fb fc fd fe. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" "\Q. \x. \y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \ \f fa fb fc fd fe ff. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" "\Q. \x. \y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \ \f fa fb fc fd fe ff fg. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" by metis+ lemma bchoices: "\Q. \x \ S. \y ya. Q x y ya \ \f fa. \x \ S. Q x (f x) (fa x)" "\Q. \x \ S. \y ya yb. Q x y ya yb \ \f fa fb. \x \ S. Q x (f x) (fa x) (fb x)" "\Q. \x \ S. \y ya yb yc. Q x y ya yb yc \ \f fa fb fc. \x \ S. Q x (f x) (fa x) (fb x) (fc x)" "\Q. \x \ S. \y ya yb yc yd. Q x y ya yb yc yd \ \f fa fb fc fd. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x)" "\Q. \x \ S. \y ya yb yc yd ye. Q x y ya yb yc yd ye \ \f fa fb fc fd fe. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" "\Q. \x \ S. \y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \ \f fa fb fc fd fe ff. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" "\Q. \x \ S. \y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \ \f fa fb fc fd fe ff fg. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" by metis+ ML \ fun moura_tac ctxt = Atomize_Elim.atomize_elim_tac ctxt THEN' SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs) ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE' blast_tac ctxt)) \ method_setup moura = \ Scan.succeed (SIMPLE_METHOD' o moura_tac) \ "solve skolemization goals, especially those arising from Z3 proofs" hide_fact (open) choices bchoices subsection \Triggers for quantifier instantiation\ text \ Some SMT solvers support patterns as a quantifier instantiation heuristics. Patterns may either be positive terms (tagged by "pat") triggering quantifier instantiations -- when the solver finds a term matching a positive pattern, it instantiates the corresponding quantifier accordingly -- or negative terms (tagged by "nopat") inhibiting quantifier instantiations. A list of patterns of the same kind is called a multipattern, and all patterns in a multipattern are considered conjunctively for quantifier instantiation. A list of multipatterns is called a trigger, and their multipatterns act disjunctively during quantifier instantiation. Each multipattern should mention at least all quantified variables of the preceding quantifier block. \ typedecl 'a symb_list consts Symb_Nil :: "'a symb_list" Symb_Cons :: "'a \ 'a symb_list \ 'a symb_list" typedecl pattern consts pat :: "'a \ pattern" nopat :: "'a \ pattern" definition trigger :: "pattern symb_list symb_list \ bool \ bool" where "trigger _ P = P" subsection \Higher-order encoding\ text \ Application is made explicit for constants occurring with varying numbers of arguments. This is achieved by the introduction of the following constant. \ definition fun_app :: "'a \ 'a" where "fun_app f = f" text \ Some solvers support a theory of arrays which can be used to encode higher-order functions. The following set of lemmas specifies the properties of such (extensional) arrays. \ lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_app_def subsection \Normalization\ lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)" by simp lemmas Ex1_def_raw = Ex1_def[abs_def] lemmas Ball_def_raw = Ball_def[abs_def] lemmas Bex_def_raw = Bex_def[abs_def] lemmas abs_if_raw = abs_if[abs_def] lemmas min_def_raw = min_def[abs_def] lemmas max_def_raw = max_def[abs_def] lemma nat_zero_as_int: "0 = nat 0" by simp lemma nat_one_as_int: "1 = nat 1" by simp lemma nat_numeral_as_int: "numeral = (\i. nat (numeral i))" by simp lemma nat_less_as_int: "(<) = (\a b. int a < int b)" by simp lemma nat_leq_as_int: "(\) = (\a b. int a \ int b)" by simp lemma Suc_as_int: "Suc = (\a. nat (int a + 1))" by (rule ext) simp lemma nat_plus_as_int: "(+) = (\a b. nat (int a + int b))" by (rule ext)+ simp lemma nat_minus_as_int: "(-) = (\a b. nat (int a - int b))" by (rule ext)+ simp lemma nat_times_as_int: "(*) = (\a b. nat (int a * int b))" by (simp add: nat_mult_distrib) lemma nat_div_as_int: "(div) = (\a b. nat (int a div int b))" by (simp add: nat_div_distrib) lemma nat_mod_as_int: "(mod) = (\a b. nat (int a mod int b))" by (simp add: nat_mod_distrib) lemma int_Suc: "int (Suc n) = int n + 1" by simp lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add) lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto lemma nat_int_comparison: fixes a b :: nat shows "(a = b) = (int a = int b)" and "(a < b) = (int a < int b)" and "(a \ b) = (int a \ int b)" by simp_all lemma int_ops: fixes a b :: nat shows "int 0 = 0" and "int 1 = 1" and "int (numeral n) = numeral n" and "int (Suc a) = int a + 1" and "int (a + b) = int a + int b" and "int (a - b) = (if int a < int b then 0 else int a - int b)" and "int (a * b) = int a * int b" and "int (a div b) = int a div int b" and "int (a mod b) = int a mod int b" by (auto intro: zdiv_int zmod_int) lemma int_if: fixes a b :: nat shows "int (if P then a else b) = (if P then int a else int b)" by simp subsection \Integer division and modulo for Z3\ text \ The following Z3-inspired definitions are overspecified for the case where \l = 0\. This Schönheitsfehler is corrected in the \div_as_z3div\ and \mod_as_z3mod\ theorems. \ definition z3div :: "int \ int \ int" where "z3div k l = (if l \ 0 then k div l else - (k div - l))" definition z3mod :: "int \ int \ int" where "z3mod k l = k mod (if l \ 0 then l else - l)" lemma div_as_z3div: "\k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div (- k) (- l))" by (simp add: z3div_def) lemma mod_as_z3mod: "\k l. k mod l = (if l = 0 then k else if l > 0 then z3mod k l else - z3mod (- k) (- l))" by (simp add: z3mod_def) subsection \Extra theorems for veriT reconstruction\ lemma verit_sko_forall: \(\x. P x) \ P (SOME x. \P x)\ using someI[of \\x. \P x\] by auto lemma verit_sko_forall': \P (SOME x. \P x) = A \ (\x. P x) = A\ by (subst verit_sko_forall) lemma verit_sko_forall'': \B = A \ (SOME x. P x) = A \ (SOME x. P x) = B\ by auto lemma verit_sko_forall_indirect: \x = (SOME x. \P x) \ (\x. P x) \ P x\ using someI[of \\x. \P x\] by auto lemma verit_sko_forall_indirect2: \x = (SOME x. \P x) \ (\x :: 'a. (P x = P' x)) \(\x. P' x) \ P x\ using someI[of \\x. \P x\] by auto lemma verit_sko_ex: \(\x. P x) \ P (SOME x. P x)\ using someI[of \\x. P x\] by auto lemma verit_sko_ex': \P (SOME x. P x) = A \ (\x. P x) = A\ by (subst verit_sko_ex) lemma verit_sko_ex_indirect: \x = (SOME x. P x) \ (\x. P x) \ P x\ using someI[of \\x. P x\] by auto lemma verit_sko_ex_indirect2: \x = (SOME x. P x) \ (\x. P x = P' x) \ (\x. P' x) \ P x\ using someI[of \\x. P x\] by auto lemma verit_Pure_trans: \P \ Q \ Q \ P\ by auto lemma verit_if_cong: assumes \b \ c\ and \c \ x \ u\ and \\ c \ y \ v\ shows \(if b then x else y) \ (if c then u else v)\ using assms if_cong[of b c x u] by auto lemma verit_if_weak_cong': \b \ c \ (if b then x else y) \ (if c then x else y)\ by auto lemma verit_or_neg: \(A \ B) \ B \ \A\ \(\A \ B) \ B \ A\ by auto lemma verit_subst_bool: \P \ f True \ f P\ by auto lemma verit_and_pos: \(a \ \(b \ c) \ A) \ \(a \ b \ c) \ A\ \(a \ b \ A) \ \(a \ b) \ A\ \(a \ A) \ \a \ A\ \(\a \ A) \ a \ A\ by blast+ lemma verit_or_pos: \A \ A' \ (c \ A) \ (\c \ A')\ \A \ A' \ (\c \ A) \ (c \ A')\ by blast+ lemma verit_la_generic: \(a::int) \ x \ a = x \ a \ x\ by linarith lemma verit_bfun_elim: \(if b then P True else P False) = P b\ \(\b. P' b) = (P' False \ P' True)\ \(\b. P' b) = (P' False \ P' True)\ by (cases b) (auto simp: all_bool_eq ex_bool_eq) lemma verit_eq_true_simplify: \(P = True) \ P\ by auto lemma verit_and_neg: \(a \ \b \ A) \ \(a \ b) \ A\ \(a \ A) \ \a \ A\ \(\a \ A) \ a \ A\ by blast+ lemma verit_forall_inst: \A \ B \ \A \ B\ \\A \ B \ A \ B\ \A \ B \ \B \ A\ \A \ \B \ B \ A\ \A \ B \ \A \ B\ \\A \ B \ A \ B\ by blast+ lemma verit_eq_transitive: \A = B \ B = C \ A = C\ \A = B \ C = B \ A = C\ \B = A \ B = C \ A = C\ \B = A \ C = B \ A = C\ by auto lemma verit_bool_simplify: \\(P \ Q) \ P \ \Q\ \\(P \ Q) \ \P \ \Q\ \\(P \ Q) \ \P \ \Q\ \(P \ (Q \ R)) \ ((P \ Q) \ R)\ \((P \ Q) \ Q) \ P \ Q\ \(Q \ (P \ Q)) \ (P \ Q)\ \ \This rule was inverted\ \P \ (P \ Q) \ P \ Q\ \(P \ Q) \ P \ P \ Q\ (* \\Additional rules:\ * \((P \ Q) \ P) \ P\ * \((P \ Q) \ Q) \ P \ Q\ * \(P \ Q) \ P\ *) unfolding not_imp imp_conjL by auto text \We need the last equation for \<^term>\\(\a b. \P a b)\\ lemma verit_connective_def: \ \the definition of XOR is missing as the operator is not generated by Isabelle\ \(A = B) \ ((A \ B) \ (B \ A))\ \(If A B C) = ((A \ B) \ (\A \ C))\ \(\x. P x) \ \(\x. \P x)\ \\(\x. P x) \ (\x. \P x)\ by auto lemma verit_ite_simplify: \(If True B C) = B\ \(If False B C) = C\ \(If A' B B) = B\ \(If (\A') B C) = (If A' C B)\ \(If c (If c A B) C) = (If c A C)\ \(If c C (If c A B)) = (If c C B)\ \(If A' True False) = A'\ \(If A' False True) \ \A'\ \(If A' True B') \ A'\B'\ \(If A' B' False) \ A'\B'\ \(If A' False B') \ \A'\B'\ \(If A' B' True) \ \A'\B'\ \x \ True \ x\ \x \ False \ x\ for B C :: 'a and A' B' C' :: bool by auto lemma verit_and_simplify1: \True \ b \ b\ \b \ True \ b\ \False \ b \ False\ \b \ False \ False\ \(c \ \c) \ False\ \(\c \ c) \ False\ \\\a = a\ by auto lemmas verit_and_simplify = conj_ac de_Morgan_conj disj_not1 lemma verit_or_simplify_1: \False \ b \ b\ \b \ False \ b\ \b \ \b\ \\b \ b\ by auto lemmas verit_or_simplify = disj_ac lemma verit_not_simplify: \\ \b \ b\ \\True \ False\ \\False \ True\ by auto lemma verit_implies_simplify: \(\a \ \b) \ (b \ a)\ \(False \ a) \ True\ \(a \ True) \ True\ \(True \ a) \ a\ \(a \ False) \ \a\ \(a \ a) \ True\ \(\a \ a) \ a\ \(a \ \a) \ \a\ \((a \ b) \ b) \ a \ b\ by auto lemma verit_equiv_simplify: \((\a) = (\b)) \ (a = b)\ \(a = a) \ True\ \(a = (\a)) \ False\ \((\a) = a) \ False\ \(True = a) \ a\ \(a = True) \ a\ \(False = a) \ \a\ \(a = False) \ \a\ \\\a \ a\ \(\ False) = True\ for a b :: bool by auto lemmas verit_eq_simplify = semiring_char_0_class.eq_numeral_simps eq_refl zero_neq_one num.simps neg_equal_zero equal_neg_zero one_neq_zero neg_equal_iff_equal lemma verit_minus_simplify: \(a :: 'a :: cancel_comm_monoid_add) - a = 0\ \(a :: 'a :: cancel_comm_monoid_add) - 0 = a\ \0 - (b :: 'b :: {group_add}) = -b\ \- (- (b :: 'b :: group_add)) = b\ by auto lemma verit_sum_simplify: \(a :: 'a :: cancel_comm_monoid_add) + 0 = a\ by auto lemmas verit_prod_simplify = (* already included: mult_zero_class.mult_zero_right mult_zero_class.mult_zero_left *) mult_1 mult_1_right lemma verit_comp_simplify1: \(a :: 'a ::order) < a \ False\ \a \ a\ \\(b' \ a') \ (a' :: 'b :: linorder) < b'\ by auto lemmas verit_comp_simplify = verit_comp_simplify1 le_numeral_simps le_num_simps less_numeral_simps less_num_simps zero_less_one zero_le_one less_neg_numeral_simps lemma verit_la_disequality: \(a :: 'a ::linorder) = b \ \a \ b \ \b \ a\ by auto context begin text \For the reconstruction, we need to keep the order of the arguments.\ named_theorems smt_arith_multiplication \Theorems to reconstruct arithmetic theorems.\ named_theorems smt_arith_combine \Theorems to reconstruct arithmetic theorems.\ named_theorems smt_arith_simplify \Theorems to combine theorems in the LA procedure\ lemmas [smt_arith_simplify] = div_add dvd_numeral_simp divmod_steps less_num_simps le_num_simps if_True if_False divmod_cancel dvd_mult dvd_mult2 less_irrefl prod.case numeral_plus_one divmod_step_eq order.refl le_zero_eq le_numeral_simps less_numeral_simps mult.right_neutral simp_thms divides_aux_eq mult_nonneg_nonneg dvd_imp_mod_0 dvd_add zero_less_one mod_mult_self4 numeral_mod_numeral divmod_trivial prod.sel mult.left_neutral div_pos_pos_trivial arith_simps div_add div_mult_self1 add_le_cancel_left add_le_same_cancel2 not_one_le_zero le_numeral_simps add_le_same_cancel1 zero_neq_one zero_le_one le_num_simps add_Suc mod_div_trivial nat.distinct mult_minus_right add.inverse_inverse distrib_left_numeral mult_num_simps numeral_times_numeral add_num_simps divmod_steps rel_simps if_True if_False numeral_div_numeral divmod_cancel prod.case add_num_simps one_plus_numeral fst_conv divmod_step_eq arith_simps sub_num_simps dbl_inc_simps dbl_simps mult_1 add_le_cancel_right left_diff_distrib_numeral add_uminus_conv_diff zero_neq_one zero_le_one One_nat_def add_Suc mod_div_trivial nat.distinct of_int_1 numerals numeral_One of_int_numeral add_uminus_conv_diff zle_diff1_eq add_less_same_cancel2 minus_add_distrib add_uminus_conv_diff mult.left_neutral semiring_class.distrib_right add_diff_cancel_left' add_diff_eq ring_distribs mult_minus_left minus_diff_eq lemma [smt_arith_simplify]: \\ (a' :: 'a :: linorder) < b' \ b' \ a'\ \\ (a' :: 'a :: linorder) \ b' \ b' < a'\ \(c::int) mod Numeral1 = 0\ \(a::nat) mod Numeral1 = 0\ \(c::int) div Numeral1 = c\ \a div Numeral1 = a\ \(c::int) mod 1 = 0\ \a mod 1 = 0\ \(c::int) div 1 = c\ \a div 1 = a\ \\(a' \ b') \ a' = b'\ by auto lemma div_mod_decomp: "A = (A div n) * n + (A mod n)" for A :: nat by auto lemma div_less_mono: fixes A B :: nat assumes "A < B" "0 < n" and mod: "A mod n = 0""B mod n = 0" shows "(A div n) < (B div n)" proof - show ?thesis using assms(1) apply (subst (asm) div_mod_decomp[of "A" n]) apply (subst (asm) div_mod_decomp[of "B" n]) unfolding mod by (use assms(2,3) in \auto simp: ac_simps\) qed lemma verit_le_mono_div: fixes A B :: nat assumes "A < B" "0 < n" shows "(A div n) + (if B mod n = 0 then 1 else 0) \ (B div n)" by (auto simp: ac_simps Suc_leI assms less_mult_imp_div_less div_le_mono less_imp_le_nat) lemmas [smt_arith_multiplication] = verit_le_mono_div[THEN mult_le_mono1, unfolded add_mult_distrib] div_le_mono[THEN mult_le_mono2, unfolded add_mult_distrib] lemma div_mod_decomp_int: "A = (A div n) * n + (A mod n)" for A :: int by auto lemma zdiv_mono_strict: fixes A B :: int assumes "A < B" "0 < n" and mod: "A mod n = 0""B mod n = 0" shows "(A div n) < (B div n)" proof - show ?thesis using assms(1) apply (subst (asm) div_mod_decomp_int[of A n]) apply (subst (asm) div_mod_decomp_int[of B n]) unfolding mod by (use assms(2,3) in \auto simp: ac_simps\) qed lemma verit_le_mono_div_int: fixes A B :: int assumes "A < B" "0 < n" shows "(A div n) + (if B mod n = 0 then 1 else 0) \ (B div n)" proof - have f2: "B div n = A div n \ A div n < B div n" by (metis (no_types) assms less_le zdiv_mono1) have "B div n \ A div n \ B mod n \ 0" using assms(1) by (metis Groups.add_ac(2) assms(2) eucl_rel_int eucl_rel_int_iff group_cancel.rule0 le_add_same_cancel2 not_le) then have "B mod n = 0 \ A div n + (if B mod n = 0 then 1 else 0) \ B div n" using f2 by (auto dest: zless_imp_add1_zle) then show ?thesis using assms zdiv_mono1 by auto qed lemma verit_less_mono_div_int2: fixes A B :: int assumes "A \ B" "0 < -n" shows "(A div n) \ (B div n)" using assms(1) assms(2) zdiv_mono1_neg by auto lemmas [smt_arith_multiplication] = verit_le_mono_div_int[THEN mult_left_mono, unfolded int_distrib] zdiv_mono1[THEN mult_left_mono, unfolded int_distrib] lemmas [smt_arith_multiplication] = arg_cong[of _ _ \\a :: nat. a div n * p\ for n p :: nat, THEN sym] arg_cong[of _ _ \\a :: int. a div n * p\ for n p :: int, THEN sym] lemma [smt_arith_combine]: "a < b \ c < d \ a + c + 2 \ b + d" "a < b \ c \ d \ a + c + 1 \ b + d" "a \ b \ c < d \ a + c + 1 \ b + d" for a b c :: int by auto lemma [smt_arith_combine]: "a < b \ c < d \ a + c + 2 \ b + d" "a < b \ c \ d \ a + c + 1 \ b + d" "a \ b \ c < d \ a + c + 1 \ b + d" for a b c :: nat by auto lemmas [smt_arith_combine] = add_strict_mono add_less_le_mono add_mono add_le_less_mono lemma [smt_arith_combine]: \m < n \ c = d \ m + c < n + d\ \m \ n \ c = d \ m + c \ n + d\ \c = d \ m < n \ m + c < n + d\ \c = d \ m \ n \ m + c \ n + d\ for m :: \'a :: ordered_cancel_ab_semigroup_add\ by (auto intro: ordered_cancel_ab_semigroup_add_class.add_strict_right_mono ordered_ab_semigroup_add_class.add_right_mono) lemma verit_negate_coefficient: \a \ (b :: 'a :: {ordered_ab_group_add}) \ -a \ -b\ \a < b \ -a > -b\ \a = b \ -a = -b\ by auto end lemma verit_ite_intro: \(if a then P (if a then a' else b') else Q) \ (if a then P a' else Q)\ \(if a then P' else Q' (if a then a' else b')) \ (if a then P' else Q' b')\ \A = f (if a then R else S) \ (if a then A = f R else A = f S)\ by auto lemma verit_ite_if_cong: fixes x y :: bool assumes "b=c" and "c \ True \ x = u" and "c \ False \ y = v" shows "(if b then x else y) \ (if c then u else v)" proof - have H: "(if b then x else y) = (if c then u else v)" using assms by (auto split: if_splits) show "(if b then x else y) \ (if c then u else v)" by (subst H) auto qed subsection \Setup\ ML_file \Tools/SMT/smt_util.ML\ ML_file \Tools/SMT/smt_failure.ML\ ML_file \Tools/SMT/smt_config.ML\ ML_file \Tools/SMT/smt_builtin.ML\ ML_file \Tools/SMT/smt_datatypes.ML\ ML_file \Tools/SMT/smt_normalize.ML\ ML_file \Tools/SMT/smt_translate.ML\ ML_file \Tools/SMT/smtlib.ML\ ML_file \Tools/SMT/smtlib_interface.ML\ ML_file \Tools/SMT/smtlib_proof.ML\ ML_file \Tools/SMT/smtlib_isar.ML\ ML_file \Tools/SMT/z3_proof.ML\ ML_file \Tools/SMT/z3_isar.ML\ ML_file \Tools/SMT/smt_solver.ML\ ML_file \Tools/SMT/cvc4_interface.ML\ +ML_file \Tools/SMT/lethe_proof.ML\ +ML_file \Tools/SMT/lethe_isar.ML\ +ML_file \Tools/SMT/lethe_proof_parse.ML\ ML_file \Tools/SMT/cvc4_proof_parse.ML\ ML_file \Tools/SMT/verit_proof.ML\ -ML_file \Tools/SMT/verit_isar.ML\ -ML_file \Tools/SMT/verit_proof_parse.ML\ ML_file \Tools/SMT/conj_disj_perm.ML\ ML_file \Tools/SMT/smt_replay_methods.ML\ ML_file \Tools/SMT/smt_replay.ML\ ML_file \Tools/SMT/smt_replay_arith.ML\ ML_file \Tools/SMT/z3_interface.ML\ ML_file \Tools/SMT/z3_replay_rules.ML\ ML_file \Tools/SMT/z3_replay_methods.ML\ ML_file \Tools/SMT/z3_replay.ML\ +ML_file \Tools/SMT/lethe_replay_methods.ML\ ML_file \Tools/SMT/verit_replay_methods.ML\ ML_file \Tools/SMT/verit_replay.ML\ ML_file \Tools/SMT/smt_systems.ML\ subsection \Configuration\ text \ The current configuration can be printed by the command \smt_status\, which shows the values of most options. \ subsection \General configuration options\ text \ The option \smt_solver\ can be used to change the target SMT solver. The possible values can be obtained from the \smt_status\ command. \ declare [[smt_solver = z3]] text \ Since SMT solvers are potentially nonterminating, there is a timeout (given in seconds) to restrict their runtime. \ declare [[smt_timeout = 0]] text \ SMT solvers apply randomized heuristics. In case a problem is not solvable by an SMT solver, changing the following option might help. \ declare [[smt_random_seed = 1]] text \ In general, the binding to SMT solvers runs as an oracle, i.e, the SMT solvers are fully trusted without additional checks. The following option can cause the SMT solver to run in proof-producing mode, giving a checkable certificate. This is currently implemented only for veriT and Z3. \ declare [[smt_oracle = false]] text \ Each SMT solver provides several command-line options to tweak its behaviour. They can be passed to the solver by setting the following options. \ declare [[cvc4_options = ""]] declare [[verit_options = ""]] declare [[z3_options = ""]] text \ The SMT method provides an inference mechanism to detect simple triggers in quantified formulas, which might increase the number of problems solvable by SMT solvers (note: triggers guide quantifier instantiations in the SMT solver). To turn it on, set the following option. \ declare [[smt_infer_triggers = false]] text \ Enable the following option to use built-in support for datatypes, codatatypes, and records in CVC4. Currently, this is implemented only in oracle mode. \ declare [[cvc4_extensions = false]] text \ Enable the following option to use built-in support for div/mod, datatypes, and records in Z3. Currently, this is implemented only in oracle mode. \ declare [[z3_extensions = false]] subsection \Certificates\ text \ By setting the option \smt_certificates\ to the name of a file, all following applications of an SMT solver a cached in that file. Any further application of the same SMT solver (using the very same configuration) re-uses the cached certificate instead of invoking the solver. An empty string disables caching certificates. The filename should be given as an explicit path. It is good practice to use the name of the current theory (with ending \.certs\ instead of \.thy\) as the certificates file. Certificate files should be used at most once in a certain theory context, to avoid race conditions with other concurrent accesses. \ declare [[smt_certificates = ""]] text \ The option \smt_read_only_certificates\ controls whether only stored certificates should be used or invocation of an SMT solver is allowed. When set to \true\, no SMT solver will ever be invoked and only the existing certificates found in the configured cache are used; when set to \false\ and there is no cached certificate for some proposition, then the configured SMT solver is invoked. \ declare [[smt_read_only_certificates = false]] subsection \Tracing\ text \ The SMT method, when applied, traces important information. To make it entirely silent, set the following option to \false\. \ declare [[smt_verbose = true]] text \ For tracing the generated problem file given to the SMT solver as well as the returned result of the solver, the option \smt_trace\ should be set to \true\. \ declare [[smt_trace = false]] subsection \Schematic rules for Z3 proof reconstruction\ text \ Several prof rules of Z3 are not very well documented. There are two lemma groups which can turn failing Z3 proof reconstruction attempts into succeeding ones: the facts in \z3_rule\ are tried prior to any implemented reconstruction procedure for all uncertain Z3 proof rules; the facts in \z3_simp\ are only fed to invocations of the simplifier when reconstructing theory-specific proof steps. \ lemmas [z3_rule] = refl eq_commute conj_commute disj_commute simp_thms nnf_simps ring_distribs field_simps times_divide_eq_right times_divide_eq_left if_True if_False not_not NO_MATCH_def lemma [z3_rule]: "(P \ Q) = (\ (\ P \ \ Q))" "(P \ Q) = (\ (\ Q \ \ P))" "(\ P \ Q) = (\ (P \ \ Q))" "(\ P \ Q) = (\ (\ Q \ P))" "(P \ \ Q) = (\ (\ P \ Q))" "(P \ \ Q) = (\ (Q \ \ P))" "(\ P \ \ Q) = (\ (P \ Q))" "(\ P \ \ Q) = (\ (Q \ P))" by auto lemma [z3_rule]: "(P \ Q) = (Q \ \ P)" "(\ P \ Q) = (P \ Q)" "(\ P \ Q) = (Q \ P)" "(True \ P) = P" "(P \ True) = True" "(False \ P) = True" "(P \ P) = True" "(\ (A \ \ B)) \ (A \ B)" by auto lemma [z3_rule]: "((P = Q) \ R) = (R \ (Q = (\ P)))" by auto lemma [z3_rule]: "(\ True) = False" "(\ False) = True" "(x = x) = True" "(P = True) = P" "(True = P) = P" "(P = False) = (\ P)" "(False = P) = (\ P)" "((\ P) = P) = False" "(P = (\ P)) = False" "((\ P) = (\ Q)) = (P = Q)" "\ (P = (\ Q)) = (P = Q)" "\ ((\ P) = Q) = (P = Q)" "(P \ Q) = (Q = (\ P))" "(P = Q) = ((\ P \ Q) \ (P \ \ Q))" "(P \ Q) = ((\ P \ \ Q) \ (P \ Q))" by auto lemma [z3_rule]: "(if P then P else \ P) = True" "(if \ P then \ P else P) = True" "(if P then True else False) = P" "(if P then False else True) = (\ P)" "(if P then Q else True) = ((\ P) \ Q)" "(if P then Q else True) = (Q \ (\ P))" "(if P then Q else \ Q) = (P = Q)" "(if P then Q else \ Q) = (Q = P)" "(if P then \ Q else Q) = (P = (\ Q))" "(if P then \ Q else Q) = ((\ Q) = P)" "(if \ P then x else y) = (if P then y else x)" "(if P then (if Q then x else y) else x) = (if P \ (\ Q) then y else x)" "(if P then (if Q then x else y) else x) = (if (\ Q) \ P then y else x)" "(if P then (if Q then x else y) else y) = (if P \ Q then x else y)" "(if P then (if Q then x else y) else y) = (if Q \ P then x else y)" "(if P then x else if P then y else z) = (if P then x else z)" "(if P then x else if Q then x else y) = (if P \ Q then x else y)" "(if P then x else if Q then x else y) = (if Q \ P then x else y)" "(if P then x = y else x = z) = (x = (if P then y else z))" "(if P then x = y else y = z) = (y = (if P then x else z))" "(if P then x = y else z = y) = (y = (if P then x else z))" by auto lemma [z3_rule]: "0 + (x::int) = x" "x + 0 = x" "x + x = 2 * x" "0 * x = 0" "1 * x = x" "x + y = y + x" by auto lemma [z3_rule]: (* for def-axiom *) "P = Q \ P \ Q" "P = Q \ \ P \ \ Q" "(\ P) = Q \ \ P \ Q" "(\ P) = Q \ P \ \ Q" "P = (\ Q) \ \ P \ Q" "P = (\ Q) \ P \ \ Q" "P \ Q \ P \ \ Q" "P \ Q \ \ P \ Q" "P \ (\ Q) \ P \ Q" "(\ P) \ Q \ P \ Q" "P \ Q \ P \ (\ Q)" "P \ Q \ (\ P) \ Q" "P \ \ Q \ P \ Q" "\ P \ Q \ P \ Q" "P \ y = (if P then x else y)" "P \ (if P then x else y) = y" "\ P \ x = (if P then x else y)" "\ P \ (if P then x else y) = x" "P \ R \ \ (if P then Q else R)" "\ P \ Q \ \ (if P then Q else R)" "\ (if P then Q else R) \ \ P \ Q" "\ (if P then Q else R) \ P \ R" "(if P then Q else R) \ \ P \ \ Q" "(if P then Q else R) \ P \ \ R" "(if P then \ Q else R) \ \ P \ Q" "(if P then Q else \ R) \ P \ R" by auto - hide_type (open) symb_list pattern hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod end diff --git a/src/HOL/Tools/SMT/lethe_isar.ML b/src/HOL/Tools/SMT/lethe_isar.ML new file mode 100644 --- /dev/null +++ b/src/HOL/Tools/SMT/lethe_isar.ML @@ -0,0 +1,60 @@ +(* Title: HOL/Tools/SMT/verit_isar.ML + Author: Mathias Fleury, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +LETHE proofs as generic ATP proofs for Isar proof reconstruction. +*) + +signature LETHE_ISAR = +sig + type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step + val atp_proof_of_veriT_proof: Proof.context -> term list -> thm list -> term list -> term -> + (string * term) list -> int list -> int -> (int * string) list -> Lethe_Proof.lethe_step list -> + (term, string) ATP_Proof.atp_step list +end; + +structure Lethe_Isar: LETHE_ISAR = +struct + +open ATP_Util +open ATP_Problem +open ATP_Proof +open ATP_Proof_Reconstruct +open SMTLIB_Interface +open SMTLIB_Isar +open Lethe_Proof + +fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids + conjecture_id fact_helper_ids = + let + fun steps_of (Lethe_Proof.Lethe_Step {id, rule, prems, concl, ...}) = + let + val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl + fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems) + in + if rule = input_rule then + let + val (_, id_num) = SMTLIB_Interface.role_and_index_of_assert_name id + val ss = the_list (AList.lookup (op =) fact_helper_ids id_num) + in + (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids + fact_helper_ts hyp_ts concl_t of + NONE => [] + | SOME (role0, concl00) => + let + val name0 = (id ^ "a", ss) + val concl0 = unskolemize_names ctxt concl00 + in + [(name0, role0, concl0, rule, []), + ((id, []), Plain, concl', rewrite_rule, + name0 :: normalizing_prems ctxt concl0)] + end) + end + else + [standard_step (if null prems then Lemma else Plain)] + end + in + maps steps_of + end + +end; diff --git a/src/HOL/Tools/SMT/lethe_proof.ML b/src/HOL/Tools/SMT/lethe_proof.ML new file mode 100644 --- /dev/null +++ b/src/HOL/Tools/SMT/lethe_proof.ML @@ -0,0 +1,785 @@ +(* Title: HOL/Tools/SMT/Lethe_Proof.ML + Author: Mathias Fleury, ENS Rennes + Author: Sascha Boehme, TU Muenchen + +Lethe proofs: parsing and abstract syntax tree. +*) + +signature LETHE_PROOF = +sig + (*proofs*) + datatype lethe_step = Lethe_Step of { + id: string, + rule: string, + prems: string list, + proof_ctxt: term list, + concl: term, + fixes: string list} + + datatype lethe_replay_node = Lethe_Replay_Node of { + id: string, + rule: string, + args: term list, + prems: string list, + proof_ctxt: term list, + concl: term, + bounds: (string * typ) list, + declarations: (string * term) list, + insts: term Symtab.table, + subproof: (string * typ) list * term list * term list * lethe_replay_node list} + + val mk_replay_node: string -> string -> term list -> string list -> term list -> + term -> (string * typ) list -> term Symtab.table -> (string * term) list -> + (string * typ) list * term list * term list * lethe_replay_node list -> lethe_replay_node + + (*proof parser*) + val parse: typ Symtab.table -> term Symtab.table -> string list -> + Proof.context -> lethe_step list * Proof.context + val parse_replay: typ Symtab.table -> term Symtab.table -> string list -> + Proof.context -> lethe_replay_node list * Proof.context + + val step_prefix : string + val input_rule: string + val keep_app_symbols: string -> bool + val keep_raw_lifting: string -> bool + val normalized_input_rule: string + val la_generic_rule : string + val rewrite_rule : string + val simp_arith_rule : string + val lethe_deep_skolemize_rule : string + val lethe_def : string + val subproof_rule : string + val local_input_rule : string + val not_not_rule : string + val contract_rule : string + val ite_intro_rule : string + val eq_congruent_rule : string + val eq_congruent_pred_rule : string + val skolemization_steps : string list + val theory_resolution2_rule: string + val equiv_pos2_rule: string + val th_resolution_rule: string + + val is_skolemization: string -> bool + val is_skolemization_step: lethe_replay_node -> bool + + val number_of_steps: lethe_replay_node list -> int + +end; + +structure Lethe_Proof: LETHE_PROOF = +struct + +open SMTLIB_Proof + +datatype raw_lethe_node = Raw_Lethe_Node of { + id: string, + rule: string, + args: SMTLIB.tree, + prems: string list, + concl: SMTLIB.tree, + declarations: (string * SMTLIB.tree) list, + subproof: raw_lethe_node list} + +fun mk_raw_node id rule args prems declarations concl subproof = + Raw_Lethe_Node {id = id, rule = rule, args = args, prems = prems, declarations = declarations, + concl = concl, subproof = subproof} + +datatype lethe_node = Lethe_Node of { + id: string, + rule: string, + prems: string list, + proof_ctxt: term list, + concl: term} + +fun mk_node id rule prems proof_ctxt concl = + Lethe_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl} + +datatype lethe_replay_node = Lethe_Replay_Node of { + id: string, + rule: string, + args: term list, + prems: string list, + proof_ctxt: term list, + concl: term, + bounds: (string * typ) list, + insts: term Symtab.table, + declarations: (string * term) list, + subproof: (string * typ) list * term list * term list * lethe_replay_node list} + +fun mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations subproof = + Lethe_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, + concl = concl, bounds = bounds, insts = insts, declarations = declarations, + subproof = subproof} + +datatype lethe_step = Lethe_Step of { + id: string, + rule: string, + prems: string list, + proof_ctxt: term list, + concl: term, + fixes: string list} + +fun mk_step id rule prems proof_ctxt concl fixes = + Lethe_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl, + fixes = fixes} + +val step_prefix = ".c" +val input_rule = "input" +val la_generic_rule = "la_generic" +val normalized_input_rule = "__normalized_input" (*arbitrary*) +val rewrite_rule = "__rewrite" (*arbitrary*) +val subproof_rule = "subproof" +val local_input_rule = "__local_input" (*arbitrary*) +val simp_arith_rule = "simp_arith" +val lethe_def = "__skolem_definition" (*arbitrary*) +val not_not_rule = "not_not" +val contract_rule = "contraction" +val eq_congruent_pred_rule = "eq_congruent_pred" +val eq_congruent_rule = "eq_congruent" +val ite_intro_rule = "ite_intro" +val default_skolem_rule = "sko_forall" (*arbitrary, but must be one of the skolems*) +val theory_resolution2_rule = "__theory_resolution2" (*arbitrary*) +val equiv_pos2_rule = "equiv_pos2" +val th_resolution_rule = "th_resolution" + +val skolemization_steps = ["sko_forall", "sko_ex"] +val is_skolemization = member (op =) skolemization_steps +val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule] +val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule] +val is_SH_trivial = member (op =) [not_not_rule, contract_rule] + +fun is_skolemization_step (Lethe_Replay_Node {id, ...}) = is_skolemization id + +(* Even the lethe developers do not know if the following rule can still appear in proofs: *) +val lethe_deep_skolemize_rule = "deep_skolemize" + +fun number_of_steps [] = 0 + | number_of_steps ((Lethe_Replay_Node {subproof = (_, _, _, subproof), ...}) :: pf) = + 1 + number_of_steps subproof + number_of_steps pf + +(* proof parser *) + +fun node_of p cx = + ([], cx) + ||>> `(with_fresh_names (term_of p)) + |>> snd + +fun synctactic_var_subst old_name new_name (u $ v) = + (synctactic_var_subst old_name new_name u $ synctactic_var_subst old_name new_name v) + | synctactic_var_subst old_name new_name (Abs (v, T, u)) = + Abs (if String.isPrefix old_name v then new_name else v, T, + synctactic_var_subst old_name new_name u) + | synctactic_var_subst old_name new_name (Free (v, T)) = + if String.isPrefix old_name v then Free (new_name, T) else Free (v, T) + | synctactic_var_subst _ _ t = t + +fun synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\HOL.eq\, T) $ t1 $ t2) = + Const(\<^const_name>\HOL.eq\, T) $ synctactic_var_subst old_name new_name t1 $ t2 + | synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\Trueprop\, T) $ t1) = + Const(\<^const_name>\Trueprop\, T) $ (synctatic_rew_in_lhs_subst old_name new_name t1) + | synctatic_rew_in_lhs_subst _ _ t = t + +fun add_bound_variables_to_ctxt cx = + fold (update_binding o + (fn (s, SOME typ) => (s, Term (Free (s, type_of cx typ))))) + +local + fun extract_symbols bds = + bds + |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) => [([x, y], typ)] + | t => raise (Fail ("match error " ^ @{make_string} t))) + |> flat + + (* onepoint can bind a variable to another variable or to a constant *) + fun extract_qnt_symbols cx bds = + bds + |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) => + (case node_of (SMTLIB.Sym y) cx of + ((_, []), _) => [([x], typ)] + | _ => [([x, y], typ)]) + | (SMTLIB.S (SMTLIB.Sym "=" :: SMTLIB.Sym x :: _), typ) => [([x], typ)] + | t => raise (Fail ("match error " ^ @{make_string} t))) + |> flat + + fun extract_symbols_map bds = + bds + |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, _], typ) => [([x], typ)]) + |> flat +in + +fun declared_csts _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [(x, typ)] + | declared_csts _ "__skolem_definition" t = raise (Fail ("unrecognized skolem_definition " ^ @{make_string} t)) + | declared_csts _ _ _ = [] + +fun skolems_introduced_by_rule (SMTLIB.S bds) = + fold (fn (SMTLIB.S [SMTLIB.Sym "=", _, SMTLIB.Sym y]) => curry (op ::) y) bds [] + +(*FIXME there is probably a way to use the information given by onepoint*) +fun bound_vars_by_rule _ "bind" (bds) = extract_symbols bds + | bound_vars_by_rule cx "onepoint" bds = extract_qnt_symbols cx bds + | bound_vars_by_rule _ "sko_forall" bds = extract_symbols_map bds + | bound_vars_by_rule _ "sko_ex" bds = extract_symbols_map bds + | bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [([x], SOME typ)] + | bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [_, SMTLIB.Sym x, _], _)] = [([x], NONE)] + | bound_vars_by_rule _ _ _ = [] + +(* Lethe adds "?" before some variables. *) +fun remove_all_qm (SMTLIB.Sym v :: l) = + SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l + | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l' + | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l + | remove_all_qm (v :: l) = v :: remove_all_qm l + | remove_all_qm [] = [] + +fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v) + | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l) + | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v + | remove_all_qm2 v = v + +end + +datatype step_kind = ASSUME | ANCHOR | NO_STEP | NORMAL_STEP | SKOLEM + +fun parse_raw_proof_steps (limit : string option) (ls : SMTLIB.tree list) (cx : name_bindings) : + (raw_lethe_node list * SMTLIB.tree list * name_bindings) = + let + fun rotate_pair (a, (b, c)) = ((a, b), c) + fun step_kind [] = (NO_STEP, SMTLIB.S [], []) + | step_kind ((p as SMTLIB.S (SMTLIB.Sym "anchor" :: _)) :: l) = (ANCHOR, p, l) + | step_kind ((p as SMTLIB.S (SMTLIB.Sym "assume" :: _)) :: l) = (ASSUME, p, l) + | step_kind ((p as SMTLIB.S (SMTLIB.Sym "step" :: _)) :: l) = (NORMAL_STEP, p, l) + | step_kind ((p as SMTLIB.S (SMTLIB.Sym "define-fun" :: _)) :: l) = (SKOLEM, p, l) + | step_kind p = raise (Fail ("step_kind unrec: " ^ @{make_string} p)) + fun parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id, _, typ, + SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name])]) cx = + (*replace the name binding by the constant instead of the full term in order to reduce + the size of the generated terms and therefore the reconstruction time*) + let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) t cx + |> apsnd (SMTLIB_Proof.update_name_binding (name, SMTLIB.Sym id)) + in + (mk_raw_node (id ^ lethe_def) lethe_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] [] + (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx) + end + | parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id, _, typ, SMTLIB.S l]) cx = + let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) (SMTLIB.S l ) cx + in + (mk_raw_node (id ^ lethe_def) lethe_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] [] + (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx) + end + | parse_skolem t _ = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) + fun get_id_cx (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l), cx) = (id, (l, cx)) + | get_id_cx t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) + fun get_id (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l)) = (id, l) + | get_id t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) + fun parse_source (SMTLIB.Key "premises" :: SMTLIB.S source ::l, cx) = + (SOME (map (fn (SMTLIB.Sym id) => id) source), (l, cx)) + | parse_source (l, cx) = (NONE, (l, cx)) + fun parse_rule (SMTLIB.Key "rule" :: SMTLIB.Sym r :: l, cx) = (r, (l, cx)) + | parse_rule t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) + fun parse_anchor_step (SMTLIB.S (SMTLIB.Sym "anchor" :: SMTLIB.Key "step" :: SMTLIB.Sym r :: l), cx) = (r, (l, cx)) + | parse_anchor_step t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) + fun parse_args (SMTLIB.Key "args" :: args :: l, cx) = + let val ((args, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings args cx + in (args, (l, cx)) end + | parse_args (l, cx) = (SMTLIB.S [], (l, cx)) + fun parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: []) :: l, cx) = + (SMTLIB.Sym "false", (l, cx)) + | parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: concl) :: l, cx) = + let val (concl, cx) = fold_map (fst oo SMTLIB_Proof.extract_and_update_name_bindings) concl cx + in (SMTLIB.S (SMTLIB.Sym "or" :: concl), (l, cx)) end + | parse_and_clausify_conclusion t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) + val parse_normal_step = + get_id_cx + ##> parse_and_clausify_conclusion + #> rotate_pair + ##> parse_rule + #> rotate_pair + ##> parse_source + #> rotate_pair + ##> parse_args + #> rotate_pair + + fun to_raw_node subproof ((((id, concl), rule), prems), args) = + mk_raw_node id rule args (the_default [] prems) [] concl subproof + fun at_discharge NONE _ = false + | at_discharge (SOME id) p = p |> get_id |> fst |> (fn id2 => id = id2) + in + case step_kind ls of + (NO_STEP, _, _) => ([],[], cx) + | (NORMAL_STEP, p, l) => + if at_discharge limit p then ([], ls, cx) else + let + (*ignores content of "discharge": Isabelle is keeping track of it via the context*) + val (s, (_, cx)) = (p, cx) + |> parse_normal_step + |>> (to_raw_node []) + val (rp, rl, cx) = parse_raw_proof_steps limit l cx + in (s :: rp, rl, cx) end + | (ASSUME, p, l) => + let + val (id, t :: []) = p + |> get_id + val ((t, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings t cx + val s = mk_raw_node id input_rule (SMTLIB.S []) [] [] t [] + val (rp, rl, cx) = parse_raw_proof_steps limit l cx + in (s :: rp, rl, cx) end + | (ANCHOR, p, l) => + let + val (anchor_id, (anchor_args, (_, cx))) = (p, cx) |> (parse_anchor_step ##> parse_args) + val (subproof, discharge_step :: remaining_proof, cx) = parse_raw_proof_steps (SOME anchor_id) l cx + val (curss, (_, cx)) = parse_normal_step (discharge_step, cx) + val s = to_raw_node subproof (fst curss, anchor_args) + val (rp, rl, cx) = parse_raw_proof_steps limit remaining_proof cx + in (s :: rp, rl, cx) end + | (SKOLEM, p, l) => + let + val (s, cx) = parse_skolem p cx + val (rp, rl, cx) = parse_raw_proof_steps limit l cx + in (s :: rp, rl, cx) end + end + +fun proof_ctxt_of_rule "bind" t = t + | proof_ctxt_of_rule "sko_forall" t = t + | proof_ctxt_of_rule "sko_ex" t = t + | proof_ctxt_of_rule "let" t = t + | proof_ctxt_of_rule "onepoint" t = t + | proof_ctxt_of_rule _ _ = [] + +fun args_of_rule "bind" t = t + | args_of_rule "la_generic" t = t + | args_of_rule _ _ = [] + +fun insts_of_forall_inst "forall_inst" t = map (fn SMTLIB.S [_, SMTLIB.Sym x, a] => (x, a)) t + | insts_of_forall_inst _ _ = [] + +fun id_of_last_step prems = + if null prems then [] + else + let val Lethe_Replay_Node {id, ...} = List.last prems in [id] end + +fun extract_assumptions_from_subproof subproof = + let fun extract_assumptions_from_subproof (Lethe_Replay_Node {rule, concl, ...}) assms = + if rule = local_input_rule then concl :: assms else assms + in + fold extract_assumptions_from_subproof subproof [] + end + +fun normalized_rule_name id rule = + (case (rule = input_rule, can SMTLIB_Interface.role_and_index_of_assert_name id) of + (true, true) => normalized_input_rule + | (true, _) => local_input_rule + | _ => rule) + +fun is_assm_repetition id rule = + rule = input_rule andalso can SMTLIB_Interface.role_and_index_of_assert_name id + +fun extract_skolem ([SMTLIB.Sym var, typ, choice]) = (var, typ, choice) + | extract_skolem t = raise Fail ("fail to parse type" ^ @{make_string} t) + +(* The preprocessing takes care of: + 1. unfolding the shared terms + 2. extract the declarations of skolems to make sure that there are not unfolded +*) +fun preprocess compress step = + let + fun expand_assms cs = + map (fn t => case AList.lookup (op =) cs t of NONE => t | SOME a => a) + fun expand_lonely_arguments (args as SMTLIB.S [SMTLIB.Sym "=", _, _]) = [args] + | expand_lonely_arguments (x as SMTLIB.S [SMTLIB.Sym var, _]) = [SMTLIB.S [SMTLIB.Sym "=", x, SMTLIB.Sym var]] + + fun preprocess (Raw_Lethe_Node {id, rule, args, prems, concl, subproof, ...}) (cx, remap_assms) = + let + val (skolem_names, stripped_args) = args + |> (fn SMTLIB.S args => args) + |> map + (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y] + | x => x) + |> (rule = "bind" orelse rule = "onepoint") ? flat o (map expand_lonely_arguments) + |> `(if rule = lethe_def then single o extract_skolem else K []) + ||> SMTLIB.S + + val (subproof, (cx, _)) = fold_map preprocess subproof (cx, remap_assms) |> apfst flat + val remap_assms = (if rule = "or" then (id, hd prems) :: remap_assms else remap_assms) + (* declare variables in the context *) + val declarations = + if rule = lethe_def + then skolem_names |> map (fn (name, _, choice) => (name, choice)) + else [] + in + if compress andalso rule = "or" + then ([], (cx, remap_assms)) + else ([Raw_Lethe_Node {id = id, rule = rule, args = stripped_args, + prems = expand_assms remap_assms prems, declarations = declarations, concl = concl, subproof = subproof}], + (cx, remap_assms)) + end + in preprocess step end + +fun filter_split _ [] = ([], []) + | filter_split f (a :: xs) = + (if f a then apfst (curry op :: a) else apsnd (curry op :: a)) (filter_split f xs) + +fun extract_types_of_args (SMTLIB.S [var, typ, t as SMTLIB.S [SMTLIB.Sym "choice", _, _]]) = + (SMTLIB.S [var, typ, t], SOME typ) + |> single + | extract_types_of_args (SMTLIB.S t) = + let + fun extract_types_of_arg (SMTLIB.S [eq, SMTLIB.S [var, typ], t]) = (SMTLIB.S [eq, var, t], SOME typ) + | extract_types_of_arg t = (t, NONE) + in + t + |> map extract_types_of_arg + end + +fun collect_skolem_defs (Raw_Lethe_Node {rule, subproof = subproof, args, ...}) = + (if is_skolemization rule then map (fn id => id ^ lethe_def) (skolems_introduced_by_rule args) else []) @ + flat (map collect_skolem_defs subproof) + +(*The postprocessing does: + 1. translate the terms to Isabelle syntax, taking care of free variables + 2. remove the ambiguity in the proof terms: + x \ y |- x = x + means y = x. To remove ambiguity, we use the fact that y is a free variable and replace the term + by: + xy \ y |- xy = x. + This is now does not have an ambiguity and we can safely move the "xy \ y" to the proof + assumptions. +*) +fun postprocess_proof compress ctxt step cx = + let + fun postprocess (Raw_Lethe_Node {id, rule, args, prems, declarations, concl, subproof}) (cx, rew) = + let + val _ = (SMT_Config.verit_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl)) + + val args = extract_types_of_args args + val globally_bound_vars = declared_csts cx rule args + val cx = fold (update_binding o (fn (s, typ) => (s, Term (Free (s, type_of cx typ))))) + globally_bound_vars cx + + (*find rebound variables specific to the LHS of the equivalence symbol*) + val bound_vars = bound_vars_by_rule cx rule args + val bound_vars_no_typ = map fst bound_vars + val rhs_vars = + fold (fn [t', t] => t <> t' ? (curry (op ::) t) | _ => fn x => x) bound_vars_no_typ [] + + fun not_already_bound cx t = SMTLIB_Proof.lookup_binding cx t = None andalso + not (member (op =) rhs_vars t) + val (shadowing_vars, rebound_lhs_vars) = bound_vars + |> filter_split (fn ([t, _], typ) => not_already_bound cx t | _ => true) + |>> map (apfst (hd)) + |>> (fn vars => vars @ flat (map (fn ([_, t], typ) => [(t, typ)] | _ => []) bound_vars)) + val subproof_rew = fold (fn [t, t'] => curry (op ::) (t, t ^ t')) + (map fst rebound_lhs_vars) rew + val subproof_rewriter = fold (fn (t, t') => synctatic_rew_in_lhs_subst t t') + subproof_rew + + val ((concl, bounds), cx') = node_of concl cx + + val extra_lhs_vars = map (fn ([a,b], typ) => (a, a^b, typ)) rebound_lhs_vars + val old_lhs_vars = map (fn (a, _, typ) => (a, typ)) extra_lhs_vars + val new_lhs_vars = map (fn (_, newvar, typ) => (newvar, typ)) extra_lhs_vars + + (* postprocess conclusion *) + val concl = SMTLIB_Isar.unskolemize_names ctxt (subproof_rewriter concl) + + val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "concl =", concl)) + val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "cx' =", cx', + "bound_vars =", bound_vars)) + + val bound_tvars = + map (fn (s, SOME typ) => (s, type_of cx typ)) + (shadowing_vars @ new_lhs_vars) + val subproof_cx = + add_bound_variables_to_ctxt cx (shadowing_vars @ new_lhs_vars) cx + + fun could_unify (Bound i, Bound j) = i = j + | could_unify (Var v, Var v') = v = v' + | could_unify (Free v, Free v') = v = v' + | could_unify (Const (v, ty), Const (v', ty')) = v = v' andalso ty = ty' + | could_unify (Abs (_, ty, bdy), Abs (_, ty', bdy')) = ty = ty' andalso could_unify (bdy, bdy') + | could_unify (u $ v, u' $ v') = could_unify (u, u') andalso could_unify (v, v') + | could_unify _ = false + fun is_alpha_renaming t = + t + |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq + |> could_unify + handle TERM _ => false + val alpha_conversion = rule = "bind" andalso is_alpha_renaming concl + + val can_remove_subproof = + compress andalso (is_skolemization rule orelse alpha_conversion) + val (fixed_subproof : lethe_replay_node list, _) = + fold_map postprocess (if can_remove_subproof then [] else subproof) + (subproof_cx, subproof_rew) + + val unsk_and_rewrite = SMTLIB_Isar.unskolemize_names ctxt o subproof_rewriter + + (* postprocess assms *) + val stripped_args = map fst args + val sanitized_args = proof_ctxt_of_rule rule stripped_args + + val arg_cx = add_bound_variables_to_ctxt cx (shadowing_vars @ old_lhs_vars) subproof_cx + val (termified_args, _) = fold_map node_of sanitized_args arg_cx |> apfst (map fst) + val normalized_args = map unsk_and_rewrite termified_args + + val subproof_assms = proof_ctxt_of_rule rule normalized_args + + (* postprocess arguments *) + val rule_args = args_of_rule rule stripped_args + val (termified_args, _) = fold_map term_of rule_args subproof_cx + val normalized_args = map unsk_and_rewrite termified_args + val rule_args = map subproof_rewriter normalized_args + + val raw_insts = insts_of_forall_inst rule stripped_args + fun termify_term (x, t) cx = let val (t, cx) = term_of t cx in ((x, t), cx) end + val (termified_args, _) = fold_map termify_term raw_insts subproof_cx + val insts = Symtab.empty + |> fold (fn (x, t) => fn insts => Symtab.update_new (x, t) insts) termified_args + |> Symtab.map (K unsk_and_rewrite) + + (* declarations *) + val (declarations, _) = fold_map termify_term declarations cx + |> apfst (map (apsnd unsk_and_rewrite)) + + (* fix step *) + val _ = if bounds <> [] then raise (Fail "found dangling variable in concl") else () + + val skolem_defs = (if is_skolemization rule + then map (fn id => id ^ lethe_def) (skolems_introduced_by_rule (SMTLIB.S (map fst args))) else []) + val skolems_of_subproof = (if is_skolemization rule + then flat (map collect_skolem_defs subproof) else []) + val fixed_prems = + prems @ (if is_assm_repetition id rule then [id] else []) @ + skolem_defs @ skolems_of_subproof @ (id_of_last_step fixed_subproof) + + (* fix subproof *) + val normalized_rule = normalized_rule_name id rule + |> (if compress andalso alpha_conversion then K "refl" else I) + + val extra_assms2 = + (if rule = subproof_rule then extract_assumptions_from_subproof fixed_subproof else []) + + val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl + [] insts declarations (bound_tvars, subproof_assms, extra_assms2, fixed_subproof) + + in + (step, (cx', rew)) + end + in + postprocess step (cx, []) + |> (fn (step, (cx, _)) => (step, cx)) + end + +fun combine_proof_steps ((step1 : lethe_replay_node) :: step2 :: steps) = + let + val (Lethe_Replay_Node {id = id1, rule = rule1, args = args1, prems = prems1, + proof_ctxt = proof_ctxt1, concl = concl1, bounds = bounds1, insts = insts1, + declarations = declarations1, + subproof = (bound_sub1, assms_sub1, assms_extra1, subproof1)}) = step1 + val (Lethe_Replay_Node {id = id2, rule = rule2, args = args2, prems = prems2, + proof_ctxt = proof_ctxt2, concl = concl2, bounds = bounds2, insts = insts2, + declarations = declarations2, + subproof = (bound_sub2, assms_sub2, assms_extra2, subproof2)}) = step2 + val goals1 = + (case concl1 of + _ $ (Const (\<^const_name>\HOL.disj\, _) $ _ $ + (Const (\<^const_name>\HOL.disj\, _) $ (Const (\<^const_name>\HOL.Not\, _) $a) $ b)) => [a,b] + | _ => []) + val goal2 = (case concl2 of _ $ a => a) + in + if rule1 = equiv_pos2_rule andalso rule2 = th_resolution_rule andalso member (op =) prems2 id1 + andalso member (op =) goals1 goal2 + then + mk_replay_node id2 theory_resolution2_rule args2 (filter_out (curry (op =) id1) prems2) + proof_ctxt2 concl2 bounds2 insts2 declarations2 + (bound_sub2, assms_sub2, assms_extra2, combine_proof_steps subproof2) :: + combine_proof_steps steps + else + mk_replay_node id1 rule1 args1 prems1 + proof_ctxt1 concl1 bounds1 insts1 declarations1 + (bound_sub1, assms_sub1, assms_extra1, combine_proof_steps subproof1) :: + combine_proof_steps (step2 :: steps) + end + | combine_proof_steps steps = steps + + +val linearize_proof = + let + fun map_node_concl f (Lethe_Node {id, rule, prems, proof_ctxt, concl}) = + mk_node id rule prems proof_ctxt (f concl) + fun linearize (Lethe_Replay_Node {id = id, rule = rule, args = _, prems = prems, + proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = _, declarations = _, + subproof = (bounds', assms, inputs, subproof)}) = + let + val bounds = distinct (op =) bounds + val bounds' = distinct (op =) bounds' + fun mk_prop_of_term concl = + concl |> fastype_of concl = \<^typ>\bool\ ? curry (op $) \<^term>\Trueprop\ + fun remove_assumption_id assumption_id prems = + filter_out (curry (op =) assumption_id) prems + fun add_assumption assumption concl = + \<^Const>\Pure.imp for \mk_prop_of_term assumption\ \mk_prop_of_term concl\\ + fun inline_assumption assumption assumption_id + (Lethe_Node {id, rule, prems, proof_ctxt, concl}) = + mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt + (add_assumption assumption concl) + fun find_input_steps_and_inline [] = [] + | find_input_steps_and_inline + (Lethe_Node {id = id', rule, prems, concl, ...} :: steps) = + if rule = input_rule then + find_input_steps_and_inline (map (inline_assumption concl id') steps) + else + mk_node (id') rule prems [] concl :: find_input_steps_and_inline steps + + fun free_bounds bounds (concl) = + fold (fn (var, typ) => fn t => Logic.all (Free (var, typ)) t) bounds concl + val subproof = subproof + |> flat o map linearize + |> map (map_node_concl (fold add_assumption (assms @ inputs))) + |> map (map_node_concl (free_bounds (bounds @ bounds'))) + |> find_input_steps_and_inline + val concl = free_bounds bounds concl + in + subproof @ [mk_node id rule prems proof_ctxt concl] + end + in linearize end + +fun rule_of (Lethe_Replay_Node {rule,...}) = rule +fun subproof_of (Lethe_Replay_Node {subproof = (_, _, _, subproof),...}) = subproof + + +(* Massage Skolems for Sledgehammer. + +We have to make sure that there is an "arrow" in the graph for skolemization steps. + + +A. The normal easy case + +This function detects the steps of the form + P \ Q :skolemization + Q :resolution with P +and replace them by + Q :skolemization +Throwing away the step "P \ Q" completely. This throws away a lot of information, but it does not +matter too much for Sledgehammer. + + +B. Skolems in subproofs +Supporting this is more or less hopeless as long as the Isar reconstruction of Sledgehammer +does not support more features like definitions. lethe is able to generate proofs with skolemization +happening in subproofs inside the formula. + (assume "A \ P" + ... + P \ Q :skolemization in the subproof + ...) + hence A \ P \ A \ Q :lemma + ... + R :something with some rule +and replace them by + R :skolemization with some rule +Without any subproof +*) +fun remove_skolem_definitions_proof steps = + let + fun replace_equivalent_by_imp (judgement $ ((Const(\<^const_name>\HOL.eq\, typ) $ arg1) $ arg2)) = + judgement $ ((Const(\<^const_name>\HOL.implies\, typ) $ arg1) $ arg2) + | replace_equivalent_by_imp a = a (*This case is probably wrong*) + fun remove_skolem_definitions (Lethe_Replay_Node {id = id, rule = rule, args = args, + prems = prems, + proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = insts, + declarations = declarations, + subproof = (vars, assms', extra_assms', subproof)}) (prems_to_remove, skolems) = + let + val prems = prems + |> filter_out (member (op =) prems_to_remove) + val trivial_step = is_SH_trivial rule + fun has_skolem_substep st NONE = if is_skolemization (rule_of st) then SOME (rule_of st) + else fold has_skolem_substep (subproof_of st) NONE + | has_skolem_substep _ a = a + val promote_to_skolem = exists (fn t => member (op =) skolems t) prems + val promote_from_assms = fold has_skolem_substep subproof NONE <> NONE + val promote_step = promote_to_skolem orelse promote_from_assms + val skolem_step_to_skip = is_skolemization rule orelse + (promote_from_assms andalso length prems > 1) + val is_skolem = is_skolemization rule orelse promote_step + val prems = prems + |> filter_out (fn t => member (op =) skolems t) + |> is_skolem ? filter_out (String.isPrefix id) + val rule = (if promote_step then default_skolem_rule else rule) + val subproof = subproof + |> (is_skolem ? K []) (*subproofs of skolemization steps are useless for SH*) + |> map (fst o (fn st => remove_skolem_definitions st (prems_to_remove, skolems))) + (*no new definitions in subproofs*) + |> flat + val concl = concl + |> is_skolem ? replace_equivalent_by_imp + val step = (if skolem_step_to_skip orelse rule = lethe_def orelse trivial_step then [] + else mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations + (vars, assms', extra_assms', subproof) + |> single) + val defs = (if rule = lethe_def orelse trivial_step then id :: prems_to_remove + else prems_to_remove) + val skolems = (if skolem_step_to_skip then id :: skolems else skolems) + in + (step, (defs, skolems)) + end + in + fold_map remove_skolem_definitions steps ([], []) + |> fst + |> flat + end + +local + (*TODO useful?*) + fun remove_pattern (SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.S _])) = t + | remove_pattern (SMTLIB.S xs) = SMTLIB.S (map remove_pattern xs) + | remove_pattern p = p + + fun import_proof_and_post_process typs funs lines ctxt = + let + val compress = SMT_Config.compress_verit_proofs ctxt + val smtlib_lines_without_qm = + lines + |> map single + |> map SMTLIB.parse + |> map remove_all_qm2 + |> map remove_pattern + val (raw_steps, _, _) = + parse_raw_proof_steps NONE smtlib_lines_without_qm SMTLIB_Proof.empty_name_binding + + fun process step (cx, cx') = + let fun postprocess step (cx, cx') = + let val (step, cx) = postprocess_proof compress ctxt step cx + in (step, (cx, cx')) end + in uncurry (fold_map postprocess) (preprocess compress step (cx, cx')) end + val step = + (empty_context ctxt typs funs, []) + |> fold_map process raw_steps + |> (fn (steps, (cx, _)) => (flat steps, cx)) + |> compress? apfst combine_proof_steps + in step end +in + +fun parse typs funs lines ctxt = + let + val (u, env) = import_proof_and_post_process typs funs lines ctxt + val t = u + |> remove_skolem_definitions_proof + |> flat o (map linearize_proof) + fun node_to_step (Lethe_Node {id, rule, prems, concl, ...}) = + mk_step id rule prems [] concl [] + in + (map node_to_step t, ctxt_of env) + end + +fun parse_replay typs funs lines ctxt = + let + val (u, env) = import_proof_and_post_process typs funs lines ctxt + val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> u) + in + (u, ctxt_of env) + end +end + +end; diff --git a/src/HOL/Tools/SMT/lethe_proof_parse.ML b/src/HOL/Tools/SMT/lethe_proof_parse.ML new file mode 100644 --- /dev/null +++ b/src/HOL/Tools/SMT/lethe_proof_parse.ML @@ -0,0 +1,76 @@ +(* Title: HOL/Tools/SMT/verit_proof_parse.ML + Author: Mathias Fleury, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +VeriT proof parsing. +*) + +signature LETHE_PROOF_PARSE = +sig + type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step + val parse_proof: SMT_Translate.replay_data -> + ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> + SMT_Solver.parsed_proof +end; + +structure Lethe_Proof_Parse: LETHE_PROOF_PARSE = +struct + +open ATP_Util +open ATP_Problem +open ATP_Proof +open ATP_Proof_Reconstruct +open Lethe_Isar +open Lethe_Proof + +fun parse_proof + ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) + xfacts prems concl output = + let + val num_ll_defs = length ll_defs + + val id_of_index = Integer.add num_ll_defs + val index_of_id = Integer.add (~ num_ll_defs) + + fun step_of_assume j (_, th) = + Lethe_Proof.Lethe_Step {id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j), + rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []} + + val (actual_steps, _) = Lethe_Proof.parse typs terms output ctxt + val used_assert_ids = + map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) output + val used_assm_js = + map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end) + used_assert_ids + val used_assms = map (nth assms) used_assm_js + val assm_steps = map2 step_of_assume used_assm_js used_assms + val steps = assm_steps @ actual_steps + + val conjecture_i = 0 + val prems_i = conjecture_i + 1 + val num_prems = length prems + val facts_i = prems_i + num_prems + val num_facts = length xfacts + val helpers_i = facts_i + num_facts + + val conjecture_id = id_of_index conjecture_i + val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1) + val fact_ids' = + map_filter (fn j => + let val (i, _) = nth assms j in + try (apsnd (nth xfacts)) (id_of_index j, i - facts_i) + end) used_assm_js + val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms + + val fact_helper_ts = + map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @ + map (fn (_, ((s, _), th)) => (s, Thm.prop_of th)) fact_ids' + val fact_helper_ids' = + map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids' + in + {outcome = NONE, fact_ids = SOME fact_ids', + atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl + fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps} + end + +end; diff --git a/src/HOL/Tools/SMT/lethe_replay_methods.ML b/src/HOL/Tools/SMT/lethe_replay_methods.ML new file mode 100644 --- /dev/null +++ b/src/HOL/Tools/SMT/lethe_replay_methods.ML @@ -0,0 +1,1191 @@ +(* Title: HOL/Tools/SMT/verit_replay_methods.ML + Author: Mathias Fleury, MPII, JKU, University Freiburg + +Proof method for replaying veriT proofs. +*) + +signature LETHE_REPLAY_METHODS = +sig + + + datatype verit_rule = + False | True | + + (*input: a repeated (normalized) assumption of assumption of in a subproof*) + Normalized_Input | Local_Input | + (*Subproof:*) + Subproof | + (*Conjunction:*) + And | Not_And | And_Pos | And_Neg | + (*Disjunction""*) + Or | Or_Pos | Not_Or | Or_Neg | + (*Disjunction:*) + Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 | + (*Equivalence:*) + Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 | + (*If-then-else:*) + ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 | + (*Equality:*) + Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans | Refl | Cong | + (*Arithmetics:*) + LA_Disequality | LA_Generic | LA_Tautology | LIA_Generic | LA_Totality | LA_RW_Eq | + NLA_Generic | + (*Quantifiers:*) + Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Onepoint | Bind | Skolem_Forall | Skolem_Ex | + (*Resolution:*) + Theory_Resolution | Resolution | + (*Temporary rules, that the verit developers want to remove:*) + AC_Simp | + Bfun_Elim | + Qnt_CNF | + (*Used to introduce skolem constants*) + Definition | + (*Former cong rules*) + Bool_Simplify | Or_Simplify | Not_Simplify | And_Simplify | Equiv_Simplify | + Implies_Simplify | Connective_Def | Minus_Simplify | Comp_Simplify | + Eq_Simplify | ITE_Simplify | Sum_Simplify | Prod_Simplify | All_Simplify | + Qnt_Simplify | Not_Not | Tautological_Clause | Duplicate_Literals | + (*Unsupported rule*) + Unsupported | + (*For compression*) + Theory_Resolution2 | + (*Extended rules*) + Symm | Not_Symm | Reordering | Tmp_Quantifier_Simplify + + val requires_subproof_assms : string list -> string -> bool + val requires_local_input: string list -> string -> bool + + val string_of_verit_rule: verit_rule -> string + + type lethe_tac_args = Proof.context -> thm list -> term list -> term -> thm + type lethe_tac = Proof.context -> thm list -> term -> thm + type lethe_tac2 = Proof.context -> thm list -> term list -> term Symtab.table -> term -> thm + val bind: lethe_tac_args + val and_rule: lethe_tac + val and_neg_rule: lethe_tac + val and_pos: lethe_tac + val rewrite_and_simplify: lethe_tac + val rewrite_bool_simplify: lethe_tac + val rewrite_comp_simplify: lethe_tac + val rewrite_minus_simplify: lethe_tac + val rewrite_not_simplify: lethe_tac + val rewrite_eq_simplify: lethe_tac + val rewrite_equiv_simplify: lethe_tac + val rewrite_implies_simplify: lethe_tac + val rewrite_or_simplify: lethe_tac + val cong: lethe_tac + val rewrite_connective_def: lethe_tac + val duplicate_literals: lethe_tac + val eq_congruent: lethe_tac + val eq_congruent_pred: lethe_tac + val eq_reflexive: lethe_tac + val eq_transitive: lethe_tac + val equiv1: lethe_tac + val equiv2: lethe_tac + val equiv_neg1: lethe_tac + val equiv_neg2: lethe_tac + val equiv_pos1: lethe_tac + val equiv_pos2: lethe_tac + val false_rule: lethe_tac + val forall_inst: lethe_tac2 + val implies_rules: lethe_tac + val implies_neg1: lethe_tac + val implies_neg2: lethe_tac + val implies_pos: lethe_tac + val ite1: lethe_tac + val ite2: lethe_tac + val ite_intro: lethe_tac + val ite_neg1: lethe_tac + val ite_neg2: lethe_tac + val ite_pos1: lethe_tac + val ite_pos2: lethe_tac + val rewrite_ite_simplify: lethe_tac + val la_disequality: lethe_tac + val la_generic: lethe_tac_args + val la_rw_eq: lethe_tac + val lia_generic: lethe_tac + val refl: lethe_tac + val normalized_input: lethe_tac + val not_and_rule: lethe_tac + val not_equiv1: lethe_tac + val not_equiv2: lethe_tac + val not_implies1: lethe_tac + val not_implies2: lethe_tac + val not_ite1: lethe_tac + val not_ite2: lethe_tac + val not_not: lethe_tac + val not_or_rule: lethe_tac + val or: lethe_tac + val or_neg_rule: lethe_tac + val or_pos_rule: lethe_tac + val theory_resolution2: lethe_tac + val prod_simplify: lethe_tac + val qnt_join: lethe_tac + val qnt_rm_unused: lethe_tac + val onepoint: lethe_tac + val qnt_simplify: lethe_tac + val all_simplify: lethe_tac + val unit_res: lethe_tac + val skolem_ex: lethe_tac + val skolem_forall: lethe_tac + val subproof: lethe_tac + val sum_simplify: lethe_tac + val tautological_clause: lethe_tac + val tmp_AC_rule: lethe_tac + val bfun_elim: lethe_tac + val qnt_cnf: lethe_tac + val trans: lethe_tac + val symm: lethe_tac + val not_symm: lethe_tac + val reordering: lethe_tac + +(* + val : lethe_tac +*) + val REPEAT_CHANGED: ('a -> tactic) -> 'a -> tactic + val TRY': ('a -> tactic) -> 'a -> tactic + +end; + + +structure Lethe_Replay_Methods: LETHE_REPLAY_METHODS = +struct + +type lethe_tac_args = Proof.context -> thm list -> term list -> term -> thm +type lethe_tac = Proof.context -> thm list -> term -> thm +type lethe_tac2 = Proof.context -> thm list -> term list -> term Symtab.table -> term -> thm + +(*Some general comments on the proof format: + 1. Double negations are not always removed. This means for example that the equivalence rules + cannot assume that the double negations have already been removed. Therefore, we match the + term, instantiate the theorem, then use simp (to remove double negations), and finally use + assumption. + 2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule + is doing much more that is supposed to do. Moreover types can make trivial goals (for the + boolean structure) impossible to prove. + 3. Duplicate literals are sometimes removed, mostly by the SAT solver. + + Rules unsupported on purpose: + * Distinct_Elim, XOR, let (we don't need them). + * deep_skolemize (because it is not clear if verit still generates using it). +*) + + +datatype verit_rule = + False | True | + + (*input: a repeated (normalized) assumption of assumption of in a subproof*) + Normalized_Input | Local_Input | + (*Subproof:*) + Subproof | + (*Conjunction:*) + And | Not_And | And_Pos | And_Neg | + (*Disjunction""*) + Or | Or_Pos | Not_Or | Or_Neg | + (*Disjunction:*) + Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 | + (*Equivalence:*) + Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 | + (*If-then-else:*) + ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 | + (*Equality:*) + Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans | Refl | Cong | + (*Arithmetics:*) + LA_Disequality | LA_Generic | LA_Tautology | LIA_Generic | LA_Totality | LA_RW_Eq | + NLA_Generic | + (*Quantifiers:*) + Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Onepoint | Bind | Skolem_Forall | Skolem_Ex | + (*Resolution:*) + Theory_Resolution | Resolution | + (*Temporary rules, that the verit developpers want to remove:*) + AC_Simp | + Bfun_Elim | + Qnt_CNF | + (*Used to introduce skolem constants*) + Definition | + (*Former cong rules*) + Bool_Simplify | Or_Simplify | Not_Simplify | And_Simplify | Equiv_Simplify | + Implies_Simplify | Connective_Def | Minus_Simplify | Comp_Simplify | + Eq_Simplify | ITE_Simplify | Sum_Simplify | Prod_Simplify | All_Simplify | + Qnt_Simplify | Not_Not | Tautological_Clause | Duplicate_Literals | + (*Unsupported rule*) + Unsupported | + (*For compression*) + Theory_Resolution2 | + (*Extended rules*) + Symm | Not_Symm | Reordering | Tmp_Quantifier_Simplify + +fun string_of_verit_rule Bind = "Bind" + | string_of_verit_rule Cong = "Cong" + | string_of_verit_rule Refl = "Refl" + | string_of_verit_rule Equiv1 = "Equiv1" + | string_of_verit_rule Equiv2 = "Equiv2" + | string_of_verit_rule Equiv_pos1 = "Equiv_pos1" + | string_of_verit_rule Equiv_pos2 = "Equiv_pos2" + | string_of_verit_rule Equiv_neg1 = "Equiv_neg1" + | string_of_verit_rule Equiv_neg2 = "Equiv_neg2" + | string_of_verit_rule Skolem_Forall = "Skolem_Forall" + | string_of_verit_rule Skolem_Ex = "Skolem_Ex" + | string_of_verit_rule Eq_Reflexive = "Eq_Reflexive" + | string_of_verit_rule Theory_Resolution = "Theory_Resolution" + | string_of_verit_rule Theory_Resolution2 = "Theory_Resolution2" + | string_of_verit_rule Forall_Inst = "forall_inst" + | string_of_verit_rule Or = "Or" + | string_of_verit_rule Not_Or = "Not_Or" + | string_of_verit_rule Resolution = "Resolution" + | string_of_verit_rule Eq_Congruent = "eq_congruent" + | string_of_verit_rule Trans = "trans" + | string_of_verit_rule False = "false" + | string_of_verit_rule And = "and" + | string_of_verit_rule And_Pos = "and_pos" + | string_of_verit_rule Not_And = "not_and" + | string_of_verit_rule And_Neg = "and_neg" + | string_of_verit_rule Or_Pos = "or_pos" + | string_of_verit_rule Or_Neg = "or_neg" + | string_of_verit_rule AC_Simp = "ac_simp" + | string_of_verit_rule Not_Equiv1 = "not_equiv1" + | string_of_verit_rule Not_Equiv2 = "not_equiv2" + | string_of_verit_rule Not_Implies1 = "not_implies1" + | string_of_verit_rule Not_Implies2 = "not_implies2" + | string_of_verit_rule Implies_Neg1 = "implies_neg1" + | string_of_verit_rule Implies_Neg2 = "implies_neg2" + | string_of_verit_rule Implies = "implies" + | string_of_verit_rule Bfun_Elim = "bfun_elim" + | string_of_verit_rule ITE1 = "ite1" + | string_of_verit_rule ITE2 = "ite2" + | string_of_verit_rule Not_ITE1 = "not_ite1" + | string_of_verit_rule Not_ITE2 = "not_ite2" + | string_of_verit_rule ITE_Pos1 = "ite_pos1" + | string_of_verit_rule ITE_Pos2 = "ite_pos2" + | string_of_verit_rule ITE_Neg1 = "ite_neg1" + | string_of_verit_rule ITE_Neg2 = "ite_neg2" + | string_of_verit_rule ITE_Intro = "ite_intro" + | string_of_verit_rule LA_Disequality = "la_disequality" + | string_of_verit_rule LA_Generic = "la_generic" + | string_of_verit_rule LIA_Generic = "lia_generic" + | string_of_verit_rule LA_Tautology = "la_tautology" + | string_of_verit_rule LA_RW_Eq = "la_rw_eq" + | string_of_verit_rule LA_Totality = "LA_Totality" + | string_of_verit_rule NLA_Generic = "nla_generic" + | string_of_verit_rule Eq_Transitive = "eq_transitive" + | string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused" + | string_of_verit_rule Onepoint = "onepoint" + | string_of_verit_rule Qnt_Join = "qnt_join" + | string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred" + | string_of_verit_rule Normalized_Input = Lethe_Proof.normalized_input_rule + | string_of_verit_rule Local_Input = Lethe_Proof.local_input_rule + | string_of_verit_rule Subproof = "subproof" + | string_of_verit_rule Bool_Simplify = "bool_simplify" + | string_of_verit_rule Equiv_Simplify = "equiv_simplify" + | string_of_verit_rule Eq_Simplify = "eq_simplify" + | string_of_verit_rule Not_Simplify = "not_simplify" + | string_of_verit_rule And_Simplify = "and_simplify" + | string_of_verit_rule Or_Simplify = "or_simplify" + | string_of_verit_rule ITE_Simplify = "ite_simplify" + | string_of_verit_rule Implies_Simplify = "implies_simplify" + | string_of_verit_rule Connective_Def = "connective_def" + | string_of_verit_rule Minus_Simplify = "minus_simplify" + | string_of_verit_rule Sum_Simplify = "sum_simplify" + | string_of_verit_rule Prod_Simplify = "prod_simplify" + | string_of_verit_rule All_Simplify = "all_simplify" + | string_of_verit_rule Comp_Simplify = "comp_simplify" + | string_of_verit_rule Qnt_Simplify = "qnt_simplify" + | string_of_verit_rule Symm = "symm" + | string_of_verit_rule Not_Symm = "not_symm" + | string_of_verit_rule Reordering = "reordering" + | string_of_verit_rule Not_Not = Lethe_Proof.not_not_rule + | string_of_verit_rule Tautological_Clause = "tautology" + | string_of_verit_rule Duplicate_Literals = Lethe_Proof.contract_rule + | string_of_verit_rule Qnt_CNF = "qnt_cnf" + | string_of_verit_rule r = "Unknown rule: " ^ \<^make_string> r + +fun replay_error ctxt msg rule thms t = + SMT_Replay_Methods.replay_error ctxt msg (string_of_verit_rule rule) thms t + +(* utility function *) + +fun eqsubst_all ctxt thms = + K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_asm_tac ctxt [0] thms)) + THEN' K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_tac ctxt [0] thms)) + +fun simplify_tac ctxt thms = + ctxt + |> empty_simpset + |> put_simpset HOL_basic_ss + |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms) + |> Simplifier.asm_full_simp_tac + +(* sko_forall requires the assumptions to be able to prove the equivalence in case of double +skolemization. See comment below. *) +fun requires_subproof_assms _ t = + member (op =) ["refl", "sko_forall", "sko_ex", "cong"] t + +fun requires_local_input _ t = + member (op =) [Lethe_Proof.local_input_rule] t + +(*This is a weaker simplification form. It is weaker, but is also less likely to loop*) +fun partial_simplify_tac ctxt thms = + ctxt + |> empty_simpset + |> put_simpset HOL_basic_ss + |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms) + |> Simplifier.full_simp_tac + +val try_provers = SMT_Replay_Methods.try_provers "verit" + +fun TRY' tac = fn i => TRY (tac i) +fun REPEAT' tac = fn i => REPEAT (tac i) +fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i)) + + +(* Bind *) + +(*The bind rule is non-obvious due to the handling of quantifiers: + "\x y a. x = y ==> (\b. P a b x) \ (\b. P' a b y)" + ------------------------------------------------------ + \a. (\b x. P a b x) \ (\b y. P' a b y) +is a valid application.*) + +val bind_thms = + [@{lemma \(\x x'. x = x' \ P x = Q x') \ (\x. P x) = (\y. Q y)\ by blast}, + @{lemma \(\x x'. x = x' \ P x = Q x') \ (\x. P x) = (\y. Q y)\ by blast}, + @{lemma \(\x x'. x = x' \ P x = Q x') \ (\x. P x = Q x)\ by blast}, + @{lemma \(\x x'. x = x' \ P x = Q x') \ (\x. P x = Q x)\ by blast}] + +val bind_thms_same_name = + [@{lemma \(\x. P x = Q x) \ (\x. P x) = (\y. Q y)\ by blast}, + @{lemma \(\x. P x = Q x) \ (\x. P x) = (\y. Q y)\ by blast}, + @{lemma \(\x. P x = Q x) \ (\x. P x = Q x)\ by blast}, + @{lemma \(\x. P x = Q x) \ (\x. P x = Q x)\ by blast}] + +fun extract_quantified_names_q (_ $ Abs (name, _, t)) = + apfst (curry (op ::) name) (extract_quantified_names_q t) + | extract_quantified_names_q t = ([], t) + +fun extract_forall_quantified_names_q (Const(\<^const_name>\HOL.All\, _) $ Abs (name, ty, t)) = + (name, ty) :: (extract_forall_quantified_names_q t) + | extract_forall_quantified_names_q _ = [] + +fun extract_all_forall_quantified_names_q (Const(\<^const_name>\HOL.All\, _) $ Abs (name, _, t)) = + name :: (extract_all_forall_quantified_names_q t) + | extract_all_forall_quantified_names_q (t $ u) = + extract_all_forall_quantified_names_q t @ extract_all_forall_quantified_names_q u + | extract_all_forall_quantified_names_q _ = [] + +val extract_quantified_names_ba = + SMT_Replay_Methods.dest_prop + #> extract_quantified_names_q + ##> HOLogic.dest_eq + ##> fst + ##> extract_quantified_names_q + ##> fst + +val extract_quantified_names = + extract_quantified_names_ba + #> (op @) + +val extract_all_forall_quantified_names = + SMT_Replay_Methods.dest_prop + #> HOLogic.dest_eq + #> fst + #> extract_all_forall_quantified_names_q + + +fun extract_all_exists_quantified_names_q (Const(\<^const_name>\HOL.Ex\, _) $ Abs (name, _, t)) = + name :: (extract_all_exists_quantified_names_q t) + | extract_all_exists_quantified_names_q (t $ u) = + extract_all_exists_quantified_names_q t @ extract_all_exists_quantified_names_q u + | extract_all_exists_quantified_names_q _ = [] + +val extract_all_exists_quantified_names = + SMT_Replay_Methods.dest_prop + #> HOLogic.dest_eq + #> fst + #> extract_all_exists_quantified_names_q + + +val extract_bind_names = + HOLogic.dest_eq + #> apply2 (fn (Free (name, _)) => name) + +fun combine_quant ctxt ((n1, n2) :: bounds) (n1' :: formula) = + TRY' (if n1 = n1' + then if n1 <> n2 + then + resolve_tac ctxt bind_thms + THEN' TRY'(resolve_tac ctxt [@{thm refl}]) + THEN' combine_quant ctxt bounds formula + else resolve_tac ctxt bind_thms_same_name THEN' combine_quant ctxt bounds formula + else resolve_tac ctxt @{thms allI} THEN' combine_quant ctxt ((n1, n2) :: bounds) formula) + | combine_quant _ _ _ = K all_tac + +fun bind_quants ctxt args t = + combine_quant ctxt (map extract_bind_names args) (extract_quantified_names t) + +fun generalize_prems_q [] prems = prems + | generalize_prems_q (_ :: quants) prems = + generalize_prems_q quants (@{thm spec} OF [prems]) + +fun generalize_prems t = generalize_prems_q (fst (extract_quantified_names_ba t)) + +fun bind ctxt [prems] args t = + SMT_Replay_Methods.prove ctxt t (fn _ => + bind_quants ctxt args t + THEN' TRY' (SOLVED' (resolve_tac ctxt [generalize_prems t prems] + THEN_ALL_NEW TRY' (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms refl})))) + | bind ctxt thms _ t = replay_error ctxt "invalid bind application" Bind thms t + + +(* Congruence/Refl *) + +fun cong ctxt thms = try_provers ctxt + (string_of_verit_rule Cong) [ + ("basic", SMT_Replay_Methods.cong_basic ctxt thms), + ("unfolding then reflexivity", SMT_Replay_Methods.cong_unfolding_trivial ctxt thms), + ("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms), + ("full", SMT_Replay_Methods.cong_full ctxt thms)] thms + +fun refl ctxt thm t = + (case find_first (fn thm => t = Thm.full_prop_of thm) thm of + SOME thm => thm + | NONE => + (case try (fn t => SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}) t of + NONE => cong ctxt thm t + | SOME thm => thm)) + +(* Instantiation *) + +local +fun dropWhile _ [] = [] + | dropWhile f (x :: xs) = if f x then dropWhile f xs else x :: xs +in + +fun forall_inst ctxt _ _ insts t = + let + fun instantiate_and_solve i ({context = ctxt, prems = [prem], ...}: Subgoal.focus) = + let + val t = Thm.prop_of prem + val quants = t + |> SMT_Replay_Methods.dest_prop + |> extract_forall_quantified_names_q + val insts = map (Symtab.lookup insts o fst) (rev quants) + |> dropWhile (curry (op =) NONE) + |> rev + fun option_map _ NONE = NONE + | option_map f (SOME a) = SOME (f a) + fun instantiate_with inst prem = + Drule.infer_instantiate' ctxt [NONE, inst] @{thm spec} OF [prem] + val inst_thm = + fold instantiate_with + (map (option_map (Thm.cterm_of ctxt)) insts) + prem + in + (Method.insert_tac ctxt [inst_thm] + THEN' TRY' (fn i => assume_tac ctxt i) + THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute})) i + end + | instantiate_and_solve _ ({context = ctxt, prems = thms, ...}: Subgoal.focus) = + replay_error ctxt "invalid application" Forall_Inst thms t + in + SMT_Replay_Methods.prove ctxt t (fn _ => + match_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]] + THEN' (fn i => Subgoal.FOCUS (instantiate_and_solve i) ctxt i)) + end +end + + +(* Or *) + +fun or _ (thm :: _) _ = thm + | or ctxt thms t = replay_error ctxt "invalid bind application" Or thms t + + +(* Implication *) + +val implies_pos_thm = + [@{lemma \\(A \ B) \ \A \ B\ by blast}, + @{lemma \\(\A \ B) \ A \ B\ by blast}] + +fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt implies_pos_thm) + +(* Skolemization *) + +fun extract_rewrite_rule_assumption _ thms = + let + fun is_rewrite_rule thm = + (case Thm.prop_of thm of + \<^term>\Trueprop\ $ (Const(\<^const_name>\HOL.eq\, _) $ _ $ Free(_, _)) => true + | _ => false) + fun is_context_rule thm = + (case Thm.prop_of thm of + \<^term>\Trueprop\ $ (Const(\<^const_name>\HOL.eq\, _) $ Free(_, _) $ Free(_, _)) => true + | _ => false) + val ctxt_eq = + thms + |> filter is_context_rule + val rew = + thms + |> filter_out is_context_rule + |> filter is_rewrite_rule + in + (ctxt_eq, rew) + end + +local + fun rewrite_all_skolems thm_indirect ctxt (SOME thm :: thms) = + EqSubst.eqsubst_tac ctxt [0] [thm_indirect OF [thm]] + THEN' (partial_simplify_tac ctxt (@{thms eq_commute})) + THEN' rewrite_all_skolems thm_indirect ctxt thms + | rewrite_all_skolems thm_indirect ctxt (NONE :: thms) = rewrite_all_skolems thm_indirect ctxt thms + | rewrite_all_skolems _ _ [] = K (all_tac) + + fun extract_var_name (thm :: thms) = + let val name = Thm.concl_of thm + |> SMT_Replay_Methods.dest_prop + |> HOLogic.dest_eq + |> fst + |> (fn Const(_,_) $ Abs(name, _, _) => [(name,@{thm sym} OF [thm])] + | _ => []) + in name :: extract_var_name thms end + | extract_var_name [] = [] + +fun skolem_tac extractor thm1 thm2 ctxt thms t = + let + val (ctxt_eq, ts) = extract_rewrite_rule_assumption ctxt thms + fun ordered_definitions () = + let + val var_order = extractor t + val thm_names_with_var = extract_var_name ts |> flat + in map (AList.lookup (op =) thm_names_with_var) var_order end + + in + SMT_Replay_Methods.prove ctxt t (fn _ => + K (unfold_tac ctxt ctxt_eq) + THEN' ((SOLVED' (K (unfold_tac ctxt (map (fn thm => thm1 OF [@{thm sym} OF [thm]]) ts)))) + ORELSE' + (rewrite_all_skolems thm2 ctxt (ordered_definitions ()) + THEN' partial_simplify_tac ctxt @{thms eq_commute}))) + end +in + +val skolem_forall = + skolem_tac extract_all_forall_quantified_names @{thm verit_sko_forall_indirect} + @{thm verit_sko_forall_indirect2} + +val skolem_ex = + skolem_tac extract_all_exists_quantified_names @{thm verit_sko_ex_indirect} + @{thm verit_sko_ex_indirect2} + +end + +fun eq_reflexive ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm refl} + +local + fun not_not_prove ctxt _ = + K (unfold_tac ctxt @{thms not_not}) + THEN' match_tac ctxt @{thms verit_or_simplify_1} + + fun duplicate_literals_prove ctxt prems = + Method.insert_tac ctxt prems + THEN' match_tac ctxt @{thms ccontr} + THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not}) + THEN' TRY o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE}) + THEN' CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms disjE}) + THEN' REPEAT' (ematch_tac ctxt @{thms notE} THEN' TRY' (assume_tac ctxt)) + + fun tautological_clause_prove ctxt _ = + match_tac ctxt @{thms verit_or_neg} + THEN' K (unfold_tac ctxt @{thms not_not disj_assoc[symmetric]}) + THEN' TRY' (match_tac ctxt @{thms notE} THEN_ALL_NEW assume_tac ctxt) + + val theory_resolution2_lemma = @{lemma \a \ a = b \ b\ by blast} + +in + +fun prove_abstract abstracter tac ctxt thms t = + let + val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms + val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t)) + val (_, t2) = Logic.dest_equals (Thm.prop_of t') + val thm = + SMT_Replay_Methods.prove_abstract ctxt thms t2 tac ( + fold_map (abstracter o SMT_Replay_Methods.dest_thm) thms ##>> + abstracter (SMT_Replay_Methods.dest_prop t2)) + in + @{thm verit_Pure_trans} OF [t', thm] + end + +val not_not = prove_abstract SMT_Replay_Methods.abstract_bool_shallow not_not_prove + +val tautological_clause = + prove_abstract SMT_Replay_Methods.abstract_bool_shallow tautological_clause_prove + +val duplicate_literals = + prove_abstract SMT_Replay_Methods.abstract_bool_shallow duplicate_literals_prove + +val unit_res = prove_abstract SMT_Replay_Methods.abstract_bool_shallow SMT_Replay_Methods.prop_tac + +(*match_instantiate does not work*) +fun theory_resolution2 ctxt prems t = + SMT_Replay_Methods.prove ctxt t (fn _ => match_tac ctxt [theory_resolution2_lemma OF prems]) + +end + + +fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt prems + THEN' TRY' (K (unfold_tac ctxt @{thms SMT.trigger_def})) + THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute})) + +val false_rule_thm = @{lemma \\False\ by blast} + +fun false_rule ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t false_rule_thm + + +(* Transitivity *) + +val trans_bool_thm = + @{lemma \P = Q \ Q \ P\ by blast} + +fun trans ctxt thms t = + let + val prop_of = HOLogic.dest_Trueprop o Thm.full_prop_of + fun combine_thms [thm1, thm2] = + (case (prop_of thm1, prop_of thm2) of + ((Const(\<^const_name>\HOL.eq\, _) $ t1 $ t2), + (Const(\<^const_name>\HOL.eq\, _) $ t3 $ t4)) => + if t2 aconv t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans})) + else if t2 aconv t4 then thm1 RSN ((1, ((thm2 RS sym)) RSN (2, @{thm trans}))) + else if t1 aconv t4 then thm2 RSN (1, thm1 RSN (2, @{thm trans})) + else raise Fail "invalid trans theorem" + | _ => trans_bool_thm OF [thm1, thm2]) + | combine_thms (thm1 :: thm2 :: thms) = + combine_thms (combine_thms [thm1, thm2] :: thms) + | combine_thms thms = replay_error ctxt "invalid bind application" Trans thms t + val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t)) + val (_, t2) = Logic.dest_equals (Thm.prop_of t') + val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms + val trans_thm = combine_thms thms + in + (case (prop_of trans_thm, t2) of + ((Const(\<^const_name>\HOL.eq\, _) $ t1 $ _), + (Const(\<^const_name>\HOL.eq\, _) $ t3 $ _)) => + if t1 aconv t3 then trans_thm else trans_thm RS sym + | _ => trans_thm (*to be on the safe side*)) + end + + +fun tmp_AC_rule ctxt thms t = + SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt thms + THEN' REPEAT_ALL_NEW (partial_simplify_tac ctxt @{thms eq_commute} + THEN' TRY' (simplify_tac ctxt @{thms ac_simps conj_ac}) + THEN' TRY' (Classical.fast_tac ctxt))) + + +(* And/Or *) + +local + fun not_and_rule_prove ctxt prems = + Method.insert_tac ctxt prems + THEN' K (unfold_tac ctxt @{thms de_Morgan_conj}) + THEN_ALL_NEW TRY' (assume_tac ctxt) + + fun or_pos_prove ctxt _ = + K (unfold_tac ctxt @{thms de_Morgan_disj not_not}) + THEN' match_tac ctxt @{thms verit_and_pos} + THEN' K (unfold_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not}) + THEN' TRY' (assume_tac ctxt) + + fun not_or_rule_prove ctxt prems = + Method.insert_tac ctxt prems + THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not}) + THEN' TRY' (REPEAT' (match_tac ctxt @{thms conjI})) + THEN_ALL_NEW ((REPEAT' (ematch_tac ctxt @{thms conjE})) + THEN' TRY' (assume_tac ctxt)) + + fun and_rule_prove ctxt prems = + Method.insert_tac ctxt prems + THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1))) + THEN' TRY' (assume_tac ctxt) + + fun and_neg_rule_prove ctxt _ = + match_tac ctxt @{thms verit_and_neg} + THEN' K (unfold_tac ctxt @{thms de_Morgan_conj not_not}) + THEN' TRY' (assume_tac ctxt) + + fun prover tac = prove_abstract SMT_Replay_Methods.abstract_prop tac + +in + +val and_rule = prover and_rule_prove + +val not_and_rule = prover not_and_rule_prove + +val not_or_rule = prover not_or_rule_prove + +val or_pos_rule = prover or_pos_prove + +val and_neg_rule = prover and_neg_rule_prove + +val or_neg_rule = prove_abstract SMT_Replay_Methods.abstract_bool (fn ctxt => fn _ => + resolve_tac ctxt @{thms verit_or_neg} + THEN' K (unfold_tac ctxt @{thms not_not}) + THEN_ALL_NEW + (REPEAT' + (SOLVED' (match_tac ctxt @{thms disjI1} THEN_ALL_NEW assume_tac ctxt) + ORELSE' (match_tac ctxt @{thms disjI2} THEN' TRY' (assume_tac ctxt))))) + +fun and_pos ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos}) + THEN' TRY' (assume_tac ctxt)) + +end + + +(* Equivalence Transformation *) + +local + fun prove_equiv equiv_thm ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [equiv_thm OF [thm]] + THEN' TRY' (assume_tac ctxt)) + | prove_equiv _ ctxt thms t = replay_error ctxt "invalid application in some equiv rule" Unsupported thms t +in + +val not_equiv1 = prove_equiv @{lemma \\(A \ B) \ A \ B\ by blast} +val not_equiv2 = prove_equiv @{lemma \\(A \ B) \ \A \ \B\ by blast} +val equiv1 = prove_equiv @{lemma \(A \ B) \ \A \ B\ by blast} +val equiv2 = prove_equiv @{lemma \(A \ B) \ A \ \B\ by blast} +val not_implies1 = prove_equiv @{lemma \\(A \ B) \ A\ by blast} +val not_implies2 = prove_equiv @{lemma \\(A \B) \ \B\ by blast} + +end + + +(* Equivalence Lemma *) +(*equiv_pos2 is very important for performance. We have tried various tactics, including +a specialisation of SMT_Replay_Methods.match_instantiate, but there never was a measurable +and consistent gain.*) +local + fun prove_equiv_pos_neg2 thm ctxt _ t = + SMT_Replay_Methods.match_instantiate ctxt t thm +in + +val equiv_pos1_thm = @{lemma \\(a \ b) \ a \ \b\ by blast+} +val equiv_pos1 = prove_equiv_pos_neg2 equiv_pos1_thm + +val equiv_pos2_thm = @{lemma \\a b. (a \ b) \ \a \ b\ by blast+} +val equiv_pos2 = prove_equiv_pos_neg2 equiv_pos2_thm + +val equiv_neg1_thm = @{lemma \(a \ b) \ \a \ \b\ by blast+} +val equiv_neg1 = prove_equiv_pos_neg2 equiv_neg1_thm + +val equiv_neg2_thm = @{lemma \(a \ b) \ a \ b\ by blast} +val equiv_neg2 = prove_equiv_pos_neg2 equiv_neg2_thm + +end + + +local + fun implies_pos_neg_term ctxt thm (\<^term>\Trueprop\ $ + (\<^term>\HOL.disj\ $ (\<^term>\HOL.implies\ $ a $ b) $ _)) = + Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm + | implies_pos_neg_term ctxt thm t = + replay_error ctxt "invalid application in Implies" Unsupported [thm] t + + fun prove_implies_pos_neg thm ctxt _ t = + let val thm = implies_pos_neg_term ctxt thm t + in + SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [thm] + THEN' TRY' (assume_tac ctxt)) + end +in + +val implies_neg1_thm = @{lemma \(a \ b) \ a\ by blast} +val implies_neg1 = prove_implies_pos_neg implies_neg1_thm + +val implies_neg2_thm = @{lemma \(a \ b) \ \b\ by blast} +val implies_neg2 = prove_implies_pos_neg implies_neg2_thm + +val implies_thm = @{lemma \(a \ b) \ \a \ b\ by blast} +fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [implies_thm OF prems] + THEN' TRY' (assume_tac ctxt)) + +end + + +(* BFun *) + +local + val bfun_theorems = @{thms verit_bfun_elim} +in + +fun bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt prems + THEN' TRY' (eqsubst_all ctxt bfun_theorems) + THEN' TRY' (simplify_tac ctxt @{thms eq_commute all_conj_distrib ex_disj_distrib})) + +end + + +(* If-Then-Else *) + +local + fun prove_ite ite_thm thm ctxt = + resolve_tac ctxt [ite_thm OF [thm]] + THEN' TRY' (assume_tac ctxt) +in + +val ite_pos1_thm = + @{lemma \\(if x then P else Q) \ x \ Q\ by auto} + +fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt [ite_pos1_thm]) + +val ite_pos2_thms = + @{lemma \\(if x then P else Q) \ \x \ P\ \\(if \x then P else Q) \ x \ P\ by auto} + +fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_pos2_thms) + +val ite_neg1_thms = + @{lemma \(if x then P else Q) \ x \ \Q\ \(if x then P else \Q) \ x \ Q\ by auto} + +fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg1_thms) + +val ite_neg2_thms = + @{lemma \(if x then P else Q) \ \x \ \P\ \(if \x then P else Q) \ x \ \P\ + \(if x then \P else Q) \ \x \ P\ \(if \x then \P else Q) \ x \ P\ + by auto} + +fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg2_thms) + +val ite1_thm = + @{lemma \(if x then P else Q) \ x \ Q\ by (auto split: if_splits) } + +fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite1_thm thm ctxt) + +val ite2_thm = + @{lemma \(if x then P else Q) \ \x \ P\ by (auto split: if_splits) } + +fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite2_thm thm ctxt) + +val not_ite1_thm = + @{lemma \\(if x then P else Q) \ x \ \Q\ by (auto split: if_splits) } + +fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite1_thm thm ctxt) + +val not_ite2_thm = + @{lemma \\(if x then P else Q) \ \x \ \P\ by (auto split: if_splits) } + +fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite2_thm thm ctxt) + +(*ite_intro can introduce new terms that are in the proof exactly the sames as the old one, but are +not internally, hence the possible reordering.*) +fun ite_intro ctxt _ t = + let + fun simplify_ite ctxt thms = + ctxt + |> empty_simpset + |> put_simpset HOL_basic_ss + |> (fn ctxt => ctxt addsimps thms @ @{thms if_True if_False refl simp_thms if_cancel}) + |> Raw_Simplifier.add_eqcong @{thm verit_ite_if_cong} + |> Simplifier.full_simp_tac + in + SMT_Replay_Methods.prove ctxt t (fn _ => simplify_ite ctxt [] + THEN' TRY' (simplify_ite ctxt @{thms eq_commute})) + end +end + + +(* Quantifiers *) + +local + val rm_unused = @{lemma \(\x. P) = P\ \(\x. P) = P\ by blast+} + + fun qnt_cnf_tac ctxt = + simplify_tac ctxt @{thms de_Morgan_conj de_Morgan_disj imp_conv_disj + iff_conv_conj_imp if_bool_eq_disj ex_simps all_simps ex_disj_distrib + verit_connective_def(3) all_conj_distrib} + THEN' TRY' (Blast.blast_tac ctxt) +in +fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + K (unfold_tac ctxt rm_unused)) + +fun onepoint ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt prems + THEN' Simplifier.full_simp_tac (put_simpset HOL_basic_ss (empty_simpset ctxt) + addsimps @{thms HOL.simp_thms HOL.all_simps} + addsimprocs [@{simproc HOL.defined_All}, @{simproc HOL.defined_Ex}]) + THEN' TRY' (Blast.blast_tac ctxt) + THEN' TRY' (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt [])) + +fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t Classical.fast_tac + +fun qnt_cnf ctxt _ t = SMT_Replay_Methods.prove ctxt t qnt_cnf_tac + +fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + partial_simplify_tac ctxt []) + +end + +(* Equality *) + +fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}]) + THEN' REPEAT' (resolve_tac ctxt @{thms impI}) + THEN' REPEAT' (eresolve_tac ctxt @{thms conjI}) + THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1)) + THEN' resolve_tac ctxt @{thms refl}) + +local + fun find_rew rews t t' = + (case AList.lookup (op =) rews (t, t') of + SOME thm => SOME (thm COMP @{thm symmetric}) + | NONE => + (case AList.lookup (op =) rews (t', t) of + SOME thm => SOME thm + | NONE => NONE)) + + fun eq_pred_conv rews t ctxt ctrm = + (case find_rew rews t (Thm.term_of ctrm) of + SOME thm => Conv.rewr_conv thm ctrm + | NONE => + (case t of + f $ arg => + (Conv.fun_conv (eq_pred_conv rews f ctxt) then_conv + Conv.arg_conv (eq_pred_conv rews arg ctxt)) ctrm + | Abs (_, _, f) => Conv.abs_conv (eq_pred_conv rews f o snd) ctxt ctrm + | _ => Conv.all_conv ctrm)) + + fun eq_pred_rewrite_tac ({context = ctxt, prems, concl, ...}: Subgoal.focus) = + let + val rews = prems + |> map_filter (try (apfst (HOLogic.dest_eq o Thm.term_of o Object_Logic.dest_judgment ctxt o + Thm.cconcl_of) o `(fn x => x))) + |> map (apsnd (fn x => @{thm eq_reflection} OF [x])) + fun conv_left conv = Conv.arg_conv (Conv.arg_conv conv) + fun conv_left_neg conv = Conv.arg_conv (Conv.arg_conv (Conv.arg_conv conv)) + val (t1, conv_term) = + (case Thm.term_of (Object_Logic.dest_judgment ctxt concl) of + Const(_, _) $ (Const(\<^const_name>\HOL.Not\, _) $ t1) $ _ => (t1, conv_left) + | Const(_, _) $ t1 $ (Const(\<^const_name>\HOL.Not\, _) $ _) => (t1, conv_left_neg) + | Const(_, _) $ t1 $ _ => (t1, conv_left) + | t1 => (t1, conv_left)) + fun throwing_CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st) + in + throwing_CONVERSION (conv_term (eq_pred_conv rews t1 ctxt)) + end +in + +fun eq_congruent_pred ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \_ = _\]} RSN (1, @{thm iffD2}) OF @{thms impI}]) + THEN' (fn i => Subgoal.FOCUS (fn focus => eq_pred_rewrite_tac focus i) ctxt i) + THEN' (resolve_tac ctxt @{thms refl excluded_middle excluded_middle[of \\_\, unfolded not_not]} + ORELSE' assume_tac ctxt)) + +val eq_congruent = eq_congruent_pred + +end + + +(* Subproof *) + +fun subproof ctxt [prem] t = + SMT_Replay_Methods.prove ctxt t (fn _ => + (REPEAT' (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}], + @{thm disj_not1[of \\_\, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]]) + THEN' resolve_tac ctxt [prem] + THEN_ALL_NEW assume_tac ctxt + THEN' TRY' (assume_tac ctxt)) + ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt)) + | subproof ctxt prems t = + replay_error ctxt "invalid application, only one assumption expected" Subproof prems t + + +(* Simplifying Steps *) + +(* The reconstruction is a bit tricky: At first we only rewrite only based on the rules that are +passed as argument. Then we simply use simp_thms to reconstruct all the proofs (and these theorems +cover all the simplification below). +*) +local + fun rewrite_only_thms ctxt thms = + ctxt + |> empty_simpset + |> put_simpset HOL_basic_ss + |> (fn ctxt => ctxt addsimps thms) + |> Simplifier.full_simp_tac + fun rewrite_only_thms_tmp ctxt thms = + rewrite_only_thms ctxt thms + THEN' TRY' (K (Clasimp.auto_tac ctxt)) (*TODO: TEMP until cvc5 produces fine grained simplification steps *) + + fun rewrite_thms ctxt thms = + ctxt + |> empty_simpset + |> put_simpset HOL_basic_ss + |> Raw_Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]} + |> (fn ctxt => ctxt addsimps thms addsimps @{thms simp_thms}) + |> Simplifier.full_simp_tac + + fun chain_rewrite_thms ctxt thms = + TRY' (rewrite_only_thms ctxt thms) + THEN' TRY' (rewrite_thms ctxt thms) + THEN' TRY' (K (Clasimp.auto_tac ctxt)) (*TODO: TEMP until cvc5 produces fine grained simplification steps *) + + fun chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2 = + TRY' (rewrite_only_thms ctxt thms1) + THEN' TRY' (rewrite_thms ctxt thms2) + THEN' TRY' (K (Clasimp.auto_tac ctxt)) (*TODO: TEMP until cvc5 produces fine grained simplification steps *) + + fun chain_rewrite_thms_two_step ctxt thms1 thms2 thms3 thms4 = + chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2 + THEN' TRY' (chain_rewrite_two_step_with_ac_simps ctxt thms3 thms4) + + val imp_refl = @{lemma \(P \ P) = True\ by blast} + +in +fun rewrite_bool_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + (chain_rewrite_thms ctxt @{thms verit_bool_simplify})) + +fun rewrite_and_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_and_simplify verit_and_simplify1} + @{thms verit_and_simplify})) + +fun rewrite_or_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_or_simplify verit_or_simplify_1} + @{thms verit_or_simplify}) + THEN' TRY' (REPEAT' (match_tac ctxt @{thms verit_and_pos}) THEN' assume_tac ctxt)) + +fun rewrite_not_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + (rewrite_only_thms_tmp ctxt @{thms verit_not_simplify})) + +fun rewrite_equiv_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + (rewrite_only_thms_tmp ctxt @{thms verit_equiv_simplify})) + +fun rewrite_eq_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + (chain_rewrite_two_step_with_ac_simps ctxt + @{thms verit_eq_simplify} + (Named_Theorems.get ctxt @{named_theorems ac_simps}))) + +fun rewrite_implies_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + (rewrite_only_thms_tmp ctxt @{thms verit_implies_simplify})) + +(* It is more efficient to first fold the implication symbols. + That is however not enough when symbols appears within + expressions, hence we also unfold implications in the + other direction. *) +fun rewrite_connective_def ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + chain_rewrite_thms_two_step ctxt + (imp_refl :: @{thms not_not verit_connective_def[symmetric]}) + (@{thms verit_connective_def[symmetric]}) + (imp_refl :: @{thms not_not verit_connective_def}) + (@{thms verit_connective_def})) + +fun rewrite_minus_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + chain_rewrite_two_step_with_ac_simps ctxt + @{thms arith_simps verit_minus_simplify} + (Named_Theorems.get ctxt @{named_theorems ac_simps} @ + @{thms numerals arith_simps arith_special + numeral_class.numeral.numeral_One})) + +fun rewrite_comp_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + chain_rewrite_thms ctxt @{thms verit_comp_simplify}) + +fun rewrite_ite_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + (rewrite_only_thms_tmp ctxt @{thms verit_ite_simplify})) +end + + +(* Simplifications *) + +local + fun simplify_arith ctxt thms = partial_simplify_tac ctxt + (thms @ Named_Theorems.get ctxt @{named_theorems ac_simps} @ @{thms arith_simps}) +in + +fun sum_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + simplify_arith ctxt @{thms verit_sum_simplify arith_special} + THEN' TRY' (K (Clasimp.auto_tac ctxt))) (*TODO: TEMP until cvc5 produces fine grained simplification steps *) + +fun prod_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + simplify_arith ctxt @{thms verit_prod_simplify} + THEN' TRY' (K (Clasimp.auto_tac ctxt))) (*TODO: TEMP until cvc5 produces fine grained simplification steps *) +end + +fun all_simplify ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + TRY' (K (Clasimp.auto_tac ctxt))) (*TODO: TEMP until cvc5 produces fine grained simplification steps *) + +(* Arithmetics *) +local + +val la_rw_eq_thm = @{lemma \(a :: nat) = b \ (a \ b) \ (a \ b)\ by auto} +in +fun la_rw_eq ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t la_rw_eq_thm + +fun la_generic_prove args ctxt _ = SMT_Replay_Arith.la_farkas args ctxt + +fun la_generic ctxt _ args = + prove_abstract (SMT_Replay_Methods.abstract_arith_shallow ctxt) (la_generic_prove args) ctxt [] + +fun lia_generic ctxt _ t = + SMT_Replay_Methods.prove_arith_rewrite SMT_Replay_Methods.abstract_neq ctxt t + +fun la_disequality ctxt _ t = + SMT_Replay_Methods.match_instantiate ctxt t @{thm verit_la_disequality} + +end + + +(* Symm and Not_Symm*) + +local + fun prove_symm symm_thm ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [symm_thm OF [thm]] + THEN' TRY' (assume_tac ctxt)) + | prove_symm _ ctxt thms t = replay_error ctxt "invalid application in some symm rule" Unsupported thms t +in + val symm_thm = + @{lemma \(B = A) \ A = B\ by blast } + val symm = prove_symm symm_thm + + val not_symm_thm = + @{lemma \\(B = A) \ \(A = B)\ by blast } + val not_symm = prove_symm not_symm_thm +end + +(* Reordering *) +local + fun prove_reordering ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>( + Method.insert_tac ctxt [thm] + THEN' match_tac ctxt @{thms ccontr} + THEN' K (unfold_tac ctxt @{thms de_Morgan_disj}) + THEN' TRY o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE}) + THEN' CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms disjE}) + THEN' REPEAT'(ematch_tac ctxt @{thms notE} THEN' TRY' (assume_tac ctxt)) + )) + | prove_reordering ctxt thms t = + replay_error ctxt "invalid application in some reordering rule" Unsupported thms t +in + val reordering = prove_reordering +end + +end; diff --git a/src/HOL/Tools/SMT/smt_systems.ML b/src/HOL/Tools/SMT/smt_systems.ML --- a/src/HOL/Tools/SMT/smt_systems.ML +++ b/src/HOL/Tools/SMT/smt_systems.ML @@ -1,234 +1,234 @@ (* Title: HOL/Tools/SMT/smt_systems.ML Author: Sascha Boehme, TU Muenchen Setup SMT solvers. *) signature SMT_SYSTEMS = sig val cvc4_extensions: bool Config.T val z3_extensions: bool Config.T end; structure SMT_Systems: SMT_SYSTEMS = struct val mashN = "mash" val mepoN = "mepo" val meshN = "mesh" (* helper functions *) fun check_tool var () = (case getenv var of "" => NONE | s => if File.is_file (Path.variable var |> Path.expand |> Path.platform_exe) then SOME [s] else NONE); fun make_avail name () = getenv (name ^ "_SOLVER") <> "" fun make_command name () = [getenv (name ^ "_SOLVER")] fun outcome_of unsat sat unknown timeout solver_name line = if String.isPrefix unsat line then SMT_Solver.Unsat else if String.isPrefix sat line then SMT_Solver.Sat else if String.isPrefix unknown line then SMT_Solver.Unknown else if String.isPrefix timeout line then SMT_Solver.Time_Out else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^ " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^ " option for details")) (* When used with bitvectors, CVC4 can produce error messages like: $ISABELLE_TMP_PREFIX/... No set-logic command was given before this point. These message should be ignored. *) fun is_blank_or_error_line "" = true | is_blank_or_error_line s = String.isPrefix "(error " s orelse String.isPrefix (getenv "ISABELLE_TMP_PREFIX") s fun on_first_line test_outcome solver_name lines = let val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) val (l, ls) = split_first (drop_prefix is_blank_or_error_line lines) in (test_outcome solver_name l, ls) end fun on_first_non_unsupported_line test_outcome solver_name lines = on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines) (* CVC4 *) val cvc4_extensions = Attrib.setup_config_bool \<^binding>\cvc4_extensions\ (K false) local fun cvc4_options ctxt = ["--no-stats", "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), "--lang=smt2"] @ (case SMT_Config.get_timeout ctxt of NONE => [] | SOME t => ["--tlimit", string_of_int (Time.toMilliseconds t)]) fun select_class ctxt = if Config.get ctxt cvc4_extensions then if Config.get ctxt SMT_Config.higher_order then CVC4_Interface.hosmtlib_cvc4C else CVC4_Interface.smtlib_cvc4C else if Config.get ctxt SMT_Config.higher_order then SMTLIB_Interface.hosmtlibC else if Config.get ctxt SMT_Config.native_bv then SMTLIB_Interface.bvsmlibC else SMTLIB_Interface.smtlibC in val cvc4: SMT_Solver.solver_config = { name = "cvc4", class = select_class, avail = make_avail "CVC4", command = make_command "CVC4", options = cvc4_options, smt_options = [(":produce-unsat-cores", "true")], good_slices = (* FUDGE *) [((512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]), ((64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]), ((1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]), ((256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]), ((32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]), ((128, meshN), ["--no-e-matching", "--full-saturate-quant"]), ((256, meshN), ["--finite-model-find", "--fmf-inst-engine"])], outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), parse_proof = SOME (K CVC4_Proof_Parse.parse_proof), replay = NONE } end (* veriT *) local fun select_class ctxt = if Config.get ctxt SMT_Config.higher_order then SMTLIB_Interface.hosmtlibC else SMTLIB_Interface.smtlibC fun veriT_options ctxt = ["--proof-with-sharing", "--proof-define-skolems", "--proof-prune", "--proof-merge", "--disable-print-success", "--disable-banner"] @ Verit_Proof.veriT_current_strategy (Context.Proof ctxt) @ (case SMT_Config.get_timeout ctxt of NONE => [] | SOME t => ["--max-time=" ^ string_of_int (Time.toMilliseconds t)]) in val veriT: SMT_Solver.solver_config = { name = "verit", class = select_class, avail = is_some o check_tool "ISABELLE_VERIT", command = the o check_tool "ISABELLE_VERIT", options = veriT_options, smt_options = [(":produce-proofs", "true")], good_slices = (* FUDGE *) [((1024, meshN), []), ((512, mashN), []), ((64, meshN), []), ((128, meshN), []), ((256, mepoN), []), ((32, meshN), [])], outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"), - parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), + parse_proof = SOME (K Lethe_Proof_Parse.parse_proof), replay = SOME Verit_Replay.replay } end (* Z3 *) val z3_extensions = Attrib.setup_config_bool \<^binding>\z3_extensions\ (K false) local fun z3_options ctxt = ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), "smt.refine_inj_axioms=false"] @ (case SMT_Config.get_timeout ctxt of NONE => [] | SOME t => ["-T:" ^ string_of_int (Real.ceil (Time.toReal t))]) @ ["-smt2"] fun select_class ctxt = if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else if Config.get ctxt SMT_Config.native_bv then SMTLIB_Interface.bvsmlibC else SMTLIB_Interface.smtlibC in val z3: SMT_Solver.solver_config = { name = "z3", class = select_class, avail = make_avail "Z3", command = make_command "Z3", options = z3_options, smt_options = [(":produce-proofs", "true")], good_slices = (* FUDGE *) [((1024, meshN), []), ((512, mepoN), []), ((64, meshN), []), ((256, meshN), []), ((128, mashN), []), ((32, meshN), [])], outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), parse_proof = SOME Z3_Replay.parse_proof, replay = SOME Z3_Replay.replay } end (* smt tactic *) val parse_smt_options = Scan.optional (Args.parens (Args.name -- Scan.option (\<^keyword>\,\ |-- Args.name)) >> apfst SOME) (NONE, NONE) fun smt_method ((solver, stgy), thms) ctxt facts = let val default_solver = SMT_Config.solver_of ctxt val solver = the_default default_solver solver val _ = if solver = "z3" andalso stgy <> NONE then warning ("No strategy is available for z3. Ignoring " ^ quote (the stgy)) else () val ctxt = ctxt |> (if stgy <> NONE then Context.proof_map (Verit_Proof.select_veriT_stgy (the stgy)) else I) |> Context.Proof |> SMT_Config.select_solver solver |> Context.proof_of in HEADGOAL (SOLVED' (SMT_Solver.smt_tac ctxt (thms @ facts))) end val _ = Theory.setup (Method.setup \<^binding>\smt\ (Scan.lift parse_smt_options -- Attrib.thms >> (METHOD oo smt_method)) "Call to the SMT solvers veriT or z3") (* overall setup *) val _ = Theory.setup ( SMT_Solver.add_solver cvc4 #> SMT_Solver.add_solver veriT #> SMT_Solver.add_solver z3) end; diff --git a/src/HOL/Tools/SMT/verit_replay.ML b/src/HOL/Tools/SMT/verit_replay.ML --- a/src/HOL/Tools/SMT/verit_replay.ML +++ b/src/HOL/Tools/SMT/verit_replay.ML @@ -1,322 +1,322 @@ (* Title: HOL/Tools/SMT/verit_replay.ML Author: Mathias Fleury, MPII VeriT proof parsing and replay. *) signature VERIT_REPLAY = sig val replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm end; structure Verit_Replay: VERIT_REPLAY = struct fun subst_only_free pairs = let fun substf u = (case Termtab.lookup pairs u of SOME u' => u' | NONE => (case u of (Abs(a,T,t)) => Abs(a, T, substf t) | (t$u') => substf t $ substf u' | u => u)) in substf end; fun under_fixes f unchanged_prems (prems, nthms) names args insts decls (concl, ctxt) = let val thms1 = unchanged_prems @ map (SMT_Replay.varify ctxt) prems val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("names =", names)) val thms2 = map snd nthms val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("prems=", prems)) val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("nthms=", nthms)) val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("thms1=", thms1)) val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("thms2=", thms2)) in (f ctxt (thms1 @ thms2) args insts decls concl) end (** Replaying **) fun replay_thm method_for rewrite_rules ll_defs ctxt assumed unchanged_prems prems nthms concl_transformation global_transformation args insts (Verit_Proof.VeriT_Replay_Node {id, rule, concl, bounds, declarations = decls, ...}) = let val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> id) val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in Raw_Simplifier.rewrite_term thy rewrite_rules [] #> not (null ll_defs andalso Verit_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs end val rewrite_concl = if Verit_Proof.keep_app_symbols rule then filter (curry Term.could_unify (Thm.concl_of @{thm SMT.fun_app_def}) o Thm.concl_of) rewrite_rules else rewrite_rules val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in Raw_Simplifier.rewrite_term thy rewrite_concl [] #> Object_Logic.atomize_term ctxt #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs #> SMTLIB_Isar.unskolemize_names ctxt #> HOLogic.mk_Trueprop end val concl = concl |> Term.subst_free concl_transformation |> subst_only_free global_transformation |> post in if rule = Verit_Proof.input_rule then (case Symtab.lookup assumed id of SOME (_, thm) => thm | _ => raise Fail ("assumption " ^ @{make_string} id ^ " not found")) else under_fixes (method_for rule) unchanged_prems (prems, nthms) (map fst bounds) (map rewrite args) (Symtab.map (K rewrite) insts) decls (concl, ctxt) |> Simplifier.simplify (empty_simpset ctxt addsimps rewrite_rules) end fun add_used_asserts_in_step (Verit_Proof.VeriT_Replay_Node {prems, subproof = (_, _, _, subproof), ...}) = union (op =) (map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) prems @ flat (map (fn x => add_used_asserts_in_step x []) subproof)) fun remove_rewrite_rules_from_rules n = (fn (step as Verit_Proof.VeriT_Replay_Node {id, ...}) => (case try (snd o SMTLIB_Interface.role_and_index_of_assert_name) id of NONE => SOME step | SOME a => if a < n then NONE else SOME step)) fun replay_theorem_step rewrite_rules ll_defs assumed inputs proof_prems (step as Verit_Proof.VeriT_Replay_Node {id, rule, prems, bounds, args, insts, subproof = (fixes, assms, input, subproof), concl, ...}) state = let val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state val (_, ctxt) = Variable.variant_fixes (map fst bounds) ctxt |> (fn (names, ctxt) => (names, fold Variable.declare_term [SMTLIB_Isar.unskolemize_names ctxt concl] ctxt)) val (names, sub_ctxt) = Variable.variant_fixes (map fst fixes) ctxt ||> fold Variable.declare_term (map Free fixes) val export_vars = concl_tranformation @ (ListPair.zip (map Free fixes, map Free (ListPair.zip (names, map snd fixes)))) val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in Raw_Simplifier.rewrite_term thy ((if Verit_Proof.keep_raw_lifting rule then tl rewrite_rules else rewrite_rules)) [] #> Object_Logic.atomize_term ctxt #> not (null ll_defs andalso Verit_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs #> SMTLIB_Isar.unskolemize_names ctxt #> HOLogic.mk_Trueprop end val assms = map (subst_only_free global_transformation o Term.subst_free (export_vars) o post) assms val input = map (subst_only_free global_transformation o Term.subst_free (export_vars) o post) input val (all_proof_prems', sub_ctxt2) = Assumption.add_assumes (map (Thm.cterm_of sub_ctxt) (assms @ input)) sub_ctxt fun is_refl thm = Thm.concl_of thm |> (fn (_ $ t) => t) |> HOLogic.dest_eq |> (op =) handle TERM _=> false val all_proof_prems' = all_proof_prems' |> filter_out is_refl val proof_prems' = take (length assms) all_proof_prems' val input = drop (length assms) all_proof_prems' val all_proof_prems = proof_prems @ proof_prems' val replay = replay_theorem_step rewrite_rules ll_defs assumed (input @ inputs) all_proof_prems val (proofs', stats, _, _, sub_global_rew) = fold replay subproof (proofs, stats, sub_ctxt2, export_vars, global_transformation) val export_thm = singleton (Proof_Context.export sub_ctxt2 ctxt) (*for sko_ex and sko_forall, assumptions are in proofs', but the definition of the skolem function is in proofs *) val nthms = prems |> map (apsnd export_thm) o map_filter (Symtab.lookup (if (null subproof) then proofs else proofs')) val nthms' = (if Verit_Proof.is_skolemization rule then prems else []) |> map_filter (Symtab.lookup proofs) val args = map (Term.subst_free concl_tranformation o subst_only_free global_transformation) args val insts = Symtab.map (K (Term.subst_free concl_tranformation o subst_only_free global_transformation)) insts val proof_prems = - if Verit_Replay_Methods.requires_subproof_assms prems rule then proof_prems else [] + if Lethe_Replay_Methods.requires_subproof_assms prems rule then proof_prems else [] val local_inputs = - if Verit_Replay_Methods.requires_local_input prems rule then input @ inputs else [] + if Lethe_Replay_Methods.requires_local_input prems rule then input @ inputs else [] val replay = Timing.timing (replay_thm Verit_Replay_Methods.method_for rewrite_rules ll_defs ctxt assumed [] (proof_prems @ local_inputs) (nthms @ nthms') concl_tranformation global_transformation args insts) val ({elapsed, ...}, thm) = SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out val stats' = Symtab.cons_list (rule, Time.toNanoseconds elapsed) stats (* val _ = ((Time.toMilliseconds elapsed > 10 andalso (rule = "cong")) ? @{print}) ("WARNING slow " ^ id ^ @{make_string} rule ^ ": " ^ string_of_int (Time.toMilliseconds elapsed) ^ " " ^ @{make_string} (proof_prems @ local_inputs)) val _ = ((Time.toMilliseconds elapsed > 10 andalso (rule = "cong")) ? @{print}) ( (proof_prems @ local_inputs)) val _ = ((Time.toMilliseconds elapsed > 10 andalso (rule = "cong")) ? @{print}) thm val _ = ((Time.toMilliseconds elapsed > 40) ? @{print}) ("WARNING slow " ^ id ^ @{make_string} rule ^ ": " ^ string_of_int (Time.toMilliseconds elapsed)) *) val proofs = Symtab.update (id, (map fst bounds, thm)) proofs in (proofs, stats', ctxt, concl_tranformation, sub_global_rew) end fun replay_definition_step rewrite_rules ll_defs _ _ _ (Verit_Proof.VeriT_Replay_Node {id, declarations = raw_declarations, subproof = (_, _, _, subproof), ...}) state = let val _ = if null subproof then () else raise (Fail ("unrecognized veriT proof, definition has a subproof")) val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state val global_transformer = subst_only_free global_transformation val rewrite = let val thy = Proof_Context.theory_of ctxt in Raw_Simplifier.rewrite_term thy (rewrite_rules) [] #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs end val start0 = Timing.start () val declaration = map (apsnd (rewrite o global_transformer)) raw_declarations val (names, ctxt) = Variable.variant_fixes (map fst declaration) ctxt ||> fold Variable.declare_term (map Free (map (apsnd fastype_of) declaration)) val old_names = map Free (map (fn (a, b) => (a, fastype_of b)) declaration) val new_names = map Free (ListPair.zip (names, map (fastype_of o snd) declaration)) fun update_mapping (a, b) tab = if a <> b andalso Termtab.lookup tab a = NONE then Termtab.update_new (a, b) tab else tab val global_transformation = global_transformation |> fold update_mapping (ListPair.zip (old_names, new_names)) val global_transformer = subst_only_free global_transformation val generate_definition = (fn (name, term) => (HOLogic.mk_Trueprop (Const(\<^const_name>\HOL.eq\, fastype_of term --> fastype_of term --> @{typ bool}) $ Free (name, fastype_of term) $ term))) #> global_transformer #> Thm.cterm_of ctxt val decls = map generate_definition declaration val (defs, ctxt) = Assumption.add_assumes decls ctxt val thms_with_old_name = ListPair.zip (map fst declaration, defs) val proofs = fold (fn (name, thm) => Symtab.update (id, ([name], @{thm sym} OF [thm]))) thms_with_old_name proofs val total = Time.toNanoseconds (#elapsed (Timing.result start0)) val stats = Symtab.cons_list ("choice", total) stats in (proofs, stats, ctxt, concl_tranformation, global_transformation) end fun replay_assumed assms ll_defs rewrite_rules stats ctxt term = let val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in Raw_Simplifier.rewrite_term thy rewrite_rules [] #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs end val replay = Timing.timing (SMT_Replay_Methods.prove ctxt (rewrite term)) val ({elapsed, ...}, thm) = SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay (fn _ => Method.insert_tac ctxt (map snd assms) THEN' Classical.fast_tac ctxt) handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out val stats' = Symtab.cons_list (Verit_Proof.input_rule, Time.toNanoseconds elapsed) stats in (thm, stats') end fun replay_step rewrite_rules ll_defs assumed inputs proof_prems (step as Verit_Proof.VeriT_Replay_Node {rule, ...}) state = if rule = Verit_Proof.veriT_def then replay_definition_step rewrite_rules ll_defs assumed inputs proof_prems step state else replay_theorem_step rewrite_rules ll_defs assumed inputs proof_prems step state fun replay outer_ctxt ({context = ctxt, typs, terms, rewrite_rules, assms, ll_defs, ...} : SMT_Translate.replay_data) output = let val rewrite_rules = filter_out (fn thm => Term.could_unify (Thm.prop_of @{thm verit_eq_true_simplify}, Thm.prop_of thm)) rewrite_rules val num_ll_defs = length ll_defs val index_of_id = Integer.add (~ num_ll_defs) val id_of_index = Integer.add num_ll_defs val start0 = Timing.start () val (actual_steps, ctxt2) = Verit_Proof.parse_replay typs terms output ctxt val parsing_time = Time.toNanoseconds (#elapsed (Timing.result start0)) fun step_of_assume (j, (_, th)) = Verit_Proof.VeriT_Replay_Node { id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j), rule = Verit_Proof.input_rule, args = [], prems = [], proof_ctxt = [], concl = Thm.prop_of th |> Raw_Simplifier.rewrite_term (Proof_Context.theory_of (empty_simpset ctxt addsimps rewrite_rules)) rewrite_rules [], bounds = [], insts = Symtab.empty, declarations = [], subproof = ([], [], [], [])} val used_assert_ids = fold add_used_asserts_in_step actual_steps [] fun normalize_tac ctxt = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in Raw_Simplifier.rewrite_term thy rewrite_rules [] end val used_assm_js = map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME (i, nth assms i) else NONE end) used_assert_ids val assm_steps = map step_of_assume used_assm_js fun extract (Verit_Proof.VeriT_Replay_Node {id, rule, concl, bounds, ...}) = (id, rule, concl, map fst bounds) fun cond rule = rule = Verit_Proof.input_rule val add_asssert = SMT_Replay.add_asserted Symtab.update Symtab.empty extract cond val ((_, _), (ctxt3, assumed)) = add_asssert outer_ctxt rewrite_rules assms (map_filter (remove_rewrite_rules_from_rules num_ll_defs) assm_steps) ctxt2 val used_rew_js = map_filter (fn id => let val i = index_of_id id in if i < 0 then SOME (id, normalize_tac ctxt (nth ll_defs id)) else NONE end) used_assert_ids val (assumed, stats) = fold (fn ((id, thm)) => fn (assumed, stats) => let val (thm, stats) = replay_assumed assms ll_defs rewrite_rules stats ctxt thm val name = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom id in (Symtab.update (name, ([], thm)) assumed, stats) end) used_rew_js (assumed, Symtab.cons_list ("parsing", parsing_time) Symtab.empty) val ctxt4 = ctxt3 |> put_simpset (SMT_Replay.make_simpset ctxt3 []) |> Config.put SAT.solver (Config.get ctxt3 SMT_Config.sat_solver) val len = Verit_Proof.number_of_steps actual_steps fun steps_with_depth _ [] = [] | steps_with_depth i (p :: ps) = (i + Verit_Proof.number_of_steps [p], p) :: steps_with_depth (i + Verit_Proof.number_of_steps [p]) ps val actual_steps = steps_with_depth 0 actual_steps val start = Timing.start () val print_runtime_statistics = SMT_Replay.intermediate_statistics ctxt4 start len fun blockwise f (i, x) (next, y) = (if i > next then print_runtime_statistics i else (); (if i > next then i + 10 else next, f x y)) val global_transformation : term Termtab.table = Termtab.empty val (_, (proofs, stats, ctxt5, _, _)) = fold (blockwise (replay_step rewrite_rules ll_defs assumed [] [])) actual_steps (1, (assumed, stats, ctxt4, [], global_transformation)) val total = Time.toMilliseconds (#elapsed (Timing.result start)) val (_, (_, Verit_Proof.VeriT_Replay_Node {id, ...})) = split_last actual_steps val _ = print_runtime_statistics len val thm_with_defs = Symtab.lookup proofs id |> the |> snd |> singleton (Proof_Context.export ctxt5 outer_ctxt) val _ = SMT_Config.statistics_msg ctxt5 (Pretty.string_of o SMT_Replay.pretty_statistics "veriT" total) stats val _ = SMT_Replay.spying (SMT_Config.spy_verit ctxt) ctxt (fn () => SMT_Replay.print_stats (Symtab.dest stats)) "spy_verit" in Verit_Replay_Methods.discharge ctxt [thm_with_defs] @{term False} end end diff --git a/src/HOL/Tools/SMT/verit_replay_methods.ML b/src/HOL/Tools/SMT/verit_replay_methods.ML --- a/src/HOL/Tools/SMT/verit_replay_methods.ML +++ b/src/HOL/Tools/SMT/verit_replay_methods.ML @@ -1,1194 +1,210 @@ (* Title: HOL/Tools/SMT/verit_replay_methods.ML Author: Mathias Fleury, MPII, JKU Proof method for replaying veriT proofs. *) signature VERIT_REPLAY_METHODS = sig (*methods for verit proof rules*) val method_for: string -> Proof.context -> thm list -> term list -> term Symtab.table -> (string * term) list -> term -> thm - val requires_subproof_assms : string list -> string -> bool - val requires_local_input: string list -> string -> bool - val eq_congruent_pred: Proof.context -> 'a -> term -> thm val discharge: Proof.context -> thm list -> term -> thm end; structure Verit_Replay_Methods: VERIT_REPLAY_METHODS = struct -(*Some general comments on the proof format: - 1. Double negations are not always removed. This means for example that the equivalence rules - cannot assume that the double negations have already been removed. Therefore, we match the - term, instantiate the theorem, then use simp (to remove double negations), and finally use - assumption. - 2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule - is doing much more that is supposed to do. Moreover types can make trivial goals (for the - boolean structure) impossible to prove. - 3. Duplicate literals are sometimes removed, mostly by the SAT solver. - - Rules unsupported on purpose: - * Distinct_Elim, XOR, let (we don't need them). - * deep_skolemize (because it is not clear if verit still generates using it). -*) - -datatype verit_rule = - False | True | - - (*input: a repeated (normalized) assumption of assumption of in a subproof*) - Normalized_Input | Local_Input | - (*Subproof:*) - Subproof | - (*Conjunction:*) - And | Not_And | And_Pos | And_Neg | - (*Disjunction""*) - Or | Or_Pos | Not_Or | Or_Neg | - (*Disjunction:*) - Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 | - (*Equivalence:*) - Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 | - (*If-then-else:*) - ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 | - (*Equality:*) - Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans | Refl | Cong | - (*Arithmetics:*) - LA_Disequality | LA_Generic | LA_Tautology | LIA_Generic | LA_Totality | LA_RW_Eq | - NLA_Generic | - (*Quantifiers:*) - Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Onepoint | Bind | Skolem_Forall | Skolem_Ex | - (*Resolution:*) - Theory_Resolution | Resolution | - (*Temporary rules, that the verit developpers want to remove:*) - AC_Simp | - Bfun_Elim | - Qnt_CNF | - (*Used to introduce skolem constants*) - Definition | - (*Former cong rules*) - Bool_Simplify | Or_Simplify | Not_Simplify | And_Simplify | Equiv_Simplify | - Implies_Simplify | Connective_Def | Minus_Simplify | Comp_Simplify | - Eq_Simplify | ITE_Simplify | Sum_Simplify | Prod_Simplify | - Qnt_Simplify | Not_Not | Tautological_Clause | Duplicate_Literals | - (*Unsupported rule*) - Unsupported | - (*For compression*) - Theory_Resolution2 - +open Lethe_Replay_Methods fun verit_rule_of "bind" = Bind | verit_rule_of "cong" = Cong | verit_rule_of "refl" = Refl | verit_rule_of "equiv1" = Equiv1 | verit_rule_of "equiv2" = Equiv2 | verit_rule_of "equiv_pos1" = Equiv_pos1 (*Equiv_pos2 covered below*) | verit_rule_of "equiv_neg1" = Equiv_neg1 | verit_rule_of "equiv_neg2" = Equiv_neg2 | verit_rule_of "sko_forall" = Skolem_Forall | verit_rule_of "sko_ex" = Skolem_Ex | verit_rule_of "eq_reflexive" = Eq_Reflexive | verit_rule_of "forall_inst" = Forall_Inst | verit_rule_of "implies_pos" = Implies_Pos | verit_rule_of "or" = Or | verit_rule_of "not_or" = Not_Or | verit_rule_of "resolution" = Resolution | verit_rule_of "trans" = Trans | verit_rule_of "false" = False | verit_rule_of "ac_simp" = AC_Simp | verit_rule_of "and" = And | verit_rule_of "not_and" = Not_And | verit_rule_of "and_pos" = And_Pos | verit_rule_of "and_neg" = And_Neg | verit_rule_of "or_pos" = Or_Pos | verit_rule_of "or_neg" = Or_Neg | verit_rule_of "not_equiv1" = Not_Equiv1 | verit_rule_of "not_equiv2" = Not_Equiv2 | verit_rule_of "not_implies1" = Not_Implies1 | verit_rule_of "not_implies2" = Not_Implies2 | verit_rule_of "implies_neg1" = Implies_Neg1 | verit_rule_of "implies_neg2" = Implies_Neg2 | verit_rule_of "implies" = Implies | verit_rule_of "bfun_elim" = Bfun_Elim | verit_rule_of "ite1" = ITE1 | verit_rule_of "ite2" = ITE2 | verit_rule_of "not_ite1" = Not_ITE1 | verit_rule_of "not_ite2" = Not_ITE2 | verit_rule_of "ite_pos1" = ITE_Pos1 | verit_rule_of "ite_pos2" = ITE_Pos2 | verit_rule_of "ite_neg1" = ITE_Neg1 | verit_rule_of "ite_neg2" = ITE_Neg2 | verit_rule_of "la_disequality" = LA_Disequality | verit_rule_of "lia_generic" = LIA_Generic | verit_rule_of "la_generic" = LA_Generic | verit_rule_of "la_tautology" = LA_Tautology | verit_rule_of "la_totality" = LA_Totality | verit_rule_of "la_rw_eq"= LA_RW_Eq | verit_rule_of "nla_generic"= NLA_Generic | verit_rule_of "eq_transitive" = Eq_Transitive | verit_rule_of "qnt_rm_unused" = Qnt_Rm_Unused | verit_rule_of "onepoint" = Onepoint | verit_rule_of "qnt_join" = Qnt_Join | verit_rule_of "subproof" = Subproof | verit_rule_of "bool_simplify" = Bool_Simplify | verit_rule_of "or_simplify" = Or_Simplify | verit_rule_of "ite_simplify" = ITE_Simplify | verit_rule_of "and_simplify" = And_Simplify | verit_rule_of "not_simplify" = Not_Simplify | verit_rule_of "equiv_simplify" = Equiv_Simplify | verit_rule_of "eq_simplify" = Eq_Simplify | verit_rule_of "implies_simplify" = Implies_Simplify | verit_rule_of "connective_def" = Connective_Def | verit_rule_of "minus_simplify" = Minus_Simplify | verit_rule_of "sum_simplify" = Sum_Simplify | verit_rule_of "prod_simplify" = Prod_Simplify | verit_rule_of "comp_simplify" = Comp_Simplify | verit_rule_of "qnt_simplify" = Qnt_Simplify | verit_rule_of "tautology" = Tautological_Clause | verit_rule_of "qnt_cnf" = Qnt_CNF | verit_rule_of r = - if r = Verit_Proof.normalized_input_rule then Normalized_Input - else if r = Verit_Proof.local_input_rule then Local_Input - else if r = Verit_Proof.veriT_def then Definition - else if r = Verit_Proof.not_not_rule then Not_Not - else if r = Verit_Proof.contract_rule then Duplicate_Literals - else if r = Verit_Proof.ite_intro_rule then ITE_Intro - else if r = Verit_Proof.eq_congruent_rule then Eq_Congruent - else if r = Verit_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred - else if r = Verit_Proof.theory_resolution2_rule then Theory_Resolution2 - else if r = Verit_Proof.th_resolution_rule then Theory_Resolution - else if r = Verit_Proof.equiv_pos2_rule then Equiv_pos2 + if r = Lethe_Proof.normalized_input_rule then Normalized_Input + else if r = Lethe_Proof.local_input_rule then Local_Input + else if r = Lethe_Proof.lethe_def then Definition + else if r = Lethe_Proof.not_not_rule then Not_Not + else if r = Lethe_Proof.contract_rule then Duplicate_Literals + else if r = Lethe_Proof.ite_intro_rule then ITE_Intro + else if r = Lethe_Proof.eq_congruent_rule then Eq_Congruent + else if r = Lethe_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred + else if r = Lethe_Proof.theory_resolution2_rule then Theory_Resolution2 + else if r = Lethe_Proof.th_resolution_rule then Theory_Resolution + else if r = Lethe_Proof.equiv_pos2_rule then Equiv_pos2 else (@{print} ("Unsupport rule", r); Unsupported) -fun string_of_verit_rule Bind = "Bind" - | string_of_verit_rule Cong = "Cong" - | string_of_verit_rule Refl = "Refl" - | string_of_verit_rule Equiv1 = "Equiv1" - | string_of_verit_rule Equiv2 = "Equiv2" - | string_of_verit_rule Equiv_pos1 = "Equiv_pos1" - | string_of_verit_rule Equiv_pos2 = "Equiv_pos2" - | string_of_verit_rule Equiv_neg1 = "Equiv_neg1" - | string_of_verit_rule Equiv_neg2 = "Equiv_neg2" - | string_of_verit_rule Skolem_Forall = "Skolem_Forall" - | string_of_verit_rule Skolem_Ex = "Skolem_Ex" - | string_of_verit_rule Eq_Reflexive = "Eq_Reflexive" - | string_of_verit_rule Theory_Resolution = "Theory_Resolution" - | string_of_verit_rule Theory_Resolution2 = "Theory_Resolution2" - | string_of_verit_rule Forall_Inst = "forall_inst" - | string_of_verit_rule Or = "Or" - | string_of_verit_rule Not_Or = "Not_Or" - | string_of_verit_rule Resolution = "Resolution" - | string_of_verit_rule Eq_Congruent = "eq_congruent" - | string_of_verit_rule Trans = "trans" - | string_of_verit_rule False = "false" - | string_of_verit_rule And = "and" - | string_of_verit_rule And_Pos = "and_pos" - | string_of_verit_rule Not_And = "not_and" - | string_of_verit_rule And_Neg = "and_neg" - | string_of_verit_rule Or_Pos = "or_pos" - | string_of_verit_rule Or_Neg = "or_neg" - | string_of_verit_rule AC_Simp = "ac_simp" - | string_of_verit_rule Not_Equiv1 = "not_equiv1" - | string_of_verit_rule Not_Equiv2 = "not_equiv2" - | string_of_verit_rule Not_Implies1 = "not_implies1" - | string_of_verit_rule Not_Implies2 = "not_implies2" - | string_of_verit_rule Implies_Neg1 = "implies_neg1" - | string_of_verit_rule Implies_Neg2 = "implies_neg2" - | string_of_verit_rule Implies = "implies" - | string_of_verit_rule Bfun_Elim = "bfun_elim" - | string_of_verit_rule ITE1 = "ite1" - | string_of_verit_rule ITE2 = "ite2" - | string_of_verit_rule Not_ITE1 = "not_ite1" - | string_of_verit_rule Not_ITE2 = "not_ite2" - | string_of_verit_rule ITE_Pos1 = "ite_pos1" - | string_of_verit_rule ITE_Pos2 = "ite_pos2" - | string_of_verit_rule ITE_Neg1 = "ite_neg1" - | string_of_verit_rule ITE_Neg2 = "ite_neg2" - | string_of_verit_rule ITE_Intro = "ite_intro" - | string_of_verit_rule LA_Disequality = "la_disequality" - | string_of_verit_rule LA_Generic = "la_generic" - | string_of_verit_rule LIA_Generic = "lia_generic" - | string_of_verit_rule LA_Tautology = "la_tautology" - | string_of_verit_rule LA_RW_Eq = "la_rw_eq" - | string_of_verit_rule LA_Totality = "LA_Totality" - | string_of_verit_rule NLA_Generic = "nla_generic" - | string_of_verit_rule Eq_Transitive = "eq_transitive" - | string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused" - | string_of_verit_rule Onepoint = "onepoint" - | string_of_verit_rule Qnt_Join = "qnt_join" - | string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred" - | string_of_verit_rule Normalized_Input = Verit_Proof.normalized_input_rule - | string_of_verit_rule Local_Input = Verit_Proof.local_input_rule - | string_of_verit_rule Subproof = "subproof" - | string_of_verit_rule Bool_Simplify = "bool_simplify" - | string_of_verit_rule Equiv_Simplify = "equiv_simplify" - | string_of_verit_rule Eq_Simplify = "eq_simplify" - | string_of_verit_rule Not_Simplify = "not_simplify" - | string_of_verit_rule And_Simplify = "and_simplify" - | string_of_verit_rule Or_Simplify = "or_simplify" - | string_of_verit_rule ITE_Simplify = "ite_simplify" - | string_of_verit_rule Implies_Simplify = "implies_simplify" - | string_of_verit_rule Connective_Def = "connective_def" - | string_of_verit_rule Minus_Simplify = "minus_simplify" - | string_of_verit_rule Sum_Simplify = "sum_simplify" - | string_of_verit_rule Prod_Simplify = "prod_simplify" - | string_of_verit_rule Comp_Simplify = "comp_simplify" - | string_of_verit_rule Qnt_Simplify = "qnt_simplify" - | string_of_verit_rule Not_Not = Verit_Proof.not_not_rule - | string_of_verit_rule Tautological_Clause = "tautology" - | string_of_verit_rule Duplicate_Literals = Verit_Proof.contract_rule - | string_of_verit_rule Qnt_CNF = "qnt_cnf" - | string_of_verit_rule r = "Unknown rule: " ^ \<^make_string> r - -fun replay_error ctxt msg rule thms t = - SMT_Replay_Methods.replay_error ctxt msg (string_of_verit_rule rule) thms t - - -(* utility function *) - -fun eqsubst_all ctxt thms = - K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_asm_tac ctxt [0] thms)) - THEN' K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_tac ctxt [0] thms)) - -fun simplify_tac ctxt thms = - ctxt - |> empty_simpset - |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms) - |> Simplifier.asm_full_simp_tac - -(* sko_forall requires the assumptions to be able to prove the equivalence in case of double -skolemization. See comment below. *) -fun requires_subproof_assms _ t = - member (op =) ["refl", "sko_forall", "sko_ex", "cong"] t - -fun requires_local_input _ t = - member (op =) [Verit_Proof.local_input_rule] t - -(*This is a weaker simplification form. It is weaker, but is also less likely to loop*) -fun partial_simplify_tac ctxt thms = - ctxt - |> empty_simpset - |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms) - |> Simplifier.full_simp_tac - -val try_provers = SMT_Replay_Methods.try_provers "verit" - -fun TRY' tac = fn i => TRY (tac i) -fun REPEAT' tac = fn i => REPEAT (tac i) -fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i)) - - -(* Bind *) - -(*The bind rule is non-obvious due to the handling of quantifiers: - "\x y a. x = y ==> (\b. P a b x) \ (\b. P' a b y)" - ------------------------------------------------------ - \a. (\b x. P a b x) \ (\b y. P' a b y) -is a valid application.*) - -val bind_thms = - [@{lemma \(\x x'. x = x' \ P x = Q x') \ (\x. P x) = (\y. Q y)\ by blast}, - @{lemma \(\x x'. x = x' \ P x = Q x') \ (\x. P x) = (\y. Q y)\ by blast}, - @{lemma \(\x x'. x = x' \ P x = Q x') \ (\x. P x = Q x)\ by blast}, - @{lemma \(\x x'. x = x' \ P x = Q x') \ (\x. P x = Q x)\ by blast}] - -val bind_thms_same_name = - [@{lemma \(\x. P x = Q x) \ (\x. P x) = (\y. Q y)\ by blast}, - @{lemma \(\x. P x = Q x) \ (\x. P x) = (\y. Q y)\ by blast}, - @{lemma \(\x. P x = Q x) \ (\x. P x = Q x)\ by blast}, - @{lemma \(\x. P x = Q x) \ (\x. P x = Q x)\ by blast}] - -fun extract_quantified_names_q (_ $ Abs (name, _, t)) = - apfst (curry (op ::) name) (extract_quantified_names_q t) - | extract_quantified_names_q t = ([], t) - -fun extract_forall_quantified_names_q (Const(\<^const_name>\HOL.All\, _) $ Abs (name, ty, t)) = - (name, ty) :: (extract_forall_quantified_names_q t) - | extract_forall_quantified_names_q _ = [] - -fun extract_all_forall_quantified_names_q (Const(\<^const_name>\HOL.All\, _) $ Abs (name, _, t)) = - name :: (extract_all_forall_quantified_names_q t) - | extract_all_forall_quantified_names_q (t $ u) = - extract_all_forall_quantified_names_q t @ extract_all_forall_quantified_names_q u - | extract_all_forall_quantified_names_q _ = [] - -val extract_quantified_names_ba = - SMT_Replay_Methods.dest_prop - #> extract_quantified_names_q - ##> HOLogic.dest_eq - ##> fst - ##> extract_quantified_names_q - ##> fst - -val extract_quantified_names = - extract_quantified_names_ba - #> (op @) - -val extract_all_forall_quantified_names = - SMT_Replay_Methods.dest_prop - #> HOLogic.dest_eq - #> fst - #> extract_all_forall_quantified_names_q - - -fun extract_all_exists_quantified_names_q (Const(\<^const_name>\HOL.Ex\, _) $ Abs (name, _, t)) = - name :: (extract_all_exists_quantified_names_q t) - | extract_all_exists_quantified_names_q (t $ u) = - extract_all_exists_quantified_names_q t @ extract_all_exists_quantified_names_q u - | extract_all_exists_quantified_names_q _ = [] - -val extract_all_exists_quantified_names = - SMT_Replay_Methods.dest_prop - #> HOLogic.dest_eq - #> fst - #> extract_all_exists_quantified_names_q - - -val extract_bind_names = - HOLogic.dest_eq - #> apply2 (fn (Free (name, _)) => name) - -fun combine_quant ctxt ((n1, n2) :: bounds) (n1' :: formula) = - TRY' (if n1 = n1' - then if n1 <> n2 - then - resolve_tac ctxt bind_thms - THEN' TRY'(resolve_tac ctxt [@{thm refl}]) - THEN' combine_quant ctxt bounds formula - else resolve_tac ctxt bind_thms_same_name THEN' combine_quant ctxt bounds formula - else resolve_tac ctxt @{thms allI} THEN' combine_quant ctxt ((n1, n2) :: bounds) formula) - | combine_quant _ _ _ = K all_tac - -fun bind_quants ctxt args t = - combine_quant ctxt (map extract_bind_names args) (extract_quantified_names t) - -fun generalize_prems_q [] prems = prems - | generalize_prems_q (_ :: quants) prems = - generalize_prems_q quants (@{thm spec} OF [prems]) - -fun generalize_prems t = generalize_prems_q (fst (extract_quantified_names_ba t)) - -fun bind ctxt [prems] args t = - SMT_Replay_Methods.prove ctxt t (fn _ => - bind_quants ctxt args t - THEN' TRY' (SOLVED' (resolve_tac ctxt [generalize_prems t prems] - THEN_ALL_NEW TRY' (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms refl})))) - | bind ctxt thms _ t = replay_error ctxt "invalid bind application" Bind thms t - - -(* Congruence/Refl *) - -fun cong ctxt thms = try_provers ctxt - (string_of_verit_rule Cong) [ - ("basic", SMT_Replay_Methods.cong_basic ctxt thms), - ("unfolding then reflexivity", SMT_Replay_Methods.cong_unfolding_trivial ctxt thms), - ("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms), - ("full", SMT_Replay_Methods.cong_full ctxt thms)] thms - -fun refl ctxt thm t = - (case find_first (fn thm => t = Thm.full_prop_of thm) thm of - SOME thm => thm - | NONE => - (case try (fn t => SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}) t of - NONE => cong ctxt thm t - | SOME thm => thm)) - - -(* Instantiation *) - -local -fun dropWhile _ [] = [] - | dropWhile f (x :: xs) = if f x then dropWhile f xs else x :: xs -in - -fun forall_inst ctxt _ _ insts t = - let - fun instantiate_and_solve i ({context = ctxt, prems = [prem], ...}: Subgoal.focus) = - let - val t = Thm.prop_of prem - val quants = t - |> SMT_Replay_Methods.dest_prop - |> extract_forall_quantified_names_q - val insts = map (Symtab.lookup insts o fst) (rev quants) - |> dropWhile (curry (op =) NONE) - |> rev - fun option_map _ NONE = NONE - | option_map f (SOME a) = SOME (f a) - fun instantiate_with inst prem = - Drule.infer_instantiate' ctxt [NONE, inst] @{thm spec} OF [prem] - val inst_thm = - fold instantiate_with - (map (option_map (Thm.cterm_of ctxt)) insts) - prem - in - (Method.insert_tac ctxt [inst_thm] - THEN' TRY' (fn i => assume_tac ctxt i) - THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute})) i - end - | instantiate_and_solve _ ({context = ctxt, prems = thms, ...}: Subgoal.focus) = - replay_error ctxt "invalid application" Forall_Inst thms t - in - SMT_Replay_Methods.prove ctxt t (fn _ => - match_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]] - THEN' (fn i => Subgoal.FOCUS (instantiate_and_solve i) ctxt i)) - end -end - - -(* Or *) - -fun or _ (thm :: _) _ = thm - | or ctxt thms t = replay_error ctxt "invalid bind application" Or thms t - - -(* Implication *) - -val implies_pos_thm = - [@{lemma \\(A \ B) \ \A \ B\ by blast}, - @{lemma \\(\A \ B) \ A \ B\ by blast}] - -fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => - resolve_tac ctxt implies_pos_thm) - -fun extract_rewrite_rule_assumption _ thms = - let - fun is_rewrite_rule thm = - (case Thm.prop_of thm of - \<^term>\Trueprop\ $ (Const(\<^const_name>\HOL.eq\, _) $ _ $ Free(_, _)) => true - | _ => false) - fun is_context_rule thm = - (case Thm.prop_of thm of - \<^term>\Trueprop\ $ (Const(\<^const_name>\HOL.eq\, _) $ Free(_, _) $ Free(_, _)) => true - | _ => false) - val ctxt_eq = - thms - |> filter is_context_rule - val rew = - thms - |> filter_out is_context_rule - |> filter is_rewrite_rule - in - (ctxt_eq, rew) - end - -local - fun rewrite_all_skolems thm_indirect ctxt (SOME thm :: thms) = - EqSubst.eqsubst_tac ctxt [0] [thm_indirect OF [thm]] - THEN' (partial_simplify_tac ctxt (@{thms eq_commute})) - THEN' rewrite_all_skolems thm_indirect ctxt thms - | rewrite_all_skolems thm_indirect ctxt (NONE :: thms) = rewrite_all_skolems thm_indirect ctxt thms - | rewrite_all_skolems _ _ [] = K (all_tac) - - fun extract_var_name (thm :: thms) = - let val name = Thm.concl_of thm - |> SMT_Replay_Methods.dest_prop - |> HOLogic.dest_eq - |> fst - |> (fn Const(_,_) $ Abs(name, _, _) => [(name,@{thm sym} OF [thm])] - | _ => []) - in name :: extract_var_name thms end - | extract_var_name [] = [] - -fun skolem_tac extractor thm1 thm2 ctxt thms t = - let - val (ctxt_eq, ts) = extract_rewrite_rule_assumption ctxt thms - fun ordered_definitions () = - let - val var_order = extractor t - val thm_names_with_var = extract_var_name ts |> flat - in map (AList.lookup (op =) thm_names_with_var) var_order end - - in - SMT_Replay_Methods.prove ctxt t (fn _ => - K (unfold_tac ctxt ctxt_eq) - THEN' ((SOLVED' (K (unfold_tac ctxt (map (fn thm => thm1 OF [@{thm sym} OF [thm]]) ts)))) - ORELSE' - (rewrite_all_skolems thm2 ctxt (ordered_definitions ()) - THEN' partial_simplify_tac ctxt @{thms eq_commute}))) - end -in - -val skolem_forall = - skolem_tac extract_all_forall_quantified_names @{thm verit_sko_forall_indirect} - @{thm verit_sko_forall_indirect2} - -val skolem_ex = - skolem_tac extract_all_exists_quantified_names @{thm verit_sko_ex_indirect} - @{thm verit_sko_ex_indirect2} - -end - -fun eq_reflexive ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm refl} - -local - fun not_not_prove ctxt _ = - K (unfold_tac ctxt @{thms not_not}) - THEN' match_tac ctxt @{thms verit_or_simplify_1} - - fun duplicate_literals_prove ctxt prems = - Method.insert_tac ctxt prems - THEN' match_tac ctxt @{thms ccontr} - THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not}) - THEN' TRY o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE}) - THEN' CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms disjE}) - THEN' REPEAT' (ematch_tac ctxt @{thms notE} THEN' TRY' (assume_tac ctxt)) - - fun tautological_clause_prove ctxt _ = - match_tac ctxt @{thms verit_or_neg} - THEN' K (unfold_tac ctxt @{thms not_not disj_assoc[symmetric]}) - THEN' TRY' (match_tac ctxt @{thms notE} THEN_ALL_NEW assume_tac ctxt) - - val theory_resolution2_lemma = @{lemma \a \ a = b \ b\ by blast} -in - -fun prove_abstract abstracter tac ctxt thms t = - let - val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms - val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t)) - val (_, t2) = Logic.dest_equals (Thm.prop_of t') - val thm = - SMT_Replay_Methods.prove_abstract ctxt thms t2 tac ( - fold_map (abstracter o SMT_Replay_Methods.dest_thm) thms ##>> - abstracter (SMT_Replay_Methods.dest_prop t2)) - in - @{thm verit_Pure_trans} OF [t', thm] - end - -val not_not = prove_abstract SMT_Replay_Methods.abstract_bool_shallow not_not_prove - -val tautological_clause = - prove_abstract SMT_Replay_Methods.abstract_bool_shallow tautological_clause_prove - -val duplicate_literals = - prove_abstract SMT_Replay_Methods.abstract_bool_shallow duplicate_literals_prove - -val unit_res = prove_abstract SMT_Replay_Methods.abstract_bool_shallow SMT_Replay_Methods.prop_tac - -(*match_instantiate does not work*) -fun theory_resolution2 ctxt prems t = - SMT_Replay_Methods.prove ctxt t (fn _ => match_tac ctxt [theory_resolution2_lemma OF prems]) - -end - - -fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => - Method.insert_tac ctxt prems - THEN' TRY' (K (unfold_tac ctxt @{thms SMT.trigger_def})) - THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute})) - -val false_rule_thm = @{lemma \\False\ by blast} - -fun false_rule ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t false_rule_thm - - -(* Transitivity *) - -val trans_bool_thm = - @{lemma \P = Q \ Q \ P\ by blast} - -fun trans ctxt thms t = - let - val prop_of = HOLogic.dest_Trueprop o Thm.full_prop_of - fun combine_thms [thm1, thm2] = - (case (prop_of thm1, prop_of thm2) of - ((Const(\<^const_name>\HOL.eq\, _) $ t1 $ t2), - (Const(\<^const_name>\HOL.eq\, _) $ t3 $ t4)) => - if t2 aconv t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans})) - else if t2 aconv t4 then thm1 RSN ((1, ((thm2 RS sym)) RSN (2, @{thm trans}))) - else if t1 aconv t4 then thm2 RSN (1, thm1 RSN (2, @{thm trans})) - else raise Fail "invalid trans theorem" - | _ => trans_bool_thm OF [thm1, thm2]) - | combine_thms (thm1 :: thm2 :: thms) = - combine_thms (combine_thms [thm1, thm2] :: thms) - | combine_thms thms = replay_error ctxt "invalid bind application" Trans thms t - val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t)) - val (_, t2) = Logic.dest_equals (Thm.prop_of t') - val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms - val trans_thm = combine_thms thms - in - (case (prop_of trans_thm, t2) of - ((Const(\<^const_name>\HOL.eq\, _) $ t1 $ _), - (Const(\<^const_name>\HOL.eq\, _) $ t3 $ _)) => - if t1 aconv t3 then trans_thm else trans_thm RS sym - | _ => trans_thm (*to be on the safe side*)) - end - - -fun tmp_AC_rule ctxt thms t = - SMT_Replay_Methods.prove ctxt t (fn _ => - Method.insert_tac ctxt thms - THEN' REPEAT_ALL_NEW (partial_simplify_tac ctxt @{thms eq_commute} - THEN' TRY' (simplify_tac ctxt @{thms ac_simps conj_ac}) - THEN' TRY' (Classical.fast_tac ctxt))) - - -(* And/Or *) - -local - fun not_and_rule_prove ctxt prems = - Method.insert_tac ctxt prems - THEN' K (unfold_tac ctxt @{thms de_Morgan_conj}) - THEN_ALL_NEW TRY' (assume_tac ctxt) - - fun or_pos_prove ctxt _ = - K (unfold_tac ctxt @{thms de_Morgan_disj not_not}) - THEN' match_tac ctxt @{thms verit_and_pos} - THEN' K (unfold_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not}) - THEN' TRY' (assume_tac ctxt) - - fun not_or_rule_prove ctxt prems = - Method.insert_tac ctxt prems - THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not}) - THEN' TRY' (REPEAT' (match_tac ctxt @{thms conjI})) - THEN_ALL_NEW ((REPEAT' (ematch_tac ctxt @{thms conjE})) - THEN' TRY' (assume_tac ctxt)) - - fun and_rule_prove ctxt prems = - Method.insert_tac ctxt prems - THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1))) - THEN' TRY' (assume_tac ctxt) - - fun and_neg_rule_prove ctxt _ = - match_tac ctxt @{thms verit_and_neg} - THEN' K (unfold_tac ctxt @{thms de_Morgan_conj not_not}) - THEN' TRY' (assume_tac ctxt) - - fun prover tac = prove_abstract SMT_Replay_Methods.abstract_prop tac - -in - -val and_rule = prover and_rule_prove - -val not_and_rule = prover not_and_rule_prove - -val not_or_rule = prover not_or_rule_prove - -val or_pos_rule = prover or_pos_prove - -val and_neg_rule = prover and_neg_rule_prove - -val or_neg_rule = prove_abstract SMT_Replay_Methods.abstract_bool (fn ctxt => fn _ => - resolve_tac ctxt @{thms verit_or_neg} - THEN' K (unfold_tac ctxt @{thms not_not}) - THEN_ALL_NEW - (REPEAT' - (SOLVED' (match_tac ctxt @{thms disjI1} THEN_ALL_NEW assume_tac ctxt) - ORELSE' (match_tac ctxt @{thms disjI2} THEN' TRY' (assume_tac ctxt))))) - -fun and_pos ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos}) - THEN' TRY' (assume_tac ctxt)) - -end - - -(* Equivalence Transformation *) - -local - fun prove_equiv equiv_thm ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => - Method.insert_tac ctxt [equiv_thm OF [thm]] - THEN' TRY' (assume_tac ctxt)) - | prove_equiv _ ctxt thms t = replay_error ctxt "invalid application in some equiv rule" Unsupported thms t -in - -val not_equiv1 = prove_equiv @{lemma \\(A \ B) \ A \ B\ by blast} -val not_equiv2 = prove_equiv @{lemma \\(A \ B) \ \A \ \B\ by blast} -val equiv1 = prove_equiv @{lemma \(A \ B) \ \A \ B\ by blast} -val equiv2 = prove_equiv @{lemma \(A \ B) \ A \ \B\ by blast} -val not_implies1 = prove_equiv @{lemma \\(A \ B) \ A\ by blast} -val not_implies2 = prove_equiv @{lemma \\(A \B) \ \B\ by blast} - -end - - -(* Equivalence Lemma *) -(*equiv_pos2 is very important for performance. We have tried various tactics, including -a specialisation of SMT_Replay_Methods.match_instantiate, but there never was a measurable -and consistent gain.*) -local - fun prove_equiv_pos_neg2 thm ctxt _ t = - SMT_Replay_Methods.match_instantiate ctxt t thm -in - -val equiv_pos1_thm = @{lemma \\(a \ b) \ a \ \b\ by blast+} -val equiv_pos1 = prove_equiv_pos_neg2 equiv_pos1_thm - -val equiv_pos2_thm = @{lemma \\a b. (a \ b) \ \a \ b\ by blast+} -val equiv_pos2 = prove_equiv_pos_neg2 equiv_pos2_thm - -val equiv_neg1_thm = @{lemma \(a \ b) \ \a \ \b\ by blast+} -val equiv_neg1 = prove_equiv_pos_neg2 equiv_neg1_thm - -val equiv_neg2_thm = @{lemma \(a \ b) \ a \ b\ by blast} -val equiv_neg2 = prove_equiv_pos_neg2 equiv_neg2_thm - -end - - -local - fun implies_pos_neg_term ctxt thm (\<^term>\Trueprop\ $ - (\<^term>\HOL.disj\ $ (\<^term>\HOL.implies\ $ a $ b) $ _)) = - Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm - | implies_pos_neg_term ctxt thm t = - replay_error ctxt "invalid application in Implies" Unsupported [thm] t - - fun prove_implies_pos_neg thm ctxt _ t = - let val thm = implies_pos_neg_term ctxt thm t - in - SMT_Replay_Methods.prove ctxt t (fn _ => - Method.insert_tac ctxt [thm] - THEN' TRY' (assume_tac ctxt)) - end -in - -val implies_neg1_thm = @{lemma \(a \ b) \ a\ by blast} -val implies_neg1 = prove_implies_pos_neg implies_neg1_thm - -val implies_neg2_thm = @{lemma \(a \ b) \ \b\ by blast} -val implies_neg2 = prove_implies_pos_neg implies_neg2_thm - -val implies_thm = @{lemma \(a \ b) \ \a \ b\ by blast} -fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => - Method.insert_tac ctxt [implies_thm OF prems] - THEN' TRY' (assume_tac ctxt)) - -end - - -(* BFun *) - -local - val bfun_theorems = @{thms verit_bfun_elim} -in - -fun bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => - Method.insert_tac ctxt prems - THEN' TRY' (eqsubst_all ctxt bfun_theorems) - THEN' TRY' (simplify_tac ctxt @{thms eq_commute all_conj_distrib ex_disj_distrib})) - -end - - -(* If-Then-Else *) - -local - fun prove_ite ite_thm thm ctxt = - resolve_tac ctxt [ite_thm OF [thm]] - THEN' K (unfold_tac ctxt @{thms not_not}) - THEN' TRY' (assume_tac ctxt) -in - -val ite_pos1_thm = - @{lemma \\(if x then P else Q) \ x \ Q\ by auto} - -fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => - resolve_tac ctxt [ite_pos1_thm]) - -val ite_pos2_thms = - @{lemma \\(if x then P else Q) \ \x \ P\ \\(if \x then P else Q) \ x \ P\ by auto} - -fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_pos2_thms) - -val ite_neg1_thms = - @{lemma \(if x then P else Q) \ x \ \Q\ \(if x then P else \Q) \ x \ Q\ by auto} - -fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg1_thms) - -val ite_neg2_thms = - @{lemma \(if x then P else Q) \ \x \ \P\ \(if \x then P else Q) \ x \ \P\ - \(if x then \P else Q) \ \x \ P\ \(if \x then \P else Q) \ x \ P\ - by auto} - -fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg2_thms) - -val ite1_thm = - @{lemma \(if x then P else Q) \ x \ Q\ by (auto split: if_splits) } - -fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite1_thm thm ctxt) - -val ite2_thm = - @{lemma \(if x then P else Q) \ \x \ P\ by (auto split: if_splits) } - -fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite2_thm thm ctxt) - -val not_ite1_thm = - @{lemma \\(if x then P else Q) \ x \ \Q\ by (auto split: if_splits) } - -fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite1_thm thm ctxt) - -val not_ite2_thm = - @{lemma \\(if x then P else Q) \ \x \ \P\ by (auto split: if_splits) } - -fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite2_thm thm ctxt) - -(*ite_intro can introduce new terms that are in the proof exactly the sames as the old one, but are -not internally, hence the possible reordering.*) -fun ite_intro ctxt _ t = - let - fun simplify_ite ctxt thms = - ctxt - |> empty_simpset - |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps thms @ @{thms if_True if_False refl simp_thms if_cancel}) - |> Raw_Simplifier.add_eqcong @{thm verit_ite_if_cong} - |> Simplifier.full_simp_tac - in - SMT_Replay_Methods.prove ctxt t (fn _ => simplify_ite ctxt [] - THEN' TRY' (simplify_ite ctxt @{thms eq_commute})) - end -end - - -(* Quantifiers *) - -local - val rm_unused = @{lemma \(\x. P) = P\ \(\x. P) = P\ by blast+} - - fun qnt_cnf_tac ctxt = - simplify_tac ctxt @{thms de_Morgan_conj de_Morgan_disj imp_conv_disj - iff_conv_conj_imp if_bool_eq_disj ex_simps all_simps ex_disj_distrib - verit_connective_def(3) all_conj_distrib} - THEN' TRY' (Blast.blast_tac ctxt) -in -fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => - K (unfold_tac ctxt rm_unused)) - -fun onepoint ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => - Method.insert_tac ctxt prems - THEN' Simplifier.full_simp_tac (put_simpset HOL_basic_ss (empty_simpset ctxt) - addsimps @{thms HOL.simp_thms HOL.all_simps} - addsimprocs [@{simproc HOL.defined_All}, @{simproc HOL.defined_Ex}]) - THEN' TRY' (Blast.blast_tac ctxt) - THEN' TRY' (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt [])) - -fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t Classical.fast_tac - -fun qnt_cnf ctxt _ t = SMT_Replay_Methods.prove ctxt t qnt_cnf_tac - -fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => - partial_simplify_tac ctxt []) - -end - -(* Equality *) - -fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => - REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}]) - THEN' REPEAT' (resolve_tac ctxt @{thms impI}) - THEN' REPEAT' (eresolve_tac ctxt @{thms conjI}) - THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1)) - THEN' resolve_tac ctxt @{thms refl}) - -local - fun find_rew rews t t' = - (case AList.lookup (op =) rews (t, t') of - SOME thm => SOME (thm COMP @{thm symmetric}) - | NONE => - (case AList.lookup (op =) rews (t', t) of - SOME thm => SOME thm - | NONE => NONE)) - - fun eq_pred_conv rews t ctxt ctrm = - (case find_rew rews t (Thm.term_of ctrm) of - SOME thm => Conv.rewr_conv thm ctrm - | NONE => - (case t of - f $ arg => - (Conv.fun_conv (eq_pred_conv rews f ctxt) then_conv - Conv.arg_conv (eq_pred_conv rews arg ctxt)) ctrm - | Abs (_, _, f) => Conv.abs_conv (eq_pred_conv rews f o snd) ctxt ctrm - | _ => Conv.all_conv ctrm)) - - fun eq_pred_rewrite_tac ({context = ctxt, prems, concl, ...}: Subgoal.focus) = - let - val rews = prems - |> map_filter (try (apfst (HOLogic.dest_eq o Thm.term_of o Object_Logic.dest_judgment ctxt o - Thm.cconcl_of) o `(fn x => x))) - |> map (apsnd (fn x => @{thm eq_reflection} OF [x])) - fun conv_left conv = Conv.arg_conv (Conv.arg_conv conv) - fun conv_left_neg conv = Conv.arg_conv (Conv.arg_conv (Conv.arg_conv conv)) - val (t1, conv_term) = - (case Thm.term_of (Object_Logic.dest_judgment ctxt concl) of - Const(_, _) $ (Const(\<^const_name>\HOL.Not\, _) $ t1) $ _ => (t1, conv_left) - | Const(_, _) $ t1 $ (Const(\<^const_name>\HOL.Not\, _) $ _) => (t1, conv_left_neg) - | Const(_, _) $ t1 $ _ => (t1, conv_left) - | t1 => (t1, conv_left)) - - fun throwing_CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st) - in - throwing_CONVERSION (conv_term (eq_pred_conv rews t1 ctxt)) - end -in - -fun eq_congruent_pred ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \_ = _\]} RSN (1, @{thm iffD2}) OF @{thms impI}]) - THEN' (fn i => Subgoal.FOCUS (fn focus => eq_pred_rewrite_tac focus i) ctxt i) - THEN' (resolve_tac ctxt @{thms refl excluded_middle excluded_middle[of \\_\, unfolded not_not]} - ORELSE' assume_tac ctxt)) - -val eq_congruent = eq_congruent_pred - -end - - -(* Subproof *) - -fun subproof ctxt [prem] t = - SMT_Replay_Methods.prove ctxt t (fn _ => - (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}], - @{thm disj_not1[of \\_\, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]] - THEN' resolve_tac ctxt [prem] - THEN_ALL_NEW assume_tac ctxt - THEN' TRY' (assume_tac ctxt)) - ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt)) - | subproof ctxt prems t = - replay_error ctxt "invalid application, only one assumption expected" Subproof prems t - - -(* Simplifying Steps *) - -(* The reconstruction is a bit tricky: At first we only rewrite only based on the rules that are -passed as argument. Then we simply use simp_thms to reconstruct all the proofs (and these theorems -cover all the simplification below). -*) -local - fun rewrite_only_thms ctxt thms = - ctxt - |> empty_simpset - |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps thms) - |> Simplifier.full_simp_tac - fun rewrite_thms ctxt thms = - ctxt - |> empty_simpset - |> put_simpset HOL_basic_ss - |> Raw_Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]} - |> (fn ctxt => ctxt addsimps thms addsimps @{thms simp_thms}) - |> Simplifier.full_simp_tac - - fun chain_rewrite_thms ctxt thms = - TRY' (rewrite_only_thms ctxt thms) - THEN' TRY' (rewrite_thms ctxt thms) - - fun chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2 = - TRY' (rewrite_only_thms ctxt thms1) - THEN' TRY' (rewrite_thms ctxt thms2) - - fun chain_rewrite_thms_two_step ctxt thms1 thms2 thms3 thms4 = - chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2 - THEN' TRY' (chain_rewrite_two_step_with_ac_simps ctxt thms3 thms4) - - val imp_refl = @{lemma \(P \ P) = True\ by blast} - -in -fun rewrite_bool_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - (chain_rewrite_thms ctxt @{thms verit_bool_simplify})) - -fun rewrite_and_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_and_simplify verit_and_simplify1} - @{thms verit_and_simplify})) - -fun rewrite_or_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_or_simplify verit_or_simplify_1} - @{thms verit_or_simplify}) - THEN' TRY' (REPEAT' (match_tac ctxt @{thms verit_and_pos}) THEN' assume_tac ctxt)) - -fun rewrite_not_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - (rewrite_only_thms ctxt @{thms verit_not_simplify})) - -fun rewrite_equiv_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - (rewrite_only_thms ctxt @{thms verit_equiv_simplify})) - -fun rewrite_eq_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - (chain_rewrite_two_step_with_ac_simps ctxt - @{thms verit_eq_simplify} - (Named_Theorems.get ctxt @{named_theorems ac_simps}))) - -fun rewrite_implies_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - (rewrite_only_thms ctxt @{thms verit_implies_simplify})) - -(* It is more efficient to first fold the implication symbols. - That is however not enough when symbols appears within - expressions, hence we also unfold implications in the - other direction. *) -fun rewrite_connective_def ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - chain_rewrite_thms_two_step ctxt - (imp_refl :: @{thms not_not verit_connective_def[symmetric]}) - (@{thms verit_connective_def[symmetric]}) - (imp_refl :: @{thms not_not verit_connective_def}) - (@{thms verit_connective_def})) - -fun rewrite_minus_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - chain_rewrite_two_step_with_ac_simps ctxt - @{thms arith_simps verit_minus_simplify} - (Named_Theorems.get ctxt @{named_theorems ac_simps} @ - @{thms numerals arith_simps arith_special - numeral_class.numeral.numeral_One})) - -fun rewrite_comp_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - chain_rewrite_thms ctxt @{thms verit_comp_simplify}) - -fun rewrite_ite_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - (rewrite_only_thms ctxt @{thms verit_ite_simplify})) -end - - -(* Simplifications *) - -local - fun simplify_arith ctxt thms = partial_simplify_tac ctxt - (thms @ Named_Theorems.get ctxt @{named_theorems ac_simps} @ @{thms arith_simps}) -in - -fun sum_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - simplify_arith ctxt @{thms verit_sum_simplify arith_special}) - -fun prod_simplify ctxt _ t = - SMT_Replay_Methods.prove ctxt t (fn _ => - simplify_arith ctxt @{thms verit_prod_simplify}) - -end - - -(* Arithmetics *) -local - -val la_rw_eq_thm = @{lemma \(a :: nat) = b \ (a \ b) \ (a \ b)\ by auto} -in -fun la_rw_eq ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t la_rw_eq_thm - -fun la_generic_prove args ctxt _ = SMT_Replay_Arith.la_farkas args ctxt - -fun la_generic ctxt _ args = - prove_abstract (SMT_Replay_Methods.abstract_arith_shallow ctxt) (la_generic_prove args) ctxt [] - -fun lia_generic ctxt _ t = - SMT_Replay_Methods.prove_arith_rewrite SMT_Replay_Methods.abstract_neq ctxt t - -fun la_disequality ctxt _ t = - SMT_Replay_Methods.match_instantiate ctxt t @{thm verit_la_disequality} - -end (* Combining all together *) fun unsupported rule ctxt thms _ _ _ = SMT_Replay_Methods.replay_error ctxt "Unsupported verit rule" rule thms fun ignore_args f ctxt thm _ _ _ t = f ctxt thm t fun ignore_decls f ctxt thm args insts _ t = f ctxt thm args insts t fun ignore_insts f ctxt thm args _ _ t = f ctxt thm args t fun choose And = ignore_args and_rule | choose And_Neg = ignore_args and_neg_rule | choose And_Pos = ignore_args and_pos | choose And_Simplify = ignore_args rewrite_and_simplify | choose Bind = ignore_insts bind | choose Bool_Simplify = ignore_args rewrite_bool_simplify | choose Comp_Simplify = ignore_args rewrite_comp_simplify | choose Cong = ignore_args cong | choose Connective_Def = ignore_args rewrite_connective_def | choose Duplicate_Literals = ignore_args duplicate_literals | choose Eq_Congruent = ignore_args eq_congruent | choose Eq_Congruent_Pred = ignore_args eq_congruent_pred | choose Eq_Reflexive = ignore_args eq_reflexive | choose Eq_Simplify = ignore_args rewrite_eq_simplify | choose Eq_Transitive = ignore_args eq_transitive | choose Equiv1 = ignore_args equiv1 | choose Equiv2 = ignore_args equiv2 | choose Equiv_neg1 = ignore_args equiv_neg1 | choose Equiv_neg2 = ignore_args equiv_neg2 | choose Equiv_pos1 = ignore_args equiv_pos1 | choose Equiv_pos2 = ignore_args equiv_pos2 | choose Equiv_Simplify = ignore_args rewrite_equiv_simplify | choose False = ignore_args false_rule | choose Forall_Inst = ignore_decls forall_inst | choose Implies = ignore_args implies_rules | choose Implies_Neg1 = ignore_args implies_neg1 | choose Implies_Neg2 = ignore_args implies_neg2 | choose Implies_Pos = ignore_args implies_pos | choose Implies_Simplify = ignore_args rewrite_implies_simplify | choose ITE1 = ignore_args ite1 | choose ITE2 = ignore_args ite2 | choose ITE_Intro = ignore_args ite_intro | choose ITE_Neg1 = ignore_args ite_neg1 | choose ITE_Neg2 = ignore_args ite_neg2 | choose ITE_Pos1 = ignore_args ite_pos1 | choose ITE_Pos2 = ignore_args ite_pos2 | choose ITE_Simplify = ignore_args rewrite_ite_simplify | choose LA_Disequality = ignore_args la_disequality | choose LA_Generic = ignore_insts la_generic | choose LA_RW_Eq = ignore_args la_rw_eq | choose LA_Tautology = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow | choose LA_Totality = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow | choose LIA_Generic = ignore_args lia_generic | choose Local_Input = ignore_args refl | choose Minus_Simplify = ignore_args rewrite_minus_simplify | choose NLA_Generic = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow | choose Normalized_Input = ignore_args normalized_input | choose Not_And = ignore_args not_and_rule | choose Not_Equiv1 = ignore_args not_equiv1 | choose Not_Equiv2 = ignore_args not_equiv2 | choose Not_Implies1 = ignore_args not_implies1 | choose Not_Implies2 = ignore_args not_implies2 | choose Not_ITE1 = ignore_args not_ite1 | choose Not_ITE2 = ignore_args not_ite2 | choose Not_Not = ignore_args not_not | choose Not_Or = ignore_args not_or_rule | choose Not_Simplify = ignore_args rewrite_not_simplify | choose Or = ignore_args or | choose Or_Neg = ignore_args or_neg_rule | choose Or_Pos = ignore_args or_pos_rule | choose Or_Simplify = ignore_args rewrite_or_simplify | choose Theory_Resolution2 = ignore_args theory_resolution2 | choose Prod_Simplify = ignore_args prod_simplify | choose Qnt_Join = ignore_args qnt_join | choose Qnt_Rm_Unused = ignore_args qnt_rm_unused | choose Onepoint = ignore_args onepoint | choose Qnt_Simplify = ignore_args qnt_simplify | choose Refl = ignore_args refl | choose Resolution = ignore_args unit_res | choose Skolem_Ex = ignore_args skolem_ex | choose Skolem_Forall = ignore_args skolem_forall | choose Subproof = ignore_args subproof | choose Sum_Simplify = ignore_args sum_simplify | choose Tautological_Clause = ignore_args tautological_clause | choose Theory_Resolution = ignore_args unit_res | choose AC_Simp = ignore_args tmp_AC_rule | choose Bfun_Elim = ignore_args bfun_elim | choose Qnt_CNF = ignore_args qnt_cnf | choose Trans = ignore_args trans | choose r = unsupported (string_of_verit_rule r) type verit_method = Proof.context -> thm list -> term -> thm type abs_context = int * term Termtab.table fun with_tracing rule method ctxt thms args insts decls t = let val _ = SMT_Replay_Methods.trace_goal ctxt rule thms t in method ctxt thms args insts decls t end fun method_for rule = with_tracing rule (choose (verit_rule_of rule)) fun discharge ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt [thm] THEN_ALL_NEW (resolve_tac ctxt @{thms refl})) end;