diff -r 550a8ecffe0c -r d37babdf5cae src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Thu Mar 03 18:43:15 2011 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Mar 03 21:43:06 2011 +0100 @@ -1480,7 +1480,7 @@ let ?at = "snd (zsplit0 t)" have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \ n=-?nt" using 5 by (simp add: Let_def split_def) - from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast + from abj 5 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast from th2[simplified] th[simplified] show ?case by simp next case (6 s t n a) @@ -1490,12 +1490,12 @@ let ?at = "snd (zsplit0 t)" have abjs: "zsplit0 s = (?ns,?as)" by simp moreover have abjt: "zsplit0 t = (?nt,?at)" by simp - ultimately have th: "a=Add ?as ?at \ n=?ns + ?nt" using prems + ultimately have th: "a=Add ?as ?at \ n=?ns + ?nt" using 6 by (simp add: Let_def split_def) from abjs[symmetric] have bluddy: "\ x y. (x,y) = zsplit0 s" by blast - from prems have "(\ x y. (x,y) = zsplit0 s) \ (\xa xb. zsplit0 t = (xa, xb) \ Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \ numbound0 xb)" by blast (*FIXME*) + from 6 have "(\ x y. (x,y) = zsplit0 s) \ (\xa xb. zsplit0 t = (xa, xb) \ Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \ numbound0 xb)" by blast (*FIXME*) with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast - from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \ ?N ?as" by blast + from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \ ?N ?as" by blast from th3[simplified] th2[simplified] th[simplified] show ?case by (simp add: left_distrib) next @@ -1506,31 +1506,31 @@ let ?at = "snd (zsplit0 t)" have abjs: "zsplit0 s = (?ns,?as)" by simp moreover have abjt: "zsplit0 t = (?nt,?at)" by simp - ultimately have th: "a=Sub ?as ?at \ n=?ns - ?nt" using prems + ultimately have th: "a=Sub ?as ?at \ n=?ns - ?nt" using 7 by (simp add: Let_def split_def) from abjs[symmetric] have bluddy: "\ x y. (x,y) = zsplit0 s" by blast - from prems have "(\ x y. (x,y) = zsplit0 s) \ (\xa xb. zsplit0 t = (xa, xb) \ Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \ numbound0 xb)" by blast (*FIXME*) + from 7 have "(\ x y. (x,y) = zsplit0 s) \ (\xa xb. zsplit0 t = (xa, xb) \ Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \ numbound0 xb)" by blast (*FIXME*) with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast - from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \ ?N ?as" by blast + from abjs 7 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \ ?N ?as" by blast from th3[simplified] th2[simplified] th[simplified] show ?case by (simp add: left_diff_distrib) next case (8 i t n a) let ?nt = "fst (zsplit0 t)" let ?at = "snd (zsplit0 t)" - have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \ n=i*?nt" using prems + have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \ n=i*?nt" using 8 by (simp add: Let_def split_def) - from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast - hence " ?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp + from abj 8 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast + hence "?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp also have "\ = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib) finally show ?case using th th2 by simp next case (9 t n a) let ?nt = "fst (zsplit0 t)" let ?at = "snd (zsplit0 t)" - have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a= Floor ?at \ n=?nt" using prems + have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a= Floor ?at \ n=?nt" using 9 by (simp add: Let_def split_def) - from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast + from abj 9 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast hence na: "?N a" using th by simp have th': "(real ?nt)*(real x) = real (?nt * x)" by simp have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp @@ -1864,8 +1864,8 @@ let ?N = "\ t. Inum (real i#bs) t" have "j=0 \ (j\0 \ ?c = 0) \ (j\0 \ ?c >0 \ ?c\0) \ (j\ 0 \ ?c<0 \ ?c\0)" by arith moreover - {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) - hence ?case using prems by (simp del: zlfm.simps add: rdvd_left_0_eq)} + { assume j: "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) + hence ?case using 11 j by (simp del: zlfm.simps add: rdvd_left_0_eq)} moreover {assume "?c=0" and "j\0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"] @@ -1910,8 +1910,8 @@ let ?N = "\ t. Inum (real i#bs) t" have "j=0 \ (j\0 \ ?c = 0) \ (j\0 \ ?c >0 \ ?c\0) \ (j\ 0 \ ?c<0 \ ?c\0)" by arith moreover - {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) - hence ?case using prems by (simp del: zlfm.simps add: rdvd_left_0_eq)} + {assume j: "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) + hence ?case using 12 j by (simp del: zlfm.simps add: rdvd_left_0_eq)} moreover {assume "?c=0" and "j\0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"] @@ -2012,20 +2012,21 @@ proof (induct p rule: iszlfm.induct) case (1 p q) let ?d = "\ (And p q)" - from prems lcm_pos_int have dp: "?d >0" by simp - have d1: "\ p dvd \ (And p q)" using prems by simp - hence th: "d\ p ?d" - using delta_mono prems by(simp only: iszlfm.simps) blast - have "\ q dvd \ (And p q)" using prems by simp - hence th': "d\ q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast + from 1 lcm_pos_int have dp: "?d >0" by simp + have d1: "\ p dvd \ (And p q)" using 1 by simp + hence th: "d\ p ?d" + using delta_mono 1 by (simp only: iszlfm.simps) blast + have "\ q dvd \ (And p q)" using 1 by simp + hence th': "d\ q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast from th th' dp show ?case by simp next case (2 p q) let ?d = "\ (And p q)" - from prems lcm_pos_int have dp: "?d >0" by simp - have "\ p dvd \ (And p q)" using prems by simp hence th: "d\ p ?d" using delta_mono prems - by(simp only: iszlfm.simps) blast - have "\ q dvd \ (And p q)" using prems by simp hence th': "d\ q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast + from 2 lcm_pos_int have dp: "?d >0" by simp + have "\ p dvd \ (And p q)" using 2 by simp + hence th: "d\ p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast + have "\ q dvd \ (And p q)" using 2 by simp + hence th': "d\ q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast from th th' dp show ?case by simp qed simp_all @@ -2037,25 +2038,27 @@ using linp proof (induct p rule: minusinf.induct) case (1 f g) - from prems have "?P f" by simp + then have "?P f" by simp then obtain z1 where z1_def: "\ x < z1. ?I x (?M f) = ?I x f" by blast - from prems have "?P g" by simp + with 1 have "?P g" by simp then obtain z2 where z2_def: "\ x < z2. ?I x (?M g) = ?I x g" by blast let ?z = "min z1 z2" from z1_def z2_def have "\ x < ?z. ?I x (?M (And f g)) = ?I x (And f g)" by simp thus ?case by blast next - case (2 f g) from prems have "?P f" by simp + case (2 f g) + then have "?P f" by simp then obtain z1 where z1_def: "\ x < z1. ?I x (?M f) = ?I x f" by blast - from prems have "?P g" by simp + with 2 have "?P g" by simp then obtain z2 where z2_def: "\ x < z2. ?I x (?M g) = ?I x g" by blast let ?z = "min z1 z2" from z1_def z2_def have "\ x < ?z. ?I x (?M (Or f g)) = ?I x (Or f g)" by simp thus ?case by blast next case (3 c e) - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp - from prems have nbe: "numbound0 e" by simp + then have "c > 0" by simp + hence rcpos: "real c > 0" by simp + from 3 have nbe: "numbound0 e" by simp fix y have "\ x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Eq (CN 0 c e))) = ?I x (Eq (CN 0 c e))" proof (simp add: less_floor_eq , rule allI, rule impI) @@ -2071,8 +2074,8 @@ thus ?case by blast next case (4 c e) - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp - from prems have nbe: "numbound0 e" by simp + then have "c > 0" by simp hence rcpos: "real c > 0" by simp + from 4 have nbe: "numbound0 e" by simp fix y have "\ x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (NEq (CN 0 c e))) = ?I x (NEq (CN 0 c e))" proof (simp add: less_floor_eq , rule allI, rule impI) @@ -2088,8 +2091,8 @@ thus ?case by blast next case (5 c e) - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp - from prems have nbe: "numbound0 e" by simp + then have "c > 0" by simp hence rcpos: "real c > 0" by simp + from 5 have nbe: "numbound0 e" by simp fix y have "\ x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Lt (CN 0 c e))) = ?I x (Lt (CN 0 c e))" proof (simp add: less_floor_eq , rule allI, rule impI) @@ -2104,8 +2107,8 @@ thus ?case by blast next case (6 c e) - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp - from prems have nbe: "numbound0 e" by simp + then have "c > 0" by simp hence rcpos: "real c > 0" by simp + from 6 have nbe: "numbound0 e" by simp fix y have "\ x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Le (CN 0 c e))) = ?I x (Le (CN 0 c e))" proof (simp add: less_floor_eq , rule allI, rule impI) @@ -2120,8 +2123,8 @@ thus ?case by blast next case (7 c e) - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp - from prems have nbe: "numbound0 e" by simp + then have "c > 0" by simp hence rcpos: "real c > 0" by simp + from 7 have nbe: "numbound0 e" by simp fix y have "\ x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Gt (CN 0 c e))) = ?I x (Gt (CN 0 c e))" proof (simp add: less_floor_eq , rule allI, rule impI) @@ -2136,8 +2139,8 @@ thus ?case by blast next case (8 c e) - from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp - from prems have nbe: "numbound0 e" by simp + then have "c > 0" by simp hence rcpos: "real c > 0" by simp + from 8 have nbe: "numbound0 e" by simp fix y have "\ x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Ge (CN 0 c e))) = ?I x (Ge (CN 0 c e))" proof (simp add: less_floor_eq , rule allI, rule impI) @@ -2336,15 +2339,15 @@ have th: "(real j rdvd real c * real x - Inum (real x # bs) e) = (real j rdvd - (real c * real x - Inum (real x # bs) e))" by (simp only: rdvd_minus[symmetric]) - from prems th show ?case + from 9 th show ?case by (simp add: algebra_simps numbound0_I[where bs="bs" and b'="real x" and b="- real x"]) next - case (10 j c e) + case (10 j c e) have th: "(real j rdvd real c * real x - Inum (real x # bs) e) = (real j rdvd - (real c * real x - Inum (real x # bs) e))" by (simp only: rdvd_minus[symmetric]) - from prems th show ?case + from 10 th show ?case by (simp add: algebra_simps numbound0_I[where bs="bs" and b'="real x" and b="- real x"]) qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"]) @@ -2396,16 +2399,16 @@ using linp proof(induct p rule: iszlfm.induct) case (1 p q) - from prems have dl1: "\ p dvd lcm (\ p) (\ q)" by simp - from prems have dl2: "\ q dvd lcm (\ p) (\ q)" by simp - from prems d\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] + then have dl1: "\ p dvd lcm (\ p) (\ q)" by simp + from 1 have dl2: "\ q dvd lcm (\ p) (\ q)" by simp + from 1 d\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] d\_mono[where p = "q" and l="\ q" and l'="lcm (\ p) (\ q)"] dl1 dl2 show ?case by (auto simp add: lcm_pos_int) next case (2 p q) - from prems have dl1: "\ p dvd lcm (\ p) (\ q)" by simp - from prems have dl2: "\ q dvd lcm (\ p) (\ q)" by simp - from prems d\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] + then have dl1: "\ p dvd lcm (\ p) (\ q)" by simp + from 2 have dl2: "\ q dvd lcm (\ p) (\ q)" by simp + from 2 d\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] d\_mono[where p = "q" and l="\ q" and l'="lcm (\ p) (\ q)"] dl1 dl2 show ?case by (auto simp add: lcm_pos_int) qed (auto simp add: lcm_pos_int) @@ -2577,19 +2580,20 @@ shows "?P (x - d)" using lp u d dp nob p proof(induct p rule: iszlfm.induct) - case (5 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+ - with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] prems - show ?case by (simp del: real_of_int_minus) + case (5 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp_all + with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] 5 + show ?case by (simp del: real_of_int_minus) next - case (6 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+ - with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] prems - show ?case by (simp del: real_of_int_minus) + case (6 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp_all + with dp p c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] 6 + show ?case by (simp del: real_of_int_minus) next - 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+ - let ?e = "Inum (real x # bs) e" - from ie1 have ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="a#bs"] + 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_all + let ?e = "Inum (real x # bs) e" + from ie1 have ie: "real (floor ?e) = ?e" using isint_iff[where n="e" and bs="a#bs"] numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"] - by (simp add: isint_iff) + by (simp add: isint_iff) {assume "real (x-d) +?e > 0" hence ?case using c1 numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] by (simp del: real_of_int_minus)} @@ -2597,7 +2601,7 @@ {assume H: "\ real (x-d) + ?e > 0" let ?v="Neg e" have vb: "?v \ set (\ (Gt (CN 0 c e)))" by simp - from prems(11)[simplified simp_thms Inum.simps \.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] + from 7(5)[simplified simp_thms Inum.simps \.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] have nob: "\ (\ j\ {1 ..d}. real x = - ?e + real j)" by auto from H p have "real x + ?e > 0 \ real x + ?e \ real d" by (simp add: c1) hence "real (x + floor ?e) > real (0::int) \ real (x + floor ?e) \ real d" @@ -2623,7 +2627,7 @@ {assume H: "\ real (x-d) + ?e \ 0" let ?v="Sub (C -1) e" have vb: "?v \ set (\ (Ge (CN 0 c e)))" by simp - from prems(11)[simplified simp_thms Inum.simps \.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] + from 8(5)[simplified simp_thms Inum.simps \.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] have nob: "\ (\ j\ {1 ..d}. real x = - ?e - 1 + real j)" by auto from H p have "real x + ?e \ 0 \ real x + ?e < real d" by (simp add: c1) hence "real (x + floor ?e) \ real (0::int) \ real (x + floor ?e) < real d" @@ -2643,7 +2647,7 @@ let ?e = "Inum (real x # bs) e" let ?v="(Sub (C -1) e)" have vb: "?v \ set (\ (Eq (CN 0 c e)))" by simp - from p have "real x= - ?e" by (simp add: c1) with prems(11) show ?case using dp + from p have "real x= - ?e" by (simp add: c1) with 3(5) show ?case using dp by simp (erule ballE[where x="1"], simp_all add:algebra_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"]) next @@ -2659,47 +2663,49 @@ hence "real x = - Inum ((real (x -d)) # bs) e + real d" by simp hence "real x = - Inum (a # bs) e + real d" by (simp add: numbound0_I[OF bn,where b="real x - real d"and b'="a"and bs="bs"]) - with prems(11) have ?case using dp by simp} + with 4(5) have ?case using dp by simp} ultimately show ?case by blast next case (9 j c e) hence p: "Ifm (real x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+ - let ?e = "Inum (real x # bs) e" - from prems have "isint e (a #bs)" by simp - 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"] - by (simp add: isint_iff) - from prems have id: "j dvd d" by simp - from c1 ie[symmetric] have "?p x = (real j rdvd real (x+ floor ?e))" by simp - also have "\ = (j dvd x + floor ?e)" - using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp - also have "\ = (j dvd x - d + floor ?e)" - using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp - also have "\ = (real j rdvd real (x - d + floor ?e))" - using int_rdvd_real[where i="j" and x="real (x-d + floor ?e)",symmetric, simplified] + let ?e = "Inum (real x # bs) e" + from 9 have "isint e (a #bs)" by simp + 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"] + by (simp add: isint_iff) + from 9 have id: "j dvd d" by simp + from c1 ie[symmetric] have "?p x = (real j rdvd real (x+ floor ?e))" by simp + also have "\ = (j dvd x + floor ?e)" + using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp + also have "\ = (j dvd x - d + floor ?e)" + using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp + also have "\ = (real j rdvd real (x - d + floor ?e))" + using int_rdvd_real[where i="j" and x="real (x-d + floor ?e)",symmetric, simplified] ie by simp - also have "\ = (real j rdvd real x - real d + ?e)" - using ie by simp - finally show ?case - using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp + also have "\ = (real j rdvd real x - real d + ?e)" + using ie by simp + finally show ?case + using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp next 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+ - let ?e = "Inum (real x # bs) e" - from prems have "isint e (a#bs)" by simp - 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"] - by (simp add: isint_iff) - from prems have id: "j dvd d" by simp - from c1 ie[symmetric] have "?p x = (\ real j rdvd real (x+ floor ?e))" by simp - also have "\ = (\ j dvd x + floor ?e)" - using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp - also have "\ = (\ j dvd x - d + floor ?e)" - using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp - also have "\ = (\ real j rdvd real (x - d + floor ?e))" - using int_rdvd_real[where i="j" and x="real (x-d + floor ?e)",symmetric, simplified] + let ?e = "Inum (real x # bs) e" + from 10 have "isint e (a#bs)" by simp + 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"] + by (simp add: isint_iff) + from 10 have id: "j dvd d" by simp + from c1 ie[symmetric] have "?p x = (\ real j rdvd real (x+ floor ?e))" by simp + also have "\ = (\ j dvd x + floor ?e)" + using int_rdvd_real[where i="j" and x="real (x+ floor ?e)"] by simp + also have "\ = (\ j dvd x - d + floor ?e)" + using dvd_period[OF id, where x="x" and c="-1" and t="floor ?e"] by simp + also have "\ = (\ real j rdvd real (x - d + floor ?e))" + using int_rdvd_real[where i="j" and x="real (x-d + floor ?e)",symmetric, simplified] ie by simp - also have "\ = (\ real j rdvd real x - real d + ?e)" - using ie by simp - finally show ?case using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp -qed (auto simp add: numbound0_I[where bs="bs" and b="real (x - d)" and b'="real x"] simp del: real_of_int_diff) + also have "\ = (\ real j rdvd real x - real d + ?e)" + using ie by simp + finally show ?case + using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp +qed (auto simp add: numbound0_I[where bs="bs" and b="real (x - d)" and b'="real x"] + simp del: real_of_int_diff) lemma \': assumes lp: "iszlfm p (a #bs)" @@ -2834,179 +2840,213 @@ using linp kpos tnb proof(induct p rule: \\.induct) case (3 c e) - from prems have cp: "c > 0" and nb: "numbound0 e" by auto - {assume kdc: "k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + from 3 have cp: "c > 0" and nb: "numbound0 e" by auto + { assume kdc: "k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } - moreover - {assume "\ k dvd c" - from kpos have knz: "k\0" by simp hence knz': "real k \ 0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - 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)" - using real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) - also have "\ = (?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"] + moreover + { assume *: "\ k dvd c" + from kpos have knz: "k\0" by simp hence knz': "real k \ 0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" + using isint_def by simp + 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)" + using real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti algebra_simps) + also have "\ = (?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"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) finally have ?case . } ultimately show ?case by blast next case (4 c e) - from prems have cp: "c > 0" and nb: "numbound0 e" by auto - {assume kdc: "k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + then have cp: "c > 0" and nb: "numbound0 e" by auto + { assume kdc: "k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } - moreover - {assume "\ k dvd c" - from kpos have knz: "k\0" by simp hence knz': "real k \ 0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - 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 \ 0)" - using real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) - also have "\ = (?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"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] - by (simp add: ti) - finally have ?case . } - ultimately show ?case by blast + moreover + { assume *: "\ k dvd c" + from kpos have knz: "k\0" by simp hence knz': "real k \ 0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + 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 \ 0)" + using real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti algebra_simps) + also have "\ = (?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"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti) + finally have ?case . } + ultimately show ?case by blast next case (5 c e) - from prems have cp: "c > 0" and nb: "numbound0 e" by auto - {assume kdc: "k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + then have cp: "c > 0" and nb: "numbound0 e" by auto + { assume kdc: "k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } - moreover - {assume "\ k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - 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)" - using real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) - also have "\ = (?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"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] - by (simp add: ti) - finally have ?case . } - ultimately show ?case by blast + moreover + { assume *: "\ k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + 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)" + using real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti algebra_simps) + also have "\ = (?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"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti) + finally have ?case . } + ultimately show ?case by blast next case (6 c e) - from prems have cp: "c > 0" and nb: "numbound0 e" by auto - {assume kdc: "k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + then have cp: "c > 0" and nb: "numbound0 e" by auto + { assume kdc: "k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } - moreover - {assume "\ k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - 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 \ 0)" - using real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) - also have "\ = (?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"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] - by (simp add: ti) - finally have ?case . } - ultimately show ?case by blast + moreover + { assume *: "\ k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + 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 \ 0)" + using real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti algebra_simps) + also have "\ = (?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"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti) + finally have ?case . } + ultimately show ?case by blast next case (7 c e) - from prems have cp: "c > 0" and nb: "numbound0 e" by auto - {assume kdc: "k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + then have cp: "c > 0" and nb: "numbound0 e" by auto + { assume kdc: "k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } - moreover - {assume "\ k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - 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)" - using real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) - also have "\ = (?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"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] - by (simp add: ti) - finally have ?case . } - ultimately show ?case by blast + moreover + { assume *: "\ k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + 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)" + using real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti algebra_simps) + also have "\ = (?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"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti) + finally have ?case . } + ultimately show ?case by blast next case (8 c e) - from prems have cp: "c > 0" and nb: "numbound0 e" by auto - {assume kdc: "k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + then have cp: "c > 0" and nb: "numbound0 e" by auto + { assume kdc: "k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } - moreover - {assume "\ k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - 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 \ 0)" - using real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) - also have "\ = (?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"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] - by (simp add: ti) - finally have ?case . } - ultimately show ?case by blast + moreover + { assume *: "\ k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + 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 \ 0)" + using real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti algebra_simps) + also have "\ = (?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"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti) + finally have ?case . } + ultimately show ?case by blast next - case (9 i c e) from prems have cp: "c > 0" and nb: "numbound0 e" by auto - {assume kdc: "k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + case (9 i c e) + then have cp: "c > 0" and nb: "numbound0 e" by auto + { assume kdc: "k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } - moreover - {assume "\ k dvd c" - from kpos have knz: "k\0" by simp hence knz': "real k \ 0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - 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)" - using real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) - also have "\ = (?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"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] - by (simp add: ti) - finally have ?case . } - ultimately show ?case by blast + moreover + { assume *: "\ k dvd c" + from kpos have knz: "k\0" by simp hence knz': "real k \ 0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + 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)" + using real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti algebra_simps) + also have "\ = (?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"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti) + finally have ?case . } + ultimately show ?case by blast next - case (10 i c e) from prems have cp: "c > 0" and nb: "numbound0 e" by auto - {assume kdc: "k dvd c" - from kpos have knz: "k\0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - from prems have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + case (10 i c e) + then have cp: "c > 0" and nb: "numbound0 e" by auto + { assume kdc: "k dvd c" + from kpos have knz: "k\0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } - moreover - {assume "\ k dvd c" - from kpos have knz: "k\0" by simp hence knz': "real k \ 0" by simp - from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp - from prems have "?I (real x) (?s (NDvd i (CN 0 c e))) = (\ (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k))" - using real_of_int_div[OF knz kdt] - numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps) - also have "\ = (?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"] - numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] - by (simp add: ti) - finally have ?case . } - ultimately show ?case by blast -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"]) + moreover + { assume *: "\ k dvd c" + from kpos have knz: "k\0" by simp hence knz': "real k \ 0" by simp + from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp + from assms * have "?I (real x) (?s (NDvd i (CN 0 c e))) = (\ (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k))" + using real_of_int_div[OF knz kdt] + numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti algebra_simps) + also have "\ = (?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"] + numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] + by (simp add: ti) + finally have ?case . } + ultimately show ?case by blast +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"]) lemma \\_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t" @@ -3054,16 +3094,16 @@ ultimately show ?case by blast next case (5 c e) hence cp: "c > 0" by simp - from prems mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] + from 5 mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] real_of_int_mult] - show ?case using prems dp + show ?case using 5 dp by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] algebra_simps) next - case (6 c e) hence cp: "c > 0" by simp - from prems mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] + case (6 c e) hence cp: "c > 0" by simp + from 6 mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] real_of_int_mult] - show ?case using prems dp + show ?case using 6 dp by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] algebra_simps) next @@ -3118,45 +3158,48 @@ ultimately show ?case by blast next 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+ - let ?e = "Inum (real i # bs) e" - from prems have "isint e (real i #bs)" by simp - 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"] - by (simp add: isint_iff) - from prems have id: "j dvd d" by simp - from ie[symmetric] have "?p i = (real j rdvd real (c*i+ floor ?e))" by simp - also have "\ = (j dvd c*i + floor ?e)" - using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp - also have "\ = (j dvd c*i - c*d + floor ?e)" - using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp - also have "\ = (real j rdvd real (c*i - c*d + floor ?e))" - using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified] + let ?e = "Inum (real i # bs) e" + from 9 have "isint e (real i #bs)" by simp + 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"] + by (simp add: isint_iff) + from 9 have id: "j dvd d" by simp + from ie[symmetric] have "?p i = (real j rdvd real (c*i+ floor ?e))" by simp + also have "\ = (j dvd c*i + floor ?e)" + using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp + also have "\ = (j dvd c*i - c*d + floor ?e)" + using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp + also have "\ = (real j rdvd real (c*i - c*d + floor ?e))" + using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified] ie by simp - also have "\ = (real j rdvd real (c*(i - d)) + ?e)" - using ie by (simp add:algebra_simps) - finally show ?case - using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p - by (simp add: algebra_simps) + also have "\ = (real j rdvd real (c*(i - d)) + ?e)" + using ie by (simp add:algebra_simps) + finally show ?case + using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p + by (simp add: algebra_simps) next - case (10 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+ - let ?e = "Inum (real i # bs) e" - from prems have "isint e (real i #bs)" by simp - 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"] - by (simp add: isint_iff) - from prems have id: "j dvd d" by simp - from ie[symmetric] have "?p i = (\ (real j rdvd real (c*i+ floor ?e)))" by simp - also have "\ = Not (j dvd c*i + floor ?e)" - using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp - also have "\ = Not (j dvd c*i - c*d + floor ?e)" - using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp - also have "\ = Not (real j rdvd real (c*i - c*d + floor ?e))" - using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified] + case (10 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+ + let ?e = "Inum (real i # bs) e" + from 10 have "isint e (real i #bs)" by simp + 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"] + by (simp add: isint_iff) + from 10 have id: "j dvd d" by simp + from ie[symmetric] have "?p i = (\ (real j rdvd real (c*i+ floor ?e)))" by simp + also have "\ = Not (j dvd c*i + floor ?e)" + using int_rdvd_iff [where i="j" and t="c*i+ floor ?e"] by simp + also have "\ = Not (j dvd c*i - c*d + floor ?e)" + using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp + also have "\ = Not (real j rdvd real (c*i - c*d + floor ?e))" + using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified] ie by simp - also have "\ = Not (real j rdvd real (c*(i - d)) + ?e)" - using ie by (simp add:algebra_simps) - finally show ?case - using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p - by (simp add: algebra_simps) -qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"]) + also have "\ = Not (real j rdvd real (c*(i - d)) + ?e)" + using ie by (simp add:algebra_simps) + finally show ?case + using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p + by (simp add: algebra_simps) +qed (auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"]) lemma \_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t" shows "bound0 (\ p k t)" @@ -3361,10 +3404,10 @@ (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {0 .. n}})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {n .. 0}})))" by blast show ?case - proof(simp only: FS, clarsimp simp del: Ifm.simps Inum.simps, -) - fix p n s - let ?ths = "(?I p \ (?N (Floor a) = ?N (CN 0 n s))) \ numbound0 s \ isrlfm p" - assume "(\ba. (p, 0, ba) \ set (rsplit0 a) \ n = 0 \ s = Floor ba) \ + proof(simp only: FS, clarsimp simp del: Ifm.simps Inum.simps, -) + fix p n s + let ?ths = "(?I p \ (?N (Floor a) = ?N (CN 0 n s))) \ numbound0 s \ isrlfm p" + assume "(\ba. (p, 0, ba) \ set (rsplit0 a) \ n = 0 \ s = Floor ba) \ (\ab ac ba. (ab, ac, ba) \ set (rsplit0 a) \ 0 < ac \ @@ -3375,70 +3418,70 @@ ac < 0 \ (\j. p = fp ab ac ba j \ n = 0 \ s = Add (Floor ba) (C j) \ ac \ j \ j \ 0))" - moreover - {fix s' - assume "(p, 0, s') \ ?SS a" and "n = 0" and "s = Floor s'" - hence ?ths using prems by auto} - moreover - { fix p' n' s' j - assume pns: "(p', n', s') \ ?SS a" - and np: "0 < n'" - and p_def: "p = ?p (p',n',s') j" - and n0: "n = 0" - and s_def: "s = (Add (Floor s') (C j))" - and jp: "0 \ j" and jn: "j \ n'" - from prems pns have H:"(Ifm ((x\real) # (bs\real list)) p' \ + moreover + { fix s' + assume "(p, 0, s') \ ?SS a" and "n = 0" and "s = Floor s'" + hence ?ths using 5(1) by auto } + moreover + { fix p' n' s' j + assume pns: "(p', n', s') \ ?SS a" + and np: "0 < n'" + and p_def: "p = ?p (p',n',s') j" + and n0: "n = 0" + and s_def: "s = (Add (Floor s') (C j))" + and jp: "0 \ j" and jn: "j \ n'" + from 5 pns have H:"(Ifm ((x\real) # (bs\real list)) p' \ Inum (x # bs) a = Inum (x # bs) (CN 0 n' s')) \ numbound0 s' \ isrlfm p'" by blast - hence nb: "numbound0 s'" by simp - from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by (simp add: numsub_nb) - let ?nxs = "CN 0 n' s'" - let ?l = "floor (?N s') + j" - from H - have "?I (?p (p',n',s') j) \ + hence nb: "numbound0 s'" by simp + from H have nf: "isrlfm (?p (p',n',s') j)" using fp_def np by (simp add: numsub_nb) + let ?nxs = "CN 0 n' s'" + let ?l = "floor (?N s') + j" + from H + have "?I (?p (p',n',s') j) \ (((?N ?nxs \ real ?l) \ (?N ?nxs < real (?l + 1))) \ (?N a = ?N ?nxs ))" - by (simp add: fp_def np algebra_simps numsub numadd numfloor) - also have "\ \ ((floor (?N ?nxs) = ?l) \ (?N a = ?N ?nxs ))" - using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp - moreover - have "\ \ (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp - ultimately have "?I (?p (p',n',s') j) \ (?N (Floor a) = ?N ((Add (Floor s') (C j))))" - by blast - with s_def n0 p_def nb nf have ?ths by auto} + by (simp add: fp_def np algebra_simps numsub numadd numfloor) + also have "\ \ ((floor (?N ?nxs) = ?l) \ (?N a = ?N ?nxs ))" + using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp moreover - {fix p' n' s' j - assume pns: "(p', n', s') \ ?SS a" - and np: "n' < 0" - and p_def: "p = ?p (p',n',s') j" - and n0: "n = 0" - and s_def: "s = (Add (Floor s') (C j))" - and jp: "n' \ j" and jn: "j \ 0" - from prems pns have H:"(Ifm ((x\real) # (bs\real list)) p' \ + have "\ \ (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp + ultimately have "?I (?p (p',n',s') j) \ (?N (Floor a) = ?N ((Add (Floor s') (C j))))" + by blast + with s_def n0 p_def nb nf have ?ths by auto} + moreover + { fix p' n' s' j + assume pns: "(p', n', s') \ ?SS a" + and np: "n' < 0" + and p_def: "p = ?p (p',n',s') j" + and n0: "n = 0" + and s_def: "s = (Add (Floor s') (C j))" + and jp: "n' \ j" and jn: "j \ 0" + from 5 pns have H:"(Ifm ((x\real) # (bs\real list)) p' \