author  haftmann 
Wed, 29 Apr 2009 14:20:26 +0200  
changeset 31021  53642251a04f 
parent 30960  fec1a04b7220 
child 31080  21ffc770ebc0 
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 
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
30506
diff
changeset

8 
imports Main 
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 

30506  39 
fun card_univ_tr' show_sorts _ [Const (@{const_syntax 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 

30001  45 
lemma card_unit [simp]: "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 

30001  48 
lemma card_bool [simp]: "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 

30001  51 
lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)" 
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 

30001  54 
lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)" 
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 

30001  57 
lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)" 
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 

30001  64 
lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)" 
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 

30001  68 
lemma card_nat [simp]: "CARD(nat) = 0" 
69 
by (simp add: infinite_UNIV_nat card_eq_0_iff) 

70 

71 

72 
subsection {* Classes with at least 1 and 2 *} 

73 

74 
text {* Class finite already captures "at least 1" *} 

75 

76 
lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)" 

29997  77 
unfolding neq0_conv [symmetric] by simp 
78 

30001  79 
lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)" 
80 
by (simp add: less_Suc_eq_le [symmetric]) 

81 

82 
text {* Class for cardinality "at least 2" *} 

83 

84 
class card2 = finite + 

85 
assumes two_le_card: "2 \<le> CARD('a)" 

86 

87 
lemma one_less_card: "Suc 0 < CARD('a::card2)" 

88 
using two_le_card [where 'a='a] by simp 

89 

90 
lemma one_less_int_card: "1 < int CARD('a::card2)" 

91 
using one_less_card [where 'a='a] by simp 

92 

25378  93 

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

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

95 

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

97 
typedef (open) num1 = "UNIV :: unit set" .. 
29997  98 

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

100 
proof 

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

102 
by simp 

103 
qed 

104 

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

106 
proof 

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

108 
by simp 

109 
qed 

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

110 

30001  111 
lemma card_num0 [simp]: "CARD (num0) = 0" 
112 
unfolding type_definition.card [OF type_definition_num0] 

113 
by simp 

114 

115 
lemma card_num1 [simp]: "CARD(num1) = 1" 

116 
unfolding type_definition.card [OF type_definition_num1] 

117 
by (simp only: card_unit) 

118 

119 
lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)" 

120 
unfolding type_definition.card [OF type_definition_bit0] 

121 
by simp 

122 

123 
lemma card_bit1 [simp]: "CARD('a bit1) = Suc (2 * CARD('a::finite))" 

124 
unfolding type_definition.card [OF type_definition_bit1] 

125 
by simp 

126 

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

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

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

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

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

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

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

133 

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

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

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

137 
unfolding type_definition.univ [OF type_definition_bit0] 
29997  138 
by simp 
30001  139 
show "2 \<le> CARD('a bit0)" 
140 
by simp 

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

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

142 

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

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

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

146 
unfolding type_definition.univ [OF type_definition_bit1] 
29997  147 
by simp 
30001  148 
show "2 \<le> CARD('a bit1)" 
149 
by simp 

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

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

151 

25378  152 

29997  153 
subsection {* Locale for modular arithmetic subtypes *} 
154 

155 
locale mod_type = 

156 
fixes n :: int 

30960  157 
and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int" 
158 
and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}" 

29997  159 
assumes type: "type_definition Rep Abs {0..<n}" 
160 
and size1: "1 < n" 

161 
and zero_def: "0 = Abs 0" 

162 
and one_def: "1 = Abs 1" 

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

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

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

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

167 
begin 

168 

169 
lemma size0: "0 < n" 

170 
by (cut_tac size1, simp) 

171 

172 
lemmas definitions = 

30960  173 
zero_def one_def add_def mult_def minus_def diff_def 
29997  174 

175 
lemma Rep_less_n: "Rep x < n" 

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

177 

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

179 
by (rule Rep_less_n [THEN order_less_imp_le]) 

180 

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

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

183 

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

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

186 

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

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

189 

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

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

192 

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

194 
by (simp add: Abs_inverse size0) 

195 

196 
lemma Rep_0: "Rep 0 = 0" 

197 
by (simp add: zero_def Rep_Abs_0) 

198 

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

200 
by (simp add: Abs_inverse size1) 

201 

202 
lemma Rep_1: "Rep 1 = 1" 

203 
by (simp add: one_def Rep_Abs_1) 

204 

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

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

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

208 
apply (simp add: mod_pos_pos_trivial) 

209 
done 

210 

211 
lemmas Rep_simps = 

212 
Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1 

213 

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

215 
apply (intro_classes, unfold definitions) 

216 
apply (simp_all add: Rep_simps zmod_simps ring_simps) 

217 
done 

218 

219 
end 

220 

221 
locale mod_ring = mod_type + 

222 
constrains n :: int 

