src/HOL/Library/Bit.thy
 author haftmann Tue Nov 19 10:05:53 2013 +0100 (2013-11-19) changeset 54489 03ff4d1e6784 parent 53063 8f7ac535892f child 55416 dd7992d4a61a permissions -rw-r--r--
eliminiated neg_numeral in favour of - (numeral _)
1 (*  Title:      HOL/Library/Bit.thy
2     Author:     Brian Huffman
3 *)
5 header {* The Field of Integers mod 2 *}
7 theory Bit
8 imports Main
9 begin
11 subsection {* Bits as a datatype *}
13 typedef bit = "UNIV :: bool set"
14   morphisms set Bit
15   ..
17 instantiation bit :: "{zero, one}"
18 begin
20 definition zero_bit_def:
21   "0 = Bit False"
23 definition one_bit_def:
24   "1 = Bit True"
26 instance ..
28 end
30 rep_datatype "0::bit" "1::bit"
31 proof -
32   fix P and x :: bit
33   assume "P (0::bit)" and "P (1::bit)"
34   then have "\<forall>b. P (Bit b)"
35     unfolding zero_bit_def one_bit_def
36     by (simp add: all_bool_eq)
37   then show "P x"
38     by (induct x) simp
39 next
40   show "(0::bit) \<noteq> (1::bit)"
41     unfolding zero_bit_def one_bit_def
42     by (simp add: Bit_inject)
43 qed
45 lemma Bit_set_eq [simp]:
46   "Bit (set b) = b"
47   by (fact set_inverse)
49 lemma set_Bit_eq [simp]:
50   "set (Bit P) = P"
51   by (rule Bit_inverse) rule
53 lemma bit_eq_iff:
54   "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
55   by (auto simp add: set_inject)
57 lemma Bit_inject [simp]:
58   "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
59   by (auto simp add: Bit_inject)
61 lemma set [iff]:
62   "\<not> set 0"
63   "set 1"
64   by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
66 lemma [code]:
67   "set 0 \<longleftrightarrow> False"
68   "set 1 \<longleftrightarrow> True"
69   by simp_all
71 lemma set_iff:
72   "set b \<longleftrightarrow> b = 1"
73   by (cases b) simp_all
75 lemma bit_eq_iff_set:
76   "b = 0 \<longleftrightarrow> \<not> set b"
77   "b = 1 \<longleftrightarrow> set b"
78   by (simp_all add: bit_eq_iff)
80 lemma Bit [simp, code]:
81   "Bit False = 0"
82   "Bit True = 1"
83   by (simp_all add: zero_bit_def one_bit_def)
85 lemma bit_not_0_iff [iff]:
86   "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
87   by (simp add: bit_eq_iff)
89 lemma bit_not_1_iff [iff]:
90   "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
91   by (simp add: bit_eq_iff)
93 lemma [code]:
94   "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
95   "HOL.equal 1 b \<longleftrightarrow> set b"
96   by (simp_all add: equal set_iff)
99 subsection {* Type @{typ bit} forms a field *}
101 instantiation bit :: field_inverse_zero
102 begin
104 definition plus_bit_def:
105   "x + y = bit_case y (bit_case 1 0 y) x"
107 definition times_bit_def:
108   "x * y = bit_case 0 y x"
110 definition uminus_bit_def [simp]:
111   "- x = (x :: bit)"
113 definition minus_bit_def [simp]:
114   "x - y = (x + y :: bit)"
116 definition inverse_bit_def [simp]:
117   "inverse x = (x :: bit)"
119 definition divide_bit_def [simp]:
120   "x / y = (x * y :: bit)"
122 lemmas field_bit_defs =
123   plus_bit_def times_bit_def minus_bit_def uminus_bit_def
124   divide_bit_def inverse_bit_def
126 instance proof
127 qed (unfold field_bit_defs, auto split: bit.split)
129 end
131 lemma bit_add_self: "x + x = (0 :: bit)"
132   unfolding plus_bit_def by (simp split: bit.split)
134 lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
135   unfolding times_bit_def by (simp split: bit.split)
137 text {* Not sure whether the next two should be simp rules. *}
139 lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y"
140   unfolding plus_bit_def by (simp split: bit.split)
142 lemma bit_add_eq_1_iff: "x + y = (1 :: bit) \<longleftrightarrow> x \<noteq> y"
143   unfolding plus_bit_def by (simp split: bit.split)
146 subsection {* Numerals at type @{typ bit} *}
148 text {* All numerals reduce to either 0 or 1. *}
150 lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
151   by (simp only: uminus_bit_def)
153 lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
154   by (simp only: uminus_bit_def)
156 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
157   by (simp only: numeral_Bit0 bit_add_self)
159 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
160   by (simp only: numeral_Bit1 bit_add_self add_0_left)
163 subsection {* Conversion from @{typ bit} *}
165 context zero_neq_one
166 begin
168 definition of_bit :: "bit \<Rightarrow> 'a"
169 where
170   "of_bit b = bit_case 0 1 b"
172 lemma of_bit_eq [simp, code]:
173   "of_bit 0 = 0"
174   "of_bit 1 = 1"
175   by (simp_all add: of_bit_def)
177 lemma of_bit_eq_iff:
178   "of_bit x = of_bit y \<longleftrightarrow> x = y"
179   by (cases x) (cases y, simp_all)+
181 end
183 context semiring_1
184 begin
186 lemma of_nat_of_bit_eq:
187   "of_nat (of_bit b) = of_bit b"
188   by (cases b) simp_all
190 end
192 context ring_1
193 begin
195 lemma of_int_of_bit_eq:
196   "of_int (of_bit b) = of_bit b"
197   by (cases b) simp_all
199 end
201 hide_const (open) set
203 end