author | haftmann |
Mon, 23 Mar 2009 08:14:24 +0100 | |
changeset 30663 | 0b6aff7451b2 |
parent 30506 | 105ad9a68e51 |
child 30729 | 461ee3e49ad3 |
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 |
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 |
|
157 |
and Rep :: "'a::{zero,one,plus,times,uminus,minus,power} \<Rightarrow> int" |
|
158 |
and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus,power}" |
|
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 |
and power_def: "x ^ k = Abs (Rep x ^ k mod n)" |
|
168 |
begin |
|
169 |
||
170 |
lemma size0: "0 < n" |
|
171 |
by (cut_tac size1, simp) |
|
172 |
||
173 |
lemmas definitions = |
|
174 |
zero_def one_def add_def mult_def minus_def diff_def power_def |
|
175 |
||
176 |
lemma Rep_less_n: "Rep x < n" |
|
177 |
by (rule type_definition.Rep [OF type, simplified, THEN conjunct2]) |
|
178 |
||
179 |
lemma Rep_le_n: "Rep x \<le> n" |
|
180 |
by (rule Rep_less_n [THEN order_less_imp_le]) |
|
181 |
||
182 |
lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y" |
|
183 |
by (rule type_definition.Rep_inject [OF type, symmetric]) |
|
184 |
||
185 |
lemma Rep_inverse: "Abs (Rep x) = x" |
|
186 |
by (rule type_definition.Rep_inverse [OF type]) |
|
187 |
||
188 |
lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m" |
|
189 |
by (rule type_definition.Abs_inverse [OF type]) |
|
190 |
||
191 |
lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n" |
|
192 |
by (simp add: Abs_inverse IntDiv.pos_mod_conj [OF size0]) |
|
193 |
||
194 |
lemma Rep_Abs_0: "Rep (Abs 0) = 0" |
|
195 |
by (simp add: Abs_inverse size0) |
|
196 |
||
197 |
lemma Rep_0: "Rep 0 = 0" |
|
198 |
by (simp add: zero_def Rep_Abs_0) |
|
199 |
||
200 |
lemma Rep_Abs_1: "Rep (Abs 1) = 1" |
|
201 |
by (simp add: Abs_inverse size1) |
|
202 |
||
203 |
lemma Rep_1: "Rep 1 = 1" |
|
204 |
by (simp add: one_def Rep_Abs_1) |
|
205 |
||
206 |
lemma Rep_mod: "Rep x mod n = Rep x" |
|
207 |
apply (rule_tac x=x in type_definition.Abs_cases [OF type]) |
|
208 |
apply (simp add: type_definition.Abs_inverse [OF type]) |
|
209 |
apply (simp add: mod_pos_pos_trivial) |
|
210 |
done |
|
211 |
||
212 |
lemmas Rep_simps = |
|
213 |
Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1 |
|
214 |
||
215 |
lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)" |
|
216 |
apply (intro_classes, unfold definitions) |
|
217 |
apply (simp_all add: Rep_simps zmod_simps ring_simps) |
|
218 |
done |
|
219 |
||
220 |
lemma recpower: "OFCLASS('a, recpower_class)" |
|
221 |
apply (intro_classes, unfold definitions) |
|
222 |
apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc |
|
223 |
mod_pos_pos_trivial size1) |
|
224 |
done |
|
225 |
||
226 |
end |
|
227 |
||
228 |
locale mod_ring = mod_type + |
|
229 |
constrains n :: int |
|
230 |
and Rep :: "'a::{number_ring,power} \<Rightarrow> int" |
|
231 |
and Abs :: "int \<Rightarrow> 'a::{number_ring,power}" |
|
232 |
begin |
|
233 |
||
234 |
lemma of_nat_eq: "of_nat k = Abs (int k mod n)" |
|
235 |
apply (induct k) |
|
236 |
apply (simp add: zero_def) |
|
237 |
apply (simp add: Rep_simps add_def one_def zmod_simps add_ac) |
|
238 |
done |
|
239 |
||
240 |
lemma of_int_eq: "of_int z = Abs (z mod n)" |
|
241 |
apply (cases z rule: int_diff_cases) |
|
242 |
apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps) |
|
243 |
done |
|
244 |
||
245 |
lemma Rep_number_of: |
|
246 |
"Rep (number_of w) = number_of w mod n" |
|
247 |
by (simp add: number_of_eq of_int_eq Rep_Abs_mod) |
|
248 |
||
249 |
lemma iszero_number_of: |
|
250 |
"iszero (number_of w::'a) \<longleftrightarrow> number_of w mod n = 0" |
|
251 |
by (simp add: Rep_simps number_of_eq of_int_eq iszero_def zero_def) |
|
252 |
||
253 |
lemma cases: |
|
254 |
assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P" |
|
255 |
shows "P" |
|
256 |
apply (cases x rule: type_definition.Abs_cases [OF type]) |
|
257 |
apply (rule_tac z="y" in 1) |
|
258 |
apply (simp_all add: of_int_eq mod_pos_pos_trivial) |
|
259 |
done |
|
260 |
||
261 |
lemma induct: |
|
262 |
"(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)" |
|
263 |
by (cases x rule: cases) simp |
|
264 |
||
265 |
end |
|
266 |
||
267 |
||
268 |
subsection {* Number ring instances *} |
|
269 |
||
30032 | 270 |
text {* |
271 |
Unfortunately a number ring instance is not possible for |
|
272 |
@{typ num1}, since 0 and 1 are not distinct. |
|
273 |
*} |
|
274 |
||
275 |
instantiation num1 :: "{comm_ring,comm_monoid_mult,number,recpower}" |
|
276 |
begin |
|
277 |
||
278 |
lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True" |
|
279 |
by (induct x, induct y) simp |
|
280 |
||
281 |
instance proof |
|
282 |
qed (simp_all add: num1_eq_iff) |
|
283 |
||
284 |
end |
|
285 |
||
29997 | 286 |
instantiation |
287 |
bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}" |
|
288 |
begin |
|
289 |
||
290 |
definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where |
|
29998 | 291 |
"Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))" |
29997 | 292 |
|
293 |
definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where |
|
29998 | 294 |
"Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))" |
29997 | 295 |
|
296 |
definition "0 = Abs_bit0 0" |
|
297 |
definition "1 = Abs_bit0 1" |
|
298 |
definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)" |
|
299 |
definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)" |
|
300 |
definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)" |
|
301 |
definition "- x = Abs_bit0' (- Rep_bit0 x)" |
|
302 |
definition "x ^ k = Abs_bit0' (Rep_bit0 x ^ k)" |
|
303 |
||
304 |
definition "0 = Abs_bit1 0" |
|
305 |
definition "1 = Abs_bit1 1" |
|
306 |
definition "x + y = Abs_bit1' (Rep_bit1 x + Rep_bit1 y)" |
|
307 |
definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)" |
|
308 |
definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)" |
|
309 |
definition "- x = Abs_bit1' (- Rep_bit1 x)" |
|
310 |
definition "x ^ k = Abs_bit1' (Rep_bit1 x ^ k)" |
|
311 |
||
312 |
instance .. |
|
313 |
||
314 |
end |
|
315 |
||
316 |
interpretation bit0!: |
|
29998 | 317 |
mod_type "int CARD('a::finite bit0)" |
29997 | 318 |
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" |
319 |
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" |
|
320 |
apply (rule mod_type.intro) |
|
29998 | 321 |
apply (simp add: int_mult type_definition_bit0) |
30001 | 322 |
apply (rule one_less_int_card) |
29997 | 323 |
apply (rule zero_bit0_def) |
324 |
apply (rule one_bit0_def) |
|
325 |
apply (rule plus_bit0_def [unfolded Abs_bit0'_def]) |
|
326 |
apply (rule times_bit0_def [unfolded Abs_bit0'_def]) |
|
327 |
apply (rule minus_bit0_def [unfolded Abs_bit0'_def]) |
|
328 |
apply (rule uminus_bit0_def [unfolded Abs_bit0'_def]) |
|
329 |
apply (rule power_bit0_def [unfolded Abs_bit0'_def]) |
|
330 |
done |
|
331 |
||
332 |
interpretation bit1!: |
|
29998 | 333 |
mod_type "int CARD('a::finite bit1)" |
29997 | 334 |
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" |
335 |
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" |
|
336 |
apply (rule mod_type.intro) |
|
29998 | 337 |
apply (simp add: int_mult type_definition_bit1) |
30001 | 338 |
apply (rule one_less_int_card) |
29997 | 339 |
apply (rule zero_bit1_def) |
340 |
apply (rule one_bit1_def) |
|
341 |
apply (rule plus_bit1_def [unfolded Abs_bit1'_def]) |
|
342 |
apply (rule times_bit1_def [unfolded Abs_bit1'_def]) |
|
343 |
apply (rule minus_bit1_def [unfolded Abs_bit1'_def]) |
|
344 |
apply (rule uminus_bit1_def [unfolded Abs_bit1'_def]) |
|
345 |
apply (rule power_bit1_def [unfolded Abs_bit1'_def]) |
|
346 |
done |
|
347 |
||
348 |
instance bit0 :: (finite) "{comm_ring_1,recpower}" |
|
349 |
by (rule bit0.comm_ring_1 bit0.recpower)+ |
|
350 |
||
351 |
instance bit1 :: (finite) "{comm_ring_1,recpower}" |
|
352 |
by (rule bit1.comm_ring_1 bit1.recpower)+ |
|
353 |
||
354 |
instantiation bit0 and bit1 :: (finite) number_ring |
|
355 |
begin |
|
356 |
||
357 |
definition "(number_of w :: _ bit0) = of_int w" |
|
358 |
||
359 |
definition "(number_of w :: _ bit1) = of_int w" |
|
360 |
||
361 |
instance proof |
|
362 |
qed (rule number_of_bit0_def number_of_bit1_def)+ |
|
363 |
||
364 |
end |
|
365 |
||
366 |
interpretation bit0!: |
|
29998 | 367 |
mod_ring "int CARD('a::finite bit0)" |
29997 | 368 |
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" |
369 |
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" |
|
370 |
.. |
|
371 |
||
372 |
interpretation bit1!: |
|
29998 | 373 |
mod_ring "int CARD('a::finite bit1)" |
29997 | 374 |
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" |
375 |
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" |
|
376 |
.. |
|
377 |
||
378 |
text {* Set up cases, induction, and arithmetic *} |
|
379 |
||
29999 | 380 |
lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases |
381 |
lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases |
|
29997 | 382 |
|
29999 | 383 |
lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct |
384 |
lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct |
|
29997 | 385 |
|
386 |
lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of |
|
387 |
lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of |
|
388 |
||
389 |
declare power_Suc [where ?'a="'a::finite bit0", standard, simp] |
|
390 |
declare power_Suc [where ?'a="'a::finite bit1", standard, simp] |
|
391 |
||
392 |
||
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
393 |
subsection {* Syntax *} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
394 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
395 |
syntax |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
396 |
"_NumeralType" :: "num_const => type" ("_") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
397 |
"_NumeralType0" :: type ("0") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
398 |
"_NumeralType1" :: type ("1") |
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 |
translations |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
401 |
"_NumeralType1" == (type) "num1" |
24406 | 402 |
"_NumeralType0" == (type) "num0" |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
403 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
404 |
parse_translation {* |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
405 |
let |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
406 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
407 |
val num1_const = Syntax.const "Numeral_Type.num1"; |
24406 | 408 |
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
|
409 |
val B0_const = Syntax.const "Numeral_Type.bit0"; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
410 |
val B1_const = Syntax.const "Numeral_Type.bit1"; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
411 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
412 |
fun mk_bintype n = |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
413 |
let |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
414 |
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
|
415 |
fun bin_of n = |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
416 |
if n = 1 then num1_const |
24406 | 417 |
else if n = 0 then num0_const |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
418 |
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
|
419 |
else |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset
|
420 |
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
|
421 |
in mk_bit r $ bin_of q end; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
422 |
in bin_of n end; |
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 |
fun numeral_tr (*"_NumeralType"*) [Const (str, _)] = |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset
|
425 |
mk_bintype (valOf (Int.fromString str)) |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
426 |
| 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
|
427 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
428 |
in [("_NumeralType", numeral_tr)] end; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
429 |
*} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
430 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
431 |
print_translation {* |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
432 |
let |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
433 |
fun int_of [] = 0 |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset
|
434 |
| 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
|
435 |
|
24406 | 436 |
fun bin_of (Const ("num0", _)) = [] |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
437 |
| bin_of (Const ("num1", _)) = [1] |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
438 |
| 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
|
439 |
| 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
|
440 |
| bin_of t = raise TERM("bin_of", [t]); |
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 |
fun bit_tr' b [t] = |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
443 |
let |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
444 |
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
|
445 |
val i = int_of rev_digs; |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24407
diff
changeset
|
446 |
val num = string_of_int (abs i); |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
447 |
in |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
448 |
Syntax.const "_NumeralType" $ Syntax.free num |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
449 |
end |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
450 |
| bit_tr' b _ = raise Match; |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
451 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
452 |
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
|
453 |
*} |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
454 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
455 |
subsection {* Examples *} |
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 |
lemma "CARD(0) = 0" by simp |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
458 |
lemma "CARD(17) = 17" by simp |
29997 | 459 |
lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp |
28920 | 460 |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
461 |
end |