src/HOL/Decision_Procs/MIR.thy
changeset 41891 d37babdf5cae
parent 41882 ae8d62656392
child 44013 5cfc1c36ae97
equal deleted inserted replaced
41890:550a8ecffe0c 41891:d37babdf5cae
  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)
  1862   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1862   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1863   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1863   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1864   let ?N = "\<lambda> t. Inum (real i#bs) t"
  1864   let ?N = "\<lambda> t. Inum (real i#bs) t"
  1865   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
  1865   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
  1866   moreover
  1866   moreover
  1867   {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 
  1867   { assume j: "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 
  1868     hence ?case using prems by (simp del: zlfm.simps add: rdvd_left_0_eq)}
  1868     hence ?case using 11 j by (simp del: zlfm.simps add: rdvd_left_0_eq)}
  1869   moreover
  1869   moreover
  1870   {assume "?c=0" and "j\<noteq>0" hence ?case 
  1870   {assume "?c=0" and "j\<noteq>0" hence ?case 
  1871       using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"]
  1871       using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"]
  1872       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
  1872       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
  1873   moreover
  1873   moreover
  1908   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1908   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1909   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1909   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1910   let ?N = "\<lambda> t. Inum (real i#bs) t"
  1910   let ?N = "\<lambda> t. Inum (real i#bs) t"
  1911   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
  1911   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
  1912   moreover
  1912   moreover
  1913   {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 
  1913   {assume j: "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 
  1914     hence ?case using prems by (simp del: zlfm.simps add: rdvd_left_0_eq)}
  1914     hence ?case using 12 j by (simp del: zlfm.simps add: rdvd_left_0_eq)}
  1915   moreover
  1915   moreover
  1916   {assume "?c=0" and "j\<noteq>0" hence ?case 
  1916   {assume "?c=0" and "j\<noteq>0" hence ?case 
  1917       using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"]
  1917       using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"]
  1918       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
  1918       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
  1919   moreover
  1919   moreover
  2010   shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0"
  2010   shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0"
  2011 using lin
  2011 using lin
  2012 proof (induct p rule: iszlfm.induct)
  2012 proof (induct p rule: iszlfm.induct)
  2013   case (1 p q) 
  2013   case (1 p q) 
  2014   let ?d = "\<delta> (And p q)"
  2014   let ?d = "\<delta> (And p q)"
  2015   from prems lcm_pos_int have dp: "?d >0" by simp
  2015   from 1 lcm_pos_int have dp: "?d >0" by simp
  2016   have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp 
  2016   have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp 
  2017    hence th: "d\<delta> p ?d" 
  2017   hence th: "d\<delta> p ?d" 
  2018      using delta_mono prems by(simp only: iszlfm.simps) blast
  2018     using delta_mono 1 by (simp only: iszlfm.simps) blast
  2019   have "\<delta> q dvd \<delta> (And p q)" using prems  by simp 
  2019   have "\<delta> q dvd \<delta> (And p q)" using 1 by simp 
  2020   hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast
  2020   hence th': "d\<delta> q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast
  2021   from th th' dp show ?case by simp 
  2021   from th th' dp show ?case by simp 
  2022 next
  2022 next
  2023   case (2 p q)  
  2023   case (2 p q)  
  2024   let ?d = "\<delta> (And p q)"
  2024   let ?d = "\<delta> (And p q)"
  2025   from prems lcm_pos_int have dp: "?d >0" by simp
  2025   from 2 lcm_pos_int have dp: "?d >0" by simp
  2026   have "\<delta> p dvd \<delta> (And p q)" using prems by simp hence th: "d\<delta> p ?d" using delta_mono prems 
  2026   have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
  2027     by(simp only: iszlfm.simps) blast
  2027   hence th: "d\<delta> p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
  2028   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
  2028   have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
       
  2029   hence th': "d\<delta> q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
  2029   from th th' dp show ?case by simp
  2030   from th th' dp show ?case by simp
  2030 qed simp_all
  2031 qed simp_all
  2031 
  2032 
  2032 
  2033 
  2033 lemma minusinf_inf:
  2034 lemma minusinf_inf:
  2035   shows "\<exists> (z::int). \<forall> x < z. Ifm ((real x)#bs) (minusinf p) = Ifm ((real x)#bs) p"
  2036   shows "\<exists> (z::int). \<forall> x < z. Ifm ((real x)#bs) (minusinf p) = Ifm ((real x)#bs) p"
  2036   (is "?P p" is "\<exists> (z::int). \<forall> x < z. ?I x (?M p) = ?I x p")
  2037   (is "?P p" is "\<exists> (z::int). \<forall> x < z. ?I x (?M p) = ?I x p")
  2037 using linp
  2038 using linp
  2038 proof (induct p rule: minusinf.induct)
  2039 proof (induct p rule: minusinf.induct)
  2039   case (1 f g)
  2040   case (1 f g)
  2040   from prems have "?P f" by simp
  2041   then have "?P f" by simp
  2041   then obtain z1 where z1_def: "\<forall> x < z1. ?I x (?M f) = ?I x f" by blast
  2042   then obtain z1 where z1_def: "\<forall> x < z1. ?I x (?M f) = ?I x f" by blast
  2042   from prems have "?P g" by simp
  2043   with 1 have "?P g" by simp
  2043   then obtain z2 where z2_def: "\<forall> x < z2. ?I x (?M g) = ?I x g" by blast
  2044   then obtain z2 where z2_def: "\<forall> x < z2. ?I x (?M g) = ?I x g" by blast
  2044   let ?z = "min z1 z2"
  2045   let ?z = "min z1 z2"
  2045   from z1_def z2_def have "\<forall> x < ?z. ?I x (?M (And f g)) = ?I x (And f g)" by simp
  2046   from z1_def z2_def have "\<forall> x < ?z. ?I x (?M (And f g)) = ?I x (And f g)" by simp
  2046   thus ?case by blast
  2047   thus ?case by blast
  2047 next
  2048 next
  2048   case (2 f g)   from prems have "?P f" by simp
  2049   case (2 f g)
       
  2050   then have "?P f" by simp
  2049   then obtain z1 where z1_def: "\<forall> x < z1. ?I x (?M f) = ?I x f" by blast
  2051   then obtain z1 where z1_def: "\<forall> x < z1. ?I x (?M f) = ?I x f" by blast
  2050   from prems have "?P g" by simp
  2052   with 2 have "?P g" by simp
  2051   then obtain z2 where z2_def: "\<forall> x < z2. ?I x (?M g) = ?I x g" by blast
  2053   then obtain z2 where z2_def: "\<forall> x < z2. ?I x (?M g) = ?I x g" by blast
  2052   let ?z = "min z1 z2"
  2054   let ?z = "min z1 z2"
  2053   from z1_def z2_def have "\<forall> x < ?z. ?I x (?M (Or f g)) = ?I x (Or f g)" by simp
  2055   from z1_def z2_def have "\<forall> x < ?z. ?I x (?M (Or f g)) = ?I x (Or f g)" by simp
  2054   thus ?case by blast
  2056   thus ?case by blast
  2055 next
  2057 next
  2056   case (3 c e) 
  2058   case (3 c e) 
  2057   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2059   then have "c > 0" by simp
  2058   from prems have nbe: "numbound0 e" by simp
  2060   hence rcpos: "real c > 0" by simp
       
  2061   from 3 have nbe: "numbound0 e" by simp
  2059   fix y
  2062   fix y
  2060   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))"
  2063   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))"
  2061   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2064   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2062     fix x
  2065     fix x
  2063     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2066     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2069       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
  2072       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
  2070   qed
  2073   qed
  2071   thus ?case by blast
  2074   thus ?case by blast
  2072 next
  2075 next
  2073   case (4 c e) 
  2076   case (4 c e) 
  2074   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2077   then have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2075   from prems have nbe: "numbound0 e" by simp
  2078   from 4 have nbe: "numbound0 e" by simp
  2076   fix y
  2079   fix y
  2077   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))"
  2080   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))"
  2078   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2081   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2079     fix x
  2082     fix x
  2080     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2083     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2086       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
  2089       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
  2087   qed
  2090   qed
  2088   thus ?case by blast
  2091   thus ?case by blast
  2089 next
  2092 next
  2090   case (5 c e) 
  2093   case (5 c e) 
  2091   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2094   then have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2092   from prems have nbe: "numbound0 e" by simp
  2095   from 5 have nbe: "numbound0 e" by simp
  2093   fix y
  2096   fix y
  2094   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))"
  2097   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))"
  2095   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2098   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2096     fix x
  2099     fix x
  2097     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2100     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2102       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
  2105       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
  2103   qed
  2106   qed
  2104   thus ?case by blast
  2107   thus ?case by blast
  2105 next
  2108 next
  2106   case (6 c e) 
  2109   case (6 c e) 
  2107   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2110   then have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2108   from prems have nbe: "numbound0 e" by simp
  2111   from 6 have nbe: "numbound0 e" by simp
  2109   fix y
  2112   fix y
  2110   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))"
  2113   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))"
  2111   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2114   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2112     fix x
  2115     fix x
  2113     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2116     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2118       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
  2121       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
  2119   qed
  2122   qed
  2120   thus ?case by blast
  2123   thus ?case by blast
  2121 next
  2124 next
  2122   case (7 c e) 
  2125   case (7 c e) 
  2123   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2126   then have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2124   from prems have nbe: "numbound0 e" by simp
  2127   from 7 have nbe: "numbound0 e" by simp
  2125   fix y
  2128   fix y
  2126   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))"
  2129   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))"
  2127   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2130   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2128     fix x
  2131     fix x
  2129     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2132     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2134       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
  2137       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
  2135   qed
  2138   qed
  2136   thus ?case by blast
  2139   thus ?case by blast
  2137 next
  2140 next
  2138   case (8 c e) 
  2141   case (8 c e) 
  2139   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2142   then have "c > 0" by simp hence rcpos: "real c > 0" by simp
  2140   from prems have nbe: "numbound0 e" by simp
  2143   from 8 have nbe: "numbound0 e" by simp
  2141   fix y
  2144   fix y
  2142   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))"
  2145   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))"
  2143   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2146   proof (simp add: less_floor_eq , rule allI, rule impI) 
  2144     fix x
  2147     fix x
  2145     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2148     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
  2334 proof(induct p rule: iszlfm.induct)
  2337 proof(induct p rule: iszlfm.induct)
  2335   case (9 j c e)
  2338   case (9 j c e)
  2336   have th: "(real j rdvd real c * real x - Inum (real x # bs) e) =
  2339   have th: "(real j rdvd real c * real x - Inum (real x # bs) e) =
  2337        (real j rdvd - (real c * real x - Inum (real x # bs) e))"
  2340        (real j rdvd - (real c * real x - Inum (real x # bs) e))"
  2338     by (simp only: rdvd_minus[symmetric])
  2341     by (simp only: rdvd_minus[symmetric])
  2339   from prems th show  ?case
  2342   from 9 th show ?case
  2340     by (simp add: algebra_simps
  2343     by (simp add: algebra_simps
  2341       numbound0_I[where bs="bs" and b'="real x" and b="- real x"])
  2344       numbound0_I[where bs="bs" and b'="real x" and b="- real x"])
  2342 next
  2345 next
  2343     case (10 j c e)
  2346   case (10 j c e)
  2344   have th: "(real j rdvd real c * real x - Inum (real x # bs) e) =
  2347   have th: "(real j rdvd real c * real x - Inum (real x # bs) e) =
  2345        (real j rdvd - (real c * real x - Inum (real x # bs) e))"
  2348        (real j rdvd - (real c * real x - Inum (real x # bs) e))"
  2346     by (simp only: rdvd_minus[symmetric])
  2349     by (simp only: rdvd_minus[symmetric])
  2347   from prems th show  ?case
  2350   from 10 th show  ?case
  2348     by (simp add: algebra_simps
  2351     by (simp add: algebra_simps
  2349       numbound0_I[where bs="bs" and b'="real x" and b="- real x"])
  2352       numbound0_I[where bs="bs" and b'="real x" and b="- real x"])
  2350 qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"])
  2353 qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"])
  2351 
  2354 
  2352 lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"
  2355 lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"
  2394   assumes linp: "iszlfm p (a #bs)"
  2397   assumes linp: "iszlfm p (a #bs)"
  2395   shows "\<zeta> p > 0 \<and> d\<beta> p (\<zeta> p)"
  2398   shows "\<zeta> p > 0 \<and> d\<beta> p (\<zeta> p)"
  2396 using linp
  2399 using linp
  2397 proof(induct p rule: iszlfm.induct)
  2400 proof(induct p rule: iszlfm.induct)
  2398   case (1 p q)
  2401   case (1 p q)
  2399   from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  2402   then  have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  2400   from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  2403   from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  2401   from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  2404   from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  2402     d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  2405     d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  2403     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
  2406     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
  2404 next
  2407 next
  2405   case (2 p q)
  2408   case (2 p q)
  2406   from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  2409   then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  2407   from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  2410   from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  2408   from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  2411   from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  2409     d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  2412     d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  2410     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
  2413     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
  2411 qed (auto simp add: lcm_pos_int)
  2414 qed (auto simp add: lcm_pos_int)
  2412 
  2415 
  2413 lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"
  2416 lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"
  2575   and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). real x = b + real j)"
  2578   and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). real x = b + real j)"
  2576   and p: "Ifm (real x#bs) p" (is "?P x")
  2579   and p: "Ifm (real x#bs) p" (is "?P x")
  2577   shows "?P (x - d)"
  2580   shows "?P (x - d)"
  2578 using lp u d dp nob p
  2581 using lp u d dp nob p
  2579 proof(induct p rule: iszlfm.induct)
  2582 proof(induct p rule: iszlfm.induct)
  2580   case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
  2583   case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp_all
  2581     with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] prems
  2584   with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] 5
  2582     show ?case by (simp del: real_of_int_minus)
  2585   show ?case by (simp del: real_of_int_minus)
  2583 next
  2586 next
  2584   case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
  2587   case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp_all
  2585     with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] prems
  2588   with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] 6
  2586     show ?case by (simp del: real_of_int_minus)
  2589   show ?case by (simp del: real_of_int_minus)
  2587 next
  2590 next
  2588   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+
  2591   case (7 c e) hence p: "Ifm (real x #bs) (Gt (CN 0 c e))" and c1: "c=1"
  2589     let ?e = "Inum (real x # bs) e"
  2592     and bn:"numbound0 e" and ie1:"isint e (a#bs)" using dvd1_eq1[where x="c"] by simp_all
  2590     from ie1 have ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="a#bs"]
  2593   let ?e = "Inum (real x # bs) e"
       
  2594   from ie1 have ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="a#bs"]
  2591       numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]
  2595       numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]
  2592       by (simp add: isint_iff)
  2596     by (simp add: isint_iff)
  2593     {assume "real (x-d) +?e > 0" hence ?case using c1 
  2597     {assume "real (x-d) +?e > 0" hence ?case using c1 
  2594       numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"]
  2598       numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"]
  2595         by (simp del: real_of_int_minus)}
  2599         by (simp del: real_of_int_minus)}
  2596     moreover
  2600     moreover
  2597     {assume H: "\<not> real (x-d) + ?e > 0" 
  2601     {assume H: "\<not> real (x-d) + ?e > 0" 
  2598       let ?v="Neg e"
  2602       let ?v="Neg e"
  2599       have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
  2603       have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
  2600       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"]] 
  2604       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"]] 
  2601       have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x =  - ?e + real j)" by auto 
  2605       have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x =  - ?e + real j)" by auto 
  2602       from H p have "real x + ?e > 0 \<and> real x + ?e \<le> real d" by (simp add: c1)
  2606       from H p have "real x + ?e > 0 \<and> real x + ?e \<le> real d" by (simp add: c1)
  2603       hence "real (x + floor ?e) > real (0::int) \<and> real (x + floor ?e) \<le> real d"
  2607       hence "real (x + floor ?e) > real (0::int) \<and> real (x + floor ?e) \<le> real d"
  2604         using ie by simp
  2608         using ie by simp
  2605       hence "x + floor ?e \<ge> 1 \<and> x + floor ?e \<le> d"  by simp
  2609       hence "x + floor ?e \<ge> 1 \<and> x + floor ?e \<le> d"  by simp
  2621         by (simp del: real_of_int_minus)}
  2625         by (simp del: real_of_int_minus)}
  2622     moreover
  2626     moreover
  2623     {assume H: "\<not> real (x-d) + ?e \<ge> 0" 
  2627     {assume H: "\<not> real (x-d) + ?e \<ge> 0" 
  2624       let ?v="Sub (C -1) e"
  2628       let ?v="Sub (C -1) e"
  2625       have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
  2629       have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
  2626       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"]] 
  2630       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"]] 
  2627       have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x =  - ?e - 1 + real j)" by auto 
  2631       have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x =  - ?e - 1 + real j)" by auto 
  2628       from H p have "real x + ?e \<ge> 0 \<and> real x + ?e < real d" by (simp add: c1)
  2632       from H p have "real x + ?e \<ge> 0 \<and> real x + ?e < real d" by (simp add: c1)
  2629       hence "real (x + floor ?e) \<ge> real (0::int) \<and> real (x + floor ?e) < real d"
  2633       hence "real (x + floor ?e) \<ge> real (0::int) \<and> real (x + floor ?e) < real d"
  2630         using ie by simp
  2634         using ie by simp
  2631       hence "x + floor ?e +1 \<ge> 1 \<and> x + floor ?e + 1 \<le> d"  by simp
  2635       hence "x + floor ?e +1 \<ge> 1 \<and> x + floor ?e + 1 \<le> d"  by simp
  2641   case (3 c e) hence p: "Ifm (real x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" 
  2645   case (3 c e) hence p: "Ifm (real x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" 
  2642     and bn:"numbound0 e" and ie1: "isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+
  2646     and bn:"numbound0 e" and ie1: "isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+
  2643     let ?e = "Inum (real x # bs) e"
  2647     let ?e = "Inum (real x # bs) e"
  2644     let ?v="(Sub (C -1) e)"
  2648     let ?v="(Sub (C -1) e)"
  2645     have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
  2649     have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
  2646     from p have "real x= - ?e" by (simp add: c1) with prems(11) show ?case using dp
  2650     from p have "real x= - ?e" by (simp add: c1) with 3(5) show ?case using dp
  2647       by simp (erule ballE[where x="1"],
  2651       by simp (erule ballE[where x="1"],
  2648         simp_all add:algebra_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"])
  2652         simp_all add:algebra_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"])
  2649 next
  2653 next
  2650   case (4 c e)hence p: "Ifm (real x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" 
  2654   case (4 c e)hence p: "Ifm (real x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" 
  2651     and bn:"numbound0 e" and ie1: "isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+
  2655     and bn:"numbound0 e" and ie1: "isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+
  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 (x-d + floor ?e)",symmetric, simplified]
  2682     using int_rdvd_real[where i="j" and x="real (x-d + 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 (x-d)" and b'="real x" and bs="bs"] c1 p by simp
  2687     using numbound0_I[OF bn,where b="real (x-d)" 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 (x-d + floor ?e)",symmetric, simplified]
  2701     using int_rdvd_real[where i="j" and x="real (x-d + 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 (x-d)" 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 (x-d)" 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
  3052     from mult_strict_left_mono[OF dp cp] have d: "(c*d) \<in> {1 .. c*d}" by simp
  3092     from mult_strict_left_mono[OF dp cp] have d: "(c*d) \<in> {1 .. c*d}" by simp
  3053     from nob[rule_format, where j="c*d", OF d] pi have ?case by simp }
  3093     from nob[rule_format, where j="c*d", OF d] pi have ?case by simp }
  3054   ultimately show ?case by blast
  3094   ultimately show ?case by blast
  3055 next
  3095 next
  3056   case (5 c e) hence cp: "c > 0" by simp
  3096   case (5 c e) hence cp: "c > 0" by simp
  3057   from prems mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 
  3097   from 5 mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 
  3058     real_of_int_mult]
  3098     real_of_int_mult]
  3059   show ?case using prems dp 
  3099   show ?case using 5 dp 
  3060     by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
  3100     by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
  3061       algebra_simps)
  3101       algebra_simps)
  3062 next
  3102 next
  3063   case (6 c e)  hence cp: "c > 0" by simp
  3103   case (6 c e) hence cp: "c > 0" by simp
  3064   from prems mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 
  3104   from 6 mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 
  3065     real_of_int_mult]
  3105     real_of_int_mult]
  3066   show ?case using prems dp 
  3106   show ?case using 6 dp 
  3067     by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
  3107     by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
  3068       algebra_simps)
  3108       algebra_simps)
  3069 next
  3109 next
  3070   case (7 c e) hence cp: "c >0" and nb: "numbound0 e" and ei: "isint e (real i#bs)"
  3110   case (7 c e) hence cp: "c >0" and nb: "numbound0 e" and ei: "isint e (real i#bs)"
  3071     and nob: "\<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> - ?N i e + real j"
  3111     and nob: "\<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> - ?N i e + real j"
  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")
  3450 lemma rsplit0_complete:
  3493 lemma rsplit0_complete:
  3451   assumes xp:"0 \<le> x" and x1:"x < 1"
  3494   assumes xp:"0 \<le> x" and x1:"x < 1"
  3452   shows "\<exists> (p,n,s) \<in> set (rsplit0 t). Ifm (x#bs) p" (is "\<exists> (p,n,s) \<in> ?SS t. ?I p")
  3495   shows "\<exists> (p,n,s) \<in> set (rsplit0 t). Ifm (x#bs) p" (is "\<exists> (p,n,s) \<in> ?SS t. ?I p")
  3453 proof(induct t rule: rsplit0.induct)
  3496 proof(induct t rule: rsplit0.induct)
  3454   case (2 a b) 
  3497   case (2 a b) 
  3455   from prems have "\<exists> (pa,na,sa) \<in> ?SS a. ?I pa" by auto
  3498   then have "\<exists> (pa,na,sa) \<in> ?SS a. ?I pa" by auto
  3456   then obtain "pa" "na" "sa" where pa: "(pa,na,sa)\<in> ?SS a \<and> ?I pa" by blast
  3499   then obtain "pa" "na" "sa" where pa: "(pa,na,sa)\<in> ?SS a \<and> ?I pa" by blast
  3457   from prems have "\<exists> (pb,nb,sb) \<in> ?SS b. ?I pb" by blast
  3500   with 2 have "\<exists> (pb,nb,sb) \<in> ?SS b. ?I pb" by blast
  3458   then obtain "pb" "nb" "sb" where pb: "(pb,nb,sb)\<in> ?SS b \<and> ?I pb" by blast
  3501   then obtain "pb" "nb" "sb" where pb: "(pb,nb,sb)\<in> ?SS b \<and> ?I pb" by blast
  3459   from pa pb have th: "((pa,na,sa),(pb,nb,sb)) \<in> set[(x,y). x\<leftarrow>rsplit0 a, y\<leftarrow>rsplit0 b]"
  3502   from pa pb have th: "((pa,na,sa),(pb,nb,sb)) \<in> set[(x,y). x\<leftarrow>rsplit0 a, y\<leftarrow>rsplit0 b]"
  3460     by (auto)
  3503     by (auto)
  3461   let ?f="(\<lambda> ((p,n,t),(q,m,s)). (And p q, n+m, Add t s))"
  3504   let ?f="(\<lambda> ((p,n,t),(q,m,s)). (And p q, n+m, Add t s))"
  3462   from imageI[OF th, where f="?f"] have "?f ((pa,na,sa),(pb,nb,sb)) \<in> ?SS (Add a b)"
  3505   from imageI[OF th, where f="?f"] have "?f ((pa,na,sa),(pb,nb,sb)) \<in> ?SS (Add a b)"
  3513     (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
  3556     (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
  3514   finally 
  3557   finally 
  3515   have FS: "?SS (Floor a) =   
  3558   have FS: "?SS (Floor a) =   
  3516     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
  3559     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
  3517     (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 
  3560     (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 
  3518     (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
  3561     (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}})))"
  3519   from prems have "\<exists> (p,n,s) \<in> ?SS a. ?I p" by auto
  3562     by blast
       
  3563   from 5 have "\<exists> (p,n,s) \<in> ?SS a. ?I p" by auto
  3520   then obtain "p" "n" "s" where pns: "(p,n,s) \<in> ?SS a \<and> ?I p" by blast
  3564   then obtain "p" "n" "s" where pns: "(p,n,s) \<in> ?SS a \<and> ?I p" by blast
  3521   let ?N = "\<lambda> t. Inum (x#bs) t"
  3565   let ?N = "\<lambda> t. Inum (x#bs) t"
  3522   from rsplit0_cs[rule_format] pns have ans:"(?N a = ?N (CN 0 n s)) \<and> numbound0 s \<and> isrlfm p"
  3566   from rsplit0_cs[rule_format] pns have ans:"(?N a = ?N (CN 0 n s)) \<and> numbound0 s \<and> isrlfm p"
  3523     by auto
  3567     by auto
  3524   
  3568   
  3931   {assume "bound0 (Lt a)" hence bn:"bound0 (simpfm (Lt a))"  
  3975   {assume "bound0 (Lt a)" hence bn:"bound0 (simpfm (Lt a))"  
  3932       using simpfm_bound0 by blast
  3976       using simpfm_bound0 by blast
  3933     have "isatom (simpfm (Lt a))" by (cases "simpnum a", auto simp add: Let_def)
  3977     have "isatom (simpfm (Lt a))" by (cases "simpnum a", auto simp add: Let_def)
  3934     with bn bound0at_l have ?case by blast}
  3978     with bn bound0at_l have ?case by blast}
  3935   moreover 
  3979   moreover 
  3936   {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e"
  3980   { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e"
  3937     {
  3981     { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
  3938       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
       
  3939       with numgcd_pos[where t="CN 0 c (simpnum e)"]
  3982       with numgcd_pos[where t="CN 0 c (simpnum e)"]
  3940       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
  3983       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
  3941       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
  3984       from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
  3942         by (simp add: numgcd_def)
  3985         by (simp add: numgcd_def)
  3943       from prems have th': "c\<noteq>0" by auto
  3986       from `c > 0` have th': "c\<noteq>0" by auto
  3944       from prems have cp: "c \<ge> 0" by simp
  3987       from `c > 0` have cp: "c \<ge> 0" by simp
  3945       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
  3988       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
  3946         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
  3989       have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
  3947     }
  3990     }
  3948     with prems have ?case
  3991     with Lt a have ?case
  3949       by (simp add: Let_def reducecoeff_def reducecoeffh_numbound0)}
  3992       by (simp add: Let_def reducecoeff_def reducecoeffh_numbound0)}
  3950   ultimately show ?case by blast
  3993   ultimately show ?case by blast
  3951 next
  3994 next
  3952   case (Le a)   
  3995   case (Le a)   
  3953   hence "bound0 (Le a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
  3996   hence "bound0 (Le a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
  3954     by (cases a,simp_all, case_tac "nat", simp_all)
  3997     by (cases a,simp_all, case_tac "nat", simp_all)
  3955   moreover
  3998   moreover
  3956   {assume "bound0 (Le a)" hence bn:"bound0 (simpfm (Le a))"  
  3999   { assume "bound0 (Le a)" hence bn:"bound0 (simpfm (Le a))"  
  3957       using simpfm_bound0 by blast
  4000       using simpfm_bound0 by blast
  3958     have "isatom (simpfm (Le a))" by (cases "simpnum a", auto simp add: Let_def)
  4001     have "isatom (simpfm (Le a))" by (cases "simpnum a", auto simp add: Let_def)
  3959     with bn bound0at_l have ?case by blast}
  4002     with bn bound0at_l have ?case by blast}
  3960   moreover 
  4003   moreover 
  3961   {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e"
  4004   { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e"
  3962     {
  4005     { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
  3963       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
       
  3964       with numgcd_pos[where t="CN 0 c (simpnum e)"]
  4006       with numgcd_pos[where t="CN 0 c (simpnum e)"]
  3965       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
  4007       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
  3966       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
  4008       from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
  3967         by (simp add: numgcd_def)
  4009         by (simp add: numgcd_def)
  3968       from prems have th': "c\<noteq>0" by auto
  4010       from `c > 0` have th': "c\<noteq>0" by auto
  3969       from prems have cp: "c \<ge> 0" by simp
  4011       from `c > 0` have cp: "c \<ge> 0" by simp
  3970       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
  4012       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
  3971         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
  4013       have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
  3972     }
  4014     }
  3973     with prems have ?case
  4015     with Le a have ?case
  3974       by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)}
  4016       by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)}
  3975   ultimately show ?case by blast
  4017   ultimately show ?case by blast
  3976 next
  4018 next
  3977   case (Gt a)   
  4019   case (Gt a)   
  3978   hence "bound0 (Gt a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
  4020   hence "bound0 (Gt a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
  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)"
  4056   {assume "bound0 (NEq a)" hence bn:"bound0 (simpfm (NEq a))"  
  4095   {assume "bound0 (NEq a)" hence bn:"bound0 (simpfm (NEq a))"  
  4057       using simpfm_bound0 by blast
  4096       using simpfm_bound0 by blast
  4058     have "isatom (simpfm (NEq a))" by (cases "simpnum a", auto simp add: Let_def)
  4097     have "isatom (simpfm (NEq a))" by (cases "simpnum a", auto simp add: Let_def)
  4059     with bn bound0at_l have ?case by blast}
  4098     with bn bound0at_l have ?case by blast}
  4060   moreover 
  4099   moreover 
  4061   {fix c e assume "a = CN 0 c e" and "c>0" and "numbound0 e"
  4100   { fix c e assume a: "a = CN 0 c e" and "c>0" and "numbound0 e"
  4062     {
  4101     { assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
  4063       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
       
  4064       with numgcd_pos[where t="CN 0 c (simpnum e)"]
  4102       with numgcd_pos[where t="CN 0 c (simpnum e)"]
  4065       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
  4103       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
  4066       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
  4104       from `c > 0` have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
  4067         by (simp add: numgcd_def)
  4105         by (simp add: numgcd_def)
  4068       from prems have th': "c\<noteq>0" by auto
  4106       from `c > 0` have th': "c\<noteq>0" by auto
  4069       from prems have cp: "c \<ge> 0" by simp
  4107       from `c > 0` have cp: "c \<ge> 0" by simp
  4070       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
  4108       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
  4071         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
  4109       have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
  4072     }
  4110     }
  4073     with prems have ?case
  4111     with NEq a have ?case
  4074       by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)}
  4112       by (simp add: Let_def reducecoeff_def simpnum_numbound0 reducecoeffh_numbound0)}
  4075   ultimately show ?case by blast
  4113   ultimately show ?case by blast
  4076 next
  4114 next
  4077   case (Dvd i a) hence "bound0 (Dvd i a)" by auto hence bn:"bound0 (simpfm (Dvd i a))"  
  4115   case (Dvd i a) hence "bound0 (Dvd i a)" by auto hence bn:"bound0 (simpfm (Dvd i a))"  
  4078     using simpfm_bound0 by blast
  4116     using simpfm_bound0 by blast
  4109   case (1 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto
  4147   case (1 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto
  4110 next
  4148 next
  4111   case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto
  4149   case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto
  4112 next
  4150 next
  4113   case (3 c e) 
  4151   case (3 c e) 
  4114   from prems have nb: "numbound0 e" by simp
  4152   from 3 have nb: "numbound0 e" by simp
  4115   from prems have cp: "real c > 0" by simp
  4153   from 3 have cp: "real c > 0" by simp
  4116   fix a
  4154   fix a
  4117   let ?e="Inum (a#bs) e"
  4155   let ?e="Inum (a#bs) e"
  4118   let ?z = "(- ?e) / real c"
  4156   let ?z = "(- ?e) / real c"
  4119   {fix x
  4157   {fix x
  4120     assume xz: "x < ?z"
  4158     assume xz: "x < ?z"
  4126       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp  }
  4164       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp  }
  4127   hence "\<forall> x < ?z. ?P ?z x (Eq (CN 0 c e))" by simp
  4165   hence "\<forall> x < ?z. ?P ?z x (Eq (CN 0 c e))" by simp
  4128   thus ?case by blast
  4166   thus ?case by blast
  4129 next
  4167 next
  4130   case (4 c e)   
  4168   case (4 c e)   
  4131   from prems have nb: "numbound0 e" by simp
  4169   from 4 have nb: "numbound0 e" by simp
  4132   from prems have cp: "real c > 0" by simp
  4170   from 4 have cp: "real c > 0" by simp
  4133   fix a
  4171   fix a
  4134   let ?e="Inum (a#bs) e"
  4172   let ?e="Inum (a#bs) e"
  4135   let ?z = "(- ?e) / real c"
  4173   let ?z = "(- ?e) / real c"
  4136   {fix x
  4174   {fix x
  4137     assume xz: "x < ?z"
  4175     assume xz: "x < ?z"
  4143       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4181       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4144   hence "\<forall> x < ?z. ?P ?z x (NEq (CN 0 c e))" by simp
  4182   hence "\<forall> x < ?z. ?P ?z x (NEq (CN 0 c e))" by simp
  4145   thus ?case by blast
  4183   thus ?case by blast
  4146 next
  4184 next
  4147   case (5 c e) 
  4185   case (5 c e) 
  4148     from prems have nb: "numbound0 e" by simp
  4186   from 5 have nb: "numbound0 e" by simp
  4149   from prems have cp: "real c > 0" by simp
  4187   from 5 have cp: "real c > 0" by simp
  4150   fix a
  4188   fix a
  4151   let ?e="Inum (a#bs) e"
  4189   let ?e="Inum (a#bs) e"
  4152   let ?z = "(- ?e) / real c"
  4190   let ?z = "(- ?e) / real c"
  4153   {fix x
  4191   {fix x
  4154     assume xz: "x < ?z"
  4192     assume xz: "x < ?z"
  4159       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]  by simp }
  4197       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]  by simp }
  4160   hence "\<forall> x < ?z. ?P ?z x (Lt (CN 0 c e))" by simp
  4198   hence "\<forall> x < ?z. ?P ?z x (Lt (CN 0 c e))" by simp
  4161   thus ?case by blast
  4199   thus ?case by blast
  4162 next
  4200 next
  4163   case (6 c e)  
  4201   case (6 c e)  
  4164     from prems have nb: "numbound0 e" by simp
  4202   from 6 have nb: "numbound0 e" by simp
  4165   from prems have cp: "real c > 0" by simp
  4203   from 6 have cp: "real c > 0" by simp
  4166   fix a
  4204   fix a
  4167   let ?e="Inum (a#bs) e"
  4205   let ?e="Inum (a#bs) e"
  4168   let ?z = "(- ?e) / real c"
  4206   let ?z = "(- ?e) / real c"
  4169   {fix x
  4207   {fix x
  4170     assume xz: "x < ?z"
  4208     assume xz: "x < ?z"
  4175       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4213       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4176   hence "\<forall> x < ?z. ?P ?z x (Le (CN 0 c e))" by simp
  4214   hence "\<forall> x < ?z. ?P ?z x (Le (CN 0 c e))" by simp
  4177   thus ?case by blast
  4215   thus ?case by blast
  4178 next
  4216 next
  4179   case (7 c e)  
  4217   case (7 c e)  
  4180     from prems have nb: "numbound0 e" by simp
  4218   from 7 have nb: "numbound0 e" by simp
  4181   from prems have cp: "real c > 0" by simp
  4219   from 7 have cp: "real c > 0" by simp
  4182   fix a
  4220   fix a
  4183   let ?e="Inum (a#bs) e"
  4221   let ?e="Inum (a#bs) e"
  4184   let ?z = "(- ?e) / real c"
  4222   let ?z = "(- ?e) / real c"
  4185   {fix x
  4223   {fix x
  4186     assume xz: "x < ?z"
  4224     assume xz: "x < ?z"
  4191       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4229       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4192   hence "\<forall> x < ?z. ?P ?z x (Gt (CN 0 c e))" by simp
  4230   hence "\<forall> x < ?z. ?P ?z x (Gt (CN 0 c e))" by simp
  4193   thus ?case by blast
  4231   thus ?case by blast
  4194 next
  4232 next
  4195   case (8 c e)  
  4233   case (8 c e)  
  4196     from prems have nb: "numbound0 e" by simp
  4234   from 8 have nb: "numbound0 e" by simp
  4197   from prems have cp: "real c > 0" by simp
  4235   from 8 have cp: "real c > 0" by simp
  4198   fix a
  4236   fix a
  4199   let ?e="Inum (a#bs) e"
  4237   let ?e="Inum (a#bs) e"
  4200   let ?z = "(- ?e) / real c"
  4238   let ?z = "(- ?e) / real c"
  4201   {fix x
  4239   {fix x
  4202     assume xz: "x < ?z"
  4240     assume xz: "x < ?z"
  4217   case (1 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto
  4255   case (1 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto
  4218 next
  4256 next
  4219   case (2 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto
  4257   case (2 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto
  4220 next
  4258 next
  4221   case (3 c e) 
  4259   case (3 c e) 
  4222   from prems have nb: "numbound0 e" by simp
  4260   from 3 have nb: "numbound0 e" by simp
  4223   from prems have cp: "real c > 0" by simp
  4261   from 3 have cp: "real c > 0" by simp
  4224   fix a
  4262   fix a
  4225   let ?e="Inum (a#bs) e"
  4263   let ?e="Inum (a#bs) e"
  4226   let ?z = "(- ?e) / real c"
  4264   let ?z = "(- ?e) / real c"
  4227   {fix x
  4265   {fix x
  4228     assume xz: "x > ?z"
  4266     assume xz: "x > ?z"
  4234       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4272       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4235   hence "\<forall> x > ?z. ?P ?z x (Eq (CN 0 c e))" by simp
  4273   hence "\<forall> x > ?z. ?P ?z x (Eq (CN 0 c e))" by simp
  4236   thus ?case by blast
  4274   thus ?case by blast
  4237 next
  4275 next
  4238   case (4 c e) 
  4276   case (4 c e) 
  4239   from prems have nb: "numbound0 e" by simp
  4277   from 4 have nb: "numbound0 e" by simp
  4240   from prems have cp: "real c > 0" by simp
  4278   from 4 have cp: "real c > 0" by simp
  4241   fix a
  4279   fix a
  4242   let ?e="Inum (a#bs) e"
  4280   let ?e="Inum (a#bs) e"
  4243   let ?z = "(- ?e) / real c"
  4281   let ?z = "(- ?e) / real c"
  4244   {fix x
  4282   {fix x
  4245     assume xz: "x > ?z"
  4283     assume xz: "x > ?z"
  4251       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4289       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4252   hence "\<forall> x > ?z. ?P ?z x (NEq (CN 0 c e))" by simp
  4290   hence "\<forall> x > ?z. ?P ?z x (NEq (CN 0 c e))" by simp
  4253   thus ?case by blast
  4291   thus ?case by blast
  4254 next
  4292 next
  4255   case (5 c e) 
  4293   case (5 c e) 
  4256   from prems have nb: "numbound0 e" by simp
  4294   from 5 have nb: "numbound0 e" by simp
  4257   from prems have cp: "real c > 0" by simp
  4295   from 5 have cp: "real c > 0" by simp
  4258   fix a
  4296   fix a
  4259   let ?e="Inum (a#bs) e"
  4297   let ?e="Inum (a#bs) e"
  4260   let ?z = "(- ?e) / real c"
  4298   let ?z = "(- ?e) / real c"
  4261   {fix x
  4299   {fix x
  4262     assume xz: "x > ?z"
  4300     assume xz: "x > ?z"
  4267       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4305       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4268   hence "\<forall> x > ?z. ?P ?z x (Lt (CN 0 c e))" by simp
  4306   hence "\<forall> x > ?z. ?P ?z x (Lt (CN 0 c e))" by simp
  4269   thus ?case by blast
  4307   thus ?case by blast
  4270 next
  4308 next
  4271   case (6 c e) 
  4309   case (6 c e) 
  4272   from prems have nb: "numbound0 e" by simp
  4310   from 6 have nb: "numbound0 e" by simp
  4273   from prems have cp: "real c > 0" by simp
  4311   from 6 have cp: "real c > 0" by simp
  4274   fix a
  4312   fix a
  4275   let ?e="Inum (a#bs) e"
  4313   let ?e="Inum (a#bs) e"
  4276   let ?z = "(- ?e) / real c"
  4314   let ?z = "(- ?e) / real c"
  4277   {fix x
  4315   {fix x
  4278     assume xz: "x > ?z"
  4316     assume xz: "x > ?z"
  4283       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4321       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4284   hence "\<forall> x > ?z. ?P ?z x (Le (CN 0 c e))" by simp
  4322   hence "\<forall> x > ?z. ?P ?z x (Le (CN 0 c e))" by simp
  4285   thus ?case by blast
  4323   thus ?case by blast
  4286 next
  4324 next
  4287   case (7 c e) 
  4325   case (7 c e) 
  4288   from prems have nb: "numbound0 e" by simp
  4326   from 7 have nb: "numbound0 e" by simp
  4289   from prems have cp: "real c > 0" by simp
  4327   from 7 have cp: "real c > 0" by simp
  4290   fix a
  4328   fix a
  4291   let ?e="Inum (a#bs) e"
  4329   let ?e="Inum (a#bs) e"
  4292   let ?z = "(- ?e) / real c"
  4330   let ?z = "(- ?e) / real c"
  4293   {fix x
  4331   {fix x
  4294     assume xz: "x > ?z"
  4332     assume xz: "x > ?z"
  4299       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4337       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
  4300   hence "\<forall> x > ?z. ?P ?z x (Gt (CN 0 c e))" by simp
  4338   hence "\<forall> x > ?z. ?P ?z x (Gt (CN 0 c e))" by simp
  4301   thus ?case by blast
  4339   thus ?case by blast
  4302 next
  4340 next
  4303   case (8 c e) 
  4341   case (8 c e) 
  4304   from prems have nb: "numbound0 e" by simp
  4342   from 8 have nb: "numbound0 e" by simp
  4305   from prems have cp: "real c > 0" by simp
  4343   from 8 have cp: "real c > 0" by simp
  4306   fix a
  4344   fix a
  4307   let ?e="Inum (a#bs) e"
  4345   let ?e="Inum (a#bs) e"
  4308   let ?z = "(- ?e) / real c"
  4346   let ?z = "(- ?e) / real c"
  4309   {fix x
  4347   {fix x
  4310     assume xz: "x > ?z"
  4348     assume xz: "x > ?z"
  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
  5600 
  5645 
  5601 use "mir_tac.ML"
  5646 use "mir_tac.ML"
  5602 setup "Mir_Tac.setup"
  5647 setup "Mir_Tac.setup"
  5603 
  5648 
  5604 lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
  5649 lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
  5605 apply mir
  5650   by mir
  5606 done
       
  5607 
  5651 
  5608 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))"
  5652 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))"
  5609 apply mir
  5653   by mir
  5610 done
       
  5611 
  5654 
  5612 lemma "ALL (x::real). 2*\<lfloor>x\<rfloor> \<le> \<lfloor>2*x\<rfloor> \<and> \<lfloor>2*x\<rfloor> \<le> 2*\<lfloor>x+1\<rfloor>"
  5655 lemma "ALL (x::real). 2*\<lfloor>x\<rfloor> \<le> \<lfloor>2*x\<rfloor> \<and> \<lfloor>2*x\<rfloor> \<le> 2*\<lfloor>x+1\<rfloor>"
  5613 apply mir 
  5656   by mir 
  5614 done
       
  5615 
  5657 
  5616 lemma "ALL (x::real). \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)"
  5658 lemma "ALL (x::real). \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)"
  5617 apply mir
  5659   by mir
  5618 done
       
  5619 
  5660 
  5620 lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
  5661 lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
  5621 apply mir
  5662   by mir
  5622 done
       
  5623 
  5663 
  5624 end
  5664 end