src/HOL/ex/MIR.thy

   from gp have gnz: "g \<noteq> 0" by simp
   from prems show ?case by (simp add: real_of_int_div[OF gnz gd])
 next
   case (2 n c t)  hence gd: "g dvd c" by simp
   from gp have gnz: "g \<noteq> 0" by simp
-  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_simps)
+  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
 next
   case (3 c s t)  hence gd: "g dvd c" by simp
   from gp have gnz: "g \<noteq> 0" by simp
-  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_simps) 
+  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) 
 qed (auto simp add: numgcd_def gp)
 consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
 recdef ismaxcoeff "measure size"
   "ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)"
   "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"

   "numadd (a,b) = Add a b"
 
 lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
 apply (induct t s rule: numadd.induct, simp_all add: Let_def)
  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
-  apply (case_tac "n1 = n2", simp_all add: ring_simps)
+  apply (case_tac "n1 = n2", simp_all add: algebra_simps)
   apply (simp only: left_distrib[symmetric])
  apply simp
 apply (case_tac "lex_bnd t1 t2", simp_all)
  apply (case_tac "c1+c2 = 0")
-  by (case_tac "t1 = t2", simp_all add: ring_simps left_distrib[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add left_distrib)
+  by (case_tac "t1 = t2", simp_all add: algebra_simps left_distrib[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add left_distrib)
 
 lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
 by (induct t s rule: numadd.induct, auto simp add: Let_def)
 
 recdef nummul "measure size"

   "nummul (CF c t s) = (\<lambda> i. CF (c*i) t (nummul s i))"
   "nummul (Mul c t) = (\<lambda> i. nummul t (i*c))"
   "nummul t = (\<lambda> i. Mul i t)"
 
 lemma nummul[simp]: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)"
-by (induct t rule: nummul.induct, auto simp add: ring_simps)
+by (induct t rule: nummul.induct, auto simp add: algebra_simps)
 
 lemma nummul_nb[simp]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"
 by (induct t rule: nummul.induct, auto)
 
 constdefs numneg :: "num \<Rightarrow> num"

   let ?bi = "snd (split_int b)"
   have "split_int b = (?bv,?bi)" by simp
   with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
   from prems(2) have tibi: "ti = CF c a ?bi" by (simp add: Let_def split_def)
   from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF)
-qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def ring_simps)
+qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def algebra_simps)
 
 lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (snd (split_int t)) "
 by (induct t rule: split_int.induct, auto simp add: Let_def split_def)
 
 definition

   "(real (a::int) + b > 0) = (real a + real (floor b) > 0 \<or> (real a + real (floor b) = 0 \<and> real (floor b) - b < 0))"
 proof- 
   have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith
   show ?thesis using myless[rule_format, where b="real (floor b)"] 
     by (simp only:th split_int_less_real'[where a="-a" and b="-b"]) 
-    (simp add: ring_simps diff_def[symmetric],arith)
+    (simp add: algebra_simps diff_def[symmetric],arith)
 qed
 
 lemma split_int_le_real: 
   "(real (a::int) \<le> b) = (a \<le> floor b \<or> (a = floor b \<and> real (floor b) < b))"
 proof( auto)

 lemma split_int_ge_real': 
   "(real (a::int) + b \<ge> 0) = (real a + real (floor b) \<ge> 0 \<or> (real a + real (floor b) = 0 \<and> real (floor b) - b < 0))"
 proof- 
   have th: "(real a + b \<ge>0) = (real (-a) + (-b) \<le> 0)" by arith
   show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"])
-    (simp add: ring_simps diff_def[symmetric],arith)
+    (simp add: algebra_simps diff_def[symmetric],arith)
 qed
 
 lemma split_int_eq_real: "(real (a::int) = b) = ( a = floor b \<and> b = real (floor b))" (is "?l = ?r")
 by auto
 

       assume 
 	"real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e"
       (is "?ri rdvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri rdvd ?rt")
       hence "\<exists> (l::int). ?rt = ?ri * (real l)" by (simp add: rdvd_def)
       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real l)+?rc*(?rk * (real i) * (real di))" 
-	by (simp add: ring_simps di_def)
+	by (simp add: algebra_simps di_def)
       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real (l + c*k*di))"
-	by (simp add: ring_simps)
+	by (simp add: algebra_simps)
       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri* (real l)" by blast
       thus "real i rdvd real c * real x + Inum (real x # bs) e" using rdvd_def by simp
     next
       assume 
 	"real i rdvd real c * real x + Inum (real x # bs) e" (is "?ri rdvd ?rc*?rx+?e")
       hence "\<exists> (l::int). ?rc*?rx+?e = ?ri * (real l)" by (simp add: rdvd_def)
       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real d)" by simp
       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real i * real di)" by (simp add: di_def)
-      hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_simps)
+      hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: algebra_simps)
       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l)"
 	by blast
       thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp
     qed
 next

       assume 
 	"real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e"
       (is "?ri rdvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri rdvd ?rt")
       hence "\<exists> (l::int). ?rt = ?ri * (real l)" by (simp add: rdvd_def)
       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real l)+?rc*(?rk * (real i) * (real di))" 
-	by (simp add: ring_simps di_def)
+	by (simp add: algebra_simps di_def)
       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real (l + c*k*di))"
-	by (simp add: ring_simps)
+	by (simp add: algebra_simps)
       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri* (real l)" by blast
       thus "real i rdvd real c * real x + Inum (real x # bs) e" using rdvd_def by simp
     next
       assume 
 	"real i rdvd real c * real x + Inum (real x # bs) e" (is "?ri rdvd ?rc*?rx+?e")
       hence "\<exists> (l::int). ?rc*?rx+?e = ?ri * (real l)" by (simp add: rdvd_def)
       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real d)" by simp
       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real i * real di)" by (simp add: di_def)
-      hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_simps)
+      hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: algebra_simps)
       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l)"
 	by blast
       thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp
     qed
 qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="real(x - k*d)" and b'="real x"] simp del: real_of_int_mult real_of_int_diff)

 proof(induct p rule: iszlfm.induct)
   case (9 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 show  ?case
-    by (simp add: ring_simps th[simplified ring_simps]
+  from prems 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)
   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 show  ?case
-    by (simp add: ring_simps th[simplified ring_simps]
+  from prems 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"] nth_pos2)
 
 lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"
 by (induct p rule: mirror.induct, auto simp add: isint_neg)

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e < (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e < 0)"
       by simp
-    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) < (real (l div c)) * 0)" by (simp add: ring_simps)
+    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) < (real (l div c)) * 0)" by (simp add: algebra_simps)
     also have "\<dots> = (real c * real x + Inum (real x # bs) e < 0)"
     using mult_less_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] be  isint_Mul[OF ei] by simp
 next
   case (6 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<le> (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<le> 0)"
       by simp
-    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<le> (real (l div c)) * 0)" by (simp add: ring_simps)
+    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<le> (real (l div c)) * 0)" by (simp add: algebra_simps)
     also have "\<dots> = (real c * real x + Inum (real x # bs) e \<le> 0)"
     using mult_le_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp
 next
   case (7 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e > (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e > 0)"
       by simp
-    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) > (real (l div c)) * 0)" by (simp add: ring_simps)
+    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) > (real (l div c)) * 0)" by (simp add: algebra_simps)
     also have "\<dots> = (real c * real x + Inum (real x # bs) e > 0)"
     using zero_less_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp
 next
   case (8 c e) hence cp: "c>0" and be: "numbound0 e"  and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<ge> (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<ge> 0)"
       by simp
-    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<ge> (real (l div c)) * 0)" by (simp add: ring_simps)
+    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<ge> (real (l div c)) * 0)" by (simp add: algebra_simps)
     also have "\<dots> = (real c * real x + Inum (real x # bs) e \<ge> 0)"
     using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp
 next
   case (3 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e = (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = 0)"
       by simp
-    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) = (real (l div c)) * 0)" by (simp add: ring_simps)
+    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) = (real (l div c)) * 0)" by (simp add: algebra_simps)
     also have "\<dots> = (real c * real x + Inum (real x # bs) e = 0)"
     using mult_eq_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp
 next
   case (4 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<noteq> (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<noteq> 0)"
       by simp
-    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<noteq> (real (l div c)) * 0)" by (simp add: ring_simps)
+    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<noteq> (real (l div c)) * 0)" by (simp add: algebra_simps)
     also have "\<dots> = (real c * real x + Inum (real x # bs) e \<noteq> 0)"
     using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp
 next
   case (9 j c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and jp: "j > 0" and d': "c dvd l" by simp+

       by (simp add: zdiv_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)"  by simp
-    also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: ring_simps)
+    also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: algebra_simps)
     also fix k have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"
     using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp
   also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp
   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def  be  isint_Mul[OF ei] mult_strict_mono[OF ldcp jp ldcp ] by simp 
 next

       by (simp add: zdiv_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)"  by simp
-    also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: ring_simps)
+    also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: algebra_simps)
     also fix k have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"
     using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp
   also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp
   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def  be  isint_Mul[OF ei]  mult_strict_mono[OF ldcp jp ldcp ] by simp
 qed (simp_all add: nth_pos2 numbound0_I[where bs="bs" and b="real (l * x)" and b'="real x"] isint_Mul del: real_of_int_mult)

       hence "real (x + floor ?e) > real (0::int) \<and> real (x + floor ?e) \<le> real d"
 	using ie by simp
       hence "x + floor ?e \<ge> 1 \<and> x + floor ?e \<le> d"  by simp
       hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e" by simp
       hence "\<exists> (j::int) \<in> {1 .. d}. real x = real (- floor ?e + j)" 
-	by (simp only: real_of_int_inject) (simp add: ring_simps)
+	by (simp only: real_of_int_inject) (simp add: algebra_simps)
       hence "\<exists> (j::int) \<in> {1 .. d}. real x = - ?e + real j" 
 	by (simp add: ie[simplified isint_iff])
       with nob have ?case by auto}
     ultimately show ?case by blast
 next

       from H p have "real x + ?e \<ge> 0 \<and> real x + ?e < real d" by (simp add: c1)
       hence "real (x + floor ?e) \<ge> real (0::int) \<and> real (x + floor ?e) < real d"
 	using ie by simp
       hence "x + floor ?e +1 \<ge> 1 \<and> x + floor ?e + 1 \<le> d"  by simp
       hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e + 1" by simp
-      hence "\<exists> (j::int) \<in> {1 .. d}. x= - floor ?e - 1 + j" by (simp add: ring_simps)
+      hence "\<exists> (j::int) \<in> {1 .. d}. x= - floor ?e - 1 + j" by (simp add: algebra_simps)
       hence "\<exists> (j::int) \<in> {1 .. d}. real x= real (- floor ?e - 1 + j)" 
 	by (simp only: real_of_int_inject)
       hence "\<exists> (j::int) \<in> {1 .. d}. real x= - ?e - 1 + real j" 
 	by (simp add: ie[simplified isint_iff])
       with nob have ?case by simp }

     let ?e = "Inum (real x # bs) e"
     let ?v="(Sub (C -1) e)"
     have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
     from p have "real x= - ?e" by (simp add: c1) with prems(11) show ?case using dp
       by simp (erule ballE[where x="1"],
-	simp_all add:ring_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"])
+	simp_all add:algebra_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"])
 next
   case (4 c e)hence p: "Ifm (real x #bs) (NEq (CN 0 c e))" (is "?p x") 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"
     let ?v="Neg e"

       from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 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 ring_simps)
