src/HOL/Library/Code_Target_Nat.thy
changeset 69946 494934c30f38
parent 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Fri Mar 22 12:34:49 2019 +0000
     1.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Fri Mar 22 19:18:08 2019 +0000
     1.3 @@ -93,14 +93,26 @@
     1.4    "integer_of_nat (m mod n) = of_nat m mod of_nat n"
     1.5    by transfer (simp add: zmod_int)
     1.6  
     1.7 -lemma [code]:
     1.8 -  "Divides.divmod_nat m n = (m div n, m mod n)"
     1.9 -  by (fact divmod_nat_def)
    1.10 +context
    1.11 +  includes integer.lifting
    1.12 +begin
    1.13 +
    1.14 +lemma divmod_nat_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
    1.15 +  "Divides.divmod_nat m n = (
    1.16 +     let k = integer_of_nat m; l = integer_of_nat n
    1.17 +     in map_prod nat_of_integer nat_of_integer
    1.18 +       (if k = 0 then (0, 0)
    1.19 +        else if l = 0 then (0, k) else
    1.20 +          Code_Numeral.divmod_abs k l))"
    1.21 +  by (simp add: prod_eq_iff Let_def; transfer)
    1.22 +    (simp add: nat_div_distrib nat_mod_distrib)
    1.23 +
    1.24 +end
    1.25  
    1.26  lemma [code]:
    1.27    "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
    1.28 -  by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv)
    1.29 -    (transfer, simp_all only: nat_div_distrib nat_mod_distrib
    1.30 +  by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv; transfer)
    1.31 +    (simp_all only: nat_div_distrib nat_mod_distrib
    1.32          zero_le_numeral nat_numeral)
    1.33    
    1.34  lemma [code]: