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"