author | huffman |
Fri, 01 Jun 2012 11:53:58 +0200 | |
changeset 48063 | f02b4302d5dd |
parent 47108 | 2a1953f0d20d |
child 49834 | b27bbb021df1 |
permissions | -rw-r--r-- |
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 |
37653 | 8 |
imports Cardinality |
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 {* Numeral Types *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
12 |
|
24406 | 13 |
typedef (open) num0 = "UNIV :: nat set" .. |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
14 |
typedef (open) num1 = "UNIV :: unit set" .. |
29997 | 15 |
|
16 |
typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}" |
|
17 |
proof |
|
18 |
show "0 \<in> {0 ..< 2 * int CARD('a)}" |
|
19 |
by simp |
|
20 |
qed |
|
21 |
||
22 |
typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}" |
|
23 |
proof |
|
24 |
show "0 \<in> {0 ..< 1 + 2 * int CARD('a)}" |
|
25 |
by simp |
|
26 |
qed |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
27 |
|
30001 | 28 |
lemma card_num0 [simp]: "CARD (num0) = 0" |
29 |
unfolding type_definition.card [OF type_definition_num0] |
|
30 |
by simp |
|
31 |
||
32 |
lemma card_num1 [simp]: "CARD(num1) = 1" |
|
33 |
unfolding type_definition.card [OF type_definition_num1] |
|
48063
f02b4302d5dd
remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
huffman
parents:
47108
diff
changeset
|
34 |
by (simp only: card_UNIV_unit) |
30001 | 35 |
|
36 |
lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)" |
|
37 |
unfolding type_definition.card [OF type_definition_bit0] |
|
38 |
by simp |
|
39 |
||
40 |
lemma card_bit1 [simp]: "CARD('a bit1) = Suc (2 * CARD('a::finite))" |
|
41 |
unfolding type_definition.card [OF type_definition_bit1] |
|
42 |
by simp |
|
43 |
||
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
44 |
instance num1 :: finite |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
45 |
proof |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
46 |
show "finite (UNIV::num1 set)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
47 |
unfolding type_definition.univ [OF type_definition_num1] |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
48 |
using finite by (rule finite_imageI) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
49 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
50 |
|
30001 | 51 |
instance bit0 :: (finite) card2 |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
52 |
proof |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
53 |
show "finite (UNIV::'a bit0 set)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
54 |
unfolding type_definition.univ [OF type_definition_bit0] |
29997 | 55 |
by simp |
30001 | 56 |
show "2 \<le> CARD('a bit0)" |
57 |
by simp |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
58 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
59 |
|
30001 | 60 |
instance bit1 :: (finite) card2 |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
61 |
proof |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
62 |
show "finite (UNIV::'a bit1 set)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
63 |
unfolding type_definition.univ [OF type_definition_bit1] |
29997 | 64 |
by simp |
30001 | 65 |
show "2 \<le> CARD('a bit1)" |
66 |
by simp |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
67 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
68 |
|
37653 | 69 |
subsection {* Locales for for modular arithmetic subtypes *} |
29997 | 70 |
|
71 |
locale mod_type = |
|
72 |
fixes n :: int |
|
30960 | 73 |
and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int" |
74 |
and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}" |
|
29997 | 75 |
assumes type: "type_definition Rep Abs {0..<n}" |
76 |
and size1: "1 < n" |
|
77 |
and zero_def: "0 = Abs 0" |
|
78 |
and one_def: "1 = Abs 1" |
|
79 |
and add_def: "x + y = Abs ((Rep x + Rep y) mod n)" |
|
80 |
and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)" |
|
81 |
and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)" |
|
82 |
and minus_def: "- x = Abs ((- Rep x) mod n)" |
|
83 |
begin |
|
84 |
||
85 |
lemma size0: "0 < n" |
|
35362 | 86 |
using size1 by simp |
29997 | 87 |
|
88 |
lemmas definitions = |
|
30960 | 89 |
zero_def one_def add_def mult_def minus_def diff_def |
29997 | 90 |
|
91 |
lemma Rep_less_n: "Rep x < n" |
|
92 |
by (rule type_definition.Rep [OF type, simplified, THEN conjunct2]) |
|
93 |
||
94 |
lemma Rep_le_n: "Rep x \<le> n" |
|
95 |
by (rule Rep_less_n [THEN order_less_imp_le]) |
|
96 |
||
97 |
lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y" |
|
98 |
by (rule type_definition.Rep_inject [OF type, symmetric]) |
|
99 |
||
100 |
lemma Rep_inverse: "Abs (Rep x) = x" |
|
101 |
by (rule type_definition.Rep_inverse [OF type]) |
|
102 |
||
103 |
lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m" |
|
104 |
by (rule type_definition.Abs_inverse [OF type]) |
|
105 |
||
106 |
lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n" |
|
33361
1f18de40b43f
combined former theories Divides and IntDiv to one theory Divides
haftmann
parents:
33035
diff
changeset
|
107 |
by (simp add: Abs_inverse pos_mod_conj [OF size0]) |
29997 | 108 |
|
109 |
lemma Rep_Abs_0: "Rep (Abs 0) = 0" |
|
110 |
by (simp add: Abs_inverse size0) |
|
111 |
||
112 |
lemma Rep_0: "Rep 0 = 0" |
|
113 |
by (simp add: zero_def Rep_Abs_0) |
|
114 |
||
115 |
lemma Rep_Abs_1: "Rep (Abs 1) = 1" |
|
116 |
by (simp add: Abs_inverse size1) |
|
117 |
||
118 |
lemma Rep_1: "Rep 1 = 1" |
|
119 |
by (simp add: one_def Rep_Abs_1) |
|
120 |
||
121 |
lemma Rep_mod: "Rep x mod n = Rep x" |
|
122 |
apply (rule_tac x=x in type_definition.Abs_cases [OF type]) |
|
123 |
apply (simp add: type_definition.Abs_inverse [OF type]) |
|
124 |
apply (simp add: mod_pos_pos_trivial) |
|
125 |
done |
|
126 |
||
127 |
lemmas Rep_simps = |
|
128 |
Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1 |
|
129 |
||
130 |
lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)" |
|
131 |
apply (intro_classes, unfold definitions) |
|
36350 | 132 |
apply (simp_all add: Rep_simps zmod_simps field_simps) |
29997 | 133 |
done |
134 |
||
135 |
end |
|
136 |
||
46868 | 137 |
locale mod_ring = mod_type n Rep Abs |
138 |
for n :: int |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
139 |
and Rep :: "'a::{comm_ring_1} \<Rightarrow> int" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
140 |
and Abs :: "int \<Rightarrow> 'a::{comm_ring_1}" |
29997 | 141 |
begin |
142 |
||
143 |
lemma of_nat_eq: "of_nat k = Abs (int k mod n)" |
|
144 |
apply (induct k) |
|
145 |
apply (simp add: zero_def) |
|
146 |
apply (simp add: Rep_simps add_def one_def zmod_simps add_ac) |
|
147 |
done |
|
148 |
||
149 |
lemma of_int_eq: "of_int z = Abs (z mod n)" |
|
150 |
apply (cases z rule: int_diff_cases) |
|
151 |
apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps) |
|
152 |
done |
|
153 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
154 |
lemma Rep_numeral: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
155 |
"Rep (numeral w) = numeral w mod n" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
156 |
using of_int_eq [of "numeral w"] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
157 |
by (simp add: Rep_inject_sym Rep_Abs_mod) |
29997 | 158 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
159 |
lemma iszero_numeral: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
160 |
"iszero (numeral w::'a) \<longleftrightarrow> numeral w mod n = 0" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
161 |
by (simp add: Rep_inject_sym Rep_numeral Rep_0 iszero_def) |
29997 | 162 |
|
163 |
lemma cases: |
|
164 |
assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P" |
|
165 |
shows "P" |
|
166 |
apply (cases x rule: type_definition.Abs_cases [OF type]) |
|
167 |
apply (rule_tac z="y" in 1) |
|
168 |
apply (simp_all add: of_int_eq mod_pos_pos_trivial) |
|
169 |
done |
|
170 |
||
171 |
lemma induct: |
|
172 |
"(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)" |
|
173 |
by (cases x rule: cases) simp |
|
174 |
||
175 |
end |
|
176 |
||
177 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
178 |
subsection {* Ring class instances *} |
29997 | 179 |
|
30032 | 180 |
text {* |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
181 |
Unfortunately @{text ring_1} instance is not possible for |
30032 | 182 |
@{typ num1}, since 0 and 1 are not distinct. |
183 |
*} |
|
184 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
185 |
instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}" |
30032 | 186 |
begin |
187 |
||
188 |
lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True" |
|
189 |
by (induct x, induct y) simp |
|
190 |
||
191 |
instance proof |
|
192 |
qed (simp_all add: num1_eq_iff) |
|
193 |
||
194 |
end |
|
195 |
||
29997 | 196 |
instantiation |
30960 | 197 |
bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}" |
29997 | 198 |
begin |
199 |
||
200 |
definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where |
|
29998 | 201 |
"Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))" |
29997 | 202 |
|
203 |
definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where |
|
29998 | 204 |
"Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))" |
29997 | 205 |
|
206 |
definition "0 = Abs_bit0 0" |
|
207 |
definition "1 = Abs_bit0 1" |
|
208 |
definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)" |
|
209 |
definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)" |
|
210 |
definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)" |
|
211 |
definition "- x = Abs_bit0' (- Rep_bit0 x)" |
|
212 |
||
213 |
definition "0 = Abs_bit1 0" |
|
214 |
definition "1 = Abs_bit1 1" |
|
215 |
definition "x + y = Abs_bit1' (Rep_bit1 x + Rep_bit1 y)" |
|
216 |
definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)" |
|
217 |
definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)" |
|
218 |
definition "- x = Abs_bit1' (- Rep_bit1 x)" |
|
219 |
||
220 |
instance .. |
|
221 |
||
222 |
end |
|
223 |
||
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset
|
224 |
interpretation bit0: |
29998 | 225 |
mod_type "int CARD('a::finite bit0)" |
29997 | 226 |
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" |
227 |
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" |
|
228 |
apply (rule mod_type.intro) |
|
29998 | 229 |
apply (simp add: int_mult type_definition_bit0) |
30001 | 230 |
apply (rule one_less_int_card) |
29997 | 231 |
apply (rule zero_bit0_def) |
232 |
apply (rule one_bit0_def) |
|
233 |
apply (rule plus_bit0_def [unfolded Abs_bit0'_def]) |
|
234 |
apply (rule times_bit0_def [unfolded Abs_bit0'_def]) |
|
235 |
apply (rule minus_bit0_def [unfolded Abs_bit0'_def]) |
|
236 |
apply (rule uminus_bit0_def [unfolded Abs_bit0'_def]) |
|
237 |
done |
|
238 |
||
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset
|
239 |
interpretation bit1: |
29998 | 240 |
mod_type "int CARD('a::finite bit1)" |
29997 | 241 |
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" |
242 |
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" |
|
243 |
apply (rule mod_type.intro) |
|
29998 | 244 |
apply (simp add: int_mult type_definition_bit1) |
30001 | 245 |
apply (rule one_less_int_card) |
29997 | 246 |
apply (rule zero_bit1_def) |
247 |
apply (rule one_bit1_def) |
|
248 |
apply (rule plus_bit1_def [unfolded Abs_bit1'_def]) |
|
249 |
apply (rule times_bit1_def [unfolded Abs_bit1'_def]) |
|
250 |
apply (rule minus_bit1_def [unfolded Abs_bit1'_def]) |
|
251 |
apply (rule uminus_bit1_def [unfolded Abs_bit1'_def]) |
|
252 |
done |
|
253 |
||
31021 | 254 |
instance bit0 :: (finite) comm_ring_1 |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
255 |
by (rule bit0.comm_ring_1) |
29997 | 256 |
|
31021 | 257 |
instance bit1 :: (finite) comm_ring_1 |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
258 |
by (rule bit1.comm_ring_1) |
29997 | 259 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset
|
260 |
interpretation bit0: |
29998 | 261 |
mod_ring "int CARD('a::finite bit0)" |
29997 | 262 |
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" |
263 |
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" |
|
264 |
.. |
|
265 |
||
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset
|
266 |
interpretation bit1: |
29998 | 267 |
mod_ring "int CARD('a::finite bit1)" |
29997 | 268 |
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" |
269 |
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" |
|
270 |
.. |
|
271 |
||
272 |
text {* Set up cases, induction, and arithmetic *} |
|
273 |
||
29999 | 274 |
lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases |
275 |
lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases |
|
29997 | 276 |
|
29999 | 277 |
lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct |
278 |
lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct |
|
29997 | 279 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
280 |
lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
281 |
lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral |
29997 | 282 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
283 |
declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
284 |
declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp] |
29997 | 285 |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
286 |
subsection {* Syntax *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
287 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
288 |
syntax |
46236
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
289 |
"_NumeralType" :: "num_token => type" ("_") |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
290 |
"_NumeralType0" :: type ("0") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
291 |
"_NumeralType1" :: type ("1") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
292 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
293 |
translations |
35362 | 294 |
(type) "1" == (type) "num1" |
295 |
(type) "0" == (type) "num0" |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
296 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
297 |
parse_translation {* |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
298 |
let |
46236
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
299 |
fun mk_bintype n = |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
300 |
let |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
301 |
fun mk_bit 0 = Syntax.const @{type_syntax bit0} |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
302 |
| mk_bit 1 = Syntax.const @{type_syntax bit1}; |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
303 |
fun bin_of n = |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
304 |
if n = 1 then Syntax.const @{type_syntax num1} |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
305 |
else if n = 0 then Syntax.const @{type_syntax num0} |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
306 |
else if n = ~1 then raise TERM ("negative type numeral", []) |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
307 |
else |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
308 |
let val (q, r) = Integer.div_mod n 2; |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
309 |
in mk_bit r $ bin_of q end; |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
310 |
in bin_of n end; |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
311 |
|
46236
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
312 |
fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str)) |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
313 |
| numeral_tr ts = raise TERM ("numeral_tr", ts); |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
314 |
|
35115 | 315 |
in [(@{syntax_const "_NumeralType"}, numeral_tr)] end; |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
316 |
*} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
317 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
318 |
print_translation {* |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
319 |
let |
46236
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
320 |
fun int_of [] = 0 |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
321 |
| 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
|
322 |
|
46236
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
323 |
fun bin_of (Const (@{type_syntax num0}, _)) = [] |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
324 |
| bin_of (Const (@{type_syntax num1}, _)) = [1] |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
325 |
| bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
326 |
| bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
327 |
| bin_of t = raise TERM ("bin_of", [t]); |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
328 |
|
46236
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
329 |
fun bit_tr' b [t] = |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
330 |
let |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
331 |
val rev_digs = b :: bin_of t handle TERM _ => raise Match |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
332 |
val i = int_of rev_digs; |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
333 |
val num = string_of_int (abs i); |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
334 |
in |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
335 |
Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
336 |
end |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
337 |
| bit_tr' b _ = raise Match; |
35362 | 338 |
in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end; |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
339 |
*} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
340 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
341 |
subsection {* Examples *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
342 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
343 |
lemma "CARD(0) = 0" by simp |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
344 |
lemma "CARD(17) = 17" by simp |
29997 | 345 |
lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp |
28920 | 346 |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
347 |
end |