# HG changeset patch
# User haftmann
# Date 1645126936 0
# Node ID f3fcc7c5a0db9c9c6054e94cb86a258f7e85b495
# Parent  4cc719621825ff87e140a529bbf63346e30cae6b
Avoid overaggresive splitting.

diff -r 4cc719621825 -r f3fcc7c5a0db NEWS
--- a/NEWS	Thu Feb 17 19:42:15 2022 +0000
+++ b/NEWS	Thu Feb 17 19:42:16 2022 +0000
@@ -15,6 +15,9 @@
 
 *** HOL ***
 
+* Rule split_of_bool_asm is not split any longer, analogously to
+split_if_asm.  INCOMPATIBILITY.
+
 * Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
 longer. INCOMPATIBILITY.
 
diff -r 4cc719621825 -r f3fcc7c5a0db src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Thu Feb 17 19:42:15 2022 +0000
+++ b/src/HOL/Library/Indicator_Function.thy	Thu Feb 17 19:42:16 2022 +0000
@@ -208,6 +208,6 @@
 lemma indicator_UN_disjoint:
   "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (\<Union>(f ` A)) x = (\<Sum>y\<in>A. indicator (f y) x)"
   by (induct A rule: finite_induct)
-    (auto simp: disjoint_family_on_def indicator_def split: if_splits)
+    (auto simp: disjoint_family_on_def indicator_def split: if_splits split_of_bool_asm)
 
 end
diff -r 4cc719621825 -r f3fcc7c5a0db src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Thu Feb 17 19:42:15 2022 +0000
+++ b/src/HOL/Library/Word.thy	Thu Feb 17 19:42:16 2022 +0000
@@ -1581,7 +1581,7 @@
 
 lemma mod_word_one [simp]:
   \<open>1 mod w = 1 - w * of_bool (w = 1)\<close> for w :: \<open>'a::len word\<close>
-  using div_mult_mod_eq [of 1 w] by simp
+  using div_mult_mod_eq [of 1 w] by auto
 
 lemma div_word_by_minus_1_eq [simp]:
   \<open>w div - 1 = of_bool (w = - 1)\<close> for w :: \<open>'a::len word\<close>
@@ -1589,9 +1589,17 @@
 
 lemma mod_word_by_minus_1_eq [simp]:
   \<open>w mod - 1 = w * of_bool (w < - 1)\<close> for w :: \<open>'a::len word\<close>
-  apply (cases \<open>w = - 1\<close>)
-   apply (auto simp add: word_order.not_eq_extremum)
-  using div_mult_mod_eq [of w \<open>- 1\<close>] by simp
+proof (cases \<open>w = - 1\<close>)
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  moreover have \<open>w < - 1\<close>
+    using False by (simp add: word_order.not_eq_extremum)
+  ultimately show ?thesis
+    by (simp add: mod_word_less)
+qed
 
 text \<open>Legacy theorems:\<close>
 
diff -r 4cc719621825 -r f3fcc7c5a0db src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Feb 17 19:42:15 2022 +0000
+++ b/src/HOL/Rings.thy	Thu Feb 17 19:42:16 2022 +0000
@@ -114,7 +114,7 @@
 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 [split]: "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
+lemma split_of_bool_asm: "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]: