# HG changeset patch
# User huffman
# Date 1266531704 28800
# Node ID 7641e8d831d2754af71de9f2cbc438bcef8ee0a4
# Parent  a03462cbf86f25c2278e784a3dc0890a9eb3651f
get rid of many duplicate simp rule warnings

diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Datatype.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -144,11 +144,10 @@
 (** Scons vs Atom **)
 
 lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)"
-apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def)
-apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
+unfolding Atom_def Scons_def Push_Node_def One_nat_def
+by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
          dest!: Abs_Node_inj 
          elim!: apfst_convE sym [THEN Push_neq_K0])  
-done
 
 lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard]
 
@@ -199,14 +198,12 @@
 (** Injectiveness of Scons **)
 
 lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'"
-apply (simp add: Scons_def One_nat_def)
-apply (blast dest!: Push_Node_inject)
-done
+unfolding Scons_def One_nat_def
+by (blast dest!: Push_Node_inject)
 
 lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'"
-apply (simp add: Scons_def One_nat_def)
-apply (blast dest!: Push_Node_inject)
-done
+unfolding Scons_def One_nat_def
+by (blast dest!: Push_Node_inject)
 
 lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
 apply (erule equalityE)
@@ -230,14 +227,14 @@
 (** Scons vs Leaf **)
 
 lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
-by (simp add: Leaf_def o_def Scons_not_Atom)
+unfolding Leaf_def o_def by (rule Scons_not_Atom)
 
 lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym, standard]
 
 (** Scons vs Numb **)
 
 lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
-by (simp add: Numb_def o_def Scons_not_Atom)
+unfolding Numb_def o_def by (rule Scons_not_Atom)
 
 lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard]
 
@@ -281,14 +278,15 @@
 by (auto simp add: Atom_def ntrunc_def ndepth_K0)
 
 lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)"
-by (simp add: Leaf_def o_def ntrunc_Atom)
+unfolding Leaf_def o_def by (rule ntrunc_Atom)
 
 lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)"
-by (simp add: Numb_def o_def ntrunc_Atom)
+unfolding Numb_def o_def by (rule ntrunc_Atom)
 
 lemma ntrunc_Scons [simp]: 
     "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"
-by (auto simp add: Scons_def ntrunc_def One_nat_def ndepth_Push_Node) 
+unfolding Scons_def ntrunc_def One_nat_def
+by (auto simp add: ndepth_Push_Node)
 
 
 
@@ -351,7 +349,7 @@
 (** Injection **)
 
 lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
-by (auto simp add: In0_def In1_def One_nat_def)
+unfolding In0_def In1_def One_nat_def by auto
 
 lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard]
 
@@ -417,10 +415,10 @@
 by (simp add: Scons_def, blast)
 
 lemma In0_mono: "M<=N ==> In0(M) <= In0(N)"
-by (simp add: In0_def subset_refl Scons_mono)
+by (simp add: In0_def Scons_mono)
 
 lemma In1_mono: "M<=N ==> In1(M) <= In1(N)"
-by (simp add: In1_def subset_refl Scons_mono)
+by (simp add: In1_def Scons_mono)
 
 
 (*** Split and Case ***)
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Deriv.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -260,7 +260,7 @@
           -- x --> d (f x) * D"
     by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]])
   thus "(\<lambda>z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D"
-    by (simp add: d dfx real_scaleR_def)
+    by (simp add: d dfx)
 qed
 
 text {*
@@ -279,7 +279,7 @@
 
 text {* Standard version *}
 lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
-by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute)
+by (drule (1) DERIV_chain', simp add: o_def mult_commute)
 
 lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
 by (auto dest: DERIV_chain simp add: o_def)
@@ -290,7 +290,7 @@
 
 lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
 apply (cut_tac DERIV_power [OF DERIV_ident])
-apply (simp add: real_scaleR_def real_of_nat_def)
+apply (simp add: real_of_nat_def)
 done
 
 text {* Power of @{text "-1"} *}
@@ -1532,12 +1532,12 @@
   moreover
   have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
   proof -
-    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by (simp add: differentiable_const)
-    with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by (simp add: differentiable_mult)
+    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by simp
+    with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by simp
     moreover
-    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by (simp add: differentiable_const)
-    with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by (simp add: differentiable_mult)
-    ultimately show ?thesis by (simp add: differentiable_diff)
+    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by simp
+    with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by simp
+    ultimately show ?thesis by simp
   qed
   ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT)
   then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Divides.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -1090,7 +1090,7 @@
 lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
 apply (subgoal_tac "m mod 2 < 2")
 apply (erule less_2_cases [THEN disjE])
-apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
+apply (simp_all (no_asm_simp) add: Let_def mod_Suc)
 done
 
 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
@@ -1929,7 +1929,7 @@
 apply (rule order_le_less_trans)
  apply (erule_tac [2] mult_strict_right_mono)
  apply (rule mult_left_mono_neg)
-  using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps pos_mod_bound)
+  using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
  apply (simp)
 apply (simp)
 done
@@ -1954,7 +1954,7 @@
  apply (erule mult_strict_right_mono)
  apply (rule_tac [2] mult_left_mono)
   apply simp
