# HG changeset patch
# User wenzelm
# Date 1378577558 -7200
# Node ID 8adcf1f0042d309da09a3a55d2b2f1419c676c6b
# Parent 6301ed01e34dbe755007be20052b3f5178218687# Parent 19e7d50446178763636a681607f538a832d68167
merged
diff -r 6301ed01e34d -r 8adcf1f0042d Admin/MacOS/App3/Info.plist
--- a/Admin/MacOS/App3/Info.plist Fri Sep 06 20:59:36 2013 +0200
+++ b/Admin/MacOS/App3/Info.plist Sat Sep 07 20:12:38 2013 +0200
@@ -34,7 +34,7 @@
isabelle.Main
JVMOptions
--Dapple.laf.useScreenMenuBar=true
+-Dapple.laf.useScreenMenuBar=true -Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false
-Disabelle.home=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}
JVMArguments
diff -r 6301ed01e34d -r 8adcf1f0042d Admin/Windows/launch4j/isabelle.xml
--- a/Admin/Windows/launch4j/isabelle.xml Fri Sep 06 20:59:36 2013 +0200
+++ b/Admin/Windows/launch4j/isabelle.xml Sat Sep 07 20:12:38 2013 +0200
@@ -16,15 +16,19 @@
isabelle.Main
%EXEDIR%\lib\classes\ext\Pure.jar
+ %EXEDIR%\lib\classes\ext\scala-compiler.jar
%EXEDIR%\lib\classes\ext\scala-library.jar
%EXEDIR%\lib\classes\ext\scala-swing.jar
+ %EXEDIR%\lib\classes\ext\scala-actors.jar
+ %EXEDIR%\lib\classes\ext\scala-reflect.jar
+ %EXEDIR%\src\Tools\jEdit\dist\jedit.jar
%EXEDIR%\contrib\jdk\x86-cygwin
jdkOnly
- -Disabelle.home="%EXEDIR%"
+ -Dfile.encoding=UTF-8 -server -Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false -Disabelle.home="%EXEDIR%"
isabelle.bmp
diff -r 6301ed01e34d -r 8adcf1f0042d Admin/build
--- a/Admin/build Fri Sep 06 20:59:36 2013 +0200
+++ b/Admin/build Sat Sep 07 20:12:38 2013 +0200
@@ -74,6 +74,10 @@
## main
+#workaround for scalac
+function stty() { :; }
+export -f stty
+
for MODULE in $MODULES
do
case $MODULE in
diff -r 6301ed01e34d -r 8adcf1f0042d Admin/components/bundled-windows
--- a/Admin/components/bundled-windows Fri Sep 06 20:59:36 2013 +0200
+++ b/Admin/components/bundled-windows Sat Sep 07 20:12:38 2013 +0200
@@ -1,3 +1,3 @@
#additional components to be bundled for release
cygwin-20130117
-windows_app-20130905
+windows_app-20130906
diff -r 6301ed01e34d -r 8adcf1f0042d Admin/components/components.sha1
--- a/Admin/components/components.sha1 Fri Sep 06 20:59:36 2013 +0200
+++ b/Admin/components/components.sha1 Sat Sep 07 20:12:38 2013 +0200
@@ -55,6 +55,7 @@
869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd vampire-1.0.tar.gz
81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz
fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz
+e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz
2ae13aa17d0dc95ce254a52f1dba10929763a10d xz-java-1.2.tar.gz
4530a1aa6f4498ee3d78d6000fa71a3f63bd077f yices-1.0.28.tar.gz
12ae71acde43bd7bed1e005c43034b208c0cba4c z3-3.2.tar.gz
diff -r 6301ed01e34d -r 8adcf1f0042d Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle Fri Sep 06 20:59:36 2013 +0200
+++ b/Admin/lib/Tools/makedist_bundle Sat Sep 07 20:12:38 2013 +0200
@@ -126,6 +126,15 @@
case "$PLATFORM_FAMILY" in
linux)
purge_contrib '-name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
+ cat > "$ISABELLE_TARGET/$ISABELLE_NAME" < "$APP/Contents/Info.plist"
- for NAME in Pure.jar scala-library.jar scala-swing.jar
+ for NAME in Pure.jar scala-compiler.jar scala-library.jar scala-swing.jar scala-actors.jar scala-reflect.jar
do
ln -sf "../Resources/${ISABELLE_NAME}/lib/classes/ext/$NAME" "$APP/Contents/Java"
done
+ ln -sf "../Resources/${ISABELLE_NAME}/src/Tools/jEdit/dist/jedit.jar" "$APP/Contents/Java"
cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/."
cp "$APP_TEMPLATE/../isabelle.icns" "$APP/Contents/Resources/."
diff -r 6301ed01e34d -r 8adcf1f0042d Isabelle
--- a/Isabelle Fri Sep 06 20:59:36 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Default Isabelle application wrapper.
-
-exec "$(dirname "$0")"/bin/isabelle jedit -s -- "$@"
-
diff -r 6301ed01e34d -r 8adcf1f0042d src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Sep 06 20:59:36 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Sat Sep 07 20:12:38 2013 +0200
@@ -3125,131 +3125,284 @@
subsection {* Cauchy-type criterion for integrability. *}
(* XXXXXXX *)
-lemma integrable_cauchy: fixes f::"'n::ordered_euclidean_space \ 'a::{real_normed_vector,complete_space}"
+lemma integrable_cauchy:
+ fixes f :: "'n::ordered_euclidean_space \ 'a::{real_normed_vector,complete_space}"
shows "f integrable_on {a..b} \
- (\e>0.\d. gauge d \ (\p1 p2. p1 tagged_division_of {a..b} \ d fine p1 \
- p2 tagged_division_of {a..b} \ d fine p2
- \ norm(setsum (\(x,k). content k *\<^sub>R f x) p1 -
- setsum (\(x,k). content k *\<^sub>R f x) p2) < e))" (is "?l = (\e>0. \d. ?P e d)")
-proof assume ?l
+ (\e>0.\d. gauge d \
+ (\p1 p2. p1 tagged_division_of {a..b} \ d fine p1 \
+ p2 tagged_division_of {a..b} \ d fine p2 \
+ norm (setsum (\(x,k). content k *\<^sub>R f x) p1 -
+ setsum (\(x,k). content k *\<^sub>R f x) p2) < e))"
+ (is "?l = (\e>0. \d. ?P e d)")
+proof
+ assume ?l
then guess y unfolding integrable_on_def has_integral .. note y=this
- show "\e>0. \d. ?P e d" proof(rule,rule) case goal1 hence "e/2 > 0" by auto
+ show "\e>0. \d. ?P e d"
+ proof (rule, rule)
+ case goal1
+ then have "e/2 > 0" by auto
then guess d apply- apply(drule y[rule_format]) by(erule exE,erule conjE) note d=this[rule_format]
- show ?case apply(rule_tac x=d in exI,rule,rule d) apply(rule,rule,rule,(erule conjE)+)
- proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b}" "d fine p1" "p2 tagged_division_of {a..b}" "d fine p2"
+ show ?case
+ apply (rule_tac x=d in exI)
+ apply rule
+ apply (rule d)
+ apply rule
+ apply rule
+ apply rule
+ apply (erule conjE)+
+ proof -
+ fix p1 p2
+ assume as: "p1 tagged_division_of {a..b}" "d fine p1"
+ "p2 tagged_division_of {a..b}" "d fine p2"
show "norm ((\(x, k)\p1. content k *\<^sub>R f x) - (\(x, k)\p2. content k *\<^sub>R f x)) < e"
- apply(rule dist_triangle_half_l[where y=y,unfolded dist_norm])
+ apply (rule dist_triangle_half_l[where y=y,unfolded dist_norm])
using d(2)[OF conjI[OF as(1-2)]] d(2)[OF conjI[OF as(3-4)]] .
- qed qed
-next assume "\e>0. \d. ?P e d" hence "\n::nat. \d. ?P (inverse(real (n + 1))) d" by auto
+ qed
+ qed
+next
+ assume "\e>0. \d. ?P e d"
+ then have "\n::nat. \d. ?P (inverse(real (n + 1))) d"
+ by auto
from choice[OF this] guess d .. note d=conjunctD2[OF this[rule_format],rule_format]
- have "\n. gauge (\x. \{d i x |i. i \ {0..n}})" apply(rule gauge_inters) using d(1) by auto
- hence "\n. \p. p tagged_division_of {a..b} \ (\x. \{d i x |i. i \ {0..n}}) fine p" apply-
- proof case goal1 from this[of n] show ?case apply(drule_tac fine_division_exists) by auto qed
+ have "\n. gauge (\x. \{d i x |i. i \ {0..n}})"
+ apply (rule gauge_inters)
+ using d(1)
+ apply auto
+ done
+ then have "\n. \p. p tagged_division_of {a..b} \ (\x. \{d i x |i. i \ {0..n}}) fine p"
+ apply -
+ proof
+ case goal1
+ from this[of n]
+ show ?case
+ apply (drule_tac fine_division_exists)
+ apply auto
+ done
+ qed
from choice[OF this] guess p .. note p = conjunctD2[OF this[rule_format]]
- have dp:"\i n. i\n \ d i fine p n" using p(2) unfolding fine_inters by auto
+ have dp: "\i n. i\n \ d i fine p n"
+ using p(2) unfolding fine_inters by auto
have "Cauchy (\n. setsum (\(x,k). content k *\<^sub>R (f x)) (p n))"
- proof(rule CauchyI) case goal1 then guess N unfolding real_arch_inv[of e] .. note N=this
- show ?case apply(rule_tac x=N in exI)
- proof(rule,rule,rule,rule) fix m n assume mn:"N \ m" "N \ n" have *:"N = (N - 1) + 1" using N by auto
+ proof (rule CauchyI)
+ case goal1
+ then guess N unfolding real_arch_inv[of e] .. note N=this
+ show ?case
+ apply (rule_tac x=N in exI)
+ proof (rule, rule, rule, rule)
+ fix m n
+ assume mn: "N \ m" "N \ n"
+ have *: "N = (N - 1) + 1" using N by auto
show "norm ((\(x, k)\p m. content k *\<^sub>R f x) - (\(x, k)\p n. content k *\<^sub>R f x)) < e"
- apply(rule less_trans[OF _ N[THEN conjunct2,THEN conjunct2]]) apply(subst *) apply(rule d(2))
- using dp p(1) using mn by auto
- qed qed
+ apply (rule less_trans[OF _ N[THEN conjunct2,THEN conjunct2]])
+ apply(subst *)
+ apply(rule d(2))
+ using dp p(1)
+ using mn
+ apply auto
+ done
+ qed
+ qed
then guess y unfolding convergent_eq_cauchy[symmetric] .. note y=this[THEN LIMSEQ_D]
- show ?l unfolding integrable_on_def has_integral apply(rule_tac x=y in exI)
- proof(rule,rule) fix e::real assume "e>0" hence *:"e/2 > 0" by auto
- then guess N1 unfolding real_arch_inv[of "e/2"] .. note N1=this hence N1':"N1 = N1 - 1 + 1" by auto
+ show ?l
+ unfolding integrable_on_def has_integral
+ apply (rule_tac x=y in exI)
+ proof (rule, rule)
+ fix e :: real
+ assume "e>0"
+ then have *:"e/2 > 0" by auto
+ then guess N1 unfolding real_arch_inv[of "e/2"] .. note N1=this
+ then have N1': "N1 = N1 - 1 + 1"
+ by auto
guess N2 using y[OF *] .. note N2=this
- show "\d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ norm ((\(x, k)\p. content k *\<^sub>R f x) - y) < e)"
- apply(rule_tac x="d (N1 + N2)" in exI) apply rule defer
- proof(rule,rule,erule conjE) show "gauge (d (N1 + N2))" using d by auto
- fix q assume as:"q tagged_division_of {a..b}" "d (N1 + N2) fine q"
- have *:"inverse (real (N1 + N2 + 1)) < e / 2" apply(rule less_trans) using N1 by auto
- show "norm ((\(x, k)\q. content k *\<^sub>R f x) - y) < e" apply(rule norm_triangle_half_r)
- apply(rule less_trans[OF _ *]) apply(subst N1', rule d(2)[of "p (N1+N2)"]) defer
+ show "\d. gauge d \
+ (\p. p tagged_division_of {a..b} \ d fine p \ norm ((\(x, k)\p. content k *\<^sub>R f x) - y) < e)"
+ apply (rule_tac x="d (N1 + N2)" in exI)
+ apply rule
+ defer
+ proof (rule, rule, erule conjE)
+ show "gauge (d (N1 + N2))"
+ using d by auto
+ fix q
+ assume as: "q tagged_division_of {a..b}" "d (N1 + N2) fine q"
+ have *: "inverse (real (N1 + N2 + 1)) < e / 2"
+ apply (rule less_trans)
+ using N1
+ apply auto
+ done
+ show "norm ((\(x, k)\q. content k *\<^sub>R f x) - y) < e"
+ apply (rule norm_triangle_half_r)
+ apply (rule less_trans[OF _ *])
+ apply (subst N1', rule d(2)[of "p (N1+N2)"])
+ defer
using N2[rule_format,of "N1+N2"]
- using as dp[of "N1 - 1 + 1 + N2" "N1 + N2"] using p(1)[of "N1 + N2"] using N1 by auto qed qed qed
+ using as dp[of "N1 - 1 + 1 + N2" "N1 + N2"]
+ using p(1)[of "N1 + N2"]
+ using N1
+ apply auto
+ done
+ qed
+ qed
+qed
+
subsection {* Additivity of integral on abutting intervals. *}
lemma interval_split:
- fixes a::"'a::ordered_euclidean_space" assumes "k \ Basis"
+ fixes a :: "'a::ordered_euclidean_space"
+ assumes "k \ Basis"
shows
"{a..b} \ {x. x\k \ c} = {a .. (\i\Basis. (if i = k then min (b\k) c else b\i) *\<^sub>R i)}"
"{a..b} \ {x. x\k \ c} = {(\i\Basis. (if i = k then max (a\k) c else a\i) *\<^sub>R i) .. b}"
- apply(rule_tac[!] set_eqI) unfolding Int_iff mem_interval mem_Collect_eq using assms
- by auto
-
-lemma content_split: fixes a::"'a::ordered_euclidean_space" assumes "k\Basis" shows
- "content {a..b} = content({a..b} \ {x. x\k \ c}) + content({a..b} \ {x. x\k >= c})"
+ apply (rule_tac[!] set_eqI)
+ unfolding Int_iff mem_interval mem_Collect_eq
+ using assms
+ apply auto
+ done
+
+lemma content_split:
+ fixes a :: "'a::ordered_euclidean_space"
+ assumes "k \ Basis"
+ shows "content {a..b} = content({a..b} \ {x. x\k \ c}) + content({a..b} \ {x. x\k \ c})"
proof cases
note simps = interval_split[OF assms] content_closed_interval_cases eucl_le[where 'a='a]
- have *:"Basis = insert k (Basis - {k})" "\x. finite (Basis-{x})" "\x. x\Basis-{x}"
+ have *: "Basis = insert k (Basis - {k})" "\x. finite (Basis-{x})" "\x. x\Basis-{x}"
using assms by auto
- have *:"\X Y Z. (\i\Basis. Z i (if i = k then X else Y i)) = Z k X * (\i\Basis-{k}. Z i (Y i))"
+ have *: "\X Y Z. (\i\Basis. Z i (if i = k then X else Y i)) = Z k X * (\i\Basis-{k}. Z i (Y i))"
"(\i\Basis. b\i - a\i) = (\i\Basis-{k}. b\i - a\i) * (b\k - a\k)"
- apply(subst *(1)) defer apply(subst *(1)) unfolding setprod_insert[OF *(2-)] by auto
- assume as:"a\b" moreover have "\x. min (b \ k) c = max (a \ k) c
- \ x* (b\k - a\k) = x*(max (a \ k) c - a \ k) + x*(b \ k - max (a \ k) c)"
- by (auto simp add:field_simps)
- moreover have **:"(\i\Basis. ((\i\Basis. (if i = k then min (b \ k) c else b \ i) *\<^sub>R i) \ i - a \ i)) =
+ apply (subst *(1))
+ defer
+ apply (subst *(1))
+ unfolding setprod_insert[OF *(2-)]
+ apply auto
+ done
+ assume as: "a \ b"
+ moreover
+ have "\x. min (b \ k) c = max (a \ k) c \
+ x * (b\k - a\k) = x * (max (a \ k) c - a \ k) + x * (b \ k - max (a \ k) c)"
+ by (auto simp add: field_simps)
+ moreover
+ have **: "(\i\Basis. ((\i\Basis. (if i = k then min (b \ k) c else b \ i) *\<^sub>R i) \ i - a \ i)) =
(\i\Basis. (if i = k then min (b \ k) c else b \ i) - a \ i)"
"(\i\Basis. b \ i - ((\i\Basis. (if i = k then max (a \ k) c else a \ i) *\<^sub>R i) \ i)) =
(\i\Basis. b \ i - (if i = k then max (a \ k) c else a \ i))"
by (auto intro!: setprod_cong)
have "\ a \ k \ c \ \ c \ b \ k \ False"
- unfolding not_le using as[unfolded eucl_le[where 'a='a],rule_format,of k] assms by auto
- ultimately show ?thesis using assms unfolding simps **
- unfolding *(1)[of "\i x. b\i - x"] *(1)[of "\i x. x - a\i"] unfolding *(2)
+ unfolding not_le
+ using as[unfolded eucl_le[where 'a='a],rule_format,of k] assms
+ by auto
+ ultimately show ?thesis
+ using assms
+ unfolding simps **
+ unfolding *(1)[of "\i x. b\i - x"] *(1)[of "\i x. x - a\i"]
+ unfolding *(2)
by auto
next
- assume "\ a \ b" then have "{a .. b} = {}"
+ assume "\ a \ b"
+ then have "{a .. b} = {}"
unfolding interval_eq_empty by (auto simp: eucl_le[where 'a='a] not_le)
- then show ?thesis by auto
+ then show ?thesis
+ by auto
qed
-lemma division_split_left_inj: fixes type::"'a::ordered_euclidean_space"
- assumes "d division_of i" "k1 \ d" "k2 \ d" "k1 \ k2"
- "k1 \ {x::'a. x\k \ c} = k2 \ {x. x\k \ c}"and k:"k\Basis"
+lemma division_split_left_inj:
+ fixes type :: "'a::ordered_euclidean_space"
+ assumes "d division_of i"
+ and "k1 \ d"
+ and "k2 \ d"
+ and "k1 \ k2"
+ and "k1 \ {x::'a. x\k \ c} = k2 \ {x. x\k \ c}"
+ and k: "k\Basis"
shows "content(k1 \ {x. x\k \ c}) = 0"
-proof- note d=division_ofD[OF assms(1)]
- have *:"\a b::'a. \