--- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy Fri May 27 20:23:55 2016 +0200
@@ -480,8 +480,8 @@
proof-
{fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
apply(induct rule: wf_raw_coind) apply safe
- unfolding deftr_simps image_comp map_sum.comp id_comp
- root_o_deftr map_sum.id image_id id_apply apply(rule S_P)
+ apply (simp only: deftr_simps image_comp map_sum.comp id_comp
+ root_o_deftr map_sum.id image_id id_apply) apply(rule S_P)
unfolding inj_on_def by auto
}
thus ?thesis by auto
--- a/src/HOL/Decision_Procs/Approximation.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri May 27 20:23:55 2016 +0200
@@ -514,9 +514,10 @@
proof -
have "(sqrt y * lb_arctan_horner prec n 1 y) \<le> ?S n"
using bounds(1) \<open>0 \<le> sqrt y\<close>
- unfolding power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric]
- unfolding mult.commute[where 'a=real] mult.commute[of _ "2::nat"] power_mult
- by (auto intro!: mult_left_mono)
+ apply (simp only: power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric])
+ apply (simp only: mult.commute[where 'a=real] mult.commute[of _ "2::nat"] power_mult)
+ apply (auto intro!: mult_left_mono)
+ done
also have "\<dots> \<le> arctan (sqrt y)" using arctan_bounds ..
finally show ?thesis .
qed
@@ -526,9 +527,10 @@
have "arctan (sqrt y) \<le> ?S (Suc n)" using arctan_bounds ..
also have "\<dots> \<le> (sqrt y * ub_arctan_horner prec (Suc n) 1 y)"
using bounds(2)[of "Suc n"] \<open>0 \<le> sqrt y\<close>
- unfolding power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric]
- unfolding mult.commute[where 'a=real] mult.commute[of _ "2::nat"] power_mult
- by (auto intro!: mult_left_mono)
+ apply (simp only: power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric])
+ apply (simp only: mult.commute[where 'a=real] mult.commute[of _ "2::nat"] power_mult)
+ apply (auto intro!: mult_left_mono)
+ done
finally show ?thesis .
qed
ultimately show ?thesis by auto
@@ -1210,9 +1212,10 @@
from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
OF \<open>0 \<le> real_of_float (x * x)\<close> f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
show "?lb" and "?ub" using \<open>0 \<le> real_of_float x\<close>
- unfolding power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric]
- unfolding mult.commute[where 'a=real] of_nat_fact
- by (auto intro!: mult_left_mono simp add: power_mult power2_eq_square[of "real_of_float x"])
+ apply (simp_all only: power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric])
+ apply (simp_all only: mult.commute[where 'a=real] of_nat_fact)
+ apply (auto intro!: mult_left_mono simp add: power_mult power2_eq_square[of "real_of_float x"])
+ done
qed
lemma sin_boundaries:
--- a/src/HOL/Deriv.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Deriv.thy Fri May 27 20:23:55 2016 +0200
@@ -857,7 +857,7 @@
lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow>
((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)"
using has_derivative_compose[of f "op * D" x s g "op * E"]
- unfolding has_field_derivative_def mult_commute_abs ac_simps .
+ by (simp only: has_field_derivative_def mult_commute_abs ac_simps)
corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
((\<lambda>x. f (g x)) has_field_derivative Da * Db) (at x within s)"
--- a/src/HOL/Inequalities.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Inequalities.thy Fri May 27 20:23:55 2016 +0200
@@ -58,8 +58,8 @@
proof -
let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
have "2 * (of_nat n * (\<Sum>j=0..<n. (a j * b j)) - (\<Sum>j=0..<n. b j) * (\<Sum>k=0..<n. a k)) = ?S"
- unfolding one_add_one[symmetric] algebra_simps
- by (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
+ by (simp only: one_add_one[symmetric] algebra_simps)
+ (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
also
{ fix i j::nat assume "i<n" "j<n"
hence "a i - a j \<le> 0 \<and> b i - b j \<ge> 0 \<or> a i - a j \<ge> 0 \<and> b i - b j \<le> 0"
--- a/src/HOL/Library/Complete_Partial_Order2.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Fri May 27 20:23:55 2016 +0200
@@ -308,7 +308,8 @@
fix x y
assume "x \<sqsubseteq> y"
show "?fixp x \<le> ?fixp y"
- unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain
+ apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
+ using chain
proof(rule ccpo_Sup_least)
fix x'
assume "x' \<in> (\<lambda>f. f x) ` ?iter"
@@ -599,7 +600,8 @@
fix x y
assume "x \<sqsubseteq> y"
show "?fixp x \<le> ?fixp y"
- unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain
+ apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
+ using chain
proof(rule ccpo_Sup_least)
fix x'
assume "x' \<in> (\<lambda>f. f x) ` ?iter"
--- a/src/HOL/MicroJava/DFA/Err.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy Fri May 27 20:23:55 2016 +0200
@@ -132,7 +132,7 @@
assumes semilat: "semilat (A, r, f)"
shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
apply(insert semilat)
- apply (unfold semilat_Def closed_def plussub_def lesub_def
+ apply (simp only: semilat_Def closed_def plussub_def lesub_def
lift2_def Err.le_def err_def)
apply (simp split: err.split)
done
--- a/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Fri May 27 20:23:55 2016 +0200
@@ -97,7 +97,7 @@
"order r \<Longrightarrow> app_mono r app n A \<Longrightarrow> bounded (err_step n app step) n \<Longrightarrow>
\<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> step p s \<le>|r| step p t \<Longrightarrow>
mono (Err.le r) (err_step n app step) n (err A)"
-apply (unfold app_mono_def mono_def err_step_def)
+apply (simp only: app_mono_def mono_def err_step_def)
apply clarify
apply (case_tac s)
apply simp
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri May 27 20:23:55 2016 +0200
@@ -3315,7 +3315,7 @@
then show "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
apply (rule_tac x=s in exI)
using hull_subset[of s convex]
- using convex_convex_hull[unfolded convex_explicit, of s,
+ using convex_convex_hull[simplified convex_explicit, of s,
THEN spec[where x=s], THEN spec[where x=u]]
apply auto
done
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri May 27 20:23:55 2016 +0200
@@ -1487,8 +1487,7 @@
by (auto simp add: algebra_simps)
also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
using e0(2)[rule_format, OF *]
- unfolding algebra_simps **
- by auto
+ by (simp only: algebra_simps **) auto
also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
using as(1)[unfolded mem_cball dist_norm]
by auto
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Fri May 27 20:23:55 2016 +0200
@@ -991,7 +991,8 @@
have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
"\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)"
by simp_all
- from fd[rule_format, of "axis i 1" "axis j 1", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul]
+ from fd[rule_format, of "axis i 1" "axis j 1",
+ simplified matrix_works[OF lf, symmetric] dot_matrix_vector_mul]
have "?A$i$j = ?m1 $ i $ j"
by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def
th0 setsum.delta[OF fU] mat_def axis_def)
@@ -1006,8 +1007,8 @@
{
assume lf: "linear f" and om: "orthogonal_matrix ?mf"
from lf om have ?lhs
- unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
- unfolding matrix_works[OF lf, symmetric]
+ apply (simp only: orthogonal_matrix_def norm_eq orthogonal_transformation)
+ apply (simp only: matrix_works[OF lf, symmetric])
apply (subst dot_matrix_vector_mul)
apply (simp add: dot_matrix_product matrix_mul_lid)
done
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri May 27 20:23:55 2016 +0200
@@ -2559,8 +2559,7 @@
"(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow>
((\<lambda>x. f x - g x) has_integral (k - l)) s"
using has_integral_add[OF _ has_integral_neg, of f k s g l]
- unfolding algebra_simps
- by auto
+ by (auto simp: algebra_simps)
lemma integral_0 [simp]:
"integral s (\<lambda>x::'n::euclidean_space. 0::'m::real_normed_vector) = 0"
@@ -6703,9 +6702,10 @@
using inj(1) unfolding inj_on_def by fastforce
have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _")
using assms(7)
- unfolding algebra_simps add_left_cancel scaleR_right.setsum
- by (subst setsum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
- (auto intro!: * setsum.cong simp: bij_betw_def dest!: p(4))
+ apply (simp only: algebra_simps add_left_cancel scaleR_right.setsum)
+ apply (subst setsum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
+ apply (auto intro!: * setsum.cong simp: bij_betw_def dest!: p(4))
+ done
also have "\<dots> = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r")
unfolding scaleR_diff_right scaleR_scaleR
using assms(1)
@@ -7759,7 +7759,7 @@
assume as: "c \<le> t" "t < c + ?d"
have *: "integral {a .. c} f = integral {a .. b} f - integral {c .. b} f"
"integral {a .. t} f = integral {a .. b} f - integral {t .. b} f"
- unfolding algebra_simps
+ apply (simp_all only: algebra_simps)
apply (rule_tac[!] integral_combine)
using assms as
apply auto
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri May 27 20:23:55 2016 +0200
@@ -1398,11 +1398,11 @@
inner_scaleR_left inner_scaleR_right
lemma dot_norm: "x \<bullet> y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
- unfolding power2_norm_eq_inner inner_simps inner_commute by auto
+ by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
lemma dot_norm_neg: "x \<bullet> y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
- unfolding power2_norm_eq_inner inner_simps inner_commute
- by (auto simp add: algebra_simps)
+ by (simp only: power2_norm_eq_inner inner_simps inner_commute)
+ (auto simp add: algebra_simps)
text\<open>Equality of vectors in terms of @{term "op \<bullet>"} products.\<close>
@@ -2434,7 +2434,7 @@
apply simp unfolding inner_simps
apply (clarsimp simp add: inner_add inner_setsum_left)
apply (rule setsum.neutral, rule ballI)
- unfolding inner_commute
+ apply (simp only: inner_commute)
apply (auto simp add: x field_simps
intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
done
--- a/src/HOL/Multivariate_Analysis/Polytope.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Polytope.thy Fri May 27 20:23:55 2016 +0200
@@ -1859,7 +1859,7 @@
with faceq [OF that] show ?thesis by simp
qed
moreover have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> affine hull S"
- apply (rule affine_affine_hull [unfolded affine_alt, rule_format])
+ apply (rule affine_affine_hull [simplified affine_alt, rule_format])
apply (simp add: \<open>w \<in> affine hull S\<close>)
using yaff apply blast
done
@@ -1874,7 +1874,7 @@
have yeq: "y = (1 - inverse T) *\<^sub>R w + c /\<^sub>R T"
using \<open>0 < T\<close> by (simp add: c_def algebra_simps)
show "y \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
- by (metis yeq affine_affine_hull [unfolded affine_alt, rule_format, OF waff caff])
+ by (metis yeq affine_affine_hull [simplified affine_alt, rule_format, OF waff caff])
qed
qed
ultimately show ?thesis
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri May 27 20:23:55 2016 +0200
@@ -921,7 +921,7 @@
qed
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
- unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
+ by (simp add: open_dist subset_eq mem_ball Ball_def dist_commute)
lemma openI [intro?]: "(\<And>x. x\<in>S \<Longrightarrow> \<exists>e>0. ball x e \<subseteq> S) \<Longrightarrow> open S"
by (auto simp: open_contains_ball)
@@ -5611,8 +5611,7 @@
using N[THEN spec[where x=n]]
using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]]
using x and y
- unfolding dist_commute
- by simp
+ by (simp add: dist_commute)
}
then have "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"
by auto
@@ -5854,8 +5853,8 @@
have *: "\<forall>x. x \<in> s \<and> f x \<in> t \<longleftrightarrow> x \<in> s \<and> f x \<in> (t \<inter> f ` s)"
by auto
have "closedin (subtopology euclidean (f ` s)) (t \<inter> f ` s)"
- using closedin_closed_Int[of t "f ` s", OF assms(2)] unfolding Int_commute
- by auto
+ using closedin_closed_Int[of t "f ` s", OF assms(2)]
+ by (simp add: Int_commute)
then show ?thesis
using assms(1)[unfolded continuous_on_closed, THEN spec[where x="t \<inter> f ` s"]]
using * by auto
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri May 27 20:23:55 2016 +0200
@@ -1761,8 +1761,8 @@
(fn {context = ctxt, prems = _} =>
mk_rel_map0_tac ctxt live (Lazy.force rel_OO) (Lazy.force rel_conversep)
(Lazy.force rel_Grp) (Lazy.force map_id)))
- |> map (unfold_thms lthy @{thms vimage2p_def[of id, unfolded id_apply]
- vimage2p_def[of _ id, unfolded id_apply]})
+ |> map (unfold_thms lthy @{thms vimage2p_def[of id, simplified id_apply]
+ vimage2p_def[of _ id, simplified id_apply]})
|> map Thm.close_derivation
end;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri May 27 20:23:55 2016 +0200
@@ -66,9 +66,9 @@
open BNF_FP_Util
val case_sum_transfer = @{thm case_sum_transfer};
-val case_sum_transfer_eq = @{thm case_sum_transfer[of "op =" _ "op =", unfolded sum.rel_eq]};
+val case_sum_transfer_eq = @{thm case_sum_transfer[of "op =" _ "op =", simplified sum.rel_eq]};
val case_prod_transfer = @{thm case_prod_transfer};
-val case_prod_transfer_eq = @{thm case_prod_transfer[of "op =" "op =", unfolded prod.rel_eq]};
+val case_prod_transfer_eq = @{thm case_prod_transfer[of "op =" "op =", simplified prod.rel_eq]};
val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
@@ -244,11 +244,11 @@
val Inl_Inr_Pair_tac = REPEAT_DETERM o (resolve_tac ctxt
[mk_rel_funDN 1 @{thm Inl_transfer},
- mk_rel_funDN 1 @{thm Inl_transfer[of "op =" "op =", unfolded sum.rel_eq]},
+ mk_rel_funDN 1 @{thm Inl_transfer[of "op =" "op =", simplified sum.rel_eq]},
mk_rel_funDN 1 @{thm Inr_transfer},
- mk_rel_funDN 1 @{thm Inr_transfer[of "op =" "op =", unfolded sum.rel_eq]},
+ mk_rel_funDN 1 @{thm Inr_transfer[of "op =" "op =", simplified sum.rel_eq]},
mk_rel_funDN 2 @{thm Pair_transfer},
- mk_rel_funDN 2 @{thm Pair_transfer[of "op =" "op =", unfolded prod.rel_eq]}]);
+ mk_rel_funDN 2 @{thm Pair_transfer[of "op =" "op =", simplified prod.rel_eq]}]);
fun mk_unfold_If_tac total pos =
HEADGOAL (Inl_Inr_Pair_tac THEN'
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Fri May 27 20:23:55 2016 +0200
@@ -50,7 +50,7 @@
val transfer_rules =
@{thm Abs_transfer[OF type_definition_id_bnf_UNIV type_definition_id_bnf_UNIV]} ::
map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions @
- map (Local_Defs.unfold ctxt rel_pre_defs) dtor_corec_transfers;
+ map (Local_Defs.unfold0 ctxt rel_pre_defs) dtor_corec_transfers;
val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add;
val ctxt' = Context.proof_map (fold add_transfer_rule transfer_rules) ctxt;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML Fri May 27 20:23:55 2016 +0200
@@ -381,7 +381,7 @@
unfold_thms_tac ctxt (map_ids @ @{thms Grp_def rel_fun_def}) THEN
HEADGOAL (REPEAT_DETERM_N m o rtac ctxt ext THEN'
asm_full_simp_tac (ss_only_silent @{thms simp_thms id_apply o_apply mem_Collect_eq
- top_greatest UNIV_I subset_UNIV[unfolded UNIV_def]} ctxt)) THEN
+ top_greatest UNIV_I subset_UNIV[simplified UNIV_def]} ctxt)) THEN
ALLGOALS (REPEAT_DETERM o etac ctxt @{thm meta_allE} THEN' REPEAT_DETERM o etac ctxt allE THEN'
forward_tac ctxt [sym] THEN' assume_tac ctxt)
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri May 27 20:23:55 2016 +0200
@@ -99,13 +99,13 @@
open BNF_FP_Util
open BNF_GFP_Util
-val fst_convol_fun_cong_sym = @{thm fst_convol[unfolded convol_def]} RS fun_cong RS sym;
+val fst_convol_fun_cong_sym = @{thm fst_convol[simplified convol_def]} RS fun_cong RS sym;
val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};
val nat_induct = @{thm nat_induct};
val o_apply_trans_sym = o_apply RS trans RS sym;
val ord_eq_le_trans = @{thm ord_eq_le_trans};
val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
-val snd_convol_fun_cong_sym = @{thm snd_convol[unfolded convol_def]} RS fun_cong RS sym;
+val snd_convol_fun_cong_sym = @{thm snd_convol[simplified convol_def]} RS fun_cong RS sym;
val sum_case_cong_weak = @{thm sum.case_cong_weak};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
val Collect_splitD_set_mp = @{thm Collect_case_prodD[OF set_mp]};
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri May 27 20:23:55 2016 +0200
@@ -102,8 +102,8 @@
set_selssss = [[[@{thms set_sum_sel(1)}], [[]]], [[[]], [@{thms set_sum_sel(2)}]]],
set_introssss = [[[@{thms setl.intros[OF refl]}], [[]]],
[[[]], [@{thms setr.intros[OF refl]}]]],
- set_cases = @{thms setl.cases[unfolded hypsubst_in_prems]
- setr.cases[unfolded hypsubst_in_prems]}},
+ set_cases = @{thms setl.cases[simplified hypsubst_in_prems]
+ setr.cases[simplified hypsubst_in_prems]}},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
common_co_inducts = @{thms sum.induct},
@@ -172,10 +172,10 @@
pred_injects = @{thms pred_prod_inject},
set_thms = @{thms prod_set_simps},
set_selssss = [[[@{thms fsts.intros}, []]], [[[], @{thms snds.intros}]]],
- set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, unfolded fst_conv]}, []]],
- [[[], @{thms snds.intros[of "(a, b)" for a b, unfolded snd_conv]}]]],
- set_cases = @{thms fsts.cases[unfolded eq_fst_iff ex_neg_all_pos]
- snds.cases[unfolded eq_snd_iff ex_neg_all_pos]}},
+ set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, simplified fst_conv]}, []]],
+ [[[], @{thms snds.intros[of "(a, b)" for a b, simplified snd_conv]}]]],
+ set_cases = @{thms fsts.cases[simplified eq_fst_iff ex_neg_all_pos]
+ snds.cases[simplified eq_snd_iff ex_neg_all_pos]}},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
common_co_inducts = @{thms prod.induct},
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri May 27 20:23:55 2016 +0200
@@ -81,7 +81,7 @@
can (Logic.dest_equals o Thm.prop_of) overloaded_size_def ? cons overloaded_size_def)
(Data.get (Context.Proof ctxt)) [];
-val size_gen_o_map_simps = @{thms inj_on_id snd_comp_apfst[unfolded apfst_def]};
+val size_gen_o_map_simps = @{thms inj_on_id snd_comp_apfst[simplified apfst_def]};
fun mk_size_gen_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
unfold_thms_tac ctxt [size_def] THEN
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Fri May 27 20:23:55 2016 +0200
@@ -48,7 +48,7 @@
tac, REPEAT_DETERM_N (n - k) o etac ctxt thin_rl]);
fun unfold_thms_tac _ [] = all_tac
- | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
+ | unfold_thms_tac ctxt thms = Local_Defs.unfold0_tac ctxt (distinct Thm.eq_thm_prop thms);
fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri May 27 20:23:55 2016 +0200
@@ -214,7 +214,7 @@
let val thy = Proof_Context.theory_of ctxt
in Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty) end;
-fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
+fun unfold_thms ctxt thms = Local_Defs.unfold0 ctxt (distinct Thm.eq_thm_prop thms);
fun name_noted_thms _ _ [] = []
| name_noted_thms qualifier base ((local_name, thms) :: noted) =
--- a/src/HOL/Tools/Function/mutual.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Fri May 27 20:23:55 2016 +0200
@@ -186,7 +186,7 @@
Goal.prove simp_ctxt [] []
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
(fn _ =>
- Local_Defs.unfold_tac ctxt all_orig_fdefs
+ Local_Defs.unfold0_tac ctxt all_orig_fdefs
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
THEN (simp_tac ctxt) 1)
|> restore_cond
--- a/src/HOL/Tools/Function/partial_function.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Fri May 27 20:23:55 2016 +0200
@@ -68,7 +68,7 @@
(*rewrite conclusion with k-th assumtion*)
fun rewrite_with_asm_tac ctxt k =
Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
- Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;
+ Local_Defs.unfold0_tac ctxt' [nth prems k]) ctxt;
fun dest_case ctxt t =
case strip_comb t of
@@ -107,7 +107,7 @@
(*monotonicity proof: apply rules + split case expressions*)
fun mono_tac ctxt =
- K (Local_Defs.unfold_tac ctxt [@{thm curry_def}])
+ K (Local_Defs.unfold0_tac ctxt [@{thm curry_def}])
THEN' (TRY o REPEAT_ALL_NEW
(resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems partial_function_mono}))
ORELSE' split_cases_tac ctxt));
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 27 20:23:55 2016 +0200
@@ -119,11 +119,11 @@
resolve_tac ctxt @{thms subsetI} 1
THEN eresolve_tac ctxt @{thms CollectE} 1
THEN REPEAT (eresolve_tac ctxt @{thms exE} 1)
- THEN Local_Defs.unfold_tac ctxt @{thms inv_image_def}
+ THEN Local_Defs.unfold0_tac ctxt @{thms inv_image_def}
THEN resolve_tac ctxt @{thms CollectI} 1
THEN eresolve_tac ctxt @{thms conjE} 1
THEN eresolve_tac ctxt @{thms ssubst} 1
- THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.case}
+ THEN Local_Defs.unfold0_tac ctxt @{thms split_conv triv_forall_equality sum.case}
(* Sets *)
@@ -249,7 +249,7 @@
THEN mset_pwleq_tac ctxt 1
THEN EVERY (map2 (less_proof false) qs ps)
THEN (if strict orelse qs <> lq
- then Local_Defs.unfold_tac ctxt set_of_simps
+ then Local_Defs.unfold0_tac ctxt set_of_simps
THEN steps_tac MAX true
(subtract (op =) qs lq) (subtract (op =) ps lp)
else all_tac)
@@ -280,7 +280,7 @@
THEN (resolve_tac ctxt [order_rpair ms_rp label] 1)
THEN PRIMITIVE (Thm.instantiate' [] [SOME level_mapping])
THEN unfold_tac ctxt @{thms rp_inv_image_def}
- THEN Local_Defs.unfold_tac ctxt @{thms split_conv fst_conv snd_conv}
+ THEN Local_Defs.unfold0_tac ctxt @{thms split_conv fst_conv snd_conv}
THEN REPEAT (SOMEGOAL (resolve_tac ctxt [@{thm Un_least}, @{thm empty_subsetI}]))
THEN EVERY (map (prove_lev true) sl)
THEN EVERY (map (prove_lev false) (subtract (op =) sl (0 upto length cs - 1))))
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Fri May 27 20:23:55 2016 +0200
@@ -25,16 +25,16 @@
val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
val inst = map dest_Var vars ~~ map (Thm.cterm_of ctxt) UNIVs
val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst)
- |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
+ |> Local_Defs.unfold0 ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
|> (fn thm => thm RS sym)
val rel_mono = rel_mono_of_bnf bnf
val rel_conversep_sym = rel_conversep_of_bnf bnf RS sym
in
- EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Quotient_alt_def5}]),
- REPEAT_DETERM o (etac ctxt conjE), rtac ctxt conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_Grp_UNIV_sym]),
- rtac ctxt rel_mono THEN_ALL_NEW assume_tac ctxt, rtac ctxt conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt
+ EVERY' [SELECT_GOAL (Local_Defs.unfold0_tac ctxt [@{thm Quotient_alt_def5}]),
+ REPEAT_DETERM o (etac ctxt conjE), rtac ctxt conjI, SELECT_GOAL (Local_Defs.unfold0_tac ctxt [rel_Grp_UNIV_sym]),
+ rtac ctxt rel_mono THEN_ALL_NEW assume_tac ctxt, rtac ctxt conjI, SELECT_GOAL (Local_Defs.unfold0_tac ctxt
[rel_conversep_sym, rel_Grp_UNIV_sym]), rtac ctxt rel_mono THEN_ALL_NEW assume_tac ctxt,
- SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]),
+ SELECT_GOAL (Local_Defs.unfold0_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]),
hyp_subst_tac ctxt, rtac ctxt refl] i
end
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri May 27 20:23:55 2016 +0200
@@ -325,7 +325,7 @@
@{thm map_fun_def[abs_def]} |>
unabs_def @{context} |>
unabs_def @{context} |>
- Local_Defs.unfold @{context} [@{thm comp_def}]
+ Local_Defs.unfold0 @{context} [@{thm comp_def}]
fun unfold_fun_maps ctm =
let
@@ -360,7 +360,7 @@
exception CODE_CERT_GEN of string
fun simplify_code_eq ctxt def_thm =
- Local_Defs.unfold ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm
+ Local_Defs.unfold0 ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm
(*
quot_thm - quotient theorem (Quotient R Abs Rep T).
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri May 27 20:23:55 2016 +0200
@@ -296,7 +296,7 @@
val f_alt_def_goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (f_alt_def_goal_lhs, f_alt_def_goal_rhs));
fun f_alt_def_tac ctxt i =
EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o Transfer.transfer_tac true ctxt,
- SELECT_GOAL (Local_Defs.unfold_tac ctxt [id_apply]), rtac ctxt refl] i;
+ SELECT_GOAL (Local_Defs.unfold0_tac ctxt [id_apply]), rtac ctxt refl] i;
val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data
val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
[([rep_isom_transfer], [Transfer.transfer_add])])] lthy
@@ -320,7 +320,7 @@
let
(* logical definition of qty qty_isom isomorphism *)
val uTname = unique_Tname (rty, qty)
- fun eq_onp_to_top_tac ctxt = SELECT_GOAL (Local_Defs.unfold_tac ctxt
+ fun eq_onp_to_top_tac ctxt = SELECT_GOAL (Local_Defs.unfold0_tac ctxt
(@{thm eq_onp_top_eq_eq[symmetric]} :: Lifting_Info.get_relator_eq_onp_rules ctxt))
fun lift_isom_tac ctxt = HEADGOAL (eq_onp_to_top_tac ctxt
THEN' (rtac ctxt @{thm id_transfer}));
@@ -437,9 +437,9 @@
val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |>
HOLogic.mk_Trueprop;
fun typ_isom_tac ctxt i =
- EVERY' [ SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms type_definition_def}),
+ EVERY' [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms type_definition_def}),
DETERM o Transfer.transfer_tac true ctxt,
- SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms eq_onp_top_eq_eq}) (* normalize *),
+ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms eq_onp_top_eq_eq}) (* normalize *),
Raw_Simplifier.rewrite_goal_tac ctxt
(map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
rtac ctxt TrueI] i;
@@ -564,7 +564,7 @@
fun non_empty_typedef_tac non_empty_pred ctxt i =
(Method.insert_tac ctxt [non_empty_pred] THEN'
- SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i
+ SELECT_GOAL (Local_Defs.unfold0_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i
val uTname = unique_Tname (rty, qty)
val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
val ((_, tcode_dt), lthy) = conceal_naming_result (typedef (Binding.concealed uTname, TFrees, NoSyn)
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri May 27 20:23:55 2016 +0200
@@ -334,7 +334,7 @@
val rules = Transfer.get_transfer_raw ctxt'
val rules = constraint :: OO_rules @ rules
val tac =
- K (Local_Defs.unfold_tac ctxt' [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac ctxt' rules)
+ K (Local_Defs.unfold0_tac ctxt' [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac ctxt' rules)
in
(singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
end
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri May 27 20:23:55 2016 +0200
@@ -192,7 +192,7 @@
| _ =>
let
val thaa'bb' as [(tha', _), (thb', _)] =
- map (`(Local_Defs.unfold ctxt meta_not_not)) [tha, thb]
+ map (`(Local_Defs.unfold0 ctxt meta_not_not)) [tha, thb]
in
if forall Thm.eq_thm_prop thaa'bb' then
raise THM ("resolve_inc_tyvars: unique result expected", i, [tha, thb])
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri May 27 20:23:55 2016 +0200
@@ -592,7 +592,7 @@
fun prepare_split_thm ctxt split_thm =
(split_thm RS @{thm iffD2})
- |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
+ |> Local_Defs.unfold0 ctxt [@{thm atomize_conjL[symmetric]},
@{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
fun find_split_thm thy (Const (name, _)) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri May 27 20:23:55 2016 +0200
@@ -152,7 +152,7 @@
val th'' =
Goal.prove ctxt (Term.add_free_names t' []) [] t'
(fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))
- val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
+ val th''' = Local_Defs.unfold0 ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
in
th'''
end;
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Fri May 27 20:23:55 2016 +0200
@@ -616,7 +616,7 @@
fun arith_th_lemma_tac ctxt prems =
Method.insert_tac ctxt prems
- THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms z3div_def z3mod_def})
+ THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms z3div_def z3mod_def})
THEN' Arith_Data.arith_tac ctxt
fun arith_th_lemma ctxt thms t =
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri May 27 20:23:55 2016 +0200
@@ -60,12 +60,12 @@
val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf,
rel_OO_of_bnf bnf]
in
- SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac ctxt (rel_mono_of_bnf bnf)
+ SELECT_GOAL (Local_Defs.unfold0_tac ctxt thms) THEN' rtac ctxt (rel_mono_of_bnf bnf)
THEN_ALL_NEW assume_tac ctxt
end
fun bi_constraint_tac constr_iff sided_constr_intros ctxt =
- SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
+ SELECT_GOAL (Local_Defs.unfold0_tac ctxt [constr_iff]) THEN'
CONJ_WRAP' (fn thm => rtac ctxt thm THEN_ALL_NEW
(REPEAT_DETERM o etac ctxt conjE THEN' assume_tac ctxt)) sided_constr_intros
@@ -153,7 +153,7 @@
val n = live_of_bnf bnf
val set_map's = set_map_of_bnf bnf
in
- EVERY' [rtac ctxt ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
+ EVERY' [rtac ctxt ext, SELECT_GOAL (Local_Defs.unfold0_tac ctxt [@{thm Domainp.simps},
in_rel_of_bnf bnf, pred_def]), rtac ctxt iffI,
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt,
CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt ballI, dtac ctxt (set_map RS equalityD1 RS set_mp),
--- a/src/HOL/Tools/reification.ML Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/reification.ML Fri May 27 20:23:55 2016 +0200
@@ -82,7 +82,7 @@
(Goal.prove ctxt'' [] (map mk_def env)
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
(fn {context, prems, ...} =>
- Local_Defs.unfold_tac context (map tryext prems) THEN resolve_tac ctxt'' [th'] 1)) RS sym;
+ Local_Defs.unfold0_tac context (map tryext prems) THEN resolve_tac ctxt'' [th'] 1)) RS sym;
val (cong' :: vars') =
Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o Thm.cterm_of ctxt'') vs);
val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';
--- a/src/HOL/Topological_Spaces.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy Fri May 27 20:23:55 2016 +0200
@@ -75,22 +75,22 @@
using closed_Union [of "B ` A"] by simp
lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
- unfolding closed_def by simp
+ by (simp add: closed_def)
lemma closed_open: "closed S \<longleftrightarrow> open (- S)"
- unfolding closed_def by simp
+ by (rule closed_def)
lemma open_Diff [continuous_intros, intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
- unfolding closed_open Diff_eq by (rule open_Int)
+ by (simp add: closed_open Diff_eq open_Int)
lemma closed_Diff [continuous_intros, intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"
- unfolding open_closed Diff_eq by (rule closed_Int)
+ by (simp add: open_closed Diff_eq closed_Int)
lemma open_Compl [continuous_intros, intro]: "closed S \<Longrightarrow> open (- S)"
- unfolding closed_open .
+ by (simp add: closed_open)
lemma closed_Compl [continuous_intros, intro]: "open S \<Longrightarrow> closed (- S)"
- unfolding open_closed .
+ by (simp add: open_closed)
lemma open_Collect_neg: "closed {x. P x} \<Longrightarrow> open {x. \<not> P x}"
unfolding Collect_neg_eq by (rule open_Compl)
--- a/src/HOL/Transcendental.thy Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Transcendental.thy Fri May 27 20:23:55 2016 +0200
@@ -1080,7 +1080,7 @@
unfolding real_norm_def abs_mult
using le mult_right_mono by fastforce
qed (rule powser_insidea[OF converges[OF \<open>R' \<in> {-R <..< R}\<close>] \<open>norm x < norm R'\<close>])
- from this[THEN summable_mult2[where c=x], unfolded mult.assoc, unfolded mult.commute]
+ from this[THEN summable_mult2[where c=x], simplified mult.assoc, simplified mult.commute]
show "summable (?f x)" by auto
}
show "summable (?f' x0)"
@@ -3241,12 +3241,13 @@
shows "\<lbrakk>summable f;
\<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
\<Longrightarrow> setsum f {..<k} < suminf f"
-unfolding One_nat_def
+apply (simp only: One_nat_def)
apply (subst suminf_split_initial_segment [where k=k], assumption, simp)
apply (drule_tac k=k in summable_ignore_initial_segment)
apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
apply simp
-by (metis (no_types, lifting) add.commute suminf_pos summable_def sums_unique)
+apply (metis (no_types, lifting) add.commute suminf_pos summable_def sums_unique)
+done
lemma cos_two_less_zero [simp]:
"cos 2 < (0::real)"
@@ -5128,7 +5129,7 @@
next
fix x :: real
assume "(\<lambda> n. if even n then f (n div 2) else 0) sums x"
- from LIMSEQ_linear[OF this[unfolded sums_def] pos2, unfolded sum_split_even_odd[unfolded mult.commute]]
+ from LIMSEQ_linear[OF this[simplified sums_def] pos2, simplified sum_split_even_odd[simplified mult.commute]]
show "f sums x" unfolding sums_def by auto
qed
hence "op sums f = op sums (\<lambda> n. if even n then f (n div 2) else 0)" ..