- using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps pos_mod_bound)
+ using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
 apply simp
 done
 
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Equiv_Relations.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -328,7 +328,7 @@
    apply assumption
   apply simp
  apply(fastsimp simp add:inj_on_def)
-apply (simp add:setsum_constant)
+apply simp
 done
 
 end
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Fields.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -230,7 +230,7 @@
 lemma inverse_minus_eq [simp]:
    "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
 proof cases
-  assume "a=0" thus ?thesis by (simp add: inverse_zero)
+  assume "a=0" thus ?thesis by simp
 next
   assume "a\<noteq>0" 
   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
@@ -283,13 +283,13 @@
 lemma mult_divide_mult_cancel_left:
   "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
 apply (cases "b = 0")
-apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
+apply simp_all
 done
 
 lemma mult_divide_mult_cancel_right:
   "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
 apply (cases "b = 0")
-apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
+apply simp_all
 done
 
 lemma divide_divide_eq_right [simp,noatp]:
@@ -339,7 +339,7 @@
 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::linordered_field)"
 proof -
   have "0 < a * inverse a" 
-    by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
+    by (simp add: a_gt_0 [THEN order_less_imp_not_eq2])
   thus "0 < inverse a" 
     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
 qed
@@ -524,8 +524,7 @@
 
 lemma one_le_inverse_iff:
   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{linordered_field,division_by_zero}))"
-by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
-                    eq_commute [of 1]) 
+by (force simp add: order_le_less one_less_inverse_iff)
 
 lemma inverse_less_1_iff:
   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{linordered_field,division_by_zero}))"
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Finite_Set.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -355,7 +355,7 @@
   apply (induct set: finite)
    apply simp_all
   apply (subst vimage_insert)
-  apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
+  apply (simp add: finite_subset [OF inj_vimage_singleton])
   done
 
 lemma finite_vimageD:
@@ -485,7 +485,7 @@
 next
   assume "finite A"
   thus "finite (Pow A)"
-    by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
+    by induct (simp_all add: Pow_insert)
 qed
 
 lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
@@ -634,7 +634,7 @@
   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
   let ?hm = "Fun.swap k m h"
   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
-    by (simp add: inj_on_swap_iff inj_on)
+    by (simp add: inj_on)
   show ?thesis
   proof (intro exI conjI)
     show "inj_on ?hm {i. i < m}" using inj_hm
@@ -764,7 +764,7 @@
 
 lemma fold_insert2:
   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
-by (simp add: fold_insert fold_fun_comm)
+by (simp add: fold_fun_comm)
 
 lemma fold_rec:
 assumes "finite A" and "x \<in> A"
@@ -824,8 +824,8 @@
 
 lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
 apply unfold_locales
- apply (simp add: mult_ac)
-apply (simp add: mult_idem mult_assoc[symmetric])
+ apply (rule mult_left_commute)
+apply (rule mult_left_idem)
 done
 
 end
@@ -1366,7 +1366,7 @@
 
 lemma (in comm_monoid_mult) fold_image_1: "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
   apply (induct set: finite)
-  apply simp by (auto simp add: fold_image_insert)
+  apply simp by auto
 
 lemma (in comm_monoid_mult) fold_image_Un_one:
   assumes fS: "finite S" and fT: "finite T"
@@ -1412,8 +1412,8 @@
 next
   case (2 T F)
   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
-    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert)
-  from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union)
+    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
+  from fTF have fUF: "finite (\<Union>F)" by auto
   from "2.prems" TF fTF
   show ?case 
     by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
@@ -2056,7 +2056,7 @@
   shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
 proof (cases "finite A")
   case True thus ?thesis
-    by induct (auto simp add: field_simps setprod_insert abs_mult)
+    by induct (auto simp add: field_simps abs_mult)
 qed auto
 
 
@@ -2215,7 +2215,7 @@
      (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
      k * card(C) = card (\<Union> C)"
 apply (erule finite_induct, simp)
-apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
+apply (simp add: card_Un_disjoint insert_partition 
        finite_subset [of _ "\<Union> (insert x F)"])
 done
 
@@ -2285,7 +2285,7 @@
 
 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
 apply (erule finite_induct)
-apply (auto simp add: power_Suc)
+apply auto
 done
 
 lemma setprod_gen_delta:
@@ -2370,7 +2370,7 @@
 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
 apply (induct set: finite)
  apply simp
-apply (simp add: le_SucI finite_imageI card_insert_if)
+apply (simp add: le_SucI card_insert_if)
 done
 
 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
@@ -2473,7 +2473,7 @@
 apply(rotate_tac -1)
 apply (induct set: finite, simp_all, clarify)
 apply (subst card_Un_disjoint)
-   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
+   apply (auto simp add: disjoint_eq_subset_Compl)
 done
 
 
@@ -2514,7 +2514,7 @@
   ultimately have "finite (UNIV::nat set)"
     by (rule finite_imageD)
   then show "False"
-    by (simp add: infinite_UNIV_nat)
+    by simp
 qed
 
 subsection{* A fold functional for non-empty sets *}
@@ -2542,7 +2542,7 @@
 
 
 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
-by (blast intro: fold_graph.intros elim: fold_graph.cases)
+by (blast elim: fold_graph.cases)
 
 lemma fold1_singleton [simp]: "fold1 f {a} = a"
 by (unfold fold1_def) blast
@@ -2612,9 +2612,9 @@
 apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times])
 apply (rule sym, clarify)
 apply (case_tac "Aa=A")
