# HG changeset patch
# User haftmann
# Date 1383216260 -3600
# Node ID 8a49a5a302840909a31df7409ee36ec78ace691e
# Parent  9fda41a04c32e2df1f26783683c7017215e17b12
generalized of_bool conversion

diff -r 9fda41a04c32 -r 8a49a5a30284 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Rings.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -86,7 +86,20 @@
 lemma one_neq_zero [simp]: "1 \<noteq> 0"
 by (rule not_sym) (rule zero_neq_one)
 
-end
+definition of_bool :: "bool \<Rightarrow> 'a"
+where
+  "of_bool p = (if p then 1 else 0)" 
+
+lemma of_bool_eq [simp, code]:
+  "of_bool False = 0"
+  "of_bool True = 1"
+  by (simp_all add: of_bool_def)
+
+lemma of_bool_eq_iff:
+  "of_bool p = of_bool q \<longleftrightarrow> p = q"
+  by (simp add: of_bool_def)
+
+end  
 
 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
 
diff -r 9fda41a04c32 -r 8a49a5a30284 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Word/Word.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -506,10 +506,6 @@
 definition max_word :: "'a::len word" -- "Largest representable machine integer." where
   "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
 
-primrec of_bool :: "bool \<Rightarrow> 'a::len word" where
-  "of_bool False = 0"
-| "of_bool True = 1"
-
 (* FIXME: only provide one theorem name *)
 lemmas of_nth_def = word_set_bits_def