1478 case (5 t n a) 
1478 case (5 t n a) 
1479 let ?nt = "fst (zsplit0 t)" 
1479 let ?nt = "fst (zsplit0 t)" 
1480 let ?at = "snd (zsplit0 t)" 
1480 let ?at = "snd (zsplit0 t)" 
1481 have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=?nt" using 5 
1481 have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=?nt" using 5 
1482 by (simp add: Let_def split_def) 
1482 by (simp add: Let_def split_def) 
1483 from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 
1483 from abj 5 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 
1484 from th2[simplified] th[simplified] show ?case by simp 
1484 from th2[simplified] th[simplified] show ?case by simp 
1485 next 
1485 next 
1486 case (6 s t n a) 
1486 case (6 s t n a) 
1487 let ?ns = "fst (zsplit0 s)" 
1487 let ?ns = "fst (zsplit0 s)" 
1488 let ?as = "snd (zsplit0 s)" 
1488 let ?as = "snd (zsplit0 s)" 
1489 let ?nt = "fst (zsplit0 t)" 
1489 let ?nt = "fst (zsplit0 t)" 
1490 let ?at = "snd (zsplit0 t)" 
1490 let ?at = "snd (zsplit0 t)" 
1491 have abjs: "zsplit0 s = (?ns,?as)" by simp 
1491 have abjs: "zsplit0 s = (?ns,?as)" by simp 
1492 moreover have abjt: "zsplit0 t = (?nt,?at)" by simp 
1492 moreover have abjt: "zsplit0 t = (?nt,?at)" by simp 
1493 ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using prems 
1493 ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using 6 
1494 by (simp add: Let_def split_def) 
1494 by (simp add: Let_def split_def) 
1495 from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast 
1495 from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast 
1496 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*) 
1496 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*) 
1497 with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 
1497 with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 
1498 from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast 
1498 from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast 
1499 from th3[simplified] th2[simplified] th[simplified] show ?case 
1499 from th3[simplified] th2[simplified] th[simplified] show ?case 
1500 by (simp add: left_distrib) 
1500 by (simp add: left_distrib) 
1501 next 
1501 next 
1502 case (7 s t n a) 
1502 case (7 s t n a) 
1503 let ?ns = "fst (zsplit0 s)" 
1503 let ?ns = "fst (zsplit0 s)" 
1504 let ?as = "snd (zsplit0 s)" 
1504 let ?as = "snd (zsplit0 s)" 
1505 let ?nt = "fst (zsplit0 t)" 
1505 let ?nt = "fst (zsplit0 t)" 
1506 let ?at = "snd (zsplit0 t)" 
1506 let ?at = "snd (zsplit0 t)" 
1507 have abjs: "zsplit0 s = (?ns,?as)" by simp 
1507 have abjs: "zsplit0 s = (?ns,?as)" by simp 
1508 moreover have abjt: "zsplit0 t = (?nt,?at)" by simp 
1508 moreover have abjt: "zsplit0 t = (?nt,?at)" by simp 
1509 ultimately have th: "a=Sub ?as ?at \<and> n=?ns  ?nt" using prems 
1509 ultimately have th: "a=Sub ?as ?at \<and> n=?ns  ?nt" using 7 
1510 by (simp add: Let_def split_def) 
1510 by (simp add: Let_def split_def) 
1511 from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast 
1511 from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast 
1512 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*) 
1512 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*) 
1513 with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 
1513 with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 
1514 from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast 
1514 from abjs 7 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast 
1515 from th3[simplified] th2[simplified] th[simplified] show ?case 
1515 from th3[simplified] th2[simplified] th[simplified] show ?case 
1516 by (simp add: left_diff_distrib) 
1516 by (simp add: left_diff_distrib) 
1517 next 
1517 next 
1518 case (8 i t n a) 
1518 case (8 i t n a) 
1519 let ?nt = "fst (zsplit0 t)" 
1519 let ?nt = "fst (zsplit0 t)" 
1520 let ?at = "snd (zsplit0 t)" 
1520 let ?at = "snd (zsplit0 t)" 
1521 have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using prems 
1521 have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using 8 
1522 by (simp add: Let_def split_def) 
1522 by (simp add: Let_def split_def) 
1523 from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 
1523 from abj 8 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 
1524 hence " ?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp 
1524 hence "?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp 
1525 also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib) 
1525 also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib) 
1526 finally show ?case using th th2 by simp 
1526 finally show ?case using th th2 by simp 
1527 next 
1527 next 
1528 case (9 t n a) 
1528 case (9 t n a) 
1529 let ?nt = "fst (zsplit0 t)" 
1529 let ?nt = "fst (zsplit0 t)" 
1530 let ?at = "snd (zsplit0 t)" 
1530 let ?at = "snd (zsplit0 t)" 
1531 have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a= Floor ?at \<and> n=?nt" using prems 
1531 have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a= Floor ?at \<and> n=?nt" using 9 
1532 by (simp add: Let_def split_def) 
1532 by (simp add: Let_def split_def) 
1533 from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 
1533 from abj 9 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast 
1534 hence na: "?N a" using th by simp 
1534 hence na: "?N a" using th by simp 
1535 have th': "(real ?nt)*(real x) = real (?nt * x)" by simp 
1535 have th': "(real ?nt)*(real x) = real (?nt * x)" by simp 
1536 have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp 
1536 have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp 
1537 also have "\<dots> = real (floor ((real ?nt)* real(x) + ?I x ?at))" by simp 
1537 also have "\<dots> = real (floor ((real ?nt)* real(x) + ?I x ?at))" by simp 
1538 also have "\<dots> = real (floor (?I x ?at + real (?nt* x)))" by (simp add: add_ac) 
1538 also have "\<dots> = real (floor (?I x ?at + real (?nt* x)))" by (simp add: add_ac) 
2657 moreover 
2661 moreover 
2658 {assume H: "real x  real d + Inum ((real (x d)) # bs) e = 0" 
2662 {assume H: "real x  real d + Inum ((real (x d)) # bs) e = 0" 
2659 hence "real x =  Inum ((real (x d)) # bs) e + real d" by simp 
2663 hence "real x =  Inum ((real (x d)) # bs) e + real d" by simp 
2660 hence "real x =  Inum (a # bs) e + real d" 
2664 hence "real x =  Inum (a # bs) e + real d" 
2661 by (simp add: numbound0_I[OF bn,where b="real x  real d"and b'="a"and bs="bs"]) 
2665 by (simp add: numbound0_I[OF bn,where b="real x  real d"and b'="a"and bs="bs"]) 
2662 with prems(11) have ?case using dp by simp} 
2666 with 4(5) have ?case using dp by simp} 
2663 ultimately show ?case by blast 
2667 ultimately show ?case by blast 
2664 next 
2668 next 
2665 case (9 j c e) hence p: "Ifm (real x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" 
2669 case (9 j c e) hence p: "Ifm (real x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" 
2666 and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+ 
2670 and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+ 
2667 let ?e = "Inum (real x # bs) e" 
2671 let ?e = "Inum (real x # bs) e" 
2668 from prems have "isint e (a #bs)" by simp 
2672 from 9 have "isint e (a #bs)" by simp 
2669 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"] 
2673 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"] 
2670 by (simp add: isint_iff) 
2674 by (simp add: isint_iff) 
2671 from prems have id: "j dvd d" by simp 
2675 from 9 have id: "j dvd d" by simp 
2672 from c1 ie[symmetric] have "?p x = (real j rdvd real (x+ floor ?e))" by simp 
2676 from c1 ie[symmetric] have "?p x = (real j rdvd real (x+ floor ?e))" by simp 
2673 also have "\<dots> = (j dvd x + floor ?e)" 
2677 also have "\<dots> = (j dvd x + floor ?e)" 
2674 using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp 
2678 using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp 
2675 also have "\<dots> = (j dvd x  d + floor ?e)" 
2679 also have "\<dots> = (j dvd x  d + floor ?e)" 
2676 using dvd_period[OF id, where x="x" and c="1" and t="floor ?e"] by simp 
2680 using dvd_period[OF id, where x="x" and c="1" and t="floor ?e"] by simp 
2677 also have "\<dots> = (real j rdvd real (x  d + floor ?e))" 
2681 also have "\<dots> = (real j rdvd real (x  d + floor ?e))" 
2678 using int_rdvd_real[where i="j" and x="real (xd + floor ?e)",symmetric, simplified] 
2682 using int_rdvd_real[where i="j" and x="real (xd + floor ?e)",symmetric, simplified] 
2679 ie by simp 
2683 ie by simp 
2680 also have "\<dots> = (real j rdvd real x  real d + ?e)" 
2684 also have "\<dots> = (real j rdvd real x  real d + ?e)" 
2681 using ie by simp 
2685 using ie by simp 
2682 finally show ?case 
2686 finally show ?case 
2683 using numbound0_I[OF bn,where b="real (xd)" and b'="real x" and bs="bs"] c1 p by simp 
2687 using numbound0_I[OF bn,where b="real (xd)" and b'="real x" and bs="bs"] c1 p by simp 
2684 next 
2688 next 
2685 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+ 
2689 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+ 
2686 let ?e = "Inum (real x # bs) e" 
2690 let ?e = "Inum (real x # bs) e" 
2687 from prems have "isint e (a#bs)" by simp 
2691 from 10 have "isint e (a#bs)" by simp 
2688 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"] 
2692 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"] 
2689 by (simp add: isint_iff) 
2693 by (simp add: isint_iff) 
2690 from prems have id: "j dvd d" by simp 
2694 from 10 have id: "j dvd d" by simp 
2691 from c1 ie[symmetric] have "?p x = (\<not> real j rdvd real (x+ floor ?e))" by simp 
2695 from c1 ie[symmetric] have "?p x = (\<not> real j rdvd real (x+ floor ?e))" by simp 
2692 also have "\<dots> = (\<not> j dvd x + floor ?e)" 
2696 also have "\<dots> = (\<not> j dvd x + floor ?e)" 
2693 using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp 
2697 using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp 
2694 also have "\<dots> = (\<not> j dvd x  d + floor ?e)" 
2698 also have "\<dots> = (\<not> j dvd x  d + floor ?e)" 
2695 using dvd_period[OF id, where x="x" and c="1" and t="floor ?e"] by simp 
2699 using dvd_period[OF id, where x="x" and c="1" and t="floor ?e"] by simp 
2696 also have "\<dots> = (\<not> real j rdvd real (x  d + floor ?e))" 
2700 also have "\<dots> = (\<not> real j rdvd real (x  d + floor ?e))" 
2697 using int_rdvd_real[where i="j" and x="real (xd + floor ?e)",symmetric, simplified] 
2701 using int_rdvd_real[where i="j" and x="real (xd + floor ?e)",symmetric, simplified] 
2698 ie by simp 
2702 ie by simp 
2699 also have "\<dots> = (\<not> real j rdvd real x  real d + ?e)" 
2703 also have "\<dots> = (\<not> real j rdvd real x  real d + ?e)" 
2700 using ie by simp 
2704 using ie by simp 
2701 finally show ?case using numbound0_I[OF bn,where b="real (xd)" and b'="real x" and bs="bs"] c1 p by simp 
2705 finally show ?case 
2702 qed (auto simp add: numbound0_I[where bs="bs" and b="real (x  d)" and b'="real x"] simp del: real_of_int_diff) 
2706 using numbound0_I[OF bn,where b="real (xd)" and b'="real x" and bs="bs"] c1 p by simp 

2707 qed (auto simp add: numbound0_I[where bs="bs" and b="real (x  d)" and b'="real x"] 

2708 simp del: real_of_int_diff) 
2703 
2709 
2704 lemma \<beta>': 
2710 lemma \<beta>': 
2705 assumes lp: "iszlfm p (a #bs)" 
2711 assumes lp: "iszlfm p (a #bs)" 
2706 and u: "d\<beta> p 1" 
2712 and u: "d\<beta> p 1" 
2707 and d: "d\<delta> p d" 
2713 and d: "d\<delta> p d" 
2832 (Ifm ((real ((floor (Inum (b'#bs) t)) div k))#bs) p)" 
2838 (Ifm ((real ((floor (Inum (b'#bs) t)) div k))#bs) p)" 
2833 (is "?I (real x) (?s p) = (?I (real ((floor (?N b' t)) div k)) p)" is "_ = (?I ?tk p)") 
2839 (is "?I (real x) (?s p) = (?I (real ((floor (?N b' t)) div k)) p)" is "_ = (?I ?tk p)") 
2834 using linp kpos tnb 
2840 using linp kpos tnb 
2835 proof(induct p rule: \<sigma>\<rho>.induct) 
2841 proof(induct p rule: \<sigma>\<rho>.induct) 
2836 case (3 c e) 
2842 case (3 c e) 
2837 from prems have cp: "c > 0" and nb: "numbound0 e" by auto 
2843 from 3 have cp: "c > 0" and nb: "numbound0 e" by auto 
2838 {assume kdc: "k dvd c" 
2844 { assume kdc: "k dvd c" 
2839 from kpos have knz: "k\<noteq>0" by simp 
2845 from kpos have knz: "k\<noteq>0" by simp 
2840 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2846 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2841 from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 
2847 from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2848 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2849 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 

2850 moreover 

2851 { assume *: "\<not> k dvd c" 

2852 from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 

2853 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" 

2854 using isint_def by simp 

2855 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)" 

2856 using real_of_int_div[OF knz kdt] 
2842 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2857 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2843 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2858 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 
2844 moreover 
2859 by (simp add: ti algebra_simps) 
2845 {assume "\<not> k dvd c" 
2860 also have "\<dots> = (?I ?tk (Eq (CN 0 c e)))" 
2846 from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 
2861 using nonzero_eq_divide_eq[OF knz', 
2847 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2862 where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 
2848 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)" 
2863 real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2849 using real_of_int_div[OF knz kdt] 

2850 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2851 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 

2852 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"] 

2853 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 
2864 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 
2854 by (simp add: ti) 
2865 by (simp add: ti) 
2855 finally have ?case . } 
2866 finally have ?case . } 
2856 ultimately show ?case by blast 
2867 ultimately show ?case by blast 
2857 next 
2868 next 
2858 case (4 c e) 
2869 case (4 c e) 
2859 from prems have cp: "c > 0" and nb: "numbound0 e" by auto 
2870 then have cp: "c > 0" and nb: "numbound0 e" by auto 
2860 {assume kdc: "k dvd c" 
2871 { assume kdc: "k dvd c" 
2861 from kpos have knz: "k\<noteq>0" by simp 
2872 from kpos have knz: "k\<noteq>0" by simp 
2862 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2873 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2863 from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 
2874 from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2875 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2876 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 

2877 moreover 

2878 { assume *: "\<not> k dvd c" 

2879 from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 

2880 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2881 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)" 

2882 using real_of_int_div[OF knz kdt] 
2864 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2883 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2884 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2885 by (simp add: ti algebra_simps) 

2886 also have "\<dots> = (?I ?tk (NEq (CN 0 c e)))" 

2887 using nonzero_eq_divide_eq[OF knz', 

2888 where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 

2889 real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2890 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2891 by (simp add: ti) 

2892 finally have ?case . } 

2893 ultimately show ?case by blast 

2894 next 

2895 case (5 c e) 

2896 then have cp: "c > 0" and nb: "numbound0 e" by auto 

2897 { assume kdc: "k dvd c" 

2898 from kpos have knz: "k\<noteq>0" by simp 

2899 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2900 from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2901 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2865 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2902 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2866 moreover 
2903 moreover 
2867 {assume "\<not> k dvd c" 
2904 { assume *: "\<not> k dvd c" 
2868 from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 
2905 from kpos have knz: "k\<noteq>0" by simp 
2869 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2906 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2870 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)" 
2907 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)" 
2871 using real_of_int_div[OF knz kdt] 
2908 using real_of_int_div[OF knz kdt] 
2872 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2873 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 

2874 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"] 

2875 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2876 by (simp add: ti) 

2877 finally have ?case . } 

2878 ultimately show ?case by blast 

2879 next 

2880 case (5 c e) 

2881 from prems have cp: "c > 0" and nb: "numbound0 e" by auto 

2882 {assume kdc: "k dvd c" 

2883 from kpos have knz: "k\<noteq>0" by simp 

2884 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2885 from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2886 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2909 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2910 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2911 by (simp add: ti algebra_simps) 

2912 also have "\<dots> = (?I ?tk (Lt (CN 0 c e)))" 

2913 using pos_less_divide_eq[OF kpos, 

2914 where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 

2915 real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2916 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2917 by (simp add: ti) 

2918 finally have ?case . } 

2919 ultimately show ?case by blast 

2920 next 

2921 case (6 c e) 

2922 then have cp: "c > 0" and nb: "numbound0 e" by auto 

2923 { assume kdc: "k dvd c" 

2924 from kpos have knz: "k\<noteq>0" by simp 

2925 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2926 from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2927 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2887 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2928 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2888 moreover 
2929 moreover 
2889 {assume "\<not> k dvd c" 
2930 { assume *: "\<not> k dvd c" 
2890 from kpos have knz: "k\<noteq>0" by simp 
2931 from kpos have knz: "k\<noteq>0" by simp 
2891 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2932 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2892 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)" 
2933 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)" 
2893 using real_of_int_div[OF knz kdt] 
2934 using real_of_int_div[OF knz kdt] 
2894 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2895 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 

2896 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"] 

2897 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2898 by (simp add: ti) 

2899 finally have ?case . } 

2900 ultimately show ?case by blast 

2901 next 

2902 case (6 c e) 

2903 from prems have cp: "c > 0" and nb: "numbound0 e" by auto 

2904 {assume kdc: "k dvd c" 

2905 from kpos have knz: "k\<noteq>0" by simp 

2906 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2907 from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2908 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2935 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2936 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2937 by (simp add: ti algebra_simps) 

2938 also have "\<dots> = (?I ?tk (Le (CN 0 c e)))" 

2939 using pos_le_divide_eq[OF kpos, 

2940 where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 

2941 real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2942 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2943 by (simp add: ti) 

2944 finally have ?case . } 

2945 ultimately show ?case by blast 

2946 next 

2947 case (7 c e) 

2948 then have cp: "c > 0" and nb: "numbound0 e" by auto 

2949 { assume kdc: "k dvd c" 

2950 from kpos have knz: "k\<noteq>0" by simp 

2951 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2952 from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2953 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2909 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2954 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2910 moreover 
2955 moreover 
2911 {assume "\<not> k dvd c" 
2956 { assume *: "\<not> k dvd c" 
2912 from kpos have knz: "k\<noteq>0" by simp 
2957 from kpos have knz: "k\<noteq>0" by simp 
2913 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2958 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2914 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)" 
2959 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)" 
2915 using real_of_int_div[OF knz kdt] 
2960 using real_of_int_div[OF knz kdt] 
2916 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2917 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 

2918 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"] 

2919 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2920 by (simp add: ti) 

2921 finally have ?case . } 

2922 ultimately show ?case by blast 

2923 next 

2924 case (7 c e) 

2925 from prems have cp: "c > 0" and nb: "numbound0 e" by auto 

2926 {assume kdc: "k dvd c" 

2927 from kpos have knz: "k\<noteq>0" by simp 

2928 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2929 from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2930 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2961 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2962 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2963 by (simp add: ti algebra_simps) 

2964 also have "\<dots> = (?I ?tk (Gt (CN 0 c e)))" 

2965 using pos_divide_less_eq[OF kpos, 

2966 where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 

2967 real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2968 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2969 by (simp add: ti) 

2970 finally have ?case . } 

2971 ultimately show ?case by blast 

2972 next 

2973 case (8 c e) 

2974 then have cp: "c > 0" and nb: "numbound0 e" by auto 

2975 { assume kdc: "k dvd c" 

2976 from kpos have knz: "k\<noteq>0" by simp 

2977 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2978 from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2979 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2931 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2980 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2932 moreover 
2981 moreover 
2933 {assume "\<not> k dvd c" 
2982 { assume *: "\<not> k dvd c" 
2934 from kpos have knz: "k\<noteq>0" by simp 
2983 from kpos have knz: "k\<noteq>0" by simp 
2935 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2984 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2936 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)" 
2985 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)" 
2937 using real_of_int_div[OF knz kdt] 
2986 using real_of_int_div[OF knz kdt] 
2938 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2939 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 

2940 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"] 

2941 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2942 by (simp add: ti) 

2943 finally have ?case . } 

2944 ultimately show ?case by blast 

2945 next 

2946 case (8 c e) 

2947 from prems have cp: "c > 0" and nb: "numbound0 e" by auto 

2948 {assume kdc: "k dvd c" 

2949 from kpos have knz: "k\<noteq>0" by simp 

2950 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2951 from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2952 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2987 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2988 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2989 by (simp add: ti algebra_simps) 

2990 also have "\<dots> = (?I ?tk (Ge (CN 0 c e)))" 

2991 using pos_divide_le_eq[OF kpos, 

2992 where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] 

2993 real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2994 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2995 by (simp add: ti) 

2996 finally have ?case . } 

2997 ultimately show ?case by blast 

2998 next 

2999 case (9 i c e) 

3000 then have cp: "c > 0" and nb: "numbound0 e" by auto 

3001 { assume kdc: "k dvd c" 

3002 from kpos have knz: "k\<noteq>0" by simp 

3003 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

3004 from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

3005 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2953 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
3006 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2954 moreover 
3007 moreover 
2955 {assume "\<not> k dvd c" 
3008 { assume *: "\<not> k dvd c" 
2956 from kpos have knz: "k\<noteq>0" by simp 
3009 from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 
2957 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
3010 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2958 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)" 
3011 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)" 
2959 using real_of_int_div[OF knz kdt] 
3012 using real_of_int_div[OF knz kdt] 
2960 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2961 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 

2962 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"] 

2963 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2964 by (simp add: ti) 

2965 finally have ?case . } 

2966 ultimately show ?case by blast 

2967 next 

2968 case (9 i c e) from prems have cp: "c > 0" and nb: "numbound0 e" by auto 

2969 {assume kdc: "k dvd c" 

2970 from kpos have knz: "k\<noteq>0" by simp 

2971 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2972 from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2973 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
3013 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

3014 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

3015 by (simp add: ti algebra_simps) 

3016 also have "\<dots> = (?I ?tk (Dvd i (CN 0 c e)))" 

3017 using rdvd_mult[OF knz, where n="i"] 

3018 real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

3019 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

3020 by (simp add: ti) 

3021 finally have ?case . } 

3022 ultimately show ?case by blast 

3023 next 

3024 case (10 i c e) 

3025 then have cp: "c > 0" and nb: "numbound0 e" by auto 

3026 { assume kdc: "k dvd c" 

3027 from kpos have knz: "k\<noteq>0" by simp 

3028 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

3029 from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

3030 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2974 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
3031 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
2975 moreover 
3032 moreover 
2976 {assume "\<not> k dvd c" 
3033 { assume *: "\<not> k dvd c" 
2977 from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 
3034 from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 
2978 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
3035 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
2979 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)" 
3036 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))" 
2980 using real_of_int_div[OF knz kdt] 
3037 using real_of_int_div[OF knz kdt] 
2981 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 

2982 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 

2983 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"] 

2984 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 

2985 by (simp add: ti) 

2986 finally have ?case . } 

2987 ultimately show ?case by blast 

2988 next 

2989 case (10 i c e) from prems have cp: "c > 0" and nb: "numbound0 e" by auto 

2990 {assume kdc: "k dvd c" 

2991 from kpos have knz: "k\<noteq>0" by simp 

2992 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 

2993 from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] 

2994 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
3038 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
2995 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
3039 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 
2996 moreover 
3040 by (simp add: ti algebra_simps) 
2997 {assume "\<not> k dvd c" 
3041 also have "\<dots> = (?I ?tk (NDvd i (CN 0 c e)))" 
2998 from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp 
3042 using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt] 
2999 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp 
3043 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
3000 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))" 
3044 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 
3001 using real_of_int_div[OF knz kdt] 
3045 by (simp add: ti) 
3002 numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] 
3046 finally have ?case . } 
3003 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) 
3047 ultimately show ?case by blast 
3004 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"] 
3048 qed (simp_all add: bound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"] 
3005 numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] 
3049 numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"]) 
3006 by (simp add: ti) 

3007 finally have ?case . } 

3008 ultimately show ?case by blast 

3009 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"]) 

3010 
3050 
3011 
3051 
3012 lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t" 
3052 lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t" 
3013 shows "bound0 (\<sigma>\<rho> p (t,k))" 
3053 shows "bound0 (\<sigma>\<rho> p (t,k))" 
3014 using lp 
3054 using lp 
3116 by (simp only: add_ac diff_minus) 
3156 by (simp only: add_ac diff_minus) 
3117 with nob have ?case by blast } 
3157 with nob have ?case by blast } 
3118 ultimately show ?case by blast 
3158 ultimately show ?case by blast 
3119 next 
3159 next 
3120 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+ 
3160 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+ 
3121 let ?e = "Inum (real i # bs) e" 
3161 let ?e = "Inum (real i # bs) e" 
3122 from prems have "isint e (real i #bs)" by simp 
3162 from 9 have "isint e (real i #bs)" by simp 
3123 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"] 
3163 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"] 
3124 by (simp add: isint_iff) 
3164 by (simp add: isint_iff) 
3125 from prems have id: "j dvd d" by simp 
3165 from 9 have id: "j dvd d" by simp 
3126 from ie[symmetric] have "?p i = (real j rdvd real (c*i+ floor ?e))" by simp 
3166 from ie[symmetric] have "?p i = (real j rdvd real (c*i+ floor ?e))" by simp 
3127 also have "\<dots> = (j dvd c*i + floor ?e)" 
3167 also have "\<dots> = (j dvd c*i + floor ?e)" 
3128 using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp 
3168 using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp 
3129 also have "\<dots> = (j dvd c*i  c*d + floor ?e)" 
3169 also have "\<dots> = (j dvd c*i  c*d + floor ?e)" 
3130 using dvd_period[OF id, where x="c*i" and c="c" and t="floor ?e"] by simp 
3170 using dvd_period[OF id, where x="c*i" and c="c" and t="floor ?e"] by simp 
3131 also have "\<dots> = (real j rdvd real (c*i  c*d + floor ?e))" 
3171 also have "\<dots> = (real j rdvd real (c*i  c*d + floor ?e))" 
3132 using int_rdvd_iff[where i="j" and t="(c*i  c*d + floor ?e)",symmetric, simplified] 
3172 using int_rdvd_iff[where i="j" and t="(c*i  c*d + floor ?e)",symmetric, simplified] 
3133 ie by simp 
3173 ie by simp 
3134 also have "\<dots> = (real j rdvd real (c*(i  d)) + ?e)" 
3174 also have "\<dots> = (real j rdvd real (c*(i  d)) + ?e)" 
3135 using ie by (simp add:algebra_simps) 
3175 using ie by (simp add:algebra_simps) 
3136 finally show ?case 
3176 finally show ?case 
3137 using numbound0_I[OF bn,where b="real i  real d" and b'="real i" and bs="bs"] p 
3177 using numbound0_I[OF bn,where b="real i  real d" and b'="real i" and bs="bs"] p 
3138 by (simp add: algebra_simps) 
3178 by (simp add: algebra_simps) 
3139 next 
3179 next 
3140 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+ 
3180 case (10 j c e) 
3141 let ?e = "Inum (real i # bs) e" 
3181 hence p: "\<not> (real j rdvd real (c*i) + ?N i e)" (is "?p x") and cp: "c > 0" and bn:"numbound0 e" 
3142 from prems have "isint e (real i #bs)" by simp 
3182 by simp+ 
3143 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"] 
3183 let ?e = "Inum (real i # bs) e" 
3144 by (simp add: isint_iff) 
3184 from 10 have "isint e (real i #bs)" by simp 
3145 from prems have id: "j dvd d" by simp 
3185 hence ie: "real (floor ?e) = ?e" 
3146 from ie[symmetric] have "?p i = (\<not> (real j rdvd real (c*i+ floor ?e)))" by simp 
3186 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"] 
3147 also have "\<dots> = Not (j dvd c*i + floor ?e)" 
3187 by (simp add: isint_iff) 
3148 using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp 
3188 from 10 have id: "j dvd d" by simp 
3149 also have "\<dots> = Not (j dvd c*i  c*d + floor ?e)" 
3189 from ie[symmetric] have "?p i = (\<not> (real j rdvd real (c*i+ floor ?e)))" by simp 
3150 using dvd_period[OF id, where x="c*i" and c="c" and t="floor ?e"] by simp 
3190 also have "\<dots> = Not (j dvd c*i + floor ?e)" 
3151 also have "\<dots> = Not (real j rdvd real (c*i  c*d + floor ?e))" 
3191 using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp 
3152 using int_rdvd_iff[where i="j" and t="(c*i  c*d + floor ?e)",symmetric, simplified] 
3192 also have "\<dots> = Not (j dvd c*i  c*d + floor ?e)" 

3193 using dvd_period[OF id, where x="c*i" and c="c" and t="floor ?e"] by simp 

3194 also have "\<dots> = Not (real j rdvd real (c*i  c*d + floor ?e))" 

3195 using int_rdvd_iff[where i="j" and t="(c*i  c*d + floor ?e)",symmetric, simplified] 
3153 ie by simp 
3196 ie by simp 
3154 also have "\<dots> = Not (real j rdvd real (c*(i  d)) + ?e)" 
3197 also have "\<dots> = Not (real j rdvd real (c*(i  d)) + ?e)" 
3155 using ie by (simp add:algebra_simps) 
3198 using ie by (simp add:algebra_simps) 
3156 finally show ?case 
3199 finally show ?case 
3157 using numbound0_I[OF bn,where b="real i  real d" and b'="real i" and bs="bs"] p 
3200 using numbound0_I[OF bn,where b="real i  real d" and b'="real i" and bs="bs"] p 
3158 by (simp add: algebra_simps) 
3201 by (simp add: algebra_simps) 
3159 qed(auto simp add: numbound0_I[where bs="bs" and b="real i  real d" and b'="real i"]) 
3202 qed (auto simp add: numbound0_I[where bs="bs" and b="real i  real d" and b'="real i"]) 
3160 
3203 
3161 lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t" 
3204 lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t" 
3162 shows "bound0 (\<sigma> p k t)" 
3205 shows "bound0 (\<sigma> p k t)" 
3163 using \<sigma>\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def) 
3206 using \<sigma>\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def) 
3164 
3207 
3359 have FS: "?SS (Floor a) = 
3402 have FS: "?SS (Floor a) = 
3360 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
3403 ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
3361 (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 
3404 (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 
3362 (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 
3405 (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 
3363 show ?case 
3406 show ?case 
3364 proof(simp only: FS, clarsimp simp del: Ifm.simps Inum.simps, ) 
3407 proof(simp only: FS, clarsimp simp del: Ifm.simps Inum.simps, ) 
3365 fix p n s 
3408 fix p n s 
3366 let ?ths = "(?I p \<longrightarrow> (?N (Floor a) = ?N (CN 0 n s))) \<and> numbound0 s \<and> isrlfm p" 
3409 let ?ths = "(?I p \<longrightarrow> (?N (Floor a) = ?N (CN 0 n s))) \<and> numbound0 s \<and> isrlfm p" 
3367 assume "(\<exists>ba. (p, 0, ba) \<in> set (rsplit0 a) \<and> n = 0 \<and> s = Floor ba) \<or> 
3410 assume "(\<exists>ba. (p, 0, ba) \<in> set (rsplit0 a) \<and> n = 0 \<and> s = Floor ba) \<or> 
3368 (\<exists>ab ac ba. 
3411 (\<exists>ab ac ba. 
3369 (ab, ac, ba) \<in> set (rsplit0 a) \<and> 
3412 (ab, ac, ba) \<in> set (rsplit0 a) \<and> 
3370 0 < ac \<and> 
3413 0 < ac \<and> 
3371 (\<exists>j. p = fp ab ac ba j \<and> 
3414 (\<exists>j. p = fp ab ac ba j \<and> 
3372 n = 0 \<and> s = Add (Floor ba) (C j) \<and> 0 \<le> j \<and> j \<le> ac)) \<or> 
3415 n = 0 \<and> s = Add (Floor ba) (C j) \<and> 0 \<le> j \<and> j \<le> ac)) \<or> 
3373 (\<exists>ab ac ba. 
3416 (\<exists>ab ac ba. 
3374 (ab, ac, ba) \<in> set (rsplit0 a) \<and> 
3417 (ab, ac, ba) \<in> set (rsplit0 a) \<and> 
3375 ac < 0 \<and> 
3418 ac < 0 \<and> 
3376 (\<exists>j. p = fp ab ac ba j \<and> 
3419 (\<exists>j. p = fp ab ac ba j \<and> 
3377 n = 0 \<and> s = Add (Floor ba) (C j) \<and> ac \<le> j \<and> j \<le> 0))" 
3420 n = 0 \<and> s = Add (Floor ba) (C j) \<and> ac \<le> j \<and> j \<le> 0))" 
3378 moreover 
3421 moreover 
3379 {fix s' 
3422 { fix s' 
3380 assume "(p, 0, s') \<in> ?SS a" and "n = 0" and "s = Floor s'" 
3423 assume "(p, 0, s') \<in> ?SS a" and "n = 0" and "s = Floor s'" 
3381 hence ?ths using prems by auto} 
3424 hence ?ths using 5(1) by auto } 
3382 moreover 
3425 moreover 
3383 { fix p' n' s' j 
3426 { fix p' n' s' j 
3384 assume pns: "(p', n', s') \<in> ?SS a" 
3427 assume pns: "(p', n', s') \<in> ?SS a" 
3385 and np: "0 < n'" 
3428 and np: "0 < n'" 
3386 and p_def: "p = ?p (p',n',s') j" 
3429 and p_def: "p = ?p (p',n',s') j" 
3387 and n0: "n = 0" 
3430 and n0: "n = 0" 
3388 and s_def: "s = (Add (Floor s') (C j))" 
3431 and s_def: "s = (Add (Floor s') (C j))" 
3389 and jp: "0 \<le> j" and jn: "j \<le> n'" 
3432 and jp: "0 \<le> j" and jn: "j \<le> n'" 
3390 from prems pns have H:"(Ifm ((x\<Colon>real) # (bs\<Colon>real list)) p' \<longrightarrow> 
3433 from 5 pns have H:"(Ifm ((x\<Colon>real) # (bs\<Colon>real list)) p' \<longrightarrow> 
3391 Inum (x # bs) a = Inum (x # bs) (CN 0 n' s')) \<and> 
3434 Inum (x # bs) a = Inum (x # bs) (CN 0 n' s')) \<and> 
3392 numbound0 s' \<and> isrlfm p'" by blast 
3435 numbound0 s' \<and> isrlfm p'" by blast 
3393 hence nb: "numbound0 s'" by simp 
3436 hence nb: "numbound0 s'" by simp 
3394 from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by (simp add: numsub_nb) 
3437 from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by (simp add: numsub_nb) 
3395 let ?nxs = "CN 0 n' s'" 
3438 let ?nxs = "CN 0 n' s'" 
3396 let ?l = "floor (?N s') + j" 
3439 let ?l = "floor (?N s') + j" 
3397 from H 
3440 from H 
3398 have "?I (?p (p',n',s') j) \<longrightarrow> 
3441 have "?I (?p (p',n',s') j) \<longrightarrow> 
3399 (((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?N a = ?N ?nxs ))" 
3442 (((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?N a = ?N ?nxs ))" 
3400 by (simp add: fp_def np algebra_simps numsub numadd numfloor) 
3443 by (simp add: fp_def np algebra_simps numsub numadd numfloor) 
3401 also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))" 
3444 also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))" 
3402 using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp 
3445 using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp 
3403 moreover 

3404 have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp 

3405 ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" 

3406 by blast 

3407 with s_def n0 p_def nb nf have ?ths by auto} 

3408 moreover 
3446 moreover 
3409 {fix p' n' s' j 
3447 have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp 
3410 assume pns: "(p', n', s') \<in> ?SS a" 
3448 ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" 
3411 and np: "n' < 0" 
3449 by blast 
3412 and p_def: "p = ?p (p',n',s') j" 
3450 with s_def n0 p_def nb nf have ?ths by auto} 
3413 and n0: "n = 0" 
3451 moreover 
3414 and s_def: "s = (Add (Floor s') (C j))" 
3452 { fix p' n' s' j 
3415 and jp: "n' \<le> j" and jn: "j \<le> 0" 
3453 assume pns: "(p', n', s') \<in> ?SS a" 
3416 from prems pns have H:"(Ifm ((x\<Colon>real) # (bs\<Colon>real list)) p' \<longrightarrow> 
3454 and np: "n' < 0" 

3455 and p_def: "p = ?p (p',n',s') j" 

3456 and n0: "n = 0" 

3457 and s_def: "s = (Add (Floor s') (C j))" 

3458 and jp: "n' \<le> j" and jn: "j \<le> 0" 

3459 from 5 pns have H:"(Ifm ((x\<Colon>real) # (bs\<Colon>real list)) p' \<longrightarrow> 
3417 Inum (x # bs) a = Inum (x # bs) (CN 0 n' s')) \<and> 
3460 Inum (x # bs) a = Inum (x # bs) (CN 0 n' s')) \<and> 
3418 numbound0 s' \<and> isrlfm p'" by blast 
3461 numbound0 s' \<and> isrlfm p'" by blast 
3419 hence nb: "numbound0 s'" by simp 
3462 hence nb: "numbound0 s'" by simp 
3420 from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by (simp add: numneg_nb) 
3463 from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by (simp add: numneg_nb) 
3421 let ?nxs = "CN 0 n' s'" 
3464 let ?nxs = "CN 0 n' s'" 
3422 let ?l = "floor (?N s') + j" 
3465 let ?l = "floor (?N s') + j" 
3423 from H 
3466 from H 
3424 have "?I (?p (p',n',s') j) \<longrightarrow> 
3467 have "?I (?p (p',n',s') j) \<longrightarrow> 
3425 (((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?N a = ?N ?nxs ))" 
3468 (((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?N a = ?N ?nxs ))" 
3426 by (simp add: np fp_def algebra_simps numneg numfloor numadd numsub) 
3469 by (simp add: np fp_def algebra_simps numneg numfloor numadd numsub) 
3427 also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))" 
3470 also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))" 
3428 using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp 
3471 using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp 
3429 moreover 
3472 moreover 
3430 have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp 
3473 have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp 
3431 ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" 
3474 ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" 
3432 by blast 
3475 by blast 
3433 with s_def n0 p_def nb nf have ?ths by auto} 
3476 with s_def n0 p_def nb nf have ?ths by auto} 
3434 ultimately show ?ths by auto 
3477 ultimately show ?ths by auto 
3435 qed 
3478 qed 
3436 next 
3479 next 
3437 case (3 a b) then show ?case 
3480 case (3 a b) then show ?case 
3438 apply auto 
3481 apply auto 
3439 apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all 
3482 apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all 
3440 apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all 
3483 apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all 
3441 done 
3484 done 
3442 qed (auto simp add: Let_def split_def algebra_simps conj_rl) 
3485 qed (auto simp add: Let_def split_def algebra_simps conj_rl) 
3443 
3486 
3444 lemma real_in_int_intervals: 
3487 lemma real_in_int_intervals: 
3445 assumes xb: "real m \<le> x \<and> x < real ((n::int) + 1)" 
3488 assumes xb: "real m \<le> x \<and> x < real ((n::int) + 1)" 
3446 shows "\<exists> j\<in> {m.. n}. real j \<le> x \<and> x < real (j+1)" (is "\<exists> j\<in> ?N. ?P j") 
3489 shows "\<exists> j\<in> {m.. n}. real j \<le> x \<and> x < real (j+1)" (is "\<exists> j\<in> ?N. ?P j") 
3981 {assume "bound0 (Gt a)" hence bn:"bound0 (simpfm (Gt a))" 
4023 {assume "bound0 (Gt a)" hence bn:"bound0 (simpfm (Gt a))" 
3982 using simpfm_bound0 by blast 
4024 using simpfm_bound0 by blast 
3983 have "isatom (simpfm (Gt a))" by (cases "simpnum a", auto simp add: Let_def) 
4025 have "isatom (simpfm (Gt a))" by (cases "simpnum a", auto simp add: Let_def) 
3984 with bn bound0at_l have ?case by blast} 
4026 with bn bound0at_l have ?case by blast} 
3985 moreover 
4027 moreover 
3986 {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e" 
4028 { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e" 
3987 { 
4029 { assume cn1: "numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 
3988 assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 

3989 with numgcd_pos[where t="CN 0 c (simpnum e)"] 
4030 with numgcd_pos[where t="CN 0 c (simpnum e)"] 
3990 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 
4031 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 
3991 from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
4032 from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
3992 by (simp add: numgcd_def) 
4033 by (simp add: numgcd_def) 
3993 from prems have th': "c\<noteq>0" by auto 
4034 from `c > 0` have th': "c\<noteq>0" by auto 
3994 from prems have cp: "c \<ge> 0" by simp 
4035 from `c > 0` have cp: "c \<ge> 0" by simp 
3995 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 
4036 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 
3996 have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 
4037 have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 
3997 } 
4038 } 
3998 with prems have ?case 
4039 with Gt a have ?case 
3999 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 
4040 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 
4000 ultimately show ?case by blast 
4041 ultimately show ?case by blast 
4001 next 
4042 next 
4002 case (Ge a) 
4043 case (Ge a) 
4003 hence "bound0 (Ge a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)" 
4044 hence "bound0 (Ge a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)" 
4004 by (cases a,simp_all, case_tac "nat", simp_all) 
4045 by (cases a,simp_all, case_tac "nat", simp_all) 
4005 moreover 
4046 moreover 
4006 {assume "bound0 (Ge a)" hence bn:"bound0 (simpfm (Ge a))" 
4047 { assume "bound0 (Ge a)" hence bn:"bound0 (simpfm (Ge a))" 
4007 using simpfm_bound0 by blast 
4048 using simpfm_bound0 by blast 
4008 have "isatom (simpfm (Ge a))" by (cases "simpnum a", auto simp add: Let_def) 
4049 have "isatom (simpfm (Ge a))" by (cases "simpnum a", auto simp add: Let_def) 
4009 with bn bound0at_l have ?case by blast} 
4050 with bn bound0at_l have ?case by blast} 
4010 moreover 
4051 moreover 
4011 {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e" 
4052 { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e" 
4012 { 
4053 { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 
4013 assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 

4014 with numgcd_pos[where t="CN 0 c (simpnum e)"] 
4054 with numgcd_pos[where t="CN 0 c (simpnum e)"] 
4015 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 
4055 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 
4016 from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
4056 from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
4017 by (simp add: numgcd_def) 
4057 by (simp add: numgcd_def) 
4018 from prems have th': "c\<noteq>0" by auto 
4058 from `c > 0` have th': "c\<noteq>0" by auto 
4019 from prems have cp: "c \<ge> 0" by simp 
4059 from `c > 0` have cp: "c \<ge> 0" by simp 
4020 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 
4060 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 
4021 have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 
4061 have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 
4022 } 
4062 } 
4023 with prems have ?case 
4063 with Ge a have ?case 
4024 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 
4064 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 
4025 ultimately show ?case by blast 
4065 ultimately show ?case by blast 
4026 next 
4066 next 
4027 case (Eq a) 
4067 case (Eq a) 
4028 hence "bound0 (Eq a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)" 
4068 hence "bound0 (Eq a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)" 
4029 by (cases a,simp_all, case_tac "nat", simp_all) 
4069 by (cases a,simp_all, case_tac "nat", simp_all) 
4030 moreover 
4070 moreover 
4031 {assume "bound0 (Eq a)" hence bn:"bound0 (simpfm (Eq a))" 
4071 { assume "bound0 (Eq a)" hence bn:"bound0 (simpfm (Eq a))" 
4032 using simpfm_bound0 by blast 
4072 using simpfm_bound0 by blast 
4033 have "isatom (simpfm (Eq a))" by (cases "simpnum a", auto simp add: Let_def) 
4073 have "isatom (simpfm (Eq a))" by (cases "simpnum a", auto simp add: Let_def) 
4034 with bn bound0at_l have ?case by blast} 
4074 with bn bound0at_l have ?case by blast} 
4035 moreover 
4075 moreover 
4036 {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e" 
4076 { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e" 
4037 { 
4077 { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 
4038 assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0" 

4039 with numgcd_pos[where t="CN 0 c (simpnum e)"] 
4078 with numgcd_pos[where t="CN 0 c (simpnum e)"] 
4040 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 
4079 have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp 
4041 from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
4080 from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
4042 by (simp add: numgcd_def) 
4081 by (simp add: numgcd_def) 
4043 from prems have th': "c\<noteq>0" by auto 
4082 from `c > 0` have th': "c\<noteq>0" by auto 
4044 from prems have cp: "c \<ge> 0" by simp 
4083 from `c > 0` have cp: "c \<ge> 0" by simp 
4045 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 
4084 from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']] 
4046 have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 
4085 have "0 < c div numgcd (CN 0 c (simpnum e))" by simp 
4047 } 
4086 } 
4048 with prems have ?case 
4087 with Eq a have ?case 
4049 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 
4088 by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)} 
4050 ultimately show ?case by blast 
4089 ultimately show ?case by blast 
4051 next 
4090 next 
4052 case (NEq a) 
4091 case (NEq a) 
4053 hence "bound0 (NEq a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)" 
4092 hence "bound0 (NEq a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)" 
4385 lemma \<upsilon>_I: assumes lp: "isrlfm p" 
4423 lemma \<upsilon>_I: assumes lp: "isrlfm p" 
4386 and np: "real n > 0" and nbt: "numbound0 t" 
4424 and np: "real n > 0" and nbt: "numbound0 t" 
4387 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> _") 
4425 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> _") 
4388 using lp 
4426 using lp 
4389 proof(induct p rule: \<upsilon>.induct) 
4427 proof(induct p rule: \<upsilon>.induct) 
4390 case (5 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 
4428 case (5 c e) 

4429 from 5 have cp: "c >0" and nb: "numbound0 e" by simp_all 
4391 have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)" 
4430 have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)" 
4392 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4431 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4393 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)" 
4432 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)" 
4394 by (simp only: pos_less_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4433 by (simp only: pos_less_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4395 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) 
4434 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) 
4396 also have "\<dots> = (real c *?t + ?n* (?N x e) < 0)" 
4435 also have "\<dots> = (real c *?t + ?n* (?N x e) < 0)" 
4397 using np by simp 
4436 using np by simp 
4398 finally show ?case using nbt nb by (simp add: algebra_simps) 
4437 finally show ?case using nbt nb by (simp add: algebra_simps) 
4399 next 
4438 next 
4400 case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 
4439 case (6 c e) 

4440 from 6 have cp: "c >0" and nb: "numbound0 e" by simp_all 
4401 have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)" 
4441 have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)" 
4402 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4442 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4403 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)" 
4443 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)" 
4404 by (simp only: pos_le_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4444 by (simp only: pos_le_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4405 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) 
4445 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) 
4406 also have "\<dots> = (real c *?t + ?n* (?N x e) \<le> 0)" 
4446 also have "\<dots> = (real c *?t + ?n* (?N x e) \<le> 0)" 
4407 using np by simp 
4447 using np by simp 
4408 finally show ?case using nbt nb by (simp add: algebra_simps) 
4448 finally show ?case using nbt nb by (simp add: algebra_simps) 
4409 next 
4449 next 
4410 case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 
4450 case (7 c e) 

4451 from 7 have cp: "c >0" and nb: "numbound0 e" by simp_all 
4411 have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)" 
4452 have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)" 
4412 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4453 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4413 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)" 
4454 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)" 
4414 by (simp only: pos_divide_less_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4455 by (simp only: pos_divide_less_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4415 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) 
4456 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) 
4416 also have "\<dots> = (real c *?t + ?n* (?N x e) > 0)" 
4457 also have "\<dots> = (real c *?t + ?n* (?N x e) > 0)" 
4417 using np by simp 
4458 using np by simp 
4418 finally show ?case using nbt nb by (simp add: algebra_simps) 
4459 finally show ?case using nbt nb by (simp add: algebra_simps) 
4419 next 
4460 next 
4420 case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 
4461 case (8 c e) 

4462 from 8 have cp: "c >0" and nb: "numbound0 e" by simp_all 
4421 have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)" 
4463 have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)" 
4422 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4464 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4423 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)" 
4465 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)" 
4424 by (simp only: pos_divide_le_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4466 by (simp only: pos_divide_le_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4425 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) 
4467 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) 
4426 also have "\<dots> = (real c *?t + ?n* (?N x e) \<ge> 0)" 
4468 also have "\<dots> = (real c *?t + ?n* (?N x e) \<ge> 0)" 
4427 using np by simp 
4469 using np by simp 
4428 finally show ?case using nbt nb by (simp add: algebra_simps) 
4470 finally show ?case using nbt nb by (simp add: algebra_simps) 
4429 next 
4471 next 
4430 case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 
4472 case (3 c e) 

4473 from 3 have cp: "c >0" and nb: "numbound0 e" by simp_all 
4431 from np have np: "real n \<noteq> 0" by simp 
4474 from np have np: "real n \<noteq> 0" by simp 
4432 have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)" 
4475 have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)" 
4433 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4476 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4434 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) = 0)" 
4477 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) = 0)" 
4435 by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4478 by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4436 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) 
4479 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) 
4437 also have "\<dots> = (real c *?t + ?n* (?N x e) = 0)" 
4480 also have "\<dots> = (real c *?t + ?n* (?N x e) = 0)" 
4438 using np by simp 
4481 using np by simp 
4439 finally show ?case using nbt nb by (simp add: algebra_simps) 
4482 finally show ?case using nbt nb by (simp add: algebra_simps) 
4440 next 
4483 next 
4441 case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ 
4484 case (4 c e) 

4485 from 4 have cp: "c >0" and nb: "numbound0 e" by simp_all 
4442 from np have np: "real n \<noteq> 0" by simp 
4486 from np have np: "real n \<noteq> 0" by simp 
4443 have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<noteq> 0)" 
4487 have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<noteq> 0)" 
4444 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4488 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp 
4445 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)" 
4489 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)" 
4446 by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4490 by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
4495 and lx: "l < x" and xu:"x < u" and px:" Ifm (x#bs) p" 
4539 and lx: "l < x" and xu:"x < u" and px:" Ifm (x#bs) p" 
4496 and ly: "l < y" and yu: "y < u" 
4540 and ly: "l < y" and yu: "y < u" 
4497 shows "Ifm (y#bs) p" 
4541 shows "Ifm (y#bs) p" 
4498 using lp px noS 
4542 using lp px noS 
4499 proof (induct p rule: isrlfm.induct) 
4543 proof (induct p rule: isrlfm.induct) 
4500 case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 
4544 case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 
4501 from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps) 
4545 from 5 have "x * real c + ?N x e < 0" by (simp add: algebra_simps) 
4502 hence pxc: "x < ( ?N x e) / real c" 
4546 hence pxc: "x < ( ?N x e) / real c" 
4503 by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="?N x e"]) 
4547 by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="?N x e"]) 
4504 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4548 from 5 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4505 with ly yu have yne: "y \<noteq>  ?N x e / real c" by auto 
4549 with ly yu have yne: "y \<noteq>  ?N x e / real c" by auto 
4506 hence "y < ( ?N x e) / real c \<or> y > (?N x e) / real c" by auto 
4550 hence "y < ( ?N x e) / real c \<or> y > (?N x e) / real c" by auto 
4507 moreover {assume y: "y < (?N x e)/ real c" 
4551 moreover {assume y: "y < (?N x e)/ real c" 
4508 hence "y * real c <  ?N x e" 
4552 hence "y * real c <  ?N x e" 
4509 by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="?N x e", symmetric]) 
4553 by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="?N x e", symmetric]) 
4510 hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 
4554 hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 
4511 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 
4555 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 
4512 moreover {assume y: "y > ( ?N x e) / real c" 
4556 moreover {assume y: "y > ( ?N x e) / real c" 
4513 with yu have eu: "u > ( ?N x e) / real c" by auto 
4557 with yu have eu: "u > ( ?N x e) / real c" by auto 
4514 with noSc ly yu have "( ?N x e) / real c \<le> l" by (cases "( ?N x e) / real c > l", auto) 
4558 with noSc ly yu have "( ?N x e) / real c \<le> l" by (cases "( ?N x e) / real c > l", auto) 
4515 with lx pxc have "False" by auto 
4559 with lx pxc have "False" by auto 
4516 hence ?case by simp } 
4560 hence ?case by simp } 
4517 ultimately show ?case by blast 
4561 ultimately show ?case by blast 
4518 next 
4562 next 
4519 case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp + 
4563 case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 
4520 from prems have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps) 
4564 from 6 have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps) 
4521 hence pxc: "x \<le> ( ?N x e) / real c" 
4565 hence pxc: "x \<le> ( ?N x e) / real c" 
4522 by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="?N x e"]) 
4566 by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="?N x e"]) 
4523 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4567 from 6 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4524 with ly yu have yne: "y \<noteq>  ?N x e / real c" by auto 
4568 with ly yu have yne: "y \<noteq>  ?N x e / real c" by auto 
4525 hence "y < ( ?N x e) / real c \<or> y > (?N x e) / real c" by auto 
4569 hence "y < ( ?N x e) / real c \<or> y > (?N x e) / real c" by auto 
4526 moreover {assume y: "y < (?N x e)/ real c" 
4570 moreover {assume y: "y < (?N x e)/ real c" 
4527 hence "y * real c <  ?N x e" 
4571 hence "y * real c <  ?N x e" 
4528 by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="?N x e", symmetric]) 
4572 by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="?N x e", symmetric]) 
4529 hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 
4573 hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) 
4530 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 
4574 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 
4531 moreover {assume y: "y > ( ?N x e) / real c" 
4575 moreover {assume y: "y > ( ?N x e) / real c" 
4532 with yu have eu: "u > ( ?N x e) / real c" by auto 
4576 with yu have eu: "u > ( ?N x e) / real c" by auto 
4533 with noSc ly yu have "( ?N x e) / real c \<le> l" by (cases "( ?N x e) / real c > l", auto) 
4577 with noSc ly yu have "( ?N x e) / real c \<le> l" by (cases "( ?N x e) / real c > l", auto) 
4534 with lx pxc have "False" by auto 
4578 with lx pxc have "False" by auto 
4535 hence ?case by simp } 
4579 hence ?case by simp } 
4536 ultimately show ?case by blast 
4580 ultimately show ?case by blast 
4537 next 
4581 next 
4538 case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 
4582 case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 
4539 from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps) 
4583 from 7 have "x * real c + ?N x e > 0" by (simp add: algebra_simps) 
4540 hence pxc: "x > ( ?N x e) / real c" 
4584 hence pxc: "x > ( ?N x e) / real c" 
4541 by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="?N x e"]) 
4585 by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="?N x e"]) 
4542 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4586 from 7 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4543 with ly yu have yne: "y \<noteq>  ?N x e / real c" by auto 
4587 with ly yu have yne: "y \<noteq>  ?N x e / real c" by auto 
4544 hence "y < ( ?N x e) / real c \<or> y > (?N x e) / real c" by auto 
4588 hence "y < ( ?N x e) / real c \<or> y > (?N x e) / real c" by auto 
4545 moreover {assume y: "y > (?N x e)/ real c" 
4589 moreover {assume y: "y > (?N x e)/ real c" 
4546 hence "y * real c >  ?N x e" 
4590 hence "y * real c >  ?N x e" 
4547 by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="?N x e", symmetric]) 
4591 by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="?N x e", symmetric]) 
4548 hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 
4592 hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 
4549 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 
4593 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 
4550 moreover {assume y: "y < ( ?N x e) / real c" 
4594 moreover {assume y: "y < ( ?N x e) / real c" 
4551 with ly have eu: "l < ( ?N x e) / real c" by auto 
4595 with ly have eu: "l < ( ?N x e) / real c" by auto 
4552 with noSc ly yu have "( ?N x e) / real c \<ge> u" by (cases "( ?N x e) / real c > l", auto) 
4596 with noSc ly yu have "( ?N x e) / real c \<ge> u" by (cases "( ?N x e) / real c > l", auto) 
4553 with xu pxc have "False" by auto 
4597 with xu pxc have "False" by auto 
4554 hence ?case by simp } 
4598 hence ?case by simp } 
4555 ultimately show ?case by blast 
4599 ultimately show ?case by blast 
4556 next 
4600 next 
4557 case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 
4601 case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 
4558 from prems have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps) 
4602 from 8 have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps) 
4559 hence pxc: "x \<ge> ( ?N x e) / real c" 
4603 hence pxc: "x \<ge> ( ?N x e) / real c" 
4560 by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="?N x e"]) 
4604 by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="?N x e"]) 
4561 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4605 from 8 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4562 with ly yu have yne: "y \<noteq>  ?N x e / real c" by auto 
4606 with ly yu have yne: "y \<noteq>  ?N x e / real c" by auto 
4563 hence "y < ( ?N x e) / real c \<or> y > (?N x e) / real c" by auto 
4607 hence "y < ( ?N x e) / real c \<or> y > (?N x e) / real c" by auto 
4564 moreover {assume y: "y > (?N x e)/ real c" 
4608 moreover {assume y: "y > (?N x e)/ real c" 
4565 hence "y * real c >  ?N x e" 
4609 hence "y * real c >  ?N x e" 
4566 by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="?N x e", symmetric]) 
4610 by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="?N x e", symmetric]) 
4567 hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 
4611 hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) 
4568 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 
4612 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} 
4569 moreover {assume y: "y < ( ?N x e) / real c" 
4613 moreover {assume y: "y < ( ?N x e) / real c" 
4570 with ly have eu: "l < ( ?N x e) / real c" by auto 
4614 with ly have eu: "l < ( ?N x e) / real c" by auto 
4571 with noSc ly yu have "( ?N x e) / real c \<ge> u" by (cases "( ?N x e) / real c > l", auto) 
4615 with noSc ly yu have "( ?N x e) / real c \<ge> u" by (cases "( ?N x e) / real c > l", auto) 
4572 with xu pxc have "False" by auto 
4616 with xu pxc have "False" by auto 
4573 hence ?case by simp } 
4617 hence ?case by simp } 
4574 ultimately show ?case by blast 
4618 ultimately show ?case by blast 
4575 next 
4619 next 
4576 case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 
4620 case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 
4577 from cp have cnz: "real c \<noteq> 0" by simp 
4621 from cp have cnz: "real c \<noteq> 0" by simp 
4578 from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps) 
4622 from 3 have "x * real c + ?N x e = 0" by (simp add: algebra_simps) 
4579 hence pxc: "x = ( ?N x e) / real c" 
4623 hence pxc: "x = ( ?N x e) / real c" 
4580 by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="?N x e"]) 
4624 by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="?N x e"]) 
4581 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4625 from 3 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4582 with lx xu have yne: "x \<noteq>  ?N x e / real c" by auto 
4626 with lx xu have yne: "x \<noteq>  ?N x e / real c" by auto 
4583 with pxc show ?case by simp 
4627 with pxc show ?case by simp 
4584 next 
4628 next 
4585 case (4 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ 
4629 case (4 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp_all 
4586 from cp have cnz: "real c \<noteq> 0" by simp 
4630 from cp have cnz: "real c \<noteq> 0" by simp 
4587 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4631 from 4 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> ( ?N x e) / real c" by auto 
4588 with ly yu have yne: "y \<noteq>  ?N x e / real c" by auto 
4632 with ly yu have yne: "y \<noteq>  ?N x e / real c" by auto 
4589 hence "y* real c \<noteq> ?N x e" 
4633 hence "y* real c \<noteq> ?N x e" 
4590 by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="?N x e"]) simp 
4634 by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="?N x e"]) simp 
4591 hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps) 
4635 hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps) 
4592 thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 
4636 thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 
4593 by (simp add: algebra_simps) 
4637 by (simp add: algebra_simps) 
4594 qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"]) 
4638 qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"]) 
4595 
4639 
4596 lemma rinf_\<Upsilon>: 
4640 lemma rinf_\<Upsilon>: 
4597 assumes lp: "isrlfm p" 
4641 assumes lp: "isrlfm p" 
4598 and nmi: "\<not> (Ifm (x#bs) (minusinf p))" (is "\<not> (Ifm (x#bs) (?M p))") 
4642 and nmi: "\<not> (Ifm (x#bs) (minusinf p))" (is "\<not> (Ifm (x#bs) (?M p))") 
4599 and npi: "\<not> (Ifm (x#bs) (plusinf p))" (is "\<not> (Ifm (x#bs) (?P p))") 
4643 and npi: "\<not> (Ifm (x#bs) (plusinf p))" (is "\<not> (Ifm (x#bs) (?P p))") 
4600 and ex: "\<exists> x. Ifm (x#bs) p" (is "\<exists> x. ?I x p") 
4644 and ex: "\<exists> x. Ifm (x#bs) p" (is "\<exists> x. ?I x p") 
4601 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" 
4645 shows "\<exists> (l,n) \<in> set (\<Upsilon> p). \<exists> (s,m) \<in> set (\<Upsilon> p). 

4646 ?I ((Inum (x#bs) l / real n + Inum (x#bs) s / real m) / 2) p" 
4602 proof 
4647 proof 
4603 let ?N = "\<lambda> x t. Inum (x#bs) t" 
4648 let ?N = "\<lambda> x t. Inum (x#bs) t" 
4604 let ?U = "set (\<Upsilon> p)" 
4649 let ?U = "set (\<Upsilon> p)" 
4605 from ex obtain a where pa: "?I a p" by blast 
4650 from ex obtain a where pa: "?I a p" by blast 
4606 from bound0_I[OF rminusinf_bound0[OF lp], where bs="bs" and b="x" and b'="a"] nmi 
4651 from bound0_I[OF rminusinf_bound0[OF lp], where bs="bs" and b="x" and b'="a"] nmi 