# HG changeset patch # User wenzelm # Date 1378892287 -7200 # Node ID 129bd52a5e5f01e4e9c5c5a6d81a24db9396426d # Parent 1905ebfec3738dc9040df64278eb90e242f08925# Parent 9b0af3298cda647647a22e8dd375d6ac5648add2 merged diff -r 1905ebfec373 -r 129bd52a5e5f Admin/components/components.sha1 --- a/Admin/components/components.sha1 Wed Sep 11 10:57:09 2013 +0200 +++ b/Admin/components/components.sha1 Wed Sep 11 11:38:07 2013 +0200 @@ -33,6 +33,7 @@ 06e9be2627ebb95c45a9bcfa025d2eeef086b408 jedit_build-20130104.tar.gz c85c0829b8170f25aa65ec6852f505ce2a50639b jedit_build-20130628.tar.gz 5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz +87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz 8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz 6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz 5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz diff -r 1905ebfec373 -r 129bd52a5e5f Admin/components/main --- a/Admin/components/main Wed Sep 11 10:57:09 2013 +0200 +++ b/Admin/components/main Wed Sep 11 11:38:07 2013 +0200 @@ -4,7 +4,7 @@ exec_process-1.0.3 Haskabelle-2013 jdk-7u25 -jedit_build-20130905 +jedit_build-20130910 jfreechart-1.0.14 kodkodi-1.5.2 polyml-5.5.0-3 diff -r 1905ebfec373 -r 129bd52a5e5f NEWS --- a/NEWS Wed Sep 11 10:57:09 2013 +0200 +++ b/NEWS Wed Sep 11 11:38:07 2013 +0200 @@ -247,8 +247,7 @@ * Locale hierarchy for abstract orderings and (semi)lattices. -* Discontinued theory src/HOL/Library/Eval_Witness. -INCOMPATIBILITY. +* Discontinued theory src/HOL/Library/Eval_Witness. INCOMPATIBILITY. * Discontinued obsolete src/HOL/IsaMakefile (considered legacy since Isabelle2013). Use "isabelle build" to operate on Isabelle sessions. @@ -265,9 +264,9 @@ Code_Target_Nat and Code_Target_Numeral. See the tutorial on code generation for details. INCOMPATIBILITY. -* Complete_Partial_Order.admissible is defined outside the type -class ccpo, but with mandatory prefix ccpo. Admissibility theorems -lose the class predicate assumption or sort constraint when possible. +* Complete_Partial_Order.admissible is defined outside the type class +ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the +class predicate assumption or sort constraint when possible. INCOMPATIBILITY. * Introduce type class "conditionally_complete_lattice": Like a diff -r 1905ebfec373 -r 129bd52a5e5f README --- a/README Wed Sep 11 10:57:09 2013 +0200 +++ b/README Wed Sep 11 11:38:07 2013 +0200 @@ -10,14 +10,12 @@ Installation Isabelle works on the three main platform families: Linux, Windows, - and Mac OS X. - - Completely integrated bundles including the full Isabelle sources, - documentation, add-on tools and precompiled logic images for - several platforms are available from the Isabelle web page. + and Mac OS X. The fully integrated application bundles from the + Isabelle web page include sources, documentation, and add-on tools + for all supported platforms. Some background information may be found in the Isabelle System - Manual, distributed with the sources (directory doc). + Manual (directory doc). User interfaces diff -r 1905ebfec373 -r 129bd52a5e5f lib/Tools/build_dialog --- a/lib/Tools/build_dialog Wed Sep 11 10:57:09 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,77 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Makarius -# -# DESCRIPTION: build Isabelle session images via GUI dialog - - -## diagnostics - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: isabelle $PRG [OPTIONS]" - echo - echo " Options are:" - echo " -L OPTION default logic via system option" - echo " -d DIR include session directory" - echo " -l NAME logic session name" - echo " -s system build mode: produce output in ISABELLE_HOME" - echo - echo " Build Isabelle logic session image via GUI dialog (default: $ISABELLE_LOGIC)." - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -## process command line - -LOGIC_OPTION="" -declare -a INCLUDE_DIRS=() -LOGIC="" -SYSTEM_MODE=false - -while getopts "L:d:l:s" OPT -do - case "$OPT" in - L) - LOGIC_OPTION="$OPTARG" - ;; - d) - INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG" - ;; - l) - LOGIC="$OPTARG" - ;; - s) - SYSTEM_MODE="true" - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - - -# args - -[ "$#" -ne 0 ] && usage - - -## main - -isabelle_admin_build jars || exit $? - -"$ISABELLE_TOOL" java isabelle.Build_Dialog \ - "$LOGIC_OPTION" "$LOGIC" "$SYSTEM_MODE" "${INCLUDE_DIRS[@]}" - diff -r 1905ebfec373 -r 129bd52a5e5f src/Doc/System/Interfaces.thy --- a/src/Doc/System/Interfaces.thy Wed Sep 11 10:57:09 2013 +0200 +++ b/src/Doc/System/Interfaces.thy Wed Sep 11 11:38:07 2013 +0200 @@ -32,10 +32,10 @@ directories may be included via option @{verbatim "-d"} to augment that name space (see also \secref{sec:tool-build}). - By default, the specified image is checked and built on demand, see - also @{tool build_dialog}. The @{verbatim "-s"} determines where to - store the result session image (see also \secref{sec:tool-build}). - The @{verbatim "-n"} option bypasses the session build dialog. + By default, the specified image is checked and built on demand. The + @{verbatim "-s"} option determines where to store the result session + image (see also \secref{sec:tool-build}). The @{verbatim "-n"} + option bypasses the session build dialog. The @{verbatim "-m"} option specifies additional print modes for the prover process. diff -r 1905ebfec373 -r 129bd52a5e5f src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Wed Sep 11 10:57:09 2013 +0200 +++ b/src/Doc/System/Sessions.thy Wed Sep 11 11:38:07 2013 +0200 @@ -419,31 +419,4 @@ \end{ttbox} *} - -section {* Build dialog *} - -text {* The @{tool_def build_dialog} provides a simple GUI wrapper to - the tool Isabelle @{tool build} tool. This enables user interfaces - like Isabelle/jEdit \secref{sec:tool-jedit} to provide read-made - logic image on startup. Its command-line usage is: -\begin{ttbox} -Usage: isabelle build_dialog [OPTIONS] LOGIC - - Options are: - -L OPTION default logic via system option - -d DIR include session directory - -l NAME logic session name - -s system build mode: produce output in ISABELLE_HOME - - Build Isabelle logic session image via GUI dialog (default: \$ISABELLE_LOGIC). -\end{ttbox} - - \medskip Option @{verbatim "-l"} specifies an explicit logic session - name. Option @{verbatim "-L"} specifies a system option name as - fall-back to determine the logic session name. If both are omitted - or have empty value, @{setting ISABELLE_LOGIC} is used as default. - - \medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same - meaning as for the command-line @{tool build} tool itself. *} - end diff -r 1905ebfec373 -r 129bd52a5e5f src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Sep 11 10:57:09 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Sep 11 11:38:07 2013 +0200 @@ -3324,12 +3324,13 @@ have *: "\(a::'a) b c. content ({a..b} \ {x. x\k \ c}) = 0 \ interior({a..b} \ {x. x\k \ c}) = {}" unfolding interval_split[OF k] content_eq_0_interior by auto - guess u1 v1 using d(4)[OF assms(2)] apply-by(erule exE)+ note uv1=this - guess u2 v2 using d(4)[OF assms(3)] apply-by(erule exE)+ note uv2=this + guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this + guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this have **: "\s t u. s \ t = {} \ u \ s \ u \ t \ u = {}" by auto show ?thesis - unfolding uv1 uv2 * apply(rule **[OF d(5)[OF assms(2-4)]]) + unfolding uv1 uv2 * + apply (rule **[OF d(5)[OF assms(2-4)]]) defer apply (subst assms(5)[unfolded uv1 uv2]) unfolding uv1 uv2 @@ -3686,7 +3687,7 @@ unfolding lem3[OF p(3)] apply (subst setsum_reindex_nonzero[OF p(3)]) defer - apply(subst setsum_reindex_nonzero[OF p(3)]) + apply (subst setsum_reindex_nonzero[OF p(3)]) defer unfolding lem4[symmetric] apply (rule refl) @@ -3903,7 +3904,7 @@ unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric] using p using assms - by (auto simp add:algebra_simps) + by (auto simp add: algebra_simps) qed qed qed @@ -3927,7 +3928,7 @@ opp (f ({a..b} \ {x. x\k \ c})) (f ({a..b} \ {x. x\k \ c}))" using assms unfolding operative_def by auto -lemma operative_trivial: "operative opp f \ content({a..b}) = 0 \ f({a..b}) = neutral opp" +lemma operative_trivial: "operative opp f \ content {a..b} = 0 \ f {a..b} = neutral opp" unfolding operative_def by auto lemma property_empty_interval: "\a b. content {a..b} = 0 \ P {a..b} \ P {}" @@ -5180,7 +5181,7 @@ by auto lemma has_integral_component_lbound: - fixes f :: "'a::ordered_euclidean_space => 'b::ordered_euclidean_space" + fixes f :: "'a::ordered_euclidean_space \ 'b::ordered_euclidean_space" assumes "(f has_integral i) {a..b}" and "\x\{a..b}. B \ f(x)\k" and "k \ Basis" @@ -6354,54 +6355,121 @@ using operative_division[OF monoidal_and assms] division_of_finite[OF assms(2)] by auto -lemma operative_approximable: assumes "0 \ e" fixes f::"'b::ordered_euclidean_space \ 'a::banach" - shows "operative op \ (\i. \g. (\x\i. norm (f x - g (x::'b)) \ e) \ g integrable_on i)" unfolding operative_def neutral_and +lemma operative_approximable: + fixes f::"'b::ordered_euclidean_space \ 'a::banach" + assumes "0 \ e" + shows "operative op \ (\i. \g. (\x\i. norm (f x - g (x::'b)) \ e) \ g integrable_on i)" + unfolding operative_def neutral_and proof safe - fix a b::"'b" - { assume "content {a..b} = 0" - thus "\g. (\x\{a..b}. norm (f x - g x) \ e) \ g integrable_on {a..b}" - apply(rule_tac x=f in exI) using assms by(auto intro!:integrable_on_null) } - { fix c g and k :: 'b - assume as:"\x\{a..b}. norm (f x - g x) \ e" "g integrable_on {a..b}" and k:"k\Basis" + fix a b :: 'b + { + assume "content {a..b} = 0" + then show "\g. (\x\{a..b}. norm (f x - g x) \ e) \ g integrable_on {a..b}" + apply (rule_tac x=f in exI) + using assms + apply (auto intro!:integrable_on_null) + done + } + { + fix c g + fix k :: 'b + assume as: "\x\{a..b}. norm (f x - g x) \ e" "g integrable_on {a..b}" + assume k: "k \ Basis" show "\g. (\x\{a..b} \ {x. x \ k \ c}. norm (f x - g x) \ e) \ g integrable_on {a..b} \ {x. x \ k \ c}" "\g. (\x\{a..b} \ {x. c \ x \ k}. norm (f x - g x) \ e) \ g integrable_on {a..b} \ {x. c \ x \ k}" - apply(rule_tac[!] x=g in exI) using as(1) integrable_split[OF as(2) k] by auto } - fix c k g1 g2 assume as:"\x\{a..b} \ {x. x \ k \ c}. norm (f x - g1 x) \ e" "g1 integrable_on {a..b} \ {x. x \ k \ c}" - "\x\{a..b} \ {x. c \ x \ k}. norm (f x - g2 x) \ e" "g2 integrable_on {a..b} \ {x. c \ x \ k}" - assume k:"k\Basis" + apply (rule_tac[!] x=g in exI) + using as(1) integrable_split[OF as(2) k] + apply auto + done + } + fix c k g1 g2 + assume as: "\x\{a..b} \ {x. x \ k \ c}. norm (f x - g1 x) \ e" "g1 integrable_on {a..b} \ {x. x \ k \ c}" + "\x\{a..b} \ {x. c \ x \ k}. norm (f x - g2 x) \ e" "g2 integrable_on {a..b} \ {x. c \ x \ k}" + assume k: "k \ Basis" let ?g = "\x. if x\k = c then f x else if x\k \ c then g1 x else g2 x" - show "\g. (\x\{a..b}. norm (f x - g x) \ e) \ g integrable_on {a..b}" apply(rule_tac x="?g" in exI) - proof safe case goal1 thus ?case apply- apply(cases "x\k=c", case_tac "x\k < c") using as assms by auto - next case goal2 presume "?g integrable_on {a..b} \ {x. x \ k \ c}" "?g integrable_on {a..b} \ {x. x \ k \ c}" - then guess h1 h2 unfolding integrable_on_def by auto from has_integral_split[OF this k] - show ?case unfolding integrable_on_def by auto - next show "?g integrable_on {a..b} \ {x. x \ k \ c}" "?g integrable_on {a..b} \ {x. x \ k \ c}" - apply(rule_tac[!] integrable_spike[OF negligible_standard_hyperplane[of k c]]) using k as(2,4) by auto qed qed - -lemma approximable_on_division: fixes f::"'b::ordered_euclidean_space \ 'a::banach" - assumes "0 \ e" "d division_of {a..b}" "\i\d. \g. (\x\i. norm (f x - g x) \ e) \ g integrable_on i" + show "\g. (\x\{a..b}. norm (f x - g x) \ e) \ g integrable_on {a..b}" + apply (rule_tac x="?g" in exI) + proof safe + case goal1 + then show ?case + apply - + apply (cases "x\k=c") + apply (case_tac "x\k < c") + using as assms + apply auto + done + next + case goal2 + presume "?g integrable_on {a..b} \ {x. x \ k \ c}" + and "?g integrable_on {a..b} \ {x. x \ k \ c}" + then guess h1 h2 unfolding integrable_on_def by auto + from has_integral_split[OF this k] show ?case + unfolding integrable_on_def by auto + next + show "?g integrable_on {a..b} \ {x. x \ k \ c}" "?g integrable_on {a..b} \ {x. x \ k \ c}" + apply(rule_tac[!] integrable_spike[OF negligible_standard_hyperplane[of k c]]) + using k as(2,4) + apply auto + done + qed +qed + +lemma approximable_on_division: + fixes f :: "'b::ordered_euclidean_space \ 'a::banach" + assumes "0 \ e" + and "d division_of {a..b}" + and "\i\d. \g. (\x\i. norm (f x - g x) \ e) \ g integrable_on i" obtains g where "\x\{a..b}. norm (f x - g x) \ e" "g integrable_on {a..b}" -proof- note * = operative_division[OF monoidal_and operative_approximable[OF assms(1)] assms(2)] - note this[unfolded iterate_and[OF division_of_finite[OF assms(2)]]] from assms(3)[unfolded this[of f]] - guess g .. thus thesis apply-apply(rule that[of g]) by auto qed - -lemma integrable_continuous: fixes f::"'b::ordered_euclidean_space \ 'a::banach" - assumes "continuous_on {a..b} f" shows "f integrable_on {a..b}" -proof(rule integrable_uniform_limit,safe) fix e::real assume e:"0 < e" +proof - + note * = operative_division[OF monoidal_and operative_approximable[OF assms(1)] assms(2)] + note this[unfolded iterate_and[OF division_of_finite[OF assms(2)]]] + from assms(3)[unfolded this[of f]] guess g .. + then show thesis + apply - + apply (rule that[of g]) + apply auto + done +qed + +lemma integrable_continuous: + fixes f :: "'b::ordered_euclidean_space \ 'a::banach" + assumes "continuous_on {a..b} f" + shows "f integrable_on {a..b}" +proof (rule integrable_uniform_limit, safe) + fix e :: real + assume e: "e > 0" from compact_uniformly_continuous[OF assms compact_interval,unfolded uniformly_continuous_on_def,rule_format,OF e] guess d .. note d=conjunctD2[OF this,rule_format] from fine_division_exists[OF gauge_ball[OF d(1)], of a b] guess p . note p=this note p' = tagged_division_ofD[OF p(1)] - have *:"\i\snd ` p. \g. (\x\i. norm (f x - g x) \ e) \ g integrable_on i" - proof(safe,unfold snd_conv) fix x l assume as:"(x,l) \ p" - from p'(4)[OF this] guess a b apply-by(erule exE)+ note l=this - show "\g. (\x\l. norm (f x - g x) \ e) \ g integrable_on l" apply(rule_tac x="\y. f x" in exI) - proof safe show "(\y. f x) integrable_on l" unfolding integrable_on_def l by(rule,rule has_integral_const) - fix y assume y:"y\l" note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this] + have *: "\i\snd ` p. \g. (\x\i. norm (f x - g x) \ e) \ g integrable_on i" + proof (safe, unfold snd_conv) + fix x l + assume as: "(x, l) \ p" + from p'(4)[OF this] guess a b by (elim exE) note l=this + show "\g. (\x\l. norm (f x - g x) \ e) \ g integrable_on l" + apply (rule_tac x="\y. f x" in exI) + proof safe + show "(\y. f x) integrable_on l" + unfolding integrable_on_def l + apply rule + apply (rule has_integral_const) + done + fix y + assume y: "y \ l" + note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this] note d(2)[OF _ _ this[unfolded mem_ball]] - thus "norm (f y - f x) \ e" using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce qed qed - from e have "0 \ e" by auto from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g . - thus "\g. (\x\{a..b}. norm (f x - g x) \ e) \ g integrable_on {a..b}" by auto qed + then show "norm (f y - f x) \ e" + using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce + qed + qed + from e have "e \ 0" + by auto + from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g . + then show "\g. (\x\{a..b}. norm (f x - g x) \ e) \ g integrable_on {a..b}" + by auto +qed + subsection {* Specialization of additivity to one dimension. *} @@ -6410,374 +6478,978 @@ and real_inner_1_right: "inner x 1 = x" by simp_all -lemma operative_1_lt: assumes "monoidal opp" +lemma operative_1_lt: + assumes "monoidal opp" shows "operative opp f \ ((\a b. b \ a \ f {a..b::real} = neutral opp) \ - (\a b c. a < c \ c < b \ opp (f{a..c})(f{c..b}) = f {a..b}))" - apply (simp add: operative_def content_eq_0 less_one) -proof safe fix a b c::"real" assume as:"\a b c. f {a..b} = opp (f ({a..b} \ {x. x \ c})) - (f ({a..b} \ {x. c \ x}))" "a < c" "c < b" - from this(2-) have "{a..b} \ {x. x \ c} = {a..c}" "{a..b} \ {x. x \ c} = {c..b}" by auto - thus "opp (f {a..c}) (f {c..b}) = f {a..b}" unfolding as(1)[rule_format,of a b "c"] by auto -next fix a b c::real - assume as:"\a b. b \ a \ f {a..b} = neutral opp" "\a b c. a < c \ c < b \ opp (f {a..c}) (f {c..b}) = f {a..b}" + (\a b c. a < c \ c < b \ opp (f {a..c}) (f {c..b}) = f {a..b}))" + apply (simp add: operative_def content_eq_0) +proof safe + fix a b c :: real + assume as: + "\a b c. f {a..b} = opp (f ({a..b} \ {x. x \ c})) (f ({a..b} \ {x. c \ x}))" + "a < c" + "c < b" + from this(2-) have "{a..b} \ {x. x \ c} = {a..c}" "{a..b} \ {x. x \ c} = {c..b}" + by auto + then show "opp (f {a..c}) (f {c..b}) = f {a..b}" + unfolding as(1)[rule_format,of a b "c"] by auto +next + fix a b c :: real + assume as: "\a b. b \ a \ f {a..b} = neutral opp" + "\a b c. a < c \ c < b \ opp (f {a..c}) (f {c..b}) = f {a..b}" show "f {a..b} = opp (f ({a..b} \ {x. x \ c})) (f ({a..b} \ {x. c \ x}))" - proof(cases "c \ {a .. b}") - case False hence "c c>b" by auto - thus ?thesis apply-apply(erule disjE) - proof- assume "c {x. x \ c} = {1..0}" "{a..b} \ {x. c \ x} = {a..b}" by auto - show ?thesis unfolding * apply(subst as(1)[rule_format,of 0 1]) using assms by auto - next assume "b {x. x \ c} = {a..b}" "{a..b} \ {x. c \ x} = {1..0}" by auto - show ?thesis unfolding * apply(subst as(1)[rule_format,of 0 1]) using assms by auto + proof (cases "c \ {a..b}") + case False + then have "c < a \ c > b" by auto + then show ?thesis + proof + assume "c < a" + then have *: "{a..b} \ {x. x \ c} = {1..0}" "{a..b} \ {x. c \ x} = {a..b}" + by auto + show ?thesis + unfolding * + apply (subst as(1)[rule_format,of 0 1]) + using assms + apply auto + done + next + assume "b < c" + then have *: "{a..b} \ {x. x \ c} = {a..b}" "{a..b} \ {x. c \ x} = {1..0}" + by auto + show ?thesis + unfolding * + apply (subst as(1)[rule_format,of 0 1]) + using assms + apply auto + done qed - next case True hence *:"min (b) c = c" "max a c = c" by auto - have **: "(1::real) \ Basis" by simp - have ***:"\P Q. (\i\Basis. (if i = 1 then P i else Q i) *\<^sub>R i) = (P 1::real)" + next + case True + then have *: "min (b) c = c" "max a c = c" + by auto + have **: "(1::real) \ Basis" + by simp + have ***: "\P Q. (\i\Basis. (if i = 1 then P i else Q i) *\<^sub>R i) = (P 1::real)" by simp show ?thesis unfolding interval_split[OF **, unfolded real_inner_1_right] unfolding *** * - proof(cases "c = a \ c = b") - case False thus "f {a..b} = opp (f {a..c}) (f {c..b})" - apply-apply(subst as(2)[rule_format]) using True by auto - next case True thus "f {a..b} = opp (f {a..c}) (f {c..b})" apply- - proof(erule disjE) assume *:"c=a" - hence "f {a..c} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto - thus ?thesis using assms unfolding * by auto - next assume *:"c=b" hence "f {c..b} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto - thus ?thesis using assms unfolding * by auto qed qed qed qed - -lemma operative_1_le: assumes "monoidal opp" + proof (cases "c = a \ c = b") + case False + then show "f {a..b} = opp (f {a..c}) (f {c..b})" + apply - + apply (subst as(2)[rule_format]) + using True + apply auto + done + next + case True + then show "f {a..b} = opp (f {a..c}) (f {c..b})" + proof + assume *: "c = a" + then have "f {a..c} = neutral opp" + apply - + apply (rule as(1)[rule_format]) + apply auto + done + then show ?thesis + using assms unfolding * by auto + next + assume *: "c = b" + then have "f {c..b} = neutral opp" + apply - + apply (rule as(1)[rule_format]) + apply auto + done + then show ?thesis + using assms unfolding * by auto + qed + qed + qed +qed + +lemma operative_1_le: + assumes "monoidal opp" shows "operative opp f \ ((\a b. b \ a \ f {a..b::real} = neutral opp) \ - (\a b c. a \ c \ c \ b \ opp (f{a..c})(f{c..b}) = f {a..b}))" -unfolding operative_1_lt[OF assms] -proof safe fix a b c::"real" assume as:"\a b c. a \ c \ c \ b \ opp (f {a..c}) (f {c..b}) = f {a..b}" "a < c" "c < b" - show "opp (f {a..c}) (f {c..b}) = f {a..b}" apply(rule as(1)[rule_format]) using as(2-) by auto -next fix a b c ::"real" assume "\a b. b \ a \ f {a..b} = neutral opp" - "\a b c. a < c \ c < b \ opp (f {a..c}) (f {c..b}) = f {a..b}" "a \ c" "c \ b" + (\a b c. a \ c \ c \ b \ opp (f {a..c}) (f {c..b}) = f {a..b}))" + unfolding operative_1_lt[OF assms] +proof safe + fix a b c :: real + assume as: + "\a b c. a \ c \ c \ b \ opp (f {a..c}) (f {c..b}) = f {a..b}" + "a < c" + "c < b" + show "opp (f {a..c}) (f {c..b}) = f {a..b}" + apply (rule as(1)[rule_format]) + using as(2-) + apply auto + done +next + fix a b c :: real + assume "\a b. b \ a \ f {a..b} = neutral opp" + and "\a b c. a < c \ c < b \ opp (f {a..c}) (f {c..b}) = f {a..b}" + and "a \ c" + and "c \ b" note as = this[rule_format] show "opp (f {a..c}) (f {c..b}) = f {a..b}" - proof(cases "c = a \ c = b") - case False thus ?thesis apply-apply(subst as(2)) using as(3-) by(auto) - next case True thus ?thesis apply- - proof(erule disjE) assume *:"c=a" hence "f {a..c} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto - thus ?thesis using assms unfolding * by auto - next assume *:"c=b" hence "f {c..b} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto - thus ?thesis using assms unfolding * by auto qed qed qed + proof (cases "c = a \ c = b") + case False + then show ?thesis + apply - + apply (subst as(2)) + using as(3-) + apply auto + done + next + case True + then show ?thesis + proof + assume *: "c = a" + then have "f {a..c} = neutral opp" + apply - + apply (rule as(1)[rule_format]) + apply auto + done + then show ?thesis + using assms unfolding * by auto + next + assume *: "c = b" + then have "f {c..b} = neutral opp" + apply - + apply (rule as(1)[rule_format]) + apply auto + done + then show ?thesis + using assms unfolding * by auto + qed + qed +qed + subsection {* Special case of additivity we need for the FCT. *} -lemma interval_bound_sing[simp]: "interval_upperbound {a} = a" "interval_lowerbound {a} = a" - unfolding interval_upperbound_def interval_lowerbound_def by (auto simp: euclidean_representation) - -lemma additive_tagged_division_1: fixes f::"real \ 'a::real_normed_vector" - assumes "a \ b" "p tagged_division_of {a..b}" +lemma interval_bound_sing[simp]: + "interval_upperbound {a} = a" + "interval_lowerbound {a} = a" + unfolding interval_upperbound_def interval_lowerbound_def + by (auto simp: euclidean_representation) + +lemma additive_tagged_division_1: + fixes f :: "real \ 'a::real_normed_vector" + assumes "a \ b" + and "p tagged_division_of {a..b}" shows "setsum (\(x,k). f(interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a" -proof- let ?f = "(\k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))" - have ***:"\i\Basis. a \ i \ b \ i" using assms by auto - have *:"operative op + ?f" unfolding operative_1_lt[OF monoidal_monoid] interval_eq_empty by auto - have **:"{a..b} \ {}" using assms(1) by auto note operative_tagged_division[OF monoidal_monoid * assms(2)] +proof - + let ?f = "(\k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))" + have ***: "\i\Basis. a \ i \ b \ i" + using assms by auto + have *: "operative op + ?f" + unfolding operative_1_lt[OF monoidal_monoid] interval_eq_empty by auto + have **: "{a..b} \ {}" + using assms(1) by auto note operative_tagged_division[OF monoidal_monoid * assms(2)] note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric] - show ?thesis unfolding * apply(subst setsum_iterate[symmetric]) defer - apply(rule setsum_cong2) unfolding split_paired_all split_conv using assms(2) by auto qed + show ?thesis + unfolding * + apply (subst setsum_iterate[symmetric]) + defer + apply (rule setsum_cong2) + unfolding split_paired_all split_conv + using assms(2) + apply auto + done +qed + subsection {* A useful lemma allowing us to factor out the content size. *} lemma has_integral_factor_content: - "(f has_integral i) {a..b} \ (\e>0. \d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p - \ norm (setsum (\(x,k). content k *\<^sub>R f x) p - i) \ e * content {a..b}))" -proof(cases "content {a..b} = 0") - case True show ?thesis unfolding has_integral_null_eq[OF True] apply safe - apply(rule,rule,rule gauge_trivial,safe) unfolding setsum_content_null[OF True] True defer - apply(erule_tac x=1 in allE,safe) defer apply(rule fine_division_exists[of _ a b],assumption) - apply(erule_tac x=p in allE) unfolding setsum_content_null[OF True] by auto -next case False note F = this[unfolded content_lt_nz[symmetric]] - let ?P = "\e opp. \d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ opp (norm ((\(x, k)\p. content k *\<^sub>R f x) - i)) e)" - show ?thesis apply(subst has_integral) - proof safe fix e::real assume e:"e>0" - { assume "\e>0. ?P e op <" thus "?P (e * content {a..b}) op \" apply(erule_tac x="e * content {a..b}" in allE) - apply(erule impE) defer apply(erule exE,rule_tac x=d in exI) - using F e by(auto simp add:field_simps intro:mult_pos_pos) } - { assume "\e>0. ?P (e * content {a..b}) op \" thus "?P e op <" apply(erule_tac x="e / 2 / content {a..b}" in allE) - apply(erule impE) defer apply(erule exE,rule_tac x=d in exI) - using F e by(auto simp add:field_simps intro:mult_pos_pos) } qed qed + "(f has_integral i) {a..b} \ + (\e>0. \d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ + norm (setsum (\(x,k). content k *\<^sub>R f x) p - i) \ e * content {a..b}))" +proof (cases "content {a..b} = 0") + case True + show ?thesis + unfolding has_integral_null_eq[OF True] + apply safe + apply (rule, rule, rule gauge_trivial, safe) + unfolding setsum_content_null[OF True] True + defer + apply (erule_tac x=1 in allE) + apply safe + defer + apply (rule fine_division_exists[of _ a b]) + apply assumption + apply (erule_tac x=p in allE) + unfolding setsum_content_null[OF True] + apply auto + done +next + case False + note F = this[unfolded content_lt_nz[symmetric]] + let ?P = "\e opp. \d. gauge d \ + (\p. p tagged_division_of {a..b} \ d fine p \ opp (norm ((\(x, k)\p. content k *\<^sub>R f x) - i)) e)" + show ?thesis + apply (subst has_integral) + proof safe + fix e :: real + assume e: "e > 0" + { + assume "\e>0. ?P e op <" + then show "?P (e * content {a..b}) op \" + apply (erule_tac x="e * content {a..b}" in allE) + apply (erule impE) + defer + apply (erule exE,rule_tac x=d in exI) + using F e + apply (auto simp add:field_simps intro:mult_pos_pos) + done + } + { + assume "\e>0. ?P (e * content {a..b}) op \" + then show "?P e op <" + apply (erule_tac x="e / 2 / content {a..b}" in allE) + apply (erule impE) + defer + apply (erule exE,rule_tac x=d in exI) + using F e + apply (auto simp add: field_simps intro: mult_pos_pos) + done + } + qed +qed + subsection {* Fundamental theorem of calculus. *} -lemma interval_bounds_real: assumes "a\(b::real)" - shows "interval_upperbound {a..b} = b" "interval_lowerbound {a..b} = a" - apply(rule_tac[!] interval_bounds) using assms by auto - -lemma fundamental_theorem_of_calculus: fixes f::"real \ 'a::banach" - assumes "a \ b" "\x\{a..b}. (f has_vector_derivative f' x) (at x within {a..b})" - shows "(f' has_integral (f b - f a)) ({a..b})" -unfolding has_integral_factor_content -proof safe fix e::real assume e:"e>0" +lemma interval_bounds_real: + fixes q b :: real + assumes "a \ b" + shows "interval_upperbound {a..b} = b" + and "interval_lowerbound {a..b} = a" + apply (rule_tac[!] interval_bounds) + using assms + apply auto + done + +lemma fundamental_theorem_of_calculus: + fixes f :: "real \ 'a::banach" + assumes "a \ b" + and "\x\{a..b}. (f has_vector_derivative f' x) (at x within {a..b})" + shows "(f' has_integral (f b - f a)) {a..b}" + unfolding has_integral_factor_content +proof safe + fix e :: real + assume e: "e > 0" note assm = assms(2)[unfolded has_vector_derivative_def has_derivative_within_alt] - have *:"\P Q. \x\{a..b}. P x \ (\e>0. \d>0. Q x e d) \ \x. \(d::real)>0. x\{a..b} \ Q x e d" using e by blast - note this[OF assm,unfolded gauge_existence_lemma] from choice[OF this,unfolded Ball_def[symmetric]] - guess d .. note d=conjunctD2[OF this[rule_format],rule_format] + have *: "\P Q. \x\{a..b}. P x \ (\e>0. \d>0. Q x e d) \ \x. \(d::real)>0. x\{a..b} \ Q x e d" + using e by blast + note this[OF assm,unfolded gauge_existence_lemma] + from choice[OF this,unfolded Ball_def[symmetric]] guess d .. + note d=conjunctD2[OF this[rule_format],rule_format] show "\d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ - norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content {a..b})" - apply(rule_tac x="\x. ball x (d x)" in exI,safe) - apply(rule gauge_ball_dependent,rule,rule d(1)) - proof- fix p assume as:"p tagged_division_of {a..b}" "(\x. ball x (d x)) fine p" + norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content {a..b})" + apply (rule_tac x="\x. ball x (d x)" in exI) + apply safe + apply (rule gauge_ball_dependent) + apply rule + apply (rule d(1)) + proof - + fix p + assume as: "p tagged_division_of {a..b}" "(\x. ball x (d x)) fine p" show "norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content {a..b}" unfolding content_real[OF assms(1)] additive_tagged_division_1[OF assms(1) as(1),of f,symmetric] unfolding additive_tagged_division_1[OF assms(1) as(1),of "\x. x",symmetric] - unfolding setsum_right_distrib defer unfolding setsum_subtractf[symmetric] - proof(rule setsum_norm_le,safe) fix x k assume "(x,k)\p" - note xk = tagged_division_ofD(2-4)[OF as(1) this] from this(3) guess u v apply-by(erule exE)+ note k=this - have *:"u \ v" using xk unfolding k by auto - have ball:"\xa\k. xa \ ball x (d x)" using as(2)[unfolded fine_def,rule_format,OF `(x,k)\p`, - unfolded split_conv subset_eq] . + unfolding setsum_right_distrib + defer + unfolding setsum_subtractf[symmetric] + proof (rule setsum_norm_le,safe) + fix x k + assume "(x, k) \ p" + note xk = tagged_division_ofD(2-4)[OF as(1) this] + from this(3) guess u v by (elim exE) note k=this + have *: "u \ v" + using xk unfolding k by auto + have ball: "\xa\k. xa \ ball x (d x)" + using as(2)[unfolded fine_def,rule_format,OF `(x,k)\p`,unfolded split_conv subset_eq] . have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \ norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)" - apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm]) - unfolding scaleR_diff_left by(auto simp add:algebra_simps) - also have "... \ e * norm (u - x) + e * norm (v - x)" - apply(rule add_mono) apply(rule d(2)[of "x" "u",unfolded o_def]) prefer 4 - apply(rule d(2)[of "x" "v",unfolded o_def]) + apply (rule order_trans[OF _ norm_triangle_ineq4]) + apply (rule eq_refl) + apply (rule arg_cong[where f=norm]) + unfolding scaleR_diff_left + apply (auto simp add:algebra_simps) + done + also have "\ \ e * norm (u - x) + e * norm (v - x)" + apply (rule add_mono) + apply (rule d(2)[of "x" "u",unfolded o_def]) + prefer 4 + apply (rule d(2)[of "x" "v",unfolded o_def]) using ball[rule_format,of u] ball[rule_format,of v] - using xk(1-2) unfolding k subset_eq by(auto simp add:dist_real_def) - also have "... \ e * (interval_upperbound k - interval_lowerbound k)" - unfolding k interval_bounds_real[OF *] using xk(1) unfolding k by(auto simp add:dist_real_def field_simps) + using xk(1-2) + unfolding k subset_eq + apply (auto simp add:dist_real_def) + done + also have "\ \ e * (interval_upperbound k - interval_lowerbound k)" + unfolding k interval_bounds_real[OF *] + using xk(1) + unfolding k + by (auto simp add: dist_real_def field_simps) finally show "norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k))) \ - e * (interval_upperbound k - interval_lowerbound k)" unfolding k interval_bounds_real[OF *] content_real[OF *] . - qed qed qed + e * (interval_upperbound k - interval_lowerbound k)" + unfolding k interval_bounds_real[OF *] content_real[OF *] . + qed + qed +qed + subsection {* Attempt a systematic general set of "offset" results for components. *} lemma gauge_modify: assumes "(\s. open s \ open {x. f(x) \ s})" "gauge d" shows "gauge (\x. {y. f y \ d (f x)})" - using assms unfolding gauge_def apply safe defer apply(erule_tac x="f x" in allE) - apply(erule_tac x="d (f x)" in allE) by auto + using assms + unfolding gauge_def + apply safe + defer + apply (erule_tac x="f x" in allE) + apply (erule_tac x="d (f x)" in allE) + apply auto + done + subsection {* Only need trivial subintervals if the interval itself is trivial. *} -lemma division_of_nontrivial: fixes s::"('a::ordered_euclidean_space) set set" - assumes "s division_of {a..b}" "content({a..b}) \ 0" - shows "{k. k \ s \ content k \ 0} division_of {a..b}" using assms(1) apply- -proof(induct "card s" arbitrary:s rule:nat_less_induct) - fix s::"'a set set" assume assm:"s division_of {a..b}" - "\mx. m = card x \ x division_of {a..b} \ {k \ x. content k \ 0} division_of {a..b}" - note s = division_ofD[OF assm(1)] let ?thesis = "{k \ s. content k \ 0} division_of {a..b}" - { presume *:"{k \ s. content k \ 0} \ s \ ?thesis" - show ?thesis apply cases defer apply(rule *,assumption) using assm(1) by auto } - assume noteq:"{k \ s. content k \ 0} \ s" - then obtain k where k:"k\s" "content k = 0" by auto - from s(4)[OF k(1)] guess c d apply-by(erule exE)+ note k=k this - from k have "card s > 0" unfolding card_gt_0_iff using assm(1) by auto - hence card:"card (s - {k}) < card s" using assm(1) k(1) apply(subst card_Diff_singleton_if) by auto - have *:"closed (\(s - {k}))" apply(rule closed_Union) defer apply rule apply(drule DiffD1,drule s(4)) - apply safe apply(rule closed_interval) using assm(1) by auto - have "k \ \(s - {k})" apply safe apply(rule *[unfolded closed_limpt,rule_format]) unfolding islimpt_approachable - proof safe fix x and e::real assume as:"x\k" "e>0" +lemma division_of_nontrivial: + fixes s :: "'a::ordered_euclidean_space set set" + assumes "s division_of {a..b}" + and "content {a..b} \ 0" + shows "{k. k \ s \ content k \ 0} division_of {a..b}" + using assms(1) + apply - +proof (induct "card s" arbitrary: s rule: nat_less_induct) + fix s::"'a set set" + assume assm: "s division_of {a..b}" + "\mx. m = card x \ + x division_of {a..b} \ {k \ x. content k \ 0} division_of {a..b}" + note s = division_ofD[OF assm(1)] + let ?thesis = "{k \ s. content k \ 0} division_of {a..b}" + { + presume *: "{k \ s. content k \ 0} \ s \ ?thesis" + show ?thesis + apply cases + defer + apply (rule *) + apply assumption + using assm(1) + apply auto + done + } + assume noteq: "{k \ s. content k \ 0} \ s" + then obtain k where k: "k \ s" "content k = 0" + by auto + from s(4)[OF k(1)] guess c d by (elim exE) note k=k this + from k have "card s > 0" + unfolding card_gt_0_iff using assm(1) by auto + then have card: "card (s - {k}) < card s" + using assm(1) k(1) + apply (subst card_Diff_singleton_if) + apply auto + done + have *: "closed (\(s - {k}))" + apply (rule closed_Union) + defer + apply rule + apply (drule DiffD1,drule s(4)) + apply safe + apply (rule closed_interval) + using assm(1) + apply auto + done + have "k \ \(s - {k})" + apply safe + apply (rule *[unfolded closed_limpt,rule_format]) + unfolding islimpt_approachable + proof safe + fix x + fix e :: real + assume as: "x \ k" "e > 0" from k(2)[unfolded k content_eq_0] guess i .. - hence i:"c\i = d\i" "i\Basis" using s(3)[OF k(1),unfolded k] unfolding interval_ne_empty by auto - hence xi:"x\i = d\i" using as unfolding k mem_interval by (metis antisym) - def y \ "(\j\Basis. (if j = i then if c\i \ (a\i + b\i) / 2 then c\i + - min e (b\i - c\i) / 2 else c\i - min e (c\i - a\i) / 2 else x\j) *\<^sub>R j)::'a" - show "\x'\\(s - {k}). x' \ x \ dist x' x < e" apply(rule_tac x=y in bexI) - proof have "d \ {c..d}" using s(3)[OF k(1)] unfolding k interval_eq_empty mem_interval by(fastforce simp add: not_less) - hence "d \ {a..b}" using s(2)[OF k(1)] unfolding k by auto note di = this[unfolded mem_interval,THEN bspec[where x=i]] - hence xyi:"y\i \ x\i" - unfolding y_def i xi using as(2) assms(2)[unfolded content_eq_0] i(2) + then have i:"c\i = d\i" "i\Basis" + using s(3)[OF k(1),unfolded k] unfolding interval_ne_empty by auto + then have xi: "x\i = d\i" + using as unfolding k mem_interval by (metis antisym) + def y \ "\j\Basis. (if j = i then if c\i \ (a\i + b\i) / 2 then c\i + + min e (b\i - c\i) / 2 else c\i - min e (c\i - a\i) / 2 else x\j) *\<^sub>R j" + show "\x'\\(s - {k}). x' \ x \ dist x' x < e" + apply (rule_tac x=y in bexI) + proof + have "d \ {c..d}" + using s(3)[OF k(1)] + unfolding k interval_eq_empty mem_interval + by (fastforce simp add: not_less) + then have "d \ {a..b}" + using s(2)[OF k(1)] + unfolding k + by auto + note di = this[unfolded mem_interval,THEN bspec[where x=i]] + then have xyi: "y\i \ x\i" + unfolding y_def i xi + using as(2) assms(2)[unfolded content_eq_0] i(2) by (auto elim!: ballE[of _ _ i]) - thus "y \ x" unfolding euclidean_eq_iff[where 'a='a] using i by auto - have *:"Basis = insert i (Basis - {i})" using i by auto - have "norm (y - x) < e + setsum (\i. 0) Basis" apply(rule le_less_trans[OF norm_le_l1]) - apply(subst *,subst setsum_insert) prefer 3 apply(rule add_less_le_mono) - proof- + then show "y \ x" + unfolding euclidean_eq_iff[where 'a='a] using i by auto + have *: "Basis = insert i (Basis - {i})" + using i by auto + have "norm (y - x) < e + setsum (\i. 0) Basis" + apply (rule le_less_trans[OF norm_le_l1]) + apply (subst *) + apply (subst setsum_insert) + prefer 3 + apply (rule add_less_le_mono) + proof - show "\(y - x) \ i\ < e" using di as(2) y_def i xi by (auto simp: inner_simps) show "(\i\Basis - {i}. \(y - x) \ i\) \ (\i\Basis. 0)" unfolding y_def by (auto simp: inner_simps) - qed auto thus "dist y x < e" unfolding dist_norm by auto - have "y\k" unfolding k mem_interval apply rule apply(erule_tac x=i in ballE) using xyi k i xi by auto - moreover have "y \ \s" - using set_rev_mp[OF as(1) s(2)[OF k(1)]] as(2) di i unfolding s mem_interval y_def + qed auto + then show "dist y x < e" + unfolding dist_norm by auto + have "y \ k" + unfolding k mem_interval + apply rule + apply (erule_tac x=i in ballE) + using xyi k i xi + apply auto + done + moreover + have "y \ \s" + using set_rev_mp[OF as(1) s(2)[OF k(1)]] as(2) di i + unfolding s mem_interval y_def by (auto simp: field_simps elim!: ballE[of _ _ i]) - ultimately show "y \ \(s - {k})" by auto - qed qed hence "\(s - {k}) = {a..b}" unfolding s(6)[symmetric] by auto - hence "{ka \ s - {k}. content ka \ 0} division_of {a..b}" apply-apply(rule assm(2)[rule_format,OF card refl]) - apply(rule division_ofI) defer apply(rule_tac[1-4] s) using assm(1) by auto - moreover have "{ka \ s - {k}. content ka \ 0} = {k \ s. content k \ 0}" using k by auto ultimately show ?thesis by auto qed + ultimately + show "y \ \(s - {k})" by auto + qed + qed + then have "\(s - {k}) = {a..b}" + unfolding s(6)[symmetric] by auto + then have "{ka \ s - {k}. content ka \ 0} division_of {a..b}" + apply - + apply (rule assm(2)[rule_format,OF card refl]) + apply (rule division_ofI) + defer + apply (rule_tac[1-4] s) + using assm(1) + apply auto + done + moreover + have "{ka \ s - {k}. content ka \ 0} = {k \ s. content k \ 0}" + using k by auto + ultimately show ?thesis by auto +qed + subsection {* Integrability on subintervals. *} -lemma operative_integrable: fixes f::"'b::ordered_euclidean_space \ 'a::banach" shows - "operative op \ (\i. f integrable_on i)" - unfolding operative_def neutral_and apply safe apply(subst integrable_on_def) - unfolding has_integral_null_eq apply(rule,rule refl) apply(rule,assumption,assumption)+ - unfolding integrable_on_def by(auto intro!: has_integral_split) - -lemma integrable_subinterval: fixes f::"'b::ordered_euclidean_space \ 'a::banach" - assumes "f integrable_on {a..b}" "{c..d} \ {a..b}" shows "f integrable_on {c..d}" - apply(cases "{c..d} = {}") defer apply(rule partial_division_extend_1[OF assms(2)],assumption) - using operative_division_and[OF operative_integrable,symmetric,of _ _ _ f] assms(1) by auto +lemma operative_integrable: + fixes f :: "'b::ordered_euclidean_space \ 'a::banach" + shows "operative op \ (\i. f integrable_on i)" + unfolding operative_def neutral_and + apply safe + apply (subst integrable_on_def) + unfolding has_integral_null_eq + apply (rule, rule refl) + apply (rule, assumption, assumption)+ + unfolding integrable_on_def + by (auto intro!: has_integral_split) + +lemma integrable_subinterval: + fixes f :: "'b::ordered_euclidean_space \ 'a::banach" + assumes "f integrable_on {a..b}" + and "{c..d} \ {a..b}" + shows "f integrable_on {c..d}" + apply (cases "{c..d} = {}") + defer + apply (rule partial_division_extend_1[OF assms(2)],assumption) + using operative_division_and[OF operative_integrable,symmetric,of _ _ _ f] assms(1) + apply auto + done + subsection {* Combining adjacent intervals in 1 dimension. *} -lemma has_integral_combine: assumes "(a::real) \ c" "c \ b" - "(f has_integral i) {a..c}" "(f has_integral (j::'a::banach)) {c..b}" +lemma has_integral_combine: + fixes a b c :: real + assumes "a \ c" + and "c \ b" + and "(f has_integral i) {a..c}" + and "(f has_integral (j::'a::banach)) {c..b}" shows "(f has_integral (i + j)) {a..b}" -proof- note operative_integral[of f, unfolded operative_1_le[OF monoidal_lifted[OF monoidal_monoid]]] - note conjunctD2[OF this,rule_format] note * = this(2)[OF conjI[OF assms(1-2)],unfolded if_P[OF assms(3)]] - hence "f integrable_on {a..b}" apply- apply(rule ccontr) apply(subst(asm) if_P) defer - apply(subst(asm) if_P) using assms(3-) by auto - with * show ?thesis apply-apply(subst(asm) if_P) defer apply(subst(asm) if_P) defer apply(subst(asm) if_P) - unfolding lifted.simps using assms(3-) by(auto simp add: integrable_on_def integral_unique) qed - -lemma integral_combine: fixes f::"real \ 'a::banach" - assumes "a \ c" "c \ b" "f integrable_on ({a..b})" - shows "integral {a..c} f + integral {c..b} f = integral({a..b}) f" - apply(rule integral_unique[symmetric]) apply(rule has_integral_combine[OF assms(1-2)]) - apply(rule_tac[!] integrable_integral integrable_subinterval[OF assms(3)])+ using assms(1-2) by auto - -lemma integrable_combine: fixes f::"real \ 'a::banach" - assumes "a \ c" "c \ b" "f integrable_on {a..c}" "f integrable_on {c..b}" - shows "f integrable_on {a..b}" using assms unfolding integrable_on_def by(fastforce intro!:has_integral_combine) +proof - + note operative_integral[of f, unfolded operative_1_le[OF monoidal_lifted[OF monoidal_monoid]]] + note conjunctD2[OF this,rule_format] + note * = this(2)[OF conjI[OF assms(1-2)],unfolded if_P[OF assms(3)]] + then have "f integrable_on {a..b}" + apply - + apply (rule ccontr) + apply (subst(asm) if_P) + defer + apply (subst(asm) if_P) + using assms(3-) + apply auto + done + with * + show ?thesis + apply - + apply (subst(asm) if_P) + defer + apply (subst(asm) if_P) + defer + apply (subst(asm) if_P) + unfolding lifted.simps + using assms(3-) + apply (auto simp add: integrable_on_def integral_unique) + done +qed + +lemma integral_combine: + fixes f :: "real \ 'a::banach" + assumes "a \ c" + and "c \ b" + and "f integrable_on {a..b}" + shows "integral {a..c} f + integral {c..b} f = integral {a..b} f" + apply (rule integral_unique[symmetric]) + apply (rule has_integral_combine[OF assms(1-2)]) + apply (rule_tac[!] integrable_integral integrable_subinterval[OF assms(3)])+ + using assms(1-2) + apply auto + done + +lemma integrable_combine: + fixes f :: "real \ 'a::banach" + assumes "a \ c" + and "c \ b" + and "f integrable_on {a..c}" + and "f integrable_on {c..b}" + shows "f integrable_on {a..b}" + using assms + unfolding integrable_on_def + by (fastforce intro!:has_integral_combine) + subsection {* Reduce integrability to "local" integrability. *} -lemma integrable_on_little_subintervals: fixes f::"'b::ordered_euclidean_space \ 'a::banach" - assumes "\x\{a..b}. \d>0. \u v. x \ {u..v} \ {u..v} \ ball x d \ {u..v} \ {a..b} \ f integrable_on {u..v}" +lemma integrable_on_little_subintervals: + fixes f :: "'b::ordered_euclidean_space \ 'a::banach" + assumes "\x\{a..b}. \d>0. \u v. x \ {u..v} \ {u..v} \ ball x d \ {u..v} \ {a..b} \ + f integrable_on {u..v}" shows "f integrable_on {a..b}" -proof- have "\x. \d. x\{a..b} \ d>0 \ (\u v. x \ {u..v} \ {u..v} \ ball x d \ {u..v} \ {a..b} \ f integrable_on {u..v})" - using assms by auto note this[unfolded gauge_existence_lemma] from choice[OF this] guess d .. note d=this[rule_format] - guess p apply(rule fine_division_exists[OF gauge_ball_dependent,of d a b]) using d by auto note p=this(1-2) - note division_of_tagged_division[OF this(1)] note * = operative_division_and[OF operative_integrable,OF this,symmetric,of f] - show ?thesis unfolding * apply safe unfolding snd_conv - proof- fix x k assume "(x,k) \ p" note tagged_division_ofD(2-4)[OF p(1) this] fineD[OF p(2) this] - thus "f integrable_on k" apply safe apply(rule d[THEN conjunct2,rule_format,of x]) by auto qed qed +proof - + have "\x. \d. x\{a..b} \ d>0 \ (\u v. x \ {u..v} \ {u..v} \ ball x d \ {u..v} \ {a..b} \ + f integrable_on {u..v})" + using assms by auto + note this[unfolded gauge_existence_lemma] + from choice[OF this] guess d .. note d=this[rule_format] + guess p + apply (rule fine_division_exists[OF gauge_ball_dependent,of d a b]) + using d + by auto + note p=this(1-2) + note division_of_tagged_division[OF this(1)] + note * = operative_division_and[OF operative_integrable,OF this,symmetric,of f] + show ?thesis + unfolding * + apply safe + unfolding snd_conv + proof - + fix x k + assume "(x, k) \ p" + note tagged_division_ofD(2-4)[OF p(1) this] fineD[OF p(2) this] + then show "f integrable_on k" + apply safe + apply (rule d[THEN conjunct2,rule_format,of x]) + apply auto + done + qed +qed + subsection {* Second FCT or existence of antiderivative. *} -lemma integrable_const[intro]:"(\x. c) integrable_on {a..b}" - unfolding integrable_on_def by(rule,rule has_integral_const) - -lemma integral_has_vector_derivative: fixes f::"real \ 'a::banach" - assumes "continuous_on {a..b} f" "x \ {a..b}" +lemma integrable_const[intro]: "(\x. c) integrable_on {a..b}" + unfolding integrable_on_def + apply rule + apply (rule has_integral_const) + done + +lemma integral_has_vector_derivative: + fixes f :: "real \ 'a::banach" + assumes "continuous_on {a..b} f" + and "x \ {a..b}" shows "((\u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})" unfolding has_vector_derivative_def has_derivative_within_alt -apply safe apply(rule bounded_linear_scaleR_left) -proof- fix e::real assume e:"e>0" + apply safe + apply (rule bounded_linear_scaleR_left) +proof - + fix e :: real + assume e: "e > 0" note compact_uniformly_continuous[OF assms(1) compact_interval,unfolded uniformly_continuous_on_def] - from this[rule_format,OF e] guess d apply-by(erule conjE exE)+ note d=this[rule_format] + from this[rule_format,OF e] guess d by (elim conjE exE) note d=this[rule_format] let ?I = "\a b. integral {a..b} f" - show "\d>0. \y\{a..b}. norm (y - x) < d \ norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \ e * norm (y - x)" - proof(rule,rule,rule d,safe) case goal1 show ?case proof(cases "y < x") - case False have "f integrable_on {a..y}" apply(rule integrable_subinterval,rule integrable_continuous) - apply(rule assms) unfolding not_less using assms(2) goal1 by auto - hence *:"?I a y - ?I a x = ?I x y" unfolding algebra_simps apply(subst eq_commute) apply(rule integral_combine) - using False unfolding not_less using assms(2) goal1 by auto - have **:"norm (y - x) = content {x..y}" apply(subst content_real) using False unfolding not_less by auto - show ?thesis unfolding ** apply(rule has_integral_bound[where f="(\u. f u - f x)"]) unfolding * unfolding o_def - defer apply(rule has_integral_sub) apply(rule integrable_integral) - apply(rule integrable_subinterval,rule integrable_continuous) apply(rule assms)+ - proof- show "{x..y} \ {a..b}" using goal1 assms(2) by auto - have *:"y - x = norm(y - x)" using False by auto - show "((\xa. f x) has_integral (y - x) *\<^sub>R f x) {x.. y}" apply(subst *) unfolding ** by auto - show "\xa\{x..y}. norm (f xa - f x) \ e" apply safe apply(rule less_imp_le) - apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto - qed(insert e,auto) - next case True have "f integrable_on {a..x}" apply(rule integrable_subinterval,rule integrable_continuous) - apply(rule assms)+ unfolding not_less using assms(2) goal1 by auto - hence *:"?I a x - ?I a y = ?I y x" unfolding algebra_simps apply(subst eq_commute) apply(rule integral_combine) - using True using assms(2) goal1 by auto - have **:"norm (y - x) = content {y..x}" apply(subst content_real) using True unfolding not_less by auto - have ***:"\fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)" unfolding scaleR_left.diff by auto - show ?thesis apply(subst ***) unfolding norm_minus_cancel ** - apply(rule has_integral_bound[where f="(\u. f u - f x)"]) unfolding * unfolding o_def - defer apply(rule has_integral_sub) apply(subst minus_minus[symmetric]) unfolding minus_minus - apply(rule integrable_integral) apply(rule integrable_subinterval,rule integrable_continuous) apply(rule assms)+ - proof- show "{y..x} \ {a..b}" using goal1 assms(2) by auto - have *:"x - y = norm(y - x)" using True by auto - show "((\xa. f x) has_integral (x - y) *\<^sub>R f x) {y..x}" apply(subst *) unfolding ** by auto - show "\xa\{y..x}. norm (f xa - f x) \ e" apply safe apply(rule less_imp_le) - apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto - qed(insert e,auto) qed qed qed - -lemma antiderivative_continuous: assumes "continuous_on {a..b::real} f" - obtains g where "\x\ {a..b}. (g has_vector_derivative (f(x)::_::banach)) (at x within {a..b})" - apply(rule that,rule) using integral_has_vector_derivative[OF assms] by auto + show "\d>0. \y\{a..b}. norm (y - x) < d \ + norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \ e * norm (y - x)" + proof (rule, rule, rule d, safe) + case goal1 + show ?case + proof (cases "y < x") + case False + have "f integrable_on {a..y}" + apply (rule integrable_subinterval,rule integrable_continuous) + apply (rule assms) + unfolding not_less + using assms(2) goal1 + apply auto + done + then have *: "?I a y - ?I a x = ?I x y" + unfolding algebra_simps + apply (subst eq_commute) + apply (rule integral_combine) + using False + unfolding not_less + using assms(2) goal1 + apply auto + done + have **: "norm (y - x) = content {x..y}" + apply (subst content_real) + using False + unfolding not_less + apply auto + done + show ?thesis + unfolding ** + apply (rule has_integral_bound[where f="(\u. f u - f x)"]) + unfolding * + unfolding o_def + defer + apply (rule has_integral_sub) + apply (rule integrable_integral) + apply (rule integrable_subinterval) + apply (rule integrable_continuous) + apply (rule assms)+ + proof - + show "{x..y} \ {a..b}" + using goal1 assms(2) by auto + have *: "y - x = norm (y - x)" + using False by auto + show "((\xa. f x) has_integral (y - x) *\<^sub>R f x) {x.. y}" + apply (subst *) + unfolding ** + apply auto + done + show "\xa\{x..y}. norm (f xa - f x) \ e" + apply safe + apply (rule less_imp_le) + apply (rule d(2)[unfolded dist_norm]) + using assms(2) + using goal1 + apply auto + done + qed (insert e, auto) + next + case True + have "f integrable_on {a..x}" + apply (rule integrable_subinterval,rule integrable_continuous) + apply (rule assms)+ + unfolding not_less + using assms(2) goal1 + apply auto + done + then have *: "?I a x - ?I a y = ?I y x" + unfolding algebra_simps + apply (subst eq_commute) + apply (rule integral_combine) + using True using assms(2) goal1 + apply auto + done + have **: "norm (y - x) = content {y..x}" + apply (subst content_real) + using True + unfolding not_less + apply auto + done + have ***: "\fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)" + unfolding scaleR_left.diff by auto + show ?thesis + apply (subst ***) + unfolding norm_minus_cancel ** + apply (rule has_integral_bound[where f="(\u. f u - f x)"]) + unfolding * + unfolding o_def + defer + apply (rule has_integral_sub) + apply (subst minus_minus[symmetric]) + unfolding minus_minus + apply (rule integrable_integral) + apply (rule integrable_subinterval,rule integrable_continuous) + apply (rule assms)+ + proof - + show "{y..x} \ {a..b}" + using goal1 assms(2) by auto + have *: "x - y = norm (y - x)" + using True by auto + show "((\xa. f x) has_integral (x - y) *\<^sub>R f x) {y..x}" + apply (subst *) + unfolding ** + apply auto + done + show "\xa\{y..x}. norm (f xa - f x) \ e" + apply safe + apply (rule less_imp_le) + apply (rule d(2)[unfolded dist_norm]) + using assms(2) + using goal1 + apply auto + done + qed (insert e, auto) + qed + qed +qed + +lemma antiderivative_continuous: + fixes q b :: real + assumes "continuous_on {a..b} f" + obtains g where "\x\ {a..b}. (g has_vector_derivative (f x::_::banach)) (at x within {a..b})" + apply (rule that) + apply rule + using integral_has_vector_derivative[OF assms] + apply auto + done + subsection {* Combined fundamental theorem of calculus. *} -lemma antiderivative_integral_continuous: fixes f::"real \ 'a::banach" assumes "continuous_on {a..b} f" +lemma antiderivative_integral_continuous: + fixes f :: "real \ 'a::banach" + assumes "continuous_on {a..b} f" obtains g where "\u\{a..b}. \v \ {a..b}. u \ v \ (f has_integral (g v - g u)) {u..v}" -proof- from antiderivative_continuous[OF assms] guess g . note g=this - show ?thesis apply(rule that[of g]) - proof safe case goal1 have "\x\{u..v}. (g has_vector_derivative f x) (at x within {u..v})" - apply(rule,rule has_vector_derivative_within_subset) apply(rule g[rule_format]) using goal1(1-2) by auto - thus ?case using fundamental_theorem_of_calculus[OF goal1(3),of "g" "f"] by auto qed qed +proof - + from antiderivative_continuous[OF assms] guess g . note g=this + show ?thesis + apply (rule that[of g]) + proof safe + case goal1 + have "\x\{u..v}. (g has_vector_derivative f x) (at x within {u..v})" + apply rule + apply (rule has_vector_derivative_within_subset) + apply (rule g[rule_format]) + using goal1(1-2) + apply auto + done + then show ?case + using fundamental_theorem_of_calculus[OF goal1(3),of "g" "f"] by auto + qed +qed + subsection {* General "twiddling" for interval-to-interval function image. *} lemma has_integral_twiddle: - assumes "0 < r" "\x. h(g x) = x" "\x. g(h x) = x" "\x. continuous (at x) g" - "\u v. \w z. g ` {u..v} = {w..z}" - "\u v. \w z. h ` {u..v} = {w..z}" - "\u v. content(g ` {u..v}) = r * content {u..v}" - "(f has_integral i) {a..b}" + assumes "0 < r" + and "\x. h(g x) = x" + and "\x. g(h x) = x" + and "\x. continuous (at x) g" + and "\u v. \w z. g ` {u..v} = {w..z}" + and "\u v. \w z. h ` {u..v} = {w..z}" + and "\u v. content(g ` {u..v}) = r * content {u..v}" + and "(f has_integral i) {a..b}" shows "((\x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` {a..b})" -proof- { presume *:"{a..b} \ {} \ ?thesis" - show ?thesis apply cases defer apply(rule *,assumption) - proof- case goal1 thus ?thesis unfolding goal1 assms(8)[unfolded goal1 has_integral_empty_eq] by auto qed } - assume "{a..b} \ {}" from assms(6)[rule_format,of a b] guess w z apply-by(erule exE)+ note wz=this - have inj:"inj g" "inj h" unfolding inj_on_def apply safe apply(rule_tac[!] ccontr) - using assms(2) apply(erule_tac x=x in allE) using assms(2) apply(erule_tac x=y in allE) defer - using assms(3) apply(erule_tac x=x in allE) using assms(3) apply(erule_tac x=y in allE) by auto - show ?thesis unfolding has_integral_def has_integral_compact_interval_def apply(subst if_P) apply(rule,rule,rule wz) - proof safe fix e::real assume e:"e>0" hence "e * r > 0" using assms(1) by(rule mult_pos_pos) - from assms(8)[unfolded has_integral,rule_format,OF this] guess d apply-by(erule exE conjE)+ note d=this[rule_format] - def d' \ "\x. {y. g y \ d (g x)}" have d':"\x. d' x = {y. g y \ (d (g x))}" unfolding d'_def .. +proof - + { + presume *: "{a..b} \ {} \ ?thesis" + show ?thesis + apply cases + defer + apply (rule *) + apply assumption + proof - + case goal1 + then show ?thesis + unfolding goal1 assms(8)[unfolded goal1 has_integral_empty_eq] by auto qed + } + assume "{a..b} \ {}" + from assms(6)[rule_format,of a b] guess w z by (elim exE) note wz=this + have inj: "inj g" "inj h" + unfolding inj_on_def + apply safe + apply(rule_tac[!] ccontr) + using assms(2) + apply(erule_tac x=x in allE) + using assms(2) + apply(erule_tac x=y in allE) + defer + using assms(3) + apply (erule_tac x=x in allE) + using assms(3) + apply(erule_tac x=y in allE) + apply auto + done + show ?thesis + unfolding has_integral_def has_integral_compact_interval_def + apply (subst if_P) + apply rule + apply rule + apply (rule wz) + proof safe + fix e :: real + assume e: "e > 0" + then have "e * r > 0" + using assms(1) by (rule mult_pos_pos) + from assms(8)[unfolded has_integral,rule_format,OF this] guess d by (elim exE conjE) note d=this[rule_format] + def d' \ "\x. {y. g y \ d (g x)}" + have d': "\x. d' x = {y. g y \ (d (g x))}" + unfolding d'_def .. show "\d. gauge d \ (\p. p tagged_division_of h ` {a..b} \ d fine p \ norm ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)" - proof(rule_tac x=d' in exI,safe) show "gauge d'" using d(1) unfolding gauge_def d' using continuous_open_preimage_univ[OF assms(4)] by auto - fix p assume as:"p tagged_division_of h ` {a..b}" "d' fine p" note p = tagged_division_ofD[OF as(1)] - have "(\(x, k). (g x, g ` k)) ` p tagged_division_of {a..b} \ d fine (\(x, k). (g x, g ` k)) ` p" unfolding tagged_division_of - proof safe show "finite ((\(x, k). (g x, g ` k)) ` p)" using as by auto - show "d fine (\(x, k). (g x, g ` k)) ` p" using as(2) unfolding fine_def d' by auto - fix x k assume xk[intro]:"(x,k) \ p" show "g x \ g ` k" using p(2)[OF xk] by auto - show "\u v. g ` k = {u..v}" using p(4)[OF xk] using assms(5-6) by auto - { fix y assume "y \ k" thus "g y \ {a..b}" "g y \ {a..b}" using p(3)[OF xk,unfolded subset_eq,rule_format,of "h (g y)"] - using assms(2)[rule_format,of y] unfolding inj_image_mem_iff[OF inj(2)] by auto } - fix x' k' assume xk':"(x',k') \ p" fix z assume "z \ interior (g ` k)" "z \ interior (g ` k')" - hence *:"interior (g ` k) \ interior (g ` k') \ {}" by auto - have same:"(x, k) = (x', k')" apply-apply(rule ccontr,drule p(5)[OF xk xk']) - proof- assume as:"interior k \ interior k' = {}" from nonempty_witness[OF *] guess z . - hence "z \ g ` (interior k \ interior k')" using interior_image_subset[OF assms(4) inj(1)] - unfolding image_Int[OF inj(1)] by auto thus False using as by blast - qed thus "g x = g x'" by auto - { fix z assume "z \ k" thus "g z \ g ` k'" using same by auto } - { fix z assume "z \ k'" thus "g z \ g ` k" using same by auto } - next fix x assume "x \ {a..b}" hence "h x \ \{k. \x. (x, k) \ p}" using p(6) by auto - then guess X unfolding Union_iff .. note X=this from this(1) guess y unfolding mem_Collect_eq .. - thus "x \ \{k. \x. (x, k) \ (\(x, k). (g x, g ` k)) ` p}" apply- - apply(rule_tac X="g ` X" in UnionI) defer apply(rule_tac x="h x" in image_eqI) - using X(2) assms(3)[rule_format,of x] by auto - qed note ** = d(2)[OF this] have *:"inj_on (\(x, k). (g x, g ` k)) p" using inj(1) unfolding inj_on_def by fastforce - have "(\(x, k)\(\(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\(x, k)\p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding algebra_simps add_left_cancel - unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv - apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto - also have "... = r *\<^sub>R ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR_diff_right scaleR_scaleR - using assms(1) by auto finally have *:"?l = ?r" . - show "norm ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" using ** unfolding * unfolding norm_scaleR - using assms(1) by(auto simp add:field_simps) qed qed qed + proof (rule_tac x=d' in exI, safe) + show "gauge d'" + using d(1) + unfolding gauge_def d' + using continuous_open_preimage_univ[OF assms(4)] + by auto + fix p + assume as: "p tagged_division_of h ` {a..b}" "d' fine p" + note p = tagged_division_ofD[OF as(1)] + have "(\(x, k). (g x, g ` k)) ` p tagged_division_of {a..b} \ d fine (\(x, k). (g x, g ` k)) ` p" + unfolding tagged_division_of + proof safe + show "finite ((\(x, k). (g x, g ` k)) ` p)" + using as by auto + show "d fine (\(x, k). (g x, g ` k)) ` p" + using as(2) unfolding fine_def d' by auto + fix x k + assume xk[intro]: "(x, k) \ p" + show "g x \ g ` k" + using p(2)[OF xk] by auto + show "\u v. g ` k = {u..v}" + using p(4)[OF xk] using assms(5-6) by auto + { + fix y + assume "y \ k" + then show "g y \ {a..b}" "g y \ {a..b}" + using p(3)[OF xk,unfolded subset_eq,rule_format,of "h (g y)"] + using assms(2)[rule_format,of y] + unfolding inj_image_mem_iff[OF inj(2)] + by auto + } + fix x' k' + assume xk': "(x', k') \ p" + fix z + assume "z \ interior (g ` k)" and "z \ interior (g ` k')" + then have *: "interior (g ` k) \ interior (g ` k') \ {}" + by auto + have same: "(x, k) = (x', k')" + apply - + apply (rule ccontr,drule p(5)[OF xk xk']) + proof - + assume as: "interior k \ interior k' = {}" + from nonempty_witness[OF *] guess z . + then have "z \ g ` (interior k \ interior k')" + using interior_image_subset[OF assms(4) inj(1)] + unfolding image_Int[OF inj(1)] + by auto + then show False + using as by blast + qed + then show "g x = g x'" + by auto + { + fix z + assume "z \ k" + then show "g z \ g ` k'" + using same by auto + } + { + fix z + assume "z \ k'" + then show "g z \ g ` k" + using same by auto + } + next + fix x + assume "x \ {a..b}" + then have "h x \ \{k. \x. (x, k) \ p}" + using p(6) by auto + then guess X unfolding Union_iff .. note X=this + from this(1) guess y unfolding mem_Collect_eq .. + then show "x \ \{k. \x. (x, k) \ (\(x, k). (g x, g ` k)) ` p}" + apply - + apply (rule_tac X="g ` X" in UnionI) + defer + apply (rule_tac x="h x" in image_eqI) + using X(2) assms(3)[rule_format,of x] + apply auto + done + qed + note ** = d(2)[OF this] + have *: "inj_on (\(x, k). (g x, g ` k)) p" + using inj(1) unfolding inj_on_def by fastforce + have "(\(x, k)\(\(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\(x, k)\p. content k *\<^sub>R f (g x)) - i" (is "?l = _") + unfolding algebra_simps add_left_cancel + unfolding setsum_reindex[OF *] + apply (subst scaleR_right.setsum) + defer + apply (rule setsum_cong2) + unfolding o_def split_paired_all split_conv + apply (drule p(4)) + apply safe + unfolding assms(7)[rule_format] + using p + apply auto + done + also have "\ = r *\<^sub>R ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") + unfolding scaleR_diff_right scaleR_scaleR + using assms(1) + by auto + finally have *: "?l = ?r" . + show "norm ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" + using ** + unfolding * + unfolding norm_scaleR + using assms(1) + by (auto simp add:field_simps) + qed + qed +qed + subsection {* Special case of a basic affine transformation. *} -lemma interval_image_affinity_interval: shows "\u v. (\x. m *\<^sub>R (x::'a::ordered_euclidean_space) + c) ` {a..b} = {u..v}" - unfolding image_affinity_interval by auto - -lemma setprod_cong2: assumes "\x. x \ A \ f x = g x" shows "setprod f A = setprod g A" - apply(rule setprod_cong) using assms by auto +lemma interval_image_affinity_interval: + "\u v. (\x. m *\<^sub>R (x::'a::ordered_euclidean_space) + c) ` {a..b} = {u..v}" + unfolding image_affinity_interval + by auto + +lemma setprod_cong2: + assumes "\x. x \ A \ f x = g x" + shows "setprod f A = setprod g A" + apply (rule setprod_cong) + using assms + apply auto + done lemma content_image_affinity_interval: - "content((\x::'a::ordered_euclidean_space. m *\<^sub>R x + c) ` {a..b}) = (abs m) ^ DIM('a) * content {a..b}" (is "?l = ?r") -proof- { presume *:"{a..b}\{} \ ?thesis" show ?thesis apply(cases,rule *,assumption) - unfolding not_not using content_empty by auto } - assume as: "{a..b}\{}" + "content((\x::'a::ordered_euclidean_space. m *\<^sub>R x + c) ` {a..b}) = + abs m ^ DIM('a) * content {a..b}" (is "?l = ?r") +proof - + { + presume *: "{a..b} \ {} \ ?thesis" + show ?thesis + apply cases + apply (rule *) + apply assumption + unfolding not_not + using content_empty + apply auto + done + } + assume as: "{a..b} \ {}" show ?thesis proof (cases "m \ 0") case True @@ -6791,7 +7463,7 @@ by (simp add: inner_simps field_simps) ultimately show ?thesis by (simp add: image_affinity_interval True content_closed_interval' - setprod_timesf setprod_constant inner_diff_left) + setprod_timesf setprod_constant inner_diff_left) next case False with as have "{m *\<^sub>R b + c..m *\<^sub>R a + c} \ {}" @@ -6804,20 +7476,43 @@ by (simp add: inner_simps field_simps) ultimately show ?thesis using False by (simp add: image_affinity_interval content_closed_interval' - setprod_timesf[symmetric] setprod_constant[symmetric] inner_diff_left) + setprod_timesf[symmetric] setprod_constant[symmetric] inner_diff_left) qed qed -lemma has_integral_affinity: fixes a::"'a::ordered_euclidean_space" assumes "(f has_integral i) {a..b}" "m \ 0" +lemma has_integral_affinity: + fixes a :: "'a::ordered_euclidean_space" + assumes "(f has_integral i) {a..b}" + and "m \ 0" shows "((\x. f(m *\<^sub>R x + c)) has_integral ((1 / (abs(m) ^ DIM('a))) *\<^sub>R i)) ((\x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` {a..b})" - apply(rule has_integral_twiddle,safe) apply(rule zero_less_power) unfolding euclidean_eq_iff[where 'a='a] + apply (rule has_integral_twiddle) + apply safe + apply (rule zero_less_power) + unfolding euclidean_eq_iff[where 'a='a] unfolding scaleR_right_distrib inner_simps scaleR_scaleR - defer apply(insert assms(2), simp add:field_simps) apply(insert assms(2), simp add:field_simps) - apply(rule continuous_intros)+ apply(rule interval_image_affinity_interval)+ apply(rule content_image_affinity_interval) using assms by auto - -lemma integrable_affinity: assumes "f integrable_on {a..b}" "m \ 0" + defer + apply (insert assms(2)) + apply (simp add: field_simps) + apply (insert assms(2)) + apply (simp add: field_simps) + apply (rule continuous_intros)+ + apply (rule interval_image_affinity_interval)+ + apply (rule content_image_affinity_interval) + using assms + apply auto + done + +lemma integrable_affinity: + assumes "f integrable_on {a..b}" + and "m \ 0" shows "(\x. f(m *\<^sub>R x + c)) integrable_on ((\x. (1 / m) *\<^sub>R x + -((1/m) *\<^sub>R c)) ` {a..b})" - using assms unfolding integrable_on_def apply safe apply(drule has_integral_affinity) by auto + using assms + unfolding integrable_on_def + apply safe + apply (drule has_integral_affinity) + apply auto + done + subsection {* Special case of stretching coordinate axes separately. *} @@ -6856,310 +7551,744 @@ qed simp lemma interval_image_stretch_interval: - "\u v. (\x. \k\Basis. (m k * (x\k))*\<^sub>R k) ` {a..b::'a::ordered_euclidean_space} = {u..v::'a}" + "\u v. (\x. \k\Basis. (m k * (x\k))*\<^sub>R k) ` {a..b::'a::ordered_euclidean_space} = {u..v::'a}" unfolding image_stretch_interval by auto lemma content_image_stretch_interval: - "content((\x::'a::ordered_euclidean_space. (\k\Basis. (m k * (x\k))*\<^sub>R k)::'a) ` {a..b}) = abs(setprod m Basis) * content({a..b})" -proof(cases "{a..b} = {}") case True thus ?thesis + "content ((\x::'a::ordered_euclidean_space. (\k\Basis. (m k * (x\k))*\<^sub>R k)::'a) ` {a..b}) = + abs (setprod m Basis) * content {a..b}" +proof (cases "{a..b} = {}") + case True + then show ?thesis unfolding content_def image_is_empty image_stretch_interval if_P[OF True] by auto -next case False hence "(\x. (\k\Basis. (m k * (x\k))*\<^sub>R k)::'a) ` {a..b} \ {}" by auto - thus ?thesis using False unfolding content_def image_stretch_interval apply- unfolding interval_bounds' if_not_P - unfolding abs_setprod setprod_timesf[symmetric] apply(rule setprod_cong2) unfolding lessThan_iff - proof (simp only: inner_setsum_left_Basis) - fix i :: 'a assume i:"i\Basis" have "(m i < 0 \ m i > 0) \ m i = 0" by auto - thus "max (m i * (a \ i)) (m i * (b \ i)) - min (m i * (a \ i)) (m i * (b \ i)) = - \m i\ * (b \ i - a \ i)" - apply-apply(erule disjE)+ unfolding min_def max_def using False[unfolded interval_ne_empty,rule_format,of i] i - by(auto simp add:field_simps not_le mult_le_cancel_left_neg mult_le_cancel_left_pos) qed qed - -lemma has_integral_stretch: fixes f::"'a::ordered_euclidean_space => 'b::real_normed_vector" - assumes "(f has_integral i) {a..b}" "\k\Basis. ~(m k = 0)" +next + case False + then have "(\x. (\k\Basis. (m k * (x\k))*\<^sub>R k)) ` {a..b} \ {}" + by auto + then show ?thesis + using False + unfolding content_def image_stretch_interval + apply - + unfolding interval_bounds' if_not_P + unfolding abs_setprod setprod_timesf[symmetric] + apply (rule setprod_cong2) + unfolding lessThan_iff + apply (simp only: inner_setsum_left_Basis) + proof - + fix i :: 'a + assume i: "i \ Basis" + have "(m i < 0 \ m i > 0) \ m i = 0" + by auto + then show "max (m i * (a \ i)) (m i * (b \ i)) - min (m i * (a \ i)) (m i * (b \ i)) = + \m i\ * (b \ i - a \ i)" + apply - + apply (erule disjE)+ + unfolding min_def max_def + using False[unfolded interval_ne_empty,rule_format,of i] i + apply (auto simp add:field_simps not_le mult_le_cancel_left_neg mult_le_cancel_left_pos) + done + qed +qed + +lemma has_integral_stretch: + fixes f :: "'a::ordered_euclidean_space \ 'b::real_normed_vector" + assumes "(f has_integral i) {a..b}" + and "\k\Basis. m k \ 0" shows "((\x. f (\k\Basis. (m k * (x\k))*\<^sub>R k)) has_integral - ((1/(abs(setprod m Basis))) *\<^sub>R i)) ((\x. (\k\Basis. (1 / m k * (x\k))*\<^sub>R k)) ` {a..b})" - apply(rule has_integral_twiddle[where f=f]) unfolding zero_less_abs_iff content_image_stretch_interval - unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a] using assms -proof- show "\y::'a. continuous (at y) (\x. (\k\Basis. (m k * (x\k))*\<^sub>R k))" - apply(rule,rule linear_continuous_at) unfolding linear_linear - unfolding linear_def inner_simps euclidean_eq_iff[where 'a='a] by(auto simp add:field_simps) + ((1/(abs(setprod m Basis))) *\<^sub>R i)) ((\x. (\k\Basis. (1 / m k * (x\k))*\<^sub>R k)) ` {a..b})" + apply (rule has_integral_twiddle[where f=f]) + unfolding zero_less_abs_iff content_image_stretch_interval + unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a] + using assms +proof - + show "\y::'a. continuous (at y) (\x. (\k\Basis. (m k * (x\k))*\<^sub>R k))" + apply rule + apply (rule linear_continuous_at) + unfolding linear_linear + unfolding linear_def inner_simps euclidean_eq_iff[where 'a='a] + apply (auto simp add: field_simps) + done qed auto -lemma integrable_stretch: fixes f::"'a::ordered_euclidean_space => 'b::real_normed_vector" - assumes "f integrable_on {a..b}" "\k\Basis. ~(m k = 0)" - shows "(\x::'a. f (\k\Basis. (m k * (x\k))*\<^sub>R k)) integrable_on ((\x. \k\Basis. (1 / m k * (x\k))*\<^sub>R k) ` {a..b})" - using assms unfolding integrable_on_def apply-apply(erule exE) - apply(drule has_integral_stretch,assumption) by auto +lemma integrable_stretch: + fixes f :: "'a::ordered_euclidean_space \ 'b::real_normed_vector" + assumes "f integrable_on {a..b}" + and "\k\Basis. m k \ 0" + shows "(\x::'a. f (\k\Basis. (m k * (x\k))*\<^sub>R k)) integrable_on + ((\x. \k\Basis. (1 / m k * (x\k))*\<^sub>R k) ` {a..b})" + using assms + unfolding integrable_on_def + apply - + apply (erule exE) + apply (drule has_integral_stretch) + apply assumption + apply auto + done + subsection {* even more special cases. *} -lemma uminus_interval_vector[simp]:"uminus ` {a..b} = {-b .. -a::'a::ordered_euclidean_space}" - apply(rule set_eqI,rule) defer unfolding image_iff - apply(rule_tac x="-x" in bexI) by(auto simp add:minus_le_iff le_minus_iff eucl_le[where 'a='a]) - -lemma has_integral_reflect_lemma[intro]: assumes "(f has_integral i) {a..b}" - shows "((\x. f(-x)) has_integral i) {-b .. -a}" - using has_integral_affinity[OF assms, of "-1" 0] by auto - -lemma has_integral_reflect[simp]: "((\x. f(-x)) has_integral i) {-b..-a} \ (f has_integral i) ({a..b})" - apply rule apply(drule_tac[!] has_integral_reflect_lemma) by auto +lemma uminus_interval_vector[simp]: + fixes a b :: "'a::ordered_euclidean_space" + shows "uminus ` {a..b} = {-b..-a}" + apply (rule set_eqI) + apply rule + defer + unfolding image_iff + apply (rule_tac x="-x" in bexI) + apply (auto simp add:minus_le_iff le_minus_iff eucl_le[where 'a='a]) + done + +lemma has_integral_reflect_lemma[intro]: + assumes "(f has_integral i) {a..b}" + shows "((\x. f(-x)) has_integral i) {-b..-a}" + using has_integral_affinity[OF assms, of "-1" 0] + by auto + +lemma has_integral_reflect[simp]: + "((\x. f (-x)) has_integral i) {-b..-a} \ (f has_integral i) {a..b}" + apply rule + apply (drule_tac[!] has_integral_reflect_lemma) + apply auto + done lemma integrable_reflect[simp]: "(\x. f(-x)) integrable_on {-b..-a} \ f integrable_on {a..b}" unfolding integrable_on_def by auto -lemma integral_reflect[simp]: "integral {-b..-a} (\x. f(-x)) = integral ({a..b}) f" +lemma integral_reflect[simp]: "integral {-b..-a} (\x. f (-x)) = integral {a..b} f" unfolding integral_def by auto + subsection {* Stronger form of FCT; quite a tedious proof. *} -lemma bgauge_existence_lemma: "(\x\s. \d::real. 0 < d \ q d x) \ (\x. \d>0. x\s \ q d x)" by(meson zero_less_one) - -lemma additive_tagged_division_1': fixes f::"real \ 'a::real_normed_vector" - assumes "a \ b" "p tagged_division_of {a..b}" +lemma bgauge_existence_lemma: "(\x\s. \d::real. 0 < d \ q d x) \ (\x. \d>0. x\s \ q d x)" + by (meson zero_less_one) + +lemma additive_tagged_division_1': + fixes f :: "real \ 'a::real_normed_vector" + assumes "a \ b" + and "p tagged_division_of {a..b}" shows "setsum (\(x,k). f (interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a" - using additive_tagged_division_1[OF _ assms(2), of f] using assms(1) by auto - -lemma split_minus[simp]:"(\(x, k). f x k) x - (\(x, k). g x k) x = (\(x, k). f x k - g x k) x" - unfolding split_def by(rule refl) + using additive_tagged_division_1[OF _ assms(2), of f] + using assms(1) + by auto + +lemma split_minus[simp]: "(\(x, k). f x k) x - (\(x, k). g x k) x = (\(x, k). f x k - g x k) x" + by (simp add: split_def) lemma norm_triangle_le_sub: "norm x + norm y \ e \ norm (x - y) \ e" - apply(subst(asm)(2) norm_minus_cancel[symmetric]) - apply(drule norm_triangle_le) by(auto simp add:algebra_simps) - -lemma fundamental_theorem_of_calculus_interior: fixes f::"real => 'a::real_normed_vector" - assumes"a \ b" "continuous_on {a..b} f" "\x\{a<.. 'a::real_normed_vector" + assumes "a \ b" + and "continuous_on {a..b} f" + and "\x\{a<.. ?thesis" - show ?thesis proof(cases,rule *,assumption) - assume "\ a < b" hence "a = b" using assms(1) by auto - hence *:"{a .. b} = {b}" "f b - f a = 0" by(auto simp add: order_antisym) - show ?thesis unfolding *(2) apply(rule has_integral_null) unfolding content_eq_0 using * `a=b` +proof - + { + presume *: "a < b \ ?thesis" + show ?thesis + proof (cases "a < b") + case True + then show ?thesis by (rule *) + next + case False + then have "a = b" + using assms(1) by auto + then have *: "{a .. b} = {b}" "f b - f a = 0" + by (auto simp add: order_antisym) + show ?thesis + unfolding *(2) + apply (rule has_integral_null) + unfolding content_eq_0 + using * `a = b` by (auto simp: ex_in_conv) - qed } assume ab:"a < b" + qed + } + assume ab: "a < b" let ?P = "\e. \d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ - norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content {a..b})" - { presume "\e. e>0 \ ?P e" thus ?thesis unfolding has_integral_factor_content by auto } - fix e::real assume e:"e>0" + norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content {a..b})" + { presume "\e. e > 0 \ ?P e" then show ?thesis unfolding has_integral_factor_content by auto } + fix e :: real + assume e: "e > 0" note assms(3)[unfolded has_vector_derivative_def has_derivative_at_alt ball_conj_distrib] - note conjunctD2[OF this] note bounded=this(1) and this(2) - from this(2) have "\x\{a<..d>0. \y. norm (y - x) < d \ norm (f y - f x - (y - x) *\<^sub>R f' x) \ e/2 * norm (y - x)" - apply-apply safe apply(erule_tac x=x in ballE,erule_tac x="e/2" in allE) using e by auto note this[unfolded bgauge_existence_lemma] - from choice[OF this] guess d .. note conjunctD2[OF this[rule_format]] note d = this[rule_format] - have "bounded (f ` {a..b})" apply(rule compact_imp_bounded compact_continuous_image)+ using compact_interval assms by auto + note conjunctD2[OF this] + note bounded=this(1) and this(2) + from this(2) have "\x\{a<..d>0. \y. norm (y - x) < d \ + norm (f y - f x - (y - x) *\<^sub>R f' x) \ e/2 * norm (y - x)" + apply - + apply safe + apply (erule_tac x=x in ballE) + apply (erule_tac x="e/2" in allE) + using e + apply auto + done + note this[unfolded bgauge_existence_lemma] + from choice[OF this] guess d .. + note conjunctD2[OF this[rule_format]] + note d = this[rule_format] + have "bounded (f ` {a..b})" + apply (rule compact_imp_bounded compact_continuous_image)+ + using compact_interval assms + apply auto + done from this[unfolded bounded_pos] guess B .. note B = this[rule_format] - have "\da. 0 < da \ (\c. a \ c \ {a..c} \ {a..b} \ {a..c} \ ball a da - \ norm(content {a..c} *\<^sub>R f' a - (f c - f a)) \ (e * (b - a)) / 4)" - proof- have "a\{a..b}" using ab by auto + have "\da. 0 < da \ (\c. a \ c \ {a..c} \ {a..b} \ {a..c} \ ball a da \ + norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \ (e * (b - a)) / 4)" + proof - + have "a \ {a..b}" + using ab by auto note assms(2)[unfolded continuous_on_eq_continuous_within,rule_format,OF this] - note * = this[unfolded continuous_within Lim_within,rule_format] have "(e * (b - a)) / 8 > 0" using e ab by(auto simp add:field_simps) + note * = this[unfolded continuous_within Lim_within,rule_format] + have "(e * (b - a)) / 8 > 0" + using e ab by (auto simp add: field_simps) from *[OF this] guess k .. note k = conjunctD2[OF this,rule_format] have "\l. 0 < l \ norm(l *\<^sub>R f' a) \ (e * (b - a)) / 8" - proof(cases "f' a = 0") case True - thus ?thesis apply(rule_tac x=1 in exI) using ab e by(auto intro!:mult_nonneg_nonneg) - next case False thus ?thesis - apply(rule_tac x="(e * (b - a)) / 8 / norm (f' a)" in exI) using ab e by(auto simp add:field_simps) - qed then guess l .. note l = conjunctD2[OF this] - show ?thesis apply(rule_tac x="min k l" in exI) apply safe unfolding min_less_iff_conj apply(rule,(rule l k)+) - proof- fix c assume as:"a \ c" "{a..c} \ {a..b}" "{a..c} \ ball a (min k l)" + proof (cases "f' a = 0") + case True + then show ?thesis + apply (rule_tac x=1 in exI) + using ab e + apply (auto intro!:mult_nonneg_nonneg) + done + next + case False + then show ?thesis + apply (rule_tac x="(e * (b - a)) / 8 / norm (f' a)" in exI) + using ab e + apply (auto simp add: field_simps) + done + qed + then guess l .. note l = conjunctD2[OF this] + show ?thesis + apply (rule_tac x="min k l" in exI) + apply safe + unfolding min_less_iff_conj + apply rule + apply (rule l k)+ + proof - + fix c + assume as: "a \ c" "{a..c} \ {a..b}" "{a..c} \ ball a (min k l)" note as' = this[unfolded subset_eq Ball_def mem_ball dist_real_def mem_interval] - have "norm ((c - a) *\<^sub>R f' a - (f c - f a)) \ norm ((c - a) *\<^sub>R f' a) + norm (f c - f a)" by(rule norm_triangle_ineq4) - also have "... \ e * (b - a) / 8 + e * (b - a) / 8" - proof(rule add_mono) case goal1 have "\c - a\ \ \l\" using as' by auto - thus ?case apply-apply(rule order_trans[OF _ l(2)]) unfolding norm_scaleR apply(rule mult_right_mono) by auto - next case goal2 show ?case apply(rule less_imp_le) apply(cases "a = c") defer - apply(rule k(2)[unfolded dist_norm]) using as' e ab by(auto simp add:field_simps) - qed finally show "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \ e * (b - a) / 4" + have "norm ((c - a) *\<^sub>R f' a - (f c - f a)) \ norm ((c - a) *\<^sub>R f' a) + norm (f c - f a)" + by (rule norm_triangle_ineq4) + also have "\ \ e * (b - a) / 8 + e * (b - a) / 8" + proof (rule add_mono) + case goal1 + have "\c - a\ \ \l\" + using as' by auto + then show ?case + apply - + apply (rule order_trans[OF _ l(2)]) + unfolding norm_scaleR + apply (rule mult_right_mono) + apply auto + done + next + case goal2 + show ?case + apply (rule less_imp_le) + apply (cases "a = c") + defer + apply (rule k(2)[unfolded dist_norm]) + using as' e ab + apply (auto simp add: field_simps) + done + qed + finally show "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \ e * (b - a) / 4" unfolding content_real[OF as(1)] by auto - qed qed then guess da .. note da=conjunctD2[OF this,rule_format] + qed + qed + then guess da .. note da=conjunctD2[OF this,rule_format] have "\db>0. \c\b. {c..b} \ {a..b} \ {c..b} \ ball b db \ - norm(content {c..b} *\<^sub>R f' b - (f b - f c)) \ (e * (b - a)) / 4" - proof- have "b\{a..b}" using ab by auto + norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \ (e * (b - a)) / 4" + proof - + have "b \ {a..b}" + using ab by auto note assms(2)[unfolded continuous_on_eq_continuous_within,rule_format,OF this] note * = this[unfolded continuous_within Lim_within,rule_format] have "(e * (b - a)) / 8 > 0" - using e ab by(auto simp add:field_simps) + using e ab by (auto simp add: field_simps) from *[OF this] guess k .. note k = conjunctD2[OF this,rule_format] - have "\l. 0 < l \ norm(l *\<^sub>R f' b) \ (e * (b - a)) / 8" - proof(cases "f' b = 0") case True - thus ?thesis apply(rule_tac x=1 in exI) using ab e by(auto intro!:mult_nonneg_nonneg) - next case False thus ?thesis - apply(rule_tac x="(e * (b - a)) / 8 / norm (f' b)" in exI) - using ab e by(auto simp add:field_simps) - qed then guess l .. note l = conjunctD2[OF this] - show ?thesis apply(rule_tac x="min k l" in exI) apply safe unfolding min_less_iff_conj apply(rule,(rule l k)+) - proof- fix c assume as:"c \ b" "{c..b} \ {a..b}" "{c..b} \ ball b (min k l)" + have "\l. 0 < l \ norm (l *\<^sub>R f' b) \ (e * (b - a)) / 8" + proof (cases "f' b = 0") + case True + then show ?thesis + apply (rule_tac x=1 in exI) + using ab e + apply (auto intro!: mult_nonneg_nonneg) + done + next + case False + then show ?thesis + apply (rule_tac x="(e * (b - a)) / 8 / norm (f' b)" in exI) + using ab e + apply (auto simp add: field_simps) + done + qed + then guess l .. note l = conjunctD2[OF this] + show ?thesis + apply (rule_tac x="min k l" in exI) + apply safe + unfolding min_less_iff_conj + apply rule + apply (rule l k)+ + proof - + fix c + assume as: "c \ b" "{c..b} \ {a..b}" "{c..b} \ ball b (min k l)" note as' = this[unfolded subset_eq Ball_def mem_ball dist_real_def mem_interval] - have "norm ((b - c) *\<^sub>R f' b - (f b - f c)) \ norm ((b - c) *\<^sub>R f' b) + norm (f b - f c)" by(rule norm_triangle_ineq4) - also have "... \ e * (b - a) / 8 + e * (b - a) / 8" - proof(rule add_mono) case goal1 have "\c - b\ \ \l\" using as' by auto - thus ?case apply-apply(rule order_trans[OF _ l(2)]) unfolding norm_scaleR apply(rule mult_right_mono) by auto - next case goal2 show ?case apply(rule less_imp_le) apply(cases "b = c") defer apply(subst norm_minus_commute) - apply(rule k(2)[unfolded dist_norm]) using as' e ab by(auto simp add:field_simps) - qed finally show "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \ e * (b - a) / 4" + have "norm ((b - c) *\<^sub>R f' b - (f b - f c)) \ norm ((b - c) *\<^sub>R f' b) + norm (f b - f c)" + by (rule norm_triangle_ineq4) + also have "\ \ e * (b - a) / 8 + e * (b - a) / 8" + proof (rule add_mono) + case goal1 + have "\c - b\ \ \l\" + using as' by auto + then show ?case + apply - + apply (rule order_trans[OF _ l(2)]) + unfolding norm_scaleR + apply (rule mult_right_mono) + apply auto + done + next + case goal2 + show ?case + apply (rule less_imp_le) + apply (cases "b = c") + defer + apply (subst norm_minus_commute) + apply (rule k(2)[unfolded dist_norm]) + using as' e ab + apply (auto simp add: field_simps) + done + qed + finally show "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \ e * (b - a) / 4" unfolding content_real[OF as(1)] by auto - qed qed then guess db .. note db=conjunctD2[OF this,rule_format] + qed + qed + then guess db .. note db=conjunctD2[OF this,rule_format] let ?d = "(\x. ball x (if x=a then da else if x=b then db else d x))" - show "?P e" apply(rule_tac x="?d" in exI) - proof safe case goal1 show ?case apply(rule gauge_ball_dependent) using ab db(1) da(1) d(1) by auto - next case goal2 note as=this let ?A = "{t. fst t \ {a, b}}" note p = tagged_division_ofD[OF goal2(1)] - have pA:"p = (p \ ?A) \ (p - ?A)" "finite (p \ ?A)" "finite (p - ?A)" "(p \ ?A) \ (p - ?A) = {}" using goal2 by auto + show "?P e" + apply (rule_tac x="?d" in exI) + proof safe + case goal1 + show ?case + apply (rule gauge_ball_dependent) + using ab db(1) da(1) d(1) + apply auto + done + next + case goal2 + note as=this + let ?A = "{t. fst t \ {a, b}}" + note p = tagged_division_ofD[OF goal2(1)] + have pA: "p = (p \ ?A) \ (p - ?A)" "finite (p \ ?A)" "finite (p - ?A)" "(p \ ?A) \ (p - ?A) = {}" + using goal2 by auto note * = additive_tagged_division_1'[OF assms(1) goal2(1), symmetric] - have **:"\n1 s1 n2 s2::real. n2 \ s2 / 2 \ n1 - s1 \ s2 / 2 \ n1 + n2 \ s1 + s2" by arith - show ?case unfolding content_real[OF assms(1)] and *[of "\x. x"] *[of f] setsum_subtractf[symmetric] split_minus - unfolding setsum_right_distrib apply(subst(2) pA,subst pA) unfolding setsum_Un_disjoint[OF pA(2-)] - proof(rule norm_triangle_le,rule **) - case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst setsum_divide_distrib) - proof(rule order_refl,safe,unfold not_le o_def split_conv fst_conv,rule ccontr) fix x k assume as:"(x,k) \ p" - "e * (interval_upperbound k - interval_lowerbound k) / 2 - < norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k)))" - from p(4)[OF this(1)] guess u v apply-by(erule exE)+ note k=this - hence "u \ v" and uv:"{u,v}\{u..v}" using p(2)[OF as(1)] by auto + have **: "\n1 s1 n2 s2::real. n2 \ s2 / 2 \ n1 - s1 \ s2 / 2 \ n1 + n2 \ s1 + s2" + by arith + show ?case + unfolding content_real[OF assms(1)] and *[of "\x. x"] *[of f] setsum_subtractf[symmetric] split_minus + unfolding setsum_right_distrib + apply (subst(2) pA) + apply (subst pA) + unfolding setsum_Un_disjoint[OF pA(2-)] + proof (rule norm_triangle_le, rule **) + case goal1 + show ?case + apply (rule order_trans) + apply (rule setsum_norm_le) + defer + apply (subst setsum_divide_distrib) + apply (rule order_refl) + apply safe + apply (unfold not_le o_def split_conv fst_conv) + proof (rule ccontr) + fix x k + assume as: "(x, k) \ p" + "e * (interval_upperbound k - interval_lowerbound k) / 2 < + norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k)))" + from p(4)[OF this(1)] guess u v by (elim exE) note k=this + then have "u \ v" and uv: "{u, v} \ {u..v}" + using p(2)[OF as(1)] by auto note result = as(2)[unfolded k interval_bounds_real[OF this(1)] content_real[OF this(1)]] - assume as':"x \ a" "x \ b" hence "x \ {a<.. a" "x \ b" + then have "x \ {a<..R f' (x) - (f (v) - f (u))) = norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))" - apply(rule arg_cong[of _ _ norm]) unfolding scaleR_left.diff by auto - also have "... \ e / 2 * norm (u - x) + e / 2 * norm (v - x)" apply(rule norm_triangle_le_sub) - apply(rule add_mono) apply(rule_tac[!] *) using fineD[OF goal2(2) as(1)] as' unfolding k subset_eq - apply- apply(erule_tac x=u in ballE,erule_tac[3] x=v in ballE) using uv by(auto simp:dist_real_def) - also have "... \ e / 2 * norm (v - u)" using p(2)[OF as(1)] unfolding k by(auto simp add:field_simps) + apply (rule arg_cong[of _ _ norm]) + unfolding scaleR_left.diff + apply auto + done + also have "\ \ e / 2 * norm (u - x) + e / 2 * norm (v - x)" + apply (rule norm_triangle_le_sub) + apply (rule add_mono) + apply (rule_tac[!] *) + using fineD[OF goal2(2) as(1)] as' + unfolding k subset_eq + apply - + apply (erule_tac x=u in ballE) + apply (erule_tac[3] x=v in ballE) + using uv + apply (auto simp:dist_real_def) + done + also have "\ \ e / 2 * norm (v - u)" + using p(2)[OF as(1)] + unfolding k + by (auto simp add: field_simps) finally have "e * (v - u) / 2 < e * (v - u) / 2" - apply- apply(rule less_le_trans[OF result]) using uv by auto thus False by auto qed - - next have *:"\x s1 s2::real. 0 \ s1 \ x \ (s1 + s2) / 2 \ x - s1 \ s2 / 2" by auto - case goal2 show ?case apply(rule *) apply(rule setsum_nonneg) apply(rule,unfold split_paired_all split_conv) - defer unfolding setsum_Un_disjoint[OF pA(2-),symmetric] pA(1)[symmetric] unfolding setsum_right_distrib[symmetric] - apply(subst additive_tagged_division_1[OF _ as(1)]) apply(rule assms) - proof- fix x k assume "(x,k) \ p \ {t. fst t \ {a, b}}" note xk=IntD1[OF this] - from p(4)[OF this] guess u v apply-by(erule exE)+ note uv=this - with p(2)[OF xk] have "{u..v} \ {}" by auto - thus "0 \ e * ((interval_upperbound k) - (interval_lowerbound k))" - unfolding uv using e by(auto simp add:field_simps) - next have *:"\s f t e. setsum f s = setsum f t \ norm(setsum f t) \ e \ norm(setsum f s) \ e" by auto + apply - + apply (rule less_le_trans[OF result]) + using uv + apply auto + done + then show False by auto + qed + next + have *: "\x s1 s2::real. 0 \ s1 \ x \ (s1 + s2) / 2 \ x - s1 \ s2 / 2" + by auto + case goal2 + show ?case + apply (rule *) + apply (rule setsum_nonneg) + apply rule + apply (unfold split_paired_all split_conv) + defer + unfolding setsum_Un_disjoint[OF pA(2-),symmetric] pA(1)[symmetric] + unfolding setsum_right_distrib[symmetric] + apply (subst additive_tagged_division_1[OF _ as(1)]) + apply (rule assms) + proof - + fix x k + assume "(x, k) \ p \ {t. fst t \ {a, b}}" + note xk=IntD1[OF this] + from p(4)[OF this] guess u v by (elim exE) note uv=this + with p(2)[OF xk] have "{u..v} \ {}" + by auto + then show "0 \ e * ((interval_upperbound k) - (interval_lowerbound k))" + unfolding uv using e by (auto simp add: field_simps) + next + have *: "\s f t e. setsum f s = setsum f t \ norm (setsum f t) \ e \ norm (setsum f s) \ e" + by auto show "norm (\(x, k)\p \ ?A. content k *\<^sub>R f' x - (f ((interval_upperbound k)) - f ((interval_lowerbound k)))) \ e * (b - a) / 2" - apply(rule *[where t="p \ {t. fst t \ {a, b} \ content(snd t) \ 0}"]) - apply(rule setsum_mono_zero_right[OF pA(2)]) defer apply(rule) unfolding split_paired_all split_conv o_def - proof- fix x k assume "(x,k) \ p \ {t. fst t \ {a, b}} - p \ {t. fst t \ {a, b} \ content (snd t) \ 0}" - hence xk:"(x,k)\p" "content k = 0" by auto from p(4)[OF xk(1)] guess u v apply-by(erule exE)+ note uv=this - have "k\{}" using p(2)[OF xk(1)] by auto hence *:"u = v" using xk - unfolding uv content_eq_0 interval_eq_empty by auto - thus "content k *\<^sub>R (f' (x)) - (f ((interval_upperbound k)) - f ((interval_lowerbound k))) = 0" using xk unfolding uv by auto - next have *:"p \ {t. fst t \ {a, b} \ content(snd t) \ 0} = - {t. t\p \ fst t = a \ content(snd t) \ 0} \ {t. t\p \ fst t = b \ content(snd t) \ 0}" by blast - have **:"\s f. \e::real. (\x y. x \ s \ y \ s \ x = y) \ (\x. x \ s \ norm(f x) \ e) - \ e>0 \ norm(setsum f s) \ e" - proof(case_tac "s={}") case goal2 then obtain x where "x\s" by auto hence *:"s = {x}" using goal2(1) by auto - thus ?case using `x\s` goal2(2) by auto + apply (rule *[where t="p \ {t. fst t \ {a, b} \ content(snd t) \ 0}"]) + apply (rule setsum_mono_zero_right[OF pA(2)]) + defer + apply rule + unfolding split_paired_all split_conv o_def + proof - + fix x k + assume "(x, k) \ p \ {t. fst t \ {a, b}} - p \ {t. fst t \ {a, b} \ content (snd t) \ 0}" + then have xk: "(x, k) \ p" "content k = 0" + by auto + from p(4)[OF xk(1)] guess u v by (elim exE) note uv=this + have "k \ {}" + using p(2)[OF xk(1)] by auto + then have *: "u = v" + using xk + unfolding uv content_eq_0 interval_eq_empty + by auto + then show "content k *\<^sub>R (f' (x)) - (f ((interval_upperbound k)) - f ((interval_lowerbound k))) = 0" + using xk unfolding uv by auto + next + have *: "p \ {t. fst t \ {a, b} \ content(snd t) \ 0} = + {t. t\p \ fst t = a \ content(snd t) \ 0} \ {t. t\p \ fst t = b \ content(snd t) \ 0}" + by blast + have **: "\s f. \e::real. (\x y. x \ s \ y \ s \ x = y) \ + (\x. x \ s \ norm (f x) \ e) \ e > 0 \ norm (setsum f s) \ e" + proof (case_tac "s = {}") + case goal2 + then obtain x where "x \ s" + by auto + then have *: "s = {x}" + using goal2(1) by auto + then show ?case + using `x \ s` goal2(2) by auto qed auto - case goal2 show ?case apply(subst *, subst setsum_Un_disjoint) prefer 4 - apply(rule order_trans[of _ "e * (b - a)/4 + e * (b - a)/4"]) - apply(rule norm_triangle_le,rule add_mono) apply(rule_tac[1-2] **) - proof- let ?B = "\x. {t \ p. fst t = x \ content (snd t) \ 0}" - have pa:"\k. (a, k) \ p \ \v. k = {a .. v} \ a \ v" - proof- case goal1 guess u v using p(4)[OF goal1] apply-by(erule exE)+ note uv=this - have *:"u \ v" using p(2)[OF goal1] unfolding uv by auto - have u:"u = a" proof(rule ccontr) have "u \ {u..v}" using p(2-3)[OF goal1(1)] unfolding uv by auto - have "u \ a" using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto moreover assume "u\a" ultimately - have "u > a" by auto - thus False using p(2)[OF goal1(1)] unfolding uv by(auto simp add:) - qed thus ?case apply(rule_tac x=v in exI) unfolding uv using * by auto + case goal2 + show ?case + apply (subst *) + apply (subst setsum_Un_disjoint) + prefer 4 + apply (rule order_trans[of _ "e * (b - a)/4 + e * (b - a)/4"]) + apply (rule norm_triangle_le,rule add_mono) + apply (rule_tac[1-2] **) + proof - + let ?B = "\x. {t \ p. fst t = x \ content (snd t) \ 0}" + have pa: "\k. (a, k) \ p \ \v. k = {a .. v} \ a \ v" + proof - + case goal1 + guess u v using p(4)[OF goal1] by (elim exE) note uv=this + have *: "u \ v" + using p(2)[OF goal1] unfolding uv by auto + have u: "u = a" + proof (rule ccontr) + have "u \ {u..v}" + using p(2-3)[OF goal1(1)] unfolding uv by auto + have "u \ a" + using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto + moreover assume "u \ a" + ultimately have "u > a" by auto + then show False + using p(2)[OF goal1(1)] unfolding uv by (auto simp add:) + qed + then show ?case + apply (rule_tac x=v in exI) + unfolding uv + using * + apply auto + done qed - have pb:"\k. (b, k) \ p \ \v. k = {v .. b} \ b \ v" - proof- case goal1 guess u v using p(4)[OF goal1] apply-by(erule exE)+ note uv=this - have *:"u \ v" using p(2)[OF goal1] unfolding uv by auto - have u:"v = b" proof(rule ccontr) have "u \ {u..v}" using p(2-3)[OF goal1(1)] unfolding uv by auto - have "v \ b" using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto moreover assume "v\ b" ultimately - have "v < b" by auto - thus False using p(2)[OF goal1(1)] unfolding uv by(auto simp add:) - qed thus ?case apply(rule_tac x=u in exI) unfolding uv using * by auto + have pb: "\k. (b, k) \ p \ \v. k = {v .. b} \ b \ v" + proof - + case goal1 + guess u v using p(4)[OF goal1] by (elim exE) note uv=this + have *: "u \ v" + using p(2)[OF goal1] unfolding uv by auto + have u: "v = b" + proof (rule ccontr) + have "u \ {u..v}" + using p(2-3)[OF goal1(1)] unfolding uv by auto + have "v \ b" + using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto + moreover assume "v \ b" + ultimately have "v < b" by auto + then show False + using p(2)[OF goal1(1)] unfolding uv by (auto simp add:) + qed + then show ?case + apply (rule_tac x=u in exI) + unfolding uv + using * + apply auto + done qed - - show "\x y. x \ ?B a \ y \ ?B a \ x = y" apply(rule,rule,rule,unfold split_paired_all) - unfolding mem_Collect_eq fst_conv snd_conv apply safe - proof- fix x k k' assume k:"( a, k) \ p" "( a, k') \ p" "content k \ 0" "content k' \ 0" + show "\x y. x \ ?B a \ y \ ?B a \ x = y" + apply (rule,rule,rule,unfold split_paired_all) + unfolding mem_Collect_eq fst_conv snd_conv + apply safe + proof - + fix x k k' + assume k: "(a, k) \ p" "(a, k') \ p" "content k \ 0" "content k' \ 0" guess v using pa[OF k(1)] .. note v = conjunctD2[OF this] - guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (min (v) (v'))" - have "{ a <..< ?v} \ k \ k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter] - moreover have " ((a + ?v)/2) \ { a <..< ?v}" using k(3-) - unfolding v v' content_eq_0 not_le by(auto simp add:not_le) - ultimately have " ((a + ?v)/2) \ interior k \ interior k'" unfolding interior_open[OF open_interval] by auto - hence *:"k = k'" apply- apply(rule ccontr) using p(5)[OF k(1-2)] by auto - { assume "x\k" thus "x\k'" unfolding * . } { assume "x\k'" thus "x\k" unfolding * . } + guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'" + have "{a <..< ?v} \ k \ k'" + unfolding v v' by (auto simp add:) + note interior_mono[OF this,unfolded interior_inter] + moreover have "(a + ?v)/2 \ { a <..< ?v}" + using k(3-) + unfolding v v' content_eq_0 not_le + by (auto simp add: not_le) + ultimately have "(a + ?v)/2 \ interior k \ interior k'" + unfolding interior_open[OF open_interval] by auto + then have *: "k = k'" + apply - + apply (rule ccontr) + using p(5)[OF k(1-2)] + apply auto + done + { assume "x \ k" then show "x \ k'" unfolding * . } + { assume "x \ k'" then show "x\k" unfolding * . } qed - show "\x y. x \ ?B b \ y \ ?B b \ x = y" apply(rule,rule,rule,unfold split_paired_all) - unfolding mem_Collect_eq fst_conv snd_conv apply safe - proof- fix x k k' assume k:"( b, k) \ p" "( b, k') \ p" "content k \ 0" "content k' \ 0" + show "\x y. x \ ?B b \ y \ ?B b \ x = y" + apply rule + apply rule + apply rule + apply (unfold split_paired_all) + unfolding mem_Collect_eq fst_conv snd_conv + apply safe + proof - + fix x k k' + assume k: "(b, k) \ p" "(b, k') \ p" "content k \ 0" "content k' \ 0" guess v using pb[OF k(1)] .. note v = conjunctD2[OF this] - guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (max (v) (v'))" - have "{?v <..< b} \ k \ k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter] - moreover have " ((b + ?v)/2) \ {?v <..< b}" using k(3-) unfolding v v' content_eq_0 not_le by auto - ultimately have " ((b + ?v)/2) \ interior k \ interior k'" unfolding interior_open[OF open_interval] by auto - hence *:"k = k'" apply- apply(rule ccontr) using p(5)[OF k(1-2)] by auto - { assume "x\k" thus "x\k'" unfolding * . } { assume "x\k'" thus "x\k" unfolding * . } + guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this] + let ?v = "max v v'" + have "{?v <..< b} \ k \ k'" + unfolding v v' by auto + note interior_mono[OF this,unfolded interior_inter] + moreover have " ((b + ?v)/2) \ {?v <..< b}" + using k(3-) unfolding v v' content_eq_0 not_le by auto + ultimately have " ((b + ?v)/2) \ interior k \ interior k'" + unfolding interior_open[OF open_interval] by auto + then have *: "k = k'" + apply - + apply (rule ccontr) + using p(5)[OF k(1-2)] + apply auto + done + { assume "x \ k" then show "x \ k'" unfolding * . } + { assume "x \ k'" then show "x\k" unfolding * . } qed let ?a = a and ?b = b (* a is something else while proofing the next theorem. *) - show "\x. x \ ?B a \ norm ((\(x, k). content k *\<^sub>R f' (x) - (f ((interval_upperbound k)) - - f ((interval_lowerbound k)))) x) \ e * (b - a) / 4" apply(rule,rule) unfolding mem_Collect_eq + show "\x. x \ ?B a \ norm ((\(x, k). content k *\<^sub>R f' x - (f (interval_upperbound k) - + f (interval_lowerbound k))) x) \ e * (b - a) / 4" + apply rule + apply rule + unfolding mem_Collect_eq unfolding split_paired_all fst_conv snd_conv - proof safe case goal1 guess v using pa[OF goal1(1)] .. note v = conjunctD2[OF this] - have " ?a\{ ?a..v}" using v(2) by auto hence "v \ ?b" using p(3)[OF goal1(1)] unfolding subset_eq v by auto - moreover have "{?a..v} \ ball ?a da" using fineD[OF as(2) goal1(1)] - apply-apply(subst(asm) if_P,rule refl) unfolding subset_eq apply safe apply(erule_tac x=" x" in ballE) - by(auto simp add:subset_eq dist_real_def v) ultimately - show ?case unfolding v interval_bounds_real[OF v(2)] apply- apply(rule da(2)[of "v"]) - using goal1 fineD[OF as(2) goal1(1)] unfolding v content_eq_0 by auto + proof safe + case goal1 + guess v using pa[OF goal1(1)] .. note v = conjunctD2[OF this] + have "?a \ {?a..v}" + using v(2) by auto + then have "v \ ?b" + using p(3)[OF goal1(1)] unfolding subset_eq v by auto + moreover have "{?a..v} \ ball ?a da" + using fineD[OF as(2) goal1(1)] + apply - + apply (subst(asm) if_P) + apply (rule refl) + unfolding subset_eq + apply safe + apply (erule_tac x=" x" in ballE) + apply (auto simp add:subset_eq dist_real_def v) + done + ultimately show ?case + unfolding v interval_bounds_real[OF v(2)] + apply - + apply(rule da(2)[of "v"]) + using goal1 fineD[OF as(2) goal1(1)] + unfolding v content_eq_0 + apply auto + done qed - show "\x. x \ ?B b \ norm ((\(x, k). content k *\<^sub>R f' (x) - - (f ((interval_upperbound k)) - f ((interval_lowerbound k)))) x) \ e * (b - a) / 4" - apply(rule,rule) unfolding mem_Collect_eq unfolding split_paired_all fst_conv snd_conv - proof safe case goal1 guess v using pb[OF goal1(1)] .. note v = conjunctD2[OF this] - have " ?b\{v.. ?b}" using v(2) by auto hence "v \ ?a" using p(3)[OF goal1(1)] + show "\x. x \ ?B b \ norm ((\(x, k). content k *\<^sub>R f' x - + (f (interval_upperbound k) - f (interval_lowerbound k))) x) \ e * (b - a) / 4" + apply rule + apply rule + unfolding mem_Collect_eq + unfolding split_paired_all fst_conv snd_conv + proof safe + case goal1 guess v using pb[OF goal1(1)] .. note v = conjunctD2[OF this] + have "?b \ {v.. ?b}" + using v(2) by auto + then have "v \ ?a" using p(3)[OF goal1(1)] unfolding subset_eq v by auto - moreover have "{v..?b} \ ball ?b db" using fineD[OF as(2) goal1(1)] - apply-apply(subst(asm) if_P,rule refl) unfolding subset_eq apply safe - apply(erule_tac x=" x" in ballE) using ab - by(auto simp add:subset_eq v dist_real_def) ultimately - show ?case unfolding v unfolding interval_bounds_real[OF v(2)] apply- apply(rule db(2)[of "v"]) - using goal1 fineD[OF as(2) goal1(1)] unfolding v content_eq_0 by auto + moreover have "{v..?b} \ ball ?b db" + using fineD[OF as(2) goal1(1)] + apply - + apply (subst(asm) if_P, rule refl) + unfolding subset_eq + apply safe + apply (erule_tac x=" x" in ballE) + using ab + apply (auto simp add:subset_eq v dist_real_def) + done + ultimately show ?case + unfolding v + unfolding interval_bounds_real[OF v(2)] + apply - + apply(rule db(2)[of "v"]) + using goal1 fineD[OF as(2) goal1(1)] + unfolding v content_eq_0 + apply auto + done qed - qed(insert p(1) ab e, auto simp add:field_simps) qed auto qed qed qed qed + qed (insert p(1) ab e, auto simp add: field_simps) + qed auto + qed + qed + qed +qed + subsection {* Stronger form with finite number of exceptional points. *} -lemma fundamental_theorem_of_calculus_interior_strong: fixes f::"real \ 'a::banach" - assumes"finite s" "a \ b" "continuous_on {a..b} f" - "\x\{a<..{a<.. c" "c \ b" by auto - thus ?thesis apply(subst *) apply(rule has_integral_combine) apply assumption+ - apply(rule_tac[!] Suc(1)[OF cs(3)]) using Suc(3) unfolding cs - proof- show "continuous_on {a..c} f" "continuous_on {c..b} f" - apply(rule_tac[!] continuous_on_subset[OF Suc(5)]) using True by auto +lemma fundamental_theorem_of_calculus_interior_strong: + fixes f :: "real \ 'a::banach" + assumes "finite s" + and "a \ b" + and "continuous_on {a..b} f" + and "\x\{a<.. {a<.. c" "c \ b" + by auto + then show ?thesis + apply (subst *) + apply (rule has_integral_combine) + apply assumption+ + apply (rule_tac[!] Suc(1)[OF cs(3)]) + using Suc(3) + unfolding cs + proof - + show "continuous_on {a..c} f" "continuous_on {c..b} f" + apply (rule_tac[!] continuous_on_subset[OF Suc(5)]) + using True + apply auto + done let ?P = "\i j. \x\{i<.. 'a::banach" - assumes "finite s" "a \ b" "continuous_on {a..b} f" - "\x\{a..b} - s. (f has_vector_derivative f'(x)) (at x)" + show "?P a c" "?P c b" + apply safe + apply (rule_tac[!] Suc(6)[rule_format]) + using True + unfolding cs + apply auto + done + qed auto + qed +qed + +lemma fundamental_theorem_of_calculus_strong: + fixes f :: "real \ 'a::banach" + assumes "finite s" + and "a \ b" + and "continuous_on {a..b} f" + and "\x\{a..b} - s. (f has_vector_derivative f'(x)) (at x)" shows "(f' has_integral (f(b) - f(a))) {a..b}" - apply(rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f']) - using assms(4) by auto - -lemma indefinite_integral_continuous_left: fixes f::"real \ 'a::banach" + apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f']) + using assms(4) + apply auto + done + +lemma indefinite_integral_continuous_left: + fixes f::"real \ 'a::banach" assumes "f integrable_on {a..b}" "a < c" "c \ b" "0 < e" obtains d where "0 < d" "\t. c - d < t \ t \ c \ norm(integral {a..c} f - integral {a..t} f) < e" proof- have "\w>0. \t. c - w < t \ t < c \ norm(f c) * norm(c - t) < e / 3" @@ -9087,7 +10216,8 @@ apply (rule_tac x=N in exI) proof safe case goal1 - have *:"\y ix. y < i + r \ i \ ix \ ix \ y \ abs(ix - i) < r" by arith + have *: "\y ix. y < i + r \ i \ ix \ ix \ y \ abs(ix - i) < r" + by arith show ?case unfolding real_norm_def apply (rule *[rule_format,OF y(2)]) diff -r 1905ebfec373 -r 129bd52a5e5f src/Pure/Concurrent/simple_thread.ML --- a/src/Pure/Concurrent/simple_thread.ML Wed Sep 11 10:57:09 2013 +0200 +++ b/src/Pure/Concurrent/simple_thread.ML Wed Sep 11 11:38:07 2013 +0200 @@ -25,7 +25,7 @@ fun fork interrupts body = Thread.fork (fn () => exception_trace (fn () => - body () handle exn => if Exn.is_interrupt exn then () else reraise exn), + body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn), attributes interrupts); fun join thread = diff -r 1905ebfec373 -r 129bd52a5e5f src/Pure/Tools/build_dialog.scala --- a/src/Pure/Tools/build_dialog.scala Wed Sep 11 10:57:09 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,84 +0,0 @@ -/* Title: Pure/Tools/build_dialog.scala - Author: Makarius - -Dialog for session build process. -*/ - -package isabelle - - -import java.awt.{GraphicsEnvironment, Point, Font} - -import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel, - BorderPanel, MainFrame, TextArea, SwingApplication, Component, Label} -import scala.swing.event.ButtonClicked - - -object Build_Dialog -{ - /* command line entry point */ - - def main(args: Array[String]) - { - GUI.init_laf() - try { - args.toList match { - case - logic_option :: - logic :: - Properties.Value.Boolean(system_mode) :: - include_dirs => - val options = Options.init() - val dirs = include_dirs.map(Path.explode(_)) - val session = - Isabelle_System.default_logic(logic, - if (logic_option != "") options.string(logic_option) else "") - - val system_dialog = new System_Dialog - dialog(options, system_dialog, system_mode, dirs, session) - system_dialog.join_exit - - case _ => error("Bad arguments:\n" + cat_lines(args)) - } - } - catch { - case exn: Throwable => - GUI.error_dialog(null, "Isabelle build failure", GUI.scrollable_text(Exn.message(exn))) - sys.exit(2) - } - } - - - /* dialog */ - - def dialog( - options: Options, - system_dialog: System_Dialog, - system_mode: Boolean, - dirs: List[Path], - session: String) - { - val more_dirs = dirs.map((false, _)) - - if (Build.build(options = options, build_heap = true, no_build = true, - more_dirs = more_dirs, sessions = List(session)) == 0) - system_dialog.return_code(0) - else { - system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")") - system_dialog.echo("Build started for Isabelle/" + session + " ...") - - val (out, rc) = - try { - ("", - Build.build(options = options, progress = system_dialog, - build_heap = true, more_dirs = more_dirs, - system_mode = system_mode, sessions = List(session))) - } - catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } - - system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) - system_dialog.return_code(rc) - } - } -} - diff -r 1905ebfec373 -r 129bd52a5e5f src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Wed Sep 11 10:57:09 2013 +0200 +++ b/src/Pure/Tools/main.scala Wed Sep 11 11:38:07 2013 +0200 @@ -7,7 +7,6 @@ package isabelle -import javax.swing.SwingUtilities import java.lang.{System, ClassLoader} import java.io.{File => JFile, BufferedReader, InputStreamReader} import java.nio.file.Files @@ -40,13 +39,32 @@ if (mode == "none") system_dialog.return_code(0) else { + val options = Options.init() val system_mode = mode == "" || mode == "system" - val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) - val options = Options.init() + val more_dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).map((false, _)) val session = Isabelle_System.default_logic( Isabelle_System.getenv("JEDIT_LOGIC"), options.string("jedit_logic")) - Build_Dialog.dialog(options, system_dialog, system_mode, dirs, session) + + if (Build.build(options = options, build_heap = true, no_build = true, + more_dirs = more_dirs, sessions = List(session)) == 0) + system_dialog.return_code(0) + else { + system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")") + system_dialog.echo("Build started for Isabelle/" + session + " ...") + + val (out, rc) = + try { + ("", + Build.build(options = options, progress = system_dialog, + build_heap = true, more_dirs = more_dirs, + system_mode = system_mode, sessions = List(session))) + } + catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } + + system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) + system_dialog.return_code(rc) + } } } catch { case exn: Throwable => exit_error(exn) } diff -r 1905ebfec373 -r 129bd52a5e5f src/Pure/build-jars --- a/src/Pure/build-jars Wed Sep 11 10:57:09 2013 +0200 +++ b/src/Pure/build-jars Wed Sep 11 11:38:07 2013 +0200 @@ -72,7 +72,6 @@ Thy/thy_load.scala Thy/thy_syntax.scala Tools/build.scala - Tools/build_dialog.scala Tools/doc.scala Tools/keywords.scala Tools/main.scala diff -r 1905ebfec373 -r 129bd52a5e5f src/Tools/jEdit/patches/jedit/numeric_keypad --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/jedit/numeric_keypad Wed Sep 11 11:38:07 2013 +0200 @@ -0,0 +1,50 @@ +--- 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-07-28 19:03:38.000000000 +0200 ++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-09-10 21:55:21.220043663 +0200 +@@ -129,7 +129,7 @@ + case KeyEvent.VK_OPEN_BRACKET : + case KeyEvent.VK_BACK_SLASH : + case KeyEvent.VK_CLOSE_BRACKET: +- /* case KeyEvent.VK_NUMPAD0 : ++ case KeyEvent.VK_NUMPAD0 : + case KeyEvent.VK_NUMPAD1 : + case KeyEvent.VK_NUMPAD2 : + case KeyEvent.VK_NUMPAD3 : +@@ -144,7 +144,7 @@ + case KeyEvent.VK_SEPARATOR: + case KeyEvent.VK_SUBTRACT : + case KeyEvent.VK_DECIMAL : +- case KeyEvent.VK_DIVIDE :*/ ++ case KeyEvent.VK_DIVIDE : + case KeyEvent.VK_BACK_QUOTE: + case KeyEvent.VK_QUOTE: + case KeyEvent.VK_DEAD_GRAVE: +@@ -202,28 +202,7 @@ + //{{{ isNumericKeypad() method + public static boolean isNumericKeypad(int keyCode) + { +- switch(keyCode) +- { +- case KeyEvent.VK_NUMPAD0: +- case KeyEvent.VK_NUMPAD1: +- case KeyEvent.VK_NUMPAD2: +- case KeyEvent.VK_NUMPAD3: +- case KeyEvent.VK_NUMPAD4: +- case KeyEvent.VK_NUMPAD5: +- case KeyEvent.VK_NUMPAD6: +- case KeyEvent.VK_NUMPAD7: +- case KeyEvent.VK_NUMPAD8: +- case KeyEvent.VK_NUMPAD9: +- case KeyEvent.VK_MULTIPLY: +- case KeyEvent.VK_ADD: +- /* case KeyEvent.VK_SEPARATOR: */ +- case KeyEvent.VK_SUBTRACT: +- case KeyEvent.VK_DECIMAL: +- case KeyEvent.VK_DIVIDE: +- return true; +- default: +- return false; +- } ++ return false; + } //}}} + + //{{{ processKeyEvent() method