diff -r 23dcee1e91ac -r 7bd794d7c86b src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Sat Jun 13 22:58:38 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Sun Jun 14 12:48:32 2015 +0100 @@ -639,7 +639,7 @@ lemma gauge_ball[intro]: "0 < e \ gauge (\x. ball x e)" unfolding gauge_def by auto -lemma gauge_trivial[intro]: "gauge (\x. ball x 1)" +lemma gauge_trivial[intro!]: "gauge (\x. ball x 1)" by (rule gauge_ball) auto lemma gauge_inter[intro]: "gauge d1 \ gauge d2 \ gauge (\x. d1 x \ d2 x)" @@ -4048,72 +4048,33 @@ qed qed - lemma iterate_image_nonzero: assumes "monoidal opp" - and "finite s" - and "\x\s. \y\s. x \ y \ f x = f y \ g (f x) = neutral opp" - shows "iterate opp (f ` s) g = iterate opp s (g \ f)" - using assms -proof (induct rule: finite_subset_induct[OF assms(2) subset_refl]) - case goal1 - show ?case - using assms(1) by auto -next - case goal2 - have *: "\x y. y = neutral opp \ x = opp y x" - using assms(1) by auto - show ?case - unfolding image_insert - apply (subst iterate_insert[OF assms(1)]) - apply (rule finite_imageI goal2)+ - apply (cases "f a \ f ` F") - unfolding if_P if_not_P - apply (subst goal2(4)[OF assms(1) goal2(1)]) - defer - apply (subst iterate_insert[OF assms(1) goal2(1)]) - defer - apply (subst iterate_insert[OF assms(1) goal2(1)]) - unfolding if_not_P[OF goal2(3)] - defer unfolding image_iff - defer - apply (erule bexE) - apply (rule *) - unfolding o_def - apply (rule_tac y=x in goal2(7)[rule_format]) - using goal2 - unfolding o_def - apply auto - done -qed + and "finite s" + and "\x y. \x\s. \y\s. x \ y \ f x = f y \ g (f x) = neutral opp" + shows "iterate opp (f ` s) g = iterate opp s (g \ f)" +using assms +by (induct rule: finite_subset_induct[OF assms(2) subset_refl]) auto lemma operative_tagged_division: assumes "monoidal opp" - and "operative opp f" - and "d tagged_division_of (cbox a b)" - shows "iterate opp d (\(x,l). f l) = f (cbox a b)" + and "operative opp f" + and "d tagged_division_of (cbox a b)" + shows "iterate opp d (\(x,l). f l) = f (cbox a b)" proof - have *: "(\(x,l). f l) = f \ snd" - unfolding o_def by rule auto note assm = tagged_division_ofD[OF assms(3)] - have "iterate opp d (\(x,l). f l) = iterate opp (snd ` d) f" + unfolding o_def by rule auto note tagged = tagged_division_ofD[OF assms(3)] + { fix a b a' + assume as: "(a, b) \ d" "(a', b) \ d" "(a, b) \ (a', b)" + have "f b = neutral opp" + using tagged(4)[OF as(1)] + apply clarify + apply (rule operativeD(1)[OF assms(2)]) + by (metis content_eq_0_interior inf.idem tagged_division_ofD(5)[OF assms(3) as(1-3)]) + } + then have "iterate opp d (\(x,l). f l) = iterate opp (snd ` d) f" unfolding * - apply (rule iterate_image_nonzero[symmetric,OF assms(1)]) - apply (rule tagged_division_of_finite assms)+ - unfolding Ball_def split_paired_All snd_conv - apply (rule, rule, rule, rule, rule, rule, rule, erule conjE) - proof - - fix a b aa ba - assume as: "(a, b) \ d" "(aa, ba) \ d" "(a, b) \ (aa, ba)" "b = ba" - guess u v using assm(4)[OF as(1)] by (elim exE) note uv=this - show "f b = neutral opp" - unfolding uv - apply (rule operativeD(1)[OF assms(2)]) - unfolding content_eq_0_interior - using tagged_division_ofD(5)[OF assms(3) as(1-3)] - unfolding as(4)[symmetric] uv - apply auto - done - qed + by (force intro!: assms iterate_image_nonzero[symmetric, OF _ tagged_division_of_finite]) also have "\ = f (cbox a b)" using operative_division[OF assms(1-2) division_of_tagged_division[OF assms(3)]] . finally show ?thesis . @@ -4126,68 +4087,45 @@ assumes "finite s" shows "setsum f s = iterate op + s f" proof - - have *: "setsum f s = setsum f (support op + f s)" - apply (rule setsum.mono_neutral_right) - unfolding support_def neutral_add + have "setsum f s = setsum f (support op + f s)" using assms - apply auto - done - then show ?thesis unfolding * iterate_def fold'_def setsum.eq_fold - unfolding neutral_add by (simp add: comp_def) + by (auto simp: support_def intro: setsum.mono_neutral_right) + then show ?thesis unfolding iterate_def fold'_def setsum.eq_fold + by (simp add: comp_def) qed lemma additive_content_division: - assumes "d division_of (cbox a b)" - shows "setsum content d = content (cbox a b)" - unfolding operative_division[OF monoidal_monoid operative_content assms,symmetric] - apply (subst setsum_iterate) - using assms - apply auto - done + "d division_of (cbox a b) \ setsum content d = content (cbox a b)" + by (metis division_ofD(1) monoidal_monoid operative_content operative_division setsum_iterate) lemma additive_content_tagged_division: - assumes "d tagged_division_of (cbox a b)" - shows "setsum (\(x,l). content l) d = content (cbox a b)" + "d tagged_division_of (cbox a b) \ setsum (\(x,l). content l) d = content (cbox a b)" unfolding operative_tagged_division[OF monoidal_monoid operative_content assms,symmetric] - apply (subst setsum_iterate) - using assms - apply auto - done + using setsum_iterate by blast subsection \Finally, the integral of a constant\ -lemma has_integral_const[intro]: +lemma has_integral_const [intro]: fixes a b :: "'a::euclidean_space" shows "((\x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)" - unfolding has_integral - apply rule - apply rule - apply (rule_tac x="\x. ball x 1" in exI) - apply rule - apply (rule gauge_trivial) - apply rule - apply rule - apply (erule conjE) - unfolding split_def + apply (auto intro!: exI [where x="\x. ball x 1"] simp: split_def has_integral) apply (subst scaleR_left.setsum[symmetric, unfolded o_def]) - defer apply (subst additive_content_tagged_division[unfolded split_def]) - apply assumption apply auto done -lemma has_integral_const_real[intro]: +lemma has_integral_const_real [intro]: fixes a b :: real shows "((\x. c) has_integral (content {a .. b} *\<^sub>R c)) {a .. b}" by (metis box_real(2) has_integral_const) -lemma integral_const[simp]: +lemma integral_const [simp]: fixes a b :: "'a::euclidean_space" shows "integral (cbox a b) (\x. c) = content (cbox a b) *\<^sub>R c" by (rule integral_unique) (rule has_integral_const) -lemma integral_const_real[simp]: +lemma integral_const_real [simp]: fixes a b :: real shows "integral {a .. b} (\x. c) = content {a .. b} *\<^sub>R c" by (metis box_real(2) integral_const) @@ -4355,7 +4293,7 @@ proof - fix a b assume ab: "(a, b) \ p" - note assm = tagged_division_ofD(2-4)[OF assms(1) ab] + note tagged = tagged_division_ofD(2-4)[OF assms(1) ab] from this(3) guess u v by (elim exE) note b=this show "(content b *\<^sub>R f a) \ i \ (content b *\<^sub>R g a) \ i" unfolding b @@ -4363,7 +4301,7 @@ apply (rule mult_left_mono) defer apply (rule content_pos_le,rule assms(2)[rule_format]) - using assm + using tagged apply auto done qed