- apply (best intro: the_equality fold_graph_determ)
+ apply (best intro: fold_graph_determ)
 apply (subgoal_tac "fold_graph times a A x")
- apply (best intro: the_equality fold_graph_determ)
+ apply (best intro: fold_graph_determ)
 apply (subgoal_tac "insert aa (Aa - {a}) = A")
  prefer 2 apply (blast elim: equalityE)
 apply (auto dest: fold_graph_permute_diff [where a=a])
@@ -2658,16 +2658,16 @@
     thus ?thesis
     proof cases
       assume "A' = {}"
-      with prems show ?thesis by (simp add: mult_idem)
+      with prems show ?thesis by simp
     next
       assume "A' \<noteq> {}"
       with prems show ?thesis
-        by (simp add: fold1_insert mult_assoc [symmetric] mult_idem)
+        by (simp add: fold1_insert mult_assoc [symmetric])
     qed
   next
     assume "a \<noteq> x"
     with prems show ?thesis
-      by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
+      by (simp add: insert_commute fold1_eq_fold)
   qed
 qed
 
@@ -2710,7 +2710,7 @@
 text{* Now the recursion rules for definitions: *}
 
 lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
-by(simp add:fold1_singleton)
+by simp
 
 lemma (in ab_semigroup_mult) fold1_insert_def:
   "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/GCD.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -156,7 +156,7 @@
       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   shows "P (gcd x y)"
-by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith)
+by (insert assms, auto, arith)
 
 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   by (simp add: gcd_int_def)
@@ -457,7 +457,7 @@
   apply (case_tac "y > 0")
   apply (subst gcd_non_0_int, auto)
   apply (insert gcd_non_0_int [of "-y" "-x"])
-  apply (auto simp add: gcd_neg1_int gcd_neg2_int)
+  apply auto
 done
 
 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
@@ -557,7 +557,7 @@
   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
-  have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat)
+  have "?g \<noteq> 0" using nz by simp
   then have gp: "?g > 0" by arith
   from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
@@ -824,7 +824,7 @@
   {assume "?g = 0" with ab n have ?thesis by auto }
   moreover
   {assume z: "?g \<noteq> 0"
-    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
+    hence zn: "?g ^ n \<noteq> 0" using n by simp
     from gcd_coprime_exists_nat[OF z]
     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
       by blast
@@ -852,7 +852,7 @@
   {assume "?g = 0" with ab n have ?thesis by auto }
   moreover
   {assume z: "?g \<noteq> 0"
-    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
+    hence zn: "?g ^ n \<noteq> 0" using n by simp
     from gcd_coprime_exists_int[OF z]
     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
       by blast
@@ -1109,7 +1109,7 @@
     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
   using ex
   apply clarsimp
-  apply (rule_tac x="d" in exI, simp add: dvd_add)
+  apply (rule_tac x="d" in exI, simp)
   apply (case_tac "a * x = b * y + d" , simp_all)
   apply (rule_tac x="x + y" in exI)
   apply (rule_tac x="y" in exI)
@@ -1124,10 +1124,10 @@
   apply(induct a b rule: ind_euclid)
   apply blast
   apply clarify
-  apply (rule_tac x="a" in exI, simp add: dvd_add)
+  apply (rule_tac x="a" in exI, simp)
   apply clarsimp
   apply (rule_tac x="d" in exI)
-  apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
+  apply (case_tac "a * x = b * y + d", simp_all)
   apply (rule_tac x="x+y" in exI)
   apply (rule_tac x="y" in exI)
   apply algebra
@@ -1693,8 +1693,7 @@
   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
 apply(auto simp add:inj_on_def)
-apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
-             dvd.neq_le_trans dvd_triv_left)
+apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
 apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
              dvd.neq_le_trans dvd_triv_right mult_commute)
 done
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Groebner_Basis.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -143,16 +143,16 @@
 next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr)
 next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp
 next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp
-next show "mul x x = pwr x 2" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
+next show "mul x x = pwr x 2" by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
 next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
 next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
 next show "pwr x 0 = r1" using pwr_0 .
-next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
+next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
 next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
 next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
-next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)
+next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number' mul_pwr)
 next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))"
