src/HOL/Code_Numeral.thy
 author haftmann Sun Oct 08 22:28:22 2017 +0200 (20 months ago) changeset 66815 93c6632ddf44 parent 66806 a4e82b58d833 child 66817 0b12755ccbb2 permissions -rw-r--r--
one uniform type class for parity structures
1 (*  Title:      HOL/Code_Numeral.thy
2     Author:     Florian Haftmann, TU Muenchen
3 *)
5 section \<open>Numeric types for code generation onto target language numerals only\<close>
7 theory Code_Numeral
8 imports Nat_Transfer Divides Lifting
9 begin
11 subsection \<open>Type of target language integers\<close>
13 typedef integer = "UNIV :: int set"
14   morphisms int_of_integer integer_of_int ..
16 setup_lifting type_definition_integer
18 lemma integer_eq_iff:
19   "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
20   by transfer rule
22 lemma integer_eqI:
23   "int_of_integer k = int_of_integer l \<Longrightarrow> k = l"
24   using integer_eq_iff [of k l] by simp
26 lemma int_of_integer_integer_of_int [simp]:
27   "int_of_integer (integer_of_int k) = k"
28   by transfer rule
30 lemma integer_of_int_int_of_integer [simp]:
31   "integer_of_int (int_of_integer k) = k"
32   by transfer rule
34 instantiation integer :: ring_1
35 begin
37 lift_definition zero_integer :: integer
38   is "0 :: int"
39   .
41 declare zero_integer.rep_eq [simp]
43 lift_definition one_integer :: integer
44   is "1 :: int"
45   .
47 declare one_integer.rep_eq [simp]
49 lift_definition plus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
50   is "plus :: int \<Rightarrow> int \<Rightarrow> int"
51   .
53 declare plus_integer.rep_eq [simp]
55 lift_definition uminus_integer :: "integer \<Rightarrow> integer"
56   is "uminus :: int \<Rightarrow> int"
57   .
59 declare uminus_integer.rep_eq [simp]
61 lift_definition minus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
62   is "minus :: int \<Rightarrow> int \<Rightarrow> int"
63   .
65 declare minus_integer.rep_eq [simp]
67 lift_definition times_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
68   is "times :: int \<Rightarrow> int \<Rightarrow> int"
69   .
71 declare times_integer.rep_eq [simp]
73 instance proof
74 qed (transfer, simp add: algebra_simps)+
76 end
78 instance integer :: Rings.dvd ..
80 lemma [transfer_rule]:
81   "rel_fun pcr_integer (rel_fun pcr_integer HOL.iff) Rings.dvd Rings.dvd"
82   unfolding dvd_def by transfer_prover
84 lemma [transfer_rule]:
85   "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
86   by (rule transfer_rule_of_nat) transfer_prover+
88 lemma [transfer_rule]:
89   "rel_fun HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
90 proof -
91   have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
92     by (rule transfer_rule_of_int) transfer_prover+
93   then show ?thesis by (simp add: id_def)
94 qed
96 lemma [transfer_rule]:
97   "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
98   by (rule transfer_rule_numeral) transfer_prover+
100 lemma [transfer_rule]:
101   "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
102   by (unfold Num.sub_def [abs_def]) transfer_prover
104 lemma int_of_integer_of_nat [simp]:
105   "int_of_integer (of_nat n) = of_nat n"
106   by transfer rule
108 lift_definition integer_of_nat :: "nat \<Rightarrow> integer"
109   is "of_nat :: nat \<Rightarrow> int"
110   .
112 lemma integer_of_nat_eq_of_nat [code]:
113   "integer_of_nat = of_nat"
114   by transfer rule
116 lemma int_of_integer_integer_of_nat [simp]:
117   "int_of_integer (integer_of_nat n) = of_nat n"
118   by transfer rule
120 lift_definition nat_of_integer :: "integer \<Rightarrow> nat"
121   is Int.nat
122   .
124 lemma nat_of_integer_of_nat [simp]:
125   "nat_of_integer (of_nat n) = n"
126   by transfer simp
128 lemma int_of_integer_of_int [simp]:
129   "int_of_integer (of_int k) = k"
130   by transfer simp
132 lemma nat_of_integer_integer_of_nat [simp]:
133   "nat_of_integer (integer_of_nat n) = n"
134   by transfer simp
136 lemma integer_of_int_eq_of_int [simp, code_abbrev]:
137   "integer_of_int = of_int"
138   by transfer (simp add: fun_eq_iff)
140 lemma of_int_integer_of [simp]:
141   "of_int (int_of_integer k) = (k :: integer)"
142   by transfer rule
144 lemma int_of_integer_numeral [simp]:
145   "int_of_integer (numeral k) = numeral k"
146   by transfer rule
148 lemma int_of_integer_sub [simp]:
149   "int_of_integer (Num.sub k l) = Num.sub k l"
150   by transfer rule
152 definition integer_of_num :: "num \<Rightarrow> integer"
153   where [simp]: "integer_of_num = numeral"
155 lemma integer_of_num [code]:
156   "integer_of_num Num.One = 1"
157   "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)"
158   "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
159   by (simp_all only: integer_of_num_def numeral.simps Let_def)
161 lemma integer_of_num_triv:
162   "integer_of_num Num.One = 1"
163   "integer_of_num (Num.Bit0 Num.One) = 2"
164   by simp_all
166 instantiation integer :: "{linordered_idom, equal}"
167 begin
169 lift_definition abs_integer :: "integer \<Rightarrow> integer"
170   is "abs :: int \<Rightarrow> int"
171   .
173 declare abs_integer.rep_eq [simp]
175 lift_definition sgn_integer :: "integer \<Rightarrow> integer"
176   is "sgn :: int \<Rightarrow> int"
177   .
179 declare sgn_integer.rep_eq [simp]
181 lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
182   is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
183   .
186 lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
187   is "less :: int \<Rightarrow> int \<Rightarrow> bool"
188   .
190 lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
191   is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
192   .
194 instance
195   by standard (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
197 end
199 lemma [transfer_rule]:
200   "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
201   by (unfold min_def [abs_def]) transfer_prover
203 lemma [transfer_rule]:
204   "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
205   by (unfold max_def [abs_def]) transfer_prover
207 lemma int_of_integer_min [simp]:
208   "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
209   by transfer rule
211 lemma int_of_integer_max [simp]:
212   "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)"
213   by transfer rule
215 lemma nat_of_integer_non_positive [simp]:
216   "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0"
217   by transfer simp
219 lemma of_nat_of_integer [simp]:
220   "of_nat (nat_of_integer k) = max 0 k"
221   by transfer auto
223 instantiation integer :: normalization_semidom
224 begin
226 lift_definition normalize_integer :: "integer \<Rightarrow> integer"
227   is "normalize :: int \<Rightarrow> int"
228   .
230 declare normalize_integer.rep_eq [simp]
232 lift_definition unit_factor_integer :: "integer \<Rightarrow> integer"
233   is "unit_factor :: int \<Rightarrow> int"
234   .
236 declare unit_factor_integer.rep_eq [simp]
238 lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
239   is "divide :: int \<Rightarrow> int \<Rightarrow> int"
240   .
242 declare divide_integer.rep_eq [simp]
244 instance
245   by (standard; transfer)
246     (auto simp add: mult_sgn_abs sgn_mult abs_eq_iff')
248 end
250 instantiation integer :: unique_euclidean_ring
251 begin
253 lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
254   is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
255   .
257 declare modulo_integer.rep_eq [simp]
259 lift_definition euclidean_size_integer :: "integer \<Rightarrow> nat"
260   is "euclidean_size :: int \<Rightarrow> nat"
261   .
263 declare euclidean_size_integer.rep_eq [simp]
265 lift_definition uniqueness_constraint_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
266   is "uniqueness_constraint :: int \<Rightarrow> int \<Rightarrow> bool"
267   .
269 declare uniqueness_constraint_integer.rep_eq [simp]
271 instance
272   by (standard; transfer)
273     (use mult_le_mono2 [of 1] in \<open>auto simp add: sgn_mult_abs abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>, rule div_eqI, simp_all)
275 end
277 lemma [code]:
278   "euclidean_size = nat_of_integer \<circ> abs"
279   by (simp add: fun_eq_iff nat_of_integer.rep_eq)
281 lemma [code]:
282   "uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
285 instance integer :: ring_parity
286   by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
288 instantiation integer :: unique_euclidean_semiring_numeral
289 begin
291 definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"
292 where
293   divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)"
295 definition divmod_step_integer :: "num \<Rightarrow> integer \<times> integer \<Rightarrow> integer \<times> integer"
296 where
297   "divmod_step_integer l qr = (let (q, r) = qr
298     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
299     else (2 * q, r))"
301 instance proof
302   show "divmod m n = (numeral m div numeral n :: integer, numeral m mod numeral n)"
303     for m n by (fact divmod_integer'_def)
304   show "divmod_step l qr = (let (q, r) = qr
305     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
306     else (2 * q, r))" for l and qr :: "integer \<times> integer"
307     by (fact divmod_step_integer_def)
308 qed (transfer,
310   unique_euclidean_semiring_numeral_class.div_less
311   unique_euclidean_semiring_numeral_class.mod_less
312   unique_euclidean_semiring_numeral_class.div_positive
313   unique_euclidean_semiring_numeral_class.mod_less_eq_dividend
314   unique_euclidean_semiring_numeral_class.pos_mod_bound
315   unique_euclidean_semiring_numeral_class.pos_mod_sign
316   unique_euclidean_semiring_numeral_class.mod_mult2_eq
317   unique_euclidean_semiring_numeral_class.div_mult2_eq
318   unique_euclidean_semiring_numeral_class.discrete)+
320 end
322 declare divmod_algorithm_code [where ?'a = integer,
323   folded integer_of_num_def, unfolded integer_of_num_triv,
324   code]
326 lemma integer_of_nat_0: "integer_of_nat 0 = 0"
327 by transfer simp
329 lemma integer_of_nat_1: "integer_of_nat 1 = 1"
330 by transfer simp
332 lemma integer_of_nat_numeral:
333   "integer_of_nat (numeral n) = numeral n"
334 by transfer simp
336 subsection \<open>Code theorems for target language integers\<close>
338 text \<open>Constructors\<close>
340 definition Pos :: "num \<Rightarrow> integer"
341 where
342   [simp, code_post]: "Pos = numeral"
344 lemma [transfer_rule]:
345   "rel_fun HOL.eq pcr_integer numeral Pos"
346   by simp transfer_prover
348 lemma Pos_fold [code_unfold]:
349   "numeral Num.One = Pos Num.One"
350   "numeral (Num.Bit0 k) = Pos (Num.Bit0 k)"
351   "numeral (Num.Bit1 k) = Pos (Num.Bit1 k)"
352   by simp_all
354 definition Neg :: "num \<Rightarrow> integer"
355 where
356   [simp, code_abbrev]: "Neg n = - Pos n"
358 lemma [transfer_rule]:
359   "rel_fun HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
360   by (simp add: Neg_def [abs_def]) transfer_prover
362 code_datatype "0::integer" Pos Neg
365 text \<open>A further pair of constructors for generated computations\<close>
367 context
368 begin
370 qualified definition positive :: "num \<Rightarrow> integer"
371   where [simp]: "positive = numeral"
373 qualified definition negative :: "num \<Rightarrow> integer"
374   where [simp]: "negative = uminus \<circ> numeral"
376 lemma [code_computation_unfold]:
377   "numeral = positive"
378   "Pos = positive"
379   "Neg = negative"
382 end
385 text \<open>Auxiliary operations\<close>
387 lift_definition dup :: "integer \<Rightarrow> integer"
388   is "\<lambda>k::int. k + k"
389   .
391 lemma dup_code [code]:
392   "dup 0 = 0"
393   "dup (Pos n) = Pos (Num.Bit0 n)"
394   "dup (Neg n) = Neg (Num.Bit0 n)"
395   by (transfer, simp only: numeral_Bit0 minus_add_distrib)+
397 lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
398   is "\<lambda>m n. numeral m - numeral n :: int"
399   .
401 lemma sub_code [code]:
402   "sub Num.One Num.One = 0"
403   "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
404   "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
405   "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
406   "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
407   "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
408   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
409   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
410   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
411   by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+
414 text \<open>Implementations\<close>
416 lemma one_integer_code [code, code_unfold]:
417   "1 = Pos Num.One"
418   by simp
420 lemma plus_integer_code [code]:
421   "k + 0 = (k::integer)"
422   "0 + l = (l::integer)"
423   "Pos m + Pos n = Pos (m + n)"
424   "Pos m + Neg n = sub m n"
425   "Neg m + Pos n = sub n m"
426   "Neg m + Neg n = Neg (m + n)"
427   by (transfer, simp)+
429 lemma uminus_integer_code [code]:
430   "uminus 0 = (0::integer)"
431   "uminus (Pos m) = Neg m"
432   "uminus (Neg m) = Pos m"
433   by simp_all
435 lemma minus_integer_code [code]:
436   "k - 0 = (k::integer)"
437   "0 - l = uminus (l::integer)"
438   "Pos m - Pos n = sub m n"
439   "Pos m - Neg n = Pos (m + n)"
440   "Neg m - Pos n = Neg (m + n)"
441   "Neg m - Neg n = sub n m"
442   by (transfer, simp)+
444 lemma abs_integer_code [code]:
445   "\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)"
446   by simp
448 lemma sgn_integer_code [code]:
449   "sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)"
450   by simp
452 lemma times_integer_code [code]:
453   "k * 0 = (0::integer)"
454   "0 * l = (0::integer)"
455   "Pos m * Pos n = Pos (m * n)"
456   "Pos m * Neg n = Neg (m * n)"
457   "Neg m * Pos n = Neg (m * n)"
458   "Neg m * Neg n = Pos (m * n)"
459   by simp_all
461 lemma normalize_integer_code [code]:
462   "normalize = (abs :: integer \<Rightarrow> integer)"
463   by transfer simp
465 lemma unit_factor_integer_code [code]:
466   "unit_factor = (sgn :: integer \<Rightarrow> integer)"
467   by transfer simp
469 definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
470 where
471   "divmod_integer k l = (k div l, k mod l)"
473 lemma fst_divmod_integer [simp]:
474   "fst (divmod_integer k l) = k div l"
477 lemma snd_divmod_integer [simp]:
478   "snd (divmod_integer k l) = k mod l"
481 definition divmod_abs :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
482 where
483   "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
485 lemma fst_divmod_abs [simp]:
486   "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"
489 lemma snd_divmod_abs [simp]:
490   "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
493 lemma divmod_abs_code [code]:
494   "divmod_abs (Pos k) (Pos l) = divmod k l"
495   "divmod_abs (Neg k) (Neg l) = divmod k l"
496   "divmod_abs (Neg k) (Pos l) = divmod k l"
497   "divmod_abs (Pos k) (Neg l) = divmod k l"
498   "divmod_abs j 0 = (0, \<bar>j\<bar>)"
499   "divmod_abs 0 j = (0, 0)"
502 lemma divmod_integer_code [code]:
503   "divmod_integer k l =
504     (if k = 0 then (0, 0) else if l = 0 then (0, k) else
505     (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
506       then divmod_abs k l
507       else (let (r, s) = divmod_abs k l in
508         if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
509 proof -
510   have aux1: "\<And>k l::int. sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0"
511     by (auto simp add: sgn_if)
512   have aux2: "\<And>q::int. - int_of_integer k = int_of_integer l * q \<longleftrightarrow> int_of_integer k = int_of_integer l * - q" by auto
513   show ?thesis
514     by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1)
515       (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
516 qed
518 lemma div_integer_code [code]:
519   "k div l = fst (divmod_integer k l)"
520   by simp
522 lemma mod_integer_code [code]:
523   "k mod l = snd (divmod_integer k l)"
524   by simp
526 lemma equal_integer_code [code]:
527   "HOL.equal 0 (0::integer) \<longleftrightarrow> True"
528   "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
529   "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
530   "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
531   "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
532   "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
533   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
534   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
535   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
538 lemma equal_integer_refl [code nbe]:
539   "HOL.equal (k::integer) k \<longleftrightarrow> True"
540   by (fact equal_refl)
542 lemma less_eq_integer_code [code]:
543   "0 \<le> (0::integer) \<longleftrightarrow> True"
544   "0 \<le> Pos l \<longleftrightarrow> True"
545   "0 \<le> Neg l \<longleftrightarrow> False"
546   "Pos k \<le> 0 \<longleftrightarrow> False"
547   "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
548   "Pos k \<le> Neg l \<longleftrightarrow> False"
549   "Neg k \<le> 0 \<longleftrightarrow> True"
550   "Neg k \<le> Pos l \<longleftrightarrow> True"
551   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
552   by simp_all
554 lemma less_integer_code [code]:
555   "0 < (0::integer) \<longleftrightarrow> False"
556   "0 < Pos l \<longleftrightarrow> True"
557   "0 < Neg l \<longleftrightarrow> False"
558   "Pos k < 0 \<longleftrightarrow> False"
559   "Pos k < Pos l \<longleftrightarrow> k < l"
560   "Pos k < Neg l \<longleftrightarrow> False"
561   "Neg k < 0 \<longleftrightarrow> True"
562   "Neg k < Pos l \<longleftrightarrow> True"
563   "Neg k < Neg l \<longleftrightarrow> l < k"
564   by simp_all
566 lift_definition num_of_integer :: "integer \<Rightarrow> num"
567   is "num_of_nat \<circ> nat"
568   .
570 lemma num_of_integer_code [code]:
571   "num_of_integer k = (if k \<le> 1 then Num.One
572      else let
573        (l, j) = divmod_integer k 2;
574        l' = num_of_integer l;
575        l'' = l' + l'
576      in if j = 0 then l'' else l'' + Num.One)"
577 proof -
578   {
579     assume "int_of_integer k mod 2 = 1"
580     then have "nat (int_of_integer k mod 2) = nat 1" by simp
581     moreover assume *: "1 < int_of_integer k"
582     ultimately have **: "nat (int_of_integer k) mod 2 = 1" by (simp add: nat_mod_distrib)
583     have "num_of_nat (nat (int_of_integer k)) =
584       num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)"
585       by simp
586     then have "num_of_nat (nat (int_of_integer k)) =
587       num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)"
589     with ** have "num_of_nat (nat (int_of_integer k)) =
590       num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)"
591       by simp
592   }
593   note aux = this
594   show ?thesis
595     by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta
596       not_le integer_eq_iff less_eq_integer_def
597       nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
598        mult_2 [where 'a=nat] aux add_One)
599 qed
601 lemma nat_of_integer_code [code]:
602   "nat_of_integer k = (if k \<le> 0 then 0
603      else let
604        (l, j) = divmod_integer k 2;
605        l' = nat_of_integer l;
606        l'' = l' + l'
607      in if j = 0 then l'' else l'' + 1)"
608 proof -
609   obtain j where "k = integer_of_int j"
610   proof
611     show "k = integer_of_int (int_of_integer k)" by simp
612   qed
613   moreover have "2 * (j div 2) = j - j mod 2"
614     by (simp add: minus_mod_eq_mult_div [symmetric] mult.commute)
615   ultimately show ?thesis
616     by (auto simp add: split_def Let_def modulo_integer_def nat_of_integer_def not_le
618       (auto simp add: mult_2 [symmetric])
619 qed
621 lemma int_of_integer_code [code]:
622   "int_of_integer k = (if k < 0 then - (int_of_integer (- k))
623      else if k = 0 then 0
624      else let
625        (l, j) = divmod_integer k 2;
626        l' = 2 * int_of_integer l
627      in if j = 0 then l' else l' + 1)"
628   by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
630 lemma integer_of_int_code [code]:
631   "integer_of_int k = (if k < 0 then - (integer_of_int (- k))
632      else if k = 0 then 0
633      else let
634        l = 2 * integer_of_int (k div 2);
635        j = k mod 2
636      in if j = 0 then l else l + 1)"
637   by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
639 hide_const (open) Pos Neg sub dup divmod_abs
642 subsection \<open>Serializer setup for target language integers\<close>
644 code_reserved Eval int Integer abs
646 code_printing
647   type_constructor integer \<rightharpoonup>
648     (SML) "IntInf.int"
649     and (OCaml) "Big'_int.big'_int"
651     and (Scala) "BigInt"
652     and (Eval) "int"
653 | class_instance integer :: equal \<rightharpoonup>
656 code_printing
657   constant "0::integer" \<rightharpoonup>
658     (SML) "!(0/ :/ IntInf.int)"
659     and (OCaml) "Big'_int.zero'_big'_int"
660     and (Haskell) "!(0/ ::/ Integer)"
661     and (Scala) "BigInt(0)"
663 setup \<open>
664   fold (fn target =>
665     Numeral.add_code @{const_name Code_Numeral.Pos} I Code_Printer.literal_numeral target
666     #> Numeral.add_code @{const_name Code_Numeral.Neg} (op ~) Code_Printer.literal_numeral target)
668 \<close>
670 code_printing
671   constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
672     (SML) "IntInf.+ ((_), (_))"
674     and (Haskell) infixl 6 "+"
675     and (Scala) infixl 7 "+"
676     and (Eval) infixl 8 "+"
677 | constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup>
678     (SML) "IntInf.~"
679     and (OCaml) "Big'_int.minus'_big'_int"
681     and (Scala) "!(- _)"
682     and (Eval) "~/ _"
683 | constant "minus :: integer \<Rightarrow> _" \<rightharpoonup>
684     (SML) "IntInf.- ((_), (_))"
685     and (OCaml) "Big'_int.sub'_big'_int"
686     and (Haskell) infixl 6 "-"
687     and (Scala) infixl 7 "-"
688     and (Eval) infixl 8 "-"
689 | constant Code_Numeral.dup \<rightharpoonup>
690     (SML) "IntInf.*/ (2,/ (_))"
691     and (OCaml) "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)"
692     and (Haskell) "!(2 * _)"
693     and (Scala) "!(2 * _)"
694     and (Eval) "!(2 * _)"
695 | constant Code_Numeral.sub \<rightharpoonup>
696     (SML) "!(raise/ Fail/ \"sub\")"
697     and (OCaml) "failwith/ \"sub\""
699     and (Scala) "!sys.error(\"sub\")"
700 | constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
701     (SML) "IntInf.* ((_), (_))"
702     and (OCaml) "Big'_int.mult'_big'_int"
703     and (Haskell) infixl 7 "*"
704     and (Scala) infixl 8 "*"
705     and (Eval) infixl 9 "*"
706 | constant Code_Numeral.divmod_abs \<rightharpoonup>
707     (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)"
708     and (OCaml) "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)"
709     and (Haskell) "divMod/ (abs _)/ (abs _)"
710     and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))"
711     and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
712 | constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
713     (SML) "!((_ : IntInf.int) = _)"
714     and (OCaml) "Big'_int.eq'_big'_int"
715     and (Haskell) infix 4 "=="
716     and (Scala) infixl 5 "=="
717     and (Eval) infixl 6 "="
718 | constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
719     (SML) "IntInf.<= ((_), (_))"
720     and (OCaml) "Big'_int.le'_big'_int"
721     and (Haskell) infix 4 "<="
722     and (Scala) infixl 4 "<="
723     and (Eval) infixl 6 "<="
724 | constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
725     (SML) "IntInf.< ((_), (_))"
726     and (OCaml) "Big'_int.lt'_big'_int"
727     and (Haskell) infix 4 "<"
728     and (Scala) infixl 4 "<"
729     and (Eval) infixl 6 "<"
730 | constant "abs :: integer \<Rightarrow> _" \<rightharpoonup>
731     (SML) "IntInf.abs"
732     and (OCaml) "Big'_int.abs'_big'_int"
734     and (Scala) "_.abs"
735     and (Eval) "abs"
737 code_identifier
738   code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
741 subsection \<open>Type of target language naturals\<close>
743 typedef natural = "UNIV :: nat set"
744   morphisms nat_of_natural natural_of_nat ..
746 setup_lifting type_definition_natural
748 lemma natural_eq_iff [termination_simp]:
749   "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"
750   by transfer rule
752 lemma natural_eqI:
753   "nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n"
754   using natural_eq_iff [of m n] by simp
756 lemma nat_of_natural_of_nat_inverse [simp]:
757   "nat_of_natural (natural_of_nat n) = n"
758   by transfer rule
760 lemma natural_of_nat_of_natural_inverse [simp]:
761   "natural_of_nat (nat_of_natural n) = n"
762   by transfer rule
764 instantiation natural :: "{comm_monoid_diff, semiring_1}"
765 begin
767 lift_definition zero_natural :: natural
768   is "0 :: nat"
769   .
771 declare zero_natural.rep_eq [simp]
773 lift_definition one_natural :: natural
774   is "1 :: nat"
775   .
777 declare one_natural.rep_eq [simp]
779 lift_definition plus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
780   is "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"
781   .
783 declare plus_natural.rep_eq [simp]
785 lift_definition minus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
786   is "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"
787   .
789 declare minus_natural.rep_eq [simp]
791 lift_definition times_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
792   is "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
793   .
795 declare times_natural.rep_eq [simp]
797 instance proof
798 qed (transfer, simp add: algebra_simps)+
800 end
802 instance natural :: Rings.dvd ..
804 lemma [transfer_rule]:
805   "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd"
806   unfolding dvd_def by transfer_prover
808 lemma [transfer_rule]:
809   "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
810 proof -
811   have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
812     by (unfold of_nat_def [abs_def]) transfer_prover
813   then show ?thesis by (simp add: id_def)
814 qed
816 lemma [transfer_rule]:
817   "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
818 proof -
819   have "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
820     by transfer_prover
821   then show ?thesis by simp
822 qed
824 lemma nat_of_natural_of_nat [simp]:
825   "nat_of_natural (of_nat n) = n"
826   by transfer rule
828 lemma natural_of_nat_of_nat [simp, code_abbrev]:
829   "natural_of_nat = of_nat"
830   by transfer rule
832 lemma of_nat_of_natural [simp]:
833   "of_nat (nat_of_natural n) = n"
834   by transfer rule
836 lemma nat_of_natural_numeral [simp]:
837   "nat_of_natural (numeral k) = numeral k"
838   by transfer rule
840 instantiation natural :: "{linordered_semiring, equal}"
841 begin
843 lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
844   is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
845   .
847 declare less_eq_natural.rep_eq [termination_simp]
849 lift_definition less_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
850   is "less :: nat \<Rightarrow> nat \<Rightarrow> bool"
851   .
853 declare less_natural.rep_eq [termination_simp]
855 lift_definition equal_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
856   is "HOL.equal :: nat \<Rightarrow> nat \<Rightarrow> bool"
857   .
859 instance proof
860 qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+
862 end
864 lemma [transfer_rule]:
865   "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
866   by (unfold min_def [abs_def]) transfer_prover
868 lemma [transfer_rule]:
869   "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
870   by (unfold max_def [abs_def]) transfer_prover
872 lemma nat_of_natural_min [simp]:
873   "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
874   by transfer rule
876 lemma nat_of_natural_max [simp]:
877   "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
878   by transfer rule
880 instantiation natural :: unique_euclidean_semiring
881 begin
883 lift_definition normalize_natural :: "natural \<Rightarrow> natural"
884   is "normalize :: nat \<Rightarrow> nat"
885   .
887 declare normalize_natural.rep_eq [simp]
889 lift_definition unit_factor_natural :: "natural \<Rightarrow> natural"
890   is "unit_factor :: nat \<Rightarrow> nat"
891   .
893 declare unit_factor_natural.rep_eq [simp]
895 lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
896   is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
897   .
899 declare divide_natural.rep_eq [simp]
901 lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
902   is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
903   .
905 declare modulo_natural.rep_eq [simp]
907 lift_definition euclidean_size_natural :: "natural \<Rightarrow> nat"
908   is "euclidean_size :: nat \<Rightarrow> nat"
909   .
911 declare euclidean_size_natural.rep_eq [simp]
913 lift_definition uniqueness_constraint_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
914   is "uniqueness_constraint :: nat \<Rightarrow> nat \<Rightarrow> bool"
915   .
917 declare uniqueness_constraint_natural.rep_eq [simp]
919 instance
920   by (standard; transfer)
921     (auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)
923 end
925 lemma [code]:
926   "euclidean_size = nat_of_natural"
929 lemma [code]:
930   "uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
933 instance natural :: semiring_parity
934   by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
936 lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
937   is "nat :: int \<Rightarrow> nat"
938   .
940 lift_definition integer_of_natural :: "natural \<Rightarrow> integer"
941   is "of_nat :: nat \<Rightarrow> int"
942   .
944 lemma natural_of_integer_of_natural [simp]:
945   "natural_of_integer (integer_of_natural n) = n"
946   by transfer simp
948 lemma integer_of_natural_of_integer [simp]:
949   "integer_of_natural (natural_of_integer k) = max 0 k"
950   by transfer auto
952 lemma int_of_integer_of_natural [simp]:
953   "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)"
954   by transfer rule
956 lemma integer_of_natural_of_nat [simp]:
957   "integer_of_natural (of_nat n) = of_nat n"
958   by transfer rule
960 lemma [measure_function]:
961   "is_measure nat_of_natural"
962   by (rule is_measure_trivial)
965 subsection \<open>Inductive representation of target language naturals\<close>
967 lift_definition Suc :: "natural \<Rightarrow> natural"
968   is Nat.Suc
969   .
971 declare Suc.rep_eq [simp]
973 old_rep_datatype "0::natural" Suc
974   by (transfer, fact nat.induct nat.inject nat.distinct)+
976 lemma natural_cases [case_names nat, cases type: natural]:
977   fixes m :: natural
978   assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
979   shows P
980   using assms by transfer blast
982 lemma [simp, code]: "size_natural = nat_of_natural"
983 proof (rule ext)
984   fix n
985   show "size_natural n = nat_of_natural n"
986     by (induct n) simp_all
987 qed
989 lemma [simp, code]: "size = nat_of_natural"
990 proof (rule ext)
991   fix n
992   show "size n = nat_of_natural n"
993     by (induct n) simp_all
994 qed
996 lemma natural_decr [termination_simp]:
997   "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
998   by transfer simp
1000 lemma natural_zero_minus_one: "(0::natural) - 1 = 0"
1001   by (rule zero_diff)
1003 lemma Suc_natural_minus_one: "Suc n - 1 = n"
1004   by transfer simp
1006 hide_const (open) Suc
1009 subsection \<open>Code refinement for target language naturals\<close>
1011 lift_definition Nat :: "integer \<Rightarrow> natural"
1012   is nat
1013   .
1015 lemma [code_post]:
1016   "Nat 0 = 0"
1017   "Nat 1 = 1"
1018   "Nat (numeral k) = numeral k"
1019   by (transfer, simp)+
1021 lemma [code abstype]:
1022   "Nat (integer_of_natural n) = n"
1023   by transfer simp
1025 lemma [code]:
1026   "natural_of_nat n = natural_of_integer (integer_of_nat n)"
1027   by transfer simp
1029 lemma [code abstract]:
1030   "integer_of_natural (natural_of_integer k) = max 0 k"
1031   by simp
1033 lemma [code_abbrev]:
1034   "natural_of_integer (Code_Numeral.Pos k) = numeral k"
1035   by transfer simp
1037 lemma [code abstract]:
1038   "integer_of_natural 0 = 0"
1039   by transfer simp
1041 lemma [code abstract]:
1042   "integer_of_natural 1 = 1"
1043   by transfer simp
1045 lemma [code abstract]:
1046   "integer_of_natural (Code_Numeral.Suc n) = integer_of_natural n + 1"
1047   by transfer simp
1049 lemma [code]:
1050   "nat_of_natural = nat_of_integer \<circ> integer_of_natural"
1051   by transfer (simp add: fun_eq_iff)
1053 lemma [code, code_unfold]:
1054   "case_natural f g n = (if n = 0 then f else g (n - 1))"
1055   by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
1057 declare natural.rec [code del]
1059 lemma [code abstract]:
1060   "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"
1061   by transfer simp
1063 lemma [code abstract]:
1064   "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)"
1065   by transfer simp
1067 lemma [code abstract]:
1068   "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
1069   by transfer simp
1071 lemma [code]:
1072   "normalize n = n" for n :: natural
1073   by transfer simp
1075 lemma [code]:
1076   "unit_factor n = of_bool (n \<noteq> 0)" for n :: natural
1077 proof (cases "n = 0")
1078   case True
1079   then show ?thesis
1080     by simp
1081 next
1082   case False
1083   then have "unit_factor n = 1"
1084   proof transfer
1085     fix n :: nat
1086     assume "n \<noteq> 0"
1087     then obtain m where "n = Suc m"
1088       by (cases n) auto
1089     then show "unit_factor n = 1"
1090       by simp
1091   qed
1092   with False show ?thesis
1093     by simp
1094 qed
1096 lemma [code abstract]:
1097   "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
1098   by transfer (simp add: zdiv_int)
1100 lemma [code abstract]:
1101   "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n"
1102   by transfer (simp add: zmod_int)
1104 lemma [code]:
1105   "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
1106   by transfer (simp add: equal)
1108 lemma [code nbe]: "HOL.equal n (n::natural) \<longleftrightarrow> True"
1109   by (rule equal_class.equal_refl)
1111 lemma [code]: "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
1112   by transfer simp
1114 lemma [code]: "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
1115   by transfer simp
1117 hide_const (open) Nat
1119 lifting_update integer.lifting
1120 lifting_forget integer.lifting
1122 lifting_update natural.lifting
1123 lifting_forget natural.lifting
1125 code_reflect Code_Numeral
1126   datatypes natural
1127   functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural"
1128     "plus :: natural \<Rightarrow> _" "minus :: natural \<Rightarrow> _"
1129     "times :: natural \<Rightarrow> _" "divide :: natural \<Rightarrow> _"
1130     "modulo :: natural \<Rightarrow> _"
1131     integer_of_natural natural_of_integer
1133 end