author | haftmann |
Tue, 12 May 2009 21:17:47 +0200 | |
changeset 31129 | d2cead76fca2 |
parent 31029 | e564767f8f78 |
child 31902 | 862ae16a799d |
permissions | -rw-r--r-- |
28021 | 1 |
(* Title: HOL/ex/Numeral.thy |
2 |
Author: Florian Haftmann |
|
29947 | 3 |
*) |
28021 | 4 |
|
29947 | 5 |
header {* An experimental alternative numeral representation. *} |
28021 | 6 |
|
7 |
theory Numeral |
|
8 |
imports Int Inductive |
|
9 |
begin |
|
10 |
||
11 |
subsection {* The @{text num} type *} |
|
12 |
||
29943 | 13 |
datatype num = One | Dig0 num | Dig1 num |
14 |
||
15 |
text {* Increment function for type @{typ num} *} |
|
16 |
||
31021 | 17 |
primrec inc :: "num \<Rightarrow> num" where |
29943 | 18 |
"inc One = Dig0 One" |
19 |
| "inc (Dig0 x) = Dig1 x" |
|
20 |
| "inc (Dig1 x) = Dig0 (inc x)" |
|
21 |
||
22 |
text {* Converting between type @{typ num} and type @{typ nat} *} |
|
23 |
||
31021 | 24 |
primrec nat_of_num :: "num \<Rightarrow> nat" where |
29943 | 25 |
"nat_of_num One = Suc 0" |
26 |
| "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x" |
|
27 |
| "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)" |
|
28 |
||
31021 | 29 |
primrec num_of_nat :: "nat \<Rightarrow> num" where |
29943 | 30 |
"num_of_nat 0 = One" |
31 |
| "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)" |
|
32 |
||
29945 | 33 |
lemma nat_of_num_pos: "0 < nat_of_num x" |
29943 | 34 |
by (induct x) simp_all |
35 |
||
31028 | 36 |
lemma nat_of_num_neq_0: "nat_of_num x \<noteq> 0" |
29943 | 37 |
by (induct x) simp_all |
38 |
||
39 |
lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)" |
|
40 |
by (induct x) simp_all |
|
41 |
||
42 |
lemma num_of_nat_double: |
|
43 |
"0 < n \<Longrightarrow> num_of_nat (n + n) = Dig0 (num_of_nat n)" |
|
44 |
by (induct n) simp_all |
|
45 |
||
28021 | 46 |
text {* |
29943 | 47 |
Type @{typ num} is isomorphic to the strictly positive |
28021 | 48 |
natural numbers. |
49 |
*} |
|
50 |
||
29943 | 51 |
lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x" |
29945 | 52 |
by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos) |
28021 | 53 |
|
29943 | 54 |
lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n" |
55 |
by (induct n) (simp_all add: nat_of_num_inc) |
|
28021 | 56 |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
57 |
lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y" |
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
58 |
apply safe |
29943 | 59 |
apply (drule arg_cong [where f=num_of_nat]) |
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
60 |
apply (simp add: nat_of_num_inverse) |
28021 | 61 |
done |
62 |
||
29943 | 63 |
lemma num_induct [case_names One inc]: |
64 |
fixes P :: "num \<Rightarrow> bool" |
|
65 |
assumes One: "P One" |
|
66 |
and inc: "\<And>x. P x \<Longrightarrow> P (inc x)" |
|
67 |
shows "P x" |
|
68 |
proof - |
|
69 |
obtain n where n: "Suc n = nat_of_num x" |
|
70 |
by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0) |
|
71 |
have "P (num_of_nat (Suc n))" |
|
72 |
proof (induct n) |
|
73 |
case 0 show ?case using One by simp |
|
28021 | 74 |
next |
29943 | 75 |
case (Suc n) |
76 |
then have "P (inc (num_of_nat (Suc n)))" by (rule inc) |
|
77 |
then show "P (num_of_nat (Suc (Suc n)))" by simp |
|
28021 | 78 |
qed |
29943 | 79 |
with n show "P x" |
80 |
by (simp add: nat_of_num_inverse) |
|
28021 | 81 |
qed |
82 |
||
83 |
text {* |
|
84 |
From now on, there are two possible models for @{typ num}: |
|
29943 | 85 |
as positive naturals (rule @{text "num_induct"}) |
28021 | 86 |
and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}). |
87 |
||
88 |
It is not entirely clear in which context it is better to use |
|
89 |
the one or the other, or whether the construction should be reversed. |
|
90 |
*} |
|
91 |
||
92 |
||
29945 | 93 |
subsection {* Numeral operations *} |
28021 | 94 |
|
95 |
ML {* |
|
96 |
structure DigSimps = |
|
97 |
NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals") |
|
98 |
*} |
|
99 |
||
100 |
setup DigSimps.setup |
|
101 |
||
29945 | 102 |
instantiation num :: "{plus,times,ord}" |
103 |
begin |
|
28021 | 104 |
|
105 |
definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where |
|
28562 | 106 |
[code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)" |
28021 | 107 |
|
108 |
definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where |
|
28562 | 109 |
[code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)" |
28021 | 110 |
|
29945 | 111 |
definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where |
112 |
[code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n" |
|
28021 | 113 |
|
29945 | 114 |
definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where |
115 |
[code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n" |
|
28021 | 116 |
|
29945 | 117 |
instance .. |
28021 | 118 |
|
119 |
end |
|
120 |
||
29945 | 121 |
lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y" |
122 |
unfolding plus_num_def |
|
123 |
by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos) |
|
124 |
||
125 |
lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y" |
|
126 |
unfolding times_num_def |
|
127 |
by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos) |
|
28021 | 128 |
|
29945 | 129 |
lemma Dig_plus [numeral, simp, code]: |
130 |
"One + One = Dig0 One" |
|
131 |
"One + Dig0 m = Dig1 m" |
|
132 |
"One + Dig1 m = Dig0 (m + One)" |
|
133 |
"Dig0 n + One = Dig1 n" |
|
134 |
"Dig0 n + Dig0 m = Dig0 (n + m)" |
|
135 |
"Dig0 n + Dig1 m = Dig1 (n + m)" |
|
136 |
"Dig1 n + One = Dig0 (n + One)" |
|
137 |
"Dig1 n + Dig0 m = Dig1 (n + m)" |
|
138 |
"Dig1 n + Dig1 m = Dig0 (n + m + One)" |
|
139 |
by (simp_all add: num_eq_iff nat_of_num_add) |
|
28021 | 140 |
|
29945 | 141 |
lemma Dig_times [numeral, simp, code]: |
142 |
"One * One = One" |
|
143 |
"One * Dig0 n = Dig0 n" |
|
144 |
"One * Dig1 n = Dig1 n" |
|
145 |
"Dig0 n * One = Dig0 n" |
|
146 |
"Dig0 n * Dig0 m = Dig0 (n * Dig0 m)" |
|
147 |
"Dig0 n * Dig1 m = Dig0 (n * Dig1 m)" |
|
148 |
"Dig1 n * One = Dig1 n" |
|
149 |
"Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)" |
|
150 |
"Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)" |
|
151 |
by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult |
|
152 |
left_distrib right_distrib) |
|
28021 | 153 |
|
29991 | 154 |
lemma Dig_eq: |
155 |
"One = One \<longleftrightarrow> True" |
|
156 |
"One = Dig0 n \<longleftrightarrow> False" |
|
157 |
"One = Dig1 n \<longleftrightarrow> False" |
|
158 |
"Dig0 m = One \<longleftrightarrow> False" |
|
159 |
"Dig1 m = One \<longleftrightarrow> False" |
|
160 |
"Dig0 m = Dig0 n \<longleftrightarrow> m = n" |
|
161 |
"Dig0 m = Dig1 n \<longleftrightarrow> False" |
|
162 |
"Dig1 m = Dig0 n \<longleftrightarrow> False" |
|
163 |
"Dig1 m = Dig1 n \<longleftrightarrow> m = n" |
|
164 |
by simp_all |
|
165 |
||
29945 | 166 |
lemma less_eq_num_code [numeral, simp, code]: |
167 |
"One \<le> n \<longleftrightarrow> True" |
|
168 |
"Dig0 m \<le> One \<longleftrightarrow> False" |
|
169 |
"Dig1 m \<le> One \<longleftrightarrow> False" |
|
170 |
"Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n" |
|
171 |
"Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n" |
|
172 |
"Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n" |
|
173 |
"Dig1 m \<le> Dig0 n \<longleftrightarrow> m < n" |
|
174 |
using nat_of_num_pos [of n] nat_of_num_pos [of m] |
|
175 |
by (auto simp add: less_eq_num_def less_num_def) |
|
176 |
||
177 |
lemma less_num_code [numeral, simp, code]: |
|
178 |
"m < One \<longleftrightarrow> False" |
|
179 |
"One < One \<longleftrightarrow> False" |
|
180 |
"One < Dig0 n \<longleftrightarrow> True" |
|
181 |
"One < Dig1 n \<longleftrightarrow> True" |
|
182 |
"Dig0 m < Dig0 n \<longleftrightarrow> m < n" |
|
183 |
"Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n" |
|
184 |
"Dig1 m < Dig1 n \<longleftrightarrow> m < n" |
|
185 |
"Dig1 m < Dig0 n \<longleftrightarrow> m < n" |
|
186 |
using nat_of_num_pos [of n] nat_of_num_pos [of m] |
|
187 |
by (auto simp add: less_eq_num_def less_num_def) |
|
188 |
||
189 |
text {* Rules using @{text One} and @{text inc} as constructors *} |
|
28021 | 190 |
|
29945 | 191 |
lemma add_One: "x + One = inc x" |
192 |
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
|
193 |
||
194 |
lemma add_inc: "x + inc y = inc (x + y)" |
|
195 |
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
|
196 |
||
197 |
lemma mult_One: "x * One = x" |
|
198 |
by (simp add: num_eq_iff nat_of_num_mult) |
|
199 |
||
200 |
lemma mult_inc: "x * inc y = x * y + x" |
|
201 |
by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc) |
|
202 |
||
203 |
text {* A double-and-decrement function *} |
|
28021 | 204 |
|
29945 | 205 |
primrec DigM :: "num \<Rightarrow> num" where |
206 |
"DigM One = One" |
|
207 |
| "DigM (Dig0 n) = Dig1 (DigM n)" |
|
208 |
| "DigM (Dig1 n) = Dig1 (Dig0 n)" |
|
28021 | 209 |
|
29945 | 210 |
lemma DigM_plus_one: "DigM n + One = Dig0 n" |
211 |
by (induct n) simp_all |
|
212 |
||
213 |
lemma add_One_commute: "One + n = n + One" |
|
214 |
by (induct n) simp_all |
|
215 |
||
216 |
lemma one_plus_DigM: "One + DigM n = Dig0 n" |
|
217 |
unfolding add_One_commute DigM_plus_one .. |
|
28021 | 218 |
|
29954 | 219 |
text {* Squaring and exponentiation *} |
29947 | 220 |
|
221 |
primrec square :: "num \<Rightarrow> num" where |
|
222 |
"square One = One" |
|
223 |
| "square (Dig0 n) = Dig0 (Dig0 (square n))" |
|
224 |
| "square (Dig1 n) = Dig1 (Dig0 (square n + n))" |
|
225 |
||
29954 | 226 |
primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" |
227 |
where |
|
228 |
"pow x One = x" |
|
229 |
| "pow x (Dig0 y) = square (pow x y)" |
|
230 |
| "pow x (Dig1 y) = x * square (pow x y)" |
|
29947 | 231 |
|
28021 | 232 |
|
233 |
subsection {* Binary numerals *} |
|
234 |
||
235 |
text {* |
|
236 |
We embed binary representations into a generic algebraic |
|
29934 | 237 |
structure using @{text of_num}. |
28021 | 238 |
*} |
239 |
||
240 |
class semiring_numeral = semiring + monoid_mult |
|
241 |
begin |
|
242 |
||
243 |
primrec of_num :: "num \<Rightarrow> 'a" where |
|
31028 | 244 |
of_num_One [numeral]: "of_num One = 1" |
28021 | 245 |
| "of_num (Dig0 n) = of_num n + of_num n" |
246 |
| "of_num (Dig1 n) = of_num n + of_num n + 1" |
|
247 |
||
29943 | 248 |
lemma of_num_inc: "of_num (inc x) = of_num x + 1" |
249 |
by (induct x) (simp_all add: add_ac) |
|
250 |
||
31028 | 251 |
lemma of_num_add: "of_num (m + n) = of_num m + of_num n" |
252 |
apply (induct n rule: num_induct) |
|
253 |
apply (simp_all add: add_One add_inc of_num_inc add_ac) |
|
254 |
done |
|
255 |
||
256 |
lemma of_num_mult: "of_num (m * n) = of_num m * of_num n" |
|
257 |
apply (induct n rule: num_induct) |
|
258 |
apply (simp add: mult_One) |
|
259 |
apply (simp add: mult_inc of_num_add of_num_inc right_distrib) |
|
260 |
done |
|
261 |
||
28021 | 262 |
declare of_num.simps [simp del] |
263 |
||
264 |
end |
|
265 |
||
266 |
text {* |
|
267 |
ML stuff and syntax. |
|
268 |
*} |
|
269 |
||
270 |
ML {* |
|
31027 | 271 |
fun mk_num k = |
272 |
if k > 1 then |
|
273 |
let |
|
274 |
val (l, b) = Integer.div_mod k 2; |
|
275 |
val bit = (if b = 0 then @{term Dig0} else @{term Dig1}); |
|
276 |
in bit $ (mk_num l) end |
|
277 |
else if k = 1 then @{term One} |
|
278 |
else error ("mk_num " ^ string_of_int k); |
|
28021 | 279 |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
280 |
fun dest_num @{term One} = 1 |
28021 | 281 |
| dest_num (@{term Dig0} $ n) = 2 * dest_num n |
31027 | 282 |
| dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1 |
283 |
| dest_num t = raise TERM ("dest_num", [t]); |
|
28021 | 284 |
|
285 |
(*FIXME these have to gain proper context via morphisms phi*) |
|
286 |
||
287 |
fun mk_numeral T k = Const (@{const_name of_num}, @{typ num} --> T) |
|
288 |
$ mk_num k |
|
289 |
||
290 |
fun dest_numeral (Const (@{const_name of_num}, Type ("fun", [@{typ num}, T])) $ t) = |
|
291 |
(T, dest_num t) |
|
292 |
*} |
|
293 |
||
294 |
syntax |
|
295 |
"_Numerals" :: "xnum \<Rightarrow> 'a" ("_") |
|
296 |
||
297 |
parse_translation {* |
|
298 |
let |
|
299 |
fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2) |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
300 |
of (0, 1) => Const (@{const_name One}, dummyT) |
28021 | 301 |
| (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n |
302 |
| (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n |
|
303 |
else raise Match; |
|
304 |
fun numeral_tr [Free (num, _)] = |
|
305 |
let |
|
306 |
val {leading_zeros, value, ...} = Syntax.read_xnum num; |
|
307 |
val _ = leading_zeros = 0 andalso value > 0 |
|
308 |
orelse error ("Bad numeral: " ^ num); |
|
309 |
in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end |
|
310 |
| numeral_tr ts = raise TERM ("numeral_tr", ts); |
|
311 |
in [("_Numerals", numeral_tr)] end |
|
312 |
*} |
|
313 |
||
314 |
typed_print_translation {* |
|
315 |
let |
|
316 |
fun dig b n = b + 2 * n; |
|
317 |
fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) = |
|
318 |
dig 0 (int_of_num' n) |
|
319 |
| int_of_num' (Const (@{const_syntax Dig1}, _) $ n) = |
|
320 |
dig 1 (int_of_num' n) |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
321 |
| int_of_num' (Const (@{const_syntax One}, _)) = 1; |
28021 | 322 |
fun num_tr' show_sorts T [n] = |
323 |
let |
|
324 |
val k = int_of_num' n; |
|
325 |
val t' = Syntax.const "_Numerals" $ Syntax.free ("#" ^ string_of_int k); |
|
326 |
in case T |
|
327 |
of Type ("fun", [_, T']) => |
|
328 |
if not (! show_types) andalso can Term.dest_Type T' then t' |
|
329 |
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T' |
|
330 |
| T' => if T' = dummyT then t' else raise Match |
|
331 |
end; |
|
332 |
in [(@{const_syntax of_num}, num_tr')] end |
|
333 |
*} |
|
334 |
||
29945 | 335 |
subsection {* Class-specific numeral rules *} |
28021 | 336 |
|
337 |
text {* |
|
338 |
@{const of_num} is a morphism. |
|
339 |
*} |
|
340 |
||
29945 | 341 |
subsubsection {* Class @{text semiring_numeral} *} |
342 |
||
28021 | 343 |
context semiring_numeral |
344 |
begin |
|
345 |
||
29943 | 346 |
abbreviation "Num1 \<equiv> of_num One" |
28021 | 347 |
|
348 |
text {* |
|
349 |
Alas, there is still the duplication of @{term 1}, |
|
350 |
thought the duplicated @{term 0} has disappeared. |
|
351 |
We could get rid of it by replacing the constructor |
|
352 |
@{term 1} in @{typ num} by two constructors |
|
353 |
@{text two} and @{text three}, resulting in a further |
|
354 |
blow-up. But it could be worth the effort. |
|
355 |
*} |
|
356 |
||
357 |
lemma of_num_plus_one [numeral]: |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
358 |
"of_num n + 1 = of_num (n + One)" |
31028 | 359 |
by (simp only: of_num_add of_num_One) |
28021 | 360 |
|
361 |
lemma of_num_one_plus [numeral]: |
|
31028 | 362 |
"1 + of_num n = of_num (One + n)" |
363 |
by (simp only: of_num_add of_num_One) |
|
28021 | 364 |
|
365 |
lemma of_num_plus [numeral]: |
|
366 |
"of_num m + of_num n = of_num (m + n)" |
|
31028 | 367 |
unfolding of_num_add .. |
28021 | 368 |
|
369 |
lemma of_num_times_one [numeral]: |
|
370 |
"of_num n * 1 = of_num n" |
|
371 |
by simp |
|
372 |
||
373 |
lemma of_num_one_times [numeral]: |
|
374 |
"1 * of_num n = of_num n" |
|
375 |
by simp |
|
376 |
||
377 |
lemma of_num_times [numeral]: |
|
378 |
"of_num m * of_num n = of_num (m * n)" |
|
31028 | 379 |
unfolding of_num_mult .. |
28021 | 380 |
|
381 |
end |
|
382 |
||
29945 | 383 |
subsubsection {* |
29947 | 384 |
Structures with a zero: class @{text semiring_1} |
28021 | 385 |
*} |
386 |
||
387 |
context semiring_1 |
|
388 |
begin |
|
389 |
||
390 |
subclass semiring_numeral .. |
|
391 |
||
392 |
lemma of_nat_of_num [numeral]: "of_nat (of_num n) = of_num n" |
|
393 |
by (induct n) |
|
394 |
(simp_all add: semiring_numeral_class.of_num.simps of_num.simps add_ac) |
|
395 |
||
396 |
declare of_nat_1 [numeral] |
|
397 |
||
398 |
lemma Dig_plus_zero [numeral]: |
|
399 |
"0 + 1 = 1" |
|
400 |
"0 + of_num n = of_num n" |
|
401 |
"1 + 0 = 1" |
|
402 |
"of_num n + 0 = of_num n" |
|
403 |
by simp_all |
|
404 |
||
405 |
lemma Dig_times_zero [numeral]: |
|
406 |
"0 * 1 = 0" |
|
407 |
"0 * of_num n = 0" |
|
408 |
"1 * 0 = 0" |
|
409 |
"of_num n * 0 = 0" |
|
410 |
by simp_all |
|
411 |
||
412 |
end |
|
413 |
||
414 |
lemma nat_of_num_of_num: "nat_of_num = of_num" |
|
415 |
proof |
|
416 |
fix n |
|
29943 | 417 |
have "of_num n = nat_of_num n" |
418 |
by (induct n) (simp_all add: of_num.simps) |
|
28021 | 419 |
then show "nat_of_num n = of_num n" by simp |
420 |
qed |
|
421 |
||
29945 | 422 |
subsubsection {* |
423 |
Equality: class @{text semiring_char_0} |
|
28021 | 424 |
*} |
425 |
||
426 |
context semiring_char_0 |
|
427 |
begin |
|
428 |
||
31028 | 429 |
lemma of_num_eq_iff [numeral]: "of_num m = of_num n \<longleftrightarrow> m = n" |
28021 | 430 |
unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric] |
29943 | 431 |
of_nat_eq_iff num_eq_iff .. |
28021 | 432 |
|
31028 | 433 |
lemma of_num_eq_one_iff [numeral]: "of_num n = 1 \<longleftrightarrow> n = One" |
434 |
using of_num_eq_iff [of n One] by (simp add: of_num_One) |
|
28021 | 435 |
|
31028 | 436 |
lemma one_eq_of_num_iff [numeral]: "1 = of_num n \<longleftrightarrow> One = n" |
437 |
using of_num_eq_iff [of One n] by (simp add: of_num_One) |
|
28021 | 438 |
|
439 |
end |
|
440 |
||
29945 | 441 |
subsubsection {* |
442 |
Comparisons: class @{text ordered_semidom} |
|
28021 | 443 |
*} |
444 |
||
29945 | 445 |
text {* Could be perhaps more general than here. *} |
446 |
||
28021 | 447 |
context ordered_semidom |
448 |
begin |
|
449 |
||
29991 | 450 |
lemma of_num_pos [numeral]: "0 < of_num n" |
451 |
by (induct n) (simp_all add: of_num.simps add_pos_pos) |
|
452 |
||
28021 | 453 |
lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n" |
454 |
proof - |
|
455 |
have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n" |
|
456 |
unfolding less_eq_num_def nat_of_num_of_num of_nat_le_iff .. |
|
457 |
then show ?thesis by (simp add: of_nat_of_num) |
|
458 |
qed |
|
459 |
||
31028 | 460 |
lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n \<le> One" |
461 |
using of_num_less_eq_iff [of n One] by (simp add: of_num_One) |
|
28021 | 462 |
|
463 |
lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n" |
|
31028 | 464 |
using of_num_less_eq_iff [of One n] by (simp add: of_num_One) |
28021 | 465 |
|
466 |
lemma of_num_less_iff [numeral]: "of_num m < of_num n \<longleftrightarrow> m < n" |
|
467 |
proof - |
|
468 |
have "of_nat (of_num m) < of_nat (of_num n) \<longleftrightarrow> m < n" |
|
469 |
unfolding less_num_def nat_of_num_of_num of_nat_less_iff .. |
|
470 |
then show ?thesis by (simp add: of_nat_of_num) |
|
471 |
qed |
|
472 |
||
473 |
lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1" |
|
31028 | 474 |
using of_num_less_iff [of n One] by (simp add: of_num_One) |
28021 | 475 |
|
31028 | 476 |
lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> One < n" |
477 |
using of_num_less_iff [of One n] by (simp add: of_num_One) |
|
28021 | 478 |
|
29991 | 479 |
lemma of_num_nonneg [numeral]: "0 \<le> of_num n" |
480 |
by (induct n) (simp_all add: of_num.simps add_nonneg_nonneg) |
|
481 |
||
482 |
lemma of_num_less_zero_iff [numeral]: "\<not> of_num n < 0" |
|
483 |
by (simp add: not_less of_num_nonneg) |
|
484 |
||
485 |
lemma of_num_le_zero_iff [numeral]: "\<not> of_num n \<le> 0" |
|
486 |
by (simp add: not_le of_num_pos) |
|
487 |
||
488 |
end |
|
489 |
||
490 |
context ordered_idom |
|
491 |
begin |
|
492 |
||
30792 | 493 |
lemma minus_of_num_less_of_num_iff: "- of_num m < of_num n" |
29991 | 494 |
proof - |
495 |
have "- of_num m < 0" by (simp add: of_num_pos) |
|
496 |
also have "0 < of_num n" by (simp add: of_num_pos) |
|
497 |
finally show ?thesis . |
|
498 |
qed |
|
499 |
||
30792 | 500 |
lemma minus_of_num_less_one_iff: "- of_num n < 1" |
31028 | 501 |
using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_One) |
29991 | 502 |
|
30792 | 503 |
lemma minus_one_less_of_num_iff: "- 1 < of_num n" |
31028 | 504 |
using minus_of_num_less_of_num_iff [of One n] by (simp add: of_num_One) |
29991 | 505 |
|
30792 | 506 |
lemma minus_one_less_one_iff: "- 1 < 1" |
31028 | 507 |
using minus_of_num_less_of_num_iff [of One One] by (simp add: of_num_One) |
30792 | 508 |
|
509 |
lemma minus_of_num_le_of_num_iff: "- of_num m \<le> of_num n" |
|
29991 | 510 |
by (simp add: less_imp_le minus_of_num_less_of_num_iff) |
511 |
||
30792 | 512 |
lemma minus_of_num_le_one_iff: "- of_num n \<le> 1" |
29991 | 513 |
by (simp add: less_imp_le minus_of_num_less_one_iff) |
514 |
||
30792 | 515 |
lemma minus_one_le_of_num_iff: "- 1 \<le> of_num n" |
29991 | 516 |
by (simp add: less_imp_le minus_one_less_of_num_iff) |
517 |
||
30792 | 518 |
lemma minus_one_le_one_iff: "- 1 \<le> 1" |
519 |
by (simp add: less_imp_le minus_one_less_one_iff) |
|
520 |
||
521 |
lemma of_num_le_minus_of_num_iff: "\<not> of_num m \<le> - of_num n" |
|
29991 | 522 |
by (simp add: not_le minus_of_num_less_of_num_iff) |
523 |
||
30792 | 524 |
lemma one_le_minus_of_num_iff: "\<not> 1 \<le> - of_num n" |
29991 | 525 |
by (simp add: not_le minus_of_num_less_one_iff) |
526 |
||
30792 | 527 |
lemma of_num_le_minus_one_iff: "\<not> of_num n \<le> - 1" |
29991 | 528 |
by (simp add: not_le minus_one_less_of_num_iff) |
529 |
||
30792 | 530 |
lemma one_le_minus_one_iff: "\<not> 1 \<le> - 1" |
531 |
by (simp add: not_le minus_one_less_one_iff) |
|
532 |
||
533 |
lemma of_num_less_minus_of_num_iff: "\<not> of_num m < - of_num n" |
|
29991 | 534 |
by (simp add: not_less minus_of_num_le_of_num_iff) |
535 |
||
30792 | 536 |
lemma one_less_minus_of_num_iff: "\<not> 1 < - of_num n" |
29991 | 537 |
by (simp add: not_less minus_of_num_le_one_iff) |
538 |
||
30792 | 539 |
lemma of_num_less_minus_one_iff: "\<not> of_num n < - 1" |
29991 | 540 |
by (simp add: not_less minus_one_le_of_num_iff) |
541 |
||
30792 | 542 |
lemma one_less_minus_one_iff: "\<not> 1 < - 1" |
543 |
by (simp add: not_less minus_one_le_one_iff) |
|
544 |
||
545 |
lemmas le_signed_numeral_special [numeral] = |
|
546 |
minus_of_num_le_of_num_iff |
|
547 |
minus_of_num_le_one_iff |
|
548 |
minus_one_le_of_num_iff |
|
549 |
minus_one_le_one_iff |
|
550 |
of_num_le_minus_of_num_iff |
|
551 |
one_le_minus_of_num_iff |
|
552 |
of_num_le_minus_one_iff |
|
553 |
one_le_minus_one_iff |
|
554 |
||
555 |
lemmas less_signed_numeral_special [numeral] = |
|
556 |
minus_of_num_less_of_num_iff |
|
557 |
minus_of_num_less_one_iff |
|
558 |
minus_one_less_of_num_iff |
|
559 |
minus_one_less_one_iff |
|
560 |
of_num_less_minus_of_num_iff |
|
561 |
one_less_minus_of_num_iff |
|
562 |
of_num_less_minus_one_iff |
|
563 |
one_less_minus_one_iff |
|
564 |
||
28021 | 565 |
end |
566 |
||
29945 | 567 |
subsubsection {* |
29947 | 568 |
Structures with subtraction: class @{text semiring_1_minus} |
28021 | 569 |
*} |
570 |
||
571 |
class semiring_minus = semiring + minus + zero + |
|
572 |
assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a" |
|
573 |
assumes minus_minus_zero_inverts_plus1: "a + b = c \<Longrightarrow> b - c = 0 - a" |
|
574 |
begin |
|
575 |
||
576 |
lemma minus_inverts_plus2: "a + b = c \<Longrightarrow> c - a = b" |
|
577 |
by (simp add: add_ac minus_inverts_plus1 [of b a]) |
|
578 |
||
579 |
lemma minus_minus_zero_inverts_plus2: "a + b = c \<Longrightarrow> a - c = 0 - b" |
|
580 |
by (simp add: add_ac minus_minus_zero_inverts_plus1 [of b a]) |
|
581 |
||
582 |
end |
|
583 |
||
584 |
class semiring_1_minus = semiring_1 + semiring_minus |
|
585 |
begin |
|
586 |
||
587 |
lemma Dig_of_num_pos: |
|
588 |
assumes "k + n = m" |
|
589 |
shows "of_num m - of_num n = of_num k" |
|
590 |
using assms by (simp add: of_num_plus minus_inverts_plus1) |
|
591 |
||
592 |
lemma Dig_of_num_zero: |
|
593 |
shows "of_num n - of_num n = 0" |
|
594 |
by (rule minus_inverts_plus1) simp |
|
595 |
||
596 |
lemma Dig_of_num_neg: |
|
597 |
assumes "k + m = n" |
|
598 |
shows "of_num m - of_num n = 0 - of_num k" |
|
599 |
by (rule minus_minus_zero_inverts_plus1) (simp add: of_num_plus assms) |
|
600 |
||
601 |
lemmas Dig_plus_eval = |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
602 |
of_num_plus of_num_eq_iff Dig_plus refl [of One, THEN eqTrueI] num.inject |
28021 | 603 |
|
604 |
simproc_setup numeral_minus ("of_num m - of_num n") = {* |
|
605 |
let |
|
606 |
(*TODO proper implicit use of morphism via pattern antiquotations*) |
|
607 |
fun cdest_of_num ct = (snd o split_last o snd o Drule.strip_comb) ct; |
|
608 |
fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n); |
|
609 |
fun attach_num ct = (dest_num (Thm.term_of ct), ct); |
|
610 |
fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t; |
|
611 |
val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval}); |
|
612 |
fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"}, |
|
613 |
[Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]]; |
|
614 |
in fn phi => fn _ => fn ct => case try cdifference ct |
|
615 |
of NONE => (NONE) |
|
616 |
| SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0 |
|
617 |
then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct |
|
618 |
else mk_meta_eq (let |
|
619 |
val cj = Thm.cterm_of (Thm.theory_of_cterm ct) (mk_num (abs j)); |
|
620 |
in |
|
621 |
(if j > 0 then (Morphism.thm phi @{thm Dig_of_num_pos}) OF [cert cj cl ck] |
|
622 |
else (Morphism.thm phi @{thm Dig_of_num_neg}) OF [cert cj ck cl]) |
|
623 |
end) end) |
|
624 |
end |
|
625 |
*} |
|
626 |
||
627 |
lemma Dig_of_num_minus_zero [numeral]: |
|
628 |
"of_num n - 0 = of_num n" |
|
629 |
by (simp add: minus_inverts_plus1) |
|
630 |
||
631 |
lemma Dig_one_minus_zero [numeral]: |
|
632 |
"1 - 0 = 1" |
|
633 |
by (simp add: minus_inverts_plus1) |
|
634 |
||
635 |
lemma Dig_one_minus_one [numeral]: |
|
636 |
"1 - 1 = 0" |
|
637 |
by (simp add: minus_inverts_plus1) |
|
638 |
||
639 |
lemma Dig_of_num_minus_one [numeral]: |
|
29941 | 640 |
"of_num (Dig0 n) - 1 = of_num (DigM n)" |
28021 | 641 |
"of_num (Dig1 n) - 1 = of_num (Dig0 n)" |
29941 | 642 |
by (auto intro: minus_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one) |
28021 | 643 |
|
644 |
lemma Dig_one_minus_of_num [numeral]: |
|
29941 | 645 |
"1 - of_num (Dig0 n) = 0 - of_num (DigM n)" |
28021 | 646 |
"1 - of_num (Dig1 n) = 0 - of_num (Dig0 n)" |
29941 | 647 |
by (auto intro: minus_minus_zero_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one) |
28021 | 648 |
|
649 |
end |
|
650 |
||
29945 | 651 |
subsubsection {* |
29947 | 652 |
Structures with negation: class @{text ring_1} |
29945 | 653 |
*} |
654 |
||
28021 | 655 |
context ring_1 |
656 |
begin |
|
657 |
||
658 |
subclass semiring_1_minus |
|
29667 | 659 |
proof qed (simp_all add: algebra_simps) |
28021 | 660 |
|
661 |
lemma Dig_zero_minus_of_num [numeral]: |
|
662 |
"0 - of_num n = - of_num n" |
|
663 |
by simp |
|
664 |
||
665 |
lemma Dig_zero_minus_one [numeral]: |
|
666 |
"0 - 1 = - 1" |
|
667 |
by simp |
|
668 |
||
669 |
lemma Dig_uminus_uminus [numeral]: |
|
670 |
"- (- of_num n) = of_num n" |
|
671 |
by simp |
|
672 |
||
673 |
lemma Dig_plus_uminus [numeral]: |
|
674 |
"of_num m + - of_num n = of_num m - of_num n" |
|
675 |
"- of_num m + of_num n = of_num n - of_num m" |
|
676 |
"- of_num m + - of_num n = - (of_num m + of_num n)" |
|
677 |
"of_num m - - of_num n = of_num m + of_num n" |
|
678 |
"- of_num m - of_num n = - (of_num m + of_num n)" |
|
679 |
"- of_num m - - of_num n = of_num n - of_num m" |
|
680 |
by (simp_all add: diff_minus add_commute) |
|
681 |
||
682 |
lemma Dig_times_uminus [numeral]: |
|
683 |
"- of_num n * of_num m = - (of_num n * of_num m)" |
|
684 |
"of_num n * - of_num m = - (of_num n * of_num m)" |
|
685 |
"- of_num n * - of_num m = of_num n * of_num m" |
|
31028 | 686 |
by simp_all |
28021 | 687 |
|
688 |
lemma of_int_of_num [numeral]: "of_int (of_num n) = of_num n" |
|
689 |
by (induct n) |
|
690 |
(simp_all only: of_num.simps semiring_numeral_class.of_num.simps of_int_add, simp_all) |
|
691 |
||
692 |
declare of_int_1 [numeral] |
|
693 |
||
694 |
end |
|
695 |
||
29945 | 696 |
subsubsection {* |
29954 | 697 |
Structures with exponentiation |
698 |
*} |
|
699 |
||
700 |
lemma of_num_square: "of_num (square x) = of_num x * of_num x" |
|
701 |
by (induct x) |
|
31028 | 702 |
(simp_all add: of_num.simps of_num_add algebra_simps) |
29954 | 703 |
|
31028 | 704 |
lemma of_num_pow: "of_num (pow x y) = of_num x ^ of_num y" |
29954 | 705 |
by (induct y) |
31028 | 706 |
(simp_all add: of_num.simps of_num_square of_num_mult power_add) |
29954 | 707 |
|
31028 | 708 |
lemma power_of_num [numeral]: "of_num x ^ of_num y = of_num (pow x y)" |
709 |
unfolding of_num_pow .. |
|
29954 | 710 |
|
711 |
lemma power_zero_of_num [numeral]: |
|
31029 | 712 |
"0 ^ of_num n = (0::'a::semiring_1)" |
29954 | 713 |
using of_num_pos [where n=n and ?'a=nat] |
714 |
by (simp add: power_0_left) |
|
715 |
||
716 |
lemma power_minus_Dig0 [numeral]: |
|
31029 | 717 |
fixes x :: "'a::ring_1" |
29954 | 718 |
shows "(- x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)" |
31028 | 719 |
by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc) |
29954 | 720 |
|
721 |
lemma power_minus_Dig1 [numeral]: |
|
31029 | 722 |
fixes x :: "'a::ring_1" |
29954 | 723 |
shows "(- x) ^ of_num (Dig1 n) = - (x ^ of_num (Dig1 n))" |
31028 | 724 |
by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc) |
29954 | 725 |
|
726 |
declare power_one [numeral] |
|
727 |
||
728 |
||
729 |
subsubsection {* |
|
28021 | 730 |
Greetings to @{typ nat}. |
731 |
*} |
|
732 |
||
733 |
instance nat :: semiring_1_minus proof qed simp_all |
|
734 |
||
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
735 |
lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)" |
28021 | 736 |
unfolding of_num_plus_one [symmetric] by simp |
737 |
||
738 |
lemma nat_number: |
|
739 |
"1 = Suc 0" |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
740 |
"of_num One = Suc 0" |
29941 | 741 |
"of_num (Dig0 n) = Suc (of_num (DigM n))" |
28021 | 742 |
"of_num (Dig1 n) = Suc (of_num (Dig0 n))" |
29941 | 743 |
by (simp_all add: of_num.simps DigM_plus_one Suc_of_num) |
28021 | 744 |
|
745 |
declare diff_0_eq_0 [numeral] |
|
746 |
||
747 |
||
748 |
subsection {* Code generator setup for @{typ int} *} |
|
749 |
||
750 |
definition Pls :: "num \<Rightarrow> int" where |
|
751 |
[simp, code post]: "Pls n = of_num n" |
|
752 |
||
753 |
definition Mns :: "num \<Rightarrow> int" where |
|
754 |
[simp, code post]: "Mns n = - of_num n" |
|
755 |
||
756 |
code_datatype "0::int" Pls Mns |
|
757 |
||
758 |
lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric] |
|
759 |
||
760 |
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where |
|
28562 | 761 |
[simp, code del]: "sub m n = (of_num m - of_num n)" |
28021 | 762 |
|
763 |
definition dup :: "int \<Rightarrow> int" where |
|
28562 | 764 |
[code del]: "dup k = 2 * k" |
28021 | 765 |
|
766 |
lemma Dig_sub [code]: |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
767 |
"sub One One = 0" |
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
768 |
"sub (Dig0 m) One = of_num (DigM m)" |
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
769 |
"sub (Dig1 m) One = of_num (Dig0 m)" |
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
770 |
"sub One (Dig0 n) = - of_num (DigM n)" |
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
771 |
"sub One (Dig1 n) = - of_num (Dig0 n)" |
28021 | 772 |
"sub (Dig0 m) (Dig0 n) = dup (sub m n)" |
773 |
"sub (Dig1 m) (Dig1 n) = dup (sub m n)" |
|
774 |
"sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1" |
|
775 |
"sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1" |
|
29667 | 776 |
apply (simp_all add: dup_def algebra_simps) |
29941 | 777 |
apply (simp_all add: of_num_plus one_plus_DigM)[4] |
28021 | 778 |
apply (simp_all add: of_num.simps) |
779 |
done |
|
780 |
||
781 |
lemma dup_code [code]: |
|
782 |
"dup 0 = 0" |
|
783 |
"dup (Pls n) = Pls (Dig0 n)" |
|
784 |
"dup (Mns n) = Mns (Dig0 n)" |
|
785 |
by (simp_all add: dup_def of_num.simps) |
|
786 |
||
28562 | 787 |
lemma [code, code del]: |
28021 | 788 |
"(1 :: int) = 1" |
789 |
"(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +" |
|
790 |
"(uminus :: int \<Rightarrow> int) = uminus" |
|
791 |
"(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -" |
|
792 |
"(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *" |
|
28367 | 793 |
"(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq" |
28021 | 794 |
"(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>" |
795 |
"(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <" |
|
796 |
by rule+ |
|
797 |
||
798 |
lemma one_int_code [code]: |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
799 |
"1 = Pls One" |
31028 | 800 |
by (simp add: of_num_One) |
28021 | 801 |
|
802 |
lemma plus_int_code [code]: |
|
803 |
"k + 0 = (k::int)" |
|
804 |
"0 + l = (l::int)" |
|
805 |
"Pls m + Pls n = Pls (m + n)" |
|
806 |
"Pls m - Pls n = sub m n" |
|
807 |
"Mns m + Mns n = Mns (m + n)" |
|
808 |
"Mns m - Mns n = sub n m" |
|
31028 | 809 |
by (simp_all add: of_num_add) |
28021 | 810 |
|
811 |
lemma uminus_int_code [code]: |
|
812 |
"uminus 0 = (0::int)" |
|
813 |
"uminus (Pls m) = Mns m" |
|
814 |
"uminus (Mns m) = Pls m" |
|
815 |
by simp_all |
|
816 |
||
817 |
lemma minus_int_code [code]: |
|
818 |
"k - 0 = (k::int)" |
|
819 |
"0 - l = uminus (l::int)" |
|
820 |
"Pls m - Pls n = sub m n" |
|
821 |
"Pls m - Mns n = Pls (m + n)" |
|
822 |
"Mns m - Pls n = Mns (m + n)" |
|
823 |
"Mns m - Mns n = sub n m" |
|
31028 | 824 |
by (simp_all add: of_num_add) |
28021 | 825 |
|
826 |
lemma times_int_code [code]: |
|
827 |
"k * 0 = (0::int)" |
|
828 |
"0 * l = (0::int)" |
|
829 |
"Pls m * Pls n = Pls (m * n)" |
|
830 |
"Pls m * Mns n = Mns (m * n)" |
|
831 |
"Mns m * Pls n = Mns (m * n)" |
|
832 |
"Mns m * Mns n = Pls (m * n)" |
|
31028 | 833 |
by (simp_all add: of_num_mult) |
28021 | 834 |
|
835 |
lemma eq_int_code [code]: |
|
28367 | 836 |
"eq_class.eq 0 (0::int) \<longleftrightarrow> True" |
837 |
"eq_class.eq 0 (Pls l) \<longleftrightarrow> False" |
|
838 |
"eq_class.eq 0 (Mns l) \<longleftrightarrow> False" |
|
839 |
"eq_class.eq (Pls k) 0 \<longleftrightarrow> False" |
|
840 |
"eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l" |
|
841 |
"eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False" |
|
842 |
"eq_class.eq (Mns k) 0 \<longleftrightarrow> False" |
|
843 |
"eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False" |
|
844 |
"eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l" |
|
28021 | 845 |
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int] |
28367 | 846 |
by (simp_all add: of_num_eq_iff eq) |
28021 | 847 |
|
848 |
lemma less_eq_int_code [code]: |
|
849 |
"0 \<le> (0::int) \<longleftrightarrow> True" |
|
850 |
"0 \<le> Pls l \<longleftrightarrow> True" |
|
851 |
"0 \<le> Mns l \<longleftrightarrow> False" |
|
852 |
"Pls k \<le> 0 \<longleftrightarrow> False" |
|
853 |
"Pls k \<le> Pls l \<longleftrightarrow> k \<le> l" |
|
854 |
"Pls k \<le> Mns l \<longleftrightarrow> False" |
|
855 |
"Mns k \<le> 0 \<longleftrightarrow> True" |
|
856 |
"Mns k \<le> Pls l \<longleftrightarrow> True" |
|
857 |
"Mns k \<le> Mns l \<longleftrightarrow> l \<le> k" |
|
858 |
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int] |
|
859 |
by (simp_all add: of_num_less_eq_iff) |
|
860 |
||
861 |
lemma less_int_code [code]: |
|
862 |
"0 < (0::int) \<longleftrightarrow> False" |
|
863 |
"0 < Pls l \<longleftrightarrow> True" |
|
864 |
"0 < Mns l \<longleftrightarrow> False" |
|
865 |
"Pls k < 0 \<longleftrightarrow> False" |
|
866 |
"Pls k < Pls l \<longleftrightarrow> k < l" |
|
867 |
"Pls k < Mns l \<longleftrightarrow> False" |
|
868 |
"Mns k < 0 \<longleftrightarrow> True" |
|
869 |
"Mns k < Pls l \<longleftrightarrow> True" |
|
870 |
"Mns k < Mns l \<longleftrightarrow> l < k" |
|
871 |
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int] |
|
872 |
by (simp_all add: of_num_less_iff) |
|
873 |
||
874 |
lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp |
|
875 |
lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp |
|
876 |
declare zero_is_num_zero [code inline del] |
|
877 |
declare one_is_num_one [code inline del] |
|
878 |
||
879 |
hide (open) const sub dup |
|
880 |
||
881 |
||
882 |
subsection {* Numeral equations as default simplification rules *} |
|
883 |
||
31029 | 884 |
declare (in semiring_numeral) of_num_One [simp] |
885 |
declare (in semiring_numeral) of_num_plus_one [simp] |
|
886 |
declare (in semiring_numeral) of_num_one_plus [simp] |
|
887 |
declare (in semiring_numeral) of_num_plus [simp] |
|
888 |
declare (in semiring_numeral) of_num_times [simp] |
|
889 |
||
890 |
declare (in semiring_1) of_nat_of_num [simp] |
|
891 |
||
892 |
declare (in semiring_char_0) of_num_eq_iff [simp] |
|
893 |
declare (in semiring_char_0) of_num_eq_one_iff [simp] |
|
894 |
declare (in semiring_char_0) one_eq_of_num_iff [simp] |
|
895 |
||
896 |
declare (in ordered_semidom) of_num_pos [simp] |
|
897 |
declare (in ordered_semidom) of_num_less_eq_iff [simp] |
|
898 |
declare (in ordered_semidom) of_num_less_eq_one_iff [simp] |
|
899 |
declare (in ordered_semidom) one_less_eq_of_num_iff [simp] |
|
900 |
declare (in ordered_semidom) of_num_less_iff [simp] |
|
901 |
declare (in ordered_semidom) of_num_less_one_iff [simp] |
|
902 |
declare (in ordered_semidom) one_less_of_num_iff [simp] |
|
903 |
declare (in ordered_semidom) of_num_nonneg [simp] |
|
904 |
declare (in ordered_semidom) of_num_less_zero_iff [simp] |
|
905 |
declare (in ordered_semidom) of_num_le_zero_iff [simp] |
|
906 |
||
907 |
declare (in ordered_idom) le_signed_numeral_special [simp] |
|
908 |
declare (in ordered_idom) less_signed_numeral_special [simp] |
|
909 |
||
910 |
declare (in semiring_1_minus) Dig_of_num_minus_one [simp] |
|
911 |
declare (in semiring_1_minus) Dig_one_minus_of_num [simp] |
|
912 |
||
913 |
declare (in ring_1) Dig_plus_uminus [simp] |
|
914 |
declare (in ring_1) of_int_of_num [simp] |
|
915 |
||
916 |
declare power_of_num [simp] |
|
917 |
declare power_zero_of_num [simp] |
|
918 |
declare power_minus_Dig0 [simp] |
|
919 |
declare power_minus_Dig1 [simp] |
|
920 |
||
921 |
declare Suc_of_num [simp] |
|
922 |
||
28021 | 923 |
thm numeral |
924 |
||
925 |
||
31025 | 926 |
subsection {* Simplification Procedures *} |
927 |
||
31026
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
928 |
subsubsection {* Reorientation of equalities *} |
31025 | 929 |
|
930 |
setup {* |
|
931 |
ReorientProc.add |
|
932 |
(fn Const(@{const_name of_num}, _) $ _ => true |
|
933 |
| Const(@{const_name uminus}, _) $ |
|
934 |
(Const(@{const_name of_num}, _) $ _) => true |
|
935 |
| _ => false) |
|
936 |
*} |
|
937 |
||
938 |
simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = ReorientProc.proc |
|
939 |
||
31026
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
940 |
subsubsection {* Constant folding for multiplication in semirings *} |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
941 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
942 |
context semiring_numeral |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
943 |
begin |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
944 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
945 |
lemma mult_of_num_commute: "x * of_num n = of_num n * x" |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
946 |
by (induct n) |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
947 |
(simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right) |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
948 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
949 |
definition |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
950 |
"commutes_with a b \<longleftrightarrow> a * b = b * a" |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
951 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
952 |
lemma commutes_with_commute: "commutes_with a b \<Longrightarrow> a * b = b * a" |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
953 |
unfolding commutes_with_def . |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
954 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
955 |
lemma commutes_with_left_commute: "commutes_with a b \<Longrightarrow> a * (b * c) = b * (a * c)" |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
956 |
unfolding commutes_with_def by (simp only: mult_assoc [symmetric]) |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
957 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
958 |
lemma commutes_with_numeral: "commutes_with x (of_num n)" "commutes_with (of_num n) x" |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
959 |
unfolding commutes_with_def by (simp_all add: mult_of_num_commute) |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
960 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
961 |
lemmas mult_ac_numeral = |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
962 |
mult_assoc |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
963 |
commutes_with_commute |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
964 |
commutes_with_left_commute |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
965 |
commutes_with_numeral |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
966 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
967 |
end |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
968 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
969 |
ML {* |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
970 |
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
971 |
struct |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
972 |
val assoc_ss = HOL_ss addsimps @{thms mult_ac_numeral} |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
973 |
val eq_reflection = eq_reflection |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
974 |
fun is_numeral (Const(@{const_name of_num}, _) $ _) = true |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
975 |
| is_numeral _ = false; |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
976 |
end; |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
977 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
978 |
structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
979 |
*} |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
980 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
981 |
simproc_setup semiring_assoc_fold' ("(a::'a::semiring_numeral) * b") = |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
982 |
{* fn phi => fn ss => fn ct => |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
983 |
Semiring_Times_Assoc.proc ss (Thm.term_of ct) *} |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
984 |
|
31025 | 985 |
|
986 |
subsection {* Toy examples *} |
|
28021 | 987 |
|
988 |
definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3" |
|
989 |
code_thms bar |
|
990 |
export_code bar in Haskell file - |
|
991 |
export_code bar in OCaml module_name Foo file - |
|
992 |
ML {* @{code bar} *} |
|
993 |
||
994 |
end |