get rid of many duplicate simp rule warnings
authorhuffman
Thu Feb 18 14:21:44 2010 -0800 (2010-02-18)
changeset 352167641e8d831d2
parent 35215 a03462cbf86f
child 35217 01e968432467
get rid of many duplicate simp rule warnings
src/HOL/Datatype.thy
src/HOL/Deriv.thy
src/HOL/Divides.thy
src/HOL/Equiv_Relations.thy
src/HOL/Fields.thy
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Groebner_Basis.thy
src/HOL/Groups.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Int.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Nat_Numeral.thy
src/HOL/NthRoot.thy
src/HOL/PReal.thy
src/HOL/Parity.thy
src/HOL/Power.thy
src/HOL/Presburger.thy
src/HOL/Rational.thy
src/HOL/RealDef.thy
src/HOL/RealPow.thy
src/HOL/RealVector.thy
src/HOL/Rings.thy
src/HOL/SEQ.thy
src/HOL/SetInterval.thy
src/HOL/SupInf.thy
src/HOL/Transcendental.thy
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Datatype.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/Datatype.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -144,11 +144,10 @@
     1.4  (** Scons vs Atom **)
     1.5  
     1.6  lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)"
     1.7 -apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def)
     1.8 -apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
     1.9 +unfolding Atom_def Scons_def Push_Node_def One_nat_def
    1.10 +by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
    1.11           dest!: Abs_Node_inj 
    1.12           elim!: apfst_convE sym [THEN Push_neq_K0])  
    1.13 -done
    1.14  
    1.15  lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard]
    1.16  
    1.17 @@ -199,14 +198,12 @@
    1.18  (** Injectiveness of Scons **)
    1.19  
    1.20  lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'"
    1.21 -apply (simp add: Scons_def One_nat_def)
    1.22 -apply (blast dest!: Push_Node_inject)
    1.23 -done
    1.24 +unfolding Scons_def One_nat_def
    1.25 +by (blast dest!: Push_Node_inject)
    1.26  
    1.27  lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'"
    1.28 -apply (simp add: Scons_def One_nat_def)
    1.29 -apply (blast dest!: Push_Node_inject)
    1.30 -done
    1.31 +unfolding Scons_def One_nat_def
    1.32 +by (blast dest!: Push_Node_inject)
    1.33  
    1.34  lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
    1.35  apply (erule equalityE)
    1.36 @@ -230,14 +227,14 @@
    1.37  (** Scons vs Leaf **)
    1.38  
    1.39  lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
    1.40 -by (simp add: Leaf_def o_def Scons_not_Atom)
    1.41 +unfolding Leaf_def o_def by (rule Scons_not_Atom)
    1.42  
    1.43  lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym, standard]
    1.44  
    1.45  (** Scons vs Numb **)
    1.46  
    1.47  lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
    1.48 -by (simp add: Numb_def o_def Scons_not_Atom)
    1.49 +unfolding Numb_def o_def by (rule Scons_not_Atom)
    1.50  
    1.51  lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard]
    1.52  
    1.53 @@ -281,14 +278,15 @@
    1.54  by (auto simp add: Atom_def ntrunc_def ndepth_K0)
    1.55  
    1.56  lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)"
    1.57 -by (simp add: Leaf_def o_def ntrunc_Atom)
    1.58 +unfolding Leaf_def o_def by (rule ntrunc_Atom)
    1.59  
    1.60  lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)"
    1.61 -by (simp add: Numb_def o_def ntrunc_Atom)
    1.62 +unfolding Numb_def o_def by (rule ntrunc_Atom)
    1.63  
    1.64  lemma ntrunc_Scons [simp]: 
    1.65      "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"
    1.66 -by (auto simp add: Scons_def ntrunc_def One_nat_def ndepth_Push_Node) 
    1.67 +unfolding Scons_def ntrunc_def One_nat_def
    1.68 +by (auto simp add: ndepth_Push_Node)
    1.69  
    1.70  
    1.71  
    1.72 @@ -351,7 +349,7 @@
    1.73  (** Injection **)
    1.74  
    1.75  lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
    1.76 -by (auto simp add: In0_def In1_def One_nat_def)
    1.77 +unfolding In0_def In1_def One_nat_def by auto
    1.78  
    1.79  lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard]
    1.80  
    1.81 @@ -417,10 +415,10 @@
    1.82  by (simp add: Scons_def, blast)
    1.83  
    1.84  lemma In0_mono: "M<=N ==> In0(M) <= In0(N)"
    1.85 -by (simp add: In0_def subset_refl Scons_mono)
    1.86 +by (simp add: In0_def Scons_mono)
    1.87  
    1.88  lemma In1_mono: "M<=N ==> In1(M) <= In1(N)"
    1.89 -by (simp add: In1_def subset_refl Scons_mono)
    1.90 +by (simp add: In1_def Scons_mono)
    1.91  
    1.92  
    1.93  (*** Split and Case ***)
     2.1 --- a/src/HOL/Deriv.thy	Thu Feb 18 13:29:59 2010 -0800
     2.2 +++ b/src/HOL/Deriv.thy	Thu Feb 18 14:21:44 2010 -0800
     2.3 @@ -260,7 +260,7 @@
     2.4            -- x --> d (f x) * D"
     2.5      by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]])
     2.6    thus "(\<lambda>z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D"
     2.7 -    by (simp add: d dfx real_scaleR_def)
     2.8 +    by (simp add: d dfx)
     2.9  qed
    2.10  
    2.11  text {*
    2.12 @@ -279,7 +279,7 @@
    2.13  
    2.14  text {* Standard version *}
    2.15  lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
    2.16 -by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute)
    2.17 +by (drule (1) DERIV_chain', simp add: o_def mult_commute)
    2.18  
    2.19  lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
    2.20  by (auto dest: DERIV_chain simp add: o_def)
    2.21 @@ -290,7 +290,7 @@
    2.22  
    2.23  lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
    2.24  apply (cut_tac DERIV_power [OF DERIV_ident])
    2.25 -apply (simp add: real_scaleR_def real_of_nat_def)
    2.26 +apply (simp add: real_of_nat_def)
    2.27  done
    2.28  
    2.29  text {* Power of @{text "-1"} *}
    2.30 @@ -1532,12 +1532,12 @@
    2.31    moreover
    2.32    have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
    2.33    proof -
    2.34 -    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by (simp add: differentiable_const)
    2.35 -    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)
    2.36 +    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by simp
    2.37 +    with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by simp
    2.38      moreover
    2.39 -    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by (simp add: differentiable_const)
    2.40 -    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)
    2.41 -    ultimately show ?thesis by (simp add: differentiable_diff)
    2.42 +    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by simp
    2.43 +    with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by simp
    2.44 +    ultimately show ?thesis by simp
    2.45    qed
    2.46    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)
    2.47    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" ..
     3.1 --- a/src/HOL/Divides.thy	Thu Feb 18 13:29:59 2010 -0800
     3.2 +++ b/src/HOL/Divides.thy	Thu Feb 18 14:21:44 2010 -0800
     3.3 @@ -1090,7 +1090,7 @@
     3.4  lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
     3.5  apply (subgoal_tac "m mod 2 < 2")
     3.6  apply (erule less_2_cases [THEN disjE])
     3.7 -apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
     3.8 +apply (simp_all (no_asm_simp) add: Let_def mod_Suc)
     3.9  done
    3.10  
    3.11  lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
    3.12 @@ -1929,7 +1929,7 @@
    3.13  apply (rule order_le_less_trans)
    3.14   apply (erule_tac [2] mult_strict_right_mono)
    3.15   apply (rule mult_left_mono_neg)
    3.16 -  using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps pos_mod_bound)
    3.17 +  using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
    3.18   apply (simp)
    3.19  apply (simp)
    3.20  done
    3.21 @@ -1954,7 +1954,7 @@
    3.22   apply (erule mult_strict_right_mono)
    3.23   apply (rule_tac [2] mult_left_mono)
    3.24    apply simp
    3.25 - using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps pos_mod_bound)
    3.26 + using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
    3.27  apply simp
    3.28  done
    3.29  
     4.1 --- a/src/HOL/Equiv_Relations.thy	Thu Feb 18 13:29:59 2010 -0800
     4.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Feb 18 14:21:44 2010 -0800
     4.3 @@ -328,7 +328,7 @@
     4.4     apply assumption
     4.5    apply simp
     4.6   apply(fastsimp simp add:inj_on_def)
     4.7 -apply (simp add:setsum_constant)
     4.8 +apply simp
     4.9  done
    4.10  
    4.11  end
     5.1 --- a/src/HOL/Fields.thy	Thu Feb 18 13:29:59 2010 -0800
     5.2 +++ b/src/HOL/Fields.thy	Thu Feb 18 14:21:44 2010 -0800
     5.3 @@ -230,7 +230,7 @@
     5.4  lemma inverse_minus_eq [simp]:
     5.5     "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
     5.6  proof cases
     5.7 -  assume "a=0" thus ?thesis by (simp add: inverse_zero)
     5.8 +  assume "a=0" thus ?thesis by simp
     5.9  next
    5.10    assume "a\<noteq>0" 
    5.11    thus ?thesis by (simp add: nonzero_inverse_minus_eq)
    5.12 @@ -283,13 +283,13 @@
    5.13  lemma mult_divide_mult_cancel_left:
    5.14    "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
    5.15  apply (cases "b = 0")
    5.16 -apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
    5.17 +apply simp_all
    5.18  done
    5.19  
    5.20  lemma mult_divide_mult_cancel_right:
    5.21    "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
    5.22  apply (cases "b = 0")
    5.23 -apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
    5.24 +apply simp_all
    5.25  done
    5.26  
    5.27  lemma divide_divide_eq_right [simp,noatp]:
    5.28 @@ -339,7 +339,7 @@
    5.29  assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::linordered_field)"
    5.30  proof -
    5.31    have "0 < a * inverse a" 
    5.32 -    by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
    5.33 +    by (simp add: a_gt_0 [THEN order_less_imp_not_eq2])
    5.34    thus "0 < inverse a" 
    5.35      by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
    5.36  qed
    5.37 @@ -524,8 +524,7 @@
    5.38  
    5.39  lemma one_le_inverse_iff:
    5.40    "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{linordered_field,division_by_zero}))"
    5.41 -by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
    5.42 -                    eq_commute [of 1]) 
    5.43 +by (force simp add: order_le_less one_less_inverse_iff)
    5.44  
    5.45  lemma inverse_less_1_iff:
    5.46    "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{linordered_field,division_by_zero}))"
     6.1 --- a/src/HOL/Finite_Set.thy	Thu Feb 18 13:29:59 2010 -0800
     6.2 +++ b/src/HOL/Finite_Set.thy	Thu Feb 18 14:21:44 2010 -0800
     6.3 @@ -355,7 +355,7 @@
     6.4    apply (induct set: finite)
     6.5     apply simp_all
     6.6    apply (subst vimage_insert)
     6.7 -  apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
     6.8 +  apply (simp add: finite_subset [OF inj_vimage_singleton])
     6.9    done
    6.10  
    6.11  lemma finite_vimageD:
    6.12 @@ -485,7 +485,7 @@
    6.13  next
    6.14    assume "finite A"
    6.15    thus "finite (Pow A)"
    6.16 -    by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
    6.17 +    by induct (simp_all add: Pow_insert)
    6.18  qed
    6.19  
    6.20  lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
    6.21 @@ -634,7 +634,7 @@
    6.22    from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
    6.23    let ?hm = "Fun.swap k m h"
    6.24    have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
    6.25 -    by (simp add: inj_on_swap_iff inj_on)
    6.26 +    by (simp add: inj_on)
    6.27    show ?thesis
    6.28    proof (intro exI conjI)
    6.29      show "inj_on ?hm {i. i < m}" using inj_hm
    6.30 @@ -764,7 +764,7 @@
    6.31  
    6.32  lemma fold_insert2:
    6.33    "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
    6.34 -by (simp add: fold_insert fold_fun_comm)
    6.35 +by (simp add: fold_fun_comm)
    6.36  
    6.37  lemma fold_rec:
    6.38  assumes "finite A" and "x \<in> A"
    6.39 @@ -824,8 +824,8 @@
    6.40  
    6.41  lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
    6.42  apply unfold_locales
    6.43 - apply (simp add: mult_ac)
    6.44 -apply (simp add: mult_idem mult_assoc[symmetric])
    6.45 + apply (rule mult_left_commute)
    6.46 +apply (rule mult_left_idem)
    6.47  done
    6.48  
    6.49  end
    6.50 @@ -1366,7 +1366,7 @@
    6.51  
    6.52  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"
    6.53    apply (induct set: finite)
    6.54 -  apply simp by (auto simp add: fold_image_insert)
    6.55 +  apply simp by auto
    6.56  
    6.57  lemma (in comm_monoid_mult) fold_image_Un_one:
    6.58    assumes fS: "finite S" and fT: "finite T"
    6.59 @@ -1412,8 +1412,8 @@
    6.60  next
    6.61    case (2 T F)
    6.62    then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
    6.63 -    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert)
    6.64 -  from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union)
    6.65 +    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
    6.66 +  from fTF have fUF: "finite (\<Union>F)" by auto
    6.67    from "2.prems" TF fTF
    6.68    show ?case 
    6.69      by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
    6.70 @@ -2056,7 +2056,7 @@
    6.71    shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
    6.72  proof (cases "finite A")
    6.73    case True thus ?thesis
    6.74 -    by induct (auto simp add: field_simps setprod_insert abs_mult)
    6.75 +    by induct (auto simp add: field_simps abs_mult)
    6.76  qed auto
    6.77  
    6.78  
    6.79 @@ -2215,7 +2215,7 @@
    6.80       (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
    6.81       k * card(C) = card (\<Union> C)"
    6.82  apply (erule finite_induct, simp)
    6.83 -apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
    6.84 +apply (simp add: card_Un_disjoint insert_partition 
    6.85         finite_subset [of _ "\<Union> (insert x F)"])
    6.86  done
    6.87  
    6.88 @@ -2285,7 +2285,7 @@
    6.89  
    6.90  lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
    6.91  apply (erule finite_induct)
    6.92 -apply (auto simp add: power_Suc)
    6.93 +apply auto
    6.94  done
    6.95  
    6.96  lemma setprod_gen_delta:
    6.97 @@ -2370,7 +2370,7 @@
    6.98  lemma card_image_le: "finite A ==> card (f ` A) <= card A"
    6.99  apply (induct set: finite)
   6.100   apply simp
   6.101 -apply (simp add: le_SucI finite_imageI card_insert_if)
   6.102 +apply (simp add: le_SucI card_insert_if)
   6.103  done
   6.104  
   6.105  lemma card_image: "inj_on f A ==> card (f ` A) = card A"
   6.106 @@ -2473,7 +2473,7 @@
   6.107  apply(rotate_tac -1)
   6.108  apply (induct set: finite, simp_all, clarify)
   6.109  apply (subst card_Un_disjoint)
   6.110 -   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
   6.111 +   apply (auto simp add: disjoint_eq_subset_Compl)
   6.112  done
   6.113  
   6.114  
   6.115 @@ -2514,7 +2514,7 @@
   6.116    ultimately have "finite (UNIV::nat set)"
   6.117      by (rule finite_imageD)
   6.118    then show "False"
   6.119 -    by (simp add: infinite_UNIV_nat)
   6.120 +    by simp
   6.121  qed
   6.122  
   6.123  subsection{* A fold functional for non-empty sets *}
   6.124 @@ -2542,7 +2542,7 @@
   6.125  
   6.126  
   6.127  lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
   6.128 -by (blast intro: fold_graph.intros elim: fold_graph.cases)
   6.129 +by (blast elim: fold_graph.cases)
   6.130  
   6.131  lemma fold1_singleton [simp]: "fold1 f {a} = a"
   6.132  by (unfold fold1_def) blast
   6.133 @@ -2612,9 +2612,9 @@
   6.134  apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times])
   6.135  apply (rule sym, clarify)
   6.136  apply (case_tac "Aa=A")
   6.137 - apply (best intro: the_equality fold_graph_determ)
   6.138 + apply (best intro: fold_graph_determ)
   6.139  apply (subgoal_tac "fold_graph times a A x")
   6.140 - apply (best intro: the_equality fold_graph_determ)
   6.141 + apply (best intro: fold_graph_determ)
   6.142  apply (subgoal_tac "insert aa (Aa - {a}) = A")
   6.143   prefer 2 apply (blast elim: equalityE)
   6.144  apply (auto dest: fold_graph_permute_diff [where a=a])
   6.145 @@ -2658,16 +2658,16 @@
   6.146      thus ?thesis
   6.147      proof cases
   6.148        assume "A' = {}"
   6.149 -      with prems show ?thesis by (simp add: mult_idem)
   6.150 +      with prems show ?thesis by simp
   6.151      next
   6.152        assume "A' \<noteq> {}"
   6.153        with prems show ?thesis
   6.154 -        by (simp add: fold1_insert mult_assoc [symmetric] mult_idem)
   6.155 +        by (simp add: fold1_insert mult_assoc [symmetric])
   6.156      qed
   6.157    next
   6.158      assume "a \<noteq> x"
   6.159      with prems show ?thesis
   6.160 -      by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
   6.161 +      by (simp add: insert_commute fold1_eq_fold)
   6.162    qed
   6.163  qed
   6.164  
   6.165 @@ -2710,7 +2710,7 @@
   6.166  text{* Now the recursion rules for definitions: *}
   6.167  
   6.168  lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
   6.169 -by(simp add:fold1_singleton)
   6.170 +by simp
   6.171  
   6.172  lemma (in ab_semigroup_mult) fold1_insert_def:
   6.173    "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
     7.1 --- a/src/HOL/GCD.thy	Thu Feb 18 13:29:59 2010 -0800
     7.2 +++ b/src/HOL/GCD.thy	Thu Feb 18 14:21:44 2010 -0800
     7.3 @@ -156,7 +156,7 @@
     7.4        and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
     7.5        and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
     7.6    shows "P (gcd x y)"
     7.7 -by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith)
     7.8 +by (insert assms, auto, arith)
     7.9  
    7.10  lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
    7.11    by (simp add: gcd_int_def)
    7.12 @@ -457,7 +457,7 @@
    7.13    apply (case_tac "y > 0")
    7.14    apply (subst gcd_non_0_int, auto)
    7.15    apply (insert gcd_non_0_int [of "-y" "-x"])
    7.16 -  apply (auto simp add: gcd_neg1_int gcd_neg2_int)
    7.17 +  apply auto
    7.18  done
    7.19  
    7.20  lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
    7.21 @@ -557,7 +557,7 @@
    7.22    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
    7.23      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
    7.24        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
    7.25 -  have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat)
    7.26 +  have "?g \<noteq> 0" using nz by simp
    7.27    then have gp: "?g > 0" by arith
    7.28    from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
    7.29    with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
    7.30 @@ -824,7 +824,7 @@
    7.31    {assume "?g = 0" with ab n have ?thesis by auto }
    7.32    moreover
    7.33    {assume z: "?g \<noteq> 0"
    7.34 -    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
    7.35 +    hence zn: "?g ^ n \<noteq> 0" using n by simp
    7.36      from gcd_coprime_exists_nat[OF z]
    7.37      obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
    7.38        by blast
    7.39 @@ -852,7 +852,7 @@
    7.40    {assume "?g = 0" with ab n have ?thesis by auto }
    7.41    moreover
    7.42    {assume z: "?g \<noteq> 0"
    7.43 -    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
    7.44 +    hence zn: "?g ^ n \<noteq> 0" using n by simp
    7.45      from gcd_coprime_exists_int[OF z]
    7.46      obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
    7.47        by blast
    7.48 @@ -1109,7 +1109,7 @@
    7.49      (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
    7.50    using ex
    7.51    apply clarsimp
    7.52 -  apply (rule_tac x="d" in exI, simp add: dvd_add)
    7.53 +  apply (rule_tac x="d" in exI, simp)
    7.54    apply (case_tac "a * x = b * y + d" , simp_all)
    7.55    apply (rule_tac x="x + y" in exI)
    7.56    apply (rule_tac x="y" in exI)
    7.57 @@ -1124,10 +1124,10 @@
    7.58    apply(induct a b rule: ind_euclid)
    7.59    apply blast
    7.60    apply clarify
    7.61 -  apply (rule_tac x="a" in exI, simp add: dvd_add)
    7.62 +  apply (rule_tac x="a" in exI, simp)
    7.63    apply clarsimp
    7.64    apply (rule_tac x="d" in exI)
    7.65 -  apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
    7.66 +  apply (case_tac "a * x = b * y + d", simp_all)
    7.67    apply (rule_tac x="x+y" in exI)
    7.68    apply (rule_tac x="y" in exI)
    7.69    apply algebra
    7.70 @@ -1693,8 +1693,7 @@
    7.71    "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
    7.72     \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
    7.73  apply(auto simp add:inj_on_def)
    7.74 -apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
    7.75 -             dvd.neq_le_trans dvd_triv_left)
    7.76 +apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
    7.77  apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
    7.78               dvd.neq_le_trans dvd_triv_right mult_commute)
    7.79  done
     8.1 --- a/src/HOL/Groebner_Basis.thy	Thu Feb 18 13:29:59 2010 -0800
     8.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Feb 18 14:21:44 2010 -0800
     8.3 @@ -143,16 +143,16 @@
     8.4  next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr)
     8.5  next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp
     8.6  next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp
     8.7 -next show "mul x x = pwr x 2" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
     8.8 +next show "mul x x = pwr x 2" by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
     8.9  next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
    8.10  next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
    8.11  next show "pwr x 0 = r1" using pwr_0 .
    8.12 -next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
    8.13 +next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
    8.14  next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
    8.15  next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
    8.16 -next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)
    8.17 +next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number' mul_pwr)
    8.18  next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))"
    8.19 -    by (simp add: nat_number pwr_Suc mul_pwr)
    8.20 +    by (simp add: nat_number' pwr_Suc mul_pwr)
    8.21  qed
    8.22  
    8.23  
    8.24 @@ -165,7 +165,7 @@
    8.25  
    8.26  interpretation class_semiring: gb_semiring
    8.27      "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1"
    8.28 -  proof qed (auto simp add: algebra_simps power_Suc)
    8.29 +  proof qed (auto simp add: algebra_simps)
    8.30  
    8.31  lemmas nat_arith =
    8.32    add_nat_number_of
    8.33 @@ -175,7 +175,7 @@
    8.34    less_nat_number_of
    8.35  
    8.36  lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
    8.37 -  by (simp add: numeral_1_eq_1)
    8.38 +  by simp
    8.39  
    8.40  lemmas comp_arith =
    8.41    Let_def arith_simps nat_arith rel_simps neg_simps if_False
    8.42 @@ -350,7 +350,7 @@
    8.43  
    8.44  interpretation class_ringb: ringb
    8.45    "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
    8.46 -proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
    8.47 +proof(unfold_locales, simp add: algebra_simps, auto)
    8.48    fix w x y z ::"'a::{idom,number_ring}"
    8.49    assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    8.50    hence ynz': "y - z \<noteq> 0" by simp
    8.51 @@ -366,7 +366,7 @@
    8.52  
    8.53  interpretation natgb: semiringb
    8.54    "op +" "op *" "op ^" "0::nat" "1"
    8.55 -proof (unfold_locales, simp add: algebra_simps power_Suc)
    8.56 +proof (unfold_locales, simp add: algebra_simps)
    8.57    fix w x y z ::"nat"
    8.58    { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    8.59      hence "y < z \<or> y > z" by arith
    8.60 @@ -375,13 +375,13 @@
    8.61        then obtain k where kp: "k>0" and yz:"z = y + k" by blast
    8.62        from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps)
    8.63        hence "x*k = w*k" by simp
    8.64 -      hence "w = x" using kp by (simp add: mult_cancel2) }
    8.65 +      hence "w = x" using kp by simp }
    8.66      moreover {
    8.67        assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
    8.68        then obtain k where kp: "k>0" and yz:"y = z + k" by blast
    8.69        from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps)
    8.70        hence "w*k = x*k" by simp
    8.71 -      hence "w = x" using kp by (simp add: mult_cancel2)}
    8.72 +      hence "w = x" using kp by simp }
    8.73      ultimately have "w=x" by blast }
    8.74    thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
    8.75  qed
     9.1 --- a/src/HOL/Groups.thy	Thu Feb 18 13:29:59 2010 -0800
     9.2 +++ b/src/HOL/Groups.thy	Thu Feb 18 14:21:44 2010 -0800
     9.3 @@ -347,6 +347,8 @@
     9.4  lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
     9.5  by (simp add: algebra_simps)
     9.6  
     9.7 +(* FIXME: duplicates right_minus_eq from class group_add *)
     9.8 +(* but only this one is declared as a simp rule. *)
     9.9  lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \<longleftrightarrow> a = b"
    9.10  by (simp add: algebra_simps)
    9.11  
    9.12 @@ -794,7 +796,7 @@
    9.13  proof
    9.14    assume assm: "a + a = 0"
    9.15    then have a: "- a = a" by (rule minus_unique)
    9.16 -  then show "a = 0" by (simp add: neg_equal_zero)
    9.17 +  then show "a = 0" by (simp only: neg_equal_zero)
    9.18  qed simp
    9.19  
    9.20  lemma double_zero_sym [simp]:
    9.21 @@ -807,7 +809,7 @@
    9.22    assume "0 < a + a"
    9.23    then have "0 - a < a" by (simp only: diff_less_eq)
    9.24    then have "- a < a" by simp
    9.25 -  then show "0 < a" by (simp add: neg_less_nonneg)
    9.26 +  then show "0 < a" by (simp only: neg_less_nonneg)
    9.27  next
    9.28    assume "0 < a"
    9.29    with this have "0 + 0 < a + a"
    10.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Feb 18 13:29:59 2010 -0800
    10.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Feb 18 14:21:44 2010 -0800
    10.3 @@ -61,7 +61,7 @@
    10.4  by (blast intro: someI2)
    10.5  
    10.6  lemma some1_equality: "[| EX!x. P x; P a |] ==> (SOME x. P x) = a"
    10.7 -by (blast intro: some_equality)
    10.8 +by blast
    10.9  
   10.10  lemma some_eq_ex: "P (SOME x. P x) =  (\<exists>x. P x)"
   10.11  by (blast intro: someI)
   10.12 @@ -108,7 +108,7 @@
   10.13  done
   10.14  
   10.15  lemma inv_f_f: "inj f ==> inv f (f x) = x"
   10.16 -by (simp add: inv_into_f_f)
   10.17 +by simp
   10.18  
   10.19  lemma f_inv_into_f: "y : f`A  ==> f (inv_into A f y) = y"
   10.20  apply (simp add: inv_into_def)
    11.1 --- a/src/HOL/Int.thy	Thu Feb 18 13:29:59 2010 -0800
    11.2 +++ b/src/HOL/Int.thy	Thu Feb 18 14:21:44 2010 -0800
    11.3 @@ -391,6 +391,7 @@
    11.4  lemma nat_int [simp]: "nat (of_nat n) = n"
    11.5  by (simp add: nat int_def)
    11.6  
    11.7 +(* FIXME: duplicates nat_0 *)
    11.8  lemma nat_zero [simp]: "nat 0 = 0"
    11.9  by (simp add: Zero_int_def nat)
   11.10  
   11.11 @@ -626,10 +627,10 @@
   11.12  
   11.13  lemmas
   11.14    max_number_of [simp] = max_def
   11.15 -    [of "number_of u" "number_of v", standard, simp]
   11.16 +    [of "number_of u" "number_of v", standard]
   11.17  and
   11.18    min_number_of [simp] = min_def 
   11.19 -    [of "number_of u" "number_of v", standard, simp]
   11.20 +    [of "number_of u" "number_of v", standard]
   11.21    -- {* unfolding @{text minx} and @{text max} on numerals *}
   11.22  
   11.23  lemmas numeral_simps = 
   11.24 @@ -1060,7 +1061,7 @@
   11.25  lemma not_iszero_1: "~ iszero 1"
   11.26  by (simp add: iszero_def eq_commute)
   11.27  
   11.28 -lemma eq_number_of_eq:
   11.29 +lemma eq_number_of_eq [simp]:
   11.30    "((number_of x::'a::number_ring) = number_of y) =
   11.31     iszero (number_of (x + uminus y) :: 'a)"
   11.32  unfolding iszero_def number_of_add number_of_minus
   11.33 @@ -1130,7 +1131,7 @@
   11.34      by (auto simp add: iszero_def number_of_eq numeral_simps)
   11.35  qed
   11.36  
   11.37 -lemmas iszero_simps =
   11.38 +lemmas iszero_simps [simp] =
   11.39    iszero_0 not_iszero_1
   11.40    iszero_number_of_Pls nonzero_number_of_Min
   11.41    iszero_number_of_Bit0 iszero_number_of_Bit1
   11.42 @@ -1218,7 +1219,7 @@
   11.43    "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y"
   11.44    unfolding number_of_eq by (rule of_int_eq_iff)
   11.45  
   11.46 -lemmas rel_simps [simp] = 
   11.47 +lemmas rel_simps =
   11.48    less_number_of less_bin_simps
   11.49    le_number_of le_bin_simps
   11.50    eq_number_of_eq eq_bin_simps
   11.51 @@ -1240,7 +1241,7 @@
   11.52  lemma add_number_of_diff1:
   11.53    "number_of v + (number_of w - c) = 
   11.54    number_of(v + w) - (c::'a::number_ring)"
   11.55 -  by (simp add: diff_minus add_number_of_left)
   11.56 +  by (simp add: diff_minus)
   11.57  
   11.58  lemma add_number_of_diff2 [simp]:
   11.59    "number_of v + (c - number_of w) =
   11.60 @@ -1437,7 +1438,7 @@
   11.61  
   11.62  text{*Allow 1 on either or both sides*}
   11.63  lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
   11.64 -by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
   11.65 +by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric])
   11.66  
   11.67  lemmas add_special =
   11.68      one_add_one_is_two
   11.69 @@ -1558,6 +1559,7 @@
   11.70  
   11.71  lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
   11.72  
   11.73 +(* FIXME: duplicates nat_zero *)
   11.74  lemma nat_0: "nat 0 = 0"
   11.75  by (simp add: nat_eq_iff)
   11.76  
   11.77 @@ -1980,7 +1982,7 @@
   11.78  
   11.79  lemma minus1_divide [simp]:
   11.80       "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
   11.81 -by (simp add: divide_inverse inverse_minus_eq)
   11.82 +by (simp add: divide_inverse)
   11.83  
   11.84  lemma half_gt_zero_iff:
   11.85       "(0 < r/2) = (0 < (r::'a::{linordered_field,division_by_zero,number_ring}))"
   11.86 @@ -2098,7 +2100,7 @@
   11.87    assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
   11.88  proof
   11.89    assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
   11.90 -    by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
   11.91 +    by (cases "n >0", auto simp add: minus_equation_iff)
   11.92  next
   11.93    assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
   11.94    from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
    12.1 --- a/src/HOL/List.thy	Thu Feb 18 13:29:59 2010 -0800
    12.2 +++ b/src/HOL/List.thy	Thu Feb 18 14:21:44 2010 -0800
    12.3 @@ -257,9 +257,9 @@
    12.4  @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
    12.5  @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
    12.6  @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
    12.7 -@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\
    12.8 -@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\
    12.9 -@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\
   12.10 +@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\
   12.11 +@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\
   12.12 +@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\
   12.13  @{lemma "listsum [1,2,3::nat] = 6" by simp}
   12.14  \end{tabular}}
   12.15  \caption{Characteristic examples}
    13.1 --- a/src/HOL/Nat.thy	Thu Feb 18 13:29:59 2010 -0800
    13.2 +++ b/src/HOL/Nat.thy	Thu Feb 18 14:21:44 2010 -0800
    13.3 @@ -1356,7 +1356,7 @@
    13.4  end
    13.5  
    13.6  lemma of_nat_id [simp]: "of_nat n = n"
    13.7 -  by (induct n) (auto simp add: One_nat_def)
    13.8 +  by (induct n) simp_all
    13.9  
   13.10  lemma of_nat_eq_id [simp]: "of_nat = id"
   13.11    by (auto simp add: expand_fun_eq)
   13.12 @@ -1619,7 +1619,7 @@
   13.13  
   13.14  lemma dvd_antisym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   13.15    unfolding dvd_def
   13.16 -  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
   13.17 +  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc)
   13.18  
   13.19  text {* @{term "op dvd"} is a partial order *}
   13.20  
    14.1 --- a/src/HOL/Nat_Numeral.thy	Thu Feb 18 13:29:59 2010 -0800
    14.2 +++ b/src/HOL/Nat_Numeral.thy	Thu Feb 18 14:21:44 2010 -0800
    14.3 @@ -211,7 +211,7 @@
    14.4    "0 \<le> a ^ (2*n)"
    14.5  proof (induct n)
    14.6    case 0
    14.7 -    show ?case by (simp add: zero_le_one)
    14.8 +    show ?case by simp
    14.9  next
   14.10    case (Suc n)
   14.11      have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   14.12 @@ -262,7 +262,7 @@
   14.13  by (simp add: neg_def)
   14.14  
   14.15  lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
   14.16 -by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
   14.17 +by (simp add: neg_def del: of_nat_Suc)
   14.18  
   14.19  lemmas neg_eq_less_0 = neg_def
   14.20  
   14.21 @@ -275,7 +275,7 @@
   14.22  by (simp add: One_int_def neg_def)
   14.23  
   14.24  lemma not_neg_1: "~ neg 1"
   14.25 -by (simp add: neg_def linorder_not_less zero_le_one)
   14.26 +by (simp add: neg_def linorder_not_less)
   14.27  
   14.28  lemma neg_nat: "neg z ==> nat z = 0"
   14.29  by (simp add: neg_def order_less_imp_le) 
   14.30 @@ -310,7 +310,7 @@
   14.31  
   14.32  subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
   14.33  
   14.34 -declare nat_0 [simp] nat_1 [simp]
   14.35 +declare nat_1 [simp]
   14.36  
   14.37  lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
   14.38  by (simp add: nat_number_of_def)
   14.39 @@ -319,10 +319,10 @@
   14.40  by (simp add: nat_number_of_def)
   14.41  
   14.42  lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
   14.43 -by (simp add: nat_1 nat_number_of_def)
   14.44 +by (simp add: nat_number_of_def)
   14.45  
   14.46  lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
   14.47 -by (simp add: nat_numeral_1_eq_1)
   14.48 +by (simp only: nat_numeral_1_eq_1 One_nat_def)
   14.49  
   14.50  
   14.51  subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
   14.52 @@ -469,7 +469,7 @@
   14.53  subsubsection{*Nat *}
   14.54  
   14.55  lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   14.56 -by (simp add: numerals)
   14.57 +by simp
   14.58  
   14.59  (*Expresses a natural number constant as the Suc of another one.
   14.60    NOT suitable for rewriting because n recurs in the condition.*)
   14.61 @@ -478,10 +478,10 @@
   14.62  subsubsection{*Arith *}
   14.63  
   14.64  lemma Suc_eq_plus1: "Suc n = n + 1"
   14.65 -by (simp add: numerals)
   14.66 +  unfolding One_nat_def by simp
   14.67  
   14.68  lemma Suc_eq_plus1_left: "Suc n = 1 + n"
   14.69 -by (simp add: numerals)
   14.70 +  unfolding One_nat_def by simp
   14.71  
   14.72  (* These two can be useful when m = number_of... *)
   14.73  
   14.74 @@ -563,13 +563,13 @@
   14.75       "(number_of v <= Suc n) =  
   14.76          (let pv = number_of (Int.pred v) in  
   14.77           if neg pv then True else nat pv <= n)"
   14.78 -by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
   14.79 +by (simp add: Let_def linorder_not_less [symmetric])
   14.80  
   14.81  lemma le_Suc_number_of [simp]:
   14.82       "(Suc n <= number_of v) =  
   14.83          (let pv = number_of (Int.pred v) in  
   14.84           if neg pv then False else n <= nat pv)"
   14.85 -by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
   14.86 +by (simp add: Let_def linorder_not_less [symmetric])
   14.87  
   14.88  
   14.89  lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
   14.90 @@ -660,7 +660,7 @@
   14.91      power_number_of_odd [of "number_of v", standard]
   14.92  
   14.93  lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   14.94 -  by (simp add: number_of_Pls nat_number_of_def)
   14.95 +  by (simp add: nat_number_of_def)
   14.96  
   14.97  lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
   14.98    apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   14.99 @@ -684,6 +684,9 @@
  14.100    nat_number_of_Pls nat_number_of_Min
  14.101    nat_number_of_Bit0 nat_number_of_Bit1
  14.102  
  14.103 +lemmas nat_number' =
  14.104 +  nat_number_of_Bit0 nat_number_of_Bit1
  14.105 +
  14.106  lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
  14.107    by (fact Let_def)
  14.108  
  14.109 @@ -736,7 +739,7 @@
  14.110  text{*Where K above is a literal*}
  14.111  
  14.112  lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
  14.113 -by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
  14.114 +by (simp split: nat_diff_split)
  14.115  
  14.116  text {*Now just instantiating @{text n} to @{text "number_of v"} does
  14.117    the right simplification, but with some redundant inequality
  14.118 @@ -761,7 +764,7 @@
  14.119  done
  14.120  
  14.121  lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
  14.122 -by (simp add: numerals split add: nat_diff_split)
  14.123 +by (simp split: nat_diff_split)
  14.124  
  14.125  
  14.126  subsubsection{*For @{term nat_case} and @{term nat_rec}*}
    15.1 --- a/src/HOL/NthRoot.thy	Thu Feb 18 13:29:59 2010 -0800
    15.2 +++ b/src/HOL/NthRoot.thy	Thu Feb 18 14:21:44 2010 -0800
    15.3 @@ -566,7 +566,7 @@
    15.4  done
    15.5  
    15.6  lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
    15.7 -by (simp add: divide_less_eq mult_compare_simps)
    15.8 +by (simp add: divide_less_eq)
    15.9  
   15.10  lemma four_x_squared: 
   15.11    fixes x::real
    16.1 --- a/src/HOL/PReal.thy	Thu Feb 18 13:29:59 2010 -0800
    16.2 +++ b/src/HOL/PReal.thy	Thu Feb 18 14:21:44 2010 -0800
    16.3 @@ -750,7 +750,7 @@
    16.4    have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)" 
    16.5    proof -
    16.6      have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
    16.7 -      by (simp add: mult_rat le_rat order_less_imp_not_eq2 mult_ac) 
    16.8 +      by (simp add: order_less_imp_not_eq2 mult_ac) 
    16.9      moreover
   16.10      have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
   16.11        by (rule mult_mono, 
   16.12 @@ -822,7 +822,7 @@
   16.13        also with ypos have "... = (r/y) * (y + ?d)"
   16.14          by (simp only: algebra_simps divide_inverse, simp)
   16.15        also have "... = r*x" using ypos
   16.16 -        by (simp add: times_divide_eq_left) 
   16.17 +        by simp
   16.18        finally show "r + ?d < r*x" .
   16.19      qed
   16.20      with r notin rdpos
    17.1 --- a/src/HOL/Parity.thy	Thu Feb 18 13:29:59 2010 -0800
    17.2 +++ b/src/HOL/Parity.thy	Thu Feb 18 14:21:44 2010 -0800
    17.3 @@ -184,7 +184,7 @@
    17.4    apply (rule conjI)
    17.5    apply simp
    17.6    apply (insert even_zero_nat, blast)
    17.7 -  apply (simp add: power_Suc)
    17.8 +  apply simp
    17.9    done
   17.10  
   17.11  lemma minus_one_even_power [simp]:
   17.12 @@ -199,7 +199,7 @@
   17.13       "(even x --> (-1::'a::{number_ring})^x = 1) &
   17.14        (odd x --> (-1::'a)^x = -1)"
   17.15    apply (induct x)
   17.16 -  apply (simp, simp add: power_Suc)
   17.17 +  apply (simp, simp)
   17.18    done
   17.19  
   17.20  lemma neg_one_even_power [simp]:
   17.21 @@ -214,7 +214,7 @@
   17.22       "(-x::'a::{comm_ring_1}) ^ n =
   17.23        (if even n then (x ^ n) else -(x ^ n))"
   17.24    apply (induct n)
   17.25 -  apply (simp_all split: split_if_asm add: power_Suc)
   17.26 +  apply simp_all
   17.27    done
   17.28  
   17.29  lemma zero_le_even_power: "even n ==>
   17.30 @@ -228,7 +228,7 @@
   17.31  
   17.32  lemma zero_le_odd_power: "odd n ==>
   17.33      (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)"
   17.34 -apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
   17.35 +apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff)
   17.36  apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
   17.37  done
   17.38  
   17.39 @@ -373,7 +373,7 @@
   17.40  
   17.41  lemma even_power_le_0_imp_0:
   17.42      "a ^ (2*k) \<le> (0::'a::{linordered_idom}) ==> a=0"
   17.43 -  by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)
   17.44 +  by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
   17.45  
   17.46  lemma zero_le_power_iff[presburger]:
   17.47    "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)"
   17.48 @@ -387,7 +387,7 @@
   17.49    then obtain k where "n = Suc(2*k)"
   17.50      by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
   17.51    thus ?thesis
   17.52 -    by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power
   17.53 +    by (auto simp add: zero_le_mult_iff zero_le_even_power
   17.54               dest!: even_power_le_0_imp_0)
   17.55  qed
   17.56  
    18.1 --- a/src/HOL/Power.thy	Thu Feb 18 13:29:59 2010 -0800
    18.2 +++ b/src/HOL/Power.thy	Thu Feb 18 14:21:44 2010 -0800
    18.3 @@ -332,7 +332,7 @@
    18.4  
    18.5  lemma abs_power_minus [simp]:
    18.6    "abs ((-a) ^ n) = abs (a ^ n)"
    18.7 -  by (simp add: abs_minus_cancel power_abs) 
    18.8 +  by (simp add: power_abs)
    18.9  
   18.10  lemma zero_less_power_abs_iff [simp, noatp]:
   18.11    "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
    19.1 --- a/src/HOL/Presburger.thy	Thu Feb 18 13:29:59 2010 -0800
    19.2 +++ b/src/HOL/Presburger.thy	Thu Feb 18 14:21:44 2010 -0800
    19.3 @@ -199,16 +199,16 @@
    19.4      hence "P 0" using P Pmod by simp
    19.5      moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
    19.6      ultimately have "P d" by simp
    19.7 -    moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
    19.8 +    moreover have "d : {1..d}" using dpos by simp
    19.9      ultimately show ?RHS ..
   19.10    next
   19.11      assume not0: "x mod d \<noteq> 0"
   19.12 -    have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
   19.13 +    have "P(x mod d)" using dpos P Pmod by simp
   19.14      moreover have "x mod d : {1..d}"
   19.15      proof -
   19.16        from dpos have "0 \<le> x mod d" by(rule pos_mod_sign)
   19.17        moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
   19.18 -      ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
   19.19 +      ultimately show ?thesis using not0 by simp
   19.20      qed
   19.21      ultimately show ?RHS ..
   19.22    qed
    20.1 --- a/src/HOL/Rational.thy	Thu Feb 18 13:29:59 2010 -0800
    20.2 +++ b/src/HOL/Rational.thy	Thu Feb 18 14:21:44 2010 -0800
    20.3 @@ -428,7 +428,7 @@
    20.4    fix q :: rat
    20.5    assume "q \<noteq> 0"
    20.6    then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero)
    20.7 -   (simp_all add: mult_rat  inverse_rat rat_number_expand eq_rat)
    20.8 +   (simp_all add: rat_number_expand eq_rat)
    20.9  next
   20.10    fix q r :: rat
   20.11    show "q / r = q * inverse r" by (simp add: divide_rat_def)
   20.12 @@ -592,7 +592,7 @@
   20.13    abs_rat_def [code del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
   20.14  
   20.15  lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
   20.16 -  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)
   20.17 +  by (auto simp add: abs_rat_def zabs_def Zero_rat_def not_less le_less eq_rat zero_less_mult_iff)
   20.18  
   20.19  definition
   20.20    sgn_rat_def [code del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
    21.1 --- a/src/HOL/RealDef.thy	Thu Feb 18 13:29:59 2010 -0800
    21.2 +++ b/src/HOL/RealDef.thy	Thu Feb 18 14:21:44 2010 -0800
    21.3 @@ -767,7 +767,8 @@
    21.4  lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
    21.5  by (simp add: add: real_of_nat_def)
    21.6  
    21.7 -lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat))"
    21.8 +(* FIXME: duplicates real_of_nat_ge_zero *)
    21.9 +lemma real_of_nat_ge_zero_cancel_iff: "(0 \<le> real (n::nat))"
   21.10  by (simp add: add: real_of_nat_def)
   21.11  
   21.12  lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
   21.13 @@ -951,13 +952,13 @@
   21.14  
   21.15  text{*Collapse applications of @{term real} to @{term number_of}*}
   21.16  lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
   21.17 -by (simp add:  real_of_int_def of_int_number_of_eq)
   21.18 +by (simp add: real_of_int_def)
   21.19  
   21.20  lemma real_of_nat_number_of [simp]:
   21.21       "real (number_of v :: nat) =  
   21.22          (if neg (number_of v :: int) then 0  
   21.23           else (number_of v :: real))"
   21.24 -by (simp add: real_of_int_real_of_nat [symmetric] int_nat_number_of)
   21.25 +by (simp add: real_of_int_real_of_nat [symmetric])
   21.26  
   21.27  declaration {*
   21.28    K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]
    22.1 --- a/src/HOL/RealPow.thy	Thu Feb 18 13:29:59 2010 -0800
    22.2 +++ b/src/HOL/RealPow.thy	Thu Feb 18 14:21:44 2010 -0800
    22.3 @@ -19,8 +19,8 @@
    22.4  apply (induct "n")
    22.5  apply (auto simp add: real_of_nat_Suc)
    22.6  apply (subst mult_2)
    22.7 -apply (rule add_less_le_mono)
    22.8 -apply (auto simp add: two_realpow_ge_one)
    22.9 +apply (erule add_less_le_mono)
   22.10 +apply (rule two_realpow_ge_one)
   22.11  done
   22.12  
   22.13  lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
   22.14 @@ -57,7 +57,7 @@
   22.15  
   22.16  lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
   22.17  apply (induct "n")
   22.18 -apply (auto simp add: real_of_nat_mult zero_less_mult_iff)
   22.19 +apply (auto simp add: zero_less_mult_iff)
   22.20  done
   22.21  
   22.22  (* used by AFP Integration theory *)
    23.1 --- a/src/HOL/RealVector.thy	Thu Feb 18 13:29:59 2010 -0800
    23.2 +++ b/src/HOL/RealVector.thy	Thu Feb 18 14:21:44 2010 -0800
    23.3 @@ -268,7 +268,7 @@
    23.4  by (induct n) simp_all
    23.5  
    23.6  lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
    23.7 -by (simp add: of_real_def scaleR_cancel_right)
    23.8 +by (simp add: of_real_def)
    23.9  
   23.10  lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
   23.11  
    24.1 --- a/src/HOL/Rings.thy	Thu Feb 18 13:29:59 2010 -0800
    24.2 +++ b/src/HOL/Rings.thy	Thu Feb 18 14:21:44 2010 -0800
    24.3 @@ -315,7 +315,7 @@
    24.4  qed
    24.5  
    24.6  lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
    24.7 -by (simp add: diff_minus dvd_minus_iff)
    24.8 +by (simp only: diff_minus dvd_add dvd_minus_iff)
    24.9  
   24.10  end
   24.11  
   24.12 @@ -336,16 +336,16 @@
   24.13    "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   24.14  proof -
   24.15    have "(a * c = b * c) = ((a - b) * c = 0)"
   24.16 -    by (simp add: algebra_simps right_minus_eq)
   24.17 -  thus ?thesis by (simp add: disj_commute right_minus_eq)
   24.18 +    by (simp add: algebra_simps)
   24.19 +  thus ?thesis by (simp add: disj_commute)
   24.20  qed
   24.21  
   24.22  lemma mult_cancel_left [simp, noatp]:
   24.23    "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   24.24  proof -
   24.25    have "(c * a = c * b) = (c * (a - b) = 0)"
   24.26 -    by (simp add: algebra_simps right_minus_eq)
   24.27 -  thus ?thesis by (simp add: right_minus_eq)
   24.28 +    by (simp add: algebra_simps)
   24.29 +  thus ?thesis by simp
   24.30  qed
   24.31  
   24.32  end
   24.33 @@ -382,7 +382,7 @@
   24.34    then have "(a - b) * (a + b) = 0"
   24.35      by (simp add: algebra_simps)
   24.36    then show "a = b \<or> a = - b"
   24.37 -    by (simp add: right_minus_eq eq_neg_iff_add_eq_0)
   24.38 +    by (simp add: eq_neg_iff_add_eq_0)
   24.39  next
   24.40    assume "a = b \<or> a = - b"
   24.41    then show "a * a = b * b" by auto
   24.42 @@ -764,13 +764,13 @@
   24.43  lemma mult_left_mono_neg:
   24.44    "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   24.45    apply (drule mult_left_mono [of _ _ "uminus c"])
   24.46 -  apply (simp_all add: minus_mult_left [symmetric]) 
   24.47 +  apply simp_all
   24.48    done
   24.49  
   24.50  lemma mult_right_mono_neg:
   24.51    "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   24.52    apply (drule mult_right_mono [of _ _ "uminus c"])
   24.53 -  apply (simp_all add: minus_mult_right [symmetric]) 
   24.54 +  apply simp_all
   24.55    done
   24.56  
   24.57  lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   24.58 @@ -791,11 +791,10 @@
   24.59  proof
   24.60    fix a b
   24.61    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   24.62 -    by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
   24.63 -    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
   24.64 -     neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
   24.65 -      auto intro!: less_imp_le add_neg_neg)
   24.66 -qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
   24.67 +    by (auto simp add: abs_if not_less)
   24.68 +    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
   24.69 +     auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
   24.70 +qed (auto simp add: abs_if)
   24.71  
   24.72  end
   24.73  
   24.74 @@ -864,14 +863,14 @@
   24.75  
   24.76  lemma mult_less_0_iff:
   24.77    "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
   24.78 -  apply (insert zero_less_mult_iff [of "-a" b]) 
   24.79 -  apply (force simp add: minus_mult_left[symmetric]) 
   24.80 +  apply (insert zero_less_mult_iff [of "-a" b])
   24.81 +  apply force
   24.82    done
   24.83  
   24.84  lemma mult_le_0_iff:
   24.85    "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   24.86    apply (insert zero_le_mult_iff [of "-a" b]) 
   24.87 -  apply (force simp add: minus_mult_left[symmetric]) 
   24.88 +  apply force
   24.89    done
   24.90  
   24.91  lemma zero_le_square [simp]: "0 \<le> a * a"
   24.92 @@ -1056,11 +1055,11 @@
   24.93  
   24.94  lemma sgn_1_pos:
   24.95    "sgn a = 1 \<longleftrightarrow> a > 0"
   24.96 -unfolding sgn_if by (simp add: neg_equal_zero)
   24.97 +unfolding sgn_if by simp
   24.98  
   24.99  lemma sgn_1_neg:
  24.100    "sgn a = - 1 \<longleftrightarrow> a < 0"
  24.101 -unfolding sgn_if by (auto simp add: equal_neg_zero)
  24.102 +unfolding sgn_if by auto
  24.103  
  24.104  lemma sgn_pos [simp]:
  24.105    "0 < a \<Longrightarrow> sgn a = 1"
  24.106 @@ -1116,11 +1115,11 @@
  24.107  
  24.108  lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
  24.109      ==> x * y <= x"
  24.110 -by (auto simp add: mult_compare_simps)
  24.111 +by (auto simp add: mult_le_cancel_left2)
  24.112  
  24.113  lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
  24.114      ==> y * x <= x"
  24.115 -by (auto simp add: mult_compare_simps)
  24.116 +by (auto simp add: mult_le_cancel_right2)
  24.117  
  24.118  context linordered_semidom
  24.119  begin
  24.120 @@ -1159,7 +1158,7 @@
  24.121  begin
  24.122  
  24.123  subclass ordered_ring_abs proof
  24.124 -qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)
  24.125 +qed (auto simp add: abs_if not_less mult_less_0_iff)
  24.126  
  24.127  lemma abs_mult:
  24.128    "abs (a * b) = abs a * abs b" 
  24.129 @@ -1187,7 +1186,7 @@
  24.130  
  24.131  lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))" 
  24.132  apply (simp add: order_less_le abs_le_iff)  
  24.133 -apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
  24.134 +apply (auto simp add: abs_if)
  24.135  done
  24.136  
  24.137  lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> 
    25.1 --- a/src/HOL/SEQ.thy	Thu Feb 18 13:29:59 2010 -0800
    25.2 +++ b/src/HOL/SEQ.thy	Thu Feb 18 14:21:44 2010 -0800
    25.3 @@ -573,7 +573,7 @@
    25.4  apply (rule allI, rule impI, rule ext)
    25.5  apply (erule conjE)
    25.6  apply (induct_tac x)
    25.7 -apply (simp add: nat_rec_0)
    25.8 +apply simp
    25.9  apply (erule_tac x="n" in allE)
   25.10  apply (simp)
   25.11  done
    26.1 --- a/src/HOL/SetInterval.thy	Thu Feb 18 13:29:59 2010 -0800
    26.2 +++ b/src/HOL/SetInterval.thy	Thu Feb 18 14:21:44 2010 -0800
    26.3 @@ -539,7 +539,7 @@
    26.4    apply (rule subset_antisym)
    26.5     apply (rule UN_finite2_subset, blast)
    26.6   apply (rule UN_finite2_subset [where k=k])
    26.7 - apply (force simp add: atLeastLessThan_add_Un [of 0] UN_Un) 
    26.8 + apply (force simp add: atLeastLessThan_add_Un [of 0])
    26.9   done
   26.10  
   26.11  
   26.12 @@ -613,7 +613,7 @@
   26.13    apply (unfold image_def lessThan_def)
   26.14    apply auto
   26.15    apply (rule_tac x = "nat x" in exI)
   26.16 -  apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym])
   26.17 +  apply (auto simp add: zless_nat_eq_int_zless [THEN sym])
   26.18    done
   26.19  
   26.20  lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
   26.21 @@ -1006,7 +1006,7 @@
   26.22    shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
   26.23  proof-
   26.24    have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)
   26.25 -  also have "\<dots> = ?r" by(simp add: setsum_constant mult_commute)
   26.26 +  also have "\<dots> = ?r" by(simp add: mult_commute)
   26.27    finally show ?thesis by auto
   26.28  qed
   26.29  
   26.30 @@ -1046,7 +1046,7 @@
   26.31  lemma geometric_sum:
   26.32    "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
   26.33    (x ^ n - 1) / (x - 1::'a::{field})"
   26.34 -by (induct "n") (simp_all add:field_simps power_Suc)
   26.35 +by (induct "n") (simp_all add: field_simps)
   26.36  
   26.37  subsection {* The formula for arithmetic sums *}
   26.38  
   26.39 @@ -1098,7 +1098,7 @@
   26.40      of_nat(n) * (a + (a + of_nat(n - 1)*d))"
   26.41      by (rule arith_series_general)
   26.42    thus ?thesis
   26.43 -    unfolding One_nat_def by (auto simp add: of_nat_id)
   26.44 +    unfolding One_nat_def by auto
   26.45  qed
   26.46  
   26.47  lemma arith_series_int:
    27.1 --- a/src/HOL/SupInf.thy	Thu Feb 18 13:29:59 2010 -0800
    27.2 +++ b/src/HOL/SupInf.thy	Thu Feb 18 14:21:44 2010 -0800
    27.3 @@ -249,7 +249,7 @@
    27.4        and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
    27.5    shows "z \<le> Inf X"
    27.6  proof -
    27.7 -  have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
    27.8 +  have "Sup (uminus ` X) \<le> -z" using x z by force
    27.9    hence "z \<le> - Sup (uminus ` X)"
   27.10      by simp
   27.11    thus ?thesis 
   27.12 @@ -306,7 +306,7 @@
   27.13    case True
   27.14    thus ?thesis
   27.15      by (simp add: min_def)
   27.16 -       (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z) 
   27.17 +       (blast intro: Inf_eq_minimum real_le_refl real_le_trans z)
   27.18  next
   27.19    case False
   27.20    hence 1:"Inf X < a" by simp
   27.21 @@ -441,7 +441,7 @@
   27.22  proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
   27.23    show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   27.24      by (rule SupInf.Sup_upper [where z=b], auto)
   27.25 -       (metis prems real_le_linear real_less_def) 
   27.26 +       (metis `a < b` `\<not> P b` real_le_linear real_less_def)
   27.27  next
   27.28    show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
   27.29      apply (rule SupInf.Sup_least) 
    28.1 --- a/src/HOL/Transcendental.thy	Thu Feb 18 13:29:59 2010 -0800
    28.2 +++ b/src/HOL/Transcendental.thy	Thu Feb 18 14:21:44 2010 -0800
    28.3 @@ -848,7 +848,7 @@
    28.4      hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
    28.5        by (simp add: pos_divide_le_eq mult_ac)
    28.6      thus "norm (S (Suc n)) \<le> r * norm (S n)"
    28.7 -      by (simp add: S_Suc norm_scaleR inverse_eq_divide)
    28.8 +      by (simp add: S_Suc inverse_eq_divide)
    28.9    qed
   28.10  qed
   28.11  
   28.12 @@ -860,7 +860,7 @@
   28.13      by (rule summable_exp_generic)
   28.14  next
   28.15    fix n show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
   28.16 -    by (simp add: norm_scaleR norm_power_ineq)
   28.17 +    by (simp add: norm_power_ineq)
   28.18  qed
   28.19  
   28.20  lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)"
   28.21 @@ -957,7 +957,7 @@
   28.22      by (simp only: scaleR_right.setsum)
   28.23    finally show
   28.24      "S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
   28.25 -    by (simp add: scaleR_cancel_left del: setsum_cl_ivl_Suc)
   28.26 +    by (simp del: setsum_cl_ivl_Suc)
   28.27  qed
   28.28  
   28.29  lemma exp_add: "exp (x + y) = exp x * exp y"
   28.30 @@ -1237,7 +1237,7 @@
   28.31        { fix x :: real assume "x \<in> {- 1<..<1}" hence "norm (-x) < 1" by auto
   28.32          show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
   28.33            unfolding One_nat_def
   28.34 -          by (auto simp del: power_mult_distrib simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
   28.35 +          by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
   28.36        }
   28.37      qed
   28.38      hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" unfolding One_nat_def by auto
   28.39 @@ -3090,7 +3090,7 @@
   28.40  
   28.41  lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<twosuperior> + y\<twosuperior>)\<bar> \<le> 1"
   28.42  apply (rule power2_le_imp_le [OF _ zero_le_one])
   28.43 -apply (simp add: abs_divide power_divide divide_le_eq not_sum_power2_lt_zero)
   28.44 +apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
   28.45  done
   28.46  
   28.47  lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
    29.1 --- a/src/HOL/Transitive_Closure.thy	Thu Feb 18 13:29:59 2010 -0800
    29.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Feb 18 14:21:44 2010 -0800
    29.3 @@ -464,7 +464,7 @@
    29.4     apply (rule subsetI)
    29.5     apply (simp only: split_tupled_all)
    29.6     apply (erule trancl_induct, blast)
    29.7 -   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)
    29.8 +   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)
    29.9    apply (rule subsetI)
   29.10    apply (blast intro: trancl_mono rtrancl_mono
   29.11      [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   29.12 @@ -503,7 +503,7 @@
   29.13    apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major])
   29.14     apply (rule cases)
   29.15     apply (erule conversepD)
   29.16 -  apply (blast intro: prems dest!: tranclp_converseD conversepD)
   29.17 +  apply (blast intro: assms dest!: tranclp_converseD)
   29.18    done
   29.19  
   29.20  lemmas converse_trancl_induct = converse_tranclp_induct [to_set]
    30.1 --- a/src/HOL/Wellfounded.thy	Thu Feb 18 13:29:59 2010 -0800
    30.2 +++ b/src/HOL/Wellfounded.thy	Thu Feb 18 14:21:44 2010 -0800
    30.3 @@ -489,7 +489,7 @@
    30.4    by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
    30.5  
    30.6  lemma trans_less_than [iff]: "trans less_than"
    30.7 -  by (simp add: less_than_def trans_trancl)
    30.8 +  by (simp add: less_than_def)
    30.9  
   30.10  lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
   30.11    by (simp add: less_than_def less_eq)