1 (* Title: HOL/ex/Numeral.thy
3 Author: Florian Haftmann
5 An experimental alternative numeral representation.
12 subsection {* The @{text num} type *}
15 We construct @{text num} as a copy of strictly positive
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)
24 A totalized abstraction function. It is not entirely clear
25 whether this is really useful.
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)"
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)"
34 apply (rule num_of_nat_abs_cases)
35 apply (unfold mem_def)
36 using assms unfolding num_of_nat_def
40 lemma num_of_nat_zero: "num_of_nat 0 = num_of_nat 1"
41 by (simp add: num_of_nat_def)
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)
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])
54 "(\<And>m. PROP P m) \<equiv> (\<And>n. PROP P (num_of_nat n))"
57 assume "\<And>m\<Colon>num. PROP P m"
58 then show "PROP P (num_of_nat n)" .
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 .
71 subsection {* Digit representation for @{typ num} *}
73 instantiation num :: "{semiring, monoid_mult}"
76 definition one_num :: num where
77 [code func del]: "1 = num_of_nat 1"
79 definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
80 [code func del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
82 definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
83 [code func del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
85 definition Dig0 :: "num \<Rightarrow> num" where
86 [code func del]: "Dig0 n = n + n"
88 definition Dig1 :: "num \<Rightarrow> num" where
89 [code func del]: "Dig1 n = n + n + 1"
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)
98 The following proofs seem horribly complicated.
99 Any room for simplification!?
102 lemma nat_dig_cases [case_names 0 1 dig0 dig1]:
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"
109 using assms proof (induct n)
110 case 0 then show ?case by simp
113 show P proof (rule Suc.hyps)
115 then have "Suc n = 1" by simp
116 then show P by (rule Suc.prems(2))
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))
124 assume "0 < m" and "n = m + m"
126 moreover from `n = m + m` have "Suc n = Suc (m + m)" by simp
127 ultimately show P by (rule Suc.prems(4))
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))
137 lemma num_induct_raw:
139 assumes not0: "n > 0"
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))"
144 using not0 proof (induct n rule: less_induct)
146 show "P n" proof (cases n rule: nat_dig_cases)
147 case 0 then show ?thesis using less by simp
149 case 1 then show ?thesis using assms by simp
152 then show ?thesis apply simp
153 apply (rule assms(3)) apply assumption
159 then show ?thesis apply simp
160 apply (rule assms(4)) apply assumption
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)
170 lemma num_induct [case_names 1 Suc, induct type: num]:
171 fixes P :: "num \<Rightarrow> bool"
173 and Suc: "\<And>n. P n \<Longrightarrow> P (n + 1)"
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)
180 rep_datatype "1::num" Dig0 Dig1 proof -
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"
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 .
190 case 2 with 1 show ?case by (simp add: one_num_def)
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)
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)
200 with m show "P m" by simp
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)
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)
213 show "1 \<noteq> Dig0 n"
215 by (auto simp add: Dig0_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
218 show "1 \<noteq> Dig1 n"
220 by (auto simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
223 have "\<And>n m. n + n \<noteq> Suc (m + 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
230 case (Suc m) then show ?case by (cases n) simp_all
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)
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"}).
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.
248 subsection {* Binary numerals *}
251 We embed binary representations into a generic algebraic
252 structure using @{text of_num}
257 NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")
262 class semiring_numeral = semiring + monoid_mult
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"
270 declare of_num.simps [simp del]
279 fun mk_num 1 = @{term "1::num"}
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;
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;
290 (*FIXME these have to gain proper context via morphisms phi*)
292 fun mk_numeral T k = Const (@{const_name of_num}, @{typ num} --> T)
295 fun dest_numeral (Const (@{const_name of_num}, Type ("fun", [@{typ num}, T])) $ t) =
300 "_Numerals" :: "xnum \<Rightarrow> 'a" ("_")
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
309 fun numeral_tr [Free (num, _)] =
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
319 typed_print_translation {*
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] =
329 val k = int_of_num' n;
330 val t' = Syntax.const "_Numerals" $ Syntax.free ("#" ^ string_of_int k);
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
337 in [(@{const_syntax of_num}, num_tr')] end
341 subsection {* Numeral operations *}
344 First, addition and multiplication on digits.
347 lemma Dig_plus [numeral, simp, code]:
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)
359 lemma Dig_times [numeral, simp, code]:
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)
372 @{const of_num} is a morphism.
375 context semiring_numeral
378 abbreviation "Num1 \<equiv> of_num 1"
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.
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)
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 ..
397 lemma of_num_plus [numeral]:
398 "of_num m + of_num n = of_num (m + n)"
399 by (induct n rule: num_induct)
400 (simp_all add: Dig_plus of_num_one semigroup_add_class.add_assoc [symmetric, of m]
401 add_ac of_num_plus_one [symmetric])
403 lemma of_num_times_one [numeral]:
404 "of_num n * 1 = of_num n"
407 lemma of_num_one_times [numeral]:
408 "1 * of_num n = of_num n"
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]
415 semiring_class.right_distrib right_distrib of_num_one)
420 Structures with a @{term 0}.
426 subclass semiring_numeral ..
428 lemma of_nat_of_num [numeral]: "of_nat (of_num n) = of_num n"
430 (simp_all add: semiring_numeral_class.of_num.simps of_num.simps add_ac)
432 declare of_nat_1 [numeral]
434 lemma Dig_plus_zero [numeral]:
436 "0 + of_num n = of_num n"
438 "of_num n + 0 = of_num n"
441 lemma Dig_times_zero [numeral]:
450 lemma nat_of_num_of_num: "nat_of_num = of_num"
453 have "of_num n = nat_of_num n" apply (induct n)
454 apply (simp_all add: of_num.simps)
456 apply (simp_all add: one_num_def plus_num_def Dig0_def Dig1_def num_of_nat_inverse mem_def)
458 then show "nat_of_num n = of_num n" by simp
465 context semiring_char_0
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 ..
473 lemma of_num_eq_one_iff [numeral]:
474 "of_num n = 1 \<longleftrightarrow> n = 1"
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)
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
487 Comparisons. Could be perhaps more general than here.
490 lemma (in ordered_semidom) of_num_pos: "0 < of_num n"
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)
502 instantiation num :: linorder
505 definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
506 [code func del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
508 definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
509 [code func del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
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)
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)
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)
540 context ordered_semidom
543 lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n"
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)
550 lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = 1"
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)
557 lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n"
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)
564 lemma of_num_less_iff [numeral]: "of_num m < of_num n \<longleftrightarrow> m < n"
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)
571 lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1"
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)
578 lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> 1"
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)
588 Structures with subtraction @{term "op -"}.
591 text {* A decrement function *}
593 primrec dec :: "num \<Rightarrow> num" where
595 | "dec (Dig0 n) = (case n of 1 \<Rightarrow> 1 | _ \<Rightarrow> Dig1 (dec n))"
596 | "dec (Dig1 n) = Dig0 n"
598 declare dec.simps [simp del, code del]
600 lemma Dig_dec [numeral, simp, code]:
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)
608 lemma Dig_dec_plus_one:
609 "dec n + 1 = (if n = 1 then Dig0 1 else n)"
611 (auto simp add: Dig_plus dec.simps,
612 auto simp add: Dig_plus split: num.splits)
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 ..
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"
623 lemma minus_inverts_plus2: "a + b = c \<Longrightarrow> c - a = b"
624 by (simp add: add_ac minus_inverts_plus1 [of b a])
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])
631 class semiring_1_minus = semiring_1 + semiring_minus
634 lemma Dig_of_num_pos:
636 shows "of_num m - of_num n = of_num k"
637 using assms by (simp add: of_num_plus minus_inverts_plus1)
639 lemma Dig_of_num_zero:
640 shows "of_num n - of_num n = 0"
641 by (rule minus_inverts_plus1) simp
643 lemma Dig_of_num_neg:
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)
648 lemmas Dig_plus_eval =
649 of_num_plus of_num_eq_iff Dig_plus refl [of "1::num", THEN eqTrueI] num.inject
651 simproc_setup numeral_minus ("of_num m - of_num n") = {*
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
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
666 val cj = Thm.cterm_of (Thm.theory_of_cterm ct) (mk_num (abs j));
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])
674 lemma Dig_of_num_minus_zero [numeral]:
675 "of_num n - 0 = of_num n"
676 by (simp add: minus_inverts_plus1)
678 lemma Dig_one_minus_zero [numeral]:
680 by (simp add: minus_inverts_plus1)
682 lemma Dig_one_minus_one [numeral]:
684 by (simp add: minus_inverts_plus1)
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)
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)
701 subclass semiring_1_minus
702 by unfold_locales (simp_all add: ring_simps)
704 lemma Dig_zero_minus_of_num [numeral]:
705 "0 - of_num n = - of_num n"
708 lemma Dig_zero_minus_one [numeral]:
712 lemma Dig_uminus_uminus [numeral]:
713 "- (- of_num n) = of_num n"
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)
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])
731 lemma of_int_of_num [numeral]: "of_int (of_num n) = of_num n"
733 (simp_all only: of_num.simps semiring_numeral_class.of_num.simps of_int_add, simp_all)
735 declare of_int_1 [numeral]
740 Greetings to @{typ nat}.
743 instance nat :: semiring_1_minus proof qed simp_all
745 lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + 1)"
746 unfolding of_num_plus_one [symmetric] by simp
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)
755 declare diff_0_eq_0 [numeral]
758 subsection {* Code generator setup for @{typ int} *}
760 definition Pls :: "num \<Rightarrow> int" where
761 [simp, code post]: "Pls n = of_num n"
763 definition Mns :: "num \<Rightarrow> int" where
764 [simp, code post]: "Mns n = - of_num n"
766 code_datatype "0::int" Pls Mns
768 lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
770 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
771 [simp, code func del]: "sub m n = (of_num m - of_num n)"
773 definition dup :: "int \<Rightarrow> int" where
774 [code func del]: "dup k = 2 * k"
776 lemma Dig_sub [code]:
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"
786 apply (simp_all add: dup_def ring_simps)
787 apply (simp_all add: of_num_plus Dig_one_plus_dec)[4]
788 apply (simp_all add: of_num.simps)
791 lemma dup_code [code]:
793 "dup (Pls n) = Pls (Dig0 n)"
794 "dup (Mns n) = Mns (Dig0 n)"
795 by (simp_all add: dup_def of_num.simps)
797 lemma [code func, code func del]:
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 *"
803 "(op = :: int \<Rightarrow> int \<Rightarrow> bool) = op ="
804 "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
805 "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
808 lemma one_int_code [code]:
810 by (simp add: of_num_one)
812 lemma plus_int_code [code]:
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])
821 lemma uminus_int_code [code]:
822 "uminus 0 = (0::int)"
823 "uminus (Pls m) = Mns m"
824 "uminus (Mns m) = Pls m"
827 lemma minus_int_code [code]:
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])
836 lemma times_int_code [code]:
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])
845 lemma eq_int_code [code]:
846 "0 = (0::int) \<longleftrightarrow> True"
847 "0 = Pls l \<longleftrightarrow> False"
848 "0 = Mns l \<longleftrightarrow> False"
849 "Pls k = 0 \<longleftrightarrow> False"
850 "Pls k = Pls l \<longleftrightarrow> k = l"
851 "Pls k = Mns l \<longleftrightarrow> False"
852 "Mns k = 0 \<longleftrightarrow> False"
853 "Mns k = Pls l \<longleftrightarrow> False"
854 "Mns k = Mns l \<longleftrightarrow> k = l"
855 using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
856 by (simp_all add: of_num_eq_iff)
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)
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)
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]
889 hide (open) const sub dup
892 subsection {* Numeral equations as default simplification rules *}
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]
902 text {* Toy examples *}
904 definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
906 export_code bar in Haskell file -
907 export_code bar in OCaml module_name Foo file -