# HG changeset patch # User paulson # Date 1523290858 -3600 # Node ID 8c012a49293a4c47c2568ffdb19a1246b5c7c085 # Parent 83c8cafdebe875ce2c8e46093c28c0b631ca16ef A couple of new results diff -r 83c8cafdebe8 -r 8c012a49293a src/HOL/Analysis/Determinants.thy --- 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 (\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 \ span {row j A| j. j \ 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 (\ i. if i = k then row k A + (\i \ ?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 diff -r 83c8cafdebe8 -r 8c012a49293a src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- 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) = (\i::'M \ Basis. prj1 (vf X - uf X))" by (rule prod_constant [symmetric]) also have "\ = (\i\Basis. vf X \ i - uf X \ i)" - using prj1_idem [OF \X \ \\] by (auto simp: algebra_simps intro: prod.cong) + apply (rule prod.cong [OF refl]) + by (simp add: \X \ \\ inner_diff_left prj1_idem) finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\i\Basis. vf X \ i - uf X \ i)" . have "uf X \ cbox (uf X) (vf X)" "vf X \ cbox (uf X) (vf X)" using uvz [OF \X \ \\] by (force simp: mem_box)+ diff -r 83c8cafdebe8 -r 8c012a49293a src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- 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 \ (\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 \ 0" + shows "(\x. c *\<^sub>R f x) integrable_on S \ f integrable_on S" + using integrable_cmul[of "\x. c *\<^sub>R f x" S "1 / c"] integrable_cmul[of f S c] \c \ 0\ + by auto + +lemma integrable_on_cmult_iff [simp]: fixes c :: real assumes "c \ 0" shows "(\x. c * f x) integrable_on S \ f integrable_on S" - using integrable_cmul[of "\x. c * f x" S "1 / c"] integrable_cmul[of f S c] \c \ 0\ - 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 \ (\x. -f(x)) integrable_on S" unfolding integrable_on_def by(auto intro: has_integral_neg) +lemma integrable_neg_iff: "(\x. -f(x)) integrable_on S \ f integrable_on S" + using integrable_neg by fastforce + lemma integrable_diff: "f integrable_on S \ g integrable_on S \ (\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 \ 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 \ T)" +proof - + have "(indicat_real (S \ 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 \ T) x" if "x \ 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 \ t) \ negligible s \ 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 \ 'a::banach" - assumes f: "(f has_integral i) s" "(f has_integral j) t" - and neg: "negligible (s \ t)" - shows "(f has_integral (i + j)) (s \ 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 \ T)" + shows "(f has_integral (i + j)) (S \ T)" + unfolding has_integral_restrict_UNIV[symmetric, of f] +proof (rule has_integral_spike[OF neg]) + let ?f = "\x. (if x \ S then f x else 0) + (if x \ 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 \ 'a::banach" + assumes "f integrable_on S" "f integrable_on T" "negligible (S \ T)" + shows "integral (S \ 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 \ 'b :: banach" diff -r 83c8cafdebe8 -r 8c012a49293a src/HOL/Computational_Algebra/Formal_Power_Series.thy --- 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 (\k. a) {0..m}" "(a oo c) ^ n = prod (\k. a oo c) {0..m}" + have "(\n = 0..m. a) oo c = (\n = 0..m. a oo c)" + using c0 fps_compose_prod_distrib by blast + moreover have th0: "a^n = prod (\k. a) {0..m}" "(a oo c) ^ n = prod (\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)"