--- a/src/HOL/Library/Code_Target_Nat.thy Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Library/Code_Target_Nat.thy Sun Aug 21 06:18:23 2022 +0000
@@ -98,13 +98,13 @@
begin
lemma divmod_nat_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
- "Divides.divmod_nat m n = (
+ "Euclidean_Division.divmod_nat m n = (
let k = integer_of_nat m; l = integer_of_nat n
in map_prod nat_of_integer nat_of_integer
(if k = 0 then (0, 0)
else if l = 0 then (0, k) else
Code_Numeral.divmod_abs k l))"
- by (simp add: prod_eq_iff Let_def; transfer)
+ by (simp add: prod_eq_iff Let_def Euclidean_Division.divmod_nat_def; transfer)
(simp add: nat_div_distrib nat_mod_distrib)
end
@@ -136,15 +136,12 @@
lemma (in semiring_1) of_nat_code_if:
"of_nat n = (if n = 0 then 0
else let
- (m, q) = Divides.divmod_nat n 2;
+ (m, q) = Euclidean_Division.divmod_nat n 2;
m' = 2 * of_nat m
in if q = 0 then m' else m' + 1)"
-proof -
- from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
- show ?thesis
- by (simp add: Let_def divmod_nat_def of_nat_add [symmetric])
- (simp add: * mult.commute of_nat_mult add.commute)
-qed
+ by (cases n)
+ (simp_all add: Let_def Euclidean_Division.divmod_nat_def ac_simps
+ flip: of_nat_numeral of_nat_mult minus_mod_eq_mult_div)
declare of_nat_code_if [code]