src/HOL/Num.thy
 author eberlm Mon Jul 17 16:49:19 2017 +0200 (2017-07-17) changeset 66283 adf3155c57e2 parent 64238 b60a9752b6d0 child 66936 cf8d8fc23891 permissions -rw-r--r--
Printing natural numbers as numerals in evaluation
1 (*  Title:      HOL/Num.thy
2     Author:     Florian Haftmann
3     Author:     Brian Huffman
4 *)
6 section \<open>Binary Numerals\<close>
8 theory Num
9   imports BNF_Least_Fixpoint Transfer
10 begin
12 subsection \<open>The \<open>num\<close> type\<close>
14 datatype num = One | Bit0 num | Bit1 num
16 text \<open>Increment function for type @{typ num}\<close>
18 primrec inc :: "num \<Rightarrow> num"
19   where
20     "inc One = Bit0 One"
21   | "inc (Bit0 x) = Bit1 x"
22   | "inc (Bit1 x) = Bit0 (inc x)"
24 text \<open>Converting between type @{typ num} and type @{typ nat}\<close>
26 primrec nat_of_num :: "num \<Rightarrow> nat"
27   where
28     "nat_of_num One = Suc 0"
29   | "nat_of_num (Bit0 x) = nat_of_num x + nat_of_num x"
30   | "nat_of_num (Bit1 x) = Suc (nat_of_num x + nat_of_num x)"
32 primrec num_of_nat :: "nat \<Rightarrow> num"
33   where
34     "num_of_nat 0 = One"
35   | "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"
37 lemma nat_of_num_pos: "0 < nat_of_num x"
38   by (induct x) simp_all
40 lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0"
41   by (induct x) simp_all
43 lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)"
44   by (induct x) simp_all
46 lemma num_of_nat_double: "0 < n \<Longrightarrow> num_of_nat (n + n) = Bit0 (num_of_nat n)"
47   by (induct n) simp_all
49 text \<open>Type @{typ num} is isomorphic to the strictly positive natural numbers.\<close>
51 lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x"
52   by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos)
54 lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n"
55   by (induct n) (simp_all add: nat_of_num_inc)
57 lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y"
58   apply safe
59   apply (drule arg_cong [where f=num_of_nat])
61   done
63 lemma num_induct [case_names One inc]:
64   fixes P :: "num \<Rightarrow> bool"
65   assumes One: "P One"
66     and inc: "\<And>x. P x \<Longrightarrow> P (inc x)"
67   shows "P x"
68 proof -
69   obtain n where n: "Suc n = nat_of_num x"
70     by (cases "nat_of_num x") (simp_all add: nat_of_num_neq_0)
71   have "P (num_of_nat (Suc n))"
72   proof (induct n)
73     case 0
74     from One show ?case by simp
75   next
76     case (Suc n)
77     then have "P (inc (num_of_nat (Suc n)))" by (rule inc)
78     then show "P (num_of_nat (Suc (Suc n)))" by simp
79   qed
80   with n show "P x"
82 qed
84 text \<open>
85   From now on, there are two possible models for @{typ num}: as positive
86   naturals (rule \<open>num_induct\<close>) and as digit representation (rules
87   \<open>num.induct\<close>, \<open>num.cases\<close>).
88 \<close>
91 subsection \<open>Numeral operations\<close>
93 instantiation num :: "{plus,times,linorder}"
94 begin
96 definition [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
98 definition [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
100 definition [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
102 definition [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
104 instance
105   by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff)
107 end
109 lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y"
110   unfolding plus_num_def
111   by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos)
113 lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y"
114   unfolding times_num_def
115   by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos)
118   "One + One = Bit0 One"
119   "One + Bit0 n = Bit1 n"
120   "One + Bit1 n = Bit0 (n + One)"
121   "Bit0 m + One = Bit1 m"
122   "Bit0 m + Bit0 n = Bit0 (m + n)"
123   "Bit0 m + Bit1 n = Bit1 (m + n)"
124   "Bit1 m + One = Bit0 (m + One)"
125   "Bit1 m + Bit0 n = Bit1 (m + n)"
126   "Bit1 m + Bit1 n = Bit0 (m + n + One)"
129 lemma mult_num_simps [simp, code]:
130   "m * One = m"
131   "One * n = n"
132   "Bit0 m * Bit0 n = Bit0 (Bit0 (m * n))"
133   "Bit0 m * Bit1 n = Bit0 (m * Bit1 n)"
134   "Bit1 m * Bit0 n = Bit0 (Bit1 m * n)"
135   "Bit1 m * Bit1 n = Bit1 (m + n + Bit0 (m * n))"
138 lemma eq_num_simps:
139   "One = One \<longleftrightarrow> True"
140   "One = Bit0 n \<longleftrightarrow> False"
141   "One = Bit1 n \<longleftrightarrow> False"
142   "Bit0 m = One \<longleftrightarrow> False"
143   "Bit1 m = One \<longleftrightarrow> False"
144   "Bit0 m = Bit0 n \<longleftrightarrow> m = n"
145   "Bit0 m = Bit1 n \<longleftrightarrow> False"
146   "Bit1 m = Bit0 n \<longleftrightarrow> False"
147   "Bit1 m = Bit1 n \<longleftrightarrow> m = n"
148   by simp_all
150 lemma le_num_simps [simp, code]:
151   "One \<le> n \<longleftrightarrow> True"
152   "Bit0 m \<le> One \<longleftrightarrow> False"
153   "Bit1 m \<le> One \<longleftrightarrow> False"
154   "Bit0 m \<le> Bit0 n \<longleftrightarrow> m \<le> n"
155   "Bit0 m \<le> Bit1 n \<longleftrightarrow> m \<le> n"
156   "Bit1 m \<le> Bit1 n \<longleftrightarrow> m \<le> n"
157   "Bit1 m \<le> Bit0 n \<longleftrightarrow> m < n"
158   using nat_of_num_pos [of n] nat_of_num_pos [of m]
159   by (auto simp add: less_eq_num_def less_num_def)
161 lemma less_num_simps [simp, code]:
162   "m < One \<longleftrightarrow> False"
163   "One < Bit0 n \<longleftrightarrow> True"
164   "One < Bit1 n \<longleftrightarrow> True"
165   "Bit0 m < Bit0 n \<longleftrightarrow> m < n"
166   "Bit0 m < Bit1 n \<longleftrightarrow> m \<le> n"
167   "Bit1 m < Bit1 n \<longleftrightarrow> m < n"
168   "Bit1 m < Bit0 n \<longleftrightarrow> m < n"
169   using nat_of_num_pos [of n] nat_of_num_pos [of m]
170   by (auto simp add: less_eq_num_def less_num_def)
172 lemma le_num_One_iff: "x \<le> num.One \<longleftrightarrow> x = num.One"
175 text \<open>Rules using \<open>One\<close> and \<open>inc\<close> as constructors.\<close>
177 lemma add_One: "x + One = inc x"
180 lemma add_One_commute: "One + n = n + One"
181   by (induct n) simp_all
183 lemma add_inc: "x + inc y = inc (x + y)"
186 lemma mult_inc: "x * inc y = x * y + x"
189 text \<open>The @{const num_of_nat} conversion.\<close>
191 lemma num_of_nat_One: "n \<le> 1 \<Longrightarrow> num_of_nat n = One"
192   by (cases n) simp_all
194 lemma num_of_nat_plus_distrib:
195   "0 < m \<Longrightarrow> 0 < n \<Longrightarrow> num_of_nat (m + n) = num_of_nat m + num_of_nat n"
198 text \<open>A double-and-decrement function.\<close>
200 primrec BitM :: "num \<Rightarrow> num"
201   where
202     "BitM One = One"
203   | "BitM (Bit0 n) = Bit1 (BitM n)"
204   | "BitM (Bit1 n) = Bit1 (Bit0 n)"
206 lemma BitM_plus_one: "BitM n + One = Bit0 n"
207   by (induct n) simp_all
209 lemma one_plus_BitM: "One + BitM n = Bit0 n"
212 text \<open>Squaring and exponentiation.\<close>
214 primrec sqr :: "num \<Rightarrow> num"
215   where
216     "sqr One = One"
217   | "sqr (Bit0 n) = Bit0 (Bit0 (sqr n))"
218   | "sqr (Bit1 n) = Bit1 (Bit0 (sqr n + n))"
220 primrec pow :: "num \<Rightarrow> num \<Rightarrow> num"
221   where
222     "pow x One = x"
223   | "pow x (Bit0 y) = sqr (pow x y)"
224   | "pow x (Bit1 y) = sqr (pow x y) * x"
226 lemma nat_of_num_sqr: "nat_of_num (sqr x) = nat_of_num x * nat_of_num x"
229 lemma sqr_conv_mult: "sqr x = x * x"
230   by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult)
233 subsection \<open>Binary numerals\<close>
235 text \<open>
236   We embed binary representations into a generic algebraic
237   structure using \<open>numeral\<close>.
238 \<close>
240 class numeral = one + semigroup_add
241 begin
243 primrec numeral :: "num \<Rightarrow> 'a"
244   where
245     numeral_One: "numeral One = 1"
246   | numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n"
247   | numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1"
249 lemma numeral_code [code]:
250   "numeral One = 1"
251   "numeral (Bit0 n) = (let m = numeral n in m + m)"
252   "numeral (Bit1 n) = (let m = numeral n in m + m + 1)"
255 lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1"
256 proof (induct x)
257   case One
258   then show ?case by simp
259 next
260   case Bit0
262 next
263   case Bit1
265 qed
267 lemma numeral_inc: "numeral (inc x) = numeral x + 1"
268 proof (induct x)
269   case One
270   then show ?case by simp
271 next
272   case Bit0
273   then show ?case by simp
274 next
275   case (Bit1 x)
276   have "numeral x + (1 + numeral x) + 1 = numeral x + (numeral x + 1) + 1"
277     by (simp only: one_plus_numeral_commute)
278   with Bit1 show ?case
280 qed
282 declare numeral.simps [simp del]
284 abbreviation "Numeral1 \<equiv> numeral One"
286 declare numeral_One [code_post]
288 end
290 text \<open>Numeral syntax.\<close>
292 syntax
293   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
295 ML_file "Tools/numeral.ML"
297 parse_translation \<open>
298   let
299     fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) \$ t \$ u] =
300           c \$ numeral_tr [t] \$ u
301       | numeral_tr [Const (num, _)] =
302           (Numeral.mk_number_syntax o #value o Lexicon.read_num) num
303       | numeral_tr ts = raise TERM ("numeral_tr", ts);
304   in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
305 \<close>
307 typed_print_translation \<open>
308   let
309     fun num_tr' ctxt T [n] =
310       let
311         val k = Numeral.dest_num_syntax n;
312         val t' =
313           Syntax.const @{syntax_const "_Numeral"} \$
314             Syntax.free (string_of_int k);
315       in
316         (case T of
317           Type (@{type_name fun}, [_, T']) =>
318             if Printer.type_emphasis ctxt T' then
319               Syntax.const @{syntax_const "_constrain"} \$ t' \$
320                 Syntax_Phases.term_of_typ ctxt T'
321             else t'
322         | _ => if T = dummyT then t' else raise Match)
323       end;
324   in
325    [(@{const_syntax numeral}, num_tr')]
326   end
327 \<close>
330 subsection \<open>Class-specific numeral rules\<close>
332 text \<open>@{const numeral} is a morphism.\<close>
335 subsubsection \<open>Structures with addition: class \<open>numeral\<close>\<close>
337 context numeral
338 begin
340 lemma numeral_add: "numeral (m + n) = numeral m + numeral n"
341   by (induct n rule: num_induct)
344 lemma numeral_plus_numeral: "numeral m + numeral n = numeral (m + n)"
347 lemma numeral_plus_one: "numeral n + 1 = numeral (n + One)"
350 lemma one_plus_numeral: "1 + numeral n = numeral (One + n)"
353 lemma one_add_one: "1 + 1 = 2"
359 end
362 subsubsection \<open>Structures with negation: class \<open>neg_numeral\<close>\<close>
364 class neg_numeral = numeral + group_add
365 begin
367 lemma uminus_numeral_One: "- Numeral1 = - 1"
370 text \<open>Numerals form an abelian subgroup.\<close>
372 inductive is_num :: "'a \<Rightarrow> bool"
373   where
374     "is_num 1"
375   | "is_num x \<Longrightarrow> is_num (- x)"
376   | "is_num x \<Longrightarrow> is_num y \<Longrightarrow> is_num (x + y)"
378 lemma is_num_numeral: "is_num (numeral k)"
379   by (induct k) (simp_all add: numeral.simps is_num.intros)
381 lemma is_num_add_commute: "is_num x \<Longrightarrow> is_num y \<Longrightarrow> x + y = y + x"
382   apply (induct x rule: is_num.induct)
383     apply (induct y rule: is_num.induct)
384       apply simp
385      apply (rule_tac a=x in add_left_imp_eq)
386      apply (rule_tac a=x in add_right_imp_eq)
390    apply (rule_tac a=x in add_left_imp_eq)
391    apply (rule_tac a=x in add_right_imp_eq)
395   done
397 lemma is_num_add_left_commute: "is_num x \<Longrightarrow> is_num y \<Longrightarrow> x + (y + z) = y + (x + z)"
400 lemmas is_num_normalize =
402   is_num.intros is_num_numeral
405 definition dbl :: "'a \<Rightarrow> 'a"
406   where "dbl x = x + x"
408 definition dbl_inc :: "'a \<Rightarrow> 'a"
409   where "dbl_inc x = x + x + 1"
411 definition dbl_dec :: "'a \<Rightarrow> 'a"
412   where "dbl_dec x = x + x - 1"
414 definition sub :: "num \<Rightarrow> num \<Rightarrow> 'a"
415   where "sub k l = numeral k - numeral l"
417 lemma numeral_BitM: "numeral (BitM n) = numeral (Bit0 n) - 1"
418   by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq)
420 lemma dbl_simps [simp]:
421   "dbl (- numeral k) = - dbl (numeral k)"
422   "dbl 0 = 0"
423   "dbl 1 = 2"
424   "dbl (- 1) = - 2"
425   "dbl (numeral k) = numeral (Bit0 k)"
428 lemma dbl_inc_simps [simp]:
429   "dbl_inc (- numeral k) = - dbl_dec (numeral k)"
430   "dbl_inc 0 = 1"
431   "dbl_inc 1 = 3"
432   "dbl_inc (- 1) = - 1"
433   "dbl_inc (numeral k) = numeral (Bit1 k)"
434   by (simp_all add: dbl_inc_def dbl_dec_def numeral.simps numeral_BitM is_num_normalize algebra_simps
437 lemma dbl_dec_simps [simp]:
438   "dbl_dec (- numeral k) = - dbl_inc (numeral k)"
439   "dbl_dec 0 = - 1"
440   "dbl_dec 1 = 1"
441   "dbl_dec (- 1) = - 3"
442   "dbl_dec (numeral k) = numeral (BitM k)"
443   by (simp_all add: dbl_dec_def dbl_inc_def numeral.simps numeral_BitM is_num_normalize)
445 lemma sub_num_simps [simp]:
446   "sub One One = 0"
447   "sub One (Bit0 l) = - numeral (BitM l)"
448   "sub One (Bit1 l) = - numeral (Bit0 l)"
449   "sub (Bit0 k) One = numeral (BitM k)"
450   "sub (Bit1 k) One = numeral (Bit0 k)"
451   "sub (Bit0 k) (Bit0 l) = dbl (sub k l)"
452   "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
453   "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
454   "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
455   by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def numeral.simps
459   "numeral m + - numeral n = sub m n"
460   "- numeral m + numeral n = sub n m"
461   "- numeral m + - numeral n = - (numeral m + numeral n)"
466   "1 + - numeral m = sub One m"
467   "- numeral m + 1 = sub One m"
468   "numeral m + - 1 = sub m One"
469   "- 1 + numeral n = sub n One"
470   "- 1 + - numeral n = - numeral (inc n)"
471   "- numeral m + - 1 = - numeral (inc m)"
472   "1 + - 1 = 0"
473   "- 1 + 1 = 0"
474   "- 1 + - 1 = - 2"
478 lemma diff_numeral_simps:
479   "numeral m - numeral n = sub m n"
480   "numeral m - - numeral n = numeral (m + n)"
481   "- numeral m - numeral n = - numeral (m + n)"
482   "- numeral m - - numeral n = sub n m"
486 lemma diff_numeral_special:
487   "1 - numeral n = sub One n"
488   "numeral m - 1 = sub m One"
489   "1 - - numeral n = numeral (One + n)"
490   "- numeral m - 1 = - numeral (m + One)"
491   "- 1 - numeral n = - numeral (inc n)"
492   "numeral m - - 1 = numeral (inc m)"
493   "- 1 - - numeral n = sub n One"
494   "- numeral m - - 1 = sub One m"
495   "1 - 1 = 0"
496   "- 1 - 1 = - 2"
497   "1 - - 1 = 2"
498   "- 1 - - 1 = 0"
502 end
505 subsubsection \<open>Structures with multiplication: class \<open>semiring_numeral\<close>\<close>
507 class semiring_numeral = semiring + monoid_mult
508 begin
510 subclass numeral ..
512 lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"
513   by (induct n rule: num_induct)
516 lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"
517   by (rule numeral_mult [symmetric])
519 lemma mult_2: "2 * z = z + z"
522 lemma mult_2_right: "z * 2 = z + z"
525 end
528 subsubsection \<open>Structures with a zero: class \<open>semiring_1\<close>\<close>
530 context semiring_1
531 begin
533 subclass semiring_numeral ..
535 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n"
536   by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
538 lemma numeral_unfold_funpow:
539   "numeral k = (op + 1 ^^ numeral k) 0"
540   unfolding of_nat_def [symmetric] by simp
542 end
544 lemma transfer_rule_numeral:
545   fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
546   assumes [transfer_rule]: "R 0 0" "R 1 1"
547     "rel_fun R (rel_fun R R) plus plus"
548   shows "rel_fun HOL.eq R numeral numeral"
549   apply (subst (2) numeral_unfold_funpow [abs_def])
550   apply (subst (1) numeral_unfold_funpow [abs_def])
551   apply transfer_prover
552   done
554 lemma nat_of_num_numeral [code_abbrev]: "nat_of_num = numeral"
555 proof
556   fix n
557   have "numeral n = nat_of_num n"
558     by (induct n) (simp_all add: numeral.simps)
559   then show "nat_of_num n = numeral n"
560     by simp
561 qed
563 lemma nat_of_num_code [code]:
564   "nat_of_num One = 1"
565   "nat_of_num (Bit0 n) = (let m = nat_of_num n in m + m)"
566   "nat_of_num (Bit1 n) = (let m = nat_of_num n in Suc (m + m))"
570 subsubsection \<open>Equality: class \<open>semiring_char_0\<close>\<close>
572 context semiring_char_0
573 begin
575 lemma numeral_eq_iff: "numeral m = numeral n \<longleftrightarrow> m = n"
576   by (simp only: of_nat_numeral [symmetric] nat_of_num_numeral [symmetric]
577     of_nat_eq_iff num_eq_iff)
579 lemma numeral_eq_one_iff: "numeral n = 1 \<longleftrightarrow> n = One"
580   by (rule numeral_eq_iff [of n One, unfolded numeral_One])
582 lemma one_eq_numeral_iff: "1 = numeral n \<longleftrightarrow> One = n"
583   by (rule numeral_eq_iff [of One n, unfolded numeral_One])
585 lemma numeral_neq_zero: "numeral n \<noteq> 0"
586   by (simp add: of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] nat_of_num_pos)
588 lemma zero_neq_numeral: "0 \<noteq> numeral n"
589   unfolding eq_commute [of 0] by (rule numeral_neq_zero)
591 lemmas eq_numeral_simps [simp] =
592   numeral_eq_iff
593   numeral_eq_one_iff
594   one_eq_numeral_iff
595   numeral_neq_zero
596   zero_neq_numeral
598 end
601 subsubsection \<open>Comparisons: class \<open>linordered_semidom\<close>\<close>
603 text \<open>Could be perhaps more general than here.\<close>
605 context linordered_semidom
606 begin
608 lemma numeral_le_iff: "numeral m \<le> numeral n \<longleftrightarrow> m \<le> n"
609 proof -
610   have "of_nat (numeral m) \<le> of_nat (numeral n) \<longleftrightarrow> m \<le> n"
611     by (simp only: less_eq_num_def nat_of_num_numeral of_nat_le_iff)
612   then show ?thesis by simp
613 qed
615 lemma one_le_numeral: "1 \<le> numeral n"
616   using numeral_le_iff [of One n] by (simp add: numeral_One)
618 lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> One"
619   using numeral_le_iff [of n One] by (simp add: numeral_One)
621 lemma numeral_less_iff: "numeral m < numeral n \<longleftrightarrow> m < n"
622 proof -
623   have "of_nat (numeral m) < of_nat (numeral n) \<longleftrightarrow> m < n"
624     unfolding less_num_def nat_of_num_numeral of_nat_less_iff ..
625   then show ?thesis by simp
626 qed
628 lemma not_numeral_less_one: "\<not> numeral n < 1"
629   using numeral_less_iff [of n One] by (simp add: numeral_One)
631 lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> One < n"
632   using numeral_less_iff [of One n] by (simp add: numeral_One)
634 lemma zero_le_numeral: "0 \<le> numeral n"
635   by (induct n) (simp_all add: numeral.simps)
637 lemma zero_less_numeral: "0 < numeral n"
640 lemma not_numeral_le_zero: "\<not> numeral n \<le> 0"
641   by (simp add: not_le zero_less_numeral)
643 lemma not_numeral_less_zero: "\<not> numeral n < 0"
644   by (simp add: not_less zero_le_numeral)
646 lemmas le_numeral_extra =
647   zero_le_one not_one_le_zero
648   order_refl [of 0] order_refl [of 1]
650 lemmas less_numeral_extra =
651   zero_less_one not_one_less_zero
652   less_irrefl [of 0] less_irrefl [of 1]
654 lemmas le_numeral_simps [simp] =
655   numeral_le_iff
656   one_le_numeral
657   numeral_le_one_iff
658   zero_le_numeral
659   not_numeral_le_zero
661 lemmas less_numeral_simps [simp] =
662   numeral_less_iff
663   one_less_numeral_iff
664   not_numeral_less_one
665   zero_less_numeral
666   not_numeral_less_zero
668 lemma min_0_1 [simp]:
669   fixes min' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
670   defines "min' \<equiv> min"
671   shows
672     "min' 0 1 = 0"
673     "min' 1 0 = 0"
674     "min' 0 (numeral x) = 0"
675     "min' (numeral x) 0 = 0"
676     "min' 1 (numeral x) = 1"
677     "min' (numeral x) 1 = 1"
678   by (simp_all add: min'_def min_def le_num_One_iff)
680 lemma max_0_1 [simp]:
681   fixes max' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
682   defines "max' \<equiv> max"
683   shows
684     "max' 0 1 = 1"
685     "max' 1 0 = 1"
686     "max' 0 (numeral x) = numeral x"
687     "max' (numeral x) 0 = numeral x"
688     "max' 1 (numeral x) = numeral x"
689     "max' (numeral x) 1 = numeral x"
690   by (simp_all add: max'_def max_def le_num_One_iff)
692 end
695 subsubsection \<open>Multiplication and negation: class \<open>ring_1\<close>\<close>
697 context ring_1
698 begin
700 subclass neg_numeral ..
702 lemma mult_neg_numeral_simps:
703   "- numeral m * - numeral n = numeral (m * n)"
704   "- numeral m * numeral n = - numeral (m * n)"
705   "numeral m * - numeral n = - numeral (m * n)"
706   by (simp_all only: mult_minus_left mult_minus_right minus_minus numeral_mult)
708 lemma mult_minus1 [simp]: "- 1 * z = - z"
711 lemma mult_minus1_right [simp]: "z * - 1 = - z"
714 end
717 subsubsection \<open>Equality using \<open>iszero\<close> for rings with non-zero characteristic\<close>
719 context ring_1
720 begin
722 definition iszero :: "'a \<Rightarrow> bool"
723   where "iszero z \<longleftrightarrow> z = 0"
725 lemma iszero_0 [simp]: "iszero 0"
728 lemma not_iszero_1 [simp]: "\<not> iszero 1"
731 lemma not_iszero_Numeral1: "\<not> iszero Numeral1"
734 lemma not_iszero_neg_1 [simp]: "\<not> iszero (- 1)"
737 lemma not_iszero_neg_Numeral1: "\<not> iszero (- Numeral1)"
740 lemma iszero_neg_numeral [simp]: "iszero (- numeral w) \<longleftrightarrow> iszero (numeral w)"
741   unfolding iszero_def by (rule neg_equal_0_iff_equal)
743 lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)"
744   unfolding iszero_def by (rule eq_iff_diff_eq_0)
746 text \<open>
747   The \<open>eq_numeral_iff_iszero\<close> lemmas are not declared \<open>[simp]\<close> by default,
748   because for rings of characteristic zero, better simp rules are possible.
749   For a type like integers mod \<open>n\<close>, type-instantiated versions of these rules
750   should be added to the simplifier, along with a type-specific rule for
751   deciding propositions of the form \<open>iszero (numeral w)\<close>.
753   bh: Maybe it would not be so bad to just declare these as simp rules anyway?
754   I should test whether these rules take precedence over the \<open>ring_char_0\<close>
755   rules in the simplifier.
756 \<close>
758 lemma eq_numeral_iff_iszero:
759   "numeral x = numeral y \<longleftrightarrow> iszero (sub x y)"
760   "numeral x = - numeral y \<longleftrightarrow> iszero (numeral (x + y))"
761   "- numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
762   "- numeral x = - numeral y \<longleftrightarrow> iszero (sub y x)"
763   "numeral x = 1 \<longleftrightarrow> iszero (sub x One)"
764   "1 = numeral y \<longleftrightarrow> iszero (sub One y)"
765   "- numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
766   "1 = - numeral y \<longleftrightarrow> iszero (numeral (One + y))"
767   "numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
768   "0 = numeral y \<longleftrightarrow> iszero (numeral y)"
769   "- numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
770   "0 = - numeral y \<longleftrightarrow> iszero (numeral y)"
771   unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special
772   by simp_all
774 end
777 subsubsection \<open>Equality and negation: class \<open>ring_char_0\<close>\<close>
779 context ring_char_0
780 begin
782 lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
785 lemma neg_numeral_eq_iff: "- numeral m = - numeral n \<longleftrightarrow> m = n"
786   by simp
788 lemma numeral_neq_neg_numeral: "numeral m \<noteq> - numeral n"
791 lemma neg_numeral_neq_numeral: "- numeral m \<noteq> numeral n"
792   by (rule numeral_neq_neg_numeral [symmetric])
794 lemma zero_neq_neg_numeral: "0 \<noteq> - numeral n"
795   by simp
797 lemma neg_numeral_neq_zero: "- numeral n \<noteq> 0"
798   by simp
800 lemma one_neq_neg_numeral: "1 \<noteq> - numeral n"
801   using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One)
803 lemma neg_numeral_neq_one: "- numeral n \<noteq> 1"
804   using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One)
806 lemma neg_one_neq_numeral: "- 1 \<noteq> numeral n"
807   using neg_numeral_neq_numeral [of One n] by (simp add: numeral_One)
809 lemma numeral_neq_neg_one: "numeral n \<noteq> - 1"
810   using numeral_neq_neg_numeral [of n One] by (simp add: numeral_One)
812 lemma neg_one_eq_numeral_iff: "- 1 = - numeral n \<longleftrightarrow> n = One"
813   using neg_numeral_eq_iff [of One n] by (auto simp add: numeral_One)
815 lemma numeral_eq_neg_one_iff: "- numeral n = - 1 \<longleftrightarrow> n = One"
816   using neg_numeral_eq_iff [of n One] by (auto simp add: numeral_One)
818 lemma neg_one_neq_zero: "- 1 \<noteq> 0"
819   by simp
821 lemma zero_neq_neg_one: "0 \<noteq> - 1"
822   by simp
824 lemma neg_one_neq_one: "- 1 \<noteq> 1"
825   using neg_numeral_neq_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
827 lemma one_neq_neg_one: "1 \<noteq> - 1"
828   using numeral_neq_neg_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
830 lemmas eq_neg_numeral_simps [simp] =
831   neg_numeral_eq_iff
832   numeral_neq_neg_numeral neg_numeral_neq_numeral
833   one_neq_neg_numeral neg_numeral_neq_one
834   zero_neq_neg_numeral neg_numeral_neq_zero
835   neg_one_neq_numeral numeral_neq_neg_one
836   neg_one_eq_numeral_iff numeral_eq_neg_one_iff
837   neg_one_neq_zero zero_neq_neg_one
838   neg_one_neq_one one_neq_neg_one
840 end
843 subsubsection \<open>Structures with negation and order: class \<open>linordered_idom\<close>\<close>
845 context linordered_idom
846 begin
848 subclass ring_char_0 ..
850 lemma neg_numeral_le_iff: "- numeral m \<le> - numeral n \<longleftrightarrow> n \<le> m"
851   by (simp only: neg_le_iff_le numeral_le_iff)
853 lemma neg_numeral_less_iff: "- numeral m < - numeral n \<longleftrightarrow> n < m"
854   by (simp only: neg_less_iff_less numeral_less_iff)
856 lemma neg_numeral_less_zero: "- numeral n < 0"
857   by (simp only: neg_less_0_iff_less zero_less_numeral)
859 lemma neg_numeral_le_zero: "- numeral n \<le> 0"
860   by (simp only: neg_le_0_iff_le zero_le_numeral)
862 lemma not_zero_less_neg_numeral: "\<not> 0 < - numeral n"
863   by (simp only: not_less neg_numeral_le_zero)
865 lemma not_zero_le_neg_numeral: "\<not> 0 \<le> - numeral n"
866   by (simp only: not_le neg_numeral_less_zero)
868 lemma neg_numeral_less_numeral: "- numeral m < numeral n"
869   using neg_numeral_less_zero zero_less_numeral by (rule less_trans)
871 lemma neg_numeral_le_numeral: "- numeral m \<le> numeral n"
872   by (simp only: less_imp_le neg_numeral_less_numeral)
874 lemma not_numeral_less_neg_numeral: "\<not> numeral m < - numeral n"
875   by (simp only: not_less neg_numeral_le_numeral)
877 lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> - numeral n"
878   by (simp only: not_le neg_numeral_less_numeral)
880 lemma neg_numeral_less_one: "- numeral m < 1"
881   by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One])
883 lemma neg_numeral_le_one: "- numeral m \<le> 1"
884   by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One])
886 lemma not_one_less_neg_numeral: "\<not> 1 < - numeral m"
887   by (simp only: not_less neg_numeral_le_one)
889 lemma not_one_le_neg_numeral: "\<not> 1 \<le> - numeral m"
890   by (simp only: not_le neg_numeral_less_one)
892 lemma not_numeral_less_neg_one: "\<not> numeral m < - 1"
893   using not_numeral_less_neg_numeral [of m One] by (simp add: numeral_One)
895 lemma not_numeral_le_neg_one: "\<not> numeral m \<le> - 1"
896   using not_numeral_le_neg_numeral [of m One] by (simp add: numeral_One)
898 lemma neg_one_less_numeral: "- 1 < numeral m"
899   using neg_numeral_less_numeral [of One m] by (simp add: numeral_One)
901 lemma neg_one_le_numeral: "- 1 \<le> numeral m"
902   using neg_numeral_le_numeral [of One m] by (simp add: numeral_One)
904 lemma neg_numeral_less_neg_one_iff: "- numeral m < - 1 \<longleftrightarrow> m \<noteq> One"
905   by (cases m) simp_all
907 lemma neg_numeral_le_neg_one: "- numeral m \<le> - 1"
908   by simp
910 lemma not_neg_one_less_neg_numeral: "\<not> - 1 < - numeral m"
911   by simp
913 lemma not_neg_one_le_neg_numeral_iff: "\<not> - 1 \<le> - numeral m \<longleftrightarrow> m \<noteq> One"
914   by (cases m) simp_all
916 lemma sub_non_negative: "sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m"
917   by (simp only: sub_def le_diff_eq) simp
919 lemma sub_positive: "sub n m > 0 \<longleftrightarrow> n > m"
920   by (simp only: sub_def less_diff_eq) simp
922 lemma sub_non_positive: "sub n m \<le> 0 \<longleftrightarrow> n \<le> m"
923   by (simp only: sub_def diff_le_eq) simp
925 lemma sub_negative: "sub n m < 0 \<longleftrightarrow> n < m"
926   by (simp only: sub_def diff_less_eq) simp
928 lemmas le_neg_numeral_simps [simp] =
929   neg_numeral_le_iff
930   neg_numeral_le_numeral not_numeral_le_neg_numeral
931   neg_numeral_le_zero not_zero_le_neg_numeral
932   neg_numeral_le_one not_one_le_neg_numeral
933   neg_one_le_numeral not_numeral_le_neg_one
934   neg_numeral_le_neg_one not_neg_one_le_neg_numeral_iff
936 lemma le_minus_one_simps [simp]:
937   "- 1 \<le> 0"
938   "- 1 \<le> 1"
939   "\<not> 0 \<le> - 1"
940   "\<not> 1 \<le> - 1"
941   by simp_all
943 lemmas less_neg_numeral_simps [simp] =
944   neg_numeral_less_iff
945   neg_numeral_less_numeral not_numeral_less_neg_numeral
946   neg_numeral_less_zero not_zero_less_neg_numeral
947   neg_numeral_less_one not_one_less_neg_numeral
948   neg_one_less_numeral not_numeral_less_neg_one
949   neg_numeral_less_neg_one_iff not_neg_one_less_neg_numeral
951 lemma less_minus_one_simps [simp]:
952   "- 1 < 0"
953   "- 1 < 1"
954   "\<not> 0 < - 1"
955   "\<not> 1 < - 1"
958 lemma abs_numeral [simp]: "\<bar>numeral n\<bar> = numeral n"
959   by simp
961 lemma abs_neg_numeral [simp]: "\<bar>- numeral n\<bar> = numeral n"
962   by (simp only: abs_minus_cancel abs_numeral)
964 lemma abs_neg_one [simp]: "\<bar>- 1\<bar> = 1"
965   by simp
967 end
970 subsubsection \<open>Natural numbers\<close>
972 lemma Suc_1 [simp]: "Suc 1 = 2"
973   unfolding Suc_eq_plus1 by (rule one_add_one)
975 lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"
976   unfolding Suc_eq_plus1 by (rule numeral_plus_one)
978 definition pred_numeral :: "num \<Rightarrow> nat"
979   where [code del]: "pred_numeral k = numeral k - 1"
981 lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
984 lemma eval_nat_numeral:
985   "numeral One = Suc 0"
986   "numeral (Bit0 n) = Suc (numeral (BitM n))"
987   "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
988   by (simp_all add: numeral.simps BitM_plus_one)
990 lemma pred_numeral_simps [simp]:
991   "pred_numeral One = 0"
992   "pred_numeral (Bit0 k) = numeral (BitM k)"
993   "pred_numeral (Bit1 k) = numeral (Bit0 k)"
994   by (simp_all only: pred_numeral_def eval_nat_numeral diff_Suc_Suc diff_0)
996 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
999 lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
1002 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
1003   by (simp only: numeral_One One_nat_def)
1005 lemma Suc_nat_number_of_add: "Suc (numeral v + n) = numeral (v + One) + n"
1006   by simp
1008 lemma numerals: "Numeral1 = (1::nat)" "2 = Suc (Suc 0)"
1009   by (rule numeral_One) (rule numeral_2_eq_2)
1011 lemmas numeral_nat = eval_nat_numeral BitM.simps One_nat_def
1013 text \<open>Comparisons involving @{term Suc}.\<close>
1015 lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n"
1018 lemma Suc_eq_numeral [simp]: "Suc n = numeral k \<longleftrightarrow> n = pred_numeral k"
1021 lemma less_numeral_Suc [simp]: "numeral k < Suc n \<longleftrightarrow> pred_numeral k < n"
1024 lemma less_Suc_numeral [simp]: "Suc n < numeral k \<longleftrightarrow> n < pred_numeral k"
1027 lemma le_numeral_Suc [simp]: "numeral k \<le> Suc n \<longleftrightarrow> pred_numeral k \<le> n"
1030 lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
1033 lemma diff_Suc_numeral [simp]: "Suc n - numeral k = n - pred_numeral k"
1036 lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n"
1039 lemma max_Suc_numeral [simp]: "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
1042 lemma max_numeral_Suc [simp]: "max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)"
1045 lemma min_Suc_numeral [simp]: "min (Suc n) (numeral k) = Suc (min n (pred_numeral k))"
1048 lemma min_numeral_Suc [simp]: "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
1051 text \<open>For @{term case_nat} and @{term rec_nat}.\<close>
1053 lemma case_nat_numeral [simp]: "case_nat a f (numeral v) = (let pv = pred_numeral v in f pv)"
1057   "case_nat a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
1060 lemma rec_nat_numeral [simp]:
1061   "rec_nat a f (numeral v) = (let pv = pred_numeral v in f pv (rec_nat a f pv))"
1062   by (simp add: numeral_eq_Suc Let_def)
1065   "rec_nat a f (numeral v + n) = (let pv = pred_numeral v in f (pv + n) (rec_nat a f (pv + n)))"
1066   by (simp add: numeral_eq_Suc Let_def)
1068 text \<open>Case analysis on @{term "n < 2"}.\<close>
1069 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0"
1070   by (auto simp add: numeral_2_eq_2)
1072 text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2.\<close>
1073 text \<open>bh: Are these rules really a good idea?\<close>
1075 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
1076   by simp
1078 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
1079   by simp
1081 text \<open>Can be used to eliminate long strings of Sucs, but not by default.\<close>
1082 lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
1083   by simp
1088 subsection \<open>Particular lemmas concerning @{term 2}\<close>
1090 context linordered_field
1091 begin
1093 subclass field_char_0 ..
1095 lemma half_gt_zero_iff: "0 < a / 2 \<longleftrightarrow> 0 < a"
1096   by (auto simp add: field_simps)
1098 lemma half_gt_zero [simp]: "0 < a \<Longrightarrow> 0 < a / 2"
1101 end
1104 subsection \<open>Numeral equations as default simplification rules\<close>
1106 declare (in numeral) numeral_One [simp]
1107 declare (in numeral) numeral_plus_numeral [simp]
1108 declare (in numeral) add_numeral_special [simp]
1109 declare (in neg_numeral) add_neg_numeral_simps [simp]
1110 declare (in neg_numeral) add_neg_numeral_special [simp]
1111 declare (in neg_numeral) diff_numeral_simps [simp]
1112 declare (in neg_numeral) diff_numeral_special [simp]
1113 declare (in semiring_numeral) numeral_times_numeral [simp]
1114 declare (in ring_1) mult_neg_numeral_simps [simp]
1116 subsection \<open>Setting up simprocs\<close>
1118 lemma mult_numeral_1: "Numeral1 * a = a"
1119   for a :: "'a::semiring_numeral"
1120   by simp
1122 lemma mult_numeral_1_right: "a * Numeral1 = a"
1123   for a :: "'a::semiring_numeral"
1124   by simp
1126 lemma divide_numeral_1: "a / Numeral1 = a"
1127   for a :: "'a::field"
1128   by simp
1130 lemma inverse_numeral_1: "inverse Numeral1 = (Numeral1::'a::division_ring)"
1131   by simp
1133 text \<open>
1134   Theorem lists for the cancellation simprocs. The use of a binary
1135   numeral for 1 reduces the number of special cases.
1136 \<close>
1138 lemma mult_1s:
1139   "Numeral1 * a = a"
1140   "a * Numeral1 = a"
1141   "- Numeral1 * b = - b"
1142   "b * - Numeral1 = - b"
1143   for a :: "'a::semiring_numeral" and b :: "'b::ring_1"
1144   by simp_all
1146 setup \<open>
1148     (fn Const (@{const_name numeral}, _) \$ _ => true
1149       | Const (@{const_name uminus}, _) \$ (Const (@{const_name numeral}, _) \$ _) => true
1150       | _ => false)
1151 \<close>
1153 simproc_setup reorient_numeral ("numeral w = x" | "- numeral w = y") =
1154   Reorient_Proc.proc
1157 subsubsection \<open>Simplification of arithmetic operations on integer constants\<close>
1159 lemmas arith_special = (* already declared simp above *)
1161   diff_numeral_special
1163 lemmas arith_extra_simps = (* rules already in simpset *)
1165   minus_zero
1166   diff_numeral_simps diff_0 diff_0_right
1167   numeral_times_numeral mult_neg_numeral_simps
1168   mult_zero_left mult_zero_right
1169   abs_numeral abs_neg_numeral
1171 text \<open>
1172   For making a minimal simpset, one must include these default simprules.
1173   Also include \<open>simp_thms\<close>.
1174 \<close>
1176 lemmas arith_simps =
1178   BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps
1179   abs_zero abs_one arith_extra_simps
1181 lemmas more_arith_simps =
1182   neg_le_iff_le
1183   minus_zero left_minus right_minus
1184   mult_1_left mult_1_right
1185   mult_minus_left mult_minus_right
1188 lemmas of_nat_simps =
1189   of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
1191 text \<open>Simplification of relational operations.\<close>
1193 lemmas eq_numeral_extra =
1194   zero_neq_one one_neq_zero
1196 lemmas rel_simps =
1197   le_num_simps less_num_simps eq_num_simps
1198   le_numeral_simps le_neg_numeral_simps le_minus_one_simps le_numeral_extra
1199   less_numeral_simps less_neg_numeral_simps less_minus_one_simps less_numeral_extra
1200   eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
1202 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
1203   \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
1204   unfolding Let_def ..
1206 lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
1207   \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
1208   unfolding Let_def ..
1210 declaration \<open>
1211 let
1212   fun number_of ctxt T n =
1213     if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral}))
1214     then raise CTERM ("number_of", [])
1215     else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
1216 in
1217   K (
1219       @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
1220         arith_special numeral_One of_nat_simps uminus_numeral_One}
1222       @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
1223         le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc
1224         Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral}
1225     #> Lin_Arith.set_number_of number_of)
1226 end
1227 \<close>
1230 subsubsection \<open>Simplification of arithmetic when nested to the right\<close>
1232 lemma add_numeral_left [simp]: "numeral v + (numeral w + z) = (numeral(v + w) + z)"
1236   "numeral v + (- numeral w + y) = (sub v w + y)"
1237   "- numeral v + (numeral w + y) = (sub w v + y)"
1238   "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
1241 lemma mult_numeral_left [simp]:
1242   "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
1243   "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
1244   "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
1245   "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
1246   by (simp_all add: mult.assoc [symmetric])
1248 hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
1251 subsection \<open>Code module namespace\<close>
1253 code_identifier
1254   code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1256 subsection \<open>Printing of evaluated natural numbers as numerals\<close>
1258 lemma [code_post]:
1259   "Suc 0 = 1"
1260   "Suc 1 = 2"
1261   "Suc (numeral n) = numeral (Num.inc n)"