+	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps)
       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"]
 	  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 

       from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 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 \<noteq> 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 ring_simps)
+	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps)
       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"]
 	  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 

       from kpos have knz: "k\<noteq>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 ring_simps)
+	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps)
       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"]
 	  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 

       from kpos have knz: "k\<noteq>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 \<le> 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 ring_simps)
+	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps)
       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"]
 	  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 

       from kpos have knz: "k\<noteq>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 ring_simps)
+	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps)
       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"]
 	  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 

       from kpos have knz: "k\<noteq>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 \<ge> 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 ring_simps)
+	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps)
       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"]
 	  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 

       from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 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 ring_simps)
+	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps)
       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"]
 	  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 

       from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 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))) = (\<not> (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 ring_simps)
+	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti algebra_simps)
       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"]
 	  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 

   case (3 c e)  
   from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
     moreover 
-    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
+    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
     ultimately show ?case by blast 
 next
   case (4 c e)   
   from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
     moreover 
-    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
+    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
     ultimately show ?case by blast 
 next
   case (5 c e)   
   from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
     moreover 
-    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_less_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
+    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_less_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
     ultimately show ?case by blast 
 next
   case (6 c e)    
   from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
     moreover 
-    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_le_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
+    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_le_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
     ultimately show ?case by blast 
 next
   case (7 c e)    
   from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
     moreover 
-    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_less_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
+    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_less_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
     ultimately show ?case by blast 
 next
   case (8 c e)    
   from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
     moreover 
-    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_le_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
+    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_le_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}
     ultimately show ?case by blast 
 next
   case (9 i c e)
   from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp

   moreover 
   {assume "\<not> k dvd c"
     hence "Ifm (real (x*k)#bs) (a\<rho> (Dvd i (CN 0 c e)) k) = 
       (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k)" 
       using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] 
-      by (simp add: ring_simps)
+      by (simp add: algebra_simps)
     also have "\<dots> = (Ifm (real x#bs) (Dvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"])
     finally have ?case . }
   ultimately show ?case by blast 
 next
   case (10 i c e) 

   moreover 
   {assume "\<not> k dvd c"
     hence "Ifm (real (x*k)#bs) (a\<rho> (NDvd i (CN 0 c e)) k) = 
       (\<not> (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k))" 
       using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] 
-      by (simp add: ring_simps)
+      by (simp add: algebra_simps)
     also have "\<dots> = (Ifm (real x#bs) (NDvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"])
     finally have ?case . }
   ultimately show ?case by blast 
 qed (simp_all add: nth_pos2)
 

   shows "(\<exists> (x::int). real k rdvd real x \<and> Ifm (real x#bs) (a\<rho> p k)) = 
   (\<exists> (x::int). Ifm (real x#bs) p)" (is "(\<exists> x. ?D x \<and> ?P' x) = (\<exists> x. ?P x)")
 proof-
   have "(\<exists> x. ?D x \<and> ?P' x) = (\<exists> x. k dvd x \<and> ?P' x)" using int_rdvd_iff by simp
   also have "\<dots> = (\<exists>x. ?P' (x*k))" using unity_coeff_ex[where P="?P'" and l="k", simplified]
-    by (simp add: ring_simps)
+    by (simp add: algebra_simps)
   also have "\<dots> = (\<exists> x. ?P x)" using a\<rho> iszlfm_gen[OF lp] kp by auto
   finally show ?thesis .
 qed
 
 lemma \<sigma>\<rho>': assumes lp: "iszlfm p (real (x::int)#bs)" and kp: "k > 0" and nb: "numbound0 t"

   hence cp: "c >0" and nb: "numbound0 e" and ei: "isint e (real i#bs)"
     and nob: "\<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> - ?N i e + real j"
     by simp+
   {assume "real (c*i) \<noteq> - ?N i e + real (c*d)"
     with numbound0_I[OF nb, where bs="bs" and b="real i - real d" and b'="real i"]
-    have ?case by (simp add: ring_simps)}
+    have ?case by (simp add: algebra_simps)}
   moreover
   {assume pi: "real (c*i) = - ?N i e + real (c*d)"
     from mult_strict_left_mono[OF dp cp] have d: "(c*d) \<in> {1 .. c*d}" by simp
     from nob[rule_format, where j="c*d", OF d] pi have ?case by simp }
   ultimately show ?case by blast

   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] 
     real_of_int_mult]
   show ?case using prems dp 
     by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
-      ring_simps)
+      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] 
     real_of_int_mult]
   show ?case using prems dp 
     by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
-      ring_simps)
+      algebra_simps)
 next
   case (7 c e) hence cp: "c >0" and nb: "numbound0 e" and ei: "isint e (real i#bs)"
     and nob: "\<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> - ?N i e + real j"
     and pi: "real (c*i) + ?N i e > 0" and cp': "real c >0"
     by simp+
   let ?fe = "floor (?N i e)"
