--- a/src/HOL/Divides.thy Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Divides.thy Tue Apr 06 18:12:20 2021 +0000
@@ -147,7 +147,7 @@
proof (cases "sgn l = sgn k")
case True
then show ?thesis
- by (simp add: div_eq_sgn_abs)
+ by (auto simp add: div_eq_sgn_abs)
next
case False
with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
--- a/src/HOL/Euclidean_Division.thy Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Euclidean_Division.thy Tue Apr 06 18:12:20 2021 +0000
@@ -1625,8 +1625,8 @@
obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
by (blast intro: int_sgnE elim: that)
with that show ?thesis
- by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
- sgn_mult mod_eq_0_iff_dvd)
+ by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg sgn_mult)
+ (simp add: dvd_eq_mod_eq_0)
qed
instance proof
--- a/src/HOL/Groups_Big.thy Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Groups_Big.thy Tue Apr 06 18:12:20 2021 +0000
@@ -1117,6 +1117,25 @@
"(\<Sum>x \<in> A. y) = of_nat (card A) * y"
by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
+context
+ fixes A
+ assumes \<open>finite A\<close>
+begin
+
+lemma sum_of_bool_eq [simp]:
+ \<open>(\<Sum>x \<in> A. of_bool (P x)) = of_nat (card (A \<inter> {x. P x}))\<close> if \<open>finite A\<close>
+ using \<open>finite A\<close> by induction simp_all
+
+lemma sum_mult_of_bool_eq [simp]:
+ \<open>(\<Sum>x \<in> A. f x * of_bool (P x)) = (\<Sum>x \<in> (A \<inter> {x. P x}). f x)\<close>
+ by (rule sum.mono_neutral_cong) (use \<open>finite A\<close> in auto)
+
+lemma sum_of_bool_mult_eq [simp]:
+ \<open>(\<Sum>x \<in> A. of_bool (P x) * f x) = (\<Sum>x \<in> (A \<inter> {x. P x}). f x)\<close>
+ by (rule sum.mono_neutral_cong) (use \<open>finite A\<close> in auto)
+
+end
+
end
lemma sum_Suc: "sum (\<lambda>x. Suc(f x)) A = sum f A + card A"
--- a/src/HOL/Groups_List.thy Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Groups_List.thy Tue Apr 06 18:12:20 2021 +0000
@@ -430,7 +430,8 @@
also have \<open>\<dots> = b # map (bit a) [0..<m]\<close>
by (simp only: flip: map_Suc_upt) (simp add: bit_Suc rec.hyps)
finally show ?thesis
- using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps mod_2_eq_odd)
+ using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps)
+ (simp_all add: ac_simps mod_2_eq_odd)
qed
qed
--- a/src/HOL/Library/Bit_Operations.thy Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Library/Bit_Operations.thy Tue Apr 06 18:12:20 2021 +0000
@@ -640,7 +640,7 @@
for k l :: int
using and_int_rec [of \<open>NOT k\<close> \<open>NOT l\<close>]
by (simp add: or_int_def even_not_iff_int not_int_div_2)
- (simp add: not_int_def)
+ (simp_all add: not_int_def)
lemma bit_or_int_iff:
\<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close> for k l :: int
@@ -856,8 +856,13 @@
fixes x y :: int
assumes "0 \<le> x"
shows "x AND y \<le> x"
- using assms by (induction x arbitrary: y rule: int_bit_induct)
- (simp_all add: and_int_rec [of \<open>_ * 2\<close>] and_int_rec [of \<open>1 + _ * 2\<close>] add_increasing)
+using assms proof (induction x arbitrary: y rule: int_bit_induct)
+ case (odd k)
+ then have \<open>k AND y div 2 \<le> k\<close>
+ by simp
+ then show ?case
+ by (simp add: and_int_rec [of \<open>1 + _ * 2\<close>])
+qed (simp_all add: and_int_rec [of \<open>_ * 2\<close>])
lemmas AND_upper1' [simp] = order_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
--- a/src/HOL/Library/Word.thy Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Library/Word.thy Tue Apr 06 18:12:20 2021 +0000
@@ -122,7 +122,7 @@
lemma exp_eq_zero_iff [simp]:
\<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
- by transfer simp
+ by transfer auto
lemma word_exp_length_eq_0 [simp]:
\<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close>
@@ -854,7 +854,7 @@
if \<open>even a\<close>
for a :: \<open>'a word\<close>
using that by transfer
- (auto dest: le_Suc_ex simp add: mod_2_eq_odd take_bit_Suc elim!: evenE)
+ (auto dest: le_Suc_ex simp add: take_bit_Suc elim!: evenE)
show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
for m n :: nat
by transfer (simp, simp add: exp_div_exp_eq)
--- a/src/HOL/Library/Z2.thy Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Library/Z2.thy Tue Apr 06 18:12:20 2021 +0000
@@ -224,7 +224,7 @@
where [simp]: \<open>NOT b = of_bool (even b)\<close> for b :: bit
instance
- by standard simp_all
+ by standard auto
end
--- a/src/HOL/Parity.thy Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Parity.thy Tue Apr 06 18:12:20 2021 +0000
@@ -1018,7 +1018,7 @@
also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
using even by (auto simp add: algebra_simps mod2_eq_if)
finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
- using \<open>2 * 2 ^ n \<noteq> 0\<close> by simp (simp flip: bit_Suc add: bit_double_iff)
+ using \<open>2 * 2 ^ n \<noteq> 0\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff)
also have \<open>\<dots> \<longleftrightarrow> bit (a div 2) n \<or> bit (b div 2) n\<close>
using bit \<open>2 ^ n \<noteq> 0\<close> by (rule Suc.IH)
finally show ?case
@@ -1883,7 +1883,7 @@
then show ?thesis
apply (auto simp add: divide_int_def not_le elim!: evenE)
apply (simp only: minus_mult_right)
- apply (subst nat_mult_distrib)
+ apply (subst (asm) nat_mult_distrib)
apply simp_all
done
qed
--- a/src/HOL/Rings.thy Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Rings.thy Tue Apr 06 18:12:20 2021 +0000
@@ -114,9 +114,17 @@
lemma split_of_bool [split]: "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
by (cases p) simp_all
-lemma split_of_bool_asm: "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
+lemma split_of_bool_asm [split]: "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
by (cases p) simp_all
+lemma of_bool_eq_0_iff [simp]:
+ \<open>of_bool P = 0 \<longleftrightarrow> \<not> P\<close>
+ by simp
+
+lemma of_bool_eq_1_iff [simp]:
+ \<open>of_bool P = 1 \<longleftrightarrow> P\<close>
+ by simp
+
end
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
@@ -374,6 +382,10 @@
subclass semiring_1_cancel ..
+lemma of_bool_not_iff [simp]:
+ \<open>of_bool (\<not> P) = 1 - of_bool P\<close>
+ by simp
+
lemma square_diff_one_factored: "x * x - 1 = (x + 1) * (x - 1)"
by (simp add: algebra_simps)
@@ -2353,6 +2365,14 @@
lemma not_one_less_zero [simp]: "\<not> 1 < 0"
by (simp add: not_less)
+lemma of_bool_less_eq_iff [simp]:
+ \<open>of_bool P \<le> of_bool Q \<longleftrightarrow> (P \<longrightarrow> Q)\<close>
+ by auto
+
+lemma of_bool_less_iff [simp]:
+ \<open>of_bool P < of_bool Q \<longleftrightarrow> \<not> P \<and> Q\<close>
+ by auto
+
lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
using mult_left_mono[of c 1 a] by simp
@@ -2378,6 +2398,26 @@
qed
qed
+lemma zero_less_eq_of_bool [simp]:
+ \<open>0 \<le> of_bool P\<close>
+ by simp
+
+lemma zero_less_of_bool_iff [simp]:
+ \<open>0 < of_bool P \<longleftrightarrow> P\<close>
+ by simp
+
+lemma of_bool_less_eq_one [simp]:
+ \<open>of_bool P \<le> 1\<close>
+ by simp
+
+lemma of_bool_less_one_iff [simp]:
+ \<open>of_bool P < 1 \<longleftrightarrow> \<not> P\<close>
+ by simp
+
+lemma of_bool_or_iff [simp]:
+ \<open>of_bool (P \<or> Q) = max (of_bool P) (of_bool Q)\<close>
+ by (simp add: max_def)
+
text \<open>Addition is the inverse of subtraction.\<close>
lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
@@ -2441,6 +2481,10 @@
by standard
(auto simp add: sgn_if abs_if zero_less_mult_iff)
+lemma abs_bool_eq [simp]:
+ \<open>\<bar>of_bool P\<bar> = of_bool P\<close>
+ by simp
+
lemma linorder_neqE_linordered_idom:
assumes "x \<noteq> y"
obtains "x < y" | "y < x"