-    by (simp add: nat_number pwr_Suc mul_pwr)
+    by (simp add: nat_number' pwr_Suc mul_pwr)
 qed
 
 
@@ -165,7 +165,7 @@
 
 interpretation class_semiring: gb_semiring
     "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1"
-  proof qed (auto simp add: algebra_simps power_Suc)
+  proof qed (auto simp add: algebra_simps)
 
 lemmas nat_arith =
   add_nat_number_of
@@ -175,7 +175,7 @@
   less_nat_number_of
 
 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
-  by (simp add: numeral_1_eq_1)
+  by simp
 
 lemmas comp_arith =
   Let_def arith_simps nat_arith rel_simps neg_simps if_False
@@ -350,7 +350,7 @@
 
 interpretation class_ringb: ringb
   "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
-proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
+proof(unfold_locales, simp add: algebra_simps, auto)
   fix w x y z ::"'a::{idom,number_ring}"
   assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
   hence ynz': "y - z \<noteq> 0" by simp
@@ -366,7 +366,7 @@
 
 interpretation natgb: semiringb
   "op +" "op *" "op ^" "0::nat" "1"
-proof (unfold_locales, simp add: algebra_simps power_Suc)
+proof (unfold_locales, simp add: algebra_simps)
   fix w x y z ::"nat"
   { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
     hence "y < z \<or> y > z" by arith
@@ -375,13 +375,13 @@
       then obtain k where kp: "k>0" and yz:"z = y + k" by blast
       from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps)
       hence "x*k = w*k" by simp
-      hence "w = x" using kp by (simp add: mult_cancel2) }
+      hence "w = x" using kp by simp }
     moreover {
       assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
       then obtain k where kp: "k>0" and yz:"y = z + k" by blast
       from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps)
       hence "w*k = x*k" by simp
-      hence "w = x" using kp by (simp add: mult_cancel2)}
+      hence "w = x" using kp by simp }
     ultimately have "w=x" by blast }
   thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
 qed
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Groups.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -347,6 +347,8 @@
 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
 by (simp add: algebra_simps)
 
+(* FIXME: duplicates right_minus_eq from class group_add *)
+(* but only this one is declared as a simp rule. *)
 lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \<longleftrightarrow> a = b"
 by (simp add: algebra_simps)
 
@@ -794,7 +796,7 @@
 proof
   assume assm: "a + a = 0"
   then have a: "- a = a" by (rule minus_unique)
-  then show "a = 0" by (simp add: neg_equal_zero)
+  then show "a = 0" by (simp only: neg_equal_zero)
 qed simp
 
 lemma double_zero_sym [simp]:
@@ -807,7 +809,7 @@
   assume "0 < a + a"
   then have "0 - a < a" by (simp only: diff_less_eq)
   then have "- a < a" by simp
-  then show "0 < a" by (simp add: neg_less_nonneg)
+  then show "0 < a" by (simp only: neg_less_nonneg)
 next
   assume "0 < a"
   with this have "0 + 0 < a + a"
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Hilbert_Choice.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -61,7 +61,7 @@
 by (blast intro: someI2)
 
 lemma some1_equality: "[| EX!x. P x; P a |] ==> (SOME x. P x) = a"
-by (blast intro: some_equality)
+by blast
 
 lemma some_eq_ex: "P (SOME x. P x) =  (\<exists>x. P x)"
 by (blast intro: someI)
@@ -108,7 +108,7 @@
 done
 
 lemma inv_f_f: "inj f ==> inv f (f x) = x"
-by (simp add: inv_into_f_f)
+by simp
 
 lemma f_inv_into_f: "y : f`A  ==> f (inv_into A f y) = y"
 apply (simp add: inv_into_def)
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Int.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -391,6 +391,7 @@
 lemma nat_int [simp]: "nat (of_nat n) = n"
 by (simp add: nat int_def)
 
+(* FIXME: duplicates nat_0 *)
 lemma nat_zero [simp]: "nat 0 = 0"
 by (simp add: Zero_int_def nat)
 
@@ -626,10 +627,10 @@
 
 lemmas
   max_number_of [simp] = max_def
-    [of "number_of u" "number_of v", standard, simp]
+    [of "number_of u" "number_of v", standard]
 and
   min_number_of [simp] = min_def 
-    [of "number_of u" "number_of v", standard, simp]
+    [of "number_of u" "number_of v", standard]
   -- {* unfolding @{text minx} and @{text max} on numerals *}
 
 lemmas numeral_simps = 
@@ -1060,7 +1061,7 @@
 lemma not_iszero_1: "~ iszero 1"
 by (simp add: iszero_def eq_commute)
 
-lemma eq_number_of_eq:
+lemma eq_number_of_eq [simp]:
   "((number_of x::'a::number_ring) = number_of y) =
    iszero (number_of (x + uminus y) :: 'a)"
 unfolding iszero_def number_of_add number_of_minus
@@ -1130,7 +1131,7 @@
     by (auto simp add: iszero_def number_of_eq numeral_simps)
 qed
 
-lemmas iszero_simps =
+lemmas iszero_simps [simp] =
   iszero_0 not_iszero_1
   iszero_number_of_Pls nonzero_number_of_Min
   iszero_number_of_Bit0 iszero_number_of_Bit1
@@ -1218,7 +1219,7 @@
   "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y"
   unfolding number_of_eq by (rule of_int_eq_iff)
 
-lemmas rel_simps [simp] = 
+lemmas rel_simps =
   less_number_of less_bin_simps
   le_number_of le_bin_simps
   eq_number_of_eq eq_bin_simps
@@ -1240,7 +1241,7 @@
 lemma add_number_of_diff1:
   "number_of v + (number_of w - c) = 
   number_of(v + w) - (c::'a::number_ring)"
-  by (simp add: diff_minus add_number_of_left)
+  by (simp add: diff_minus)
 
 lemma add_number_of_diff2 [simp]:
   "number_of v + (c - number_of w) =
@@ -1437,7 +1438,7 @@
 
 text{*Allow 1 on either or both sides*}
 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
-by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
+by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric])
 
 lemmas add_special =
     one_add_one_is_two
