author  haftmann 
Thu, 02 Jul 2020 08:49:04 +0000  
changeset 71988  ace45a11a45e 
parent 71965  d45f5d4c41bd 
child 72082  41393ecb57ac 
permissions  rwrr 
70342
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset

1 
(* Title: HOL/Library/Z2.thy 
41959  2 
Author: Brian Huffman 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

3 
*) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

4 

60500  5 
section \<open>The Field of Integers mod 2\<close> 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

6 

70342
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset

7 
theory Z2 
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

8 
imports Main "HOLLibrary.Bit_Operations" 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

9 
begin 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

10 

70342
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset

11 
text \<open> 
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset

12 
Note that in most cases \<^typ>\<open>bool\<close> is appropriate hen a binary type is needed; the 
70351  13 
type provided here, for historical reasons named \<^text>\<open>bit\<close>, is only needed if proper 
70342
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset

14 
field operations are required. 
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset

15 
\<close> 
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset

16 

71988  17 
typedef bit = \<open>UNIV :: bool set\<close> .. 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

18 

71988  19 
instantiation bit :: zero_neq_one 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

20 
begin 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

21 

71988  22 
definition zero_bit :: bit 
23 
where \<open>0 = Abs_bit False\<close> 

29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

24 

71988  25 
definition one_bit :: bit 
26 
where \<open>1 = Abs_bit True\<close> 

29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

27 

71988  28 
instance 
29 
by standard (simp add: zero_bit_def one_bit_def Abs_bit_inject) 

29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

30 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

31 
end 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

32 

71988  33 
free_constructors case_bit for \<open>0::bit\<close>  \<open>1::bit\<close> 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

34 
proof  
71988  35 
fix P :: bool 
36 
fix a :: bit 

37 
assume \<open>a = 0 \<Longrightarrow> P\<close> and \<open>a = 1 \<Longrightarrow> P\<close> 

38 
then show P 

39 
by (cases a) (auto simp add: zero_bit_def one_bit_def Abs_bit_inject) 

40 
qed simp 

41 

42 
lemma bit_not_zero_iff [simp]: 

43 
\<open>a \<noteq> 0 \<longleftrightarrow> a = 1\<close> for a :: bit 

44 
by (cases a) simp_all 

45 

46 
lemma bit_not_one_imp [simp]: 

47 
\<open>a \<noteq> 1 \<longleftrightarrow> a = 0\<close> for a :: bit 

48 
by (cases a) simp_all 

49 

50 
instantiation bit :: semidom_modulo 

51 
begin 

52 

53 
definition plus_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 

54 
where \<open>a + b = Abs_bit (Rep_bit a \<noteq> Rep_bit b)\<close> 

55 

56 
definition minus_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 

57 
where [simp]: \<open>minus_bit = plus\<close> 

58 

59 
definition times_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 

60 
where \<open>a * b = Abs_bit (Rep_bit a \<and> Rep_bit b)\<close> 

61 

62 
definition divide_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 

63 
where [simp]: \<open>divide_bit = times\<close> 

64 

65 
definition modulo_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 

66 
where \<open>a mod b = Abs_bit (Rep_bit a \<and> \<not> Rep_bit b)\<close> 

67 

68 
instance 

69 
by standard 

70 
(auto simp flip: Rep_bit_inject 

71 
simp add: zero_bit_def one_bit_def plus_bit_def times_bit_def modulo_bit_def Abs_bit_inverse Rep_bit_inverse) 

72 

73 
end 

74 

75 
lemma bit_2_eq_0 [simp]: 

76 
\<open>2 = (0::bit)\<close> 

77 
by (simp flip: one_add_one add: zero_bit_def plus_bit_def) 

78 

79 
instance bit :: semiring_parity 

80 
apply standard 

81 
apply (auto simp flip: Rep_bit_inject simp add: modulo_bit_def Abs_bit_inverse Rep_bit_inverse) 

82 
apply (auto simp add: zero_bit_def one_bit_def Abs_bit_inverse Rep_bit_inverse) 

83 
done 

84 

85 
lemma Abs_bit_eq_of_bool [code_abbrev]: 

86 
\<open>Abs_bit = of_bool\<close> 

87 
by (simp add: fun_eq_iff zero_bit_def one_bit_def) 

88 

89 
lemma Rep_bit_eq_odd: 

90 
\<open>Rep_bit = odd\<close> 

91 
proof  

92 
have \<open>\<not> Rep_bit 0\<close> 

93 
by (simp only: zero_bit_def) (subst Abs_bit_inverse, auto) 

94 
then show ?thesis 

95 
by (auto simp flip: Rep_bit_inject simp add: fun_eq_iff) 

29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

96 
qed 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

97 

71988  98 
lemma Rep_bit_iff_odd [code_abbrev]: 
99 
\<open>Rep_bit b \<longleftrightarrow> odd b\<close> 

100 
by (simp add: Rep_bit_eq_odd) 

101 

102 
lemma Not_Rep_bit_iff_even [code_abbrev]: 

103 
\<open>\<not> Rep_bit b \<longleftrightarrow> even b\<close> 

104 
by (simp add: Rep_bit_eq_odd) 

105 

106 
lemma Not_Not_Rep_bit [code_unfold]: 