-  from pi cp have th:"(real i +?N i e / real c)*real c > 0" by (simp add: ring_simps)
+  from pi cp have th:"(real i +?N i e / real c)*real c > 0" by (simp add: algebra_simps)
   from pi ei[simplified isint_iff] have "real (c*i + ?fe) > real (0::int)" by simp
   hence pi': "c*i + ?fe > 0" by (simp only: real_of_int_less_iff[symmetric])
   have "real (c*i) + ?N i e > real (c*d) \<or> real (c*i) + ?N i e \<le> real (c*d)" by auto
   moreover
   {assume "real (c*i) + ?N i e > real (c*d)" hence ?case
-      by (simp add: ring_simps 
+      by (simp add: algebra_simps 
 	numbound0_I[OF nb,where bs="bs" and b="real i - real d" and b'="real i"])} 
   moreover 
   {assume H:"real (c*i) + ?N i e \<le> real (c*d)"
     with ei[simplified isint_iff] have "real (c*i + ?fe) \<le> real (c*d)" by simp
     hence pid: "c*i + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
     with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + ?fe = j1" by auto
     hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - ?N i e + real j1" 
-      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] ring_simps)
+      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps)
     with nob  have ?case by blast }
   ultimately show ?case by blast
 next
   case (8 c e)  hence cp: "c >0" and nb: "numbound0 e" and ei: "isint e (real i#bs)"
     and nob: "\<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> - 1 - ?N i e + real j"
     and pi: "real (c*i) + ?N i e \<ge> 0" and cp': "real c >0"
     by simp+
   let ?fe = "floor (?N i e)"
-  from pi cp have th:"(real i +?N i e / real c)*real c \<ge> 0" by (simp add: ring_simps)
+  from pi cp have th:"(real i +?N i e / real c)*real c \<ge> 0" by (simp add: algebra_simps)
   from pi ei[simplified isint_iff] have "real (c*i + ?fe) \<ge> real (0::int)" by simp
   hence pi': "c*i + 1 + ?fe \<ge> 1" by (simp only: real_of_int_le_iff[symmetric])
   have "real (c*i) + ?N i e \<ge> real (c*d) \<or> real (c*i) + ?N i e < real (c*d)" by auto
   moreover
   {assume "real (c*i) + ?N i e \<ge> real (c*d)" hence ?case
-      by (simp add: ring_simps 
+      by (simp add: algebra_simps 
 	numbound0_I[OF nb,where bs="bs" and b="real i - real d" and b'="real i"])} 
   moreover 
   {assume H:"real (c*i) + ?N i e < real (c*d)"
     with ei[simplified isint_iff] have "real (c*i + ?fe) < real (c*d)" by simp
     hence pid: "c*i + 1 + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
     with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + 1+ ?fe = j1" by auto
     hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) + 1= - ?N i e + real j1"
-      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] ring_simps real_of_one) 
+      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps real_of_one) 
     hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
-      by (simp only: ring_simps diff_def[symmetric])
+      by (simp only: algebra_simps diff_def[symmetric])
         hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
 	  by (simp only: add_ac diff_def)
     with nob  have ?case by blast }
   ultimately show ?case by blast
 next

       using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp
     also have "\<dots> = (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 "\<dots> = (real j rdvd real (c*(i - d)) + ?e)" 
-      using ie by (simp add:ring_simps)
+      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: ring_simps)
+      by (simp add: algebra_simps)
 next
   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+
     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"]

       using dvd_period[OF id, where x="c*i" and c="-c" and t="floor ?e"] by simp
     also have "\<dots> = 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 "\<dots> = Not (real j rdvd real (c*(i - d)) + ?e)" 
-      using ie by (simp add:ring_simps)
+      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: ring_simps)
+      by (simp add: algebra_simps)
 qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] nth_pos2)
 
 lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t"
   shows "bound0 (\<sigma> p k t)"
   using \<sigma>\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def)

 	let ?nxs = "CN 0 n' s'"
 	let ?l = "floor (?N s') + j"
 	from H 
 	have "?I (?p (p',n',s') j) \<longrightarrow> 
 	  (((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?N a = ?N ?nxs ))" 
-	  by (simp add: fp_def np ring_simps numsub numadd numfloor)
+	  by (simp add: fp_def np algebra_simps numsub numadd numfloor)
 	also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))"
 	  using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp
 	moreover
 	have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp
 	ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"

 	let ?nxs = "CN 0 n' s'"
 	let ?l = "floor (?N s') + j"
 	from H 
 	have "?I (?p (p',n',s') j) \<longrightarrow> 
 	  (((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?N a = ?N ?nxs ))" 
-	  by (simp add: np fp_def ring_simps numneg numfloor numadd numsub)
+	  by (simp add: np fp_def algebra_simps numneg numfloor numadd numsub)
 	also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))"
 	  using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp
 	moreover
 	have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"  by simp
 	ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"

   case (3 a b) then show ?case
   apply auto
   apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all
   apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all
   done
-qed (auto simp add: Let_def split_def ring_simps conj_rl)
+qed (auto simp add: Let_def split_def algebra_simps conj_rl)
 
 lemma real_in_int_intervals: 
   assumes xb: "real m \<le> x \<and> x < real ((n::int) + 1)"
   shows "\<exists> j\<in> {m.. n}. real j \<le> x \<and> x < real (j+1)" (is "\<exists> j\<in> ?N. ?P j")
 by (rule bexI[where P="?P" and x="floor x" and A="?N"]) 

     from real_in_int_intervals th have  "\<exists> j\<in> {0 .. n}. real j \<le> real n *x + ?N s - ?N (Floor s)\<and> real n *x + ?N s - ?N (Floor s) < real (j+1)" by simp
     
     hence "\<exists> j\<in> {0 .. n}. 0 \<le> real n *x + ?N s - ?N (Floor s) - real j \<and> real n *x + ?N s - ?N (Floor s) - real (j+1) < 0"
       by(simp only: myl[rule_format, where b="real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"]) 
     hence "\<exists> j\<in> {0.. n}. ?I (?p (p,n,s) j)"
-      using pns by (simp add: fp_def np ring_simps numsub numadd)
+      using pns by (simp add: fp_def np algebra_simps numsub numadd)
     then obtain "j" where j_def: "j\<in> {0 .. n} \<and> ?I (?p (p,n,s) j)" by blast
     hence "\<exists>x \<in> {?p (p,n,s) j |j. 0\<le> j \<and> j \<le> n }. ?I x" by auto
     hence ?case using pns 
       by (simp only: FS,simp add: bex_Un) 
     (rule disjI2, rule disjI1,rule exI [where x="p"],

     moreover
     {from mult_strict_left_mono_neg[OF x1, where c="real n"] nn
       have "real n *x + ?N s \<ge> real n + ?N s" by simp 
       moreover from real_of_int_floor_le[where r="?N s"]  have "real n + ?N s \<ge> real n + ?N (Floor s)" by simp
       ultimately have "real n *x + ?N s \<ge> ?N (Floor s) + real n" 
-	by (simp only: ring_simps)}
+	by (simp only: algebra_simps)}
     ultimately have "?N (Floor s) + real n \<le> real n *x + ?N s\<and> real n *x + ?N s < ?N (Floor s) + real (1::int)" by simp
     hence th: "real n \<le> real n *x + ?N s - ?N (Floor s) \<and> real n *x + ?N s - ?N (Floor s) < real (1::int)" by simp
     have th1: "\<forall> (a::real). (- a > 0) = (a < 0)" by auto
     have th2: "\<forall> (a::real). (0 \<ge> - a) = (a \<ge> 0)" by auto
     from real_in_int_intervals th  have  "\<exists> j\<in> {n .. 0}. real j \<le> real n *x + ?N s - ?N (Floor s)\<and> real n *x + ?N s - ?N (Floor s) < real (j+1)" by simp

   (is "\<forall> a n s . ?N a = ?N (CN 0 n s) \<and> _\<longrightarrow> ?I (lt n s) = ?I (Lt a)")
 proof(clarify)
   fix a n s
   assume H: "?N a = ?N (CN 0 n s)"
   show "?I (lt n s) = ?I (Lt a)" using H by (cases "n=0", (simp add: lt_def))
-  (cases "n > 0", simp_all add: lt_def ring_simps myless[rule_format, where b="0"])
+  (cases "n > 0", simp_all add: lt_def algebra_simps myless[rule_format, where b="0"])
 qed
 
 lemma lt_l: "isrlfm (rsplit lt a)"
   by (rule rsplit_l[where f="lt" and a="a"], auto simp add: lt_def,
     case_tac s, simp_all, case_tac "nat", simp_all)

 lemma le_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (le n s) = Ifm (x#bs) (Le a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (le n s) = ?I (Le a)")
 proof(clarify)
   fix a n s
   assume H: "?N a = ?N (CN 0 n s)"
   show "?I (le n s) = ?I (Le a)" using H by (cases "n=0", (simp add: le_def))
-  (cases "n > 0", simp_all add: le_def ring_simps myl[rule_format, where b="0"])
+  (cases "n > 0", simp_all add: le_def algebra_simps myl[rule_format, where b="0"])
 qed
 
 lemma le_l: "isrlfm (rsplit le a)"
   by (rule rsplit_l[where f="le" and a="a"], auto simp add: le_def) 
 (case_tac s, simp_all, case_tac "nat",simp_all)

 lemma gt_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (gt n s) = Ifm (x#bs) (Gt a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (gt n s) = ?I (Gt a)")
 proof(clarify)
   fix a n s
   assume H: "?N a = ?N (CN 0 n s)"
   show "?I (gt n s) = ?I (Gt a)" using H by (cases "n=0", (simp add: gt_def))
-  (cases "n > 0", simp_all add: gt_def ring_simps myless[rule_format, where b="0"])
+  (cases "n > 0", simp_all add: gt_def algebra_simps myless[rule_format, where b="0"])
 qed
 lemma gt_l: "isrlfm (rsplit gt a)"
   by (rule rsplit_l[where f="gt" and a="a"], auto simp add: gt_def) 
 (case_tac s, simp_all, case_tac "nat", simp_all)
 
 lemma ge_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (ge n s) = Ifm (x#bs) (Ge a)" (is "\<forall> a n s . ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (ge n s) = ?I (Ge a)")
 proof(clarify)
   fix a n s 
   assume H: "?N a = ?N (CN 0 n s)"
   show "?I (ge n s) = ?I (Ge a)" using H by (cases "n=0", (simp add: ge_def))
-  (cases "n > 0", simp_all add: ge_def ring_simps myl[rule_format, where b="0"])
+  (cases "n > 0", simp_all add: ge_def algebra_simps myl[rule_format, where b="0"])
 qed
 lemma ge_l: "isrlfm (rsplit ge a)"
   by (rule rsplit_l[where f="ge" and a="a"], auto simp add: ge_def) 
 (case_tac s, simp_all, case_tac "nat", simp_all)
 
 lemma eq_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (eq n s) = Ifm (x#bs) (Eq a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (eq n s) = ?I (Eq a)")
 proof(clarify)
   fix a n s 
   assume H: "?N a = ?N (CN 0 n s)"
-  show "?I (eq n s) = ?I (Eq a)" using H by (auto simp add: eq_def ring_simps)
+  show "?I (eq n s) = ?I (Eq a)" using H by (auto simp add: eq_def algebra_simps)
 qed
 lemma eq_l: "isrlfm (rsplit eq a)"
   by (rule rsplit_l[where f="eq" and a="a"], auto simp add: eq_def) 
 (case_tac s, simp_all, case_tac"nat", simp_all)
 
 lemma neq_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (neq n s) = Ifm (x#bs) (NEq a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (neq n s) = ?I (NEq a)")
 proof(clarify)
   fix a n s bs
   assume H: "?N a = ?N (CN 0 n s)"
-  show "?I (neq n s) = ?I (NEq a)" using H by (auto simp add: neq_def ring_simps)
+  show "?I (neq n s) = ?I (NEq a)" using H by (auto simp add: neq_def algebra_simps)
 qed
 
 lemma neq_l: "isrlfm (rsplit neq a)"
   by (rule rsplit_l[where f="neq" and a="a"], auto simp add: neq_def) 
 (case_tac s, simp_all, case_tac"nat", simp_all)

     \<and> real(floor (real n * u - s) + floor s)< real n - ?ss)" (is "_=(?DE \<and>real ?a \<ge> _ \<and> real ?a < _)")
     using nu0 nun  by auto
   also have "\<dots> = (?DE \<and> ?a \<ge> 0 \<and> ?a < n)" by(simp only: small_le[OF ss0 ss1] small_lt[OF ss0 ss1])
   also have "\<dots> = (?DE \<and> (\<exists> j\<in> {0 .. (n - 1)}. ?a = j))" by simp
   also have "\<dots> = (?DE \<and> (\<exists> j\<in> {0 .. (n - 1)}. real (\<lfloor>real n * u - s\<rfloor>) = real j - real \<lfloor>s\<rfloor> ))"
-    by (simp only: ring_simps real_of_int_diff[symmetric] real_of_int_inject del: real_of_int_diff)
+    by (simp only: algebra_simps real_of_int_diff[symmetric] real_of_int_inject del: real_of_int_diff)
   also have "\<dots> = ((\<exists> j\<in> {0 .. (n - 1)}. real n * u - s = real j - real \<lfloor>s\<rfloor> \<and> real i rdvd real n * u - s))" using int_rdvd_iff[where i="i" and t="\<lfloor>real n * u - s\<rfloor>"]
     by (auto cong: conj_cong)
-  also have "\<dots> = ?rhs" by(simp cong: conj_cong) (simp add: ring_simps )
+  also have "\<dots> = ?rhs" by(simp cong: conj_cong) (simp add: algebra_simps )
   finally show ?thesis .
 qed
 
 definition
   DVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"

   let ?f = "\<lambda> j. conj (Eq(CN 0 n (Add s (Sub(Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))"
   let ?s= "Inum (x#bs) s"
   from foldr_disj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
   have "Ifm (x#bs) (DVDJ i n s) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" 
     by (simp add: iupt_set np DVDJ_def del: iupt.simps)
-  also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: ring_simps diff_def[symmetric])
+  also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_def[symmetric])
   also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] 
   have "\<dots> = (real i rdvd real n * x - (-?s))" by simp
   finally show ?thesis by simp
 qed
 

   let ?f = "\<lambda> j. disj(NEq(CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor(Neg s))))"
   let ?s= "Inum (x#bs) s"
   from foldr_conj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
   have "Ifm (x#bs) (NDVDJ i n s) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" 
     by (simp add: iupt_set np NDVDJ_def del: iupt.simps)
-  also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: ring_simps diff_def[symmetric])
+  also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_def[symmetric])
   also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] 
   have "\<dots> = (\<not> (real i rdvd real n * x - (-?s)))" by simp
   finally show ?thesis by simp
 qed  
 

   case (5 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)"
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)"
     by (simp only: pos_less_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
-      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
+      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   also have "\<dots> = (real c *?t + ?n* (?N x e) < 0)"
     using np by simp 
-  finally show ?case using nbt nb by (simp add: ring_simps)
+  finally show ?case using nbt nb by (simp add: algebra_simps)
 next
   case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)"
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
     by (simp only: pos_le_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
-      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
+      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   also have "\<dots> = (real c *?t + ?n* (?N x e) \<le> 0)"
     using np by simp 
-  finally show ?case using nbt nb by (simp add: ring_simps)
+  finally show ?case using nbt nb by (simp add: algebra_simps)
 next
   case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)"
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)"
     by (simp only: pos_divide_less_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
-      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
+      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   also have "\<dots> = (real c *?t + ?n* (?N x e) > 0)"
     using np by simp 
-  finally show ?case using nbt nb by (simp add: ring_simps)
+  finally show ?case using nbt nb by (simp add: algebra_simps)
 next
   case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)"
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"
     by (simp only: pos_divide_le_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
-      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
+      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   also have "\<dots> = (real c *?t + ?n* (?N x e) \<ge> 0)"
     using np by simp 
-  finally show ?case using nbt nb by (simp add: ring_simps)
+  finally show ?case using nbt nb by (simp add: algebra_simps)
 next
   case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   from np have np: "real n \<noteq> 0" by simp
   have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)"
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) = 0)"
     by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
-      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
+      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   also have "\<dots> = (real c *?t + ?n* (?N x e) = 0)"
     using np by simp 
-  finally show ?case using nbt nb by (simp add: ring_simps)
+  finally show ?case using nbt nb by (simp add: algebra_simps)
 next
   case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   from np have np: "real n \<noteq> 0" by simp
   have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<noteq> 0)"
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)"
     by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
-      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
+      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
     using np by simp 
-  finally show ?case using nbt nb by (simp add: ring_simps)
+  finally show ?case using nbt nb by (simp add: algebra_simps)
 qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2)
 
 lemma \<Upsilon>_l:
   assumes lp: "isrlfm p"
   shows "\<forall> (t,k) \<in> set (\<Upsilon> p). numbound0 t \<and> k >0"

   and ly: "l < y" and yu: "y < u"
   shows "Ifm (y#bs) p"
 using lp px noS
 proof (induct p rule: isrlfm.induct)
   case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
-    from prems have "x * real c + ?N x e < 0" by (simp add: ring_simps)
+    from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps)
     hence pxc: "x < (- ?N x e) / real c" 
       by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"])
     from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
     with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
     hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
     moreover {assume y: "y < (-?N x e)/ real c"
       hence "y * real c < - ?N x e"
 	by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
-      hence "real c * y + ?N x e < 0" by (simp add: ring_simps)
+      hence "real c * y + ?N x e < 0" by (simp add: algebra_simps)
       hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
     moreover {assume y: "y > (- ?N x e) / real c" 
       with yu have eu: "u > (- ?N x e) / real c" by auto
       with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto)
       with lx pxc have "False" by auto
       hence ?case by simp }
     ultimately show ?case by blast
 next
   case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp +
-    from prems have "x * real c + ?N x e \<le> 0" by (simp add: ring_simps)
+    from prems have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps)
     hence pxc: "x \<le> (- ?N x e) / real c" 
       by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"])
     from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
     with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
     hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
     moreover {assume y: "y < (-?N x e)/ real c"
       hence "y * real c < - ?N x e"
 	by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
-      hence "real c * y + ?N x e < 0" by (simp add: ring_simps)
+      hence "real c * y + ?N x e < 0" by (simp add: algebra_simps)
       hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
     moreover {assume y: "y > (- ?N x e) / real c" 
       with yu have eu: "u > (- ?N x e) / real c" by auto
       with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto)
       with lx pxc have "False" by auto
       hence ?case by simp }
     ultimately show ?case by blast
 next
   case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
-    from prems have "x * real c + ?N x e > 0" by (simp add: ring_simps)
+    from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps)
     hence pxc: "x > (- ?N x e) / real c" 
       by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"])
     from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
     with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
     hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
     moreover {assume y: "y > (-?N x e)/ real c"
       hence "y * real c > - ?N x e"
 	by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
-      hence "real c * y + ?N x e > 0" by (simp add: ring_simps)
+      hence "real c * y + ?N x e > 0" by (simp add: algebra_simps)
       hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
     moreover {assume y: "y < (- ?N x e) / real c" 
       with ly have eu: "l < (- ?N x e) / real c" by auto
       with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto)
       with xu pxc have "False" by auto
       hence ?case by simp }
     ultimately show ?case by blast
 next
   case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
-    from prems have "x * real c + ?N x e \<ge> 0" by (simp add: ring_simps)
+    from prems have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps)
     hence pxc: "x \<ge> (- ?N x e) / real c" 
       by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"])
     from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
     with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
     hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto
     moreover {assume y: "y > (-?N x e)/ real c"
       hence "y * real c > - ?N x e"
 	by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
-      hence "real c * y + ?N x e > 0" by (simp add: ring_simps)
+      hence "real c * y + ?N x e > 0" by (simp add: algebra_simps)
       hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
     moreover {assume y: "y < (- ?N x e) / real c" 
       with ly have eu: "l < (- ?N x e) / real c" by auto
       with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto)
       with xu pxc have "False" by auto
       hence ?case by simp }
     ultimately show ?case by blast
 next
   case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
     from cp have cnz: "real c \<noteq> 0" by simp
-    from prems have "x * real c + ?N x e = 0" by (simp add: ring_simps)
+    from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps)
     hence pxc: "x = (- ?N x e) / real c" 
       by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"])
     from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
     with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto
     with pxc show ?case by simp

     from cp have cnz: "real c \<noteq> 0" by simp
     from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
     with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
     hence "y* real c \<noteq> -?N x e"      
       by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp
-    hence "y* real c + ?N x e \<noteq> 0" by (simp add: ring_simps)
+    hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
     thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 
-      by (simp add: ring_simps)
+      by (simp add: algebra_simps)
 qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
 
 lemma finite_set_intervals:
   assumes px: "P (x::real)" 
   and lx: "l \<le> x" and xu: "x \<le> u"

       let ?st = "Add (Mul m t) (Mul n s)"
       from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
 	by (simp add: mult_commute)
       from tnb snb have st_nb: "numbound0 ?st" by simp
       have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