@@ -1558,6 +1559,7 @@
 
 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
 
+(* FIXME: duplicates nat_zero *)
 lemma nat_0: "nat 0 = 0"
 by (simp add: nat_eq_iff)
 
@@ -1980,7 +1982,7 @@
 
 lemma minus1_divide [simp]:
      "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
-by (simp add: divide_inverse inverse_minus_eq)
+by (simp add: divide_inverse)
 
 lemma half_gt_zero_iff:
      "(0 < r/2) = (0 < (r::'a::{linordered_field,division_by_zero,number_ring}))"
@@ -2098,7 +2100,7 @@
   assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
 proof
   assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
-    by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
+    by (cases "n >0", auto simp add: minus_equation_iff)
 next
   assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/List.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -257,9 +257,9 @@
 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
-@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\
-@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\
-@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\
+@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\
+@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\
+@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\
 @{lemma "listsum [1,2,3::nat] = 6" by simp}
 \end{tabular}}
 \caption{Characteristic examples}
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Nat.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -1356,7 +1356,7 @@
 end
 
 lemma of_nat_id [simp]: "of_nat n = n"
-  by (induct n) (auto simp add: One_nat_def)
+  by (induct n) simp_all
 
 lemma of_nat_eq_id [simp]: "of_nat = id"
   by (auto simp add: expand_fun_eq)
@@ -1619,7 +1619,7 @@
 
 lemma dvd_antisym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   unfolding dvd_def
-  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
+  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc)
 
 text {* @{term "op dvd"} is a partial order *}
 
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Nat_Numeral.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -211,7 +211,7 @@
   "0 \<le> a ^ (2*n)"
 proof (induct n)
   case 0
-    show ?case by (simp add: zero_le_one)
+    show ?case by simp
 next
   case (Suc n)
     have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
@@ -262,7 +262,7 @@
 by (simp add: neg_def)
 
 lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
-by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
+by (simp add: neg_def del: of_nat_Suc)
 
 lemmas neg_eq_less_0 = neg_def
 
@@ -275,7 +275,7 @@
 by (simp add: One_int_def neg_def)
 
 lemma not_neg_1: "~ neg 1"
-by (simp add: neg_def linorder_not_less zero_le_one)
+by (simp add: neg_def linorder_not_less)
 
 lemma neg_nat: "neg z ==> nat z = 0"
 by (simp add: neg_def order_less_imp_le) 
@@ -310,7 +310,7 @@
 
 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
 
-declare nat_0 [simp] nat_1 [simp]
+declare nat_1 [simp]
 
 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
 by (simp add: nat_number_of_def)
@@ -319,10 +319,10 @@
 by (simp add: nat_number_of_def)
 
 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
-by (simp add: nat_1 nat_number_of_def)
+by (simp add: nat_number_of_def)
 
 lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
-by (simp add: nat_numeral_1_eq_1)
+by (simp only: nat_numeral_1_eq_1 One_nat_def)
 
 
 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
@@ -469,7 +469,7 @@
 subsubsection{*Nat *}
 
 lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
-by (simp add: numerals)
+by simp
 
 (*Expresses a natural number constant as the Suc of another one.
   NOT suitable for rewriting because n recurs in the condition.*)
@@ -478,10 +478,10 @@
 subsubsection{*Arith *}
 
 lemma Suc_eq_plus1: "Suc n = n + 1"
-by (simp add: numerals)
+  unfolding One_nat_def by simp
 
 lemma Suc_eq_plus1_left: "Suc n = 1 + n"
-by (simp add: numerals)
+  unfolding One_nat_def by simp
 
 (* These two can be useful when m = number_of... *)
 
@@ -563,13 +563,13 @@
      "(number_of v <= Suc n) =  
         (let pv = number_of (Int.pred v) in  
          if neg pv then True else nat pv <= n)"
-by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
+by (simp add: Let_def linorder_not_less [symmetric])
 
 lemma le_Suc_number_of [simp]:
      "(Suc n <= number_of v) =  
         (let pv = number_of (Int.pred v) in  
          if neg pv then False else n <= nat pv)"
-by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
+by (simp add: Let_def linorder_not_less [symmetric])
 
 
 lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
@@ -660,7 +660,7 @@
     power_number_of_odd [of "number_of v", standard]
 
 lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
-  by (simp add: number_of_Pls nat_number_of_def)
+  by (simp add: nat_number_of_def)
 
 lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
@@ -684,6 +684,9 @@
   nat_number_of_Pls nat_number_of_Min
   nat_number_of_Bit0 nat_number_of_Bit1
 
+lemmas nat_number' =
+  nat_number_of_Bit0 nat_number_of_Bit1
+
 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   by (fact Let_def)
 
@@ -736,7 +739,7 @@
 text{*Where K above is a literal*}
 
 lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
