author  huffman 
Thu, 19 Feb 2009 16:51:46 0800  
changeset 29997  f6756c097c2d 
parent 29629  5111ce425e7a 
child 29998  19e1ef628b25 
permissions  rwrr 
29629  1 
(* Title: HOL/Library/Numeral_Type.thy 
2 
Author: Brian Huffman 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

3 
*) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

4 

29629  5 
header {* Numeral Syntax for Types *} 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

6 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

7 
theory Numeral_Type 
27487  8 
imports Plain "~~/src/HOL/Presburger" 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

9 
begin 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

10 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

11 
subsection {* Preliminary lemmas *} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

12 
(* These should be moved elsewhere *) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

13 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

14 
lemma (in type_definition) univ: 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

15 
"UNIV = Abs ` A" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

16 
proof 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

17 
show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

18 
show "UNIV \<subseteq> Abs ` A" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

19 
proof 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

20 
fix x :: 'b 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

21 
have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

22 
moreover have "Rep x \<in> A" by (rule Rep) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

23 
ultimately show "x \<in> Abs ` A" by (rule image_eqI) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

24 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

25 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

26 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

27 
lemma (in type_definition) card: "card (UNIV :: 'b set) = card A" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

28 
by (simp add: univ card_image inj_on_def Abs_inject) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

29 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

30 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

31 
subsection {* Cardinalities of types *} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

32 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

33 
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

34 

28920  35 
translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)" 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

36 

24407  37 
typed_print_translation {* 
38 
let 

28920  39 
fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] = 
24407  40 
Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T; 
28920  41 
in [(@{const_syntax card}, card_univ_tr')] 
24407  42 
end 
43 
*} 

44 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

45 
lemma card_unit: "CARD(unit) = 1" 
26153  46 
unfolding UNIV_unit by simp 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

47 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

48 
lemma card_bool: "CARD(bool) = 2" 
26153  49 
unfolding UNIV_bool by simp 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

50 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

51 
lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)" 
26153  52 
unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

53 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

54 
lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)" 
26153  55 
unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

56 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

57 
lemma card_option: "CARD('a::finite option) = Suc CARD('a)" 
26153  58 
unfolding insert_None_conv_UNIV [symmetric] 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

59 
apply (subgoal_tac "(None::'a option) \<notin> range Some") 
29997  60 
apply (simp add: card_image) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

61 
apply fast 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

62 
done 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

63 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

64 
lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)" 
26153  65 
unfolding Pow_UNIV [symmetric] 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

66 
by (simp only: card_Pow finite numeral_2_eq_2) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

67 

29997  68 
lemma card_finite_pos [simp]: "0 < CARD('a::finite)" 
69 
unfolding neq0_conv [symmetric] by simp 

70 

25378  71 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

72 
subsection {* Numeral Types *} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

73 

24406  74 
typedef (open) num0 = "UNIV :: nat set" .. 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

75 
typedef (open) num1 = "UNIV :: unit set" .. 
29997  76 

77 
typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}" 

78 
proof 

79 
show "0 \<in> {0 ..< 2 * int CARD('a)}" 

80 
by simp 

81 
qed 

82 

83 
typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}" 

84 
proof 

85 
show "0 \<in> {0 ..< 1 + 2 * int CARD('a)}" 

86 
by simp 

87 
qed 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

88 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

89 
instance num1 :: finite 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

90 
proof 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

91 
show "finite (UNIV::num1 set)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

92 
unfolding type_definition.univ [OF type_definition_num1] 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

93 
using finite by (rule finite_imageI) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

94 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

95 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

96 
instance bit0 :: (finite) finite 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

97 
proof 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

98 
show "finite (UNIV::'a bit0 set)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

99 
unfolding type_definition.univ [OF type_definition_bit0] 
29997  100 
by simp 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

101 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

102 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

103 
instance bit1 :: (finite) finite 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

104 
proof 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

105 
show "finite (UNIV::'a bit1 set)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

106 
unfolding type_definition.univ [OF type_definition_bit1] 
29997  107 
by simp 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

108 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

109 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

110 
lemma card_num1: "CARD(num1) = 1" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

111 
unfolding type_definition.card [OF type_definition_num1] 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

112 
by (simp only: card_unit) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

113 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

114 
lemma card_bit0: "CARD('a::finite bit0) = 2 * CARD('a)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

115 
unfolding type_definition.card [OF type_definition_bit0] 
29997  116 
by simp 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

117 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

118 
lemma card_bit1: "CARD('a::finite bit1) = Suc (2 * CARD('a))" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

119 
unfolding type_definition.card [OF type_definition_bit1] 
29997  120 
by simp 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

121 

