|
1 (* Title: HOL/Library/Z2.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 section \<open>The Field of Integers mod 2\<close> |
|
6 |
|
7 theory Z2 |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 text \<open> |
|
12 Note that in most cases \<^typ>\<open>bool\<close> is appropriate hen a binary type is needed; the |
|
13 type provided here, for historical reasons named \<guillemotright>bit\<guillemotleft>, is only needed if proper |
|
14 field operations are required. |
|
15 \<close> |
|
16 |
|
17 subsection \<open>Bits as a datatype\<close> |
|
18 |
|
19 typedef bit = "UNIV :: bool set" |
|
20 morphisms set Bit .. |
|
21 |
|
22 instantiation bit :: "{zero, one}" |
|
23 begin |
|
24 |
|
25 definition zero_bit_def: "0 = Bit False" |
|
26 |
|
27 definition one_bit_def: "1 = Bit True" |
|
28 |
|
29 instance .. |
|
30 |
|
31 end |
|
32 |
|
33 old_rep_datatype "0::bit" "1::bit" |
|
34 proof - |
|
35 fix P :: "bit \<Rightarrow> bool" |
|
36 fix x :: bit |
|
37 assume "P 0" and "P 1" |
|
38 then have "\<forall>b. P (Bit b)" |
|
39 unfolding zero_bit_def one_bit_def |
|
40 by (simp add: all_bool_eq) |
|
41 then show "P x" |
|
42 by (induct x) simp |
|
43 next |
|
44 show "(0::bit) \<noteq> (1::bit)" |
|
45 unfolding zero_bit_def one_bit_def |
|
46 by (simp add: Bit_inject) |
|
47 qed |
|
48 |
|
49 lemma Bit_set_eq [simp]: "Bit (set b) = b" |
|
50 by (fact set_inverse) |
|
51 |
|
52 lemma set_Bit_eq [simp]: "set (Bit P) = P" |
|
53 by (rule Bit_inverse) rule |
|
54 |
|
55 lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)" |
|
56 by (auto simp add: set_inject) |
|
57 |
|
58 lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)" |
|
59 by (auto simp add: Bit_inject) |
|
60 |
|
61 lemma set [iff]: |
|
62 "\<not> set 0" |
|
63 "set 1" |
|
64 by (simp_all add: zero_bit_def one_bit_def Bit_inverse) |
|
65 |
|
66 lemma [code]: |
|
67 "set 0 \<longleftrightarrow> False" |
|
68 "set 1 \<longleftrightarrow> True" |
|
69 by simp_all |
|
70 |
|
71 lemma set_iff: "set b \<longleftrightarrow> b = 1" |
|
72 by (cases b) simp_all |
|
73 |
|
74 lemma bit_eq_iff_set: |
|
75 "b = 0 \<longleftrightarrow> \<not> set b" |
|
76 "b = 1 \<longleftrightarrow> set b" |
|
77 by (simp_all add: bit_eq_iff) |
|
78 |
|
79 lemma Bit [simp, code]: |
|
80 "Bit False = 0" |
|
81 "Bit True = 1" |
|
82 by (simp_all add: zero_bit_def one_bit_def) |
|
83 |
|
84 lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit |
|
85 by (simp add: bit_eq_iff) |
|
86 |
|
87 lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit |
|
88 by (simp add: bit_eq_iff) |
|
89 |
|
90 lemma [code]: |
|
91 "HOL.equal 0 b \<longleftrightarrow> \<not> set b" |
|
92 "HOL.equal 1 b \<longleftrightarrow> set b" |
|
93 by (simp_all add: equal set_iff) |
|
94 |
|
95 |
|
96 subsection \<open>Type \<^typ>\<open>bit\<close> forms a field\<close> |
|
97 |
|
98 instantiation bit :: field |
|
99 begin |
|
100 |
|
101 definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x" |
|
102 |
|
103 definition times_bit_def: "x * y = case_bit 0 y x" |
|
104 |
|
105 definition uminus_bit_def [simp]: "- x = x" for x :: bit |
|
106 |
|
107 definition minus_bit_def [simp]: "x - y = x + y" for x y :: bit |
|
108 |
|
109 definition inverse_bit_def [simp]: "inverse x = x" for x :: bit |
|
110 |
|
111 definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit |
|
112 |
|
113 lemmas field_bit_defs = |
|
114 plus_bit_def times_bit_def minus_bit_def uminus_bit_def |
|
115 divide_bit_def inverse_bit_def |
|
116 |
|
117 instance |
|
118 by standard (auto simp: field_bit_defs split: bit.split) |
|
119 |
|
120 end |
|
121 |
|
122 lemma bit_add_self: "x + x = 0" for x :: bit |
|
123 unfolding plus_bit_def by (simp split: bit.split) |
|
124 |
|
125 lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit |
|
126 unfolding times_bit_def by (simp split: bit.split) |
|
127 |
|
128 text \<open>Not sure whether the next two should be simp rules.\<close> |
|
129 |
|
130 lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit |
|
131 unfolding plus_bit_def by (simp split: bit.split) |
|
132 |
|
133 lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit |
|
134 unfolding plus_bit_def by (simp split: bit.split) |
|
135 |
|
136 |
|
137 subsection \<open>Numerals at type \<^typ>\<open>bit\<close>\<close> |
|
138 |
|
139 text \<open>All numerals reduce to either 0 or 1.\<close> |
|
140 |
|
141 lemma bit_minus1 [simp]: "- 1 = (1 :: bit)" |
|
142 by (simp only: uminus_bit_def) |
|
143 |
|
144 lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w" |
|
145 by (simp only: uminus_bit_def) |
|
146 |
|
147 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)" |
|
148 by (simp only: numeral_Bit0 bit_add_self) |
|
149 |
|
150 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)" |
|
151 by (simp only: numeral_Bit1 bit_add_self add_0_left) |
|
152 |
|
153 |
|
154 subsection \<open>Conversion from \<^typ>\<open>bit\<close>\<close> |
|
155 |
|
156 context zero_neq_one |
|
157 begin |
|
158 |
|
159 definition of_bit :: "bit \<Rightarrow> 'a" |
|
160 where "of_bit b = case_bit 0 1 b" |
|
161 |
|
162 lemma of_bit_eq [simp, code]: |
|
163 "of_bit 0 = 0" |
|
164 "of_bit 1 = 1" |
|
165 by (simp_all add: of_bit_def) |
|
166 |
|
167 lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y" |
|
168 by (cases x) (cases y; simp)+ |
|
169 |
|
170 end |
|
171 |
|
172 lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b" |
|
173 by (cases b) simp_all |
|
174 |
|
175 lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b" |
|
176 by (cases b) simp_all |
|
177 |
|
178 hide_const (open) set |
|
179 |
|
180 end |