# HG changeset patch
# User haftmann
# Date 1376832590 -7200
# Node ID 8f7ac535892f6c343be32a7ba1b70cc19d91b4be
# Parent  3af1a60200145cf61b9abf5f27ce5e3fb5a8c9e2
explicit conversion from and to bool, and into algebraic structures with 0 and 1

diff -r 3af1a6020014 -r 8f7ac535892f src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Sun Aug 18 15:29:50 2013 +0200
+++ b/src/HOL/Library/Bit.thy	Sun Aug 18 15:29:50 2013 +0200
@@ -10,16 +10,18 @@
 
 subsection {* Bits as a datatype *}
 
-typedef bit = "UNIV :: bool set" ..
+typedef bit = "UNIV :: bool set"
+  morphisms set Bit
+  ..
 
 instantiation bit :: "{zero, one}"
 begin
 
 definition zero_bit_def:
-  "0 = Abs_bit False"
+  "0 = Bit False"
 
 definition one_bit_def:
-  "1 = Abs_bit True"
+  "1 = Bit True"
 
 instance ..
 
@@ -29,7 +31,7 @@
 proof -
   fix P and x :: bit
   assume "P (0::bit)" and "P (1::bit)"
-  then have "\<forall>b. P (Abs_bit b)"
+  then have "\<forall>b. P (Bit b)"
     unfolding zero_bit_def one_bit_def
     by (simp add: all_bool_eq)
   then show "P x"
@@ -37,16 +39,63 @@
 next
   show "(0::bit) \<noteq> (1::bit)"
     unfolding zero_bit_def one_bit_def
-    by (simp add: Abs_bit_inject)
+    by (simp add: Bit_inject)
 qed
 
-lemma bit_not_0_iff [iff]: "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
-  by (induct x) simp_all
+lemma Bit_set_eq [simp]:
+  "Bit (set b) = b"
+  by (fact set_inverse)
+  
+lemma set_Bit_eq [simp]:
+  "set (Bit P) = P"
+  by (rule Bit_inverse) rule
+
+lemma bit_eq_iff:
+  "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
+  by (auto simp add: set_inject)
+
+lemma Bit_inject [simp]:
+  "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
+  by (auto simp add: Bit_inject)  
+
+lemma set [iff]:
+  "\<not> set 0"
+  "set 1"
+  by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
+
+lemma [code]:
+  "set 0 \<longleftrightarrow> False"
+  "set 1 \<longleftrightarrow> True"
+  by simp_all
 
-lemma bit_not_1_iff [iff]: "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
-  by (induct x) simp_all
+lemma set_iff:
+  "set b \<longleftrightarrow> b = 1"
+  by (cases b) simp_all
+
+lemma bit_eq_iff_set:
+  "b = 0 \<longleftrightarrow> \<not> set b"
+  "b = 1 \<longleftrightarrow> set b"
+  by (simp_all add: bit_eq_iff)
+
+lemma Bit [simp, code]:
+  "Bit False = 0"
+  "Bit True = 1"
+  by (simp_all add: zero_bit_def one_bit_def)
 
+lemma bit_not_0_iff [iff]:
+  "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
+  by (simp add: bit_eq_iff)
 
+lemma bit_not_1_iff [iff]:
+  "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
+  by (simp add: bit_eq_iff)
+
+lemma [code]:
+  "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
+  "HOL.equal 1 b \<longleftrightarrow> set b"
+  by (simp_all add: equal set_iff)  
+
+  
 subsection {* Type @{typ bit} forms a field *}
 
 instantiation bit :: field_inverse_zero
@@ -110,4 +159,46 @@
 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
   by (simp only: numeral_Bit1 bit_add_self add_0_left)
 
+
+subsection {* Conversion from @{typ bit} *}
+
+context zero_neq_one
+begin
+
+definition of_bit :: "bit \<Rightarrow> 'a"
+where
+  "of_bit b = bit_case 0 1 b" 
+
+lemma of_bit_eq [simp, code]:
+  "of_bit 0 = 0"
+  "of_bit 1 = 1"
+  by (simp_all add: of_bit_def)
+
+lemma of_bit_eq_iff:
+  "of_bit x = of_bit y \<longleftrightarrow> x = y"
+  by (cases x) (cases y, simp_all)+
+
+end  
+
+context semiring_1
+begin
+
+lemma of_nat_of_bit_eq:
+  "of_nat (of_bit b) = of_bit b"
+  by (cases b) simp_all
+
 end
+
+context ring_1
+begin
+
+lemma of_int_of_bit_eq:
+  "of_int (of_bit b) = of_bit b"
+  by (cases b) simp_all
+
+end
+
+hide_const (open) set
+
+end
+