24406  122 
lemma card_num0: "CARD (num0) = 0" 
26506
c4202c67fe3e
No longer imports InfiniteSet, ATP_Linkup is sufficient.
chaieb
parents:
26153
diff
changeset

123 
by (simp add: infinite_UNIV_nat card_eq_0_iff type_definition.card [OF type_definition_num0]) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

124 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

125 
lemmas card_univ_simps [simp] = 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

126 
card_unit 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

127 
card_bool 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

128 
card_prod 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

129 
card_sum 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

130 
card_option 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

131 
card_set 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

132 
card_num1 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

133 
card_bit0 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

134 
card_bit1 
24406  135 
card_num0 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

136 

25378  137 

29997  138 
subsection {* Locale for modular arithmetic subtypes *} 
139 

140 
locale mod_type = 

141 
fixes n :: int 

142 
and Rep :: "'a::{zero,one,plus,times,uminus,minus,power} \<Rightarrow> int" 

143 
and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus,power}" 

144 
assumes type: "type_definition Rep Abs {0..<n}" 

145 
and size1: "1 < n" 

146 
and zero_def: "0 = Abs 0" 

147 
and one_def: "1 = Abs 1" 

148 
and add_def: "x + y = Abs ((Rep x + Rep y) mod n)" 

149 
and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)" 

150 
and diff_def: "x  y = Abs ((Rep x  Rep y) mod n)" 

151 
and minus_def: " x = Abs (( Rep x) mod n)" 

152 
and power_def: "x ^ k = Abs (Rep x ^ k mod n)" 

153 
begin 

154 

155 
lemma size0: "0 < n" 

156 
by (cut_tac size1, simp) 

157 

158 
lemmas definitions = 

159 
zero_def one_def add_def mult_def minus_def diff_def power_def 

160 

161 
lemma Rep_less_n: "Rep x < n" 

162 
by (rule type_definition.Rep [OF type, simplified, THEN conjunct2]) 

163 

164 
lemma Rep_le_n: "Rep x \<le> n" 

165 
by (rule Rep_less_n [THEN order_less_imp_le]) 

166 

167 
lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y" 

168 
by (rule type_definition.Rep_inject [OF type, symmetric]) 

169 

170 
lemma Rep_inverse: "Abs (Rep x) = x" 

171 
by (rule type_definition.Rep_inverse [OF type]) 

172 

173 
lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m" 

174 
by (rule type_definition.Abs_inverse [OF type]) 

175 

176 
lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n" 

177 
by (simp add: Abs_inverse IntDiv.pos_mod_conj [OF size0]) 

178 

179 
lemma Rep_Abs_0: "Rep (Abs 0) = 0" 

180 
by (simp add: Abs_inverse size0) 

181 

182 
lemma Rep_0: "Rep 0 = 0" 

183 
by (simp add: zero_def Rep_Abs_0) 

184 

185 
lemma Rep_Abs_1: "Rep (Abs 1) = 1" 

186 
by (simp add: Abs_inverse size1) 

187 

188 
lemma Rep_1: "Rep 1 = 1" 

189 
by (simp add: one_def Rep_Abs_1) 

190 

191 
lemma Rep_mod: "Rep x mod n = Rep x" 

192 
apply (rule_tac x=x in type_definition.Abs_cases [OF type]) 

193 
apply (simp add: type_definition.Abs_inverse [OF type]) 

194 
apply (simp add: mod_pos_pos_trivial) 

195 
done 

196 

197 
lemmas Rep_simps = 

198 
Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1 

199 

200 
lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)" 

201 
apply (intro_classes, unfold definitions) 

202 
apply (simp_all add: Rep_simps zmod_simps ring_simps) 

203 
done 

204 

205 
lemma recpower: "OFCLASS('a, recpower_class)" 

206 
apply (intro_classes, unfold definitions) 

207 
apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc 

208 
mod_pos_pos_trivial size1) 

209 
done 

210 

211 
end 

212 

213 
locale mod_ring = mod_type + 

214 
constrains n :: int 

215 
and Rep :: "'a::{number_ring,power} \<Rightarrow> int" 

216 
and Abs :: "int \<Rightarrow> 'a::{number_ring,power}" 

217 
begin 

218 

219 
lemma of_nat_eq: "of_nat k = Abs (int k mod n)" 

220 
apply (induct k) 

221 
apply (simp add: zero_def) 

222 
apply (simp add: Rep_simps add_def one_def zmod_simps add_ac) 

223 
done 

224 

225 
lemma of_int_eq: "of_int z = Abs (z mod n)" 

226 
apply (cases z rule: int_diff_cases) 

227 
apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps) 

228 
done 

229 

230 
lemma Rep_number_of: 

231 
"Rep (number_of w) = number_of w mod n" 

232 
by (simp add: number_of_eq of_int_eq Rep_Abs_mod) 

233 

