src/HOL/Library/Bit.thy
changeset 53063 8f7ac535892f
parent 49834 b27bbb021df1
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Library/Bit.thy	Sun Aug 18 15:29:50 2013 +0200
     1.2 +++ b/src/HOL/Library/Bit.thy	Sun Aug 18 15:29:50 2013 +0200
     1.3 @@ -10,16 +10,18 @@
     1.4  
     1.5  subsection {* Bits as a datatype *}
     1.6  
     1.7 -typedef bit = "UNIV :: bool set" ..
     1.8 +typedef bit = "UNIV :: bool set"
     1.9 +  morphisms set Bit
    1.10 +  ..
    1.11  
    1.12  instantiation bit :: "{zero, one}"
    1.13  begin
    1.14  
    1.15  definition zero_bit_def:
    1.16 -  "0 = Abs_bit False"
    1.17 +  "0 = Bit False"
    1.18  
    1.19  definition one_bit_def:
    1.20 -  "1 = Abs_bit True"
    1.21 +  "1 = Bit True"
    1.22  
    1.23  instance ..
    1.24  
    1.25 @@ -29,7 +31,7 @@
    1.26  proof -
    1.27    fix P and x :: bit
    1.28    assume "P (0::bit)" and "P (1::bit)"
    1.29 -  then have "\<forall>b. P (Abs_bit b)"
    1.30 +  then have "\<forall>b. P (Bit b)"
    1.31      unfolding zero_bit_def one_bit_def
    1.32      by (simp add: all_bool_eq)
    1.33    then show "P x"
    1.34 @@ -37,16 +39,63 @@
    1.35  next
    1.36    show "(0::bit) \<noteq> (1::bit)"
    1.37      unfolding zero_bit_def one_bit_def
    1.38 -    by (simp add: Abs_bit_inject)
    1.39 +    by (simp add: Bit_inject)
    1.40  qed
    1.41  
    1.42 -lemma bit_not_0_iff [iff]: "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
    1.43 -  by (induct x) simp_all
    1.44 +lemma Bit_set_eq [simp]:
    1.45 +  "Bit (set b) = b"
    1.46 +  by (fact set_inverse)
    1.47 +  
    1.48 +lemma set_Bit_eq [simp]:
    1.49 +  "set (Bit P) = P"
    1.50 +  by (rule Bit_inverse) rule
    1.51 +
    1.52 +lemma bit_eq_iff:
    1.53 +  "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
    1.54 +  by (auto simp add: set_inject)
    1.55 +
    1.56 +lemma Bit_inject [simp]:
    1.57 +  "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
    1.58 +  by (auto simp add: Bit_inject)  
    1.59 +
    1.60 +lemma set [iff]:
    1.61 +  "\<not> set 0"
    1.62 +  "set 1"
    1.63 +  by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
    1.64 +
    1.65 +lemma [code]:
    1.66 +  "set 0 \<longleftrightarrow> False"
    1.67 +  "set 1 \<longleftrightarrow> True"
    1.68 +  by simp_all
    1.69  
    1.70 -lemma bit_not_1_iff [iff]: "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
    1.71 -  by (induct x) simp_all
    1.72 +lemma set_iff:
    1.73 +  "set b \<longleftrightarrow> b = 1"
    1.74 +  by (cases b) simp_all
    1.75 +
    1.76 +lemma bit_eq_iff_set:
    1.77 +  "b = 0 \<longleftrightarrow> \<not> set b"
    1.78 +  "b = 1 \<longleftrightarrow> set b"
    1.79 +  by (simp_all add: bit_eq_iff)
    1.80 +
    1.81 +lemma Bit [simp, code]:
    1.82 +  "Bit False = 0"
    1.83 +  "Bit True = 1"
    1.84 +  by (simp_all add: zero_bit_def one_bit_def)
    1.85  
    1.86 +lemma bit_not_0_iff [iff]:
    1.87 +  "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
    1.88 +  by (simp add: bit_eq_iff)
    1.89  
    1.90 +lemma bit_not_1_iff [iff]:
    1.91 +  "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
    1.92 +  by (simp add: bit_eq_iff)
    1.93 +
    1.94 +lemma [code]:
    1.95 +  "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
    1.96 +  "HOL.equal 1 b \<longleftrightarrow> set b"
    1.97 +  by (simp_all add: equal set_iff)  
    1.98 +
    1.99 +  
   1.100  subsection {* Type @{typ bit} forms a field *}
   1.101  
   1.102  instantiation bit :: field_inverse_zero
   1.103 @@ -110,4 +159,46 @@
   1.104  lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
   1.105    by (simp only: numeral_Bit1 bit_add_self add_0_left)
   1.106  
   1.107 +
   1.108 +subsection {* Conversion from @{typ bit} *}
   1.109 +
   1.110 +context zero_neq_one
   1.111 +begin
   1.112 +
   1.113 +definition of_bit :: "bit \<Rightarrow> 'a"
   1.114 +where
   1.115 +  "of_bit b = bit_case 0 1 b" 
   1.116 +
   1.117 +lemma of_bit_eq [simp, code]:
   1.118 +  "of_bit 0 = 0"
   1.119 +  "of_bit 1 = 1"
   1.120 +  by (simp_all add: of_bit_def)
   1.121 +
   1.122 +lemma of_bit_eq_iff:
   1.123 +  "of_bit x = of_bit y \<longleftrightarrow> x = y"
   1.124 +  by (cases x) (cases y, simp_all)+
   1.125 +
   1.126 +end  
   1.127 +
   1.128 +context semiring_1
   1.129 +begin
   1.130 +
   1.131 +lemma of_nat_of_bit_eq:
   1.132 +  "of_nat (of_bit b) = of_bit b"
   1.133 +  by (cases b) simp_all
   1.134 +
   1.135  end
   1.136 +
   1.137 +context ring_1
   1.138 +begin
   1.139 +
   1.140 +lemma of_int_of_bit_eq:
   1.141 +  "of_int (of_bit b) = of_bit b"
   1.142 +  by (cases b) simp_all
   1.143 +
   1.144 +end
   1.145 +
   1.146 +hide_const (open) set
   1.147 +
   1.148 +end
   1.149 +