equal
deleted
inserted
replaced
113 else let |
113 else let |
114 l = 2 * of_int (k div 2); |
114 l = 2 * of_int (k div 2); |
115 j = k mod 2 |
115 j = k mod 2 |
116 in if j = 0 then l else l + 1)" |
116 in if j = 0 then l else l + 1)" |
117 proof - |
117 proof - |
118 from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp |
118 from div_mult_mod_eq have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp |
119 show ?thesis |
119 show ?thesis |
120 by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute) |
120 by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute) |
121 qed |
121 qed |
122 |
122 |
123 declare of_int_code_if [code] |
123 declare of_int_code_if [code] |