# HG changeset patch # User eberlm # Date 1502111437 -7200 # Node ID a8b89392ecb613f5551626cc72fde1d1c5e39b6b # Parent 1f66c7d77002149f9f339136e03f2e9b1292562b# Parent e2f426b54922f6506bab6ffe3ece47762d66866b Merged diff -r 1f66c7d77002 -r a8b89392ecb6 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Aug 04 18:03:50 2017 +0200 +++ b/Admin/components/components.sha1 Mon Aug 07 15:10:37 2017 +0200 @@ -34,6 +34,7 @@ e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz c11b25c919e2ec44fe2b6ac2086337b456344e97 e-1.8.tar.gz +6b962a6b4539b7ca4199977973c61a8c98a492e8 e-2.0.tar.gz 6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz 8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz diff -r 1f66c7d77002 -r a8b89392ecb6 Admin/components/main --- a/Admin/components/main Fri Aug 04 18:03:50 2017 +0200 +++ b/Admin/components/main Mon Aug 07 15:10:37 2017 +0200 @@ -2,7 +2,7 @@ bash_process-1.2.1 csdp-6.x cvc4-1.5 -e-1.8 +e-2.0 isabelle_fonts-20160830 jdk-8u131 jedit_build-20170319 diff -r 1f66c7d77002 -r a8b89392ecb6 NEWS --- a/NEWS Fri Aug 04 18:03:50 2017 +0200 +++ b/NEWS Mon Aug 07 15:10:37 2017 +0200 @@ -116,6 +116,11 @@ *** HOL *** +* Command and antiquotation "value" with modified default strategy: +terms without free variables are always evaluated using plain evaluation +only, with no fallback on normalization by evaluation. +Minor INCOMPATIBILITY. + * Notions of squarefreeness, n-th powers, and prime powers in HOL-Computational_Algebra and HOL-Number_Theory. diff -r 1f66c7d77002 -r a8b89392ecb6 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Fri Aug 04 18:03:50 2017 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Mon Aug 07 15:10:37 2017 +0200 @@ -197,8 +197,8 @@ for Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the directory that contains the \texttt{why3} executable. -Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 1.8, -LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 3.0.% +Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0, +LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 4.0.% \footnote{Following the rewrite of Vampire, the counter for version numbers was reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more recent than 9.0 or 11.5.}% @@ -206,7 +206,7 @@ versions might not work well with Sledgehammer. Ideally, you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or -\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0''). +\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``4.0''). Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER}, diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/ATP.thy --- a/src/HOL/ATP.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/ATP.thy Mon Aug 07 15:10:37 2017 +0200 @@ -6,7 +6,7 @@ section \Automatic Theorem Provers (ATPs)\ theory ATP -imports Meson + imports Meson begin subsection \ATP problems and proofs\ diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Aug 07 15:10:37 2017 +0200 @@ -1,30 +1,13 @@ (* Title: HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Author: Johannes Hölzl, TU München Author: Robert Himmelmann, TU München + Huge cleanup by LCP *) theory Equivalence_Lebesgue_Henstock_Integration imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral begin -lemma finite_product_dependent: (*FIXME DELETE*) - assumes "finite s" - and "\x. x \ s \ finite (t x)" - shows "finite {(i, j) |i j. i \ s \ j \ t i}" - using assms -proof induct - case (insert x s) - have *: "{(i, j) |i j. i \ insert x s \ j \ t i} = - (\y. (x,y)) ` (t x) \ {(i, j) |i j. i \ s \ j \ t i}" by auto - show ?case - unfolding * - apply (rule finite_UnI) - using insert - apply auto - done -qed auto - - lemma le_left_mono: "x \ y \ y \ a \ x \ (a::'a::preorder)" by (auto intro: order_trans) @@ -90,7 +73,7 @@ obtain d where "gauge d" and integral_f: "\p. p tagged_division_of cbox x y \ d fine p \ - norm ((\(x, k)\p. content k *\<^sub>R f x) - I) < e" + norm ((\(x,k) \ p. content k *\<^sub>R f x) - I) < e" using \0 f unfolding has_integral by auto define C where "C X m = X \ {x. ball x (1/Suc m) \ d x}" for X m @@ -194,14 +177,14 @@ then show "\{k. \x. (x, k) \ ?p} = cbox x y" using p(1) by auto qed - ultimately have I: "norm ((\(x, k)\?p. content k *\<^sub>R f x) - I) < e" + ultimately have I: "norm ((\(x,k) \ ?p. content k *\<^sub>R f x) - I) < e" using integral_f by auto - have "(\(x, k)\?p. content k *\<^sub>R f x) = - (\(x, k)\?T ` (p \ s). content k *\<^sub>R f x) + (\(x, k)\p - s. content k *\<^sub>R f x)" + have "(\(x,k) \ ?p. content k *\<^sub>R f x) = + (\(x,k) \ ?T ` (p \ s). content k *\<^sub>R f x) + (\(x,k) \ p - s. content k *\<^sub>R f x)" using p(1)[THEN tagged_division_ofD(1)] by (safe intro!: sum.union_inter_neutral) (auto simp: s_def T_def) - also have "(\(x, k)\?T ` (p \ s). content k *\<^sub>R f x) = (\(x, k)\p \ s. content k *\<^sub>R f (T X k))" + also have "(\(x,k) \ ?T ` (p \ s). content k *\<^sub>R f x) = (\(x,k) \ p \ s. content k *\<^sub>R f (T X k))" proof (subst sum.reindex_nontrivial, safe) fix x1 x2 k assume 1: "(x1, k) \ p" "(x1, k) \ s" and 2: "(x2, k) \ p" "(x2, k) \ s" and eq: "content k *\<^sub>R f (T X k) \ 0" @@ -209,8 +192,8 @@ show "x1 = x2" by (auto simp: content_eq_0_interior) qed (use p in \auto intro!: sum.cong\) - finally have eq: "(\(x, k)\?p. content k *\<^sub>R f x) = - (\(x, k)\p \ s. content k *\<^sub>R f (T X k)) + (\(x, k)\p - s. content k *\<^sub>R f x)" . + finally have eq: "(\(x,k) \ ?p. content k *\<^sub>R f x) = + (\(x,k) \ p \ s. content k *\<^sub>R f (T X k)) + (\(x,k) \ p - s. content k *\<^sub>R f x)" . have in_T: "(x, k) \ s \ T X k \ X" for x k using in_s[of x k] by (auto simp: C_def) @@ -224,7 +207,7 @@ have [simp]: "finite p" using tagged_division_ofD(1)[OF p(1)] . - have "(M - 3*e) * (b - a) \ (\(x, k)\p \ s. content k) * (b - a)" + have "(M - 3*e) * (b - a) \ (\(x,k) \ p \ s. content k) * (b - a)" proof (intro mult_right_mono) have fin: "?\ (E \ \{k\snd`p. k \ C X m = {}}) < \" for X using \?\ E < \\ by (rule le_less_trans[rotated]) (auto intro!: emeasure_mono \E \ sets ?L\) @@ -287,15 +270,15 @@ finally show "M - 3 * e \ (\(x, y)\p \ s. content y)" using \0 < e\ by (simp add: split_beta) qed (use \a < b\ in auto) - also have "\ = (\(x, k)\p \ s. content k * (b - a))" + also have "\ = (\(x,k) \ p \ s. content k * (b - a))" by (simp add: sum_distrib_right split_beta') - also have "\ \ (\(x, k)\p \ s. content k * (f (T ?F k) - f (T ?E k)))" + also have "\ \ (\(x,k) \ p \ s. content k * (f (T ?F k) - f (T ?E k)))" using parts(3) by (auto intro!: sum_mono mult_left_mono diff_mono) - also have "\ = (\(x, k)\p \ s. content k * f (T ?F k)) - (\(x, k)\p \ s. content k * f (T ?E k))" + also have "\ = (\(x,k) \ p \ s. content k * f (T ?F k)) - (\(x,k) \ p \ s. content k * f (T ?E k))" by (auto intro!: sum.cong simp: field_simps sum_subtractf[symmetric]) - also have "\ = (\(x, k)\?B. content k *\<^sub>R f x) - (\(x, k)\?A. content k *\<^sub>R f x)" + also have "\ = (\(x,k) \ ?B. content k *\<^sub>R f x) - (\(x,k) \ ?A. content k *\<^sub>R f x)" by (subst (1 2) parts) auto - also have "\ \ norm ((\(x, k)\?B. content k *\<^sub>R f x) - (\(x, k)\?A. content k *\<^sub>R f x))" + also have "\ \ norm ((\(x,k) \ ?B. content k *\<^sub>R f x) - (\(x,k) \ ?A. content k *\<^sub>R f x))" by auto also have "\ \ e + e" using parts(1)[of ?E] parts(1)[of ?F] by (intro norm_diff_triangle_le[of _ I]) auto @@ -574,11 +557,14 @@ shows "integral\<^sup>N lborel f = I" proof - from f_borel have "(\x. ennreal (f x)) \ borel_measurable lborel" by auto - from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this + from borel_measurable_implies_simple_function_sequence'[OF this] + obtain F where F: "\i. simple_function lborel (F i)" "incseq F" + "\i x. F i x < top" "\x. (SUP i. F i x) = ennreal (f x)" + by blast + then have [measurable]: "\i. F i \ borel_measurable lborel" + by (metis borel_measurable_simple_function) let ?B = "\i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set" - note F(1)[THEN borel_measurable_simple_function, measurable] - have "0 \ I" using I by (rule has_integral_nonneg) (simp add: nonneg) @@ -1199,13 +1185,13 @@ assume "0 < e" have "S \ lmeasurable" using \negligible S\ by (simp add: negligible_iff_null_sets fmeasurableI_null_sets) - have e22: "0 < e / 2 / (2 * B * real DIM('M)) ^ DIM('N)" + have e22: "0 < e/2 / (2 * B * real DIM('M)) ^ DIM('N)" using \0 < e\ \0 < B\ by (simp add: divide_simps) obtain T where "open T" "S \ T" "T \ lmeasurable" - and "measure lebesgue T \ measure lebesgue S + e / 2 / (2 * B * DIM('M)) ^ DIM('N)" + and "measure lebesgue T \ measure lebesgue S + e/2 / (2 * B * DIM('M)) ^ DIM('N)" by (rule lmeasurable_outer_open [OF \S \ lmeasurable\ e22]) - then have T: "measure lebesgue T \ e / 2 / (2 * B * DIM('M)) ^ DIM('N)" + then have T: "measure lebesgue T \ e/2 / (2 * B * DIM('M)) ^ DIM('N)" using \negligible S\ by (simp add: negligible_iff_null_sets measure_eq_0_null_sets) have "\r. 0 < r \ r \ 1/2 \ (x \ S \ (\y. norm(y - x) < r @@ -1286,7 +1272,7 @@ qed have countbl: "countable (fbx ` \)" using \countable \\ by blast - have "(\k\fbx`\'. measure lebesgue k) \ e / 2" if "\' \ \" "finite \'" for \' + have "(\k\fbx`\'. measure lebesgue k) \ e/2" if "\' \ \" "finite \'" for \' proof - have BM_ge0: "0 \ B * (DIM('M) * prj1 (vf X - uf X))" if "X \ \'" for X using \0 < B\ \\' \ \\ that vu_pos by fastforce @@ -1330,7 +1316,7 @@ qed also have "\ = (2 * B * DIM('M)) ^ DIM('N) * sum (measure lebesgue) \'" by (simp add: sum_distrib_left) - also have "\ \ e / 2" + also have "\ \ e/2" proof - have div: "\' division_of \\'" apply (auto simp: \finite \'\ \{} \ \'\ division_of_def) @@ -1363,13 +1349,13 @@ using \0 < B\ apply (simp add: algebra_simps) done - also have "\ \ e / 2" + also have "\ \ e/2" using T \0 < B\ by (simp add: field_simps) finally show ?thesis . qed finally show ?thesis . qed - then have e2: "sum (measure lebesgue) \ \ e / 2" if "\ \ fbx ` \" "finite \" for \ + then have e2: "sum (measure lebesgue) \ \ e/2" if "\ \ fbx ` \" "finite \" for \ by (metis finite_subset_image that) show "\W\lmeasurable. f ` S \ W \ measure lebesgue W < e" proof (intro bexI conjI) @@ -1602,7 +1588,7 @@ finally show "(\k\d. norm (integral k f)) \ integral UNIV (\x. norm (f x))" . qed -lemma helplemma: +lemma absdiff_norm_less: assumes "sum (\x. norm (f x - g x)) s < e" and "finite s" shows "\sum (\x. norm(f x)) s - sum (\x. norm(g x)) s\ < e" @@ -1613,28 +1599,27 @@ apply (rule norm_triangle_ineq3) done -text\FIXME: needs refactoring and use of Sigma\ -lemma bounded_variation_absolutely_integrable_interval: +proposition bounded_variation_absolutely_integrable_interval: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes f: "f integrable_on cbox a b" - and *: "\d. d division_of (cbox a b) \ sum (\k. norm(integral k f)) d \ B" + and *: "\d. d division_of (cbox a b) \ sum (\K. norm(integral K f)) d \ B" shows "f absolutely_integrable_on cbox a b" proof - - let ?f = "\d. \k\d. norm (integral k f)" and ?D = "{d. d division_of (cbox a b)}" + let ?f = "\d. \K\d. norm (integral K f)" and ?D = "{d. d division_of (cbox a b)}" have D_1: "?D \ {}" by (rule elementary_interval[of a b]) auto have D_2: "bdd_above (?f`?D)" by (metis * mem_Collect_eq bdd_aboveI2) note D = D_1 D_2 let ?S = "SUP x:?D. ?f x" - show ?thesis - apply (rule absolutely_integrable_onI [OF f has_integral_integrable]) - apply (subst has_integral[of _ ?S]) - apply safe - proof goal_cases - case e: (1 e) - then have "?S - e / 2 < ?S" by simp - then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\k\d. norm (integral k f))" + have *: "\\. gauge \ \ + (\p. p tagged_division_of cbox a b \ + \ fine p \ + norm ((\(x,k) \ p. content k *\<^sub>R norm (f x)) - ?S) < e)" + if e: "e > 0" for e + proof - + have "?S - e/2 < ?S" using \e > 0\ by simp + then obtain d where d: "d division_of (cbox a b)" "?S - e/2 < (\k\d. norm (integral k f))" unfolding less_cSUP_iff[OF D] by auto note d' = division_ofD[OF this(1)] @@ -1642,126 +1627,118 @@ proof fix x have "\da>0. \xa\\{i \ d. x \ i}. da \ dist x xa" - apply (rule separate_point_closed) - apply (rule closed_Union) - apply (rule finite_subset[OF _ d'(1)]) - using d'(4) - apply auto - done + proof (rule separate_point_closed) + show "closed (\{i \ d. x \ i})" + apply (rule closed_Union) + apply (simp add: d'(1)) + using d'(4) apply auto + done + show "x \ \{i \ d. x \ i}" + by auto + qed then show "\e>0. \i\d. x \ i \ ball x e \ i = {}" by force qed - then obtain k where k: "\x. 0 < k x" - "\i x. \i \ d; x \ i\ \ ball x (k x) \ i = {}" + then obtain k where k: "\x. 0 < k x" "\i x. \i \ d; x \ i\ \ ball x (k x) \ i = {}" by metis have "e/2 > 0" using e by auto - from henstock_lemma[OF assms(1) this] - obtain g where g: "gauge g" - "\p. \p tagged_partial_division_of cbox a b; g fine p\ - \ (\(x, k)\p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" + with henstock_lemma[OF f] + obtain \ where g: "gauge \" + "\p. \p tagged_partial_division_of cbox a b; \ fine p\ + \ (\(x,k) \ p. norm (content k *\<^sub>R f x - integral k f)) < e/2" by (metis (no_types, lifting)) - let ?g = "\x. g x \ ball x (k x)" - show ?case - apply (rule_tac x="?g" in exI) - apply safe - proof - + let ?g = "\x. \ x \ ball x (k x)" + show ?thesis + proof (intro exI conjI allI impI) show "gauge ?g" - using g(1) k(1) - unfolding gauge_def - by auto + using g(1) k(1) by (auto simp: gauge_def) + next fix p - assume "p tagged_division_of (cbox a b)" and "?g fine p" - note p = this(1) conjunctD2[OF this(2)[unfolded fine_Int]] + assume "p tagged_division_of (cbox a b) \ ?g fine p" + then have p: "p tagged_division_of cbox a b" "\ fine p" "(\x. ball x (k x)) fine p" + by (auto simp: fine_Int) note p' = tagged_division_ofD[OF p(1)] define p' where "p' = {(x,k) | x k. \i l. x \ i \ i \ d \ (x,l) \ p \ k = i \ l}" - have gp': "g fine p'" - using p(2) - unfolding p'_def fine_def - by auto + have gp': "\ fine p'" + using p(2) by (auto simp: p'_def fine_def) have p'': "p' tagged_division_of (cbox a b)" - apply (rule tagged_division_ofI) - proof - + proof (rule tagged_division_ofI) show "finite p'" - apply (rule finite_subset[of _ "(\(k,(x,l)). (x,k \ l)) ` - {(k,xl) | k xl. k \ d \ xl \ p}"]) - unfolding p'_def - defer - apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)]) - apply safe - unfolding image_iff - apply (rule_tac x="(i,x,l)" in bexI) - apply auto - done - fix x k - assume "(x, k) \ p'" - then have "\i l. x \ i \ i \ d \ (x, l) \ p \ k = i \ l" + proof (rule finite_subset) + show "p' \ (\(k, x, l). (x, k \ l)) ` (d \ p)" + by (force simp: p'_def image_iff) + show "finite ((\(k, x, l). (x, k \ l)) ` (d \ p))" + by (simp add: d'(1) p'(1)) + qed + next + fix x K + assume "(x, K) \ p'" + then have "\i l. x \ i \ i \ d \ (x, l) \ p \ K = i \ l" unfolding p'_def by auto - then obtain i l where il: "x \ i" "i \ d" "(x, l) \ p" "k = i \ l" by blast - show "x \ k" and "k \ cbox a b" + then obtain i l where il: "x \ i" "i \ d" "(x, l) \ p" "K = i \ l" by blast + show "x \ K" and "K \ cbox a b" using p'(2-3)[OF il(3)] il by auto - show "\a b. k = cbox a b" + show "\a b. K = cbox a b" unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)] - apply safe - unfolding Int_interval - apply auto - done + by (meson Int_interval) next - fix x1 k1 - assume "(x1, k1) \ p'" - then have "\i l. x1 \ i \ i \ d \ (x1, l) \ p \ k1 = i \ l" + fix x1 K1 + assume "(x1, K1) \ p'" + then have "\i l. x1 \ i \ i \ d \ (x1, l) \ p \ K1 = i \ l" unfolding p'_def by auto - then obtain i1 l1 where il1: "x1 \ i1" "i1 \ d" "(x1, l1) \ p" "k1 = i1 \ l1" by blast - fix x2 k2 - assume "(x2,k2)\p'" - then have "\i l. x2 \ i \ i \ d \ (x2, l) \ p \ k2 = i \ l" + then obtain i1 l1 where il1: "x1 \ i1" "i1 \ d" "(x1, l1) \ p" "K1 = i1 \ l1" by blast + fix x2 K2 + assume "(x2,K2) \ p'" + then have "\i l. x2 \ i \ i \ d \ (x2, l) \ p \ K2 = i \ l" unfolding p'_def by auto - then obtain i2 l2 where il2: "x2 \ i2" "i2 \ d" "(x2, l2) \ p" "k2 = i2 \ l2" by blast - assume "(x1, k1) \ (x2, k2)" + then obtain i2 l2 where il2: "x2 \ i2" "i2 \ d" "(x2, l2) \ p" "K2 = i2 \ l2" by blast + assume "(x1, K1) \ (x2, K2)" then have "interior i1 \ interior i2 = {} \ interior l1 \ interior l2 = {}" - using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)] - unfolding il1 il2 - by auto - then show "interior k1 \ interior k2 = {}" + using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)] by (auto simp: il1 il2) + then show "interior K1 \ interior K2 = {}" unfolding il1 il2 by auto next have *: "\(x, X) \ p'. X \ cbox a b" - unfolding p'_def using d' by auto - show "\{k. \x. (x, k) \ p'} = cbox a b" - apply rule - apply (rule Union_least) - unfolding mem_Collect_eq - apply (erule exE) - apply (drule *[rule_format]) - apply safe + unfolding p'_def using d' by blast + have "y \ \{K. \x. (x, K) \ p'}" if y: "y \ cbox a b" for y proof - - fix y - assume y: "y \ cbox a b" - then have "\x l. (x, l) \ p \ y\l" - unfolding p'(6)[symmetric] by auto - then obtain x l where xl: "(x, l) \ p" "y \ l" by metis - then have "\k. k \ d \ y \ k" + obtain x l where xl: "(x, l) \ p" "y \ l" + using y unfolding p'(6)[symmetric] by auto + obtain i where i: "i \ d" "y \ i" using y unfolding d'(6)[symmetric] by auto - then obtain i where i: "i \ d" "y \ i" by metis have "x \ i" using fineD[OF p(3) xl(1)] using k(2) i xl by auto - then show "y \ \{k. \x. (x, k) \ p'}" - unfolding p'_def Union_iff - apply (rule_tac x="i \ l" in bexI) - using i xl - apply auto - done + then show ?thesis + unfolding p'_def + by (rule_tac X="i \ l" in UnionI) (use i xl in auto) + qed + show "\{K. \x. (x, K) \ p'} = cbox a b" + proof + show "\{k. \x. (x, k) \ p'} \ cbox a b" + using * by auto + next + show "cbox a b \ \{k. \x. (x, k) \ p'}" + proof + fix y + assume y: "y \ cbox a b" + obtain x L where xl: "(x, L) \ p" "y \ L" + using y unfolding p'(6)[symmetric] by auto + obtain I where i: "I \ d" "y \ I" + using y unfolding d'(6)[symmetric] by auto + have "x \ I" + using fineD[OF p(3) xl(1)] using k(2) i xl by auto + then show "y \ \{k. \x. (x, k) \ p'}" + apply (rule_tac X="I \ L" in UnionI) + using i xl by (auto simp: p'_def) + qed qed qed - then have "(\(x, k)\p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2" + then have sum_less_e2: "(\(x,K) \ p'. norm (content K *\<^sub>R f x - integral K f)) < e/2" using g(2) gp' tagged_division_of_def by blast - then have **: "\(\(x,k)\p'. norm (content k *\<^sub>R f x)) - (\(x,k)\p'. norm (integral k f))\ < e / 2" - unfolding split_def - using p'' - by (force intro!: helplemma) - have p'alt: "p' = {(x,(i \ l)) | x i l. (x,l) \ p \ i \ d \ i \ l \ {}}" + have p'alt: "p' = {(x, I \ L) | x I L. (x,L) \ p \ I \ d \ I \ L \ {}}" proof (safe, goal_cases) case prems: (2 _ _ x i l) have "x \ i" @@ -1773,297 +1750,247 @@ apply safe apply (rule_tac x=x in exI) apply (rule_tac x="i \ l" in exI) - apply safe - using prems apply auto done then show ?case using prems(3) by auto next - fix x k - assume "(x, k) \ p'" - then have "\i l. x \ i \ i \ d \ (x, l) \ p \ k = i \ l" + fix x K + assume "(x, K) \ p'" + then obtain i l where il: "x \ i" "i \ d" "(x, l) \ p" "K = i \ l" unfolding p'_def by auto - then obtain i l where il: "x \ i" "i \ d" "(x, l) \ p" "k = i \ l" by blast - then show "\y i l. (x, k) = (y, i \ l) \ (y, l) \ p \ i \ d \ i \ l \ {}" + then show "\y i l. (x, K) = (y, i \ l) \ (y, l) \ p \ i \ d \ i \ l \ {}" using p'(2) by fastforce qed - have sum_p': "(\(x, k)\p'. norm (integral k f)) = (\k\snd ` p'. norm (integral k f))" + have sum_p': "(\(x,K) \ p'. norm (integral K f)) = (\k\snd ` p'. norm (integral k f))" apply (subst sum.over_tagged_division_lemma[OF p'',of "\k. norm (integral k f)"]) apply (auto intro: integral_null simp: content_eq_0_interior) done - note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]] + have snd_p_div: "snd ` p division_of cbox a b" + by (rule division_of_tagged_division[OF p(1)]) + note snd_p = division_ofD[OF snd_p_div] + have fin_d_sndp: "finite (d \ snd ` p)" + by (simp add: d'(1) snd_p(1)) - have *: "\sni sni' sf sf'. \sf' - sni'\ < e / 2 \ ?S - e / 2 < sni \ sni' \ ?S \ - sni \ sni' \ sf' = sf \ \sf - ?S\ < e" + have *: "\sni sni' sf sf'. \\sf' - sni'\ < e/2; ?S - e/2 < sni; sni' \ ?S; + sni \ sni'; sf' = sf\ \ \sf - ?S\ < e" by arith - show "norm ((\(x, k)\p. content k *\<^sub>R norm (f x)) - ?S) < e" + show "norm ((\(x,k) \ p. content k *\<^sub>R norm (f x)) - ?S) < e" unfolding real_norm_def - apply (rule *[rule_format,OF **]) - apply safe - apply(rule d(2)) - proof goal_cases - case 1 - show ?case + proof (rule *) + show "\(\(x,K)\p'. norm (content K *\<^sub>R f x)) - (\(x,k)\p'. norm (integral k f))\ < e/2" + using p'' sum_less_e2 unfolding split_def by (force intro!: absdiff_norm_less) + show "(\(x,k) \ p'. norm (integral k f)) \?S" by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper) - next - case 2 - have *: "{k \ l | k l. k \ d \ l \ snd ` p} = - (\(k,l). k \ l) ` {(k,l)|k l. k \ d \ l \ snd ` p}" - by auto - have "(\k\d. norm (integral k f)) \ (\i\d. \l\snd ` p. norm (integral (i \ l) f))" - proof (rule sum_mono, goal_cases) - case k: (1 k) - from d'(4)[OF this] guess u v by (elim exE) note uv=this - define d' where "d' = {cbox u v \ l |l. l \ snd ` p \ cbox u v \ l \ {}}" - note uvab = d'(2)[OF k[unfolded uv]] - have "d' division_of cbox u v" - apply (subst d'_def) - apply (rule division_inter_1) - apply (rule division_of_tagged_division[OF p(1)]) - apply (rule uvab) - done - then have "norm (integral k f) \ sum (\k. norm (integral k f)) d'" - unfolding uv - apply (subst integral_combine_division_topdown[of _ _ d']) - apply (rule integrable_on_subcbox[OF assms(1) uvab]) - apply assumption - apply (rule sum_norm_le) - apply auto - done - also have "\ = (\k\{k \ l |l. l \ snd ` p}. norm (integral k f))" - apply (rule sum.mono_neutral_left) - apply (subst Setcompr_eq_image) - apply (rule finite_imageI)+ - apply fact - unfolding d'_def uv - apply blast - proof (rule, goal_cases) - case prems: (1 i) - then have "i \ {cbox u v \ l |l. l \ snd ` p}" - by auto - from this[unfolded mem_Collect_eq] guess l .. note l=this - then have "cbox u v \ l = {}" - using prems by auto - then show ?case - using l by auto - qed - also have "\ = (\l\snd ` p. norm (integral (k \ l) f))" - unfolding Setcompr_eq_image - apply (rule sum.reindex_nontrivial [unfolded o_def]) - apply (rule finite_imageI) - apply (rule p') - proof goal_cases - case prems: (1 l y) - have "interior (k \ l) \ interior (l \ y)" - apply (subst(2) interior_Int) - by (metis Int_lower2 Int_subset_iff interior_mono prems(4)) - then have *: "interior (k \ l) = {}" - using snd_p(5)[OF prems(1-3)] by auto - from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this - show ?case - using * - unfolding uv Int_interval content_eq_0_interior[symmetric] - by auto - qed - finally show ?case . - qed - also have "\ = (\(i,l) \ d \ (snd ` p). norm (integral (i\l) f))" - apply (subst sum_Sigma_product[symmetric]) - apply fact - using p'(1) - apply auto - done - also have "\ = (\x\{(i, l) |i l. i \ d \ l \ snd ` p}. norm (integral (case_prod op \ x) f))" - by (force simp: split_def Sigma_def intro!: sum.cong) - also have "\ = (\k\{i \ l |i l. i \ d \ l \ snd ` p}. norm (integral k f))" - unfolding * - apply (rule sum.reindex_nontrivial [symmetric, unfolded o_def]) - apply (rule finite_product_dependent) - apply fact - apply (rule finite_imageI) - apply (rule p') - unfolding split_paired_all mem_Collect_eq split_conv o_def + show "(\k\d. norm (integral k f)) \ (\(x,k) \ p'. norm (integral k f))" proof - - note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)] - fix l1 l2 k1 k2 - assume as: - "(l1, k1) \ (l2, k2)" - "l1 \ k1 = l2 \ k2" - "\i l. (l1, k1) = (i, l) \ i \ d \ l \ snd ` p" - "\i l. (l2, k2) = (i, l) \ i \ d \ l \ snd ` p" - then have "l1 \ d" and "k1 \ snd ` p" - by auto from d'(4)[OF this(1)] *(1)[OF this(2)] - guess u1 v1 u2 v2 by (elim exE) note uv=this - have "l1 \ l2 \ k1 \ k2" - using as by auto - then have "interior k1 \ interior k2 = {} \ interior l1 \ interior l2 = {}" - by (metis Pair_inject \k1 \ snd ` p\ \l1 \ d\ as(4) d'(5) snd_p(5)) - moreover have "interior (l1 \ k1) = interior (l2 \ k2)" - using as(2) by auto - ultimately have "interior(l1 \ k1) = {}" - by auto - then show "norm (integral (l1 \ k1) f) = 0" - unfolding uv Int_interval - unfolding content_eq_0_interior[symmetric] - by auto - qed - also have "\ = (\(x, k)\p'. norm (integral k f))" - unfolding sum_p' - apply (rule sum.mono_neutral_right) - apply (subst *) - apply (rule finite_imageI[OF finite_product_dependent]) - apply fact - apply (rule finite_imageI[OF p'(1)]) - apply safe - proof goal_cases - case (2 i ia l a b) - then have "ia \ b = {}" - unfolding p'alt image_iff Bex_def not_ex - apply (erule_tac x="(a, ia \ b)" in allE) - apply auto - done - then show ?case + have *: "{k \ l | k l. k \ d \ l \ snd ` p} = (\(k,l). k \ l) ` (d \ snd ` p)" by auto - next - case (1 x a b) - then show ?case - unfolding p'_def + have "(\K\d. norm (integral K f)) \ (\i\d. \l\snd ` p. norm (integral (i \ l) f))" + proof (rule sum_mono) + fix K assume k: "K \ d" + from d'(4)[OF this] obtain u v where uv: "K = cbox u v" by metis + define d' where "d' = {cbox u v \ l |l. l \ snd ` p \ cbox u v \ l \ {}}" + have uvab: "cbox u v \ cbox a b" + using d(1) k uv by blast + have "d' division_of cbox u v" + unfolding d'_def by (rule division_inter_1 [OF snd_p_div uvab]) + moreover then have "norm (\i\d'. integral i f) \ (\k\d'. norm (integral k f))" + by (simp add: sum_norm_le) + ultimately have "norm (integral K f) \ sum (\k. norm (integral k f)) d'" + apply (subst integral_combine_division_topdown[of _ _ d']) + apply (auto simp: uv intro: integrable_on_subcbox[OF assms(1) uvab]) + done + also have "\ = (\I\{K \ L |L. L \ snd ` p}. norm (integral I f))" + proof - + have *: "norm (integral I f) = 0" + if "I \ {cbox u v \ l |l. l \ snd ` p}" + "I \ {cbox u v \ l |l. l \ snd ` p \ cbox u v \ l \ {}}" for I + using that by auto + show ?thesis + apply (rule sum.mono_neutral_left) + apply (simp add: snd_p(1)) + unfolding d'_def uv using * by auto + qed + also have "\ = (\l\snd ` p. norm (integral (K \ l) f))" + proof - + have *: "norm (integral (K \ l) f) = 0" + if "l \ snd ` p" "y \ snd ` p" "l \ y" "K \ l = K \ y" for l y + proof - + have "interior (K \ l) \ interior (l \ y)" + by (metis Int_lower2 interior_mono le_inf_iff that(4)) + then have "interior (K \ l) = {}" + by (simp add: snd_p(5) that) + moreover from d'(4)[OF k] snd_p(4)[OF that(1)] + obtain u1 v1 u2 v2 + where uv: "K = cbox u1 u2" "l = cbox v1 v2" by metis + ultimately show ?thesis + using that integral_null + unfolding uv Int_interval content_eq_0_interior + by (metis (mono_tags, lifting) norm_eq_zero) + qed + show ?thesis + unfolding Setcompr_eq_image + apply (rule sum.reindex_nontrivial [unfolded o_def]) + apply (rule finite_imageI) + apply (rule p') + using * by auto + qed + finally show "norm (integral K f) \ (\l\snd ` p. norm (integral (K \ l) f))" . + qed + also have "\ = (\(i,l) \ d \ snd ` p. norm (integral (i\l) f))" + by (simp add: sum.cartesian_product) + also have "\ = (\x \ d \ snd ` p. norm (integral (case_prod op \ x) f))" + by (force simp: split_def intro!: sum.cong) + also have "\ = (\k\{i \ l |i l. i \ d \ l \ snd ` p}. norm (integral k f))" proof - - assume "(a, b) \ {(x, k) |x k. \i l. x \ i \ i \ d \ (x, l) \ p \ k = i \ l}" - then have "\n N. (a, b) = (n, N) \ (\Na Nb. n \ Na \ Na \ d \ (n, Nb) \ p \ N = Na \ Nb)" - by force - then show ?thesis - by (metis (no_types) image_iff snd_conv) + have eq0: " (integral (l1 \ k1) f) = 0" + if "l1 \ k1 = l2 \ k2" "(l1, k1) \ (l2, k2)" + "l1 \ d" "(j1,k1) \ p" "l2 \ d" "(j2,k2) \ p" + for l1 l2 k1 k2 j1 j2 + proof - + obtain u1 v1 u2 v2 where uv: "l1 = cbox u1 u2" "k1 = cbox v1 v2" + using \(j1, k1) \ p\ \l1 \ d\ d'(4) p'(4) by blast + have "l1 \ l2 \ k1 \ k2" + using that by auto + then have "interior k1 \ interior k2 = {} \ interior l1 \ interior l2 = {}" + by (meson d'(5) old.prod.inject p'(5) that(3) that(4) that(5) that(6)) + moreover have "interior (l1 \ k1) = interior (l2 \ k2)" + by (simp add: that(1)) + ultimately have "interior(l1 \ k1) = {}" + by auto + then show ?thesis + unfolding uv Int_interval content_eq_0_interior[symmetric] by auto + qed + show ?thesis + unfolding * + apply (rule sum.reindex_nontrivial [OF fin_d_sndp, symmetric, unfolded o_def]) + apply clarsimp + by (metis eq0 fst_conv snd_conv) qed + also have "\ = (\(x,k) \ p'. norm (integral k f))" + proof - + have 0: "integral (ia \ snd (a, b)) f = 0" + if "ia \ snd (a, b) \ snd ` p'" "ia \ d" "(a, b) \ p" for ia a b + proof - + have "ia \ b = {}" + using that unfolding p'alt image_iff Bex_def not_ex + apply (erule_tac x="(a, ia \ b)" in allE) + apply auto + done + then show ?thesis by auto + qed + have 1: "\i l. snd (a, b) = i \ l \ i \ d \ l \ snd ` p" if "(a, b) \ p'" for a b + using that + apply (clarsimp simp: p'_def image_iff) + by (metis (no_types, hide_lams) snd_conv) + show ?thesis + unfolding sum_p' + apply (rule sum.mono_neutral_right) + apply (metis * finite_imageI[OF fin_d_sndp]) + using 0 1 by auto + qed + finally show ?thesis . qed - finally show ?case . - next - case 3 - let ?S = "{(x, i \ l) |x i l. (x, l) \ p \ i \ d}" - have *: "?S = (\(xl,i). (fst xl, snd xl \ i)) ` (p \ d)" - apply safe - unfolding image_iff - apply (rule_tac x="((x,l),i)" in bexI) - apply auto - done - note pdfin = finite_cartesian_product[OF p'(1) d'(1)] - have "(\(x, k)\p'. norm (content k *\<^sub>R f x)) = (\(x, k)\?S. \content k\ * norm (f x))" - unfolding norm_scaleR - apply (rule sum.mono_neutral_left) - apply (subst *) - apply (rule finite_imageI) - apply fact - unfolding p'alt - apply blast - apply safe - apply (rule_tac x=x in exI) - apply (rule_tac x=i in exI) - apply (rule_tac x=l in exI) - apply auto - done - also have "\ = (\((x,l),i)\p \ d. \content (l \ i)\ * norm (f x))" - unfolding * - apply (subst sum.reindex_nontrivial) - apply fact - unfolding split_paired_all - unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject - apply (elim conjE) + show "(\(x,k) \ p'. norm (content k *\<^sub>R f x)) = (\(x,k) \ p. content k *\<^sub>R norm (f x))" proof - - fix x1 l1 k1 x2 l2 k2 - assume as: "(x1, l1) \ p" "(x2, l2) \ p" "k1 \ d" "k2 \ d" - "x1 = x2" "l1 \ k1 = l2 \ k2" "\ ((x1 = x2 \ l1 = l2) \ k1 = k2)" - from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this - from as have "l1 \ l2 \ k1 \ k2" - by auto - then have "interior k1 \ interior k2 = {} \ interior l1 \ interior l2 = {}" - apply - - apply (erule disjE) - apply (rule disjI2) - defer - apply (rule disjI1) - apply (rule d'(5)[OF as(3-4)]) - apply assumption - apply (rule p'(5)[OF as(1-2)]) - apply auto - done - moreover have "interior (l1 \ k1) = interior (l2 \ k2)" - unfolding as .. - ultimately have "interior (l1 \ k1) = {}" - by auto - then show "\content (l1 \ k1)\ * norm (f x1) = 0" - unfolding uv Int_interval - unfolding content_eq_0_interior[symmetric] - by auto - qed safe - also have "\ = (\(x, k)\p. content k *\<^sub>R norm (f x))" - apply (subst sum_Sigma_product[symmetric]) - apply (rule p') - apply (rule d') - apply (rule sum.cong) - apply (rule refl) - unfolding split_paired_all split_conv - proof - - fix x l - assume as: "(x, l) \ p" - note xl = p'(2-4)[OF this] - from this(3) guess u v by (elim exE) note uv=this - have "(\i\d. \content (l \ i)\) = (\k\d. content (k \ cbox u v))" - by (simp add: Int_commute uv) - also have "\ = sum content {k \ cbox u v| k. k \ d}" - unfolding Setcompr_eq_image - apply (rule sum.reindex_nontrivial [unfolded o_def, symmetric]) - apply (rule d') - proof goal_cases - case prems: (1 k y) - from d'(4)[OF this(1)] d'(4)[OF this(2)] - guess u1 v1 u2 v2 by (elim exE) note uv=this - have "{} = interior ((k \ y) \ cbox u v)" - apply (subst interior_Int) - using d'(5)[OF prems(1-3)] - apply auto + let ?S = "{(x, i \ l) |x i l. (x, l) \ p \ i \ d}" + have *: "?S = (\(xl,i). (fst xl, snd xl \ i)) ` (p \ d)" + by force + have fin_pd: "finite (p \ d)" + using finite_cartesian_product[OF p'(1) d'(1)] by metis + have "(\(x,k) \ p'. norm (content k *\<^sub>R f x)) = (\(x,k) \ ?S. \content k\ * norm (f x))" + unfolding norm_scaleR + apply (rule sum.mono_neutral_left) + apply (subst *) + apply (rule finite_imageI [OF fin_pd]) + unfolding p'alt apply auto + by fastforce + also have "\ = (\((x,l),i)\p \ d. \content (l \ i)\ * norm (f x))" + proof - + have "\content (l1 \ k1)\ * norm (f x1) = 0" + if "(x1, l1) \ p" "(x2, l2) \ p" "k1 \ d" "k2 \ d" + "x1 = x2" "l1 \ k1 = l2 \ k2" "x1 \ x2 \ l1 \ l2 \ k1 \ k2" + for x1 l1 k1 x2 l2 k2 + proof - + obtain u1 v1 u2 v2 where uv: "k1 = cbox u1 u2" "l1 = cbox v1 v2" + by (meson \(x1, l1) \ p\ \k1 \ d\ d(1) division_ofD(4) p'(4)) + have "l1 \ l2 \ k1 \ k2" + using that by auto + then have "interior k1 \ interior k2 = {} \ interior l1 \ interior l2 = {}" + apply (rule disjE) + using that p'(5) d'(5) by auto + moreover have "interior (l1 \ k1) = interior (l2 \ k2)" + unfolding that .. + ultimately have "interior (l1 \ k1) = {}" + by auto + then show "\content (l1 \ k1)\ * norm (f x1) = 0" + unfolding uv Int_interval content_eq_0_interior[symmetric] by auto + qed + then show ?thesis + unfolding * + apply (subst sum.reindex_nontrivial [OF fin_pd]) + unfolding split_paired_all o_def split_def prod.inject + apply force+ done - also have "\ = interior (y \ (k \ cbox u v))" - by auto - also have "\ = interior (k \ cbox u v)" - unfolding prems(4) by auto - finally show ?case - unfolding uv Int_interval content_eq_0_interior .. qed - also have "\ = sum content {cbox u v \ k |k. k \ d \ cbox u v \ k \ {}}" - apply (rule sum.mono_neutral_right) - unfolding Setcompr_eq_image - apply (rule finite_imageI) - apply (rule d') - apply blast - apply safe - apply (rule_tac x=k in exI) - proof goal_cases - case prems: (1 i k) - from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this - have "interior (k \ cbox u v) \ {}" - using prems(2) - unfolding ab Int_interval content_eq_0_interior - by auto - then show ?case - using prems(1) - using interior_subset[of "k \ cbox u v"] - by auto + also have "\ = (\(x,k) \ p. content k *\<^sub>R norm (f x))" + proof - + have sumeq: "(\i\d. content (l \ i) * norm (f x)) = content l * norm (f x)" + if "(x, l) \ p" for x l + proof - + note xl = p'(2-4)[OF that] + then obtain u v where uv: "l = cbox u v" by blast + have "(\i\d. \content (l \ i)\) = (\k\d. content (k \ cbox u v))" + by (simp add: Int_commute uv) + also have "\ = sum content {k \ cbox u v| k. k \ d}" + proof - + have eq0: "content (k \ cbox u v) = 0" + if "k \ d" "y \ d" "k \ y" and eq: "k \ cbox u v = y \ cbox u v" for k y + proof - + from d'(4)[OF that(1)] d'(4)[OF that(2)] + obtain \ \ where \: "k \ cbox u v = cbox \ \" + by (meson Int_interval) + have "{} = interior ((k \ y) \ cbox u v)" + by (simp add: d'(5) that) + also have "\ = interior (y \ (k \ cbox u v))" + by auto + also have "\ = interior (k \ cbox u v)" + unfolding eq by auto + finally show ?thesis + unfolding \ content_eq_0_interior .. + qed + then show ?thesis + unfolding Setcompr_eq_image + apply (rule sum.reindex_nontrivial [OF \finite d\, unfolded o_def, symmetric]) + by auto + qed + also have "\ = sum content {cbox u v \ k |k. k \ d \ cbox u v \ k \ {}}" + apply (rule sum.mono_neutral_right) + unfolding Setcompr_eq_image + apply (rule finite_imageI [OF \finite d\]) + apply (fastforce simp: inf.commute)+ + done + finally show "(\i\d. content (l \ i) * norm (f x)) = content l * norm (f x)" + unfolding sum_distrib_right[symmetric] real_scaleR_def + apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]]) + using xl(2)[unfolded uv] unfolding uv apply auto + done + qed + show ?thesis + by (subst sum_Sigma_product[symmetric]) (auto intro!: sumeq sum.cong p' d') qed - finally show "(\i\d. \content (l \ i)\ * norm (f x)) = content l *\<^sub>R norm (f x)" - unfolding sum_distrib_right[symmetric] real_scaleR_def - apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]]) - using xl(2)[unfolded uv] - unfolding uv - apply auto - done + finally show ?thesis . qed - finally show ?case . - qed - qed + qed (rule d) + qed qed + then show ?thesis + using absolutely_integrable_onI [OF f has_integral_integrable] has_integral[of _ ?S] + by blast qed + lemma bounded_variation_absolutely_integrable: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes "f integrable_on UNIV" @@ -2169,43 +2096,40 @@ using \e > 0\ by auto from * [OF this] obtain d1 where d1: "gauge d1" "\p. p tagged_division_of (cbox a b) \ d1 fine p \ - norm ((\(x, k)\p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\x. norm (f x))) < e / 2" + norm ((\(x,k) \ p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\x. norm (f x))) < e/2" by auto from henstock_lemma [OF f(1) \e/2>0\] obtain d2 where d2: "gauge d2" "\p. p tagged_partial_division_of (cbox a b) \ d2 fine p \ - (\(x, k)\p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" . + (\(x,k) \ p. norm (content k *\<^sub>R f x - integral k f)) < e/2" . obtain p where p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p" by (rule fine_division_exists [OF gauge_Int [OF d1(1) d2(1)], of a b]) (auto simp add: fine_Int) - have *: "\sf sf' si di. sf' = sf \ si \ ?S \ \sf - si\ < e / 2 \ - \sf' - di\ < e / 2 \ di < ?S + e" + have *: "\sf sf' si di. sf' = sf \ si \ ?S \ \sf - si\ < e/2 \ + \sf' - di\ < e/2 \ di < ?S + e" by arith show "integral (cbox a b) (\x. if x \ UNIV then norm (f x) else 0) < ?S + e" apply (subst if_P) apply rule proof (rule *[rule_format]) - show "\(\(x,k)\p. norm (content k *\<^sub>R f x)) - (\(x,k)\p. norm (integral k f))\ < e / 2" + show "\(\(x,k)\p. norm (content k *\<^sub>R f x)) - (\(x,k)\p. norm (integral k f))\ < e/2" unfolding split_def - apply (rule helplemma) + apply (rule absdiff_norm_less) using d2(2)[rule_format,of p] using p(1,3) unfolding tagged_division_of_def split_def apply auto done - show "\(\(x, k)\p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\x. norm(f x))\ < e / 2" + show "\(\(x,k) \ p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\x. norm(f x))\ < e/2" using d1(2)[rule_format,OF conjI[OF p(1,2)]] by (simp only: real_norm_def) - show "(\(x, k)\p. content k *\<^sub>R norm (f x)) = (\(x, k)\p. norm (content k *\<^sub>R f x))" + show "(\(x,k) \ p. content k *\<^sub>R norm (f x)) = (\(x,k) \ p. norm (content k *\<^sub>R f x))" apply (rule sum.cong) apply (rule refl) unfolding split_paired_all split_conv apply (drule tagged_division_ofD(4)[OF p(1)]) - unfolding norm_scaleR - apply (subst abs_of_nonneg) - apply auto - done - show "(\(x, k)\p. norm (integral k f)) \ ?S" + by simp + show "(\(x,k) \ p. norm (integral k f)) \ ?S" using partial_division_of_tagged_division[of p "cbox a b"] p(1) apply (subst sum.over_tagged_division_lemma[OF p(1)]) apply (simp add: content_eq_0_interior) @@ -2678,11 +2602,12 @@ using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans) then have F_le_T: "a \ x \ F x \ T" for x by (intro tendsto_lowerbound[OF lim]) - (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder) + (auto simp: eventually_at_top_linorder) have "(SUP i::nat. ?f i x) = ?fR x" for x proof (rule LIMSEQ_unique[OF LIMSEQ_SUP]) - from reals_Archimedean2[of "x - a"] guess n .. + obtain n where "x - a < real n" + using reals_Archimedean2[of "x - a"] .. then have "eventually (\n. ?f n x = ?fR x) sequentially" by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator) then show "(\n. ?f n x) \ ?fR x" diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Aug 07 15:10:37 2017 +0200 @@ -9,6 +9,10 @@ Lebesgue_Measure Tagged_Division begin +lemma eps_leI: + assumes "(\e::'a::linordered_idom. 0 < e \ x < y + e)" shows "x \ y" + by (metis add_diff_eq assms diff_diff_add diff_gt_0_iff_gt linorder_not_less order_less_irrefl) + (*FIXME DELETE*) lemma conjunctD2: assumes "a \ b" shows a b using assms by auto @@ -1260,7 +1264,7 @@ lemma has_integral_separate_sides: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" - assumes "(f has_integral i) (cbox a b)" + assumes f: "(f has_integral i) (cbox a b)" and "e > 0" and k: "k \ Basis" obtains d where "gauge d" @@ -1268,18 +1272,23 @@ p2 tagged_division_of (cbox a b \ {x. x\k \ c}) \ d fine p2 \ norm ((sum (\(x,k). content k *\<^sub>R f x) p1 + sum (\(x,k). content k *\<^sub>R f x) p2) - i) < e" proof - - guess d using has_integralD[OF assms(1-2)] . note d=this + obtain \ where d: "gauge \" + "\p. \p tagged_division_of cbox a b; \ fine p\ + \ norm ((\(x, k)\p. content k *\<^sub>R f x) - i) < e" + using has_integralD[OF f \e > 0\] by metis { fix p1 p2 - assume "p1 tagged_division_of (cbox a b) \ {x. x \ k \ c}" "d fine p1" - note p1=tagged_division_ofD[OF this(1)] this - assume "p2 tagged_division_of (cbox a b) \ {x. c \ x \ k}" "d fine p2" - note p2=tagged_division_ofD[OF this(1)] this - note tagged_division_union_interval[OF p1(7) p2(7)] note p12 = tagged_division_ofD[OF this] this + assume tdiv1: "p1 tagged_division_of (cbox a b) \ {x. x \ k \ c}" and "\ fine p1" + note p1=tagged_division_ofD[OF this(1)] + assume tdiv2: "p2 tagged_division_of (cbox a b) \ {x. c \ x \ k}" and "\ fine p2" + note p2=tagged_division_ofD[OF this(1)] + note tagged_division_union_interval[OF tdiv1 tdiv2] + note p12 = tagged_division_ofD[OF this] this { fix a b assume ab: "(a, b) \ p1 \ p2" have "(a, b) \ p1" using ab by auto - with p1 obtain u v where uv: "b = cbox u v" by auto + obtain u v where uv: "b = cbox u v" + using \(a, b) \ p1\ p1(4) by moura have "b \ {x. x\k = c}" using ab p1(3)[of a b] p2(3)[of a b] by fastforce moreover @@ -1288,25 +1297,23 @@ assume "\ ?thesis" then obtain x where x: "x \ interior {x::'a. x\k = c}" by auto - then guess e unfolding mem_interior .. note e=this + then obtain \ where "0 < \" and \: "ball x \ \ {x. x \ k = c}" + using mem_interior by metis have x: "x\k = c" using x interior_subset by fastforce - have *: "\i. i \ Basis \ \(x - (x + (e / 2) *\<^sub>R k)) \ i\ = (if i = k then e/2 else 0)" - using e k by (auto simp: inner_simps inner_not_same_Basis) - have "(\i\Basis. \(x - (x + (e / 2 ) *\<^sub>R k)) \ i\) = - (\i\Basis. (if i = k then e / 2 else 0))" + have *: "\i. i \ Basis \ \(x - (x + (\ / 2) *\<^sub>R k)) \ i\ = (if i = k then \/2 else 0)" + using \0 < \\ k by (auto simp: inner_simps inner_not_same_Basis) + have "(\i\Basis. \(x - (x + (\ / 2 ) *\<^sub>R k)) \ i\) = + (\i\Basis. (if i = k then \ / 2 else 0))" using "*" by (blast intro: sum.cong) - also have "\ < e" - apply (subst sum.delta) - using e - apply auto - done - finally have "x + (e/2) *\<^sub>R k \ ball x e" + also have "\ < \" + by (subst sum.delta) (use \0 < \\ in auto) + finally have "x + (\/2) *\<^sub>R k \ ball x \" unfolding mem_ball dist_norm by(rule le_less_trans[OF norm_le_l1]) - then have "x + (e/2) *\<^sub>R k \ {x. x\k = c}" - using e by auto + then have "x + (\/2) *\<^sub>R k \ {x. x\k = c}" + using \ by auto then show False - unfolding mem_Collect_eq using e x k by (auto simp: inner_simps) + using \0 < \\ x k by (auto simp: inner_simps) qed ultimately have "content b = 0" unfolding uv content_eq_0_interior @@ -1318,11 +1325,11 @@ norm ((\(x, k)\p1 \ p2. content k *\<^sub>R f x) - i)" by (subst sum.union_inter_neutral) (auto simp: p1 p2) also have "\ < e" - by (rule k d(2) p12 fine_Un p1 p2)+ + using d(2) p12 by (simp add: fine_Un k \\ fine p1\ \\ fine p2\) finally have "norm ((\(x, k)\p1. content k *\<^sub>R f x) + (\(x, k)\p2. content k *\<^sub>R f x) - i) < e" . } then show ?thesis - by (auto intro: that[of d] d elim: ) + using d(1) that by auto qed lemma integrable_split [intro]: @@ -2463,53 +2470,39 @@ proof safe fix a b :: 'b show "\g. (\x\cbox a b. norm (f x - g x) \ e) \ g integrable_on cbox a b" - if "box a b = {}" + if "box a b = {}" for a b apply (rule_tac x=f in exI) - using assms that - apply (auto simp: content_eq_0_interior) - done + using assms that by (auto simp: content_eq_0_interior) { - fix c g - fix k :: 'b - assume as: "\x\cbox a b. norm (f x - g x) \ e" "g integrable_on cbox a b" + fix c g and k :: 'b + assume fg: "\x\cbox a b. norm (f x - g x) \ e" and g: "g integrable_on cbox a b" assume k: "k \ Basis" show "\g. (\x\cbox a b \ {x. x \ k \ c}. norm (f x - g x) \ e) \ g integrable_on cbox a b \ {x. x \ k \ c}" - "\g. (\x\cbox a b \ {x. c \ x \ k}. norm (f x - g x) \ e) \ g integrable_on cbox a b \ {x. c \ x \ k}" - apply (rule_tac[!] x=g in exI) - using as(1) integrable_split[OF as(2) k] - apply auto - done + "\g. (\x\cbox a b \ {x. c \ x \ k}. norm (f x - g x) \ e) \ g integrable_on cbox a b \ {x. c \ x \ k}" + apply (rule_tac[!] x=g in exI) + using fg integrable_split[OF g k] by auto } - fix c k g1 g2 - assume as: "\x\cbox a b \ {x. x \ k \ c}. norm (f x - g1 x) \ e" "g1 integrable_on cbox a b \ {x. x \ k \ c}" - "\x\cbox a b \ {x. c \ x \ k}. norm (f x - g2 x) \ e" "g2 integrable_on cbox 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\cbox a b. norm (f x - g x) \ e) \ g integrable_on cbox a b" - apply (rule_tac x="?g" in exI) - apply safe - proof goal_cases - case (1 x) - then show ?case - apply - - apply (cases "x\k=c") - apply (case_tac "x\k < c") - using as assms - apply auto - done - next - case 2 - presume "?g integrable_on cbox a b \ {x. x \ k \ c}" - and "?g integrable_on cbox 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 cbox a b \ {x. x \ k \ c}" "?g integrable_on cbox 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 + if fg1: "\x\cbox a b \ {x. x \ k \ c}. norm (f x - g1 x) \ e" + and g1: "g1 integrable_on cbox a b \ {x. x \ k \ c}" + and fg2: "\x\cbox a b \ {x. c \ x \ k}. norm (f x - g2 x) \ e" + and g2: "g2 integrable_on cbox a b \ {x. c \ x \ k}" + and k: "k \ Basis" + for c k g1 g2 + proof - + let ?g = "\x. if x\k = c then f x else if x\k \ c then g1 x else g2 x" + show "\g. (\x\cbox a b. norm (f x - g x) \ e) \ g integrable_on cbox a b" + proof (intro exI conjI ballI) + show "norm (f x - ?g x) \ e" if "x \ cbox a b" for x + by (auto simp: that assms fg1 fg2) + show "?g integrable_on cbox a b" + proof - + have "?g integrable_on cbox a b \ {x. x \ k \ c}" "?g integrable_on cbox a b \ {x. x \ k \ c}" + by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+ + with has_integral_split[OF _ _ k] show ?thesis + unfolding integrable_on_def by blast + qed + qed qed qed @@ -2524,18 +2517,16 @@ lemma approximable_on_division: fixes f :: "'b::euclidean_space \ 'a::banach" assumes "0 \ e" - and "d division_of (cbox a b)" - and "\i\d. \g. (\x\i. norm (f x - g x) \ e) \ g integrable_on i" + and d: "d division_of (cbox a b)" + and f: "\i\d. \g. (\x\i. norm (f x - g x) \ e) \ g integrable_on i" obtains g where "\x\cbox a b. norm (f x - g x) \ e" "g integrable_on cbox a b" proof - - note * = comm_monoid_set.operative_division[OF comm_monoid_set_and operative_approximable[OF assms(1)] assms(2)] - from assms(3) this[unfolded comm_monoid_set_F_and, of f] division_of_finite[OF assms(2)] - guess g by auto - then show thesis - apply - - apply (rule that[of g]) - apply auto - done + note * = comm_monoid_set.operative_division + [OF comm_monoid_set_and operative_approximable[OF \0 \ e\] d] + have "finite d" + by (rule division_of_finite[OF d]) + with f *[unfolded comm_monoid_set_F_and, of f] that show thesis + by auto qed lemma integrable_continuous: @@ -2669,18 +2660,22 @@ 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})" + and vecd: "\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 box_real[symmetric] 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] + assume "e > 0" + then have "\x. \d>0. + x \ {a..b} \ + (\y\{a..b}. + norm (y - x) < d \ norm (f y - f x - (y - x) *\<^sub>R f' x) \ e * norm (y - x))" + using vecd[unfolded has_vector_derivative_def has_derivative_within_alt] by blast + then obtain d where d: "\x. 0 < d x" + "\x y. \x \ {a..b}; y \ {a..b}; norm (y - x) < d x\ + \ norm (f y - f x - (y - x) *\<^sub>R f' x) \ e * norm (y - x)" + by metis + show "\d. gauge d \ (\p. p tagged_division_of (cbox a b) \ d fine p \ norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content (cbox a b))" apply (rule_tac x="\x. ball x (d x)" in exI) @@ -2701,7 +2696,7 @@ 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 + then obtain u v where k: "k = cbox u v" by blast have *: "u \ v" using xk unfolding k by auto have ball: "\xa\k. xa \ ball x (d x)" @@ -2907,10 +2902,9 @@ 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" + then obtain k c d where k: "k \ s" "content k = 0" "k = cbox c d" + using s(4) by blast + then 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) @@ -2933,9 +2927,9 @@ fix x fix e :: real assume as: "x \ k" "e > 0" - from k(2)[unfolded k content_eq_0] guess i .. - then have i:"c\i = d\i" "i\Basis" - using s(3)[OF k(1),unfolded k] unfolding box_ne_empty by auto + obtain i where i: "c\i = d\i" "i\Basis" + using k(2) s(3)[OF k(1)] unfolding box_ne_empty k + by (metis dual_order.antisym content_eq_0) then have xi: "x\i = d\i" using as unfolding k mem_box by (metis antisym) define y where "y = (\j\Basis. (if j = i then if c\i \ (a\i + b\i) / 2 then c\i + @@ -3114,42 +3108,30 @@ f integrable_on cbox u v" shows "f integrable_on cbox a b" proof - - have "\x. \d. x\cbox a b \ d>0 \ (\u v. x \ cbox u v \ cbox u v \ ball x d \ cbox u v \ cbox a b \ + have "\x. \d>0. x\cbox a b \ (\u v. x \ cbox u v \ cbox u v \ ball x d \ cbox u v \ cbox a b \ f integrable_on cbox 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 + using assms by (metis zero_less_one) + then obtain d where d: "\x. 0 < d x" + "\x u v. \x \ cbox a b; x \ cbox u v; cbox u v \ ball x (d x); cbox u v \ cbox a b\ + \ f integrable_on cbox u v" + by metis + obtain p where p: "p tagged_division_of cbox a b" "(\x. ball x (d x)) fine p" + using fine_division_exists[OF gauge_ball_dependent,of d a b] d(1) by blast + then have sndp: "snd ` p division_of cbox a b" + by (metis division_of_tagged_division) + have "f integrable_on k" if "(x, k) \ p" for x k + using tagged_division_ofD(2-4)[OF p(1) that] fineD[OF p(2) that] d[of x] by auto + then show ?thesis + unfolding comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable sndp, symmetric] + comm_monoid_set_F_and by auto - note p=this(1-2) - note division_of_tagged_division[OF this(1)] - note * = comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable, OF this, symmetric, of f] - show ?thesis - unfolding * comm_monoid_set_F_and - 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 intro: order.trans) - done - qed qed subsection \Second FTC or existence of antiderivative.\ lemma integrable_const[intro]: "(\x. c) integrable_on cbox a b" - unfolding integrable_on_def - apply rule - apply (rule has_integral_const) - done + unfolding integrable_on_def by blast lemma integral_has_vector_derivative_continuous_at: fixes f :: "real \ 'a::banach" @@ -3239,22 +3221,18 @@ 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]) - apply safe - proof goal_cases - case prems: (1 u v) + obtain g + where g: "\x. x \ {a..b} \ (g has_vector_derivative f x) (at x within {a..b})" + using antiderivative_continuous[OF assms] by metis + have "(f has_integral g v - g u) {u..v}" if "u \ {a..b}" "v \ {a..b}" "u \ v" for u v + proof - have "\x\cbox u v. (g has_vector_derivative f x) (at x within cbox u v)" - apply rule - apply (rule has_vector_derivative_within_subset) - apply (rule g[rule_format]) - using prems(1,2) - apply auto - done - then show ?case - using fundamental_theorem_of_calculus[OF prems(3), of g f] by auto + by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2)) + then show ?thesis + by (simp add: fundamental_theorem_of_calculus that(3)) qed + then show ?thesis + using that by blast qed @@ -3268,7 +3246,7 @@ and "\u v. \w z. g ` cbox u v = cbox w z" and h: "\u v. \w z. h ` cbox u v = cbox w z" and "\u v. content(g ` cbox u v) = r * content (cbox u v)" - and "(f has_integral i) (cbox a b)" + and intfi: "(f has_integral i) (cbox a b)" shows "((\x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` cbox a b)" proof - show ?thesis when *: "cbox a b \ {} \ ?thesis" @@ -3282,22 +3260,11 @@ unfolding prems assms(8)[unfolded prems has_integral_empty_eq] by auto qed assume "cbox a b \ {}" - from assms(6)[rule_format,of a b] guess w z by (elim exE) note wz=this + obtain w z where wz: "h ` cbox a b = cbox w z" + using h by blast 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 + apply (metis assms(2) injI) + by (metis assms(3) injI) from h obtain ha hb where h_eq: "h ` cbox a b = cbox ha hb" by blast show ?thesis unfolding h_eq has_integral @@ -3305,12 +3272,17 @@ proof safe fix e :: real assume e: "e > 0" - with assms(1) have "e * r > 0" by simp - from assms(8)[unfolded has_integral,rule_format,OF this] guess d by (elim exE conjE) note d=this[rule_format] + with \0 < r\ have "e * r > 0" by simp + with intfi[unfolded has_integral] + obtain d where d: "gauge d" + "\p. p tagged_division_of cbox a b \ d fine p + \ norm ((\(x, k)\p. content k *\<^sub>R f x) - i) < e * r" + by metis define d' where "d' x = {y. g y \ d (g x)}" for 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 ` cbox a b \ d fine p \ norm ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)" + show "\d. gauge d \ (\p. p tagged_division_of h ` cbox 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) @@ -3377,16 +3349,10 @@ assume "x \ cbox 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 obtain X y where "h x \ X" "(y, X) \ p" by blast 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 + apply (clarsimp simp: ) + by (metis (no_types, lifting) assms(3) image_eqI pair_imageI) qed note ** = d(2)[OF this] have *: "inj_on (\(x, k). (g x, g ` k)) p" @@ -3626,8 +3592,8 @@ lemma fundamental_theorem_of_calculus_interior: fixes f :: "real \ 'a::real_normed_vector" assumes "a \ b" - and "continuous_on {a .. b} f" - and "\x\{a <..< b}. (f has_vector_derivative f'(x)) (at x)" + and contf: "continuous_on {a .. b} f" + and derf: "\x. x \ {a <..< b} \ (f has_vector_derivative f'(x)) (at x)" shows "(f' has_integral (f b - f a)) {a .. b}" proof - { @@ -3655,29 +3621,30 @@ { presume "\e. e > 0 \ ?P e" then show ?thesis unfolding has_integral_factor_content_real 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\box a b. \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] + note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt] + have bounded: "\x. x \ {a<.. bounded_linear (\u. u *\<^sub>R f' x)" + using derf_exp by simp + have "\x \ box a b. \d>0. \y. norm (y - x) < d \ norm (f y - f x - (y - x) *\<^sub>R f' x) \ e/2 * norm (y - x)" + (is "\x \ box a b. ?Q x") + proof + fix x assume x: "x \ box a b" + show "?Q x" + apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]]) + using x e by auto + qed + from this [unfolded bgauge_existence_lemma] + obtain d where d: "\x. 0 < d x" + "\x y. \x \ box a b; norm (y - x) < d x\ + \ norm (f y - f x - (y - x) *\<^sub>R f' x) \ e / 2 * norm (y - x)" + by metis have "bounded (f ` cbox a b)" apply (rule compact_imp_bounded compact_continuous_image)+ using compact_cbox assms apply auto done - from this[unfolded bounded_pos] guess B .. note B = this[rule_format] - + from this[unfolded bounded_pos] obtain B + where "0 < B" and B: "\x. x \ f ` cbox a b \ norm x \ B" + by metis 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 - @@ -3700,7 +3667,7 @@ apply (auto simp add: field_simps) done qed - then guess l .. note l = conjunctD2[OF this] + then obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \ e * (b - a) / 8" by metis show ?thesis apply (rule_tac x="min k l" in exI) apply safe @@ -3715,24 +3682,28 @@ by (rule norm_triangle_ineq4) also have "\ \ e * (b - a) / 8 + e * (b - a) / 8" proof (rule add_mono) - have "\c - a\ \ \l\" - using as' by auto - then show "norm ((c - a) *\<^sub>R f' a) \ e * (b - a) / 8" - apply - - apply (rule order_trans[OF _ l(2)]) + have "norm ((c - a) *\<^sub>R f' a) \ norm (l *\<^sub>R f' a)" unfolding norm_scaleR apply (rule mult_right_mono) - apply auto - done + using as' by auto + also have "... \ e * (b - a) / 8" + by (rule l) + finally show "norm ((c - a) *\<^sub>R f' a) \ e * (b - a) / 8" . next - show "norm (f c - f a) \ e * (b - a) / 8" - 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 + have "norm (f c - f a) < e * (b - a) / 8" + proof (cases "a = c") + case True + then show ?thesis + using \0 < e * (b - a) / 8\ by auto + next + case False + show ?thesis + apply (rule k(2)[unfolded dist_norm]) + using as' False + apply (auto simp add: field_simps) + done + qed + then show "norm (f c - f a) \ e * (b - a) / 8" by simp 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 @@ -3748,20 +3719,23 @@ 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) - 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" + from *[OF this] obtain k + where k: "0 < k" + "\x. \x \ {a..b}; 0 < dist x b \ dist x b < k\ + \ dist (f x) (f b) < e * (b - a) / 8" + by blast + obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \ (e * (b - a)) / 8" proof (cases "f' b = 0") case True - thus ?thesis using ab e by auto + thus ?thesis using ab e that by auto next case False then show ?thesis - apply (rule_tac x="(e * (b - a)) / 8 / norm (f' b)" in exI) + apply (rule_tac l="(e * (b - a)) / 8 / norm (f' b)" in that) 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 @@ -3818,7 +3792,7 @@ note p = tagged_division_ofD[OF as(1)] have pA: "p = (p \ ?A) \ (p - ?A)" "finite (p \ ?A)" "finite (p - ?A)" "(p \ ?A) \ (p - ?A) = {}" using as by auto - note * = additive_tagged_division_1'[OF assms(1) as(1), symmetric] + note * = additive_tagged_division_1[OF assms(1) as(1), symmetric] have **: "\n1 s1 n2 s2::real. n2 \ s2 / 2 \ n1 - s1 \ s2 / 2 \ n1 + n2 \ s1 + s2" by arith show ?case @@ -3842,11 +3816,12 @@ assume xk: "(x, k) \ p" "e * (Sup k - Inf k) / 2 < norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))" - from p(4)[OF this(1)] guess u v by (elim exE) note k=this + obtain u v where k: "k = cbox u v" + using p(4) xk(1) by blast then have "u \ v" and uv: "{u, v} \ cbox u v" using p(2)[OF xk(1)] by auto - note result = xk(2)[unfolded k box_real interval_bounds_real[OF this(1)] content_real[OF this(1)]] - + then have result: "e * (v - u) / 2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))" + using xk(2)[unfolded k box_real interval_bounds_real content_real] by auto assume as': "x \ a" "x \ b" then have "x \ box a b" using p(2-3)[OF xk(1)] by (auto simp: mem_box) @@ -3910,7 +3885,8 @@ 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 + then obtain u v where uv: "k = cbox u v" + using p(4) by blast have "k \ {}" using p(2)[OF xk(1)] by auto then have *: "u = v" @@ -3952,9 +3928,10 @@ let ?B = "\x. {t \ p. fst t = x \ content (snd t) \ 0}" have pa: "\v. k = cbox a v \ a \ v" if "(a, k) \ p" for k proof - - guess u v using p(4)[OF that] by (elim exE) note uv=this - have *: "u \ v" - using p(2)[OF that] unfolding uv by auto + obtain u v where uv: "k = cbox u v" + using \(a, k) \ p\ p(4) by blast + then have *: "u \ v" + using p(2)[OF that] by auto have u: "u = a" proof (rule ccontr) have "u \ cbox u v" @@ -3975,7 +3952,8 @@ qed have pb: "\v. k = cbox v b \ b \ v" if "(b, k) \ p" for k proof - - guess u v using p(4)[OF that] by (elim exE) note uv=this + obtain u v where uv: "k = cbox u v" + using \(b, k) \ p\ p(4) by blast have *: "u \ v" using p(2)[OF that] unfolding uv by auto have u: "v = b" @@ -6814,68 +6792,72 @@ and "\x\s. norm (f x) \ g x" shows "norm (integral s f) \ integral s g" proof - - have *: "\x y. (\e::real. 0 < e \ x < y + e) \ x \ y" - apply (rule ccontr) - apply (erule_tac x="x - y" in allE) - apply auto - done have norm: "norm ig < dia + e" - if "norm sg \ dsa" - and "\dsa - dia\ < e / 2" - and "norm (sg - ig) < e / 2" + if "norm sg \ dsa" and "\dsa - dia\ < e / 2" and "norm (sg - ig) < e / 2" for e dsa dia and sg ig :: 'a apply (rule le_less_trans[OF norm_triangle_sub[of ig sg]]) apply (subst real_sum_of_halves[of e,symmetric]) unfolding add.assoc[symmetric] apply (rule add_le_less_mono) - defer - apply (subst norm_minus_commute) - apply (rule that(3)) + defer + apply (subst norm_minus_commute) + apply (rule that(3)) apply (rule order_trans[OF that(1)]) using that(2) apply arith done have lem: "norm (integral(cbox a b) f) \ integral (cbox a b) g" - if "f integrable_on cbox a b" - and "g integrable_on cbox a b" - and "\x\cbox a b. norm (f x) \ g x" + if f: "f integrable_on cbox a b" + and g: "g integrable_on cbox a b" + and nle: "\x. x \ cbox a b \ norm (f x) \ g x" for f :: "'n \ 'a" and g a b - proof (rule *[rule_format]) + proof (rule eps_leI) fix e :: real assume "e > 0" - then have *: "e/2 > 0" + then have e: "e/2 > 0" by auto - from integrable_integral[OF that(1),unfolded has_integral[of f],rule_format,OF *] - guess d1 .. note d1 = conjunctD2[OF this,rule_format] - from integrable_integral[OF that(2),unfolded has_integral[of g],rule_format,OF *] - guess d2 .. note d2 = conjunctD2[OF this,rule_format] - note gauge_Int[OF d1(1) d2(1)] - from fine_division_exists[OF this, of a b] guess p . note p=this + with integrable_integral[OF f,unfolded has_integral[of f]] + obtain \ where \: "gauge \" + "\p. p tagged_division_of cbox a b \ \ fine p + \ norm ((\(x, k)\p. content k *\<^sub>R f x) - integral (cbox a b) f) < e / 2" + by meson + moreover + from integrable_integral[OF g,unfolded has_integral[of g]] e + obtain \ where \: "gauge \" + "\p. p tagged_division_of cbox a b \ \ fine p + \ norm ((\(x, k)\p. content k *\<^sub>R g x) - integral (cbox a b) g) < e / 2" + by meson + ultimately have "gauge (\x. \ x \ \ x)" + using gauge_Int by blast + with fine_division_exists obtain p + where p: "p tagged_division_of cbox a b" "(\x. \ x \ \ x) fine p" + by metis + have "\ fine p" "\ fine p" + using fine_Int p(2) by blast+ show "norm (integral (cbox a b) f) < integral (cbox a b) g + e" - apply (rule norm) - defer - apply (rule d2(2)[OF conjI[OF p(1)],unfolded real_norm_def]) - defer - apply (rule d1(2)[OF conjI[OF p(1)]]) - defer - apply (rule sum_norm_le) - proof safe - fix x k - assume "(x, k) \ p" - note as = tagged_division_ofD(2-4)[OF p(1) this] - from this(3) guess u v by (elim exE) note uv=this - show "norm (content k *\<^sub>R f x) \ content k *\<^sub>R g x" - unfolding uv norm_scaleR - unfolding abs_of_nonneg[OF content_pos_le] real_scaleR_def - apply (rule mult_left_mono) - using that(3) as - apply auto - done - qed (insert p[unfolded fine_Int], auto) + proof (rule norm) + have "norm (content K *\<^sub>R f x) \ content K *\<^sub>R g x" if "(x, K) \ p" for x K + proof- + have K: "x \ K" "K \ cbox a b" + using \(x, K) \ p\ p(1) by blast+ + obtain u v where "K = cbox u v" + using \(x, K) \ p\ p(1) by blast + moreover have "content K * norm (f x) \ content K * g x" + by (metis K subsetD dual_order.antisym measure_nonneg mult_zero_left nle not_le real_mult_le_cancel_iff2) + then show ?thesis + by simp + qed + then show "norm (\(x, k)\p. content k *\<^sub>R f x) \ (\(x, k)\p. content k *\<^sub>R g x)" + by (simp add: sum_norm_le split_def) + show "norm ((\(x, k)\p. content k *\<^sub>R f x) - integral (cbox a b) f) < e / 2" + using \\ fine p\ \ p(1) by simp + show "\(\(x, k)\p. content k *\<^sub>R g x) - integral (cbox a b) g\ < e / 2" + using \\ fine p\ \ p(1) by simp + qed qed { presume "\e. 0 < e \ norm (integral s f) < integral s g + e" - then show ?thesis by (rule *[rule_format]) auto } + then show ?thesis by (rule eps_leI) auto } fix e :: real assume "e > 0" then have e: "e/2 > 0" @@ -6903,7 +6885,6 @@ defer apply (rule w(2)[unfolded real_norm_def]) apply (rule z(2)) - apply safe apply (case_tac "x \ s") unfolding if_P apply (rule assms(3)[rule_format]) @@ -6911,6 +6892,7 @@ done qed + lemma integral_norm_bound_integral_component: fixes f :: "'n::euclidean_space \ 'a::banach" fixes g :: "'n \ 'b::euclidean_space" diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Analysis/Tagged_Division.thy --- a/src/HOL/Analysis/Tagged_Division.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/Analysis/Tagged_Division.thy Mon Aug 07 15:10:37 2017 +0200 @@ -1836,15 +1836,6 @@ 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 "sum (\(x,k). f (Sup k) - f(Inf k)) p = f b - f a" - using additive_tagged_division_1[OF _ assms(2), of f] - using assms(1) - by auto - subsection \Fine-ness of a partition w.r.t. a gauge.\ definition fine (infixr "fine" 46) diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/Equiv_Relations.thy Mon Aug 07 15:10:37 2017 +0200 @@ -5,7 +5,7 @@ section \Equivalence Relations in Higher-Order Set Theory\ theory Equiv_Relations - imports Groups_Big Relation + imports Groups_Big begin subsection \Equivalence relations -- set version\ diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/Groups_Big.thy Mon Aug 07 15:10:37 2017 +0200 @@ -8,7 +8,7 @@ section \Big sum and product over finite (non-empty) sets\ theory Groups_Big - imports Finite_Set Power + imports Power begin subsection \Generic monoid operation over a set\ diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/Lattices_Big.thy Mon Aug 07 15:10:37 2017 +0200 @@ -6,7 +6,7 @@ section \Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\ theory Lattices_Big -imports Finite_Set Option + imports Option begin subsection \Generic lattice operations over a set\ diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/List.thy --- a/src/HOL/List.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/List.thy Mon Aug 07 15:10:37 2017 +0200 @@ -4796,7 +4796,7 @@ qed lemma card_lists_distinct_length_eq: - assumes "k < card A" + assumes "finite A" "k \ card A" shows "card {xs. length xs = k \ distinct xs \ set xs \ A} = \{card A - k + 1 .. card A}" using assms proof (induct k) @@ -4808,25 +4808,32 @@ let "?k_list" = "\k xs. length xs = k \ distinct xs \ set xs \ A" have inj_Cons: "\A. inj_on (\(xs, n). n # xs) A" by (rule inj_onI) auto - from Suc have "k < card A" by simp - moreover have "finite A" using assms by (simp add: card_ge_0_finite) + from Suc have "k \ card A" by simp + moreover note \finite A\ moreover have "finite {xs. ?k_list k xs}" by (rule finite_subset) (use finite_lists_length_eq[OF \finite A\, of k] in auto) moreover have "\i j. i \ j \ {i} \ (A - set i) \ {j} \ (A - set j) = {}" by auto - moreover have "\i. i \Collect (?k_list k) \ card (A - set i) = card A - k" + moreover have "\i. i \ {xs. ?k_list k xs} \ card (A - set i) = card A - k" by (simp add: card_Diff_subset distinct_card) moreover have "{xs. ?k_list (Suc k) xs} = (\(xs, n). n#xs) ` \((\xs. {xs} \ (A - set xs)) ` {xs. ?k_list k xs})" by (auto simp: length_Suc_conv) - moreover - have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp + moreover have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp then have "(card A - k) * \{Suc (card A - k)..card A} = \{Suc (card A - Suc k)..card A}" by (subst prod.insert[symmetric]) (simp add: atLeastAtMost_insertL)+ ultimately show ?case by (simp add: card_image inj_Cons card_UN_disjoint Suc.hyps algebra_simps) qed +lemma card_lists_distinct_length_eq': + assumes "k < card A" + shows "card {xs. length xs = k \ distinct xs \ set xs \ A} = \{card A - k + 1 .. card A}" +proof - + from \k < card A\ have "finite A" and "k \ card A" using card_infinite by force+ + from this show ?thesis by (rule card_lists_distinct_length_eq) +qed + lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)" apply (rule notI) apply (drule finite_maxlen) diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Option.thy --- a/src/HOL/Option.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/Option.thy Mon Aug 07 15:10:37 2017 +0200 @@ -5,7 +5,7 @@ section \Datatype option\ theory Option -imports Lifting Finite_Set + imports Lifting begin datatype 'a option = diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Partial_Function.thy --- a/src/HOL/Partial_Function.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/Partial_Function.thy Mon Aug 07 15:10:37 2017 +0200 @@ -5,8 +5,8 @@ section \Partial Function Definitions\ theory Partial_Function -imports Complete_Partial_Order Fun_Def_Base Option -keywords "partial_function" :: thy_decl + imports Complete_Partial_Order Option + keywords "partial_function" :: thy_decl begin named_theorems partial_function_mono "monotonicity rules for partial function definitions" diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 07 15:10:37 2017 +0200 @@ -207,8 +207,6 @@ (* E *) -fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS - val e_smartN = "smart" val e_autoN = "auto" val e_fun_weightN = "fun_weight" @@ -277,23 +275,19 @@ (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "") end +val e_tff0 = TFF Monomorphic + val e_config : atp_config = - {exec = fn full_proofs => (["E_HOME"], - if full_proofs orelse not (is_e_at_least_1_8 ()) then ["eproof_ram", "eproof"] - else ["eprover"]), - arguments = fn ctxt => fn full_proofs => fn heuristic => fn timeout => fn file_name => + {exec = fn _ => (["E_HOME"], ["eprover"]), + arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn file_name => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => - (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^ - "--tstp-in --tstp-out --silent " ^ + "--auto-schedule --tstp-in --tstp-out --silent " ^ e_selection_weight_arguments ctxt heuristic sel_weights ^ e_term_order_info_arguments gen_weights gen_prec ord_info ^ "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ - (if full_proofs orelse not (is_e_at_least_1_8 ()) then - " --output-level=5 --pcl-shell-level=" ^ (if full_proofs then "0" else "2") - else - " --proof-object=1") ^ - " " ^ file_name, + " --proof-object=1 " ^ + file_name, proof_delims = [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ tstp_proof_delims, @@ -306,14 +300,14 @@ let val heuristic = Config.get ctxt e_selection_heuristic in (* FUDGE *) if heuristic = e_smartN then - [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)), - (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)), - (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)), - (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)), - (0.15, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN)), - (0.25, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN))] + [(0.15, (((128, meshN), e_tff0, "mono_native", combsN, false), e_fun_weightN)), + (0.15, (((128, mashN), e_tff0, "mono_native", combsN, false), e_sym_offset_weightN)), + (0.15, (((91, mepoN), e_tff0, "mono_native", combsN, false), e_autoN)), + (0.15, (((1000, meshN), e_tff0, "poly_guards??", combsN, false), e_sym_offset_weightN)), + (0.15, (((256, mepoN), e_tff0, "mono_native", liftingN, false), e_fun_weightN)), + (0.25, (((64, mashN), e_tff0, "mono_native", combsN, false), e_fun_weightN))] else - [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))] + [(1.0, (((500, ""), e_tff0, "mono_native", combsN, false), heuristic))] end, best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -456,9 +450,8 @@ val spass_extra_options = Attrib.setup_config_string @{binding atp_spass_extra_options} (K "") -(* FIXME: Make "SPASS_NEW_HOME" legacy. *) val spass_config : atp_config = - {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]), + {exec = K (["SPASS_HOME"], ["SPASS"]), arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ => "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ @@ -710,7 +703,7 @@ (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] - (K (((750, ""), FOF, "mono_tags??", combsN, false), "") (* FUDGE *)) + (K (((750, ""), e_tff0, "mono_native", combsN, false), "") (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) @@ -724,7 +717,7 @@ remotify_atp satallax "Satallax" ["2.7", "2.3", "2"] (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_vampire = - remotify_atp vampire "Vampire" ["4.0", "3.0", "2.6"] + remotify_atp vampire "Vampire" ["4.2", "4.0"] (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Tools/value_command.ML --- a/src/HOL/Tools/value_command.ML Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/Tools/value_command.ML Mon Aug 07 15:10:37 2017 +0200 @@ -17,9 +17,7 @@ fun default_value ctxt t = if null (Term.add_frees t []) - then case try (Code_Evaluation.dynamic_value_strict ctxt) t of - SOME t' => t' - | NONE => Nbe.dynamic_value ctxt t + then Code_Evaluation.dynamic_value_strict ctxt t else Nbe.dynamic_value ctxt t; structure Evaluator = Theory_Data diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/ex/Adhoc_Overloading_Examples.thy --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Mon Aug 07 15:10:37 2017 +0200 @@ -38,7 +38,7 @@ adhoc_overloading vars term_vars -value "vars (Fun ''f'' [Var 0, Var 1])" +value [nbe] "vars (Fun ''f'' [Var 0, Var 1])" fun rule_vars :: "('a, 'b) term \ ('a, 'b) term \ 'b set" where "rule_vars (l, r) = vars l \ vars r" @@ -46,7 +46,7 @@ adhoc_overloading vars rule_vars -value "vars (Var 1, Var 0)" +value [nbe] "vars (Var 1, Var 0)" definition trs_vars :: "(('a, 'b) term \ ('a, 'b) term) set \ 'b set" where "trs_vars R = \(rule_vars ` R)" @@ -54,7 +54,7 @@ adhoc_overloading vars trs_vars -value "vars {(Var 1, Var 0)}" +value [nbe] "vars {(Var 1, Var 0)}" text \Sometimes it is necessary to add explicit type constraints before a variant can be determined.\ diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/ex/Normalization_by_Evaluation.thy --- a/src/HOL/ex/Normalization_by_Evaluation.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy Mon Aug 07 15:10:37 2017 +0200 @@ -68,20 +68,20 @@ lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization rule lemma "rev [a, b, c] = [c, b, a]" by normalization -value "rev (a#b#cs) = rev cs @ [b, a]" -value "map (%F. F [a,b,c::'x]) (map map [f,g,h])" -value "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))" -value "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])" +value [nbe] "rev (a#b#cs) = rev cs @ [b, a]" +value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])" +value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))" +value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])" lemma "map (%x. case x of None \ False | Some y \ True) [None, Some ()] = [False, True]" by normalization -value "case xs of [] \ True | x#xs \ False" -value "map (%x. case x of None \ False | Some y \ True) xs = P" +value [nbe] "case xs of [] \ True | x#xs \ False" +value [nbe] "map (%x. case x of None \ False | Some y \ True) xs = P" lemma "let x = y in [x, x] = [y, y]" by normalization lemma "Let y (%x. [x,x]) = [y, y]" by normalization -value "case n of Z \ True | S x \ False" +value [nbe] "case n of Z \ True | S x \ False" lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization -value "filter (%x. x) ([True,False,x]@xs)" -value "filter Not ([True,False,x]@xs)" +value [nbe] "filter (%x. x) ([True,False,x]@xs)" +value [nbe] "filter Not ([True,False,x]@xs)" lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization @@ -106,7 +106,7 @@ lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization lemma "max (Suc 0) 0 = Suc 0" by normalization lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization -value "Suc 0 \ set ms" +value [nbe] "Suc 0 \ set ms" (* non-left-linear patterns, equality by extensionality *) @@ -115,13 +115,13 @@ lemma "(f o g) x = f (g x)" by normalization lemma "(f o id) x = f x" by normalization lemma "(id :: bool \ bool) = id" by normalization -value "(\x. x)" +value [nbe] "(\x. x)" (* Church numerals: *) -value "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" -value "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" -value "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" +value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" +value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" +value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" (* handling of type classes in connection with equality *) diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/ex/Transitive_Closure_Table_Ex.thy --- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy Fri Aug 04 18:03:50 2017 +0200 +++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy Mon Aug 07 15:10:37 2017 +0200 @@ -24,7 +24,7 @@ values "{x. test\<^sup>*\<^sup>* A x}" values "{x. test\<^sup>*\<^sup>* x C}" -value "test\<^sup>*\<^sup>* A C" -value "test\<^sup>*\<^sup>* C A" +value [nbe] "test\<^sup>*\<^sup>* A C" +value [nbe] "test\<^sup>*\<^sup>* C A" end diff -r 1f66c7d77002 -r a8b89392ecb6 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Fri Aug 04 18:03:50 2017 +0200 +++ b/src/Pure/System/isabelle_tool.scala Mon Aug 07 15:10:37 2017 +0200 @@ -115,6 +115,7 @@ Options.isabelle_tool, Profiling_Report.isabelle_tool, Remote_DMG.isabelle_tool, + Server.isabelle_tool, Update_Cartouches.isabelle_tool, Update_Header.isabelle_tool, Update_Then.isabelle_tool, diff -r 1f66c7d77002 -r a8b89392ecb6 src/Pure/System/system_channel.scala --- a/src/Pure/System/system_channel.scala Fri Aug 04 18:03:50 2017 +0200 +++ b/src/Pure/System/system_channel.scala Mon Aug 07 15:10:37 2017 +0200 @@ -18,7 +18,7 @@ class System_Channel private { - private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1")) + private val server = new ServerSocket(0, 50, InetAddress.getByName("127.0.0.1")) val server_name: String = "127.0.0.1:" + server.getLocalPort override def toString: String = server_name diff -r 1f66c7d77002 -r a8b89392ecb6 src/Pure/Tools/server.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/server.scala Mon Aug 07 15:10:37 2017 +0200 @@ -0,0 +1,180 @@ +/* Title: Pure/Tools/server.scala + Author: Makarius + +Resident Isabelle servers. +*/ + +package isabelle + + +import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, + IOException} +import java.net.{Socket, ServerSocket, InetAddress} + + +object Server +{ + /* per-user servers */ + + object Data + { + val database = Path.explode("$ISABELLE_HOME_USER/servers.db") + + val name = SQL.Column.string("name", primary_key = true) + val port = SQL.Column.int("port") + val password = SQL.Column.string("password") + val table = SQL.Table("isabelle_servers", List(name, port, password)) + + sealed case class Entry(name: String, port: Int, password: String) + { + def print: String = + "server " + quote(name) + " = 127.0.0.1:" + port + " (password " + quote(password) + ")" + + def active: Boolean = + try { (new Socket(InetAddress.getByName("127.0.0.1"), port)).close; true } + catch { case _: IOException => false } + } + } + + def list(db: SQLite.Database): List[Data.Entry] = + if (db.tables.contains(Data.table.name)) { + db.using_statement(Data.table.select())(stmt => + stmt.execute_query().iterator(res => + Data.Entry( + res.string(Data.name), + res.int(Data.port), + res.string(Data.password))).toList.sortBy(_.name)) + } + else Nil + + def find(db: SQLite.Database, name: String): Option[Data.Entry] = + list(db).find(entry => entry.name == name && entry.active) + + def start(name: String = "", port: Int = 0): (Data.Entry, Option[Thread]) = + { + using(SQLite.open_database(Data.database))(db => + db.transaction { + find(db, name) match { + case Some(entry) => (entry, None) + case None => + val server = new Server(port) + val entry = Data.Entry(name, server.port, server.password) + + Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check + db.create_table(Data.table) + db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute) + db.using_statement(Data.table.insert())(stmt => + { + stmt.string(1) = entry.name + stmt.int(2) = entry.port + stmt.string(3) = entry.password + stmt.execute() + }) + + (entry, Some(server.thread)) + } + }) + } + + def stop(name: String = ""): Boolean = + { + using(SQLite.open_database(Data.database))(db => + db.transaction { + find(db, name) match { + case Some(entry) => + // FIXME shutdown server + db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute) + true + case None => + false + } + }) + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("server", "manage resident Isabelle servers", args => + { + var operation_list = false + var name = "" + var port = 0 + + val getopts = + Getopts(""" +Usage: isabelle server [OPTIONS] + + Options are: + -L list servers + -n NAME explicit server name + -p PORT explicit server port + + Manage resident Isabelle servers. +""", + "L" -> (_ => operation_list = true), + "n:" -> (arg => name = arg), + "p:" -> (arg => port = Value.Int.parse(arg))) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + if (operation_list) { + for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active) + Console.println(entry.print) + } + else { + val (entry, thread) = start(name, port) + Console.println(entry.print) + thread.foreach(_.join) + } + }) +} + +class Server private(_port: Int) +{ + private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1")) + def port: Int = server_socket.getLocalPort + def close { server_socket.close } + + val password: String = Library.UUID() + + private def handle_connection(socket: Socket) + { + val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset)) + val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset)) + + def println(s: String) + { + writer.write(s) + writer.newLine() + writer.flush() + } + + reader.readLine() match { + case null => + case bad if bad != password => println("BAD PASSWORD") + case _ => + var finished = false + while (!finished) { + reader.readLine() match { + case null => println("FINISHED"); finished = true + case line => println("ECHO " + line) + } + } + } + } + + lazy val thread: Thread = + Standard_Thread.fork("server") { + var finished = false + while (!finished) { + Exn.capture(server_socket.accept) match { + case Exn.Res(socket) => + Standard_Thread.fork("server_connection") + { try { handle_connection(socket) } finally { socket.close } } + case Exn.Exn(_) => finished = true + } + } + } +} diff -r 1f66c7d77002 -r a8b89392ecb6 src/Pure/build-jars --- a/src/Pure/build-jars Fri Aug 04 18:03:50 2017 +0200 +++ b/src/Pure/build-jars Mon Aug 07 15:10:37 2017 +0200 @@ -140,6 +140,7 @@ Tools/main.scala Tools/print_operation.scala Tools/profiling_report.scala + Tools/server.scala Tools/simplifier_trace.scala Tools/spell_checker.scala Tools/task_statistics.scala diff -r 1f66c7d77002 -r a8b89392ecb6 src/Pure/library.scala --- a/src/Pure/library.scala Fri Aug 04 18:03:50 2017 +0200 +++ b/src/Pure/library.scala Mon Aug 07 15:10:37 2017 +0200 @@ -259,4 +259,9 @@ def proper_list[A](list: List[A]): Option[List[A]] = if (list == null || list.isEmpty) None else Some(list) + + + /* UUID */ + + def UUID(): String = java.util.UUID.randomUUID().toString } diff -r 1f66c7d77002 -r a8b89392ecb6 src/Tools/VSCode/src/grammar.scala --- a/src/Tools/VSCode/src/grammar.scala Fri Aug 04 18:03:50 2017 +0200 +++ b/src/Tools/VSCode/src/grammar.scala Mon Aug 07 15:10:37 2017 +0200 @@ -9,8 +9,6 @@ import isabelle._ -import java.util.UUID - object Grammar { @@ -47,7 +45,7 @@ "name": "Isabelle", "scopeName": "source.isabelle", "fileTypes": ["thy"], - "uuid": """ + JSON.Format(UUID.randomUUID().toString) + """, + "uuid": """ + JSON.Format(Library.UUID()) + """, "repository": { "comment": { "patterns": [ diff -r 1f66c7d77002 -r a8b89392ecb6 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Fri Aug 04 18:03:50 2017 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Mon Aug 07 15:10:37 2017 +0200 @@ -12,7 +12,6 @@ import javax.swing.JOptionPane import java.io.{File => JFile} -import java.util.UUID import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager} import org.gjt.sp.jedit.textarea.JEditTextArea @@ -398,7 +397,7 @@ /* HTTP server */ - val http_root: String = "/" + UUID.randomUUID().toString + val http_root: String = "/" + Library.UUID() val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))