# HG changeset patch # User wenzelm # Date 1469817247 -7200 # Node ID e5abbdee461a28c8ebffbbe0c8e0da9643f52e94 # Parent 3e3097ac37d1e601bc25dd1674586402a4b6df39 more accurate cong del; tuned proofs; diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Bali/Conform.thy --- a/src/HOL/Bali/Conform.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Bali/Conform.thy Fri Jul 29 20:34:07 2016 +0200 @@ -519,9 +519,9 @@ apply safe apply (rule lconf_upd) apply auto -apply (simp only: obj_ty_cong) +apply (simp only: obj_ty_cong) apply (force dest: conforms_globsD intro!: lconf_upd - simp add: oconf_def cong del: sum.case_cong_weak) + simp add: oconf_def cong del: old.sum.case_cong_weak) done lemma conforms_set_locals: diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Matrix_LP/Matrix.thy --- a/src/HOL/Matrix_LP/Matrix.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Matrix_LP/Matrix.thy Fri Jul 29 20:34:07 2016 +0200 @@ -514,11 +514,12 @@ foldseq f (\k. if k < m then s k else foldseq f (\k. s (k + m)) (Suc na - m)) m" apply (simp add: subd) apply (cases "m = 0") - apply (simp) + apply simp apply (drule sube) - apply (auto) + apply auto apply (rule a) - by (simp add: subc cong del: if_cong) + apply (simp add: subc cong del: if_weak_cong) + done qed then show ?thesis using assms by simp qed diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jul 29 20:34:07 2016 +0200 @@ -11551,7 +11551,8 @@ done moreover have "(\x\(s \ t). f x *\<^sub>R x) = 0" apply (simp add: f_def setsum_Un scaleR_left_diff_distrib setsum_subtractf) - apply (simp add: if_smult setsum.inter_restrict [symmetric] Int_commute eq cong del: if_cong) + apply (simp add: if_smult setsum.inter_restrict [symmetric] Int_commute eq + cong del: if_weak_cong) done ultimately have "\v. v \ s \ t \ f v = 0" using aff_independent_finite assms unfolding affine_dependent_explicit diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Number_Theory/Gauss.thy --- a/src/HOL/Number_Theory/Gauss.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Number_Theory/Gauss.thy Fri Jul 29 20:34:07 2016 +0200 @@ -329,7 +329,7 @@ "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)" proof - have "[setprod id A = setprod id F * setprod id D](mod p)" - by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong) + by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: setprod.strong_cong) then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)" apply (rule cong_trans_int) apply (metis cong_scalar_int prod_F_zcong) @@ -365,7 +365,7 @@ done then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)" apply (rule cong_trans_int) - apply (simp add: aux cong del:setprod.cong) + apply (simp add: aux cong del: setprod.strong_cong) done with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)" by (metis cong_mult_lcancel_int) diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Old_Number_Theory/Gauss.thy --- a/src/HOL/Old_Number_Theory/Gauss.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Old_Number_Theory/Gauss.thy Fri Jul 29 20:34:07 2016 +0200 @@ -443,27 +443,26 @@ "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)" proof - have "[setprod id A = setprod id F * setprod id D](mod p)" - by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong) + by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: setprod.strong_cong) then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)" - apply (rule zcong_trans) - apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod.cong) - done + by (rule zcong_trans) (auto simp add: prod_F_zcong zcong_scalar cong del: setprod.strong_cong) then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)" apply (rule zcong_trans) apply (insert C_prod_eq_D_times_E, erule subst) - apply (subst mult.assoc, auto) + apply (subst mult.assoc) + apply auto done then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)" apply (rule zcong_trans) - apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod.cong) + apply (simp add: C_B_zcong_prod zcong_scalar2 cong del: setprod.strong_cong) done then have "[setprod id A = ((-1)^(card E) * (setprod id ((%x. x * a) ` A)))] (mod p)" by (simp add: B_def) then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))] (mod p)" - by (simp add:finite_A inj_on_xa_A setprod.reindex cong del:setprod.cong) + by (simp add:finite_A inj_on_xa_A setprod.reindex cong del: setprod.strong_cong) moreover have "setprod (%x. x * a) A = setprod (%x. a) A * setprod id A" using finite_A by (induct set: finite) auto @@ -472,22 +471,16 @@ by simp then have "[setprod id A = ((-1)^(card E) * a^(card A) * setprod id A)](mod p)" - apply (rule zcong_trans) - apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult.assoc) - done + by (rule zcong_trans) (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult.assoc) then have a: "[setprod id A * (-1)^(card E) = ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)" by (rule zcong_scalar) then have "[setprod id A * (-1)^(card E) = setprod id A * (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)" - apply (rule zcong_trans) - apply (simp add: a mult.commute mult.left_commute) - done + by (rule zcong_trans) (simp add: a mult.commute mult.left_commute) then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)" - apply (rule zcong_trans) - apply (simp add: aux cong del:setprod.cong) - done + by (rule zcong_trans) (simp add: aux cong del: setprod.strong_cong) with this zcong_cancel2 [of p "setprod id A" "(- 1) ^ card E" "a ^ card A"] p_g_0 A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)" by (simp add: order_less_imp_le) diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Probability/Bochner_Integration.thy Fri Jul 29 20:34:07 2016 +0200 @@ -953,7 +953,7 @@ lemma integral_cong: "M = N \ (\x. x \ space N \ f x = g x) \ integral\<^sup>L M f = integral\<^sup>L N g" - 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_weak_cong add: lebesgue_integral_def) lemma integral_cong_AE: "f \ borel_measurable M \ g \ borel_measurable M \ AE x in M. f x = g x \ diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Probability/Borel_Space.thy Fri Jul 29 20:34:07 2016 +0200 @@ -414,7 +414,7 @@ shows "f \ borel_measurable (restrict_space M \) \ (\x. f x * indicator \ x) \ borel_measurable M" by (subst measurable_restrict_space_iff) - (auto simp: indicator_def if_distrib[where f="\x. a * x" for a] cong del: if_cong) + (auto simp: indicator_def if_distrib[where f="\x. a * x" for a] cong del: if_weak_cong) lemma borel_measurable_restrict_space_iff_ennreal: fixes f :: "'a \ ennreal" @@ -422,7 +422,7 @@ shows "f \ borel_measurable (restrict_space M \) \ (\x. f x * indicator \ x) \ borel_measurable M" by (subst measurable_restrict_space_iff) - (auto simp: indicator_def if_distrib[where f="\x. a * x" for a] cong del: if_cong) + (auto simp: indicator_def if_distrib[where f="\x. a * x" for a] cong del: if_weak_cong) lemma borel_measurable_restrict_space_iff: fixes f :: "'a \ 'b::real_normed_vector" @@ -430,7 +430,8 @@ shows "f \ borel_measurable (restrict_space M \) \ (\x. indicator \ x *\<^sub>R f x) \ borel_measurable M" by (subst measurable_restrict_space_iff) - (auto simp: indicator_def if_distrib[where f="\x. x *\<^sub>R a" for a] ac_simps cong del: if_cong) + (auto simp: indicator_def if_distrib[where f="\x. x *\<^sub>R a" for a] ac_simps + cong del: if_weak_cong) lemma cbox_borel[measurable]: "cbox a b \ sets borel" by (auto intro: borel_closed) diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Probability/Information.thy Fri Jul 29 20:34:07 2016 +0200 @@ -1913,7 +1913,7 @@ also have "\ = entropy b (count_space (Y ` space M) \\<^sub>M count_space (X ` space M)) (\x. (Y x, X x))" by (subst entropy_distr[OF simple_distributed_joint[OF YX]]) (auto simp: pair_measure_count_space sigma_finite_measure_count_space_finite lebesgue_integral_count_space_finite - cong del: setsum.cong intro!: setsum.mono_neutral_left measure_nonneg) + cong del: setsum.strong_cong intro!: setsum.mono_neutral_left measure_nonneg) finally have "\(\x. (X x, Y x)) = entropy b (count_space (Y ` space M) \\<^sub>M count_space (X ` space M)) (\x. (Y x, X x))" . then show ?thesis unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri Jul 29 20:34:07 2016 +0200 @@ -1177,7 +1177,7 @@ intro: has_field_derivative_subset[OF f(1)] \a \ b\) then have i: "((\x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV" unfolding indicator_def if_distrib[where f="\x. a * x" for a] - by (simp cong del: if_cong del: atLeastAtMost_iff) + by (simp cong del: if_weak_cong del: atLeastAtMost_iff) then have nn: "(\\<^sup>+x. f x * indicator {a .. b} x \lborel) = F b - F a" by (rule nn_integral_has_integral_lborel[OF *]) then show ?has @@ -1207,7 +1207,7 @@ have "(f has_integral integral\<^sup>L lborel ?f) {a..b}" using has_integral_integral_lborel[OF int] unfolding indicator_def if_distrib[where f="\x. x *\<^sub>R a" for a] - by (simp cong del: if_cong del: atLeastAtMost_iff) + by (simp cong del: if_weak_cong del: atLeastAtMost_iff) ultimately show ?eq by (auto dest: has_integral_unique) then show ?has diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri Jul 29 20:34:07 2016 +0200 @@ -1510,7 +1510,7 @@ show "\x. g x \ (\s. integral\<^sup>N (M s) (f top))" by (subst step) (auto simp add: top_fun_def less_le non_zero le_fun_def ennreal_top_mult - cong del: if_cong intro!: monoD[OF inf_continuous_mono[OF g], THEN le_funD]) + cong del: if_weak_cong intro!: monoD[OF inf_continuous_mono[OF g], THEN le_funD]) next fix C assume "\i::nat. C i \ borel_measurable N \ (\s. integral\<^sup>N (M s) (C i) < \)" "decseq C" with bound show "INFIMUM UNIV C \ borel_measurable N \ (\s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \)" diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Probability/SPMF.thy --- a/src/HOL/Probability/SPMF.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Probability/SPMF.thy Fri Jul 29 20:34:07 2016 +0200 @@ -2433,13 +2433,14 @@ unfolding bind_spmf_const[symmetric] apply(simp add: pair_spmf_def map_bind_pmf pair_pmf_def bind_assoc_pmf option.case_distrib) apply(subst bind_commute_pmf) -apply(auto intro!: bind_pmf_cong[OF refl] simp add: bind_return_pmf bind_spmf_def bind_return_pmf' case_option_collapse option.case_distrib[where h="map_spmf _"] option.case_distrib[symmetric] case_option_id split: option.split cong del: option.case_cong) +apply(auto intro!: bind_pmf_cong[OF refl] simp add: bind_return_pmf bind_spmf_def bind_return_pmf' case_option_collapse option.case_distrib[where h="map_spmf _"] option.case_distrib[symmetric] case_option_id split: option.split cong del: option.case_cong_weak) done lemma map_snd_pair_spmf [simp]: "map_spmf snd (pair_spmf p q) = scale_spmf (weight_spmf p) q" unfolding bind_spmf_const[symmetric] -apply(simp add: pair_spmf_def map_bind_pmf pair_pmf_def bind_assoc_pmf option.case_distrib cong del: option.case_cong) -apply(auto intro!: bind_pmf_cong[OF refl] simp add: bind_return_pmf bind_spmf_def bind_return_pmf' case_option_collapse option.case_distrib[where h="map_spmf _"] option.case_distrib[symmetric] case_option_id split: option.split cong del: option.case_cong) + apply(simp add: pair_spmf_def map_bind_pmf pair_pmf_def bind_assoc_pmf option.case_distrib + cong del: option.case_cong_weak) +apply(auto intro!: bind_pmf_cong[OF refl] simp add: bind_return_pmf bind_spmf_def bind_return_pmf' case_option_collapse option.case_distrib[where h="map_spmf _"] option.case_distrib[symmetric] case_option_id split: option.split cong del: option.case_cong_weak) done lemma set_pair_spmf [simp]: "set_spmf (pair_spmf p q) = set_spmf p \ set_spmf q" diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Product_Type.thy Fri Jul 29 20:34:07 2016 +0200 @@ -264,7 +264,7 @@ setup \Sign.parent_path\ declare prod.case [nitpick_simp del] -declare prod.case_cong_weak [cong del] +declare old.prod.case_cong_weak [cong del] declare prod.case_eq_if [mono] declare prod.split [no_atp] declare prod.split_asm [no_atp] diff -r 3e3097ac37d1 -r e5abbdee461a src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Fri Jul 29 08:22:59 2016 +0200 +++ b/src/HOL/Transcendental.thy Fri Jul 29 20:34:07 2016 +0200 @@ -261,7 +261,7 @@ from this[unfolded sums_def, THEN LIMSEQ_Suc] have "(\n. if even n then f (n div 2) else 0) sums y" by (simp add: lessThan_Suc_eq_insert_0 setsum_atLeast1_atMost_eq image_Suc_lessThan - if_eq sums_def cong del: if_cong) + if_eq sums_def cong del: if_weak_cong) from sums_add[OF g_sums this] show ?thesis by (simp only: if_sum) qed