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