234 
lemma iszero_number_of: 

235 
"iszero (number_of w::'a) \<longleftrightarrow> number_of w mod n = 0" 

236 
by (simp add: Rep_simps number_of_eq of_int_eq iszero_def zero_def) 

237 

238 
lemma cases: 

239 
assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P" 

240 
shows "P" 

241 
apply (cases x rule: type_definition.Abs_cases [OF type]) 

242 
apply (rule_tac z="y" in 1) 

243 
apply (simp_all add: of_int_eq mod_pos_pos_trivial) 

244 
done 

245 

246 
lemma induct: 

247 
"(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)" 

248 
by (cases x rule: cases) simp 

249 

250 
end 

251 

252 

253 
subsection {* Number ring instances *} 

254 

255 
instantiation 

256 
bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}" 

257 
begin 

258 

259 
definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where 

260 
"Abs_bit0' x = Abs_bit0 (x mod (2 * int CARD('a)))" 

261 

262 
definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where 

263 
"Abs_bit1' x = Abs_bit1 (x mod (1 + 2 * int CARD('a)))" 

264 

265 
definition "0 = Abs_bit0 0" 

266 
definition "1 = Abs_bit0 1" 

267 
definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)" 

268 
definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)" 

269 
definition "x  y = Abs_bit0' (Rep_bit0 x  Rep_bit0 y)" 

270 
definition " x = Abs_bit0' ( Rep_bit0 x)" 

271 
definition "x ^ k = Abs_bit0' (Rep_bit0 x ^ k)" 

272 

273 
definition "0 = Abs_bit1 0" 

274 
definition "1 = Abs_bit1 1" 

275 
definition "x + y = Abs_bit1' (Rep_bit1 x + Rep_bit1 y)" 

276 
definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)" 

277 
definition "x  y = Abs_bit1' (Rep_bit1 x  Rep_bit1 y)" 

278 
definition " x = Abs_bit1' ( Rep_bit1 x)" 

279 
definition "x ^ k = Abs_bit1' (Rep_bit1 x ^ k)" 

280 

281 
instance .. 

282 

283 
end 

284 

285 
interpretation bit0!: 

286 
mod_type "2 * int CARD('a::finite)" 

287 
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" 

288 
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" 

289 
apply (rule mod_type.intro) 

290 
apply (rule type_definition_bit0) 

291 
using card_finite_pos [where ?'a='a] apply arith 

292 
apply (rule zero_bit0_def) 

293 
apply (rule one_bit0_def) 

