--- 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 ***)
--- 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" ..
--- 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
--- 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
--- 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}))"
--- 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"
--- 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
--- 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
--- 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"
--- 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)
--- 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)
--- 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}
--- 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 *}
--- 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}*}
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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)"
--- 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]
--- 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 *)
--- 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]
--- 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 ==>
--- 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
--- 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:
--- 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)
--- 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"
--- 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]
--- 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)