30960  223 
and Rep :: "'a::{number_ring} \<Rightarrow> int" 
224 
and Abs :: "int \<Rightarrow> 'a::{number_ring}" 

29997  225 
begin 
226 

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

228 
apply (induct k) 

229 
apply (simp add: zero_def) 

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

231 
done 

232 

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

234 
apply (cases z rule: int_diff_cases) 

235 
apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps) 

236 
done 

237 

238 
lemma Rep_number_of: 

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

240 
by (simp add: number_of_eq of_int_eq Rep_Abs_mod) 

241 

242 
lemma iszero_number_of: 

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

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

245 

246 
lemma cases: 

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

248 
shows "P" 

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

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

251 
apply (simp_all add: of_int_eq mod_pos_pos_trivial) 

252 
done 

253 

254 
lemma induct: 

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

256 
by (cases x rule: cases) simp 

257 

258 
end 

259 

260 

261 
subsection {* Number ring instances *} 

262 

30032  263 
text {* 
264 
Unfortunately a number ring instance is not possible for 

265 
@{typ num1}, since 0 and 1 are not distinct. 

266 
*} 

267 

30960  268 
instantiation num1 :: "{comm_ring,comm_monoid_mult,number}" 
30032  269 
begin 
270 

271 
lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True" 

272 
by (induct x, induct y) simp 

273 

274 
instance proof 

275 
qed (simp_all add: num1_eq_iff) 

276 

277 
end 

278 

29997  279 
instantiation 
30960  280 
bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}" 
29997  281 
begin 
282 

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

29998  284 
"Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))" 
29997  285 

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

29998  287 
"Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))" 
29997  288 

289 
definition "0 = Abs_bit0 0" 

290 
definition "1 = Abs_bit0 1" 

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

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

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

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

295 

296 
definition "0 = Abs_bit1 0" 

297 
definition "1 = Abs_bit1 1" 

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

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

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

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

302 

303 
instance .. 

304 

305 
end 

306 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset

307 
interpretation bit0: 
29998  308 
mod_type "int CARD('a::finite bit0)" 
29997  309 
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" 
310 
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" 

311 
apply (rule mod_type.intro) 

29998  312 
apply (simp add: int_mult type_definition_bit0) 
30001  313 
apply (rule one_less_int_card) 
29997  314 
apply (rule zero_bit0_def) 
315 
apply (rule one_bit0_def) 

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

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

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

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

320 
done 

321 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset

322 
interpretation bit1: 
29998  323 
mod_type "int CARD('a::finite bit1)" 
29997  324 
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" 
325 
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" 

326 
apply (rule mod_type.intro) 

29998  327 
apply (simp add: int_mult type_definition_bit1) 
30001  328 
apply (rule one_less_int_card) 
29997  329 
apply (rule zero_bit1_def) 
330 
apply (rule one_bit1_def) 

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

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

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

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

335 
done 

336 

31021  337 
instance bit0 :: (finite) comm_ring_1 
338 
by (rule bit0.comm_ring_1)+ 

29997  339 

31021  340 
instance bit1 :: (finite) comm_ring_1 
341 
by (rule bit1.comm_ring_1)+ 

29997  342 

343 
instantiation bit0 and bit1 :: (finite) number_ring 

344 
begin 

345 

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

347 

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

349 

350 
instance proof 

351 
qed (rule number_of_bit0_def number_of_bit1_def)+ 

352 

353 
end 

354 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset

355 
interpretation bit0: 
29998  356 
mod_ring "int CARD('a::finite bit0)" 
29997  357 
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" 
358 
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" 

359 
.. 

360 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset

361 
interpretation bit1: 
29998  362 
mod_ring "int CARD('a::finite bit1)" 
29997  363 
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" 
364 
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" 

365 
.. 

366 

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

368 

29999  369 
lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases 
370 
lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases 

29997  371 

29999  372 
lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct 
373 
lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct 

29997  374 

375 
lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of 

376 
lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of 

377 

378 

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

379 
subsection {* Syntax *} 
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 
syntax 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

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

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

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

385 

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

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

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

389 

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

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

391 
let 
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 
val num1_const = Syntax.const "Numeral_Type.num1"; 
24406  394 
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

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

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

397 

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

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

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

400 
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

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

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

404 
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

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

406 
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

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

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

409 

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

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

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

412 
 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

413 

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

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

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

416 

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

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

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

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

420 
 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

421 

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

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

424 
 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

425 
 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

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

427 

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

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

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

430 
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

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

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

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

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

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

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

437 

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

438 
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

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

440 

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

441 
subsection {* Examples *} 
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 
lemma "CARD(0) = 0" by simp 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

444 
lemma "CARD(17) = 17" by simp 
29997  445 
lemma "8 * 11 ^ 3  6 = (2::5)" by simp 
28920  446 

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

447 
end 