--- a/src/HOL/Analysis/Determinants.thy Mon Apr 09 15:20:11 2018 +0100
+++ b/src/HOL/Analysis/Determinants.thy Mon Apr 09 17:20:58 2018 +0100
@@ -197,7 +197,7 @@
by (simp add: det_diagonal mat_def)
lemma det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
- by (simp add: det_def prod_zero)
+ by (simp add: det_def prod_zero power_0_left)
lemma det_permute_rows:
fixes A :: "'a::comm_ring_1^'n^'n"
@@ -815,20 +815,16 @@
apply (simp only: ab_left_minus add.assoc[symmetric])
apply simp
done
- from c ci
have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
- unfolding sum.remove[OF fU iU] sum_cmul
- apply -
apply (rule vector_mul_lcancel_imp[OF ci])
- apply (auto simp add: field_simps)
- unfolding *
- apply rule
+ using c ci unfolding sum.remove[OF fU iU] sum_cmul
+ apply (auto simp add: field_simps *)
done
have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
unfolding thr0
apply (rule span_sum)
apply simp
- apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
+ apply (rule span_mul [where 'a="real^'n"])
apply (rule span_superset)
apply auto
done
@@ -869,7 +865,7 @@
have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A"
apply (rule det_row_span)
apply (rule span_sum)
- apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
+ apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])
apply (rule span_superset)
apply auto
done
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Apr 09 15:20:11 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Apr 09 17:20:58 2018 +0100
@@ -1289,7 +1289,8 @@
have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
by (rule prod_constant [symmetric])
also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
- using prj1_idem [OF \<open>X \<in> \<D>\<close>] by (auto simp: algebra_simps intro: prod.cong)
+ apply (rule prod.cong [OF refl])
+ by (simp add: \<open>X \<in> \<D>\<close> inner_diff_left prj1_idem)
finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Apr 09 15:20:11 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Apr 09 17:20:58 2018 +0100
@@ -660,12 +660,18 @@
lemma integrable_cmul: "f integrable_on S \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on S"
unfolding integrable_on_def by(auto intro: has_integral_cmul)
-lemma integrable_on_cmult_iff:
+lemma integrable_on_scaleR_iff [simp]:
+ fixes c :: real
+ assumes "c \<noteq> 0"
+ shows "(\<lambda>x. c *\<^sub>R f x) integrable_on S \<longleftrightarrow> f integrable_on S"
+ using integrable_cmul[of "\<lambda>x. c *\<^sub>R f x" S "1 / c"] integrable_cmul[of f S c] \<open>c \<noteq> 0\<close>
+ by auto
+
+lemma integrable_on_cmult_iff [simp]:
fixes c :: real
assumes "c \<noteq> 0"
shows "(\<lambda>x. c * f x) integrable_on S \<longleftrightarrow> f integrable_on S"
- using integrable_cmul[of "\<lambda>x. c * f x" S "1 / c"] integrable_cmul[of f S c] \<open>c \<noteq> 0\<close>
- by auto
+ using integrable_on_scaleR_iff [of c f] assms by simp
lemma integrable_on_cmult_left:
assumes "f integrable_on S"
@@ -676,6 +682,9 @@
lemma integrable_neg: "f integrable_on S \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on S"
unfolding integrable_on_def by(auto intro: has_integral_neg)
+lemma integrable_neg_iff: "(\<lambda>x. -f(x)) integrable_on S \<longleftrightarrow> f integrable_on S"
+ using integrable_neg by fastforce
+
lemma integrable_diff:
"f integrable_on S \<Longrightarrow> g integrable_on S \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on S"
unfolding integrable_on_def by(auto intro: has_integral_diff)
@@ -2295,20 +2304,20 @@
using assms negligible_subset by force
lemma negligible_Un:
- assumes "negligible s"
- and "negligible t"
- shows "negligible (s \<union> t)"
- unfolding negligible_def
-proof (safe, goal_cases)
- case (1 a b)
- note assms[unfolded negligible_def,rule_format,of a b]
- then show ?case
- apply (subst has_integral_spike_eq[OF assms(2)])
- defer
- apply assumption
- unfolding indicator_def
- apply auto
- done
+ assumes "negligible S" and T: "negligible T"
+ shows "negligible (S \<union> T)"
+proof -
+ have "(indicat_real (S \<union> T) has_integral 0) (cbox a b)"
+ if S0: "(indicat_real S has_integral 0) (cbox a b)"
+ and "(indicat_real T has_integral 0) (cbox a b)" for a b
+ proof (subst has_integral_spike_eq[OF T])
+ show "indicat_real S x = indicat_real (S \<union> T) x" if "x \<in> cbox a b - T" for x
+ by (metis Diff_iff Un_iff indicator_def that)
+ show "(indicat_real S has_integral 0) (cbox a b)"
+ by (simp add: S0)
+ qed
+ with assms show ?thesis
+ unfolding negligible_def by blast
qed
lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
@@ -3430,7 +3439,7 @@
by (simp add: inner_simps field_simps)
ultimately show ?thesis using False
by (simp add: image_affinity_cbox content_cbox'
- prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left)
+ prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left del: prod_constant)
qed
qed
@@ -5235,19 +5244,21 @@
lemma has_integral_Un:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes f: "(f has_integral i) s" "(f has_integral j) t"
- and neg: "negligible (s \<inter> t)"
- shows "(f has_integral (i + j)) (s \<union> t)"
-proof -
- note * = has_integral_restrict_UNIV[symmetric, of f]
- show ?thesis
- unfolding *
- apply (rule has_integral_spike[OF assms(3)])
- defer
- apply (rule has_integral_add[OF f[unfolded *]])
- apply auto
- done
-qed
+ assumes f: "(f has_integral i) S" "(f has_integral j) T"
+ and neg: "negligible (S \<inter> T)"
+ shows "(f has_integral (i + j)) (S \<union> T)"
+ unfolding has_integral_restrict_UNIV[symmetric, of f]
+proof (rule has_integral_spike[OF neg])
+ let ?f = "\<lambda>x. (if x \<in> S then f x else 0) + (if x \<in> T then f x else 0)"
+ show "(?f has_integral i + j) UNIV"
+ by (simp add: f has_integral_add)
+qed auto
+
+lemma integral_Un [simp]:
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
+ assumes "f integrable_on S" "f integrable_on T" "negligible (S \<inter> T)"
+ shows "integral (S \<union> T) f = integral S f + integral T f"
+ using has_integral_Un by (simp add: has_integral_Un assms integrable_integral integral_unique)
lemma integrable_Un:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Mon Apr 09 15:20:11 2018 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Mon Apr 09 17:20:58 2018 +0100
@@ -3434,10 +3434,12 @@
then show ?thesis by simp
next
case (Suc m)
- have th0: "a^n = prod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = prod (\<lambda>k. a oo c) {0..m}"
+ have "(\<Prod>n = 0..m. a) oo c = (\<Prod>n = 0..m. a oo c)"
+ using c0 fps_compose_prod_distrib by blast
+ moreover have th0: "a^n = prod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = prod (\<lambda>k. a oo c) {0..m}"
by (simp_all add: prod_constant Suc)
- then show ?thesis
- by (simp add: fps_compose_prod_distrib[OF c0])
+ ultimately show ?thesis
+ by presburger
qed
lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"