# HG changeset patch
# User haftmann
# Date 1617732740 0
# Node ID 0f33c7031ec94db434f6e6d96b4fc7d1f59b376d
# Parent  e7fb17bca374e079266cd767cfcefb115011b529
new lemmas

diff -r e7fb17bca374 -r 0f33c7031ec9 src/HOL/Divides.thy
--- 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>
diff -r e7fb17bca374 -r 0f33c7031ec9 src/HOL/Euclidean_Division.thy
--- 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
diff -r e7fb17bca374 -r 0f33c7031ec9 src/HOL/Groups_Big.thy
--- 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"
diff -r e7fb17bca374 -r 0f33c7031ec9 src/HOL/Groups_List.thy
--- 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
 
diff -r e7fb17bca374 -r 0f33c7031ec9 src/HOL/Library/Bit_Operations.thy
--- 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>
diff -r e7fb17bca374 -r 0f33c7031ec9 src/HOL/Library/Word.thy
--- 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)
diff -r e7fb17bca374 -r 0f33c7031ec9 src/HOL/Library/Z2.thy
--- 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
 
diff -r e7fb17bca374 -r 0f33c7031ec9 src/HOL/Parity.thy
--- 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
diff -r e7fb17bca374 -r 0f33c7031ec9 src/HOL/Rings.thy
--- 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"