equal
deleted
inserted
replaced
1191 ultimately show ?thesis |
1191 ultimately show ?thesis |
1192 using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] \<open>0 \<le> l\<close> \<open>y \<noteq> 0\<close> |
1192 using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] \<open>0 \<le> l\<close> \<open>y \<noteq> 0\<close> |
1193 l_def[symmetric, THEN meta_eq_to_obj_eq] |
1193 l_def[symmetric, THEN meta_eq_to_obj_eq] |
1194 apply transfer |
1194 apply transfer |
1195 apply (auto simp add: round_up_def truncate_up_rat_precision) |
1195 apply (auto simp add: round_up_def truncate_up_rat_precision) |
|
1196 apply (metis dvd_triv_left of_nat_dvd_iff) |
1196 apply (metis floor_divide_of_int_eq of_int_of_nat_eq) |
1197 apply (metis floor_divide_of_int_eq of_int_of_nat_eq) |
1197 done |
1198 done |
1198 next |
1199 next |
1199 case False |
1200 case False |
1200 define y' where "y' = y * 2 ^ nat (- l)" |
1201 define y' where "y' = y * 2 ^ nat (- l)" |
1206 ultimately show ?thesis |
1207 ultimately show ?thesis |
1207 using ceil_divide_floor_conv[of y' x] \<open>\<not> 0 \<le> l\<close> \<open>y' \<noteq> 0\<close> \<open>y \<noteq> 0\<close> |
1208 using ceil_divide_floor_conv[of y' x] \<open>\<not> 0 \<le> l\<close> \<open>y' \<noteq> 0\<close> \<open>y \<noteq> 0\<close> |
1208 l_def[symmetric, THEN meta_eq_to_obj_eq] |
1209 l_def[symmetric, THEN meta_eq_to_obj_eq] |
1209 apply transfer |
1210 apply transfer |
1210 apply (auto simp add: round_up_def ceil_divide_floor_conv truncate_up_rat_precision) |
1211 apply (auto simp add: round_up_def ceil_divide_floor_conv truncate_up_rat_precision) |
|
1212 apply (metis dvd_triv_left of_nat_dvd_iff) |
1211 apply (metis floor_divide_of_int_eq of_int_of_nat_eq) |
1213 apply (metis floor_divide_of_int_eq of_int_of_nat_eq) |
1212 done |
1214 done |
1213 qed |
1215 qed |
1214 qed |
1216 qed |
1215 |
1217 |