294 
apply (rule plus_bit0_def [unfolded Abs_bit0'_def]) 

295 
apply (rule times_bit0_def [unfolded Abs_bit0'_def]) 

296 
apply (rule minus_bit0_def [unfolded Abs_bit0'_def]) 

297 
apply (rule uminus_bit0_def [unfolded Abs_bit0'_def]) 

298 
apply (rule power_bit0_def [unfolded Abs_bit0'_def]) 

299 
done 

300 

301 
interpretation bit1!: 

302 
mod_type "1 + 2 * int CARD('a::finite)" 

303 
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" 

304 
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" 

305 
apply (rule mod_type.intro) 

306 
apply (rule type_definition_bit1) 

307 
apply simp 

308 
apply (rule zero_bit1_def) 

309 
apply (rule one_bit1_def) 

310 
apply (rule plus_bit1_def [unfolded Abs_bit1'_def]) 

311 
apply (rule times_bit1_def [unfolded Abs_bit1'_def]) 

312 
apply (rule minus_bit1_def [unfolded Abs_bit1'_def]) 

313 
apply (rule uminus_bit1_def [unfolded Abs_bit1'_def]) 

314 
apply (rule power_bit1_def [unfolded Abs_bit1'_def]) 

315 
done 

316 

317 
instance bit0 :: (finite) "{comm_ring_1,recpower}" 

318 
by (rule bit0.comm_ring_1 bit0.recpower)+ 

319 

320 
instance bit1 :: (finite) "{comm_ring_1,recpower}" 

321 
by (rule bit1.comm_ring_1 bit1.recpower)+ 

322 

323 
instantiation bit0 and bit1 :: (finite) number_ring 

324 
begin 

325 

326 
definition "(number_of w :: _ bit0) = of_int w" 

327 

328 
definition "(number_of w :: _ bit1) = of_int w" 

329 

330 
instance proof 

331 
qed (rule number_of_bit0_def number_of_bit1_def)+ 

332 

333 
end 

334 

335 
interpretation bit0!: 

336 
mod_ring "2 * int CARD('a::finite)" 

337 
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" 

338 
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" 

339 
.. 

340 

341 
interpretation bit1!: 

342 
mod_ring "1 + 2 * int CARD('a::finite)" 

343 
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" 

344 
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" 

345 
.. 

346 

347 
text {* Set up cases, induction, and arithmetic *} 

348 

349 
lemmas bit0_cases [cases type: bit0, case_names of_int] = bit0.cases 

350 
lemmas bit1_cases [cases type: bit1, case_names of_int] = bit1.cases 

351 

352 
lemmas bit0_induct [induct type: bit0, case_names of_int] = bit0.induct 

353 
lemmas bit1_induct [induct type: bit1, case_names of_int] = bit1.induct 

354 

355 
lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of 

356 
lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of 

357 

358 
declare power_Suc [where ?'a="'a::finite bit0", standard, simp] 

359 
declare power_Suc [where ?'a="'a::finite bit1", standard, simp] 

360 

361 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

362 
subsection {* Syntax *} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

363 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

364 
syntax 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

365 
"_NumeralType" :: "num_const => type" ("_") 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

366 
"_NumeralType0" :: type ("0") 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

367 
"_NumeralType1" :: type ("1") 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

368 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

369 
translations 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

370 
"_NumeralType1" == (type) "num1" 
24406  371 
"_NumeralType0" == (type) "num0" 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

372 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

373 
parse_translation {* 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

374 
let 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

375 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

376 
val num1_const = Syntax.const "Numeral_Type.num1"; 
24406  377 
val num0_const = Syntax.const "Numeral_Type.num0"; 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

378 
val B0_const = Syntax.const "Numeral_Type.bit0"; 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

379 
val B1_const = Syntax.const "Numeral_Type.bit1"; 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

380 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

381 
fun mk_bintype n = 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

382 
let 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

383 
fun mk_bit n = if n = 0 then B0_const else B1_const; 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

384 
fun bin_of n = 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

385 
if n = 1 then num1_const 
24406  386 
else if n = 0 then num0_const 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

387 
else if n = ~1 then raise TERM ("negative type numeral", []) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

388 
else 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset

389 
let val (q, r) = Integer.div_mod n 2; 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

390 
in mk_bit r $ bin_of q end; 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

391 
in bin_of n end; 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

392 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

393 
fun numeral_tr (*"_NumeralType"*) [Const (str, _)] = 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset

394 
mk_bintype (valOf (Int.fromString str)) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

395 
 numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts); 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

396 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

397 
in [("_NumeralType", numeral_tr)] end; 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

398 
*} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

399 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

400 
print_translation {* 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

401 
let 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

402 
fun int_of [] = 0 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset

403 
 int_of (b :: bs) = b + 2 * int_of bs; 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

404 

24406  405 
fun bin_of (Const ("num0", _)) = [] 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

406 
 bin_of (Const ("num1", _)) = [1] 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

407 
 bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

408 
 bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

409 
 bin_of t = raise TERM("bin_of", [t]); 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

410 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

411 
fun bit_tr' b [t] = 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

412 
let 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

413 
val rev_digs = b :: bin_of t handle TERM _ => raise Match 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

414 
val i = int_of rev_digs; 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset

415 
val num = string_of_int (abs i); 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

416 
in 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

417 
Syntax.const "_NumeralType" $ Syntax.free num 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

418 
end 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

419 
 bit_tr' b _ = raise Match; 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

420 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

421 
in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end; 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

422 
*} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

423 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

424 

25378  425 
subsection {* Classes with at least 1 and 2 *} 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

426 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

427 
text {* Class finite already captures "at least 1" *} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

428 

24407  429 
lemma zero_less_card_finite [simp]: 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

430 
"0 < CARD('a::finite)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

431 
proof (cases "CARD('a::finite) = 0") 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

432 
case False thus ?thesis by (simp del: card_0_eq) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

433 
next 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

434 
case True 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

435 
thus ?thesis by (simp add: finite) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

436 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

437 

24407  438 
lemma one_le_card_finite [simp]: 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

439 
"Suc 0 <= CARD('a::finite)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

440 
by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

441 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

442 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

443 
text {* Class for cardinality "at least 2" *} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

444 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

445 
class card2 = finite + 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

446 
assumes two_le_card: "2 <= CARD('a)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

447 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

448 
lemma one_less_card: "Suc 0 < CARD('a::card2)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

449 
using two_le_card [where 'a='a] by simp 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

450 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

451 
instance bit0 :: (finite) card2 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

452 
by intro_classes (simp add: one_le_card_finite) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

453 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

454 
instance bit1 :: (finite) card2 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

455 
by intro_classes (simp add: one_le_card_finite) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

456 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

457 
subsection {* Examples *} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

458 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

459 
lemma "CARD(0) = 0" by simp 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

460 
lemma "CARD(17) = 17" by simp 
29997  461 
lemma "8 * 11 ^ 3  6 = (2::5)" by simp 
28920  462 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

463 
end 