diff -r 839db6346cc8 -r f4b83f03cac9 src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Sat Jun 23 19:33:22 2007 +0200
@@ -533,7 +533,7 @@
 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_eq_simps)
+  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_simps)
 qed (auto simp add: numgcd_def gp)
 consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
 recdef ismaxcoeff "measure size"
@@ -637,8 +637,8 @@
 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_eq_simps)
-by (simp only: ring_eq_simps(1)[symmetric],simp)
+apply (case_tac "n1 = n2", simp_all add: ring_simps)
+by (simp only: left_distrib[symmetric],simp)
 
 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)
@@ -649,7 +649,7 @@
   "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_eq_simps)
+by (induct t rule: nummul.induct, auto simp add: ring_simps)
 
 lemma nummul_nb[simp]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"
 by (induct t rule: nummul.induct, auto )
@@ -1002,10 +1002,10 @@
     by(cases "rsplit0 a",auto simp add: Let_def split_def)
   have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) = 
     Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)"
-    by (simp add: Let_def split_def ring_eq_simps)
+    by (simp add: Let_def split_def ring_simps)
   also have "\<dots> = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a", simp_all)
   finally show ?case using nb by simp 
-qed(auto simp add: Let_def split_def ring_eq_simps , simp add: ring_eq_simps(2)[symmetric])
+qed(auto simp add: Let_def split_def ring_simps , simp add: right_distrib[symmetric])
 
     (* Linearize a formula*)
 consts 
@@ -1370,40 +1370,40 @@
     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_eq_simps)
+      and b="0", simplified divide_zero_left]) (simp only: ring_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_eq_simps)
+  finally show ?case using nbt nb by (simp add: ring_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_eq_simps)
+      and b="0", simplified divide_zero_left]) (simp only: ring_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_eq_simps)
+  finally show ?case using nbt nb by (simp add: ring_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_eq_simps)
+      and b="0", simplified divide_zero_left]) (simp only: ring_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_eq_simps)
+  finally show ?case using nbt nb by (simp add: ring_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_eq_simps)
+      and b="0", simplified divide_zero_left]) (simp only: ring_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_eq_simps)
+  finally show ?case using nbt nb by (simp add: ring_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
@@ -1411,10 +1411,10 @@
     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_eq_simps)
+      and b="0", simplified divide_zero_left]) (simp only: ring_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_eq_simps)
+  finally show ?case using nbt nb by (simp add: ring_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
@@ -1422,10 +1422,10 @@
     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_eq_simps)
+      and b="0", simplified divide_zero_left]) (simp only: ring_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_eq_simps)
+  finally show ?case using nbt nb by (simp add: ring_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 uset_l:
@@ -1476,7 +1476,7 @@
 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_eq_simps)
+    from prems have "x * real c + ?N x e < 0" by (simp add: ring_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
@@ -1485,7 +1485,7 @@
     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_eq_simps)
+      hence "real c * y + ?N x e < 0" by (simp add: ring_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
@@ -1495,7 +1495,7 @@
     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_eq_simps)
+    from prems have "x * real c + ?N x e \<le> 0" by (simp add: ring_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
@@ -1504,7 +1504,7 @@
     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_eq_simps)
+      hence "real c * y + ?N x e < 0" by (simp add: ring_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
@@ -1514,7 +1514,7 @@
     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_eq_simps)
+    from prems have "x * real c + ?N x e > 0" by (simp add: ring_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
@@ -1523,7 +1523,7 @@
     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_eq_simps)
+      hence "real c * y + ?N x e > 0" by (simp add: ring_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
@@ -1533,7 +1533,7 @@
     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_eq_simps)
+    from prems have "x * real c + ?N x e \<ge> 0" by (simp add: ring_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
@@ -1542,7 +1542,7 @@
     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_eq_simps)
+      hence "real c * y + ?N x e > 0" by (simp add: ring_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
@@ -1553,7 +1553,7 @@
 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_eq_simps)
+    from prems have "x * real c + ?N x e = 0" by (simp add: ring_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
@@ -1566,9 +1566,9 @@
     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_eq_simps)
+    hence "y* real c + ?N x e \<noteq> 0" by (simp add: ring_simps)
     thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 
-      by (simp add: ring_eq_simps)
+      by (simp add: ring_simps)
 qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
 
 lemma finite_set_intervals:
@@ -1731,7 +1731,7 @@
 	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_eq_simps add_divide_distrib)
+	using mnp mp np by (simp add: ring_simps add_divide_distrib)
       from usubst_I[OF lp mnp st_nb, where x="x" and bs="bs"] 
       have "?I x (usubst p (?st,2*n*m)) = ?I ((?N t / real n + ?N s / real m) /2) p" by (simp only: st[symmetric])}
     with rinf_uset[OF lp nmi npi px] have "?F" by blast hence "?D" by blast}
@@ -1782,14 +1782,14 @@
   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_eq_simps add_divide_distrib)
+   using mnz nnz by (simp add: ring_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_eq_simps split_def image_def)
+    apply (auto simp add: th add_divide_distrib ring_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
@@ -1800,7 +1800,7 @@
   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_eq_simps add_divide_distrib)
+   using mnz nnz by (simp add: ring_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
@@ -1813,7 +1813,7 @@
  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_eq_simps add_divide_distrib)
+   using mnz' nnz' by (simp add: ring_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')
@@ -1843,7 +1843,7 @@
       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_eq_simps add_divide_distrib)
+   using mp np by (simp add: ring_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)
@@ -1871,7 +1871,7 @@
       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_eq_simps add_divide_distrib)
+   using mp np by (simp add: ring_simps add_divide_distrib)
   from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto
   from usubst_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
@@ -1972,8 +1972,6 @@
 using ferrack qelim_ci prep
 unfolding linrqe_def by auto
 
-declare max_def [code unfold]
-
 code_module Ferrack
 file "generated_ferrack.ML"
 contains linrqe = "linrqe"