author | wenzelm |

Thu Mar 03 21:43:06 2011 +0100 (2011-03-03) | |

changeset 41891 | d37babdf5cae |

parent 41890 | 550a8ecffe0c |

child 41892 | 2386fb64feaf |

tuned proofs -- eliminated prems;

1.1 --- a/src/HOL/Decision_Procs/MIR.thy Thu Mar 03 18:43:15 2011 +0100 1.2 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Mar 03 21:43:06 2011 +0100 1.3 @@ -1480,7 +1480,7 @@ 1.4 let ?at = "snd (zsplit0 t)" 1.5 have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using 5 1.6 by (simp add: Let_def split_def) 1.7 - from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 1.8 + from abj 5 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 1.9 from th2[simplified] th[simplified] show ?case by simp 1.10 next 1.11 case (6 s t n a) 1.12 @@ -1490,12 +1490,12 @@ 1.13 let ?at = "snd (zsplit0 t)" 1.14 have abjs: "zsplit0 s = (?ns,?as)" by simp 1.15 moreover have abjt: "zsplit0 t = (?nt,?at)" by simp 1.16 - ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using prems 1.17 + ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using 6 1.18 by (simp add: Let_def split_def) 1.19 from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast 1.20 - from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \<and> numbound0 xb)" by blast (*FIXME*) 1.21 + from 6 have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \<and> numbound0 xb)" by blast (*FIXME*) 1.22 with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 1.23 - from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast 1.24 + from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast 1.25 from th3[simplified] th2[simplified] th[simplified] show ?case 1.26 by (simp add: left_distrib) 1.27 next 1.28 @@ -1506,31 +1506,31 @@ 1.29 let ?at = "snd (zsplit0 t)" 1.30 have abjs: "zsplit0 s = (?ns,?as)" by simp 1.31 moreover have abjt: "zsplit0 t = (?nt,?at)" by simp 1.32 - ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using prems 1.33 + ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using 7 1.34 by (simp add: Let_def split_def) 1.35 from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast 1.36 - from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \<and> numbound0 xb)" by blast (*FIXME*) 1.37 + from 7 have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \<and> numbound0 xb)" by blast (*FIXME*) 1.38 with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 1.39 - from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast 1.40 + from abjs 7 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast 1.41 from th3[simplified] th2[simplified] th[simplified] show ?case 1.42 by (simp add: left_diff_distrib) 1.43 next 1.44 case (8 i t n a) 1.45 let ?nt = "fst (zsplit0 t)" 1.46 let ?at = "snd (zsplit0 t)" 1.47 - have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using prems 1.48 + have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using 8 1.49 by (simp add: Let_def split_def) 1.50 - from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 1.51 - hence " ?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp 1.52 + from abj 8 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 1.53 + hence "?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp 1.54 also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib) 1.55 finally show ?case using th th2 by simp 1.56 next 1.57 case (9 t n a) 1.58 let ?nt = "fst (zsplit0 t)" 1.59 let ?at = "snd (zsplit0 t)" 1.60 - have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a= Floor ?at \<and> n=?nt" using prems 1.61 + have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a= Floor ?at \<and> n=?nt" using 9 1.62 by (simp add: Let_def split_def) 1.63 - from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 1.64 + from abj 9 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 1.65 hence na: "?N a" using th by simp 1.66 have th': "(real ?nt)*(real x) = real (?nt * x)" by simp 1.67 have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp 1.68 @@ -1864,8 +1864,8 @@ 1.69 let ?N = "\<lambda> t. Inum (real i#bs) t" 1.70 have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0 \<and> ?c\<noteq>0) \<or> (j\<noteq> 0 \<and> ?c<0 \<and> ?c\<noteq>0)" by arith 1.71 moreover 1.72 - {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 1.73 - hence ?case using prems by (simp del: zlfm.simps add: rdvd_left_0_eq)} 1.74 + { assume j: "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 1.75 + hence ?case using 11 j by (simp del: zlfm.simps add: rdvd_left_0_eq)} 1.76 moreover 1.77 {assume "?c=0" and "j\<noteq>0" hence ?case 1.78 using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"] 1.79 @@ -1910,8 +1910,8 @@ 1.80 let ?N = "\<lambda> t. Inum (real i#bs) t" 1.81 have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0 \<and> ?c\<noteq>0) \<or> (j\<noteq> 0 \<and> ?c<0 \<and> ?c\<noteq>0)" by arith 1.82 moreover 1.83 - {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 1.84 - hence ?case using prems by (simp del: zlfm.simps add: rdvd_left_0_eq)} 1.85 + {assume j: "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 1.86 + hence ?case using 12 j by (simp del: zlfm.simps add: rdvd_left_0_eq)} 1.87 moreover 1.88 {assume "?c=0" and "j\<noteq>0" hence ?case 1.89 using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"] 1.90 @@ -2012,20 +2012,21 @@ 1.91 proof (induct p rule: iszlfm.induct) 1.92 case (1 p q) 1.93 let ?d = "\<delta> (And p q)" 1.94 - from prems lcm_pos_int have dp: "?d >0" by simp 1.95 - have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp 1.96 - hence th: "d\<delta> p ?d" 1.97 - using delta_mono prems by(simp only: iszlfm.simps) blast 1.98 - have "\<delta> q dvd \<delta> (And p q)" using prems by simp 1.99 - hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast 1.100 + from 1 lcm_pos_int have dp: "?d >0" by simp 1.101 + have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp 1.102 + hence th: "d\<delta> p ?d" 1.103 + using delta_mono 1 by (simp only: iszlfm.simps) blast 1.104 + have "\<delta> q dvd \<delta> (And p q)" using 1 by simp 1.105 + hence th': "d\<delta> q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast 1.106 from th th' dp show ?case by simp 1.107 next 1.108 case (2 p q) 1.109 let ?d = "\<delta> (And p q)" 1.110 - from prems lcm_pos_int have dp: "?d >0" by simp 1.111 - have "\<delta> p dvd \<delta> (And p q)" using prems by simp hence th: "d\<delta> p ?d" using delta_mono prems 1.112 - by(simp only: iszlfm.simps) blast 1.113 - have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast 1.114 + from 2 lcm_pos_int have dp: "?d >0" by simp 1.115 + have "\<delta> p dvd \<delta> (And p q)" using 2 by simp 1.116 + hence th: "d\<delta> p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast 1.117 + have "\<delta> q dvd \<delta> (And p q)" using 2 by simp 1.118 + hence th': "d\<delta> q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast 1.119 from th th' dp show ?case by simp 1.120 qed simp_all 1.121 1.122 @@ -2037,25 +2038,27 @@ 1.123 using linp 1.124 proof (induct p rule: minusinf.induct) 1.125 case (1 f g) 1.126 - from prems have "?P f" by simp 1.127 + then have "?P f" by simp 1.128 then obtain z1 where z1_def: "\<forall> x < z1. ?I x (?M f) = ?I x f" by blast 1.129 - from prems have "?P g" by simp 1.130 + with 1 have "?P g" by simp 1.131 then obtain z2 where z2_def: "\<forall> x < z2. ?I x (?M g) = ?I x g" by blast 1.132 let ?z = "min z1 z2" 1.133 from z1_def z2_def have "\<forall> x < ?z. ?I x (?M (And f g)) = ?I x (And f g)" by simp 1.134 thus ?case by blast 1.135 next 1.136 - case (2 f g) from prems have "?P f" by simp 1.137 + case (2 f g) 1.138 + then have "?P f" by simp 1.139 then obtain z1 where z1_def: "\<forall> x < z1. ?I x (?M f) = ?I x f" by blast 1.140 - from prems have "?P g" by simp 1.141 + with 2 have "?P g" by simp 1.142 then obtain z2 where z2_def: "\<forall> x < z2. ?I x (?M g) = ?I x g" by blast 1.143 let ?z = "min z1 z2" 1.144 from z1_def z2_def have "\<forall> x < ?z. ?I x (?M (Or f g)) = ?I x (Or f g)" by simp 1.145 thus ?case by blast 1.146 next 1.147 case (3 c e) 1.148 - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.149 - from prems have nbe: "numbound0 e" by simp 1.150 + then have "c > 0" by simp 1.151 + hence rcpos: "real c > 0" by simp 1.152 + from 3 have nbe: "numbound0 e" by simp 1.153 fix y 1.154 have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Eq (CN 0 c e))) = ?I x (Eq (CN 0 c e))" 1.155 proof (simp add: less_floor_eq , rule allI, rule impI) 1.156 @@ -2071,8 +2074,8 @@ 1.157 thus ?case by blast 1.158 next 1.159 case (4 c e) 1.160 - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.161 - from prems have nbe: "numbound0 e" by simp 1.162 + then have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.163 + from 4 have nbe: "numbound0 e" by simp 1.164 fix y 1.165 have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (NEq (CN 0 c e))) = ?I x (NEq (CN 0 c e))" 1.166 proof (simp add: less_floor_eq , rule allI, rule impI) 1.167 @@ -2088,8 +2091,8 @@ 1.168 thus ?case by blast 1.169 next 1.170 case (5 c e) 1.171 - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.172 - from prems have nbe: "numbound0 e" by simp 1.173 + then have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.174 + from 5 have nbe: "numbound0 e" by simp 1.175 fix y 1.176 have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Lt (CN 0 c e))) = ?I x (Lt (CN 0 c e))" 1.177 proof (simp add: less_floor_eq , rule allI, rule impI) 1.178 @@ -2104,8 +2107,8 @@ 1.179 thus ?case by blast 1.180 next 1.181 case (6 c e) 1.182 - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.183 - from prems have nbe: "numbound0 e" by simp 1.184 + then have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.185 + from 6 have nbe: "numbound0 e" by simp 1.186 fix y 1.187 have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Le (CN 0 c e))) = ?I x (Le (CN 0 c e))" 1.188 proof (simp add: less_floor_eq , rule allI, rule impI) 1.189 @@ -2120,8 +2123,8 @@ 1.190 thus ?case by blast 1.191 next 1.192 case (7 c e) 1.193 - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.194 - from prems have nbe: "numbound0 e" by simp 1.195 + then have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.196 + from 7 have nbe: "numbound0 e" by simp 1.197 fix y 1.198 have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Gt (CN 0 c e))) = ?I x (Gt (CN 0 c e))" 1.199 proof (simp add: less_floor_eq , rule allI, rule impI) 1.200 @@ -2136,8 +2139,8 @@ 1.201 thus ?case by blast 1.202 next 1.203 case (8 c e) 1.204 - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.205 - from prems have nbe: "numbound0 e" by simp 1.206 + then have "c > 0" by simp hence rcpos: "real c > 0" by simp 1.207 + from 8 have nbe: "numbound0 e" by simp 1.208 fix y 1.209 have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Ge (CN 0 c e))) = ?I x (Ge (CN 0 c e))" 1.210 proof (simp add: less_floor_eq , rule allI, rule impI) 1.211 @@ -2336,15 +2339,15 @@ 1.212 have th: "(real j rdvd real c * real x - Inum (real x # bs) e) = 1.213 (real j rdvd - (real c * real x - Inum (real x # bs) e))" 1.214 by (simp only: rdvd_minus[symmetric]) 1.215 - from prems th show ?case 1.216 + from 9 th show ?case 1.217 by (simp add: algebra_simps 1.218 numbound0_I[where bs="bs" and b'="real x" and b="- real x"]) 1.219 next 1.220 - case (10 j c e) 1.221 + case (10 j c e) 1.222 have th: "(real j rdvd real c * real x - Inum (real x # bs) e) = 1.223 (real j rdvd - (real c * real x - Inum (real x # bs) e))" 1.224 by (simp only: rdvd_minus[symmetric]) 1.225 - from prems th show ?case 1.226 + from 10 th show ?case 1.227 by (simp add: algebra_simps 1.228 numbound0_I[where bs="bs" and b'="real x" and b="- real x"]) 1.229 qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"]) 1.230 @@ -2396,16 +2399,16 @@ 1.231 using linp 1.232 proof(induct p rule: iszlfm.induct) 1.233 case (1 p q) 1.234 - from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp 1.235 - from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp 1.236 - from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 1.237 + then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp 1.238 + from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp 1.239 + from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 1.240 d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 1.241 dl1 dl2 show ?case by (auto simp add: lcm_pos_int) 1.242 next 1.243 case (2 p q) 1.244 - from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp 1.245 - from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp 1.246 - from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 1.247 + then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp 1.248 + from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp 1.249 + from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 1.250 d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 1.251 dl1 dl2 show ?case by (auto simp add: lcm_pos_int) 1.252 qed (auto simp add: lcm_pos_int) 1.253 @@ -2577,19 +2580,20 @@ 1.254 shows "?P (x - d)" 1.255 using lp u d dp nob p 1.256 proof(induct p rule: iszlfm.induct) 1.257 - case (5 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+ 1.258 - with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] prems 1.259 - show ?case by (simp del: real_of_int_minus) 1.260 + case (5 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp_all 1.261 + with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] 5 1.262 + show ?case by (simp del: real_of_int_minus) 1.263 next 1.264 - case (6 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+ 1.265 - with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] prems 1.266 - show ?case by (simp del: real_of_int_minus) 1.267 + case (6 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp_all 1.268 + with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] 6 1.269 + show ?case by (simp del: real_of_int_minus) 1.270 next 1.271 - case (7 c e) hence p: "Ifm (real x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" and ie1:"isint e (a#bs)" using dvd1_eq1[where x="c"] by simp+ 1.272 - let ?e = "Inum (real x # bs) e" 1.273 - from ie1 have ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="a#bs"] 1.274 + case (7 c e) hence p: "Ifm (real x #bs) (Gt (CN 0 c e))" and c1: "c=1" 1.275 + and bn:"numbound0 e" and ie1:"isint e (a#bs)" using dvd1_eq1[where x="c"] by simp_all 1.276 + let ?e = "Inum (real x # bs) e" 1.277 + from ie1 have ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="a#bs"] 1.278 numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"] 1.279 - by (simp add: isint_iff) 1.280 + by (simp add: isint_iff) 1.281 {assume "real (x-d) +?e > 0" hence ?case using c1 1.282 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] 1.283 by (simp del: real_of_int_minus)} 1.284 @@ -2597,7 +2601,7 @@ 1.285 {assume H: "\<not> real (x-d) + ?e > 0" 1.286 let ?v="Neg e" 1.287 have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp 1.288 - from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 1.289 + from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 1.290 have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x = - ?e + real j)" by auto 1.291 from H p have "real x + ?e > 0 \<and> real x + ?e \<le> real d" by (simp add: c1) 1.292 hence "real (x + floor ?e) > real (0::int) \<and> real (x + floor ?e) \<le> real d" 1.293 @@ -2623,7 +2627,7 @@ 1.294 {assume H: "\<not> real (x-d) + ?e \<ge> 0" 1.295 let ?v="Sub (C -1) e" 1.296 have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp 1.297 - from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 1.298 + from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 1.299 have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x = - ?e - 1 + real j)" by auto 1.300 from H p have "real x + ?e \<ge> 0 \<and> real x + ?e < real d" by (simp add: c1) 1.301 hence "real (x + floor ?e) \<ge> real (0::int) \<and> real (x + floor ?e) < real d" 1.302 @@ -2643,7 +2647,7 @@ 1.303 let ?e = "Inum (real x # bs) e" 1.304 let ?v="(Sub (C -1) e)" 1.305 have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp 1.306 - from p have "real x= - ?e" by (simp add: c1) with prems(11) show ?case using dp 1.307 + from p have "real x= - ?e" by (simp add: c1) with 3(5) show ?case using dp 1.308 by simp (erule ballE[where x="1"], 1.309 simp_all add:algebra_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"]) 1.310 next 1.311 @@ -2659,47 +2663,49 @@ 1.312 hence "real x = - Inum ((real (x -d)) # bs) e + real d" by simp 1.313 hence "real x = - Inum (a # bs) e + real d" 1.314 by (simp add: numbound0_I[OF bn,where b="real x - real d"and b'="a"and bs="bs"]) 1.315 - with prems(11) have ?case using dp by simp} 1.316 + with 4(5) have ?case using dp by simp} 1.317 ultimately show ?case by blast 1.318 next 1.319 case (9 j c e) hence p: "Ifm (real x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" 1.320 and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+ 1.321 - let ?e = "Inum (real x # bs) e" 1.322 - from prems have "isint e (a #bs)" by simp 1.323 - hence ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="(real x)#bs"] numbound0_I[OF bn,where b="real x" and b'="a" and bs="bs"] 1.324 - by (simp add: isint_iff) 1.325 - from prems have id: "j dvd d" by simp 1.326 - from c1 ie[symmetric] have "?p x = (real j rdvd real (x+ floor ?e))" by simp 1.327 - also have "\<dots> = (j dvd x + floor ?e)" 1.328 - using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp 1.329 - also have "\<dots> = (j dvd x - d + floor ?e)" 1.330 - using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp 1.331 - also have "\<dots> = (real j rdvd real (x - d + floor ?e))" 1.332 - using int_rdvd_real[where i="j" and x="real (x-d + floor ?e)",symmetric, simplified] 1.333 + let ?e = "Inum (real x # bs) e" 1.334 + from 9 have "isint e (a #bs)" by simp 1.335 + hence ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="(real x)#bs"] numbound0_I[OF bn,where b="real x" and b'="a" and bs="bs"] 1.336 + by (simp add: isint_iff) 1.337 + from 9 have id: "j dvd d" by simp 1.338 + from c1 ie[symmetric] have "?p x = (real j rdvd real (x+ floor ?e))" by simp 1.339 + also have "\<dots> = (j dvd x + floor ?e)" 1.340 + using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp 1.341 + also have "\<dots> = (j dvd x - d + floor ?e)" 1.342 + using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp 1.343 + also have "\<dots> = (real j rdvd real (x - d + floor ?e))" 1.344 + using int_rdvd_real[where i="j" and x="real (x-d + floor ?e)",symmetric, simplified] 1.345 ie by simp 1.346 - also have "\<dots> = (real j rdvd real x - real d + ?e)" 1.347 - using ie by simp 1.348 - finally show ?case 1.349 - using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp 1.350 + also have "\<dots> = (real j rdvd real x - real d + ?e)" 1.351 + using ie by simp 1.352 + finally show ?case 1.353 + using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp 1.354 next 1.355 case (10 j c e) hence p: "Ifm (real x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+ 1.356 - let ?e = "Inum (real x # bs) e" 1.357 - from prems have "isint e (a#bs)" by simp 1.358 - hence ie: "real (floor ?e) = ?e" using numbound0_I[OF bn,where b="real x" and b'="a" and bs="bs"] isint_iff[where n="e" and bs="(real x)#bs"] 1.359 - by (simp add: isint_iff) 1.360 - from prems have id: "j dvd d" by simp 1.361 - from c1 ie[symmetric] have "?p x = (\<not> real j rdvd real (x+ floor ?e))" by simp 1.362 - also have "\<dots> = (\<not> j dvd x + floor ?e)" 1.363 - using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp 1.364 - also have "\<dots> = (\<not> j dvd x - d + floor ?e)" 1.365 - using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp 1.366 - also have "\<dots> = (\<not> real j rdvd real (x - d + floor ?e))" 1.367 - using int_rdvd_real[where i="j" and x="real (x-d + floor ?e)",symmetric, simplified] 1.368 + let ?e = "Inum (real x # bs) e" 1.369 + from 10 have "isint e (a#bs)" by simp 1.370 + hence ie: "real (floor ?e) = ?e" using numbound0_I[OF bn,where b="real x" and b'="a" and bs="bs"] isint_iff[where n="e" and bs="(real x)#bs"] 1.371 + by (simp add: isint_iff) 1.372 + from 10 have id: "j dvd d" by simp 1.373 + from c1 ie[symmetric] have "?p x = (\<not> real j rdvd real (x+ floor ?e))" by simp 1.374 + also have "\<dots> = (\<not> j dvd x + floor ?e)" 1.375 + using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp 1.376 + also have "\<dots> = (\<not> j dvd x - d + floor ?e)" 1.377 + using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp 1.378 + also have "\<dots> = (\<not> real j rdvd real (x - d + floor ?e))" 1.379 + using int_rdvd_real[where i="j" and x="real (x-d + floor ?e)",symmetric, simplified] 1.380 ie by simp 1.381 - also have "\<dots> = (\<not> real j rdvd real x - real d + ?e)" 1.382 - using ie by simp 1.383 - finally show ?case using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp 1.384 -qed (auto simp add: numbound0_I[where bs="bs" and b="real (x - d)" and b'="real x"] simp del: real_of_int_diff) 1.385 + also have "\<dots> = (\<not> real j rdvd real x - real d + ?e)" 1.386 + using ie by simp 1.387 + finally show ?case 1.388 + using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp 1.389 +qed (auto simp add: numbound0_I[where bs="bs" and b="real (x - d)" and b'="real x"] 1.390 + simp del: real_of_int_diff) 1.391 1.392 lemma \<beta>': 1.393 assumes lp: "iszlfm p (a #bs)" 1.394 @@ -2834,179 +2840,213 @@ 1.395 using linp kpos tnb 1.396 proof(induct p rule: \<sigma>\<rho>.induct) 1.397 case (3 c e) 1.398 - from prems have cp: "c > 0" and nb: "numbound0 e" by auto 1.399 - {assume kdc: "k dvd c" 1.400 - from kpos have knz: "k\<noteq>0" by simp 1.401 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.402 - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.403 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.404 + from 3 have cp: "c > 0" and nb: "numbound0 e" by auto 1.405 + { assume kdc: "k dvd c" 1.406 + from kpos have knz: "k\<noteq>0" by simp 1.407 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.408 + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.409 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.410 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 1.411 - moreover 1.412 - {assume "\<not> k dvd c" 1.413 - from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 1.414 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.415 - from prems have "?I (real x) (?s (Eq (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k = 0)" 1.416 - using real_of_int_div[OF knz kdt] 1.417 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.418 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 1.419 - also have "\<dots> = (?I ?tk (Eq (CN 0 c e)))" using nonzero_eq_divide_eq[OF knz', where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.420 + moreover 1.421 + { assume *: "\<not> k dvd c" 1.422 + from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 1.423 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" 1.424 + using isint_def by simp 1.425 + from assms * have "?I (real x) (?s (Eq (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k = 0)" 1.426 + using real_of_int_div[OF knz kdt] 1.427 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.428 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.429 + by (simp add: ti algebra_simps) 1.430 + also have "\<dots> = (?I ?tk (Eq (CN 0 c e)))" 1.431 + using nonzero_eq_divide_eq[OF knz', 1.432 + where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 1.433 + real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.434 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.435 by (simp add: ti) 1.436 finally have ?case . } 1.437 ultimately show ?case by blast 1.438 next 1.439 case (4 c e) 1.440 - from prems have cp: "c > 0" and nb: "numbound0 e" by auto 1.441 - {assume kdc: "k dvd c" 1.442 - from kpos have knz: "k\<noteq>0" by simp 1.443 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.444 - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.445 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.446 + then have cp: "c > 0" and nb: "numbound0 e" by auto 1.447 + { assume kdc: "k dvd c" 1.448 + from kpos have knz: "k\<noteq>0" by simp 1.449 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.450 + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.451 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.452 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 1.453 - moreover 1.454 - {assume "\<not> k dvd c" 1.455 - from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 1.456 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.457 - from prems have "?I (real x) (?s (NEq (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<noteq> 0)" 1.458 - using real_of_int_div[OF knz kdt] 1.459 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.460 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 1.461 - also have "\<dots> = (?I ?tk (NEq (CN 0 c e)))" using nonzero_eq_divide_eq[OF knz', where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.462 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.463 - by (simp add: ti) 1.464 - finally have ?case . } 1.465 - ultimately show ?case by blast 1.466 + moreover 1.467 + { assume *: "\<not> k dvd c" 1.468 + from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 1.469 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.470 + from assms * have "?I (real x) (?s (NEq (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<noteq> 0)" 1.471 + using real_of_int_div[OF knz kdt] 1.472 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.473 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.474 + by (simp add: ti algebra_simps) 1.475 + also have "\<dots> = (?I ?tk (NEq (CN 0 c e)))" 1.476 + using nonzero_eq_divide_eq[OF knz', 1.477 + where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 1.478 + real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.479 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.480 + by (simp add: ti) 1.481 + finally have ?case . } 1.482 + ultimately show ?case by blast 1.483 next 1.484 case (5 c e) 1.485 - from prems have cp: "c > 0" and nb: "numbound0 e" by auto 1.486 - {assume kdc: "k dvd c" 1.487 - from kpos have knz: "k\<noteq>0" by simp 1.488 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.489 - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.490 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.491 + then have cp: "c > 0" and nb: "numbound0 e" by auto 1.492 + { assume kdc: "k dvd c" 1.493 + from kpos have knz: "k\<noteq>0" by simp 1.494 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.495 + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.496 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.497 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 1.498 - moreover 1.499 - {assume "\<not> k dvd c" 1.500 - from kpos have knz: "k\<noteq>0" by simp 1.501 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.502 - from prems have "?I (real x) (?s (Lt (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k < 0)" 1.503 - using real_of_int_div[OF knz kdt] 1.504 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.505 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 1.506 - also have "\<dots> = (?I ?tk (Lt (CN 0 c e)))" using pos_less_divide_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.507 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.508 - by (simp add: ti) 1.509 - finally have ?case . } 1.510 - ultimately show ?case by blast 1.511 + moreover 1.512 + { assume *: "\<not> k dvd c" 1.513 + from kpos have knz: "k\<noteq>0" by simp 1.514 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.515 + from assms * have "?I (real x) (?s (Lt (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k < 0)" 1.516 + using real_of_int_div[OF knz kdt] 1.517 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.518 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.519 + by (simp add: ti algebra_simps) 1.520 + also have "\<dots> = (?I ?tk (Lt (CN 0 c e)))" 1.521 + using pos_less_divide_eq[OF kpos, 1.522 + where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 1.523 + real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.524 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.525 + by (simp add: ti) 1.526 + finally have ?case . } 1.527 + ultimately show ?case by blast 1.528 next 1.529 case (6 c e) 1.530 - from prems have cp: "c > 0" and nb: "numbound0 e" by auto 1.531 - {assume kdc: "k dvd c" 1.532 - from kpos have knz: "k\<noteq>0" by simp 1.533 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.534 - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.535 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.536 + then have cp: "c > 0" and nb: "numbound0 e" by auto 1.537 + { assume kdc: "k dvd c" 1.538 + from kpos have knz: "k\<noteq>0" by simp 1.539 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.540 + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.541 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.542 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 1.543 - moreover 1.544 - {assume "\<not> k dvd c" 1.545 - from kpos have knz: "k\<noteq>0" by simp 1.546 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.547 - from prems have "?I (real x) (?s (Le (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<le> 0)" 1.548 - using real_of_int_div[OF knz kdt] 1.549 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.550 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 1.551 - also have "\<dots> = (?I ?tk (Le (CN 0 c e)))" using pos_le_divide_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.552 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.553 - by (simp add: ti) 1.554 - finally have ?case . } 1.555 - ultimately show ?case by blast 1.556 + moreover 1.557 + { assume *: "\<not> k dvd c" 1.558 + from kpos have knz: "k\<noteq>0" by simp 1.559 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.560 + from assms * have "?I (real x) (?s (Le (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<le> 0)" 1.561 + using real_of_int_div[OF knz kdt] 1.562 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.563 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.564 + by (simp add: ti algebra_simps) 1.565 + also have "\<dots> = (?I ?tk (Le (CN 0 c e)))" 1.566 + using pos_le_divide_eq[OF kpos, 1.567 + where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 1.568 + real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.569 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.570 + by (simp add: ti) 1.571 + finally have ?case . } 1.572 + ultimately show ?case by blast 1.573 next 1.574 case (7 c e) 1.575 - from prems have cp: "c > 0" and nb: "numbound0 e" by auto 1.576 - {assume kdc: "k dvd c" 1.577 - from kpos have knz: "k\<noteq>0" by simp 1.578 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.579 - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.580 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.581 + then have cp: "c > 0" and nb: "numbound0 e" by auto 1.582 + { assume kdc: "k dvd c" 1.583 + from kpos have knz: "k\<noteq>0" by simp 1.584 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.585 + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.586 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.587 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 1.588 - moreover 1.589 - {assume "\<not> k dvd c" 1.590 - from kpos have knz: "k\<noteq>0" by simp 1.591 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.592 - from prems have "?I (real x) (?s (Gt (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k > 0)" 1.593 - using real_of_int_div[OF knz kdt] 1.594 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.595 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 1.596 - also have "\<dots> = (?I ?tk (Gt (CN 0 c e)))" using pos_divide_less_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.597 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.598 - by (simp add: ti) 1.599 - finally have ?case . } 1.600 - ultimately show ?case by blast 1.601 + moreover 1.602 + { assume *: "\<not> k dvd c" 1.603 + from kpos have knz: "k\<noteq>0" by simp 1.604 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.605 + from assms * have "?I (real x) (?s (Gt (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k > 0)" 1.606 + using real_of_int_div[OF knz kdt] 1.607 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.608 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.609 + by (simp add: ti algebra_simps) 1.610 + also have "\<dots> = (?I ?tk (Gt (CN 0 c e)))" 1.611 + using pos_divide_less_eq[OF kpos, 1.612 + where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 1.613 + real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.614 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.615 + by (simp add: ti) 1.616 + finally have ?case . } 1.617 + ultimately show ?case by blast 1.618 next 1.619 case (8 c e) 1.620 - from prems have cp: "c > 0" and nb: "numbound0 e" by auto 1.621 - {assume kdc: "k dvd c" 1.622 - from kpos have knz: "k\<noteq>0" by simp 1.623 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.624 - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.625 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.626 + then have cp: "c > 0" and nb: "numbound0 e" by auto 1.627 + { assume kdc: "k dvd c" 1.628 + from kpos have knz: "k\<noteq>0" by simp 1.629 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.630 + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.631 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.632 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 1.633 - moreover 1.634 - {assume "\<not> k dvd c" 1.635 - from kpos have knz: "k\<noteq>0" by simp 1.636 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.637 - from prems have "?I (real x) (?s (Ge (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<ge> 0)" 1.638 - using real_of_int_div[OF knz kdt] 1.639 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.640 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 1.641 - also have "\<dots> = (?I ?tk (Ge (CN 0 c e)))" using pos_divide_le_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.642 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.643 - by (simp add: ti) 1.644 - finally have ?case . } 1.645 - ultimately show ?case by blast 1.646 + moreover 1.647 + { assume *: "\<not> k dvd c" 1.648 + from kpos have knz: "k\<noteq>0" by simp 1.649 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.650 + from assms * have "?I (real x) (?s (Ge (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<ge> 0)" 1.651 + using real_of_int_div[OF knz kdt] 1.652 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.653 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.654 + by (simp add: ti algebra_simps) 1.655 + also have "\<dots> = (?I ?tk (Ge (CN 0 c e)))" 1.656 + using pos_divide_le_eq[OF kpos, 1.657 + where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 1.658 + real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.659 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.660 + by (simp add: ti) 1.661 + finally have ?case . } 1.662 + ultimately show ?case by blast 1.663 next 1.664 - case (9 i c e) from prems have cp: "c > 0" and nb: "numbound0 e" by auto 1.665 - {assume kdc: "k dvd c" 1.666 - from kpos have knz: "k\<noteq>0" by simp 1.667 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.668 - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.669 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.670 + case (9 i c e) 1.671 + then have cp: "c > 0" and nb: "numbound0 e" by auto 1.672 + { assume kdc: "k dvd c" 1.673 + from kpos have knz: "k\<noteq>0" by simp 1.674 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.675 + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.676 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.677 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 1.678 - moreover 1.679 - {assume "\<not> k dvd c" 1.680 - from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 1.681 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.682 - from prems have "?I (real x) (?s (Dvd i (CN 0 c e))) = (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k)" 1.683 - using real_of_int_div[OF knz kdt] 1.684 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.685 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 1.686 - also have "\<dots> = (?I ?tk (Dvd i (CN 0 c e)))" using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.687 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.688 - by (simp add: ti) 1.689 - finally have ?case . } 1.690 - ultimately show ?case by blast 1.691 + moreover 1.692 + { assume *: "\<not> k dvd c" 1.693 + from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 1.694 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.695 + from assms * have "?I (real x) (?s (Dvd i (CN 0 c e))) = (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k)" 1.696 + using real_of_int_div[OF knz kdt] 1.697 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.698 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.699 + by (simp add: ti algebra_simps) 1.700 + also have "\<dots> = (?I ?tk (Dvd i (CN 0 c e)))" 1.701 + using rdvd_mult[OF knz, where n="i"] 1.702 + real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.703 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.704 + by (simp add: ti) 1.705 + finally have ?case . } 1.706 + ultimately show ?case by blast 1.707 next 1.708 - case (10 i c e) from prems have cp: "c > 0" and nb: "numbound0 e" by auto 1.709 - {assume kdc: "k dvd c" 1.710 - from kpos have knz: "k\<noteq>0" by simp 1.711 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.712 - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.713 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.714 + case (10 i c e) 1.715 + then have cp: "c > 0" and nb: "numbound0 e" by auto 1.716 + { assume kdc: "k dvd c" 1.717 + from kpos have knz: "k\<noteq>0" by simp 1.718 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.719 + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 1.720 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.721 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 1.722 - moreover 1.723 - {assume "\<not> k dvd c" 1.724 - from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 1.725 - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.726 - from prems have "?I (real x) (?s (NDvd i (CN 0 c e))) = (\<not> (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k))" 1.727 - using real_of_int_div[OF knz kdt] 1.728 - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.729 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 1.730 - also have "\<dots> = (?I ?tk (NDvd i (CN 0 c e)))" using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.731 - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.732 - by (simp add: ti) 1.733 - finally have ?case . } 1.734 - ultimately show ?case by blast 1.735 -qed (simp_all add: bound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"] numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"]) 1.736 + moreover 1.737 + { assume *: "\<not> k dvd c" 1.738 + from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 1.739 + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 1.740 + from assms * have "?I (real x) (?s (NDvd i (CN 0 c e))) = (\<not> (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k))" 1.741 + using real_of_int_div[OF knz kdt] 1.742 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.743 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.744 + by (simp add: ti algebra_simps) 1.745 + also have "\<dots> = (?I ?tk (NDvd i (CN 0 c e)))" 1.746 + using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt] 1.747 + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 1.748 + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 1.749 + by (simp add: ti) 1.750 + finally have ?case . } 1.751 + ultimately show ?case by blast 1.752 +qed (simp_all add: bound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"] 1.753 + numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"]) 1.754 1.755 1.756 lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t" 1.757 @@ -3054,16 +3094,16 @@ 1.758 ultimately show ?case by blast 1.759 next 1.760 case (5 c e) hence cp: "c > 0" by simp 1.761 - from prems mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 1.762 + from 5 mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 1.763 real_of_int_mult] 1.764 - show ?case using prems dp 1.765 + show ?case using 5 dp 1.766 by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 1.767 algebra_simps) 1.768 next 1.769 - case (6 c e) hence cp: "c > 0" by simp 1.770 - from prems mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 1.771 + case (6 c e) hence cp: "c > 0" by simp 1.772 + from 6 mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 1.773 real_of_int_mult] 1.774 - show ?case using prems dp 1.775 + show ?case using 6 dp 1.776 by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 1.777 algebra_simps) 1.778 next 1.779 @@ -3118,45 +3158,48 @@ 1.780 ultimately show ?case by blast 1.781 next 1.782 case (9 j c e) hence p: "real j rdvd real (c*i) + ?N i e" (is "?p x") and cp: "c > 0" and bn:"numbound0 e" by simp+ 1.783 - let ?e = "Inum (real i # bs) e" 1.784 - from prems have "isint e (real i #bs)" by simp 1.785 - hence ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="(real i)#bs"] numbound0_I[OF bn,where b="real i" and b'="real i" and bs="bs"] 1.786 - by (simp add: isint_iff) 1.787 - from prems have id: "j dvd d" by simp 1.788 - from ie[symmetric] have "?p i = (real j rdvd real (c*i+ floor ?e))" by simp 1.789 - also have "\<dots> = (j dvd c*i + floor ?e)" 1.790 - using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp 1.791 - also have "\<dots> = (j dvd c*i - c*d + floor ?e)" 1.792 - using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp 1.793 - also have "\<dots> = (real j rdvd real (c*i - c*d + floor ?e))" 1.794 - using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified] 1.795 + let ?e = "Inum (real i # bs) e" 1.796 + from 9 have "isint e (real i #bs)" by simp 1.797 + hence ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="(real i)#bs"] numbound0_I[OF bn,where b="real i" and b'="real i" and bs="bs"] 1.798 + by (simp add: isint_iff) 1.799 + from 9 have id: "j dvd d" by simp 1.800 + from ie[symmetric] have "?p i = (real j rdvd real (c*i+ floor ?e))" by simp 1.801 + also have "\<dots> = (j dvd c*i + floor ?e)" 1.802 + using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp 1.803 + also have "\<dots> = (j dvd c*i - c*d + floor ?e)" 1.804 + using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp 1.805 + also have "\<dots> = (real j rdvd real (c*i - c*d + floor ?e))" 1.806 + using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified] 1.807 ie by simp 1.808 - also have "\<dots> = (real j rdvd real (c*(i - d)) + ?e)" 1.809 - using ie by (simp add:algebra_simps) 1.810 - finally show ?case 1.811 - using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p 1.812 - by (simp add: algebra_simps) 1.813 + also have "\<dots> = (real j rdvd real (c*(i - d)) + ?e)" 1.814 + using ie by (simp add:algebra_simps) 1.815 + finally show ?case 1.816 + using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p 1.817 + by (simp add: algebra_simps) 1.818 next 1.819 - case (10 j c e) hence p: "\<not> (real j rdvd real (c*i) + ?N i e)" (is "?p x") and cp: "c > 0" and bn:"numbound0 e" by simp+ 1.820 - let ?e = "Inum (real i # bs) e" 1.821 - from prems have "isint e (real i #bs)" by simp 1.822 - hence ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="(real i)#bs"] numbound0_I[OF bn,where b="real i" and b'="real i" and bs="bs"] 1.823 - by (simp add: isint_iff) 1.824 - from prems have id: "j dvd d" by simp 1.825 - from ie[symmetric] have "?p i = (\<not> (real j rdvd real (c*i+ floor ?e)))" by simp 1.826 - also have "\<dots> = Not (j dvd c*i + floor ?e)" 1.827 - using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp 1.828 - also have "\<dots> = Not (j dvd c*i - c*d + floor ?e)" 1.829 - using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp 1.830 - also have "\<dots> = Not (real j rdvd real (c*i - c*d + floor ?e))" 1.831 - using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified] 1.832 + case (10 j c e) 1.833 + hence p: "\<not> (real j rdvd real (c*i) + ?N i e)" (is "?p x") and cp: "c > 0" and bn:"numbound0 e" 1.834 + by simp+ 1.835 + let ?e = "Inum (real i # bs) e" 1.836 + from 10 have "isint e (real i #bs)" by simp 1.837 + hence ie: "real (floor ?e) = ?e" 1.838 + using isint_iff[where n="e" and bs="(real i)#bs"] numbound0_I[OF bn,where b="real i" and b'="real i" and bs="bs"] 1.839 + by (simp add: isint_iff) 1.840 + from 10 have id: "j dvd d" by simp 1.841 + from ie[symmetric] have "?p i = (\<not> (real j rdvd real (c*i+ floor ?e)))" by simp 1.842 + also have "\<dots> = Not (j dvd c*i + floor ?e)" 1.843 + using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp 1.844 + also have "\<dots> = Not (j dvd c*i - c*d + floor ?e)" 1.845 + using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp 1.846 + also have "\<dots> = Not (real j rdvd real (c*i - c*d + floor ?e))" 1.847 + using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified] 1.848 ie by simp 1.849 - also have "\<dots> = Not (real j rdvd real (c*(i - d)) + ?e)" 1.850 - using ie by (simp add:algebra_simps) 1.851 - finally show ?case 1.852 - using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p 1.853 - by (simp add: algebra_simps) 1.854 -qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"]) 1.855 + also have "\<dots> = Not (real j rdvd real (c*(i - d)) + ?e)" 1.856 + using ie by (simp add:algebra_simps) 1.857 + finally show ?case 1.858 + using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p 1.859 + by (simp add: algebra_simps) 1.860 +qed (auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"]) 1.861 1.862 lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t" 1.863 shows "bound0 (\<sigma> p k t)" 1.864 @@ -3361,10 +3404,10 @@ 1.865 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un 1.866 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast 1.867 show ?case 1.868 - proof(simp only: FS, clarsimp simp del: Ifm.simps Inum.simps, -) 1.869 - fix p n s 1.870 - let ?ths = "(?I p \<longrightarrow> (?N (Floor a) = ?N (CN 0 n s))) \<and> numbound0 s \<and> isrlfm p" 1.871 - assume "(\<exists>ba. (p, 0, ba) \<in> set (rsplit0 a) \<and> n = 0 \<and> s = Floor ba) \<or> 1.872 + proof(simp only: FS, clarsimp simp del: Ifm.simps Inum.simps, -) 1.873 + fix p n s 1.874 + let ?ths = "(?I p \<longrightarrow> (?N (Floor a) = ?N (CN 0 n s))) \<and> numbound0 s \<and> isrlfm p" 1.875 + assume "(\<exists>ba. (p, 0, ba) \<in> set (rsplit0 a) \<and> n = 0 \<and> s = Floor ba) \<or> 1.876 (\<exists>ab ac ba. 1.877 (ab, ac, ba) \<in> set (rsplit0 a) \<and> 1.878 0 < ac \<and> 1.879 @@ -3375,70 +3418,70 @@ 1.880 ac < 0 \<and> 1.881 (\<exists>j. p = fp ab ac ba j \<and> 1.882 n = 0 \<and> s = Add (Floor ba) (C j) \<and> ac \<le> j \<and> j \<le> 0))" 1.883 - moreover 1.884 - {fix s' 1.885 - assume "(p, 0, s') \<in> ?SS a" and "n = 0" and "s = Floor s'" 1.886 - hence ?ths using prems by auto} 1.887 - moreover 1.888 - { fix p' n' s' j 1.889 - assume pns: "(p', n', s') \<in> ?SS a" 1.890 - and np: "0 < n'" 1.891 - and p_def: "p = ?p (p',n',s') j" 1.892 - and n0: "n = 0" 1.893 - and s_def: "s = (Add (Floor s') (C j))" 1.894 - and jp: "0 \<le> j" and jn: "j \<le> n'" 1.895 - from prems pns have H:"(Ifm ((x\<Colon>real) # (bs\<Colon>real list)) p' \<longrightarrow> 1.896 + moreover 1.897 + { fix s' 1.898 + assume "(p, 0, s') \<in> ?SS a" and "n = 0" and "s = Floor s'" 1.899 + hence ?ths using 5(1) by auto } 1.900 + moreover 1.901 + { fix p' n' s' j 1.902 + assume pns: "(p', n', s') \<in> ?SS a" 1.903 + and np: "0 < n'" 1.904 + and p_def: "p = ?p (p',n',s') j" 1.905 + and n0: "n = 0" 1.906 + and s_def: "s = (Add (Floor s') (C j))" 1.907 + and jp: "0 \<le> j" and jn: "j \<le> n'" 1.908 + from 5 pns have H:"(Ifm ((x\<Colon>real) # (bs\<Colon>real list)) p' \<longrightarrow> 1.909 Inum (x # bs) a = Inum (x # bs) (CN 0 n' s')) \<and> 1.910 numbound0 s' \<and> isrlfm p'" by blast 1.911 - hence nb: "numbound0 s'" by simp 1.912 - from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by (simp add: numsub_nb) 1.913 - let ?nxs = "CN 0 n' s'" 1.914 - let ?l = "floor (?N s') + j" 1.915 - from H 1.916 - have "?I (?p (p',n',s') j) \<longrightarrow> 1.917 + hence nb: "numbound0 s'" by simp 1.918 + from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by (simp add: numsub_nb) 1.919 + let ?nxs = "CN 0 n' s'" 1.920 + let ?l = "floor (?N s') + j" 1.921 + from H 1.922 + have "?I (?p (p',n',s') j) \<longrightarrow> 1.923 (((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?N a = ?N ?nxs ))" 1.924 - by (simp add: fp_def np algebra_simps numsub numadd numfloor) 1.925 - also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))" 1.926 - using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp 1.927 - moreover 1.928 - have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp 1.929 - ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" 1.930 - by blast 1.931 - with s_def n0 p_def nb nf have ?ths by auto} 1.932 + by (simp add: fp_def np algebra_simps numsub numadd numfloor) 1.933 + also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))" 1.934 + using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp 1.935 moreover 1.936 - {fix p' n' s' j 1.937 - assume pns: "(p', n', s') \<in> ?SS a" 1.938 - and np: "n' < 0" 1.939 - and p_def: "p = ?p (p',n',s') j" 1.940 - and n0: "n = 0" 1.941 - and s_def: "s = (Add (Floor s') (C j))" 1.942 - and jp: "n' \<le> j" and jn: "j \<le> 0" 1.943 - from prems pns have H:"(Ifm ((x\<Colon>real) # (bs\<Colon>real list)) p' \<longrightarrow> 1.944 + have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp 1.945 + ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" 1.946 + by blast 1.947 + with s_def n0 p_def nb nf have ?ths by auto} 1.948 + moreover 1.949 + { fix p' n' s' j 1.950 + assume pns: "(p', n', s') \<in> ?SS a" 1.951 + and np: "n' < 0" 1.952 + and p_def: "p = ?p (p',n',s') j" 1.953 + and n0: "n = 0" 1.954 + and s_def: "s = (Add (Floor s') (C j))" 1.955 + and jp: "n' \<le> j" and jn: "j \<le> 0" 1.956 + from 5 pns have H:"(Ifm ((x\<Colon>real) # (bs\<Colon>real list)) p' \<longrightarrow> 1.957 Inum (x # bs) a = Inum (x # bs) (CN 0 n' s')) \<and> 1.958 numbound0 s' \<and> isrlfm p'" by blast 1.959 - hence nb: "numbound0 s'" by simp 1.960 - from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by (simp add: numneg_nb) 1.961 - let ?nxs = "CN 0 n' s'" 1.962 - let ?l = "floor (?N s') + j" 1.963 - from H 1.964 - have "?I (?p (p',n',s') j) \<longrightarrow> 1.965 + hence nb: "numbound0 s'" by simp 1.966 + from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by (simp add: numneg_nb) 1.967 + let ?nxs = "CN 0 n' s'" 1.968 + let ?l = "floor (?N s') + j" 1.969 + from H 1.970 + have "?I (?p (p',n',s') j) \<longrightarrow> 1.971 (((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?N a = ?N ?nxs ))" 1.972 - by (simp add: np fp_def algebra_simps numneg numfloor numadd numsub) 1.973 - also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))" 1.974 - using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp 1.975 - moreover 1.976 - have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp 1.977 - ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" 1.978 - by blast 1.979 - with s_def n0 p_def nb nf have ?ths by auto} 1.980 - ultimately show ?ths by auto 1.981 - qed 1.982 + by (simp add: np fp_def algebra_simps numneg numfloor numadd numsub) 1.983 + also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))" 1.984 + using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp 1.985 + moreover 1.986 + have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp 1.987 + ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" 1.988 + by blast 1.989 + with s_def n0 p_def nb nf have ?ths by auto} 1.990 + ultimately show ?ths by auto 1.991 + qed 1.992 next 1.993 case (3 a b) then show ?case 1.994 - apply auto 1.995 - apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all 1.996 - apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all 1.997 - done 1.998 + apply auto 1.999 + apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all 1.1000 + apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all 1.1001 + done 1.1002 qed (auto simp add: Let_def split_def algebra_simps conj_rl) 1.1003 1.1004 lemma real_in_int_intervals: 1.1005 @@ -3452,9 +3495,9 @@ 1.1006 shows "\<exists> (p,n,s) \<in> set (rsplit0 t). Ifm (x#bs) p" (is "\<exists> (p,n,s) \<in> ?SS t. ?I p") 1.1007 proof(induct t rule: rsplit0.induct) 1.1008 case (2 a b) 1.1009 - from prems have "\<exists> (pa,na,sa) \<in> ?SS a. ?I pa" by auto 1.1010 + then have "\<exists> (pa,na,sa) \<in> ?SS a. ?I pa" by auto 1.1011 then obtain "pa" "na" "sa" where pa: "(pa,na,sa)\<in> ?SS a \<and> ?I pa" by blast 1.1012 - from prems have "\<exists> (pb,nb,sb) \<in> ?SS b. ?I pb" by blast 1.1013 + with 2 have "\<exists> (pb,nb,sb) \<in> ?SS b. ?I pb" by blast 1.1014 then obtain "pb" "nb" "sb" where pb: "(pb,nb,sb)\<in> ?SS b \<and> ?I pb" by blast 1.1015 from pa pb have th: "((pa,na,sa),(pb,nb,sb)) \<in> set[(x,y). x\<leftarrow>rsplit0 a, y\<leftarrow>rsplit0 b]" 1.1016 by (auto) 1.1017 @@ -3515,8 +3558,9 @@ 1.1018 have FS: "?SS (Floor a) = 1.1019 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 1.1020 (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un 1.1021 - (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast 1.1022 - from prems have "\<exists> (p,n,s) \<in> ?SS a. ?I p" by auto 1.1023 + (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))" 1.1024 + by blast 1.1025 + from 5 have "\<exists> (p,n,s) \<in> ?SS a. ?I p" by auto 1.1026 then obtain "p" "n" "s" where pns: "(p,n,s) \<in> ?SS a \<and> ?I p" by blast 1.1027 let ?N = "\<lambda> t. Inum (x#bs) t" 1.1028 from rsplit0_cs[rule_format] pns have ans:"(?N a = ?N (CN 0 n s)) \<and> numbound0 s \<and> isrlfm p" 1.1029 @@ -3933,19 +3977,18 @@ 1.1030 have "isatom (simpfm (Lt a))" by (cases "simpnum a", auto simp add: Let_def) 1.1031 with bn bound0at_l have ?case by blast} 1.1032 moreover 1.1033 - {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1034 - { 1.1035 - assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1036 + { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1037 + { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1038 with numgcd_pos[where t="CN 0 c (simpnum e)"] 1.1039 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 1.1040 - from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1041 + from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1042 by (simp add: numgcd_def) 1.1043 - from prems have th': "c\<noteq>0" by auto 1.1044 - from prems have cp: "c \<ge> 0" by simp 1.1045 + from `c > 0` have th': "c\<noteq>0" by auto 1.1046 + from `c > 0` have cp: "c \<ge> 0" by simp 1.1047 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 1.1048 - have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1049 + have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1050 } 1.1051 - with prems have ?case 1.1052 + with Lt a have ?case 1.1053 by (simp add: Let_def reducecoeff_def reducecoeffh_numbound0)} 1.1054 ultimately show ?case by blast 1.1055 next 1.1056 @@ -3953,24 +3996,23 @@ 1.1057 hence "bound0 (Le a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)" 1.1058 by (cases a,simp_all, case_tac "nat", simp_all) 1.1059 moreover 1.1060 - {assume "bound0 (Le a)" hence bn:"bound0 (simpfm (Le a))" 1.1061 + { assume "bound0 (Le a)" hence bn:"bound0 (simpfm (Le a))" 1.1062 using simpfm_bound0 by blast 1.1063 have "isatom (simpfm (Le a))" by (cases "simpnum a", auto simp add: Let_def) 1.1064 with bn bound0at_l have ?case by blast} 1.1065 moreover 1.1066 - {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1067 - { 1.1068 - assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1069 + { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1070 + { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1071 with numgcd_pos[where t="CN 0 c (simpnum e)"] 1.1072 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 1.1073 - from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1074 + from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1075 by (simp add: numgcd_def) 1.1076 - from prems have th': "c\<noteq>0" by auto 1.1077 - from prems have cp: "c \<ge> 0" by simp 1.1078 + from `c > 0` have th': "c\<noteq>0" by auto 1.1079 + from `c > 0` have cp: "c \<ge> 0" by simp 1.1080 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 1.1081 - have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1082 + have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1083 } 1.1084 - with prems have ?case 1.1085 + with Le a have ?case 1.1086 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 1.1087 ultimately show ?case by blast 1.1088 next 1.1089 @@ -3983,19 +4025,18 @@ 1.1090 have "isatom (simpfm (Gt a))" by (cases "simpnum a", auto simp add: Let_def) 1.1091 with bn bound0at_l have ?case by blast} 1.1092 moreover 1.1093 - {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1094 - { 1.1095 - assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1096 + { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1097 + { assume cn1: "numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1098 with numgcd_pos[where t="CN 0 c (simpnum e)"] 1.1099 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 1.1100 - from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1101 + from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1102 by (simp add: numgcd_def) 1.1103 - from prems have th': "c\<noteq>0" by auto 1.1104 - from prems have cp: "c \<ge> 0" by simp 1.1105 + from `c > 0` have th': "c\<noteq>0" by auto 1.1106 + from `c > 0` have cp: "c \<ge> 0" by simp 1.1107 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 1.1108 - have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1109 + have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1110 } 1.1111 - with prems have ?case 1.1112 + with Gt a have ?case 1.1113 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 1.1114 ultimately show ?case by blast 1.1115 next 1.1116 @@ -4003,24 +4044,23 @@ 1.1117 hence "bound0 (Ge a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)" 1.1118 by (cases a,simp_all, case_tac "nat", simp_all) 1.1119 moreover 1.1120 - {assume "bound0 (Ge a)" hence bn:"bound0 (simpfm (Ge a))" 1.1121 + { assume "bound0 (Ge a)" hence bn:"bound0 (simpfm (Ge a))" 1.1122 using simpfm_bound0 by blast 1.1123 have "isatom (simpfm (Ge a))" by (cases "simpnum a", auto simp add: Let_def) 1.1124 with bn bound0at_l have ?case by blast} 1.1125 moreover 1.1126 - {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1127 - { 1.1128 - assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1129 + { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1130 + { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1131 with numgcd_pos[where t="CN 0 c (simpnum e)"] 1.1132 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 1.1133 - from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1134 + from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1135 by (simp add: numgcd_def) 1.1136 - from prems have th': "c\<noteq>0" by auto 1.1137 - from prems have cp: "c \<ge> 0" by simp 1.1138 + from `c > 0` have th': "c\<noteq>0" by auto 1.1139 + from `c > 0` have cp: "c \<ge> 0" by simp 1.1140 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 1.1141 - have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1142 + have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1143 } 1.1144 - with prems have ?case 1.1145 + with Ge a have ?case 1.1146 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 1.1147 ultimately show ?case by blast 1.1148 next 1.1149 @@ -4028,24 +4068,23 @@ 1.1150 hence "bound0 (Eq a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)" 1.1151 by (cases a,simp_all, case_tac "nat", simp_all) 1.1152 moreover 1.1153 - {assume "bound0 (Eq a)" hence bn:"bound0 (simpfm (Eq a))" 1.1154 + { assume "bound0 (Eq a)" hence bn:"bound0 (simpfm (Eq a))" 1.1155 using simpfm_bound0 by blast 1.1156 have "isatom (simpfm (Eq a))" by (cases "simpnum a", auto simp add: Let_def) 1.1157 with bn bound0at_l have ?case by blast} 1.1158 moreover 1.1159 - {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1160 - { 1.1161 - assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1162 + { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1163 + { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1164 with numgcd_pos[where t="CN 0 c (simpnum e)"] 1.1165 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 1.1166 - from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1167 + from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1168 by (simp add: numgcd_def) 1.1169 - from prems have th': "c\<noteq>0" by auto 1.1170 - from prems have cp: "c \<ge> 0" by simp 1.1171 + from `c > 0` have th': "c\<noteq>0" by auto 1.1172 + from `c > 0` have cp: "c \<ge> 0" by simp 1.1173 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 1.1174 - have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1175 + have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1176 } 1.1177 - with prems have ?case 1.1178 + with Eq a have ?case 1.1179 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 1.1180 ultimately show ?case by blast 1.1181 next 1.1182 @@ -4058,19 +4097,18 @@ 1.1183 have "isatom (simpfm (NEq a))" by (cases "simpnum a", auto simp add: Let_def) 1.1184 with bn bound0at_l have ?case by blast} 1.1185 moreover 1.1186 - {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1187 - { 1.1188 - assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1189 + { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e" 1.1190 + { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 1.1191 with numgcd_pos[where t="CN 0 c (simpnum e)"] 1.1192 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 1.1193 - from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1194 + from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 1.1195 by (simp add: numgcd_def) 1.1196 - from prems have th': "c\<noteq>0" by auto 1.1197 - from prems have cp: "c \<ge> 0" by simp 1.1198 + from `c > 0` have th': "c\<noteq>0" by auto 1.1199 + from `c > 0` have cp: "c \<ge> 0" by simp 1.1200 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 1.1201 - have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1202 + have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 1.1203 } 1.1204 - with prems have ?case 1.1205 + with NEq a have ?case 1.1206 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 1.1207 ultimately show ?case by blast 1.1208 next 1.1209 @@ -4111,8 +4149,8 @@ 1.1210 case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto 1.1211 next 1.1212 case (3 c e) 1.1213 - from prems have nb: "numbound0 e" by simp 1.1214 - from prems have cp: "real c > 0" by simp 1.1215 + from 3 have nb: "numbound0 e" by simp 1.1216 + from 3 have cp: "real c > 0" by simp 1.1217 fix a 1.1218 let ?e="Inum (a#bs) e" 1.1219 let ?z = "(- ?e) / real c" 1.1220 @@ -4128,8 +4166,8 @@ 1.1221 thus ?case by blast 1.1222 next 1.1223 case (4 c e) 1.1224 - from prems have nb: "numbound0 e" by simp 1.1225 - from prems have cp: "real c > 0" by simp 1.1226 + from 4 have nb: "numbound0 e" by simp 1.1227 + from 4 have cp: "real c > 0" by simp 1.1228 fix a 1.1229 let ?e="Inum (a#bs) e" 1.1230 let ?z = "(- ?e) / real c" 1.1231 @@ -4145,8 +4183,8 @@ 1.1232 thus ?case by blast 1.1233 next 1.1234 case (5 c e) 1.1235 - from prems have nb: "numbound0 e" by simp 1.1236 - from prems have cp: "real c > 0" by simp 1.1237 + from 5 have nb: "numbound0 e" by simp 1.1238 + from 5 have cp: "real c > 0" by simp 1.1239 fix a 1.1240 let ?e="Inum (a#bs) e" 1.1241 let ?z = "(- ?e) / real c" 1.1242 @@ -4161,8 +4199,8 @@ 1.1243 thus ?case by blast 1.1244 next 1.1245 case (6 c e) 1.1246 - from prems have nb: "numbound0 e" by simp 1.1247 - from prems have cp: "real c > 0" by simp 1.1248 + from 6 have nb: "numbound0 e" by simp 1.1249 + from 6 have cp: "real c > 0" by simp 1.1250 fix a 1.1251 let ?e="Inum (a#bs) e" 1.1252 let ?z = "(- ?e) / real c" 1.1253 @@ -4177,8 +4215,8 @@ 1.1254 thus ?case by blast 1.1255 next 1.1256 case (7 c e) 1.1257 - from prems have nb: "numbound0 e" by simp 1.1258 - from prems have cp: "real c > 0" by simp 1.1259 + from 7 have nb: "numbound0 e" by simp 1.1260 + from 7 have cp: "real c > 0" by simp 1.1261 fix a 1.1262 let ?e="Inum (a#bs) e" 1.1263 let ?z = "(- ?e) / real c" 1.1264 @@ -4193,8 +4231,8 @@ 1.1265 thus ?case by blast 1.1266 next 1.1267 case (8 c e) 1.1268 - from prems have nb: "numbound0 e" by simp 1.1269 - from prems have cp: "real c > 0" by simp 1.1270 + from 8 have nb: "numbound0 e" by simp 1.1271 + from 8 have cp: "real c > 0" by simp 1.1272 fix a 1.1273 let ?e="Inum (a#bs) e" 1.1274 let ?z = "(- ?e) / real c" 1.1275 @@ -4219,8 +4257,8 @@ 1.1276 case (2 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto 1.1277 next 1.1278 case (3 c e) 1.1279 - from prems have nb: "numbound0 e" by simp 1.1280 - from prems have cp: "real c > 0" by simp 1.1281 + from 3 have nb: "numbound0 e" by simp 1.1282 + from 3 have cp: "real c > 0" by simp 1.1283 fix a 1.1284 let ?e="Inum (a#bs) e" 1.1285 let ?z = "(- ?e) / real c" 1.1286 @@ -4236,8 +4274,8 @@ 1.1287 thus ?case by blast 1.1288 next 1.1289 case (4 c e) 1.1290 - from prems have nb: "numbound0 e" by simp 1.1291 - from prems have cp: "real c > 0" by simp 1.1292 + from 4 have nb: "numbound0 e" by simp 1.1293 + from 4 have cp: "real c > 0" by simp 1.1294 fix a 1.1295 let ?e="Inum (a#bs) e" 1.1296 let ?z = "(- ?e) / real c" 1.1297 @@ -4253,8 +4291,8 @@ 1.1298 thus ?case by blast 1.1299 next 1.1300 case (5 c e) 1.1301 - from prems have nb: "numbound0 e" by simp 1.1302 - from prems have cp: "real c > 0" by simp 1.1303 + from 5 have nb: "numbound0 e" by simp 1.1304 + from 5 have cp: "real c > 0" by simp 1.1305 fix a 1.1306 let ?e="Inum (a#bs) e" 1.1307 let ?z = "(- ?e) / real c" 1.1308 @@ -4269,8 +4307,8 @@ 1.1309 thus ?case by blast 1.1310 next 1.1311 case (6 c e) 1.1312 - from prems have nb: "numbound0 e" by simp 1.1313 - from prems have cp: "real c > 0" by simp 1.1314 + from 6 have nb: "numbound0 e" by simp 1.1315 + from 6 have cp: "real c > 0" by simp 1.1316 fix a 1.1317 let ?e="Inum (a#bs) e" 1.1318 let ?z = "(- ?e) / real c" 1.1319 @@ -4285,8 +4323,8 @@ 1.1320 thus ?case by blast 1.1321 next 1.1322 case (7 c e) 1.1323 - from prems have nb: "numbound0 e" by simp 1.1324 - from prems have cp: "real c > 0" by simp 1.1325 + from 7 have nb: "numbound0 e" by simp 1.1326 + from 7 have cp: "real c > 0" by simp 1.1327 fix a 1.1328 let ?e="Inum (a#bs) e" 1.1329 let ?z = "(- ?e) / real c" 1.1330 @@ -4301,8 +4339,8 @@ 1.1331 thus ?case by blast 1.1332 next 1.1333 case (8 c e) 1.1334 - from prems have nb: "numbound0 e" by simp 1.1335 - from prems have cp: "real c > 0" by simp 1.1336 + from 8 have nb: "numbound0 e" by simp 1.1337 + from 8 have cp: "real c > 0" by simp 1.1338 fix a 1.1339 let ?e="Inum (a#bs) e" 1.1340 let ?z = "(- ?e) / real c" 1.1341 @@ -4387,7 +4425,8 @@ 1.1342 shows "(Ifm (x#bs) (\<upsilon> p (t,n)) = Ifm (((Inum (x#bs) t)/(real n))#bs) p) \<and> bound0 (\<upsilon> p (t,n))" (is "(?I x (\<upsilon> p (t,n)) = ?I ?u p) \<and> ?B p" is "(_ = ?I (?t/?n) p) \<and> _" is "(_ = ?I (?N x t /_) p) \<and> _") 1.1343 using lp 1.1344 proof(induct p rule: \<upsilon>.induct) 1.1345 - case (5 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 1.1346 + case (5 c e) 1.1347 + from 5 have cp: "c >0" and nb: "numbound0 e" by simp_all 1.1348 have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)" 1.1349 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 1.1350 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)" 1.1351 @@ -4397,7 +4436,8 @@ 1.1352 using np by simp 1.1353 finally show ?case using nbt nb by (simp add: algebra_simps) 1.1354 next 1.1355 - case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 1.1356 + case (6 c e) 1.1357 + from 6 have cp: "c >0" and nb: "numbound0 e" by simp_all 1.1358 have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)" 1.1359 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 1.1360 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)" 1.1361 @@ -4407,7 +4447,8 @@ 1.1362 using np by simp 1.1363 finally show ?case using nbt nb by (simp add: algebra_simps) 1.1364 next 1.1365 - case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 1.1366 + case (7 c e) 1.1367 + from 7 have cp: "c >0" and nb: "numbound0 e" by simp_all 1.1368 have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)" 1.1369 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 1.1370 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)" 1.1371 @@ -4417,7 +4458,8 @@ 1.1372 using np by simp 1.1373 finally show ?case using nbt nb by (simp add: algebra_simps) 1.1374 next 1.1375 - case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 1.1376 + case (8 c e) 1.1377 + from 8 have cp: "c >0" and nb: "numbound0 e" by simp_all 1.1378 have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)" 1.1379 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 1.1380 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)" 1.1381 @@ -4427,7 +4469,8 @@ 1.1382 using np by simp 1.1383 finally show ?case using nbt nb by (simp add: algebra_simps) 1.1384 next 1.1385 - case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 1.1386 + case (3 c e) 1.1387 + from 3 have cp: "c >0" and nb: "numbound0 e" by simp_all 1.1388 from np have np: "real n \<noteq> 0" by simp 1.1389 have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)" 1.1390 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 1.1391 @@ -4438,7 +4481,8 @@ 1.1392 using np by simp 1.1393 finally show ?case using nbt nb by (simp add: algebra_simps) 1.1394 next 1.1395 - case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 1.1396 + case (4 c e) 1.1397 + from 4 have cp: "c >0" and nb: "numbound0 e" by simp_all 1.1398 from np have np: "real n \<noteq> 0" by simp 1.1399 have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<noteq> 0)" 1.1400 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 1.1401 @@ -4497,100 +4541,100 @@ 1.1402 shows "Ifm (y#bs) p" 1.1403 using lp px noS 1.1404 proof (induct p rule: isrlfm.induct) 1.1405 - case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 1.1406 - from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps) 1.1407 - hence pxc: "x < (- ?N x e) / real c" 1.1408 - by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) 1.1409 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1410 - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 1.1411 - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 1.1412 - moreover {assume y: "y < (-?N x e)/ real c" 1.1413 - hence "y * real c < - ?N x e" 1.1414 - by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 1.1415 - hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 1.1416 - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 1.1417 - moreover {assume y: "y > (- ?N x e) / real c" 1.1418 - with yu have eu: "u > (- ?N x e) / real c" by auto 1.1419 - with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) 1.1420 - with lx pxc have "False" by auto 1.1421 - hence ?case by simp } 1.1422 - ultimately show ?case by blast 1.1423 + case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 1.1424 + from 5 have "x * real c + ?N x e < 0" by (simp add: algebra_simps) 1.1425 + hence pxc: "x < (- ?N x e) / real c" 1.1426 + by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) 1.1427 + from 5 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1428 + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 1.1429 + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 1.1430 + moreover {assume y: "y < (-?N x e)/ real c" 1.1431 + hence "y * real c < - ?N x e" 1.1432 + by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 1.1433 + hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 1.1434 + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 1.1435 + moreover {assume y: "y > (- ?N x e) / real c" 1.1436 + with yu have eu: "u > (- ?N x e) / real c" by auto 1.1437 + with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) 1.1438 + with lx pxc have "False" by auto 1.1439 + hence ?case by simp } 1.1440 + ultimately show ?case by blast 1.1441 next 1.1442 - case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp + 1.1443 - from prems have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps) 1.1444 - hence pxc: "x \<le> (- ?N x e) / real c" 1.1445 - by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) 1.1446 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1447 - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 1.1448 - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 1.1449 - moreover {assume y: "y < (-?N x e)/ real c" 1.1450 - hence "y * real c < - ?N x e" 1.1451 - by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 1.1452 - hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 1.1453 - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 1.1454 - moreover {assume y: "y > (- ?N x e) / real c" 1.1455 - with yu have eu: "u > (- ?N x e) / real c" by auto 1.1456 - with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) 1.1457 - with lx pxc have "False" by auto 1.1458 - hence ?case by simp } 1.1459 - ultimately show ?case by blast 1.1460 + case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 1.1461 + from 6 have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps) 1.1462 + hence pxc: "x \<le> (- ?N x e) / real c" 1.1463 + by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) 1.1464 + from 6 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1465 + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 1.1466 + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 1.1467 + moreover {assume y: "y < (-?N x e)/ real c" 1.1468 + hence "y * real c < - ?N x e" 1.1469 + by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 1.1470 + hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 1.1471 + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 1.1472 + moreover {assume y: "y > (- ?N x e) / real c" 1.1473 + with yu have eu: "u > (- ?N x e) / real c" by auto 1.1474 + with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) 1.1475 + with lx pxc have "False" by auto 1.1476 + hence ?case by simp } 1.1477 + ultimately show ?case by blast 1.1478 next 1.1479 - case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 1.1480 - from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps) 1.1481 - hence pxc: "x > (- ?N x e) / real c" 1.1482 - by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) 1.1483 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1484 - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 1.1485 - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 1.1486 - moreover {assume y: "y > (-?N x e)/ real c" 1.1487 - hence "y * real c > - ?N x e" 1.1488 - by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 1.1489 - hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 1.1490 - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 1.1491 - moreover {assume y: "y < (- ?N x e) / real c" 1.1492 - with ly have eu: "l < (- ?N x e) / real c" by auto 1.1493 - with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) 1.1494 - with xu pxc have "False" by auto 1.1495 - hence ?case by simp } 1.1496 - ultimately show ?case by blast 1.1497 + case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 1.1498 + from 7 have "x * real c + ?N x e > 0" by (simp add: algebra_simps) 1.1499 + hence pxc: "x > (- ?N x e) / real c" 1.1500 + by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) 1.1501 + from 7 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1502 + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 1.1503 + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 1.1504 + moreover {assume y: "y > (-?N x e)/ real c" 1.1505 + hence "y * real c > - ?N x e" 1.1506 + by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 1.1507 + hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 1.1508 + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 1.1509 + moreover {assume y: "y < (- ?N x e) / real c" 1.1510 + with ly have eu: "l < (- ?N x e) / real c" by auto 1.1511 + with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) 1.1512 + with xu pxc have "False" by auto 1.1513 + hence ?case by simp } 1.1514 + ultimately show ?case by blast 1.1515 next 1.1516 - case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 1.1517 - from prems have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps) 1.1518 - hence pxc: "x \<ge> (- ?N x e) / real c" 1.1519 - by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) 1.1520 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1521 - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 1.1522 - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 1.1523 - moreover {assume y: "y > (-?N x e)/ real c" 1.1524 - hence "y * real c > - ?N x e" 1.1525 - by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 1.1526 - hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 1.1527 - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 1.1528 - moreover {assume y: "y < (- ?N x e) / real c" 1.1529 - with ly have eu: "l < (- ?N x e) / real c" by auto 1.1530 - with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) 1.1531 - with xu pxc have "False" by auto 1.1532 - hence ?case by simp } 1.1533 - ultimately show ?case by blast 1.1534 + case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 1.1535 + from 8 have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps) 1.1536 + hence pxc: "x \<ge> (- ?N x e) / real c" 1.1537 + by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) 1.1538 + from 8 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1539 + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 1.1540 + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto 1.1541 + moreover {assume y: "y > (-?N x e)/ real c" 1.1542 + hence "y * real c > - ?N x e" 1.1543 + by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) 1.1544 + hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 1.1545 + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 1.1546 + moreover {assume y: "y < (- ?N x e) / real c" 1.1547 + with ly have eu: "l < (- ?N x e) / real c" by auto 1.1548 + with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) 1.1549 + with xu pxc have "False" by auto 1.1550 + hence ?case by simp } 1.1551 + ultimately show ?case by blast 1.1552 next 1.1553 - case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 1.1554 - from cp have cnz: "real c \<noteq> 0" by simp 1.1555 - from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps) 1.1556 - hence pxc: "x = (- ?N x e) / real c" 1.1557 - by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) 1.1558 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1559 - with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto 1.1560 - with pxc show ?case by simp 1.1561 + case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 1.1562 + from cp have cnz: "real c \<noteq> 0" by simp 1.1563 + from 3 have "x * real c + ?N x e = 0" by (simp add: algebra_simps) 1.1564 + hence pxc: "x = (- ?N x e) / real c" 1.1565 + by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) 1.1566 + from 3 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1567 + with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto 1.1568 + with pxc show ?case by simp 1.1569 next 1.1570 - case (4 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 1.1571 - from cp have cnz: "real c \<noteq> 0" by simp 1.1572 - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1573 - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 1.1574 - hence "y* real c \<noteq> -?N x e" 1.1575 - by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp 1.1576 - hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps) 1.1577 - thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 1.1578 - by (simp add: algebra_simps) 1.1579 + case (4 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 1.1580 + from cp have cnz: "real c \<noteq> 0" by simp 1.1581 + from 4 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto 1.1582 + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto 1.1583 + hence "y* real c \<noteq> -?N x e" 1.1584 + by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp 1.1585 + hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps) 1.1586 + thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 1.1587 + by (simp add: algebra_simps) 1.1588 qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"]) 1.1589 1.1590 lemma rinf_\<Upsilon>: 1.1591 @@ -4598,7 +4642,8 @@ 1.1592 and nmi: "\<not> (Ifm (x#bs) (minusinf p))" (is "\<not> (Ifm (x#bs) (?M p))") 1.1593 and npi: "\<not> (Ifm (x#bs) (plusinf p))" (is "\<not> (Ifm (x#bs) (?P p))") 1.1594 and ex: "\<exists> x. Ifm (x#bs) p" (is "\<exists> x. ?I x p") 1.1595 - shows "\<exists> (l,n) \<in> set (\<Upsilon> p). \<exists> (s,m) \<in> set (\<Upsilon> p). ?I ((Inum (x#bs) l / real n + Inum (x#bs) s / real m) / 2) p" 1.1596 + shows "\<exists> (l,n) \<in> set (\<Upsilon> p). \<exists> (s,m) \<in> set (\<Upsilon> p). 1.1597 + ?I ((Inum (x#bs) l / real n + Inum (x#bs) s / real m) / 2) p" 1.1598 proof- 1.1599 let ?N = "\<lambda> x t. Inum (x#bs) t" 1.1600 let ?U = "set (\<Upsilon> p)" 1.1601 @@ -5602,23 +5647,18 @@ 1.1602 setup "Mir_Tac.setup" 1.1603 1.1604 lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))" 1.1605 -apply mir 1.1606 -done 1.1607 + by mir 1.1608 1.1609 lemma "ALL (x::real). real (2::int)*x - (real (1::int)) < real \<lfloor>x\<rfloor> + real \<lceil>x\<rceil> \<and> real \<lfloor>x\<rfloor> + real \<lceil>x\<rceil> \<le> real (2::int)*x + (real (1::int))" 1.1610 -apply mir 1.1611 -done 1.1612 + by mir 1.1613 1.1614 lemma "ALL (x::real). 2*\<lfloor>x\<rfloor> \<le> \<lfloor>2*x\<rfloor> \<and> \<lfloor>2*x\<rfloor> \<le> 2*\<lfloor>x+1\<rfloor>" 1.1615 -apply mir 1.1616 -done 1.1617 + by mir 1.1618 1.1619 lemma "ALL (x::real). \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)" 1.1620 -apply mir 1.1621 -done 1.1622 + by mir 1.1623 1.1624 lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1" 1.1625 -apply mir 1.1626 -done 1.1627 + by mir 1.1628 1.1629 end

2.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Mar 03 18:43:15 2011 +0100 2.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Mar 03 21:43:06 2011 +0100 2.3 @@ -644,7 +644,7 @@ 2.4 2.5 lemma seq_mono_lemma: assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n" and "\<forall>n \<ge> m. e n <= e m" 2.6 shows "\<forall>n \<ge> m. d n < e m" 2.7 - using prems apply auto 2.8 + using assms apply auto 2.9 apply (erule_tac x="n" in allE) 2.10 apply (erule_tac x="n" in allE) 2.11 apply auto

3.1 --- a/src/HOL/Multivariate_Analysis/L2_Norm.thy Thu Mar 03 18:43:15 2011 +0100 3.2 +++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy Thu Mar 03 21:43:06 2011 +0100 3.3 @@ -44,7 +44,7 @@ 3.4 assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i" 3.5 shows "setL2 f K \<le> setL2 g K" 3.6 unfolding setL2_def 3.7 - by (simp add: setsum_nonneg setsum_mono power_mono prems) 3.8 + by (simp add: setsum_nonneg setsum_mono power_mono assms) 3.9 3.10 lemma setL2_strict_mono: 3.11 assumes "finite K" and "K \<noteq> {}"