tuned proofs -- eliminated prems;
authorwenzelm
Thu Mar 03 21:43:06 2011 +0100 (2011-03-03)
changeset 41891d37babdf5cae
parent 41890 550a8ecffe0c
child 41892 2386fb64feaf
tuned proofs -- eliminated prems;
src/HOL/Decision_Procs/MIR.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/L2_Norm.thy
     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> {}"