src/HOL/Rings.thy
changeset 54225 8a49a5a30284
parent 54147 97a8ff4e4ac9
child 54230 b1d955791529
     1.1 --- a/src/HOL/Rings.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Rings.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -86,7 +86,20 @@
     1.4  lemma one_neq_zero [simp]: "1 \<noteq> 0"
     1.5  by (rule not_sym) (rule zero_neq_one)
     1.6  
     1.7 -end
     1.8 +definition of_bool :: "bool \<Rightarrow> 'a"
     1.9 +where
    1.10 +  "of_bool p = (if p then 1 else 0)" 
    1.11 +
    1.12 +lemma of_bool_eq [simp, code]:
    1.13 +  "of_bool False = 0"
    1.14 +  "of_bool True = 1"
    1.15 +  by (simp_all add: of_bool_def)
    1.16 +
    1.17 +lemma of_bool_eq_iff:
    1.18 +  "of_bool p = of_bool q \<longleftrightarrow> p = q"
    1.19 +  by (simp add: of_bool_def)
    1.20 +
    1.21 +end  
    1.22  
    1.23  class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
    1.24