107 
\<open>\<not> \<not> Rep_bit b \<longleftrightarrow> Rep_bit b\<close> 

108 
by simp 

109 

110 
code_datatype \<open>0::bit\<close> \<open>1::bit\<close> 

63462  111 

71988  112 
lemma Abs_bit_code [code]: 
113 
\<open>Abs_bit False = 0\<close> 

114 
\<open>Abs_bit True = 1\<close> 

115 
by (simp_all add: Abs_bit_eq_of_bool) 

116 

117 
lemma Rep_bit_code [code]: 

118 
\<open>Rep_bit 0 \<longleftrightarrow> False\<close> 

119 
\<open>Rep_bit 1 \<longleftrightarrow> True\<close> 

120 
by (simp_all add: Rep_bit_eq_odd) 

121 

122 
context zero_neq_one 

123 
begin 

124 

125 
abbreviation of_bit :: \<open>bit \<Rightarrow> 'a\<close> 

126 
where \<open>of_bit b \<equiv> of_bool (odd b)\<close> 

127 

128 
end 

53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

129 

71953  130 
context 
131 
begin 

132 

71988  133 
qualified lemma bit_eq_iff: 
134 
\<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close> for a b :: bit 

135 
by (cases a; cases b) simp_all 

29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

136 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

137 
end 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

138 

71988  139 
lemma modulo_bit_unfold [simp, code]: 
140 
\<open>a mod b = of_bool (odd a \<and> even b)\<close> for a b :: bit 

141 
by (simp add: modulo_bit_def Abs_bit_eq_of_bool Rep_bit_eq_odd) 

53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

142 

71988  143 
lemma power_bit_unfold [simp, code]: 
144 
\<open>a ^ n = of_bool (odd a \<or> n = 0)\<close> for a :: bit 

145 
by (cases a) simp_all 

71953  146 

71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

147 
instantiation bit :: semiring_bits 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

148 
begin 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

149 

d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

150 
definition bit_bit :: \<open>bit \<Rightarrow> nat \<Rightarrow> bool\<close> 
71988  151 
where [simp]: \<open>bit_bit b n \<longleftrightarrow> odd b \<and> n = 0\<close> 
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

152 

d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

153 
instance 
71953  154 
apply standard 
71988  155 
apply auto 
156 
apply (metis bit.exhaust of_bool_eq(2)) 

71953  157 
done 
158 

71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

159 
end 
71953  160 

161 
instantiation bit :: semiring_bit_shifts 

162 
begin 

163 

164 
definition push_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close> 

71988  165 
where [simp]: \<open>push_bit n b = of_bool (odd b \<and> n = 0)\<close> for b :: bit 
71953  166 

167 
definition drop_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close> 

71988  168 
where [simp]: \<open>drop_bit_bit = push_bit\<close> 
71953  169 

71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

170 
definition take_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close> 
71988  171 
where [simp]: \<open>take_bit n b = of_bool (odd b \<and> n > 0)\<close> for b :: bit 
172 

173 
instance 

174 
by standard simp_all 

175 

176 
end 

177 

178 
instantiation bit :: semiring_bit_operations 

179 
begin 

180 

181 
definition and_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 

182 
where [simp]: \<open>b AND c = of_bool (odd b \<and> odd c)\<close> for b c :: bit 

183 

184 
definition or_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 

185 
where [simp]: \<open>b OR c = of_bool (odd b \<or> odd c)\<close> for b c :: bit 

186 

187 
definition xor_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 

188 
where [simp]: \<open>b XOR c = of_bool (odd b \<noteq> odd c)\<close> for b c :: bit 

71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

189 

71953  190 
instance 
71988  191 
by standard auto 
192 

193 
end 

194 

195 
lemma add_bit_eq_xor [simp, code]: 

196 
\<open>(+) = ((XOR) :: bit \<Rightarrow> _)\<close> 

197 
by (auto simp add: fun_eq_iff) 

198 

199 
lemma mult_bit_eq_and [simp, code]: 

200 
\<open>(*) = ((AND) :: bit \<Rightarrow> _)\<close> 

201 
by (simp add: fun_eq_iff) 

202 

203 
instantiation bit :: field 

204 
begin 

205 

206 
definition uminus_bit :: \<open>bit \<Rightarrow> bit\<close> 

207 
where [simp]: \<open>uminus_bit = id\<close> 

208 

209 
definition inverse_bit :: \<open>bit \<Rightarrow> bit\<close> 

210 
where [simp]: \<open>inverse_bit = id\<close> 

211 

212 
instance 

213 
by standard simp_all 

71953  214 

215 
end 

216 

71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

217 
instantiation bit :: ring_bit_operations 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

218 
begin 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

219 

3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

220 
definition not_bit :: \<open>bit \<Rightarrow> bit\<close> 
71988  221 
where [simp]: \<open>NOT b = of_bool (even b)\<close> for b :: bit 
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

222 

3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

223 
instance 
71988  224 
by standard simp_all 
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

225 

3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

226 
end 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

227 

71988  228 
lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)" 
229 
by (simp only: Z2.bit_eq_iff even_numeral) simp 

71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

230 

71988  231 
lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)" 
232 
by (simp only: Z2.bit_eq_iff odd_numeral) simp 

53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

233 

8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

234 
end 