src/HOL/Rings.thy

   by (simp add: of_bool_def)
 
 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
 begin

 
 class ring_1 = ring + zero_neq_one + monoid_mult
 begin
 
 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)
 
 end

   by (simp add: not_le)
 
 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
 
 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
   using mult_mono[of a 1 b 1] by simp

     with that show False
       by (simp add: )
   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"
   by (frule le_add_diff_inverse2) (simp add: add.commute)
 

 
 subclass idom_abs_sgn
   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"
   using assms by (rule neqE)