--- 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:
--- 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 (\<lambda>k. if k < m then s k else foldseq f (\<lambda>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
--- 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 "(\<Sum>x\<in>(s \<union> 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 "\<And>v. v \<in> s \<union> t \<Longrightarrow> f v = 0"
using aff_independent_finite assms unfolding affine_dependent_explicit
--- 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)
--- 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)
--- 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 \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> 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 \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
--- 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 \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
(\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
by (subst measurable_restrict_space_iff)
- (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_cong)
+ (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
lemma borel_measurable_restrict_space_iff_ennreal:
fixes f :: "'a \<Rightarrow> ennreal"
@@ -422,7 +422,7 @@
shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
(\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
by (subst measurable_restrict_space_iff)
- (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_cong)
+ (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
lemma borel_measurable_restrict_space_iff:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
@@ -430,7 +430,8 @@
shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
(\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
by (subst measurable_restrict_space_iff)
- (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps cong del: if_cong)
+ (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps
+ cong del: if_weak_cong)
lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
by (auto intro: borel_closed)
--- 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 "\<dots> = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>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 "\<H>(\<lambda>x. (X x, Y x)) = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))" .
then show ?thesis
unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp
--- 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)] \<open>a \<le> b\<close>)
then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
unfolding indicator_def if_distrib[where f="\<lambda>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: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>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="\<lambda>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
--- 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 "\<And>x. g x \<le> (\<lambda>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 "\<And>i::nat. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)" "decseq C"
with bound show "INFIMUM UNIV C \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \<infinity>)"
--- 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 \<times> set_spmf q"
--- 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 \<open>Sign.parent_path\<close>
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]
--- 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 "(\<lambda>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