src/HOL/Decision_Procs/Approximation_Bounds.thy
changeset 66280 0c5eb47e2696
parent 65582 a1bc1b020cf2
child 66453 cc19f7ca2ed6
equal deleted inserted replaced
66279:2dba15d3c402 66280:0c5eb47e2696
   337         have "?E mod 2 \<le> 0" using False by auto
   337         have "?E mod 2 \<le> 0" using False by auto
   338         from xt1(5)[OF \<open>0 \<le> ?E mod 2\<close> this]
   338         from xt1(5)[OF \<open>0 \<le> ?E mod 2\<close> this]
   339         show ?thesis by auto
   339         show ?thesis by auto
   340       qed
   340       qed
   341       hence "sqrt (2 powr (?E mod 2)) < sqrt (2 * 2)"
   341       hence "sqrt (2 powr (?E mod 2)) < sqrt (2 * 2)"
   342         by (auto simp del: real_sqrt_four)
   342         by (intro real_sqrt_less_mono) auto
   343       hence E_mod_pow: "sqrt (2 powr (?E mod 2)) < 2" by auto
   343       hence E_mod_pow: "sqrt (2 powr (?E mod 2)) < 2" by auto
   344 
   344 
   345       have E_eq: "2 powr ?E = 2 powr (?E div 2 + ?E div 2 + ?E mod 2)"
   345       have E_eq: "2 powr ?E = 2 powr (?E div 2 + ?E div 2 + ?E mod 2)"
   346         by auto
   346         by auto
   347       have "sqrt (2 powr ?E) = sqrt (2 powr (?E div 2) * 2 powr (?E div 2) * 2 powr (?E mod 2))"
   347       have "sqrt (2 powr ?E) = sqrt (2 powr (?E div 2) * 2 powr (?E div 2) * 2 powr (?E mod 2))"