# HG changeset patch # User paulson # Date 1504129890 -3600 # Node ID 8f12f7e0d99702bb7e65a773206aaeb9c528df13 # Parent 116f658195af7ab7f8aedd1f21b7d8bee66c53af eliminated some goal_cases diff -r 116f658195af -r 8f12f7e0d997 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Aug 30 21:46:41 2017 +0100 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Aug 30 22:51:30 2017 +0100 @@ -5166,61 +5166,54 @@ lemma has_integral_combine_division: fixes f :: "'n::euclidean_space \ 'a::banach" - assumes "d division_of S" - and "\k. k \ d \ (f has_integral (i k)) k" - shows "(f has_integral (sum i d)) S" + assumes "\ division_of S" + and "\k. k \ \ \ (f has_integral (i k)) k" + shows "(f has_integral (sum i \)) S" proof - - note d = division_ofD[OF assms(1)] - have neg: "negligible (S \ s')" if "S \ d" "s' \ d" "S \ s'" for S s' + note \ = division_ofD[OF assms(1)] + have neg: "negligible (S \ s')" if "S \ \" "s' \ \" "S \ s'" for S s' proof - - obtain a c b d where obt: "S = cbox a b" "s' = cbox c d" - by (meson \S \ d\ \s' \ d\ d(4)) - from d(5)[OF that] show ?thesis + obtain a c b \ where obt: "S = cbox a b" "s' = cbox c \" + by (meson \S \ \\ \s' \ \\ \(4)) + from \(5)[OF that] show ?thesis unfolding obt interior_cbox by (metis (no_types, lifting) Diff_empty Int_interval box_Int_box negligible_frontier_interval) qed show ?thesis - unfolding d(6)[symmetric] - by (auto intro: d neg assms has_integral_Union) + unfolding \(6)[symmetric] + by (auto intro: \ neg assms has_integral_Union) qed lemma integral_combine_division_bottomup: fixes f :: "'n::euclidean_space \ 'a::banach" - assumes "d division_of S" - and "\k. k \ d \ f integrable_on k" - shows "integral S f = sum (\i. integral i f) d" + assumes "\ division_of S" "\k. k \ \ \ f integrable_on k" + shows "integral S f = sum (\i. integral i f) \" apply (rule integral_unique) - apply (rule has_integral_combine_division[OF assms(1)]) - using assms(2) - unfolding has_integral_integral - apply assumption - done + by (meson assms has_integral_combine_division has_integral_integrable_integral) lemma has_integral_combine_division_topdown: fixes f :: "'n::euclidean_space \ 'a::banach" - assumes "f integrable_on S" - and "d division_of k" - and "k \ S" - shows "(f has_integral (sum (\i. integral i f) d)) k" - apply (rule has_integral_combine_division[OF assms(2)]) - unfolding has_integral_integral[symmetric] -proof goal_cases - case (1 k) - from division_ofD(2,4)[OF assms(2) this] - show ?case - apply safe - apply (rule integrable_on_subcbox) - apply (rule assms) - using assms(3) - apply auto - done + assumes f: "f integrable_on S" + and \: "\ division_of K" + and "K \ S" + shows "(f has_integral (sum (\i. integral i f) \)) K" +proof - + have "f integrable_on L" if "L \ \" for L + proof - + have "L \ S" + using \K \ S\ \ that by blast + then show "f integrable_on L" + using that by (metis (no_types) f \ division_ofD(4) integrable_on_subcbox) + qed + then show ?thesis + by (meson \ has_integral_combine_division has_integral_integrable_integral) qed lemma integral_combine_division_topdown: fixes f :: "'n::euclidean_space \ 'a::banach" assumes "f integrable_on S" - and "d division_of S" - shows "integral S f = sum (\i. integral i f) d" + and "\ division_of S" + shows "integral S f = sum (\i. integral i f) \" apply (rule integral_unique) apply (rule has_integral_combine_division_topdown) using assms @@ -5229,30 +5222,27 @@ lemma integrable_combine_division: fixes f :: "'n::euclidean_space \ 'a::banach" - assumes "d division_of S" - and "\i\d. f integrable_on i" + assumes \: "\ division_of S" + and f: "\i. i \ \ \ f integrable_on i" shows "f integrable_on S" - using assms(2) - unfolding integrable_on_def - by (metis has_integral_combine_division[OF assms(1)]) + using f unfolding integrable_on_def by (metis has_integral_combine_division[OF \]) lemma integrable_on_subdivision: fixes f :: "'n::euclidean_space \ 'a::banach" - assumes "d division_of i" - and "f integrable_on S" + assumes \: "\ division_of i" + and f: "f integrable_on S" and "i \ S" shows "f integrable_on i" - apply (rule integrable_combine_division assms)+ - apply safe -proof goal_cases - case 1 - note division_ofD(2,4)[OF assms(1) this] - then show ?case - apply safe - apply (rule integrable_on_subcbox[OF assms(2)]) - using assms(3) - apply auto - done +proof - + have "f integrable_on i" if "i \ \" for i +proof - + have "i \ S" + using assms that by auto + then show "f integrable_on i" + using that by (metis (no_types) \ f division_ofD(4) integrable_on_subcbox) +qed + then show ?thesis + using \ integrable_combine_division by blast qed @@ -5293,16 +5283,14 @@ lemma has_integral_combine_tagged_division_topdown: fixes f :: "'n::euclidean_space \ 'a::banach" - assumes "f integrable_on cbox a b" - and "p tagged_division_of (cbox a b)" - shows "(f has_integral (sum (\(x,k). integral k f) p)) (cbox a b)" - apply (rule has_integral_combine_tagged_division[OF assms(2)]) - apply safe -proof goal_cases - case 1 - note tagged_division_ofD(3-4)[OF assms(2) this] - then show ?case - using integrable_subinterval[OF assms(1)] by blast + assumes f: "f integrable_on cbox a b" + and p: "p tagged_division_of (cbox a b)" + shows "(f has_integral (sum (\(x,K). integral K f) p)) (cbox a b)" +proof - + have "(f has_integral integral K f) K" if "(x,K) \ p" for x K + by (metis assms integrable_integral integrable_on_subcbox tagged_division_ofD(3,4) that) + then show ?thesis + by (metis assms case_prodI2 has_integral_integrable_integral integral_combine_tagged_division_bottomup) qed lemma integral_combine_tagged_division_topdown: @@ -5310,10 +5298,8 @@ assumes "f integrable_on cbox a b" and "p tagged_division_of (cbox a b)" shows "integral (cbox a b) f = sum (\(x,k). integral k f) p" - apply (rule integral_unique) - apply (rule has_integral_combine_tagged_division_topdown) - using assms - apply auto + apply (rule integral_unique [OF has_integral_combine_tagged_division_topdown]) + using assms apply auto done