--- a/src/HOL/BNF_Def.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/BNF_Def.thy Fri May 13 20:24:10 2016 +0200
@@ -248,7 +248,7 @@
by (simp add: eq_onp_def)
lemma eq_onp_same_args: "eq_onp P x x = P x"
- using assms by (auto simp add: eq_onp_def)
+ by (auto simp add: eq_onp_def)
lemma eq_onp_eqD: "eq_onp P = Q \<Longrightarrow> P x = Q x x"
unfolding eq_onp_def by blast
--- a/src/HOL/BNF_Wellorder_Constructions.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/BNF_Wellorder_Constructions.thy Fri May 13 20:24:10 2016 +0200
@@ -570,7 +570,7 @@
lemma not_ordLess_ordIso:
"r <o r' \<Longrightarrow> \<not> r =o r'"
-using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
+using ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
lemma not_ordLeq_iff_ordLess:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
@@ -584,7 +584,7 @@
lemma ordLess_transitive[trans]:
"\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
-using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
+using ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
corollary ordLess_trans: "trans ordLess"
unfolding trans_def using ordLess_transitive by blast
@@ -1003,7 +1003,7 @@
lemma Well_order_dir_image:
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
-using assms unfolding well_order_on_def
+unfolding well_order_on_def
using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
dir_image_minus_Id[of f r]
subset_inj_on[of f "Field r" "Field(r - Id)"]
--- a/src/HOL/BNF_Wellorder_Embedding.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/BNF_Wellorder_Embedding.thy Fri May 13 20:24:10 2016 +0200
@@ -986,7 +986,7 @@
lemma iso_Field:
"iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
-using assms by (auto simp add: iso_def bij_betw_def)
+by (auto simp add: iso_def bij_betw_def)
lemma iso_iff:
assumes "Well_order r"
--- a/src/HOL/Binomial.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Binomial.thy Fri May 13 20:24:10 2016 +0200
@@ -1324,7 +1324,7 @@
proof -
have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
- by (simp add: assms binomial_altdef_nat)
+ by (simp add: binomial_altdef_nat)
also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
apply (subst div_mult_div_if_dvd)
apply (auto simp: algebra_simps fact_fact_dvd_fact)
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Fri May 13 20:24:10 2016 +0200
@@ -1105,7 +1105,7 @@
proof(auto simp add: natLeq_on_Well_order ordIso_reflexive)
assume "natLeq_on m =o natLeq_on n"
then obtain f where "bij_betw f {x. x<m} {x. x<n}"
- using Field_natLeq_on assms unfolding ordIso_def iso_def[abs_def] by auto
+ using Field_natLeq_on unfolding ordIso_def iso_def[abs_def] by auto
thus "m = n" using atLeastLessThan_injective2[of f m n]
unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
qed
--- a/src/HOL/Conditionally_Complete_Lattices.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Fri May 13 20:24:10 2016 +0200
@@ -297,10 +297,10 @@
using cSup_least [of "f ` A"] by auto
lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFIMUM A f \<le> u"
- by (auto intro: cINF_lower assms order_trans)
+ by (auto intro: cINF_lower order_trans)
lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPREMUM A f"
- by (auto intro: cSUP_upper assms order_trans)
+ by (auto intro: cSUP_upper order_trans)
lemma cSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c"
by (intro antisym cSUP_least) (auto intro: cSUP_upper)
@@ -309,10 +309,10 @@
by (intro antisym cINF_greatest) (auto intro: cINF_lower)
lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFIMUM A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
- by (metis cINF_greatest cINF_lower assms order_trans)
+ by (metis cINF_greatest cINF_lower order_trans)
lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
- by (metis cSUP_least cSUP_upper assms order_trans)
+ by (metis cSUP_least cSUP_upper order_trans)
lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
by (metis cINF_lower less_le_trans)
--- a/src/HOL/Deriv.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Deriv.thy Fri May 13 20:24:10 2016 +0200
@@ -89,7 +89,7 @@
lemma (in bounded_linear) has_derivative:
"(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F"
- using assms unfolding has_derivative_def
+ unfolding has_derivative_def
apply safe
apply (erule bounded_linear_compose [OF bounded_linear])
apply (drule tendsto)
@@ -537,7 +537,7 @@
lemma differentiable_divide [simp, derivative_intros]:
fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable (at x within s)"
- unfolding divide_inverse using assms by simp
+ unfolding divide_inverse by simp
lemma differentiable_power [simp, derivative_intros]:
fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
@@ -742,7 +742,7 @@
lemma field_differentiable_diff[derivative_intros]:
"(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow> ((\<lambda>z. f z - g z) has_field_derivative f' - g') F"
- by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
+ by (simp only: diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
corollary DERIV_diff:
"(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
--- a/src/HOL/Equiv_Relations.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Equiv_Relations.thy Fri May 13 20:24:10 2016 +0200
@@ -266,7 +266,7 @@
lemma congruent2D:
"congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
- using assms by (auto simp add: congruent2_def)
+ by (auto simp add: congruent2_def)
text\<open>Abbreviation for the common case where the relations are identical\<close>
abbreviation
@@ -426,7 +426,7 @@
lemma in_quotient_imp_subset:
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<subseteq> A"
-using assms in_quotient_imp_in_rel equiv_type by fastforce
+using in_quotient_imp_in_rel equiv_type by fastforce
subsection \<open>Equivalence relations -- predicate version\<close>
--- a/src/HOL/Groups_Big.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Groups_Big.thy Fri May 13 20:24:10 2016 +0200
@@ -181,7 +181,7 @@
lemma distrib:
"F (\<lambda>x. g x * h x) A = F g A * F h A"
- using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
+ by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
lemma Sigma:
"finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)"
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Fri May 13 20:24:10 2016 +0200
@@ -261,7 +261,6 @@
subsection {* Interaction of these predicates with our heap transitions *}
lemma list_of_set_ref: "refs_of h q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> list_of (Ref.set p v h) q as = list_of h q as"
-using assms
proof (induct as arbitrary: q rs)
case Nil thus ?case by simp
next
--- a/src/HOL/Library/Complete_Partial_Order2.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Fri May 13 20:24:10 2016 +0200
@@ -1552,7 +1552,7 @@
lemma mcont_SUP [cont_intro, simp]:
"\<lbrakk> mcont lub ord Union op \<subseteq> f; \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. g x y) \<rbrakk>
\<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. \<Squnion>y\<in>f x. g x y)"
-by(blast intro: mcontI cont_SUP[OF assms] monotone_SUP mcont_mono)
+by(blast intro: mcontI cont_SUP monotone_SUP mcont_mono)
end
--- a/src/HOL/Library/ContNotDenum.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/ContNotDenum.thy Fri May 13 20:24:10 2016 +0200
@@ -37,7 +37,6 @@
txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>
have "\<forall>a b c::real. a < b \<longrightarrow> (\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb})"
- using assms
by (auto simp add: not_le cong: conj_cong)
(metis dense le_less_linear less_linear less_trans order_refl)
then obtain i j where ij:
--- a/src/HOL/Library/Convex.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Convex.thy Fri May 13 20:24:10 2016 +0200
@@ -533,7 +533,7 @@
by (auto simp: add_pos_pos)
}
ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0"
- using assms by fastforce
+ by fastforce
qed
lemma convex_on_setsum:
--- a/src/HOL/Library/Countable_Set.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Countable_Set.thy Fri May 13 20:24:10 2016 +0200
@@ -228,7 +228,7 @@
by auto (metis Diff_insert_absorb countable_Diff insert_absorb)
lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
- by (metis Int_absorb2 assms countable_image image_vimage_eq)
+ by (metis Int_absorb2 countable_image image_vimage_eq)
lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
by (metis countable_vimage top_greatest)
@@ -342,7 +342,7 @@
lemma uncountable_minus_countable:
"uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
- using countable_Un[of B "A - B"] assms by auto
+ using countable_Un[of B "A - B"] by auto
lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)
--- a/src/HOL/Library/Extended_Real.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri May 13 20:24:10 2016 +0200
@@ -281,7 +281,7 @@
obtains (real) r where "x = ereal r"
| (PInf) "x = \<infinity>"
| (MInf) "x = -\<infinity>"
- using assms by (cases x) auto
+ by (cases x) auto
lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]
@@ -1009,7 +1009,6 @@
lemma ereal_mult_right_mono:
fixes a b c :: ereal
shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
- using assms
apply (cases "c = 0")
apply simp
apply (cases rule: ereal3_cases[of a b c])
--- a/src/HOL/Library/FSet.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/FSet.thy Fri May 13 20:24:10 2016 +0200
@@ -855,7 +855,7 @@
lemma bind_transfer [transfer_rule]:
"(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind"
- using assms unfolding rel_fun_def
+ unfolding rel_fun_def
using bind_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
text \<open>Rules requiring bi-unique, bi-total or right-total relations\<close>
@@ -885,7 +885,7 @@
lemma fSup_transfer [transfer_rule]:
"bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup"
- using assms unfolding rel_fun_def
+ unfolding rel_fun_def
apply clarify
apply transfer'
using Sup_fset_transfer[unfolded rel_fun_def] by blast
@@ -908,7 +908,7 @@
lemma card_transfer [transfer_rule]:
"bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard"
- using assms unfolding rel_fun_def
+ unfolding rel_fun_def
using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
end
--- a/src/HOL/Library/Fraction_Field.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Fri May 13 20:24:10 2016 +0200
@@ -278,7 +278,7 @@
lemma less_fract [simp]:
"\<lbrakk> b \<noteq> 0; d \<noteq> 0 \<rbrakk> \<Longrightarrow> Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)"
- by (simp add: less_fract_def less_le_not_le ac_simps assms)
+ by (simp add: less_fract_def less_le_not_le ac_simps)
instance
proof
--- a/src/HOL/Library/FuncSet.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/FuncSet.thy Fri May 13 20:24:10 2016 +0200
@@ -402,17 +402,17 @@
proof -
{
fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
- with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+ then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
}
moreover
{
fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
- with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+ then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
}
ultimately show ?thesis
- using assms by (auto intro: PiE_fun_upd)
+ by (auto intro: PiE_fun_upd)
qed
lemma PiE_Int: "Pi\<^sub>E I A \<inter> Pi\<^sub>E I B = Pi\<^sub>E I (\<lambda>x. A x \<inter> B x)"
--- a/src/HOL/Library/Indicator_Function.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Indicator_Function.thy Fri May 13 20:24:10 2016 +0200
@@ -79,7 +79,7 @@
lemma setsum_indicator_scaleR[simp]:
"finite A \<Longrightarrow>
(\<Sum>x \<in> A. indicator (B x) (g x) *\<^sub>R f x) = (\<Sum>x \<in> {x\<in>A. g x \<in> B x}. f x::'a::real_vector)"
- using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
+ by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
lemma LIMSEQ_indicator_incseq:
assumes "incseq A"
--- a/src/HOL/Library/Multiset.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Fri May 13 20:24:10 2016 +0200
@@ -967,7 +967,7 @@
lemma multiset_cases [cases type]:
obtains (empty) "M = {#}"
| (add) N x where "M = N + {#x#}"
- using assms by (induct M) simp_all
+ by (induct M) simp_all
lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
by (cases "B = {#}") (auto dest: multi_member_split)
@@ -1455,7 +1455,7 @@
by (induct n, simp_all)
lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
- by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
+ by (auto simp add: mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
by (induct D) simp_all
--- a/src/HOL/Library/Nonpos_Ints.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Nonpos_Ints.thy Fri May 13 20:24:10 2016 +0200
@@ -54,7 +54,7 @@
lemma nonpos_IntsI:
"x \<in> \<int> \<Longrightarrow> x \<le> 0 \<Longrightarrow> (x :: 'a :: linordered_idom) \<in> \<int>\<^sub>\<le>\<^sub>0"
- using assms unfolding nonpos_Ints_def Ints_def by auto
+ unfolding nonpos_Ints_def Ints_def by auto
lemma nonpos_Ints_subset_Ints: "\<int>\<^sub>\<le>\<^sub>0 \<subseteq> \<int>"
unfolding nonpos_Ints_def Ints_def by blast
--- a/src/HOL/Lifting.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Lifting.thy Fri May 13 20:24:10 2016 +0200
@@ -311,7 +311,7 @@
using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp
lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
- using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
+ using 1 2 unfolding Quotient_alt_def reflp_def by metis
lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y"
using Quotient_rel [OF 1] 2 unfolding reflp_def by simp
--- a/src/HOL/List.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/List.thy Fri May 13 20:24:10 2016 +0200
@@ -2297,7 +2297,7 @@
by (induct xs) auto
lemma hd_dropWhile: "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
-using assms by (induct xs) auto
+by (induct xs) auto
lemma takeWhile_eq_filter:
assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
@@ -4956,8 +4956,7 @@
lemma filter_insort:
"sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
- using assms by (induct xs)
- (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
+ by (induct xs) (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
lemma filter_sort:
"filter P (sort_key f xs) = sort_key f (filter P xs)"
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri May 13 20:24:10 2016 +0200
@@ -1798,7 +1798,6 @@
\<Longrightarrow> contour_integral (linepath a b) f =
contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f"
apply (rule contour_integral_split [where c = "midpoint a b" and k = "1/2"])
- using assms
apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real)
done
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Fri May 13 20:24:10 2016 +0200
@@ -179,7 +179,7 @@
lemma DERIV_zero_UNIV_unique:
fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
-by (metis DERIV_zero_unique UNIV_I assms convex_UNIV)
+by (metis DERIV_zero_unique UNIV_I convex_UNIV)
subsection \<open>Some limit theorems about real part of real series etc.\<close>
@@ -322,7 +322,7 @@
lemma field_differentiable_minus [derivative_intros]:
"f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
- using assms unfolding field_differentiable_def
+ unfolding field_differentiable_def
by (metis field_differentiable_minus)
lemma field_differentiable_add [derivative_intros]:
@@ -1047,7 +1047,6 @@
\<Longrightarrow> DERIV g (f x) :> inverse (f')"
unfolding has_field_derivative_def
apply (rule has_derivative_inverse_strong [of s x f g ])
- using assms
by auto
lemma has_complex_derivative_inverse_strong_x:
@@ -1061,7 +1060,6 @@
\<Longrightarrow> DERIV g y :> inverse (f')"
unfolding has_field_derivative_def
apply (rule has_derivative_inverse_strong_x [of s g y f])
- using assms
by auto
subsection \<open>Taylor on Complex Numbers\<close>
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Fri May 13 20:24:10 2016 +0200
@@ -984,7 +984,7 @@
using Ln_exp by blast
lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
- by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
+ by (metis exp_Ln ln_exp norm_exp_eq_Re)
corollary ln_cmod_le:
assumes z: "z \<noteq> 0"
@@ -1608,7 +1608,7 @@
hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)
also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \<i>"
by (simp add: Ln_minus Ln_of_real)
- also from x assms have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
+ also from x have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)
also note cis_pi
finally show ?thesis by simp
@@ -1621,7 +1621,7 @@
apply (simp add: powr_def)
apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
apply (auto simp: dist_complex_def)
- apply (intro derivative_eq_intros | simp add: assms)+
+ apply (intro derivative_eq_intros | simp)+
apply (simp add: field_simps exp_diff)
done
@@ -1631,7 +1631,7 @@
lemma has_field_derivative_powr_right:
"w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
apply (simp add: powr_def)
- apply (intro derivative_eq_intros | simp add: assms)+
+ apply (intro derivative_eq_intros | simp)+
done
lemma field_differentiable_powr_right:
@@ -1772,7 +1772,7 @@
qed
lemma lim_1_over_ln: "((\<lambda>n. 1 / ln(real_of_nat n)) \<longlongrightarrow> 0) sequentially"
- using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]] assms
+ using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]]
apply (subst filterlim_sequentially_Suc [symmetric])
apply (simp add: lim_sequentially dist_norm)
apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide)
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri May 13 20:24:10 2016 +0200
@@ -2427,9 +2427,9 @@
moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
by auto
moreover have "insert a (s - {a}) = insert a s"
- using assms by auto
+ by auto
ultimately have ?thesis
- using assms affine_hull_insert_span[of "a" "s-{a}"] by auto
+ using affine_hull_insert_span[of "a" "s-{a}"] by auto
}
ultimately show ?thesis by auto
qed
@@ -2998,7 +2998,7 @@
have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
using aff_dim_UNIV by auto
then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
- using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
+ using aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
qed
lemma affine_dim_equal:
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri May 13 20:24:10 2016 +0200
@@ -4189,7 +4189,7 @@
lemma additive_content_tagged_division:
"d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
- unfolding operative_tagged_division[OF monoidal_monoid operative_content assms,symmetric]
+ unfolding operative_tagged_division[OF monoidal_monoid operative_content,symmetric]
using setsum_iterate by blast
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri May 13 20:24:10 2016 +0200
@@ -1318,7 +1318,6 @@
by (auto intro!: path_component_mem path_component_refl)
lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x"
- using assms
unfolding path_component_def
apply (erule exE)
apply (rule_tac x="reversepath g" in exI)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri May 13 20:24:10 2016 +0200
@@ -2791,7 +2791,7 @@
lemma closed_contains_Inf:
fixes S :: "real set"
shows "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> closed S \<Longrightarrow> Inf S \<in> S"
- by (metis closure_contains_Inf closure_closed assms)
+ by (metis closure_contains_Inf closure_closed)
lemma closed_subset_contains_Inf:
fixes A C :: "real set"
--- a/src/HOL/Number_Theory/Cong.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Fri May 13 20:24:10 2016 +0200
@@ -341,7 +341,7 @@
lemma cong_gcd_eq_nat:
"[(a::nat) = b] (mod m) \<Longrightarrow>gcd a m = gcd b m"
- by (metis assms cong_gcd_eq_int [transferred])
+ by (metis cong_gcd_eq_int [transferred])
lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
by (auto simp add: cong_gcd_eq_nat)
--- a/src/HOL/Probability/Bochner_Integration.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Fri May 13 20:24:10 2016 +0200
@@ -943,7 +943,7 @@
lemma integrable_cong:
"M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable N g"
- using assms by (simp cong: has_bochner_integral_cong add: integrable.simps)
+ by (simp cong: has_bochner_integral_cong add: integrable.simps)
lemma integrable_cong_AE:
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
@@ -953,7 +953,7 @@
lemma integral_cong:
"M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g"
- using assms by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
+ by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
lemma integral_cong_AE:
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
--- a/src/HOL/Probability/Distribution_Functions.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Distribution_Functions.thy Fri May 13 20:24:10 2016 +0200
@@ -64,7 +64,7 @@
unfolding cdf_def by (rule measure_nonneg)
lemma cdf_bounded: "cdf M x \<le> measure M (space M)"
- unfolding cdf_def using assms by (intro bounded_measure)
+ unfolding cdf_def by (intro bounded_measure)
lemma cdf_lim_infty:
"((\<lambda>i. cdf M (real i)) \<longlonglongrightarrow> measure M (space M))"
--- a/src/HOL/Probability/Giry_Monad.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Fri May 13 20:24:10 2016 +0200
@@ -771,7 +771,7 @@
done
with M show "subprob_space (join M)"
by (intro subprob_spaceI)
- (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)
+ (auto simp: emeasure_join space_subprob_algebra M dest: subprob_space.emeasure_space_le_1)
next
assume "\<not>(space N \<noteq> {})"
thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
--- a/src/HOL/Probability/Interval_Integral.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Interval_Integral.thy Fri May 13 20:24:10 2016 +0200
@@ -335,13 +335,13 @@
lemma interval_integral_zero [simp]:
fixes a b :: ereal
shows"LBINT x=a..b. 0 = 0"
-using assms unfolding interval_lebesgue_integral_def einterval_eq
+unfolding interval_lebesgue_integral_def einterval_eq
by simp
lemma interval_integral_const [intro, simp]:
fixes a b c :: real
shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
-using assms unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
+unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
by (auto simp add: less_imp_le field_simps measure_def)
lemma interval_integral_cong_AE:
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri May 13 20:24:10 2016 +0200
@@ -923,7 +923,7 @@
lemma nn_integral_monotone_convergence_simple:
"incseq f \<Longrightarrow> (\<And>i. simple_function M (f i)) \<Longrightarrow> (SUP i. \<integral>\<^sup>S x. f i x \<partial>M) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
- using assms nn_integral_monotone_convergence_SUP[of f M]
+ using nn_integral_monotone_convergence_SUP[of f M]
by (simp add: nn_integral_eq_simple_integral[symmetric] borel_measurable_simple_function)
lemma SUP_simple_integral_sequences:
@@ -986,7 +986,7 @@
using nn_integral_linear[of f M "\<lambda>x. 0" c] by simp
lemma nn_integral_multc: "f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c"
- unfolding mult.commute[of _ c] nn_integral_cmult[OF assms] by simp
+ unfolding mult.commute[of _ c] nn_integral_cmult by simp
lemma nn_integral_divide: "f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. f x / c \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M) / c"
unfolding divide_ennreal_def by (rule nn_integral_multc)
--- a/src/HOL/Probability/Probability_Mass_Function.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Fri May 13 20:24:10 2016 +0200
@@ -653,7 +653,7 @@
qed
lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \<noteq> 0}"
-by(auto simp add: set_pmf_eq assms pmf_embed_pmf)
+by(auto simp add: set_pmf_eq pmf_embed_pmf)
end
@@ -1563,7 +1563,7 @@
ennreal_of_nat_eq_real_of_nat nn_integral_pmf_of_set)
lemma measure_pmf_of_set: "measure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
- using emeasure_pmf_of_set[OF assms, of A]
+ using emeasure_pmf_of_set[of A]
by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure)
end
--- a/src/HOL/Probability/Set_Integral.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Set_Integral.thy Fri May 13 20:24:10 2016 +0200
@@ -183,7 +183,6 @@
lemma set_integral_reflect:
fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
- using assms
by (subst lborel_integral_real_affine[where c="-1" and t=0])
(auto intro!: integral_cong split: split_indicator)
--- a/src/HOL/SPARK/Tools/spark_commands.ML Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri May 13 20:24:10 2016 +0200
@@ -48,7 +48,7 @@
val thy = Proof_Context.theory_of lthy;
val (ctxt, stmt) = get_vc thy vc_name
in
- Specification.theorem Thm.theoremK NONE
+ Specification.theorem true Thm.theoremK NONE
(fn thmss => (Local_Theory.background_theory
(SPARK_VCs.mark_proved vc_name (flat thmss))))
(Binding.name vc_name, []) [] ctxt stmt false lthy
--- a/src/HOL/Set_Interval.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Set_Interval.thy Fri May 13 20:24:10 2016 +0200
@@ -625,7 +625,7 @@
by (auto simp: min_def)
lemma Ioc_disjoint: "{a<..b} \<inter> {c<..d} = {} \<longleftrightarrow> b \<le> a \<or> d \<le> c \<or> b \<le> c \<or> d \<le> a"
- using assms by auto
+ by auto
end
--- a/src/HOL/Topological_Spaces.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy Fri May 13 20:24:10 2016 +0200
@@ -1367,7 +1367,7 @@
lemma (in first_countable_topology) sequentially_imp_eventually_at:
"(\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow> eventually P (at a)"
- using assms sequentially_imp_eventually_within [where s=UNIV] by simp
+ using sequentially_imp_eventually_within [where s=UNIV] by simp
lemma LIMSEQ_SEQ_conv1:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
--- a/src/HOL/Transcendental.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Transcendental.thy Fri May 13 20:24:10 2016 +0200
@@ -2203,7 +2203,7 @@
lemma powr_mult_base:
fixes x::real shows "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
- using assms by (auto simp: powr_add)
+ by (auto simp: powr_add)
lemma powr_powr:
fixes x::real shows "(x powr a) powr b = x powr (a * b)"
--- a/src/HOL/Transfer.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Transfer.thy Fri May 13 20:24:10 2016 +0200
@@ -510,7 +510,7 @@
"right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
"bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
-using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
+unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
by fast+
lemma right_unique_transfer [transfer_rule]: