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