# HG changeset patch # User wenzelm # Date 1464373435 -7200 # Node ID eae6549dbea291a8cec6746896fcda46d03ff0de # Parent d36c7dc40000e7711f91f9f3e01eb099eb3f3ed6 tuned proofs, to allow unfold_abs_def; diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy --- 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 "\ 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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Decision_Procs/Approximation.thy --- 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) \ ?S n" using bounds(1) \0 \ sqrt y\ - 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 "\ \ arctan (sqrt y)" using arctan_bounds .. finally show ?thesis . qed @@ -526,9 +527,10 @@ have "arctan (sqrt y) \ ?S (Suc n)" using arctan_bounds .. also have "\ \ (sqrt y * ub_arctan_horner prec (Suc n) 1 y)" using bounds(2)[of "Suc n"] \0 \ sqrt y\ - 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 \0 \ real_of_float (x * x)\ f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps] show "?lb" and "?ub" using \0 \ real_of_float x\ - 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: diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Deriv.thy --- 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) \ DERIV g (f x) :> E \ ((\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 \ (g has_field_derivative Db) (at x within s) \ ((\x. f (g x)) has_field_derivative Da * Db) (at x within s)" diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Inequalities.thy --- 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 = "(\j=0..k=0..j=0..j=0..k=0..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 "\i j. a i * b j"] setsum_right_distrib) also { fix i j::nat assume "i 0 \ b i - b j \ 0 \ a i - a j \ 0 \ b i - b j \ 0" diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Library/Complete_Partial_Order2.thy --- 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 \ y" show "?fixp x \ ?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' \ (\f. f x) ` ?iter" @@ -599,7 +600,8 @@ fix x y assume "x \ y" show "?fixp x \ ?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' \ (\f. f x) ` ?iter" diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/MicroJava/DFA/Err.thy --- 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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/MicroJava/DFA/Typing_Framework_err.thy --- 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 \ app_mono r app n A \ bounded (err_step n app step) n \ \s p t. s \ A \ p < n \ s <=_r t \ app p t \ step p s \|r| step p t \ 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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 "\s. finite s \ s \ p \ card s \ DIM('a) + 1 \ x \ 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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Multivariate_Analysis/Derivative.thy --- 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 "\ \ 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 "\ \ 1 / (B * 2) * norm (g' (z - f x)) + e/2" using as(1)[unfolded mem_cball dist_norm] by auto diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Multivariate_Analysis/Determinants.thy --- 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: "\b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" "\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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Multivariate_Analysis/Integration.thy --- 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 \ (g has_integral l) s \ ((\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 (\x::'n::euclidean_space. 0::'m::real_normed_vector) = 0" @@ -6703,9 +6702,10 @@ using inj(1) unfolding inj_on_def by fastforce have "(\(x, k)\(\(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\(x, k)\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="\(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="\(x, k). (g x, g ` k)" and S=p]) + apply (auto intro!: * setsum.cong simp: bij_betw_def dest!: p(4)) + done also have "\ = r *\<^sub>R ((\(x, k)\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 \ 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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- 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 \ 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 \ 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\Equality of vectors in terms of @{term "op \"} products.\ @@ -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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Multivariate_Analysis/Polytope.thy --- 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 \ 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: \w \ affine hull S\) using yaff apply blast done @@ -1874,7 +1874,7 @@ have yeq: "y = (1 - inverse T) *\<^sub>R w + c /\<^sub>R T" using \0 < T\ by (simp add: c_def algebra_simps) show "y \ affine hull (S \ {y. a h \ 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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 \ (\x\S. \e>0. ball x e \ 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?]: "(\x. x\S \ \e>0. ball x e \ S) \ 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 "\N. \n\N. dist (f (x n)) (f (y n)) < e" by auto @@ -5854,8 +5853,8 @@ have *: "\x. x \ s \ f x \ t \ x \ s \ f x \ (t \ f ` s)" by auto have "closedin (subtopology euclidean (f ` s)) (t \ 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 \ f ` s"]] using * by auto diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/BNF/bnf_def.ML --- 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; diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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' diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML --- 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; diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML --- 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; diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- 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]}; diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- 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}, diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML --- 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}); diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- 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) = diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Function/mutual.ML --- 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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Function/partial_function.ML --- 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)); diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Function/scnp_reconstruct.ML --- 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)))) diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Lifting/lifting_bnf.ML --- 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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Lifting/lifting_def.ML --- 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). diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- 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) diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Lifting/lifting_setup.ML --- 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 diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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]) diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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, _)) = diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- 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; diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/SMT/z3_replay_methods.ML --- 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 = diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Transfer/transfer_bnf.ML --- 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), diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/reification.ML --- 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'; diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Topological_Spaces.thy --- 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 \ closed (- S)" - unfolding closed_def by simp + by (simp add: closed_def) lemma closed_open: "closed S \ open (- S)" - unfolding closed_def by simp + by (rule closed_def) lemma open_Diff [continuous_intros, intro]: "open S \ closed T \ 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 \ open T \ 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 \ open (- S)" - unfolding closed_open . + by (simp add: closed_open) lemma closed_Compl [continuous_intros, intro]: "open S \ closed (- S)" - unfolding open_closed . + by (simp add: open_closed) lemma open_Collect_neg: "closed {x. P x} \ open {x. \ P x}" unfolding Collect_neg_eq by (rule open_Compl) diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Transcendental.thy --- 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 \R' \ {-R <..< R}\] \norm x < norm R'\]) - 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 "\summable f; \d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\ \ setsum f {.. 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 (\ n. if even n then f (n div 2) else 0)" ..