equal
deleted
inserted
replaced
101 in if j = 0 then l' else l' + 1)" |
101 in if j = 0 then l' else l' + 1)" |
102 proof - |
102 proof - |
103 from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp |
103 from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp |
104 show ?thesis |
104 show ?thesis |
105 by (simp add: Let_def divmod_int_mod_div of_int_add [symmetric]) |
105 by (simp add: Let_def divmod_int_mod_div of_int_add [symmetric]) |
106 (simp add: * mult_commute) |
106 (simp add: * mult.commute) |
107 qed |
107 qed |
108 |
108 |
109 declare of_int_code_if [code] |
109 declare of_int_code_if [code] |
110 |
110 |
111 lemma [code]: |
111 lemma [code]: |