src/HOL/Decision_Procs/Approximation_Bounds.thy
 changeset 66280 0c5eb47e2696 parent 65582 a1bc1b020cf2 child 66453 cc19f7ca2ed6
equal 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))"`