author  haftmann 
Sat, 20 Jun 2020 05:56:28 +0000  
changeset 71965  d45f5d4c41bd 
parent 71957  3e162c63371a 
child 71988  ace45a11a45e 
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 

60500  17 
subsection \<open>Bits as a datatype\<close> 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

18 

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

19 
typedef bit = "UNIV :: bool set" 
63462  20 
morphisms set Bit .. 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

21 

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

22 
instantiation bit :: "{zero, one}" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

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

24 

63462  25 
definition zero_bit_def: "0 = Bit False" 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

26 

63462  27 
definition one_bit_def: "1 = Bit True" 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

28 

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

29 
instance .. 
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 

58306
117ba6cbe414
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
blanchet
parents:
55416
diff
changeset

33 
old_rep_datatype "0::bit" "1::bit" 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

34 
proof  
63462  35 
fix P :: "bit \<Rightarrow> bool" 
36 
fix x :: bit 

37 
assume "P 0" and "P 1" 

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

38 
then have "\<forall>b. P (Bit b)" 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

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

40 
by (simp add: all_bool_eq) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

41 
then show "P x" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

42 
by (induct x) simp 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

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

44 
show "(0::bit) \<noteq> (1::bit)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

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

46 
by (simp add: Bit_inject) 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

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

48 

63462  49 
lemma Bit_set_eq [simp]: "Bit (set b) = b" 
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

50 
by (fact set_inverse) 
63462  51 

52 
lemma set_Bit_eq [simp]: "set (Bit P) = P" 

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

53 
by (rule Bit_inverse) rule 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

54 

71953  55 
context 
56 
begin 

57 

58 
qualified lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)" 

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

59 
by (auto simp add: set_inject) 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

60 

71953  61 
end 
62 

63462  63 
lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)" 
64 
by (auto simp add: Bit_inject) 

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

65 

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

66 
lemma set [iff]: 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

67 
"\<not> set 0" 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

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

69 
by (simp_all add: zero_bit_def one_bit_def Bit_inverse) 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

70 

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

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

72 
"set 0 \<longleftrightarrow> False" 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

73 
"set 1 \<longleftrightarrow> True" 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

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

75 

63462  76 
lemma set_iff: "set b \<longleftrightarrow> b = 1" 
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

77 
by (cases b) simp_all 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

78 

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

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

80 
"b = 0 \<longleftrightarrow> \<not> set b" 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

81 
"b = 1 \<longleftrightarrow> set b" 
71953  82 
by (simp_all add: Z2.bit_eq_iff) 
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

83 

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

84 
lemma Bit [simp, code]: 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

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

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

87 
by (simp_all add: zero_bit_def one_bit_def) 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

88 

63462  89 
lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit 
71953  90 
by (simp add: Z2.bit_eq_iff) 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

91 

63462  92 
lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit 
71953  93 
by (simp add: Z2.bit_eq_iff) 
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

94 

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

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

96 
"HOL.equal 0 b \<longleftrightarrow> \<not> set b" 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

97 
"HOL.equal 1 b \<longleftrightarrow> set b" 
63462  98 
by (simp_all add: equal set_iff) 
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

99 

63462  100 

69593  101 
subsection \<open>Type \<^typ>\<open>bit\<close> forms a field\<close> 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

102 

59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
58881
diff
changeset

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

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

105 

63462  106 
definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x" 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

107 

63462  108 
definition times_bit_def: "x * y = case_bit 0 y x" 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

109 

63462  110 
definition uminus_bit_def [simp]: " x = x" for x :: bit 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

111 

63462  112 
definition minus_bit_def [simp]: "x  y = x + y" for x y :: bit 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

113 

63462  114 
definition inverse_bit_def [simp]: "inverse x = x" for x :: bit 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

115 

63462  116 
definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

117 

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

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

119 
plus_bit_def times_bit_def minus_bit_def uminus_bit_def 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

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

121 

60679  122 
instance 
71942  123 
by standard (auto simp: plus_bit_def times_bit_def split: bit.split) 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

124 

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

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

126 

63462  127 
lemma bit_add_self: "x + x = 0" for x :: bit 
30129  128 
unfolding plus_bit_def by (simp split: bit.split) 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

129 

63462  130 
lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

131 
unfolding times_bit_def by (simp split: bit.split) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

132 

60500  133 
text \<open>Not sure whether the next two should be simp rules.\<close> 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

134 

63462  135 
lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

136 
unfolding plus_bit_def by (simp split: bit.split) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

137 

63462  138 
lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

139 
unfolding plus_bit_def by (simp split: bit.split) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

140 

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

141 