-by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
+by (simp split: nat_diff_split)
 
 text {*Now just instantiating @{text n} to @{text "number_of v"} does
   the right simplification, but with some redundant inequality
@@ -761,7 +764,7 @@
 done
 
 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
-by (simp add: numerals split add: nat_diff_split)
+by (simp split: nat_diff_split)
 
 
 subsubsection{*For @{term nat_case} and @{term nat_rec}*}
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/NthRoot.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -566,7 +566,7 @@
 done
 
 lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
-by (simp add: divide_less_eq mult_compare_simps)
+by (simp add: divide_less_eq)
 
 lemma four_x_squared: 
   fixes x::real
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/PReal.thy
--- a/src/HOL/PReal.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/PReal.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -750,7 +750,7 @@
   have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)" 
   proof -
     have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
-      by (simp add: mult_rat le_rat order_less_imp_not_eq2 mult_ac) 
+      by (simp add: order_less_imp_not_eq2 mult_ac) 
     moreover
     have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
       by (rule mult_mono, 
@@ -822,7 +822,7 @@
       also with ypos have "... = (r/y) * (y + ?d)"
         by (simp only: algebra_simps divide_inverse, simp)
       also have "... = r*x" using ypos
-        by (simp add: times_divide_eq_left) 
+        by simp
       finally show "r + ?d < r*x" .
     qed
     with r notin rdpos
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Parity.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -184,7 +184,7 @@
   apply (rule conjI)
   apply simp
   apply (insert even_zero_nat, blast)
-  apply (simp add: power_Suc)
+  apply simp
   done
 
 lemma minus_one_even_power [simp]:
@@ -199,7 +199,7 @@
      "(even x --> (-1::'a::{number_ring})^x = 1) &
       (odd x --> (-1::'a)^x = -1)"
   apply (induct x)
-  apply (simp, simp add: power_Suc)
+  apply (simp, simp)
   done
 
 lemma neg_one_even_power [simp]:
@@ -214,7 +214,7 @@
      "(-x::'a::{comm_ring_1}) ^ n =
       (if even n then (x ^ n) else -(x ^ n))"
   apply (induct n)
-  apply (simp_all split: split_if_asm add: power_Suc)
+  apply simp_all
   done
 
 lemma zero_le_even_power: "even n ==>
@@ -228,7 +228,7 @@
 
 lemma zero_le_odd_power: "odd n ==>
     (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)"
-apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
+apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff)
 apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
 done
 
@@ -373,7 +373,7 @@
 
 lemma even_power_le_0_imp_0:
     "a ^ (2*k) \<le> (0::'a::{linordered_idom}) ==> a=0"
-  by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)
+  by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
 
 lemma zero_le_power_iff[presburger]:
   "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)"
@@ -387,7 +387,7 @@
   then obtain k where "n = Suc(2*k)"
     by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
   thus ?thesis
-    by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power
+    by (auto simp add: zero_le_mult_iff zero_le_even_power
              dest!: even_power_le_0_imp_0)
 qed
 
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Power.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -332,7 +332,7 @@
 
 lemma abs_power_minus [simp]:
   "abs ((-a) ^ n) = abs (a ^ n)"
-  by (simp add: abs_minus_cancel power_abs) 
+  by (simp add: power_abs)
 
 lemma zero_less_power_abs_iff [simp, noatp]:
   "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Presburger.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -199,16 +199,16 @@
     hence "P 0" using P Pmod by simp
     moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
     ultimately have "P d" by simp
-    moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
+    moreover have "d : {1..d}" using dpos by simp
     ultimately show ?RHS ..
   next
     assume not0: "x mod d \<noteq> 0"
-    have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
+    have "P(x mod d)" using dpos P Pmod by simp
     moreover have "x mod d : {1..d}"
     proof -
       from dpos have "0 \<le> x mod d" by(rule pos_mod_sign)
       moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
-      ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
+      ultimately show ?thesis using not0 by simp
     qed
     ultimately show ?RHS ..
   qed
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Rational.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -428,7 +428,7 @@
   fix q :: rat
   assume "q \<noteq> 0"
   then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero)
-   (simp_all add: mult_rat  inverse_rat rat_number_expand eq_rat)
+   (simp_all add: rat_number_expand eq_rat)
 next
   fix q r :: rat
   show "q / r = q * inverse r" by (simp add: divide_rat_def)
@@ -592,7 +592,7 @@
   abs_rat_def [code del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
 
 lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
-  by (auto simp add: abs_rat_def zabs_def Zero_rat_def less_rat not_less le_less minus_rat eq_rat zero_compare_simps)
+  by (auto simp add: abs_rat_def zabs_def Zero_rat_def not_less le_less eq_rat zero_less_mult_iff)
 
 definition
   sgn_rat_def [code del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/RealDef.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -767,7 +767,8 @@
 lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
 by (simp add: add: real_of_nat_def)
 
-lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat))"
+(* FIXME: duplicates real_of_nat_ge_zero *)
+lemma real_of_nat_ge_zero_cancel_iff: "(0 \<le> real (n::nat))"
 by (simp add: add: real_of_nat_def)
 
 lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
@@ -951,13 +952,13 @@
 
 text{*Collapse applications of @{term real} to @{term number_of}*}
 lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
-by (simp add:  real_of_int_def of_int_number_of_eq)
+by (simp add: real_of_int_def)
 
 lemma real_of_nat_number_of [simp]:
      "real (number_of v :: nat) =  
         (if neg (number_of v :: int) then 0  
          else (number_of v :: real))"
