src/HOL/Rings.thy
changeset 55187 6d0d93316daf
parent 54703 499f92dc6e45
child 55912 e12a0ab9917c
     1.1 --- a/src/HOL/Rings.thy	Thu Jan 30 17:34:42 2014 +0100
     1.2 +++ b/src/HOL/Rings.thy	Thu Jan 30 16:09:03 2014 +0100
     1.3 @@ -99,6 +99,14 @@
     1.4    "of_bool p = of_bool q \<longleftrightarrow> p = q"
     1.5    by (simp add: of_bool_def)
     1.6  
     1.7 +lemma split_of_bool [split]:
     1.8 +  "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
     1.9 +  by (cases p) simp_all
    1.10 +
    1.11 +lemma split_of_bool_asm:
    1.12 +  "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
    1.13 +  by (cases p) simp_all
    1.14 +  
    1.15  end  
    1.16  
    1.17  class semiring_1 = zero_neq_one + semiring_0 + monoid_mult