69593  142 
subsection \<open>Numerals at type \<^typ>\<open>bit\<close>\<close> 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

143 

60500  144 
text \<open>All numerals reduce to either 0 or 1.\<close> 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

145 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
53063
diff
changeset

146 
lemma bit_minus1 [simp]: " 1 = (1 :: bit)" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
53063
diff
changeset

147 
by (simp only: uminus_bit_def) 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

148 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
53063
diff
changeset

149 
lemma bit_neg_numeral [simp]: "( numeral w :: bit) = numeral w" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
53063
diff
changeset

150 
by (simp only: uminus_bit_def) 
29995  151 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

152 
lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

153 
by (simp only: numeral_Bit0 bit_add_self) 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

154 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

155 
lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

156 
by (simp only: numeral_Bit1 bit_add_self add_0_left) 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

157 

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

158 

69593  159 
subsection \<open>Conversion from \<^typ>\<open>bit\<close>\<close> 
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

160 

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

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

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

163 

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

164 
definition of_bit :: "bit \<Rightarrow> 'a" 
63462  165 
where "of_bit b = case_bit 0 1 b" 
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

166 

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

167 
lemma of_bit_eq [simp, code]: 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

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

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

170 
by (simp_all add: of_bit_def) 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

171 

63462  172 
lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y" 
173 
by (cases x) (cases y; simp)+ 

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

174 

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

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

176 

63462  177 
lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b" 
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

178 
by (cases b) simp_all 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

179 

63462  180 
lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b" 
181 
by (cases b) simp_all 

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

182 

71953  183 

184 
subsection \<open>Bit structure\<close> 

185 

186 
instantiation bit :: semidom_modulo 

187 
begin 

188 

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

190 
where [simp]: \<open>a mod b = a * of_bool (b = 0)\<close> for a b :: bit 

191 

192 
instance 

193 
by standard simp 

194 

195 
end 

196 

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

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

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

199 

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

200 
definition bit_bit :: \<open>bit \<Rightarrow> nat \<Rightarrow> bool\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

201 
where [simp]: \<open>bit_bit b n \<longleftrightarrow> b = 1 \<and> n = 0\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

202 

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

203 
instance 
71953  204 
apply standard 
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

205 
apply (auto simp add: power_0_left power_add set_iff) 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

206 
apply (metis bit_not_1_iff of_bool_eq(2)) 
71953  207 
done 
208 

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

209 
end 
71953  210 

211 
instantiation bit :: semiring_bit_shifts 

212 
begin 

213 

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

215 
where \<open>push_bit n b = (if n = 0 then b else 0)\<close> for b :: bit 

216 

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

218 
where \<open>drop_bit n b = (if n = 0 then b else 0)\<close> for b :: bit 

219 

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

220 
definition take_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

221 
where \<open>take_bit n b = (if n = 0 then 0 else b)\<close> for b :: bit 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71957
diff
changeset

222 

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

224 
by standard (simp_all add: push_bit_bit_def drop_bit_bit_def take_bit_bit_def) 
71953  225 

226 
end 

227 

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

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

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

230 

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

231 
definition not_bit :: \<open>bit \<Rightarrow> bit\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

232 
where \<open>NOT b = of_bool (even b)\<close> for b :: bit 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

233 

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

234 
definition and_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

235 
where \<open>b AND c = of_bool (odd b \<and> odd c)\<close> for b c :: bit 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

236 

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

237 
definition or_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

238 
where \<open>b OR c = of_bool (odd b \<or> odd c)\<close> for b c :: bit 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

239 

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

240 
definition xor_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

241 
where \<open>b XOR c = of_bool (odd b \<noteq> odd c)\<close> for b c :: bit 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

242 

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

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

244 
by standard (auto simp add: and_bit_def or_bit_def xor_bit_def not_bit_def add_eq_0_iff) 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

245 

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

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

247 

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

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

249 
\<open>(+) = ((XOR) :: bit \<Rightarrow> _)\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

250 
by (auto simp add: fun_eq_iff plus_bit_def xor_bit_def) 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

251 

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

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

253 
\<open>(*) = ((AND) :: bit \<Rightarrow> _)\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

254 
by (simp add: fun_eq_iff times_bit_def and_bit_def split: bit.split) 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

255 

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

256 
lemma bit_NOT_eq_1_iff [simp]: "NOT b = 1 \<longleftrightarrow> b = 0" 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

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

258 
by (cases b) simp_all 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

259 

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

260 
lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1" 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

261 
for a b :: bit 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

262 
by (cases a; cases b) simp_all 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71953
diff
changeset

263 

71953  264 

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

265 
hide_const (open) set 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

266 

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

267 
end 