-by (simp add: real_of_int_real_of_nat [symmetric] int_nat_number_of)
+by (simp add: real_of_int_real_of_nat [symmetric])
 
 declaration {*
   K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/RealPow.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -19,8 +19,8 @@
 apply (induct "n")
 apply (auto simp add: real_of_nat_Suc)
 apply (subst mult_2)
-apply (rule add_less_le_mono)
-apply (auto simp add: two_realpow_ge_one)
+apply (erule add_less_le_mono)
+apply (rule two_realpow_ge_one)
 done
 
 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
@@ -57,7 +57,7 @@
 
 lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
 apply (induct "n")
-apply (auto simp add: real_of_nat_mult zero_less_mult_iff)
+apply (auto simp add: zero_less_mult_iff)
 done
 
 (* used by AFP Integration theory *)
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/RealVector.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -268,7 +268,7 @@
 by (induct n) simp_all
 
 lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
-by (simp add: of_real_def scaleR_cancel_right)
+by (simp add: of_real_def)
 
 lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
 
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Rings.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -315,7 +315,7 @@
 qed
 
 lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
-by (simp add: diff_minus dvd_minus_iff)
+by (simp only: diff_minus dvd_add dvd_minus_iff)
 
 end
 
@@ -336,16 +336,16 @@
   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
 proof -
   have "(a * c = b * c) = ((a - b) * c = 0)"
-    by (simp add: algebra_simps right_minus_eq)
-  thus ?thesis by (simp add: disj_commute right_minus_eq)
+    by (simp add: algebra_simps)
+  thus ?thesis by (simp add: disj_commute)
 qed
 
 lemma mult_cancel_left [simp, noatp]:
   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
 proof -
   have "(c * a = c * b) = (c * (a - b) = 0)"
-    by (simp add: algebra_simps right_minus_eq)
-  thus ?thesis by (simp add: right_minus_eq)
+    by (simp add: algebra_simps)
+  thus ?thesis by simp
 qed
 
 end
@@ -382,7 +382,7 @@
   then have "(a - b) * (a + b) = 0"
     by (simp add: algebra_simps)
   then show "a = b \<or> a = - b"
-    by (simp add: right_minus_eq eq_neg_iff_add_eq_0)
+    by (simp add: eq_neg_iff_add_eq_0)
 next
   assume "a = b \<or> a = - b"
   then show "a * a = b * b" by auto
@@ -764,13 +764,13 @@
 lemma mult_left_mono_neg:
   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   apply (drule mult_left_mono [of _ _ "uminus c"])
-  apply (simp_all add: minus_mult_left [symmetric]) 
+  apply simp_all
   done
 
 lemma mult_right_mono_neg:
   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   apply (drule mult_right_mono [of _ _ "uminus c"])
-  apply (simp_all add: minus_mult_right [symmetric]) 
+  apply simp_all
   done
 
 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
@@ -791,11 +791,10 @@
 proof
   fix a b
   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
-    by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
-    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
-     neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
-      auto intro!: less_imp_le add_neg_neg)
-qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
+    by (auto simp add: abs_if not_less)
+    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
+     auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
+qed (auto simp add: abs_if)
 
 end
 
@@ -864,14 +863,14 @@
 
 lemma mult_less_0_iff:
   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
-  apply (insert zero_less_mult_iff [of "-a" b]) 
-  apply (force simp add: minus_mult_left[symmetric]) 
+  apply (insert zero_less_mult_iff [of "-a" b])
+  apply force
   done
 
 lemma mult_le_0_iff:
   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   apply (insert zero_le_mult_iff [of "-a" b]) 
-  apply (force simp add: minus_mult_left[symmetric]) 
+  apply force
   done
 
 lemma zero_le_square [simp]: "0 \<le> a * a"
@@ -1056,11 +1055,11 @@
 
 lemma sgn_1_pos:
   "sgn a = 1 \<longleftrightarrow> a > 0"
-unfolding sgn_if by (simp add: neg_equal_zero)
+unfolding sgn_if by simp
 
 lemma sgn_1_neg:
   "sgn a = - 1 \<longleftrightarrow> a < 0"
-unfolding sgn_if by (auto simp add: equal_neg_zero)
+unfolding sgn_if by auto
 
 lemma sgn_pos [simp]:
   "0 < a \<Longrightarrow> sgn a = 1"
@@ -1116,11 +1115,11 @@
 
 lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
     ==> x * y <= x"
-by (auto simp add: mult_compare_simps)
+by (auto simp add: mult_le_cancel_left2)
 
 lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
     ==> y * x <= x"
-by (auto simp add: mult_compare_simps)
+by (auto simp add: mult_le_cancel_right2)
 
 context linordered_semidom
 begin
@@ -1159,7 +1158,7 @@
 begin
 
 subclass ordered_ring_abs proof
-qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)
+qed (auto simp add: abs_if not_less mult_less_0_iff)
 
 lemma abs_mult:
   "abs (a * b) = abs a * abs b" 
@@ -1187,7 +1186,7 @@
 
 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))" 
 apply (simp add: order_less_le abs_le_iff)  
-apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
+apply (auto simp add: abs_if)
 done
 
 lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> 
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/SEQ.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -573,7 +573,7 @@
 apply (rule allI, rule impI, rule ext)
 apply (erule conjE)
 apply (induct_tac x)