-	using mnp mp np by (simp add: ring_simps add_divide_distrib)
+	using mnp mp np by (simp add: algebra_simps add_divide_distrib)
       from \<upsilon>_I[OF lp mnp st_nb, where x="x" and bs="bs"] 
       have "?I x (\<upsilon> p (?st,2*n*m)) = ?I ((?N t / real n + ?N s / real m) /2) p" by (simp only: st[symmetric])}
     with rinf_\<Upsilon>[OF lp nmi npi px] have "?F" by blast hence "?D" by blast}
   ultimately show "?D" by blast
 next

   "exsplit (NOT p) = NOT (exsplit p)"
   "exsplit p = p"
 
 lemma exsplitnum: 
   "Inum (x#y#bs) (exsplitnum t) = Inum ((x+y) #bs) t"
-  by(induct t rule: exsplitnum.induct) (simp_all add: ring_simps)
+  by(induct t rule: exsplitnum.induct) (simp_all add: algebra_simps)
 
 lemma exsplit: 
   assumes qfp: "qfree p"
   shows "Ifm (x#y#bs) (exsplit p) = Ifm ((x+y)#bs) p"
 using qfp exsplitnum[where x="x" and y="y" and bs="bs"]

   let ?N = "\<lambda> t. Inum (x#bs) t"
   let ?st= "Add (Mul m t) (Mul n s)"
   from Ul th have mnz: "m \<noteq> 0" by auto
   from Ul th have  nnz: "n \<noteq> 0" by auto  
   have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
-   using mnz nnz by (simp add: ring_simps add_divide_distrib)
+   using mnz nnz by (simp add: algebra_simps add_divide_distrib)
  
   thus "(real m *  Inum (x # bs) t + real n * Inum (x # bs) s) /
        (2 * real n * real m)
        \<in> (\<lambda>((t, n), s, m).
              (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) `
          (set U \<times> set U)"using mnz nnz th  
-    apply (auto simp add: th add_divide_distrib ring_simps split_def image_def)
+    apply (auto simp add: th add_divide_distrib algebra_simps split_def image_def)
     by (rule_tac x="(s,m)" in bexI,simp_all) 
   (rule_tac x="(t,n)" in bexI,simp_all)
 next
   fix t n s m
   assume tnU: "(t,n) \<in> set U" and smU:"(s,m) \<in> set U" 
   let ?N = "\<lambda> t. Inum (x#bs) t"
   let ?st= "Add (Mul m t) (Mul n s)"
   from Ul smU have mnz: "m \<noteq> 0" by auto
   from Ul tnU have  nnz: "n \<noteq> 0" by auto  
   have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
-   using mnz nnz by (simp add: ring_simps add_divide_distrib)
+   using mnz nnz by (simp add: algebra_simps add_divide_distrib)
  let ?P = "\<lambda> (t',n') (s',m'). (Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2"
  have Pc:"\<forall> a b. ?P a b = ?P b a"
    by auto
  from Ul alluopairs_set1 have Up:"\<forall> ((t,n),(s,m)) \<in> set (alluopairs U). n \<noteq> 0 \<and> m \<noteq> 0" by blast
  from alluopairs_ex[OF Pc, where xs="U"] tnU smU

  then obtain t' n' s' m' where ts'_U: "((t',n'),(s',m')) \<in> set (alluopairs U)" 
    and Pts': "?P (t',n') (s',m')" by blast
  from ts'_U Up have mnz': "m' \<noteq> 0" and nnz': "n'\<noteq> 0" by auto
  let ?st' = "Add (Mul m' t') (Mul n' s')"
    have st': "(?N t' / real n' + ?N s' / real m')/2 = ?N ?st' / real (2*n'*m')"
-   using mnz' nnz' by (simp add: ring_simps add_divide_distrib)
+   using mnz' nnz' by (simp add: algebra_simps add_divide_distrib)
  from Pts' have 
    "(Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" by simp
  also have "\<dots> = ((\<lambda>(t, n). Inum (x # bs) t / real n) ((\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t',n'),(s',m'))))" by (simp add: st')
  finally show "(Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2
           \<in> (\<lambda>(t, n). Inum (x # bs) t / real n) `

   let ?st= "Add (Mul m t) (Mul n s)"
   from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
       by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
     from tnb snb have stnb: "numbound0 ?st" by simp
   have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
-   using mp np by (simp add: ring_simps add_divide_distrib)
+   using mp np by (simp add: algebra_simps add_divide_distrib)
   from tnU smU UU' have "?g ((t,n),(s,m)) \<in> ?f ` U'" by blast
   hence "\<exists> (t',n') \<in> U'. ?g ((t,n),(s,m)) = ?f (t',n')"
     by auto (rule_tac x="(a,b)" in bexI, auto)
   then obtain t' n' where tnU': "(t',n') \<in> U'" and th: "?g ((t,n),(s,m)) = ?f (t',n')" by blast
   from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto

   let ?st= "Add (Mul m t) (Mul n s)"
   from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
       by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
     from tnb snb have stnb: "numbound0 ?st" by simp
   have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
-   using mp np by (simp add: ring_simps add_divide_distrib)
+   using mp np by (simp add: algebra_simps add_divide_distrib)
   from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto
   from \<upsilon>_I[OF lp np' tnb', where bs="bs" and x="x",simplified th[simplified split_def fst_conv snd_conv] st] Pt'
   have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp
   with \<upsilon>_I[OF lp mnp stnb, where x="x" and bs="bs"] tnU smU show ?lhs by blast
 qed