--- a/src/HOL/SMT.thy Mon Oct 12 17:42:15 2020 +0200
+++ b/src/HOL/SMT.thy Mon Oct 12 18:59:44 2020 +0200
@@ -6,7 +6,7 @@
section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
theory SMT
- imports Divides
+ imports Divides Numeral_Simprocs
keywords "smt_status" :: diag
begin
@@ -199,10 +199,18 @@
lemma verit_sko_forall': \<open>P (SOME x. \<not>P x) = A \<Longrightarrow> (\<forall>x. P x) = A\<close>
by (subst verit_sko_forall)
+lemma verit_sko_forall'': \<open>B = A \<Longrightarrow> (SOME x. P x) = A \<equiv> (SOME x. P x) = B\<close>
+ by auto
+
lemma verit_sko_forall_indirect: \<open>x = (SOME x. \<not>P x) \<Longrightarrow> (\<forall>x. P x) \<longleftrightarrow> P x\<close>
using someI[of \<open>\<lambda>x. \<not>P x\<close>]
by auto
+lemma verit_sko_forall_indirect2:
+ \<open>x = (SOME x. \<not>P x) \<Longrightarrow> (\<And>x :: 'a. (P x = P' x)) \<Longrightarrow>(\<forall>x. P' x) \<longleftrightarrow> P x\<close>
+ using someI[of \<open>\<lambda>x. \<not>P x\<close>]
+ by auto
+
lemma verit_sko_ex: \<open>(\<exists>x. P x) \<longleftrightarrow> P (SOME x. P x)\<close>
using someI[of \<open>\<lambda>x. P x\<close>]
by auto
@@ -214,6 +222,10 @@
using someI[of \<open>\<lambda>x. P x\<close>]
by auto
+lemma verit_sko_ex_indirect2: \<open>x = (SOME x. P x) \<Longrightarrow> (\<And>x. P x = P' x) \<Longrightarrow> (\<exists>x. P' x) \<longleftrightarrow> P x\<close>
+ using someI[of \<open>\<lambda>x. P x\<close>]
+ by auto
+
lemma verit_Pure_trans:
\<open>P \<equiv> Q \<Longrightarrow> Q \<Longrightarrow> P\<close>
by auto
@@ -229,13 +241,6 @@
\<open>b \<equiv> c \<Longrightarrow> (if b then x else y) \<equiv> (if c then x else y)\<close>
by auto
-lemma verit_ite_intro_simp:
- \<open>(if c then (a :: 'a) = (if c then P else Q') else Q) = (if c then a = P else Q)\<close>
- \<open>(if c then R else b = (if c then R' else Q')) =
- (if c then R else b = Q')\<close>
- \<open>(if c then a' = a' else b' = b')\<close>
- by (auto split: if_splits)
-
lemma verit_or_neg:
\<open>(A \<Longrightarrow> B) \<Longrightarrow> B \<or> \<not>A\<close>
\<open>(\<not>A \<Longrightarrow> B) \<Longrightarrow> B \<or> A\<close>
@@ -250,13 +255,21 @@
\<open>(\<not>a \<Longrightarrow> A) \<Longrightarrow> a \<or> A\<close>
by blast+
+lemma verit_or_pos:
+ \<open>A \<and> A' \<Longrightarrow> (c \<and> A) \<or> (\<not>c \<and> A')\<close>
+ \<open>A \<and> A' \<Longrightarrow> (\<not>c \<and> A) \<or> (c \<and> A')\<close>
+ by blast+
+
+
lemma verit_la_generic:
\<open>(a::int) \<le> x \<or> a = x \<or> a \<ge> x\<close>
by linarith
-lemma verit_tmp_bfun_elim:
+lemma verit_bfun_elim:
\<open>(if b then P True else P False) = P b\<close>
- by (cases b) auto
+ \<open>(\<forall>b. P' b) = (P' False \<and> P' True)\<close>
+ \<open>(\<exists>b. P' b) = (P' False \<or> P' True)\<close>
+ by (cases b) (auto simp: all_bool_eq ex_bool_eq)
lemma verit_eq_true_simplify:
\<open>(P = True) \<equiv> P\<close>
@@ -283,6 +296,313 @@
\<open>B = A \<Longrightarrow> C = B \<Longrightarrow> A = C\<close>
by auto
+lemma verit_bool_simplify:
+ \<open>\<not>(P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not>Q\<close>
+ \<open>\<not>(P \<or> Q) \<longleftrightarrow> \<not>P \<and> \<not>Q\<close>
+ \<open>\<not>(P \<and> Q) \<longleftrightarrow> \<not>P \<or> \<not>Q\<close>
+ \<open>(P \<longrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<and> Q) \<longrightarrow> R)\<close>
+ \<open>((P \<longrightarrow> Q) \<longrightarrow> Q) \<longleftrightarrow> P \<or> Q\<close>
+ \<open>(Q \<longleftrightarrow> (P \<or> Q)) \<longleftrightarrow> (P \<longrightarrow> Q)\<close> \<comment> \<open>This rule was inverted\<close>
+ \<open>P \<and> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> Q\<close>
+ \<open>(P \<longrightarrow> Q) \<and> P \<longleftrightarrow> P \<and> Q\<close>
+ (* \<comment>\<open>Additional rules:\<close>
+ * \<open>((P \<longrightarrow> Q) \<longrightarrow> P) \<longleftrightarrow> P\<close>
+ * \<open>((P \<longrightarrow> Q) \<longrightarrow> Q) \<longleftrightarrow> P \<or> Q\<close>
+ * \<open>(P \<longrightarrow> Q) \<or> P\<close> *)
+ unfolding not_imp imp_conjL
+ by auto
+
+text \<open>We need the last equation for \<^term>\<open>\<not>(\<forall>a b. \<not>P a b)\<close>\<close>
+lemma verit_connective_def: \<comment> \<open>the definition of XOR is missing
+ as the operator is not generated by Isabelle\<close>
+ \<open>(A = B) \<longleftrightarrow> ((A \<longrightarrow> B) \<and> (B \<longrightarrow> A))\<close>
+ \<open>(If A B C) = ((A \<longrightarrow> B) \<and> (\<not>A \<longrightarrow> C))\<close>
+ \<open>(\<exists>x. P x) \<longleftrightarrow> \<not>(\<forall>x. \<not>P x)\<close>
+ \<open>\<not>(\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not>P x)\<close>
+ by auto
+
+lemma verit_ite_simplify:
+ \<open>(If True B C) = B\<close>
+ \<open>(If False B C) = C\<close>
+ \<open>(If A' B B) = B\<close>
+ \<open>(If (\<not>A') B C) = (If A' C B)\<close>
+ \<open>(If c (If c A B) C) = (If c A C)\<close>
+ \<open>(If c C (If c A B)) = (If c C B)\<close>
+ \<open>(If A' True False) = A'\<close>
+ \<open>(If A' False True) \<longleftrightarrow> \<not>A'\<close>
+ \<open>(If A' True B') \<longleftrightarrow> A'\<or>B'\<close>
+ \<open>(If A' B' False) \<longleftrightarrow> A'\<and>B'\<close>
+ \<open>(If A' False B') \<longleftrightarrow> \<not>A'\<and>B'\<close>
+ \<open>(If A' B' True) \<longleftrightarrow> \<not>A'\<or>B'\<close>
+ \<open>x \<and> True \<longleftrightarrow> x\<close>
+ \<open>x \<or> False \<longleftrightarrow> x\<close>
+ for B C :: 'a and A' B' C' :: bool
+ by auto
+
+lemma verit_and_simplify1:
+ \<open>True \<and> b \<longleftrightarrow> b\<close> \<open>b \<and> True \<longleftrightarrow> b\<close>
+ \<open>False \<and> b \<longleftrightarrow> False\<close> \<open>b \<and> False \<longleftrightarrow> False\<close>
+ \<open>(c \<and> \<not>c) \<longleftrightarrow> False\<close> \<open>(\<not>c \<and> c) \<longleftrightarrow> False\<close>
+ \<open>\<not>\<not>a = a\<close>
+ by auto
+
+lemmas verit_and_simplify = conj_ac de_Morgan_conj disj_not1
+
+
+lemma verit_or_simplify_1:
+ \<open>False \<or> b \<longleftrightarrow> b\<close> \<open>b \<or> False \<longleftrightarrow> b\<close>
+ \<open>b \<or> \<not>b\<close>
+ \<open>\<not>b \<or> b\<close>
+ by auto
+
+lemmas verit_or_simplify = disj_ac
+
+lemma verit_not_simplify:
+ \<open>\<not> \<not>b \<longleftrightarrow> b\<close> \<open>\<not>True \<longleftrightarrow> False\<close> \<open>\<not>False \<longleftrightarrow> True\<close>
+ by auto
+
+
+lemma verit_implies_simplify:
+ \<open>(\<not>a \<longrightarrow> \<not>b) \<longleftrightarrow> (b \<longrightarrow> a)\<close>
+ \<open>(False \<longrightarrow> a) \<longleftrightarrow> True\<close>
+ \<open>(a \<longrightarrow> True) \<longleftrightarrow> True\<close>
+ \<open>(True \<longrightarrow> a) \<longleftrightarrow> a\<close>
+ \<open>(a \<longrightarrow> False) \<longleftrightarrow> \<not>a\<close>
+ \<open>(a \<longrightarrow> a) \<longleftrightarrow> True\<close>
+ \<open>(\<not>a \<longrightarrow> a) \<longleftrightarrow> a\<close>
+ \<open>(a \<longrightarrow> \<not>a) \<longleftrightarrow> \<not>a\<close>
+ \<open>((a \<longrightarrow> b) \<longrightarrow> b) \<longleftrightarrow> a \<or> b\<close>
+ by auto
+
+lemma verit_equiv_simplify:
+ \<open>((\<not>a) = (\<not>b)) \<longleftrightarrow> (a = b)\<close>
+ \<open>(a = a) \<longleftrightarrow> True\<close>
+ \<open>(a = (\<not>a)) \<longleftrightarrow> False\<close>
+ \<open>((\<not>a) = a) \<longleftrightarrow> False\<close>
+ \<open>(True = a) \<longleftrightarrow> a\<close>
+ \<open>(a = True) \<longleftrightarrow> a\<close>
+ \<open>(False = a) \<longleftrightarrow> \<not>a\<close>
+ \<open>(a = False) \<longleftrightarrow> \<not>a\<close>
+ \<open>\<not>\<not>a \<longleftrightarrow> a\<close>
+ \<open>(\<not> False) = True\<close>
+ 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:
+ \<open>(a :: 'a :: cancel_comm_monoid_add) - a = 0\<close>
+ \<open>(a :: 'a :: cancel_comm_monoid_add) - 0 = a\<close>
+ \<open>0 - (b :: 'b :: {group_add}) = -b\<close>
+ \<open>- (- (b :: 'b :: group_add)) = b\<close>
+ by auto
+
+lemma verit_sum_simplify:
+ \<open>(a :: 'a :: cancel_comm_monoid_add) + 0 = a\<close>
+ 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:
+ \<open>(a :: 'a ::order) < a \<longleftrightarrow> False\<close>
+ \<open>a \<le> a\<close>
+ \<open>\<not>(b' \<le> a') \<longleftrightarrow> (a' :: 'b :: linorder) < b'\<close>
+ 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:
+ \<open>(a :: 'a ::linorder) = b \<or> \<not>a \<le> b \<or> \<not>b \<le> a\<close>
+ by auto
+
+context
+begin
+
+text \<open>For the reconstruction, we need to keep the order of the arguments.\<close>
+
+named_theorems smt_arith_multiplication \<open>Theorems to reconstruct arithmetic theorems.\<close>
+
+named_theorems smt_arith_combine \<open>Theorems to reconstruct arithmetic theorems.\<close>
+
+named_theorems smt_arith_simplify \<open>Theorems to combine theorems in the LA procedure\<close>
+
+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]:
+ \<open>\<not> (a' :: 'a :: linorder) < b' \<longleftrightarrow> b' \<le> a'\<close>
+ \<open>\<not> (a' :: 'a :: linorder) \<le> b' \<longleftrightarrow> b' < a'\<close>
+ \<open>(c::int) mod Numeral1 = 0\<close>
+ \<open>(a::nat) mod Numeral1 = 0\<close>
+ \<open>(c::int) div Numeral1 = c\<close>
+ \<open>a div Numeral1 = a\<close>
+ \<open>(c::int) mod 1 = 0\<close>
+ \<open>a mod 1 = 0\<close>
+ \<open>(c::int) div 1 = c\<close>
+ \<open>a div 1 = a\<close>
+ \<open>\<not>(a' \<noteq> b') \<longleftrightarrow> a' = b'\<close>
+ 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 \<open>auto simp: ac_simps\<close>)
+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) \<le> (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 \<open>auto simp: ac_simps\<close>)
+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) \<le> (B div n)"
+proof -
+ have f2: "B div n = A div n \<or> A div n < B div n"
+ by (metis (no_types) assms less_le zdiv_mono1)
+ have "B div n \<noteq> A div n \<or> B mod n \<noteq> 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 \<longrightarrow> A div n + (if B mod n = 0 then 1 else 0) \<le> 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 \<le> B" "0 < -n"
+ shows "(A div n) \<ge> (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 _ _ \<open>\<lambda>a :: nat. a div n * p\<close> for n p :: nat, THEN sym]
+ arg_cong[of _ _ \<open>\<lambda>a :: int. a div n * p\<close> for n p :: int, THEN sym]
+
+lemma [smt_arith_combine]:
+ "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c + 2 \<le> b + d"
+ "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c + 1 \<le> b + d"
+ "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c + 1 \<le> b + d" for a b c :: int
+ by auto
+
+lemma [smt_arith_combine]:
+ "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c + 2 \<le> b + d"
+ "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c + 1 \<le> b + d"
+ "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c + 1 \<le> 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]:
+ \<open>m < n \<Longrightarrow> c = d \<Longrightarrow> m + c < n + d\<close>
+ \<open>m \<le> n \<Longrightarrow> c = d \<Longrightarrow> m + c \<le> n + d\<close>
+ \<open>c = d \<Longrightarrow> m < n \<Longrightarrow> m + c < n + d\<close>
+ \<open>c = d \<Longrightarrow> m \<le> n \<Longrightarrow> m + c \<le> n + d\<close>
+ for m :: \<open>'a :: ordered_cancel_ab_semigroup_add\<close>
+ 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:
+ \<open>a \<le> (b :: 'a :: {ordered_ab_group_add}) \<Longrightarrow> -a \<ge> -b\<close>
+ \<open>a < b \<Longrightarrow> -a > -b\<close>
+ \<open>a = b \<Longrightarrow> -a = -b\<close>
+ by auto
+
+end
+
+lemma verit_ite_intro:
+ \<open>(if a then P (if a then a' else b') else Q) \<longleftrightarrow> (if a then P a' else Q)\<close>
+ \<open>(if a then P' else Q' (if a then a' else b')) \<longleftrightarrow> (if a then P' else Q' b')\<close>
+ \<open>A = f (if a then R else S) \<longleftrightarrow> (if a then A = f R else A = f S)\<close>
+ by auto
+
+lemma verit_ite_if_cong:
+ fixes x y :: bool
+ assumes "b=c"
+ and "c \<equiv> True \<Longrightarrow> x = u"
+ and "c \<equiv> False \<Longrightarrow> y = v"
+ shows "(if b then x else y) \<equiv> (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) \<equiv> (if c then u else v)"
+ by (subst H) auto
+qed
+
subsection \<open>Setup\<close>
@@ -308,6 +628,7 @@
ML_file \<open>Tools/SMT/conj_disj_perm.ML\<close>
ML_file \<open>Tools/SMT/smt_replay_methods.ML\<close>
ML_file \<open>Tools/SMT/smt_replay.ML\<close>
+ML_file \<open>Tools/SMT/smt_replay_arith.ML\<close>
ML_file \<open>Tools/SMT/z3_interface.ML\<close>
ML_file \<open>Tools/SMT/z3_replay_rules.ML\<close>
ML_file \<open>Tools/SMT/z3_replay_methods.ML\<close>
@@ -316,12 +637,6 @@
ML_file \<open>Tools/SMT/verit_replay.ML\<close>
ML_file \<open>Tools/SMT/smt_systems.ML\<close>
-method_setup smt = \<open>
- Scan.optional Attrib.thms [] >>
- (fn thms => fn ctxt =>
- METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
-\<close> "apply an SMT solver to the current goal"
-
subsection \<open>Configuration\<close>
@@ -372,7 +687,7 @@
declare [[cvc3_options = ""]]
declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]]
-declare [[verit_options = "--index-fresh-sorts"]]
+declare [[verit_options = ""]]
declare [[z3_options = ""]]
text \<open>
@@ -541,7 +856,7 @@
"0 * x = 0"
"1 * x = x"
"x + y = y + x"
- by (auto simp add: mult_2)
+ by auto
lemma [z3_rule]: (* for def-axiom *)
"P = Q \<or> P \<or> Q"