-apply (simp add: nat_rec_0)
+apply simp
 apply (erule_tac x="n" in allE)
 apply (simp)
 done
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/SetInterval.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -539,7 +539,7 @@
   apply (rule subset_antisym)
    apply (rule UN_finite2_subset, blast)
  apply (rule UN_finite2_subset [where k=k])
- apply (force simp add: atLeastLessThan_add_Un [of 0] UN_Un) 
+ apply (force simp add: atLeastLessThan_add_Un [of 0])
  done
 
 
@@ -613,7 +613,7 @@
   apply (unfold image_def lessThan_def)
   apply auto
   apply (rule_tac x = "nat x" in exI)
-  apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym])
+  apply (auto simp add: zless_nat_eq_int_zless [THEN sym])
   done
 
 lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
@@ -1006,7 +1006,7 @@
   shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
 proof-
   have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)
-  also have "\<dots> = ?r" by(simp add: setsum_constant mult_commute)
+  also have "\<dots> = ?r" by(simp add: mult_commute)
   finally show ?thesis by auto
 qed
 
@@ -1046,7 +1046,7 @@
 lemma geometric_sum:
   "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
   (x ^ n - 1) / (x - 1::'a::{field})"
-by (induct "n") (simp_all add:field_simps power_Suc)
+by (induct "n") (simp_all add: field_simps)
 
 subsection {* The formula for arithmetic sums *}
 
@@ -1098,7 +1098,7 @@
     of_nat(n) * (a + (a + of_nat(n - 1)*d))"
     by (rule arith_series_general)
   thus ?thesis
-    unfolding One_nat_def by (auto simp add: of_nat_id)
+    unfolding One_nat_def by auto
 qed
 
 lemma arith_series_int:
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/SupInf.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -249,7 +249,7 @@
       and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
   shows "z \<le> Inf X"
 proof -
-  have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
+  have "Sup (uminus ` X) \<le> -z" using x z by force
   hence "z \<le> - Sup (uminus ` X)"
     by simp
   thus ?thesis 
@@ -306,7 +306,7 @@
   case True
   thus ?thesis
     by (simp add: min_def)
-       (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z) 
+       (blast intro: Inf_eq_minimum real_le_refl real_le_trans z)
 next
   case False
   hence 1:"Inf X < a" by simp
@@ -441,7 +441,7 @@
 proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
   show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
     by (rule SupInf.Sup_upper [where z=b], auto)
-       (metis prems real_le_linear real_less_def) 
+       (metis `a < b` `\<not> P b` real_le_linear real_less_def)
 next
   show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
     apply (rule SupInf.Sup_least) 
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Transcendental.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -848,7 +848,7 @@
     hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
       by (simp add: pos_divide_le_eq mult_ac)
     thus "norm (S (Suc n)) \<le> r * norm (S n)"
-      by (simp add: S_Suc norm_scaleR inverse_eq_divide)
+      by (simp add: S_Suc inverse_eq_divide)
   qed
 qed
 
@@ -860,7 +860,7 @@
     by (rule summable_exp_generic)
 next
   fix n show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
-    by (simp add: norm_scaleR norm_power_ineq)
+    by (simp add: norm_power_ineq)
 qed
 
 lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)"
@@ -957,7 +957,7 @@
     by (simp only: scaleR_right.setsum)
   finally show
     "S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
-    by (simp add: scaleR_cancel_left del: setsum_cl_ivl_Suc)
+    by (simp del: setsum_cl_ivl_Suc)
 qed
 
 lemma exp_add: "exp (x + y) = exp x * exp y"
@@ -1237,7 +1237,7 @@
       { fix x :: real assume "x \<in> {- 1<..<1}" hence "norm (-x) < 1" by auto
         show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
           unfolding One_nat_def
-          by (auto simp del: power_mult_distrib simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
+          by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
       }
     qed
     hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" unfolding One_nat_def by auto
@@ -3090,7 +3090,7 @@
 
 lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<twosuperior> + y\<twosuperior>)\<bar> \<le> 1"
 apply (rule power2_le_imp_le [OF _ zero_le_one])
-apply (simp add: abs_divide power_divide divide_le_eq not_sum_power2_lt_zero)
+apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
 done
 
 lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Transitive_Closure.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -464,7 +464,7 @@
    apply (rule subsetI)
    apply (simp only: split_tupled_all)
    apply (erule trancl_induct, blast)
-   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)
+   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)
   apply (rule subsetI)
   apply (blast intro: trancl_mono rtrancl_mono
     [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
@@ -503,7 +503,7 @@
   apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major])
    apply (rule cases)
    apply (erule conversepD)
-  apply (blast intro: prems dest!: tranclp_converseD conversepD)
+  apply (blast intro: assms dest!: tranclp_converseD)
   done
 
 lemmas converse_trancl_induct = converse_tranclp_induct [to_set]
diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Wellfounded.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -489,7 +489,7 @@
   by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
 
 lemma trans_less_than [iff]: "trans less_than"
-  by (simp add: less_than_def trans_trancl)
+  by (simp add: less_than_def)
 
 lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
   by (simp add: less_than_def less_eq)