author | Manuel Eberl <eberlm@in.tum.de> |
Fri, 08 Jan 2021 19:52:10 +0100 | |
changeset 73109 | 783406dd051e |
parent 69678 | 0f4d4a13dc16 |
child 76231 | 8a48e18f081e |
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 |
|
60500 | 5 |
section \<open>Numeral Syntax for Types\<close> |
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 |
|
60500 | 11 |
subsection \<open>Numeral Types\<close> |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
12 |
|
49834 | 13 |
typedef num0 = "UNIV :: nat set" .. |
14 |
typedef num1 = "UNIV :: unit set" .. |
|
29997 | 15 |
|
49834 | 16 |
typedef 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}" |
29997 | 17 |
proof |
18 |
show "0 \<in> {0 ..< 2 * int CARD('a)}" |
|
19 |
by simp |
|
20 |
qed |
|
21 |
||
49834 | 22 |
typedef 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}" |
29997 | 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 |
||
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
32 |
lemma infinite_num0: "\<not> finite (UNIV :: num0 set)" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
33 |
using card_num0[unfolded card_eq_0_iff] |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
34 |
by simp |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
35 |
|
30001 | 36 |
lemma card_num1 [simp]: "CARD(num1) = 1" |
37 |
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
|
38 |
by (simp only: card_UNIV_unit) |
30001 | 39 |
|
40 |
lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)" |
|
41 |
unfolding type_definition.card [OF type_definition_bit0] |
|
42 |
by simp |
|
43 |
||
44 |
lemma card_bit1 [simp]: "CARD('a bit1) = Suc (2 * CARD('a::finite))" |
|
45 |
unfolding type_definition.card [OF type_definition_bit1] |
|
46 |
by simp |
|
47 |
||
69666 | 48 |
subsection \<open>@{typ num1}\<close> |
49 |
||
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
50 |
instance num1 :: finite |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
51 |
proof |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
52 |
show "finite (UNIV::num1 set)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
53 |
unfolding type_definition.univ [OF type_definition_num1] |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
54 |
using finite by (rule finite_imageI) |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
55 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
56 |
|
69663 | 57 |
instantiation num1 :: CARD_1 |
58 |
begin |
|
59 |
||
60 |
instance |
|
61 |
proof |
|
62 |
show "CARD(num1) = 1" by auto |
|
63 |
qed |
|
64 |
||
65 |
end |
|
66 |
||
69666 | 67 |
lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True" |
68 |
by (induct x, induct y) simp |
|
69 |
||
70 |
instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}" |
|
71 |
begin |
|
72 |
||
73 |
instance |
|
74 |
by standard (simp_all add: num1_eq_iff) |
|
75 |
||
76 |
end |
|
77 |
||
78 |
lemma num1_eqI: |
|
79 |
fixes a::num1 shows "a = b" |
|
80 |
by(simp add: num1_eq_iff) |
|
81 |
||
82 |
lemma num1_eq1 [simp]: |
|
83 |
fixes a::num1 shows "a = 1" |
|
84 |
by (rule num1_eqI) |
|
85 |
||
86 |
lemma forall_1[simp]: "(\<forall>i::num1. P i) \<longleftrightarrow> P 1" |
|
87 |
by (metis (full_types) num1_eq_iff) |
|
88 |
||
89 |
lemma ex_1[simp]: "(\<exists>x::num1. P x) \<longleftrightarrow> P 1" |
|
90 |
by auto (metis (full_types) num1_eq_iff) |
|
91 |
||
92 |
instantiation num1 :: linorder begin |
|
93 |
definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b" |
|
94 |
definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b" |
|
95 |
instance |
|
96 |
by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI) |
|
97 |
end |
|
98 |
||
99 |
instance num1 :: wellorder |
|
100 |
by intro_classes (auto simp: less_eq_num1_def less_num1_def) |
|
101 |
||
102 |
||
30001 | 103 |
instance bit0 :: (finite) card2 |
24332
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 bit0 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_bit0] |
29997 | 107 |
by simp |
30001 | 108 |
show "2 \<le> CARD('a bit0)" |
109 |
by simp |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
110 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
111 |
|
30001 | 112 |
instance bit1 :: (finite) card2 |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
113 |
proof |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
114 |
show "finite (UNIV::'a bit1 set)" |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
115 |
unfolding type_definition.univ [OF type_definition_bit1] |
29997 | 116 |
by simp |
30001 | 117 |
show "2 \<le> CARD('a bit1)" |
118 |
by simp |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
119 |
qed |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
120 |
|
60500 | 121 |
subsection \<open>Locales for for modular arithmetic subtypes\<close> |
29997 | 122 |
|
123 |
locale mod_type = |
|
124 |
fixes n :: int |
|
30960 | 125 |
and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int" |
126 |
and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}" |
|
29997 | 127 |
assumes type: "type_definition Rep Abs {0..<n}" |
128 |
and size1: "1 < n" |
|
129 |
and zero_def: "0 = Abs 0" |
|
130 |
and one_def: "1 = Abs 1" |
|
131 |
and add_def: "x + y = Abs ((Rep x + Rep y) mod n)" |
|
132 |
and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)" |
|
133 |
and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)" |
|
134 |
and minus_def: "- x = Abs ((- Rep x) mod n)" |
|
135 |
begin |
|
136 |
||
137 |
lemma size0: "0 < n" |
|
35362 | 138 |
using size1 by simp |
29997 | 139 |
|
140 |
lemmas definitions = |
|
30960 | 141 |
zero_def one_def add_def mult_def minus_def diff_def |
29997 | 142 |
|
143 |
lemma Rep_less_n: "Rep x < n" |
|
144 |
by (rule type_definition.Rep [OF type, simplified, THEN conjunct2]) |
|
145 |
||
146 |
lemma Rep_le_n: "Rep x \<le> n" |
|
147 |
by (rule Rep_less_n [THEN order_less_imp_le]) |
|
148 |
||
149 |
lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y" |
|
150 |
by (rule type_definition.Rep_inject [OF type, symmetric]) |
|
151 |
||
152 |
lemma Rep_inverse: "Abs (Rep x) = x" |
|
153 |
by (rule type_definition.Rep_inverse [OF type]) |
|
154 |
||
155 |
lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m" |
|
156 |
by (rule type_definition.Abs_inverse [OF type]) |
|
157 |
||
158 |
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
|
159 |
by (simp add: Abs_inverse pos_mod_conj [OF size0]) |
29997 | 160 |
|
161 |
lemma Rep_Abs_0: "Rep (Abs 0) = 0" |
|
162 |
by (simp add: Abs_inverse size0) |
|
163 |
||
164 |
lemma Rep_0: "Rep 0 = 0" |
|
165 |
by (simp add: zero_def Rep_Abs_0) |
|
166 |
||
167 |
lemma Rep_Abs_1: "Rep (Abs 1) = 1" |
|
168 |
by (simp add: Abs_inverse size1) |
|
169 |
||
170 |
lemma Rep_1: "Rep 1 = 1" |
|
171 |
by (simp add: one_def Rep_Abs_1) |
|
172 |
||
173 |
lemma Rep_mod: "Rep x mod n = Rep x" |
|
174 |
apply (rule_tac x=x in type_definition.Abs_cases [OF type]) |
|
175 |
apply (simp add: type_definition.Abs_inverse [OF type]) |
|
176 |
done |
|
177 |
||
178 |
lemmas Rep_simps = |
|
179 |
Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1 |
|
180 |
||
181 |
lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)" |
|
182 |
apply (intro_classes, unfold definitions) |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
62348
diff
changeset
|
183 |
apply (simp_all add: Rep_simps mod_simps field_simps) |
29997 | 184 |
done |
185 |
||
186 |
end |
|
187 |
||
46868 | 188 |
locale mod_ring = mod_type n Rep Abs |
189 |
for n :: int |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
190 |
and Rep :: "'a::{comm_ring_1} \<Rightarrow> int" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
191 |
and Abs :: "int \<Rightarrow> 'a::{comm_ring_1}" |
29997 | 192 |
begin |
193 |
||
194 |
lemma of_nat_eq: "of_nat k = Abs (int k mod n)" |
|
195 |
apply (induct k) |
|
196 |
apply (simp add: zero_def) |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
62348
diff
changeset
|
197 |
apply (simp add: Rep_simps add_def one_def mod_simps ac_simps) |
29997 | 198 |
done |
199 |
||
200 |
lemma of_int_eq: "of_int z = Abs (z mod n)" |
|
201 |
apply (cases z rule: int_diff_cases) |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
62348
diff
changeset
|
202 |
apply (simp add: Rep_simps of_nat_eq diff_def mod_simps) |
29997 | 203 |
done |
204 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
205 |
lemma Rep_numeral: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
206 |
"Rep (numeral w) = numeral w mod n" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
207 |
using of_int_eq [of "numeral w"] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
208 |
by (simp add: Rep_inject_sym Rep_Abs_mod) |
29997 | 209 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
210 |
lemma iszero_numeral: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
211 |
"iszero (numeral w::'a) \<longleftrightarrow> numeral w mod n = 0" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
212 |
by (simp add: Rep_inject_sym Rep_numeral Rep_0 iszero_def) |
29997 | 213 |
|
214 |
lemma cases: |
|
215 |
assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P" |
|
216 |
shows "P" |
|
217 |
apply (cases x rule: type_definition.Abs_cases [OF type]) |
|
218 |
apply (rule_tac z="y" in 1) |
|
66936 | 219 |
apply (simp_all add: of_int_eq) |
29997 | 220 |
done |
221 |
||
222 |
lemma induct: |
|
223 |
"(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)" |
|
224 |
by (cases x rule: cases) simp |
|
225 |
||
73109
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
226 |
lemma UNIV_eq: "(UNIV :: 'a set) = Abs ` {0..<n}" |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
227 |
using type type_definition.univ by blast |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
228 |
|
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
229 |
lemma CARD_eq: "CARD('a) = nat n" |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
230 |
proof - |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
231 |
have "CARD('a) = card (Abs ` {0..<n})" |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
232 |
by (simp add: UNIV_eq) |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
233 |
also have "inj_on Abs {0..<n}" |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
234 |
by (metis Abs_inverse inj_onI) |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
235 |
hence "card (Abs ` {0..<n}) = nat n" |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
236 |
using size1 by (subst card_image) auto |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
237 |
finally show ?thesis . |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
238 |
qed |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
239 |
|
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
240 |
lemma CHAR_eq [simp]: "CHAR('a) = CARD('a)" |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
241 |
proof (rule CHAR_eqI) |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
242 |
show "of_nat (CARD('a)) = (0 :: 'a)" |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
243 |
by (simp add: CARD_eq of_nat_eq zero_def) |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
244 |
next |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
245 |
fix n assume "of_nat n = (0 :: 'a)" |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
246 |
thus "CARD('a) dvd n" |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
247 |
by (metis CARD_eq Rep_0 Rep_Abs_mod Rep_le_n mod_0_imp_dvd nat_dvd_iff of_nat_eq) |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
248 |
qed |
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
249 |
|
29997 | 250 |
end |
251 |
||
252 |
||
60500 | 253 |
subsection \<open>Ring class instances\<close> |
29997 | 254 |
|
60500 | 255 |
text \<open> |
61585 | 256 |
Unfortunately \<open>ring_1\<close> instance is not possible for |
69593 | 257 |
\<^typ>\<open>num1\<close>, since 0 and 1 are not distinct. |
60500 | 258 |
\<close> |
30032 | 259 |
|
29997 | 260 |
instantiation |
30960 | 261 |
bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}" |
29997 | 262 |
begin |
263 |
||
264 |
definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where |
|
29998 | 265 |
"Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))" |
29997 | 266 |
|
267 |
definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where |
|
29998 | 268 |
"Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))" |
29997 | 269 |
|
270 |
definition "0 = Abs_bit0 0" |
|
271 |
definition "1 = Abs_bit0 1" |
|
272 |
definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)" |
|
273 |
definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)" |
|
274 |
definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)" |
|
275 |
definition "- x = Abs_bit0' (- Rep_bit0 x)" |
|
276 |
||
277 |
definition "0 = Abs_bit1 0" |
|
278 |
definition "1 = Abs_bit1 1" |
|
279 |
definition "x + y = Abs_bit1' (Rep_bit1 x + Rep_bit1 y)" |
|
280 |
definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)" |
|
281 |
definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)" |
|
282 |
definition "- x = Abs_bit1' (- Rep_bit1 x)" |
|
283 |
||
284 |
instance .. |
|
285 |
||
286 |
end |
|
287 |
||
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset
|
288 |
interpretation bit0: |
29998 | 289 |
mod_type "int CARD('a::finite bit0)" |
29997 | 290 |
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" |
291 |
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" |
|
292 |
apply (rule mod_type.intro) |
|
66936 | 293 |
apply (simp add: type_definition_bit0) |
30001 | 294 |
apply (rule one_less_int_card) |
29997 | 295 |
apply (rule zero_bit0_def) |
296 |
apply (rule one_bit0_def) |
|
297 |
apply (rule plus_bit0_def [unfolded Abs_bit0'_def]) |
|
298 |
apply (rule times_bit0_def [unfolded Abs_bit0'_def]) |
|
299 |
apply (rule minus_bit0_def [unfolded Abs_bit0'_def]) |
|
300 |
apply (rule uminus_bit0_def [unfolded Abs_bit0'_def]) |
|
301 |
done |
|
302 |
||
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset
|
303 |
interpretation bit1: |
29998 | 304 |
mod_type "int CARD('a::finite bit1)" |
29997 | 305 |
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" |
306 |
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" |
|
307 |
apply (rule mod_type.intro) |
|
66936 | 308 |
apply (simp add: type_definition_bit1) |
30001 | 309 |
apply (rule one_less_int_card) |
29997 | 310 |
apply (rule zero_bit1_def) |
311 |
apply (rule one_bit1_def) |
|
312 |
apply (rule plus_bit1_def [unfolded Abs_bit1'_def]) |
|
313 |
apply (rule times_bit1_def [unfolded Abs_bit1'_def]) |
|
314 |
apply (rule minus_bit1_def [unfolded Abs_bit1'_def]) |
|
315 |
apply (rule uminus_bit1_def [unfolded Abs_bit1'_def]) |
|
316 |
done |
|
317 |
||
31021 | 318 |
instance bit0 :: (finite) comm_ring_1 |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
319 |
by (rule bit0.comm_ring_1) |
29997 | 320 |
|
31021 | 321 |
instance bit1 :: (finite) comm_ring_1 |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
322 |
by (rule bit1.comm_ring_1) |
29997 | 323 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset
|
324 |
interpretation bit0: |
29998 | 325 |
mod_ring "int CARD('a::finite bit0)" |
29997 | 326 |
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" |
327 |
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" |
|
328 |
.. |
|
329 |
||
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset
|
330 |
interpretation bit1: |
29998 | 331 |
mod_ring "int CARD('a::finite bit1)" |
29997 | 332 |
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" |
333 |
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" |
|
334 |
.. |
|
335 |
||
60500 | 336 |
text \<open>Set up cases, induction, and arithmetic\<close> |
29997 | 337 |
|
29999 | 338 |
lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases |
339 |
lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases |
|
29997 | 340 |
|
29999 | 341 |
lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct |
342 |
lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct |
|
29997 | 343 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
344 |
lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset
|
345 |
lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral |
29997 | 346 |
|
55142 | 347 |
lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit0"] for dummy :: "'a::finite" |
348 |
lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit1"] for dummy :: "'a::finite" |
|
29997 | 349 |
|
60500 | 350 |
subsection \<open>Order instances\<close> |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
351 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
352 |
instantiation bit0 and bit1 :: (finite) linorder begin |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
353 |
definition "a < b \<longleftrightarrow> Rep_bit0 a < Rep_bit0 b" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
354 |
definition "a \<le> b \<longleftrightarrow> Rep_bit0 a \<le> Rep_bit0 b" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
355 |
definition "a < b \<longleftrightarrow> Rep_bit1 a < Rep_bit1 b" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
356 |
definition "a \<le> b \<longleftrightarrow> Rep_bit1 a \<le> Rep_bit1 b" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
357 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
358 |
instance |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
359 |
by(intro_classes) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
360 |
(auto simp add: less_eq_bit0_def less_bit0_def less_eq_bit1_def less_bit1_def Rep_bit0_inject Rep_bit1_inject) |
51288
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
361 |
end |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
362 |
|
67399 | 363 |
lemma (in preorder) tranclp_less: "(<) \<^sup>+\<^sup>+ = (<)" |
51288
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
364 |
by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct) |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
365 |
|
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
366 |
instance bit0 and bit1 :: (finite) wellorder |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
367 |
proof - |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
368 |
have "wf {(x :: 'a bit0, y). x < y}" |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
369 |
by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI) |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
370 |
thus "OFCLASS('a bit0, wellorder_class)" |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
371 |
by(rule wf_wellorderI) intro_classes |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
372 |
next |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
373 |
have "wf {(x :: 'a bit1, y). x < y}" |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
374 |
by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI) |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
375 |
thus "OFCLASS('a bit1, wellorder_class)" |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
376 |
by(rule wf_wellorderI) intro_classes |
be7e9a675ec9
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
Andreas Lochbihler
parents:
51175
diff
changeset
|
377 |
qed |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
378 |
|
60500 | 379 |
subsection \<open>Code setup and type classes for code generation\<close> |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
380 |
|
69593 | 381 |
text \<open>Code setup for \<^typ>\<open>num0\<close> and \<^typ>\<open>num1\<close>\<close> |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
382 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
383 |
definition Num0 :: num0 where "Num0 = Abs_num0 0" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
384 |
code_datatype Num0 |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
385 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
386 |
instantiation num0 :: equal begin |
52143 | 387 |
definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool" |
67399 | 388 |
where "equal_num0 = (=)" |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
389 |
instance by intro_classes (simp add: equal_num0_def) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
390 |
end |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
391 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
392 |
lemma equal_num0_code [code]: |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
393 |
"equal_class.equal Num0 Num0 = True" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
394 |
by(rule equal_refl) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
395 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
396 |
code_datatype "1 :: num1" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
397 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
398 |
instantiation num1 :: equal begin |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
399 |
definition equal_num1 :: "num1 \<Rightarrow> num1 \<Rightarrow> bool" |
67399 | 400 |
where "equal_num1 = (=)" |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
401 |
instance by intro_classes (simp add: equal_num1_def) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
402 |
end |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
403 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
404 |
lemma equal_num1_code [code]: |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
405 |
"equal_class.equal (1 :: num1) 1 = True" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
406 |
by(rule equal_refl) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
407 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
408 |
instantiation num1 :: enum begin |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
409 |
definition "enum_class.enum = [1 :: num1]" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
410 |
definition "enum_class.enum_all P = P (1 :: num1)" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
411 |
definition "enum_class.enum_ex P = P (1 :: num1)" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
412 |
instance |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
413 |
by intro_classes |
69666 | 414 |
(auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def) |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
415 |
end |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
416 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
417 |
instantiation num0 and num1 :: card_UNIV begin |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
418 |
definition "finite_UNIV = Phantom(num0) False" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
419 |
definition "card_UNIV = Phantom(num0) 0" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
420 |
definition "finite_UNIV = Phantom(num1) True" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
421 |
definition "card_UNIV = Phantom(num1) 1" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
422 |
instance |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
423 |
by intro_classes |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
424 |
(simp_all add: finite_UNIV_num0_def card_UNIV_num0_def infinite_num0 finite_UNIV_num1_def card_UNIV_num1_def) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
425 |
end |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
426 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
427 |
|
69593 | 428 |
text \<open>Code setup for \<^typ>\<open>'a bit0\<close> and \<^typ>\<open>'a bit1\<close>\<close> |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
429 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
430 |
declare |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
431 |
bit0.Rep_inverse[code abstype] |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
432 |
bit0.Rep_0[code abstract] |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
433 |
bit0.Rep_1[code abstract] |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
434 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
435 |
lemma Abs_bit0'_code [code abstract]: |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
436 |
"Rep_bit0 (Abs_bit0' x :: 'a :: finite bit0) = x mod int (CARD('a bit0))" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
437 |
by(auto simp add: Abs_bit0'_def intro!: Abs_bit0_inverse) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
438 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
439 |
lemma inj_on_Abs_bit0: |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
440 |
"inj_on (Abs_bit0 :: int \<Rightarrow> 'a bit0) {0..<2 * int CARD('a :: finite)}" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
441 |
by(auto intro: inj_onI simp add: Abs_bit0_inject) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
442 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
443 |
declare |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
444 |
bit1.Rep_inverse[code abstype] |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
445 |
bit1.Rep_0[code abstract] |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
446 |
bit1.Rep_1[code abstract] |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
447 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
448 |
lemma Abs_bit1'_code [code abstract]: |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
449 |
"Rep_bit1 (Abs_bit1' x :: 'a :: finite bit1) = x mod int (CARD('a bit1))" |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
450 |
by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse) |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
451 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
452 |
lemma inj_on_Abs_bit1: |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
453 |
"inj_on (Abs_bit1 :: int \<Rightarrow> 'a bit1) {0..<1 + 2 * int CARD('a :: finite)}" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
454 |
by(auto intro: inj_onI simp add: Abs_bit1_inject) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
455 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
456 |
instantiation bit0 and bit1 :: (finite) equal begin |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
457 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
458 |
definition "equal_class.equal x y \<longleftrightarrow> Rep_bit0 x = Rep_bit0 y" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
459 |
definition "equal_class.equal x y \<longleftrightarrow> Rep_bit1 x = Rep_bit1 y" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
460 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
461 |
instance |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
462 |
by intro_classes (simp_all add: equal_bit0_def equal_bit1_def Rep_bit0_inject Rep_bit1_inject) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
463 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
464 |
end |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
465 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
466 |
instantiation bit0 :: (finite) enum begin |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
467 |
definition "(enum_class.enum :: 'a bit0 list) = map (Abs_bit0' \<circ> int) (upt 0 (CARD('a bit0)))" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
468 |
definition "enum_class.enum_all P = (\<forall>b :: 'a bit0 \<in> set enum_class.enum. P b)" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
469 |
definition "enum_class.enum_ex P = (\<exists>b :: 'a bit0 \<in> set enum_class.enum. P b)" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
470 |
|
69661 | 471 |
instance proof |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
472 |
show "distinct (enum_class.enum :: 'a bit0 list)" |
66936 | 473 |
by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject) |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
474 |
|
69661 | 475 |
let ?Abs = "Abs_bit0 :: _ \<Rightarrow> 'a bit0" |
476 |
interpret type_definition Rep_bit0 ?Abs "{0..<2 * int CARD('a)}" |
|
477 |
by (fact type_definition_bit0) |
|
478 |
have "UNIV = ?Abs ` {0..<2 * int CARD('a)}" |
|
479 |
by (simp add: Abs_image) |
|
480 |
also have "\<dots> = ?Abs ` (int ` {0..<2 * CARD('a)})" |
|
481 |
by (simp add: image_int_atLeastLessThan) |
|
482 |
also have "\<dots> = (?Abs \<circ> int) ` {0..<2 * CARD('a)}" |
|
483 |
by (simp add: image_image cong: image_cong) |
|
484 |
also have "\<dots> = set enum_class.enum" |
|
485 |
by (simp add: enum_bit0_def Abs_bit0'_def cong: image_cong_simp) |
|
486 |
finally show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum" . |
|
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
487 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
488 |
fix P :: "'a bit0 \<Rightarrow> bool" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
489 |
show "enum_class.enum_all P = Ball UNIV P" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
490 |
and "enum_class.enum_ex P = Bex UNIV P" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
491 |
by(simp_all add: enum_all_bit0_def enum_ex_bit0_def univ_eq) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
492 |
qed |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
493 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
494 |
end |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
495 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
496 |
instantiation bit1 :: (finite) enum begin |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
497 |
definition "(enum_class.enum :: 'a bit1 list) = map (Abs_bit1' \<circ> int) (upt 0 (CARD('a bit1)))" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
498 |
definition "enum_class.enum_all P = (\<forall>b :: 'a bit1 \<in> set enum_class.enum. P b)" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
499 |
definition "enum_class.enum_ex P = (\<exists>b :: 'a bit1 \<in> set enum_class.enum. P b)" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
500 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
501 |
instance |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
502 |
proof(intro_classes) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
503 |
show "distinct (enum_class.enum :: 'a bit1 list)" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
504 |
by(simp only: Abs_bit1'_def zmod_int[symmetric] enum_bit1_def distinct_map Suc_eq_plus1 card_bit1 o_apply inj_on_def) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
505 |
(clarsimp simp add: Abs_bit1_inject) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
506 |
|
69661 | 507 |
let ?Abs = "Abs_bit1 :: _ \<Rightarrow> 'a bit1" |
508 |
interpret type_definition Rep_bit1 ?Abs "{0..<1 + 2 * int CARD('a)}" |
|
509 |
by (fact type_definition_bit1) |
|
510 |
have "UNIV = ?Abs ` {0..<1 + 2 * int CARD('a)}" |
|
511 |
by (simp add: Abs_image) |
|
512 |
also have "\<dots> = ?Abs ` (int ` {0..<1 + 2 * CARD('a)})" |
|
513 |
by (simp add: image_int_atLeastLessThan) |
|
514 |
also have "\<dots> = (?Abs \<circ> int) ` {0..<1 + 2 * CARD('a)}" |
|
515 |
by (simp add: image_image cong: image_cong) |
|
516 |
finally show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum" |
|
517 |
by (simp only: enum_bit1_def set_map set_upt) (simp add: Abs_bit1'_def cong: image_cong_simp) |
|
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
518 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
519 |
fix P :: "'a bit1 \<Rightarrow> bool" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
520 |
show "enum_class.enum_all P = Ball UNIV P" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
521 |
and "enum_class.enum_ex P = Bex UNIV P" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
522 |
by(simp_all add: enum_all_bit1_def enum_ex_bit1_def univ_eq) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
523 |
qed |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
524 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
525 |
end |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
526 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
527 |
instantiation bit0 and bit1 :: (finite) finite_UNIV begin |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
528 |
definition "finite_UNIV = Phantom('a bit0) True" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
529 |
definition "finite_UNIV = Phantom('a bit1) True" |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
530 |
instance by intro_classes (simp_all add: finite_UNIV_bit0_def finite_UNIV_bit1_def) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
531 |
end |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
532 |
|
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
533 |
instantiation bit0 and bit1 :: ("{finite,card_UNIV}") card_UNIV begin |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
534 |
definition "card_UNIV = Phantom('a bit0) (2 * of_phantom (card_UNIV :: 'a card_UNIV))" |
51175
9f472d5f112c
simplify definition as sort constraints ensure finiteness (thanks to Jesus Aransay)
Andreas Lochbihler
parents:
51153
diff
changeset
|
535 |
definition "card_UNIV = Phantom('a bit1) (1 + 2 * of_phantom (card_UNIV :: 'a card_UNIV))" |
51153
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
536 |
instance by intro_classes (simp_all add: card_UNIV_bit0_def card_UNIV_bit1_def card_UNIV) |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
537 |
end |
b14ee572cc7b
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler
parents:
49834
diff
changeset
|
538 |
|
60500 | 539 |
subsection \<open>Syntax\<close> |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
540 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
541 |
syntax |
46236
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
37653
diff
changeset
|
542 |
"_NumeralType" :: "num_token => type" ("_") |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
543 |
"_NumeralType0" :: type ("0") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
544 |
"_NumeralType1" :: type ("1") |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
545 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
546 |
translations |
35362 | 547 |
(type) "1" == (type) "num1" |
548 |
(type) "0" == (type) "num0" |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
549 |
|
60500 | 550 |
parse_translation \<open> |
52143 | 551 |
let |
552 |
fun mk_bintype n = |
|
553 |
let |
|
69593 | 554 |
fun mk_bit 0 = Syntax.const \<^type_syntax>\<open>bit0\<close> |
555 |
| mk_bit 1 = Syntax.const \<^type_syntax>\<open>bit1\<close>; |
|
52143 | 556 |
fun bin_of n = |
69593 | 557 |
if n = 1 then Syntax.const \<^type_syntax>\<open>num1\<close> |
558 |
else if n = 0 then Syntax.const \<^type_syntax>\<open>num0\<close> |
|
52143 | 559 |
else if n = ~1 then raise TERM ("negative type numeral", []) |
560 |
else |
|
561 |
let val (q, r) = Integer.div_mod n 2; |
|
562 |
in mk_bit r $ bin_of q end; |
|
563 |
in bin_of n end; |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
564 |
|
52143 | 565 |
fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str)) |
566 |
| 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
|
567 |
|
69593 | 568 |
in [(\<^syntax_const>\<open>_NumeralType\<close>, K numeral_tr)] end |
60500 | 569 |
\<close> |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
570 |
|
60500 | 571 |
print_translation \<open> |
52143 | 572 |
let |
573 |
fun int_of [] = 0 |
|
574 |
| 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
|
575 |
|
69593 | 576 |
fun bin_of (Const (\<^type_syntax>\<open>num0\<close>, _)) = [] |
577 |
| bin_of (Const (\<^type_syntax>\<open>num1\<close>, _)) = [1] |
|
578 |
| bin_of (Const (\<^type_syntax>\<open>bit0\<close>, _) $ bs) = 0 :: bin_of bs |
|
579 |
| bin_of (Const (\<^type_syntax>\<open>bit1\<close>, _) $ bs) = 1 :: bin_of bs |
|
52143 | 580 |
| 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
|
581 |
|
52143 | 582 |
fun bit_tr' b [t] = |
583 |
let |
|
584 |
val rev_digs = b :: bin_of t handle TERM _ => raise Match |
|
585 |
val i = int_of rev_digs; |
|
586 |
val num = string_of_int (abs i); |
|
587 |
in |
|
69593 | 588 |
Syntax.const \<^syntax_const>\<open>_NumeralType\<close> $ Syntax.free num |
52143 | 589 |
end |
590 |
| bit_tr' b _ = raise Match; |
|
591 |
in |
|
69593 | 592 |
[(\<^type_syntax>\<open>bit0\<close>, K (bit_tr' 0)), |
593 |
(\<^type_syntax>\<open>bit1\<close>, K (bit_tr' 1))] |
|
69216
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
67411
diff
changeset
|
594 |
end |
60500 | 595 |
\<close> |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
596 |
|
60500 | 597 |
subsection \<open>Examples\<close> |
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
598 |
|
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
599 |
lemma "CARD(0) = 0" by simp |
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
600 |
lemma "CARD(17) = 17" by simp |
73109
783406dd051e
some algebra material for HOL: characteristic of a ring, algebraic integers
Manuel Eberl <eberlm@in.tum.de>
parents:
69678
diff
changeset
|
601 |
lemma "CHAR(23) = 23" by simp |
29997 | 602 |
lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp |
28920 | 603 |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset
|
604 |
end |