author  haftmann 
Fri, 14 Jun 2019 08:34:27 +0000  
changeset 70342  e4d626692640 
parent 69593  src/HOL/Library/Bit.thy@3dda49e08b9d 
child 70351  32b4e1aec5ca 
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 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

8 
imports Main 
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 
e4d626692640
clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents:
69593
diff
changeset

13 
type provided here, for historical reasons named \<guillemotright>bit\<guillemotleft>, is only needed if proper 
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 

63462  55 
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

56 
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

57 

63462  58 
lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)" 
59 
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

60 

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

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

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

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

64 
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

65 

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

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

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

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

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

70 

63462  71 
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

72 
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

73 

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

74 
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

75 
"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

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

77 
by (simp_all add: bit_eq_iff) 
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 [simp, code]: 
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

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

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

82 
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

83 

63462  84 
lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit 
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

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

86 

63462  87 
lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit 
53063
8f7ac535892f
explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents:
49834
diff
changeset

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

89 

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

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

91 
"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

92 
"HOL.equal 1 b \<longleftrightarrow> set b" 
63462  93 
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

94 

63462  95 

69593  96 
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

97 

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

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

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

100 

63462  101 
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

102 

63462  103 
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

104 

63462  105 
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

106 

63462  107 
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

108 

63462  109 
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

110 

63462  111 
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

112 

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

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

114 
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

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

116 

60679  117 
instance 
118 
by standard (auto simp: field_bit_defs split: bit.split) 

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

119 

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

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

121 

63462  122 
lemma bit_add_self: "x + x = 0" for x :: bit 
30129  123 
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

124 

63462  125 
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

126 
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

127 

60500  128 
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

129 

63462  130 
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

131 
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

132 

63462  133 
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

134 
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

135 

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

136 

69593  137 
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

138 

60500  139 
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

140 

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

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

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

143 

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

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

145 
by (simp only: uminus_bit_def) 
29995  146 

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

147 
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

148 
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

149 

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

150 
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

151 
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

152 

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

153 

69593  154 
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

155 

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

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

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

158 

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

159 
definition of_bit :: "bit \<Rightarrow> 'a" 
63462  160 
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

161 

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

162 
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

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

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

165 
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

166 

63462  167 
lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y" 
168 
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

169 

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

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

171 

63462  172 
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

173 
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

174 

63462  175 
lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b" 
176 
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

177 

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

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

179 

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

180 
end 