--- a/src/HOL/IMP/Hoare.thy Fri Mar 12 14:04:59 2010 +0100
+++ b/src/HOL/IMP/Hoare.thy Fri Mar 12 20:04:48 2010 +0100
@@ -6,14 +6,10 @@
header "Inductive Definition of Hoare Logic"
-theory Hoare imports Denotation begin
+theory Hoare imports Natural begin
types assn = "state => bool"
-definition
- hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
- "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
-
inductive
hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
where
@@ -27,139 +23,20 @@
| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
|- {P'}c{Q'}"
-definition
- wp :: "com => assn => assn" where
- "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
-
-(*
-Soundness (and part of) relative completeness of Hoare rules
-wrt denotational semantics
-*)
-
lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
by (blast intro: conseq)
lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
by (blast intro: conseq)
-lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
-proof(induct rule: hoare.induct)
- case (While P b c)
- { fix s t
- let ?G = "Gamma b (C c)"
- assume "(s,t) \<in> lfp ?G"
- hence "P s \<longrightarrow> P t \<and> \<not> b t"
- proof(rule lfp_induct2)
- show "mono ?G" by(rule Gamma_mono)
- next
- fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
- thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
- by(auto simp: hoare_valid_def Gamma_def)
- qed
- }
- thus ?case by(simp add:hoare_valid_def)
-qed (auto simp: hoare_valid_def)
+lemma While':
+assumes "|- {%s. P s & b s} c {P}" and "ALL s. P s & \<not> b s \<longrightarrow> Q s"
+shows "|- {P} \<WHILE> b \<DO> c {Q}"
+by(rule weaken_post[OF While[OF assms(1)] assms(2)])
-lemma wp_SKIP: "wp \<SKIP> Q = Q"
-by (simp add: wp_def)
-
-lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
-by (simp add: wp_def)
-
-lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_If:
- "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_While_If:
- "wp (\<WHILE> b \<DO> c) Q s =
- wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
-by(simp only: wp_def C_While_If)
-
-(*Not suitable for rewriting: LOOPS!*)
-lemma wp_While_if:
- "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
-by(simp add:wp_While_If wp_If wp_SKIP)
-
-lemma wp_While_True: "b s ==>
- wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
-by(simp add: wp_While_if)
-
-lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
-by(simp add: wp_While_if)
-
-lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
-
-lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
- (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
-apply (simp (no_asm))
-apply (rule iffI)
- apply (rule weak_coinduct)
- apply (erule CollectI)
- apply safe
- apply simp
- apply simp
-apply (simp add: wp_def Gamma_def)
-apply (intro strip)
-apply (rule mp)
- prefer 2 apply (assumption)
-apply (erule lfp_induct2)
-apply (fast intro!: monoI)
-apply (subst gfp_unfold)
- apply (fast intro!: monoI)
-apply fast
-done
-
-declare C_while [simp del]
+lemmas [simp] = skip ass semi If
lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
-lemma wp_is_pre: "|- {wp c Q} c {Q}"
-proof(induct c arbitrary: Q)
- case SKIP show ?case by auto
-next
- case Assign show ?case by auto
-next
- case Semi thus ?case by auto
-next
- case (Cond b c1 c2)
- let ?If = "IF b THEN c1 ELSE c2"
- show ?case
- proof(rule If)
- show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
- proof(rule strengthen_pre[OF _ Cond(1)])
- show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
- qed
- show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
- proof(rule strengthen_pre[OF _ Cond(2)])
- show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
- qed
- qed
-next
- case (While b c)
- let ?w = "WHILE b DO c"
- have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
- proof(rule hoare.While)
- show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
- proof(rule strengthen_pre[OF _ While(1)])
- show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
- qed
- qed
- thus ?case
- proof(rule weaken_post)
- show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
- qed
-qed
-
-lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
-proof(rule conseq)
- show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
- by (auto simp: hoare_valid_def wp_def)
- show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
- show "\<forall>s. Q s \<longrightarrow> Q s" by auto
-qed
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Hoare_Den.thy Fri Mar 12 20:04:48 2010 +0100
@@ -0,0 +1,134 @@
+(* Title: HOL/IMP/Hoare_Def.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+*)
+
+header "Soundness and Completeness wrt Denotational Semantics"
+
+theory Hoare_Den imports Hoare Denotation begin
+
+definition
+ hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
+ "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
+
+
+lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
+proof(induct rule: hoare.induct)
+ case (While P b c)
+ { fix s t
+ let ?G = "Gamma b (C c)"
+ assume "(s,t) \<in> lfp ?G"
+ hence "P s \<longrightarrow> P t \<and> \<not> b t"
+ proof(rule lfp_induct2)
+ show "mono ?G" by(rule Gamma_mono)
+ next
+ fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
+ thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
+ by(auto simp: hoare_valid_def Gamma_def)
+ qed
+ }
+ thus ?case by(simp add:hoare_valid_def)
+qed (auto simp: hoare_valid_def)
+
+
+definition
+ wp :: "com => assn => assn" where
+ "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
+
+lemma wp_SKIP: "wp \<SKIP> Q = Q"
+by (simp add: wp_def)
+
+lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
+by (simp add: wp_def)
+
+lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
+by (rule ext) (auto simp: wp_def)
+
+lemma wp_If:
+ "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))"
+by (rule ext) (auto simp: wp_def)
+
+lemma wp_While_If:
+ "wp (\<WHILE> b \<DO> c) Q s =
+ wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
+by(simp only: wp_def C_While_If)
+
+(*Not suitable for rewriting: LOOPS!*)
+lemma wp_While_if:
+ "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
+by(simp add:wp_While_If wp_If wp_SKIP)
+
+lemma wp_While_True: "b s ==>
+ wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
+by(simp add: wp_While_if)
+
+lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
+by(simp add: wp_While_if)
+
+lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
+
+lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
+ (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
+apply (simp (no_asm))
+apply (rule iffI)
+ apply (rule weak_coinduct)
+ apply (erule CollectI)
+ apply safe
+ apply simp
+ apply simp
+apply (simp add: wp_def Gamma_def)
+apply (intro strip)
+apply (rule mp)
+ prefer 2 apply (assumption)
+apply (erule lfp_induct2)
+apply (fast intro!: monoI)
+apply (subst gfp_unfold)
+ apply (fast intro!: monoI)
+apply fast
+done
+
+declare C_while [simp del]
+
+lemma wp_is_pre: "|- {wp c Q} c {Q}"
+proof(induct c arbitrary: Q)
+ case SKIP show ?case by auto
+next
+ case Assign show ?case by auto
+next
+ case Semi thus ?case by auto
+next
+ case (Cond b c1 c2)
+ let ?If = "IF b THEN c1 ELSE c2"
+ show ?case
+ proof(rule If)
+ show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
+ proof(rule strengthen_pre[OF _ Cond(1)])
+ show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
+ qed
+ show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
+ proof(rule strengthen_pre[OF _ Cond(2)])
+ show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
+ qed
+ qed
+next
+ case (While b c)
+ let ?w = "WHILE b DO c"
+ show ?case
+ proof(rule While')
+ show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
+ proof(rule strengthen_pre[OF _ While(1)])
+ show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
+ qed
+ show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
+ qed
+qed
+
+lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
+proof(rule conseq)
+ show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
+ by (auto simp: hoare_valid_def wp_def)
+ show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
+ show "\<forall>s. Q s \<longrightarrow> Q s" by auto
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Hoare_Op.thy Fri Mar 12 20:04:48 2010 +0100
@@ -0,0 +1,106 @@
+(* Title: HOL/IMP/Hoare_Op.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+*)
+
+header "Soundness and Completeness wrt Operational Semantics"
+
+theory Hoare_Op imports Hoare begin
+
+definition
+ hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
+ "|= {P}c{Q} = (!s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> P s --> Q t)"
+
+lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
+proof(induct rule: hoare.induct)
+ case (While P b c)
+ { fix s t
+ assume "\<langle>WHILE b DO c,s\<rangle> \<longrightarrow>\<^sub>c t"
+ hence "P s \<longrightarrow> P t \<and> \<not> b t"
+ proof(induct "WHILE b DO c" s t)
+ case WhileFalse thus ?case by blast
+ next
+ case WhileTrue thus ?case
+ using While(2) unfolding hoare_valid_def by blast
+ qed
+
+ }
+ thus ?case unfolding hoare_valid_def by blast
+qed (auto simp: hoare_valid_def)
+
+definition
+ wp :: "com => assn => assn" where
+ "wp c Q = (%s. !t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> Q t)"
+
+lemma wp_SKIP: "wp \<SKIP> Q = Q"
+by (simp add: wp_def)
+
+lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
+by (simp add: wp_def)
+
+lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
+by (rule ext) (auto simp: wp_def)
+
+lemma wp_If:
+ "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))"
+by (rule ext) (auto simp: wp_def)
+
+lemma wp_While_If:
+ "wp (\<WHILE> b \<DO> c) Q s =
+ wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
+unfolding wp_def by (metis equivD1 equivD2 unfold_while)
+
+lemma wp_While_True: "b s ==>
+ wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
+by(simp add: wp_While_If wp_If wp_SKIP)
+
+lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
+by(simp add: wp_While_If wp_If wp_SKIP)
+
+lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
+
+lemma wp_is_pre: "|- {wp c Q} c {Q}"
+proof(induct c arbitrary: Q)
+ case SKIP show ?case by auto
+next
+ case Assign show ?case by auto
+next
+ case Semi thus ?case by(auto intro: semi)
+next
+ case (Cond b c1 c2)
+ let ?If = "IF b THEN c1 ELSE c2"
+ show ?case
+ proof(rule If)
+ show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
+ proof(rule strengthen_pre[OF _ Cond(1)])
+ show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
+ qed
+ show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
+ proof(rule strengthen_pre[OF _ Cond(2)])
+ show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
+ qed
+ qed
+next
+ case (While b c)
+ let ?w = "WHILE b DO c"
+ have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
+ proof(rule hoare.While)
+ show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
+ proof(rule strengthen_pre[OF _ While(1)])
+ show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
+ qed
+ qed
+ thus ?case
+ proof(rule weaken_post)
+ show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
+ qed
+qed
+
+lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
+proof(rule strengthen_pre)
+ show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
+ by (auto simp: hoare_valid_def wp_def)
+ show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
+qed
+
+end
--- a/src/HOL/IMP/ROOT.ML Fri Mar 12 14:04:59 2010 +0100
+++ b/src/HOL/IMP/ROOT.ML Fri Mar 12 20:04:48 2010 +0100
@@ -6,4 +6,4 @@
Caveat: HOLCF/IMP depends on HOL/IMP
*)
-use_thys ["Expr", "Transition", "VC", "Examples", "Compiler0", "Compiler", "Live"];
+use_thys ["Expr", "Transition", "VC", "Hoare_Den", "Examples", "Compiler0", "Compiler", "Live"];
--- a/src/HOL/IMP/VC.thy Fri Mar 12 14:04:59 2010 +0100
+++ b/src/HOL/IMP/VC.thy Fri Mar 12 20:04:48 2010 +0100
@@ -10,7 +10,7 @@
header "Verification Conditions"
-theory VC imports Hoare begin
+theory VC imports Hoare_Op begin
datatype acom = Askip
| Aass loc aexp
@@ -63,51 +63,36 @@
Soundness and completeness of vc
*)
-declare hoare.intros [intro]
+declare hoare.conseq [intro]
-lemma l: "!s. P s --> P s" by fast
-lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
-apply (induct c arbitrary: Q)
- apply (simp_all (no_asm))
- apply fast
- apply fast
- apply fast
- (* if *)
- apply atomize
- apply (tactic "deepen_tac @{claset} 4 1")
-(* while *)
-apply atomize
-apply (intro allI impI)
-apply (rule conseq)
- apply (rule l)
- apply (rule While)
- defer
- apply fast
-apply (rule_tac P="awp c fun2" in conseq)
- apply fast
- apply fast
-apply fast
-done
+lemma vc_sound: "(ALL s. vc c Q s) \<Longrightarrow> |- {awp c Q} astrip c {Q}"
+proof(induct c arbitrary: Q)
+ case (Awhile b I c)
+ show ?case
+ proof(simp, rule While')
+ from `\<forall>s. vc (Awhile b I c) Q s`
+ have vc: "ALL s. vc c I s" and IQ: "ALL s. I s \<and> \<not> b s \<longrightarrow> Q s" and
+ awp: "ALL s. I s & b s --> awp c I s" by simp_all
+ from vc have "|- {awp c I} astrip c {I}" using Awhile.hyps by blast
+ with awp show "|- {\<lambda>s. I s \<and> b s} astrip c {I}"
+ by(rule strengthen_pre)
+ show "\<forall>s. I s \<and> \<not> b s \<longrightarrow> Q s" by(rule IQ)
+ qed
+qed auto
-lemma awp_mono [rule_format (no_asm)]:
- "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
-apply (induct c)
- apply (simp_all (no_asm_simp))
-apply (rule allI, rule allI, rule impI)
-apply (erule allE, erule allE, erule mp)
-apply (erule allE, erule allE, erule mp, assumption)
-done
-lemma vc_mono [rule_format (no_asm)]:
- "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
-apply (induct c)
- apply (simp_all (no_asm_simp))
-apply safe
-apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp)
-prefer 2 apply assumption
-apply (fast elim: awp_mono)
-done
+lemma awp_mono:
+ "(!s. P s --> Q s) ==> awp c P s ==> awp c Q s"
+proof (induct c arbitrary: P Q s)
+ case Asemi thus ?case by simp metis
+qed simp_all
+
+lemma vc_mono:
+ "(!s. P s --> Q s) ==> vc c P s ==> vc c Q s"
+proof(induct c arbitrary: P Q)
+ case Asemi thus ?case by simp (metis awp_mono)
+qed simp_all
lemma vc_complete: assumes der: "|- {P}c{Q}"
shows "(\<exists>ac. astrip ac = c & (\<forall>s. vc ac Q s) & (\<forall>s. P s --> awp ac Q s))"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Mar 12 14:04:59 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Mar 12 20:04:48 2010 +0100
@@ -211,11 +211,11 @@
lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
unfolding gauge_def by auto
-lemma gauge_ball[intro?]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)" unfolding gauge_def by auto
+lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)" unfolding gauge_def by auto
lemma gauge_trivial[intro]: "gauge (\<lambda>x. ball x 1)" apply(rule gauge_ball) by auto
-lemma gauge_inter: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. (d1 x) \<inter> (d2 x))"
+lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. (d1 x) \<inter> (d2 x))"
unfolding gauge_def by auto
lemma gauge_inters: assumes "finite s" "\<forall>d\<in>s. gauge (f d)" shows "gauge(\<lambda>x. \<Inter> {f d x | d. d \<in> s})" proof-
@@ -3476,4 +3476,440 @@
apply(rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f'])
using assms(4) by auto
+lemma indefinite_integral_continuous_left: fixes f::"real^1 \<Rightarrow> 'a::banach"
+ assumes "f integrable_on {a..b}" "a < c" "c \<le> b" "0 < e"
+ obtains d where "0 < d" "\<forall>t. c$1 - d < t$1 \<and> t \<le> c \<longrightarrow> norm(integral {a..c} f - integral {a..t} f) < e"
+proof- have "\<exists>w>0. \<forall>t. c$1 - w < t$1 \<and> t < c \<longrightarrow> norm(f c) * norm(c - t) < e / 3"
+ proof(cases "f c = 0") case False hence "0 < e / 3 / norm (f c)"
+ apply-apply(rule divide_pos_pos) using `e>0` by auto
+ thus ?thesis apply-apply(rule,rule,assumption,safe)
+ proof- fix t assume as:"t < c" and "c$1 - e / 3 / norm (f c) < t$(1::1)"
+ hence "c$1 - t$1 < e / 3 / norm (f c)" by auto
+ hence "norm (c - t) < e / 3 / norm (f c)" using as unfolding norm_vector_1 vector_less_def by auto
+ thus "norm (f c) * norm (c - t) < e / 3" using False apply-
+ apply(subst real_mult_commute) apply(subst pos_less_divide_eq[THEN sym]) by auto
+ qed next case True show ?thesis apply(rule_tac x=1 in exI) unfolding True using `e>0` by auto
+ qed then guess w .. note w = conjunctD2[OF this,rule_format]
+
+ have *:"e / 3 > 0" using assms by auto
+ have "f integrable_on {a..c}" apply(rule integrable_subinterval[OF assms(1)]) using assms(2-3) by auto
+ from integrable_integral[OF this,unfolded has_integral,rule_format,OF *] guess d1 ..
+ note d1 = conjunctD2[OF this,rule_format] def d \<equiv> "\<lambda>x. ball x w \<inter> d1 x"
+ have "gauge d" unfolding d_def using w(1) d1 by auto
+ note this[unfolded gauge_def,rule_format,of c] note conjunctD2[OF this]
+ from this(2)[unfolded open_contains_ball,rule_format,OF this(1)] guess k .. note k=conjunctD2[OF this]
+
+ let ?d = "min k (c$1 - a$1)/2" show ?thesis apply(rule that[of ?d])
+ proof safe show "?d > 0" using k(1) using assms(2) unfolding vector_less_def by auto
+ fix t assume as:"c$1 - ?d < t$1" "t \<le> c" let ?thesis = "norm (integral {a..c} f - integral {a..t} f) < e"
+ { presume *:"t < c \<Longrightarrow> ?thesis"
+ show ?thesis apply(cases "t = c") defer apply(rule *)
+ unfolding vector_less_def apply(subst less_le) using `e>0` as(2) by auto } assume "t < c"
+
+ have "f integrable_on {a..t}" apply(rule integrable_subinterval[OF assms(1)]) using assms(2-3) as(2) by auto
+ from integrable_integral[OF this,unfolded has_integral,rule_format,OF *] guess d2 ..
+ note d2 = conjunctD2[OF this,rule_format]
+ def d3 \<equiv> "\<lambda>x. if x \<le> t then d1 x \<inter> d2 x else d1 x"
+ have "gauge d3" using d2(1) d1(1) unfolding d3_def gauge_def by auto
+ from fine_division_exists[OF this, of a t] guess p . note p=this
+ note p'=tagged_division_ofD[OF this(1)]
+ have pt:"\<forall>(x,k)\<in>p. x$1 \<le> t$1" proof safe case goal1 from p'(2,3)[OF this] show ?case by auto qed
+ with p(2) have "d2 fine p" unfolding fine_def d3_def apply safe apply(erule_tac x="(a,b)" in ballE)+ by auto
+ note d2_fin = d2(2)[OF conjI[OF p(1) this]]
+
+ have *:"{a..c} \<inter> {x. x$1 \<le> t$1} = {a..t}" "{a..c} \<inter> {x. x$1 \<ge> t$1} = {t..c}"
+ using assms(2-3) as by(auto simp add:field_simps)
+ have "p \<union> {(c, {t..c})} tagged_division_of {a..c} \<and> d1 fine p \<union> {(c, {t..c})}" apply rule
+ apply(rule tagged_division_union_interval[of _ _ _ 1 "t$1"]) unfolding * apply(rule p)
+ apply(rule tagged_division_of_self) unfolding fine_def
+ proof safe fix x k y assume "(x,k)\<in>p" "y\<in>k" thus "y\<in>d1 x"
+ using p(2) pt unfolding fine_def d3_def apply- apply(erule_tac x="(x,k)" in ballE)+ by auto
+ next fix x assume "x\<in>{t..c}" hence "dist c x < k" unfolding dist_real
+ using as(1) by(auto simp add:field_simps)
+ thus "x \<in> d1 c" using k(2) unfolding d_def by auto
+ qed(insert as(2), auto) note d1_fin = d1(2)[OF this]
+
+ have *:"integral{a..c} f - integral {a..t} f = -(((c$1 - t$1) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)) -
+ integral {a..c} f) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral {a..t} f) + (c$1 - t$1) *\<^sub>R f c"
+ "e = (e/3 + e/3) + e/3" by auto
+ have **:"(\<Sum>(x, k)\<in>p \<union> {(c, {t..c})}. content k *\<^sub>R f x) = (c$1 - t$1) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
+ proof- have **:"\<And>x F. F \<union> {x} = insert x F" by auto
+ have "(c, {t..c}) \<notin> p" proof safe case goal1 from p'(2-3)[OF this]
+ have "c \<in> {a..t}" by auto thus False using `t<c` unfolding vector_less_def by auto
+ qed thus ?thesis unfolding ** apply- apply(subst setsum_insert) apply(rule p')
+ unfolding split_conv defer apply(subst content_1) using as(2) by auto qed
+
+ have ***:"c$1 - w < t$1 \<and> t < c"
+ proof- have "c$1 - k < t$1" using `k>0` as(1) by(auto simp add:field_simps)
+ moreover have "k \<le> w" apply(rule ccontr) using k(2)
+ unfolding subset_eq apply(erule_tac x="c + vec ((k + w)/2)" in ballE)
+ unfolding d_def using `k>0` `w>0` by(auto simp add:field_simps not_le not_less dist_real)
+ ultimately show ?thesis using `t<c` by(auto simp add:field_simps) qed
+
+ show ?thesis unfolding *(1) apply(subst *(2)) apply(rule norm_triangle_lt add_strict_mono)+
+ unfolding norm_minus_cancel apply(rule d1_fin[unfolded **]) apply(rule d2_fin)
+ using w(2)[OF ***] unfolding norm_scaleR norm_real by(auto simp add:field_simps) qed qed
+
+lemma indefinite_integral_continuous_right: fixes f::"real^1 \<Rightarrow> 'a::banach"
+ assumes "f integrable_on {a..b}" "a \<le> c" "c < b" "0 < e"
+ obtains d where "0 < d" "\<forall>t. c \<le> t \<and> t$1 < c$1 + d \<longrightarrow> norm(integral{a..c} f - integral{a..t} f) < e"
+proof- have *:"(\<lambda>x. f (- x)) integrable_on {- b..- a}" "- b < - c" "- c \<le> - a"
+ using assms unfolding Cart_simps by auto
+ from indefinite_integral_continuous_left[OF * `e>0`] guess d . note d = this let ?d = "min d (b$1 - c$1)"
+ show ?thesis apply(rule that[of "?d"])
+ proof safe show "0 < ?d" using d(1) assms(3) unfolding Cart_simps by auto
+ fix t::"_^1" assume as:"c \<le> t" "t$1 < c$1 + ?d"
+ have *:"integral{a..c} f = integral{a..b} f - integral{c..b} f"
+ "integral{a..t} f = integral{a..b} f - integral{t..b} f" unfolding group_simps
+ apply(rule_tac[!] integral_combine) using assms as unfolding Cart_simps by auto
+ have "(- c)$1 - d < (- t)$1 \<and> - t \<le> - c" using as by auto note d(2)[rule_format,OF this]
+ thus "norm (integral {a..c} f - integral {a..t} f) < e" unfolding *
+ unfolding integral_reflect apply-apply(subst norm_minus_commute) by(auto simp add:group_simps) qed qed
+
+declare dest_vec1_eq[simp del] not_less[simp] not_le[simp]
+
+lemma indefinite_integral_continuous: fixes f::"real^1 \<Rightarrow> 'a::banach"
+ assumes "f integrable_on {a..b}" shows "continuous_on {a..b} (\<lambda>x. integral {a..x} f)"
+proof(unfold continuous_on_def, safe) fix x e assume as:"x\<in>{a..b}" "0<(e::real)"
+ let ?thesis = "\<exists>d>0. \<forall>x'\<in>{a..b}. dist x' x < d \<longrightarrow> dist (integral {a..x'} f) (integral {a..x} f) < e"
+ { presume *:"a<b \<Longrightarrow> ?thesis"
+ show ?thesis apply(cases,rule *,assumption)
+ proof- case goal1 hence "{a..b} = {x}" using as(1) unfolding Cart_simps
+ by(auto simp only:field_simps not_less Cart_eq forall_1 mem_interval)
+ thus ?case using `e>0` by auto
+ qed } assume "a<b"
+ have "(x=a \<or> x=b) \<or> (a<x \<and> x<b)" using as(1) by (auto simp add: Cart_simps)
+ thus ?thesis apply-apply(erule disjE)+
+ proof- assume "x=a" have "a \<le> a" by auto
+ from indefinite_integral_continuous_right[OF assms(1) this `a<b` `e>0`] guess d . note d=this
+ show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
+ unfolding `x=a` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
+ next assume "x=b" have "b \<le> b" by auto
+ from indefinite_integral_continuous_left[OF assms(1) `a<b` this `e>0`] guess d . note d=this
+ show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
+ unfolding `x=b` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
+ next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add:Cart_simps)
+ from indefinite_integral_continuous_left [OF assms(1) xl `e>0`] guess d1 . note d1=this
+ from indefinite_integral_continuous_right[OF assms(1) xr `e>0`] guess d2 . note d2=this
+ show ?thesis apply(rule_tac x="min d1 d2" in exI)
+ proof safe show "0 < min d1 d2" using d1 d2 by auto
+ fix y assume "y\<in>{a..b}" "dist y x < min d1 d2"
+ thus "dist (integral {a..y} f) (integral {a..x} f) < e" apply-apply(subst dist_commute)
+ apply(cases "y < x") unfolding vector_dist_norm apply(rule d1(2)[rule_format]) defer
+ apply(rule d2(2)[rule_format]) unfolding Cart_simps not_less norm_real by(auto simp add:field_simps)
+ qed qed qed
+
+subsection {* This doesn't directly involve integration, but that gives an easy proof. *}
+
+lemma has_derivative_zero_unique_strong_interval: fixes f::"real \<Rightarrow> 'a::banach"
+ assumes "finite k" "continuous_on {a..b} f" "f a = y"
+ "\<forall>x\<in>({a..b} - k). (f has_derivative (\<lambda>h. 0)) (at x within {a..b})" "x \<in> {a..b}"
+ shows "f x = y"
+proof- have ab:"a\<le>b" using assms by auto
+ have *:"(\<lambda>x. 0\<Colon>'a) \<circ> dest_vec1 = (\<lambda>x. 0)" unfolding o_def by auto have **:"a \<le> x" using assms by auto
+ have "((\<lambda>x. 0\<Colon>'a) \<circ> dest_vec1 has_integral f x - f a) {vec1 a..vec1 x}"
+ apply(rule fundamental_theorem_of_calculus_interior_strong[OF assms(1) ** ])
+ apply(rule continuous_on_subset[OF assms(2)]) defer
+ apply safe unfolding has_vector_derivative_def apply(subst has_derivative_within_open[THEN sym])
+ apply assumption apply(rule open_interval_real) apply(rule has_derivative_within_subset[where s="{a..b}"])
+ using assms(4) assms(5) by auto note this[unfolded *]
+ note has_integral_unique[OF has_integral_0 this]
+ thus ?thesis unfolding assms by auto qed
+
+subsection {* Generalize a bit to any convex set. *}
+
+lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
+ scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
+ scaleR_cancel_left scaleR_cancel_right scaleR.add_right scaleR.add_left real_vector_class.scaleR_one
+
+lemma has_derivative_zero_unique_strong_convex: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ assumes "convex s" "finite k" "continuous_on s f" "c \<in> s" "f c = y"
+ "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)" "x \<in> s"
+ shows "f x = y"
+proof- { presume *:"x \<noteq> c \<Longrightarrow> ?thesis" show ?thesis apply(cases,rule *,assumption)
+ unfolding assms(5)[THEN sym] by auto } assume "x\<noteq>c"
+ note conv = assms(1)[unfolded convex_alt,rule_format]
+ have as1:"continuous_on {0..1} (f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x))"
+ apply(rule continuous_on_intros)+ apply(rule continuous_on_subset[OF assms(3)])
+ apply safe apply(rule conv) using assms(4,7) by auto
+ have *:"\<And>t xa. (1 - t) *\<^sub>R c + t *\<^sub>R x = (1 - xa) *\<^sub>R c + xa *\<^sub>R x \<Longrightarrow> t = xa"
+ proof- case goal1 hence "(t - xa) *\<^sub>R x = (t - xa) *\<^sub>R c"
+ unfolding scaleR_simps by(auto simp add:group_simps)
+ thus ?case using `x\<noteq>c` by auto qed
+ have as2:"finite {t. ((1 - t) *\<^sub>R c + t *\<^sub>R x) \<in> k}" using assms(2)
+ apply(rule finite_surj[where f="\<lambda>z. SOME t. (1-t) *\<^sub>R c + t *\<^sub>R x = z"])
+ apply safe unfolding image_iff apply rule defer apply assumption
+ apply(rule sym) apply(rule some_equality) defer apply(drule *) by auto
+ have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x)) 1 = y"
+ apply(rule has_derivative_zero_unique_strong_interval[OF as2 as1, of ])
+ unfolding o_def using assms(5) defer apply-apply(rule)
+ proof- fix t assume as:"t\<in>{0..1} - {t. (1 - t) *\<^sub>R c + t *\<^sub>R x \<in> k}"
+ have *:"c - t *\<^sub>R c + t *\<^sub>R x \<in> s - k" apply safe apply(rule conv[unfolded scaleR_simps])
+ using `x\<in>s` `c\<in>s` as by(auto simp add:scaleR_simps)
+ have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
+ apply(rule diff_chain_within) apply(rule has_derivative_add)
+ unfolding scaleR_simps apply(rule has_derivative_sub) apply(rule has_derivative_const)
+ apply(rule has_derivative_vmul_within,rule has_derivative_id)+
+ apply(rule has_derivative_within_subset,rule assms(6)[rule_format])
+ apply(rule *) apply safe apply(rule conv[unfolded scaleR_simps]) using `x\<in>s` `c\<in>s` by auto
+ thus "((\<lambda>xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\<lambda>h. 0)) (at t within {0..1})" unfolding o_def .
+ qed auto thus ?thesis by auto qed
+
+subsection {* Also to any open connected set with finite set of exceptions. Could
+ generalize to locally convex set with limpt-free set of exceptions. *}
+
+lemma has_derivative_zero_unique_strong_connected: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ assumes "connected s" "open s" "finite k" "continuous_on s f" "c \<in> s" "f c = y"
+ "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)" "x\<in>s"
+ shows "f x = y"
+proof- have "{x \<in> s. f x \<in> {y}} = {} \<or> {x \<in> s. f x \<in> {y}} = s"
+ apply(rule assms(1)[unfolded connected_clopen,rule_format]) apply rule defer
+ apply(rule continuous_closed_in_preimage[OF assms(4) closed_sing])
+ apply(rule open_openin_trans[OF assms(2)]) unfolding open_contains_ball
+ proof safe fix x assume "x\<in>s"
+ from assms(2)[unfolded open_contains_ball,rule_format,OF this] guess e .. note e=conjunctD2[OF this]
+ show "\<exists>e>0. ball x e \<subseteq> {xa \<in> s. f xa \<in> {f x}}" apply(rule,rule,rule e)
+ proof safe fix y assume y:"y \<in> ball x e" thus "y\<in>s" using e by auto
+ show "f y = f x" apply(rule has_derivative_zero_unique_strong_convex[OF convex_ball])
+ apply(rule assms) apply(rule continuous_on_subset,rule assms) apply(rule e)+
+ apply(subst centre_in_ball,rule e,rule) apply safe
+ apply(rule has_derivative_within_subset) apply(rule assms(7)[rule_format])
+ using y e by auto qed qed
+ thus ?thesis using `x\<in>s` `f c = y` `c\<in>s` by auto qed
+
+subsection {* Integrating characteristic function of an interval. *}
+
+lemma has_integral_restrict_open_subinterval: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ assumes "(f has_integral i) {c..d}" "{c..d} \<subseteq> {a..b}"
+ shows "((\<lambda>x. if x \<in> {c<..<d} then f x else 0) has_integral i) {a..b}"
+proof- def g \<equiv> "\<lambda>x. if x \<in>{c<..<d} then f x else 0"
+ { presume *:"{c..d}\<noteq>{} \<Longrightarrow> ?thesis"
+ show ?thesis apply(cases,rule *,assumption)
+ proof- case goal1 hence *:"{c<..<d} = {}" using interval_open_subset_closed by auto
+ show ?thesis using assms(1) unfolding * using goal1 by auto
+ qed } assume "{c..d}\<noteq>{}"
+ from partial_division_extend_1[OF assms(2) this] guess p . note p=this
+ note mon = monoidal_lifted[OF monoidal_monoid]
+ note operat = operative_division[OF this operative_integral p(1), THEN sym]
+ let ?P = "(if g integrable_on {a..b} then Some (integral {a..b} g) else None) = Some i"
+ { presume "?P" hence "g integrable_on {a..b} \<and> integral {a..b} g = i"
+ apply- apply(cases,subst(asm) if_P,assumption) by auto
+ thus ?thesis using integrable_integral unfolding g_def by auto }
+
+ note iterate_eq_neutral[OF mon,unfolded neutral_lifted[OF monoidal_monoid]]
+ note * = this[unfolded neutral_monoid]
+ have iterate:"iterate (lifted op +) (p - {{c..d}})
+ (\<lambda>i. if g integrable_on i then Some (integral i g) else None) = Some 0"
+ proof(rule *,rule) case goal1 hence "x\<in>p" by auto note div = division_ofD(2-5)[OF p(1) this]
+ from div(3) guess u v apply-by(erule exE)+ note uv=this
+ have "interior x \<inter> interior {c..d} = {}" using div(4)[OF p(2)] goal1 by auto
+ hence "(g has_integral 0) x" unfolding uv apply-apply(rule has_integral_spike_interior[where f="\<lambda>x. 0"])
+ unfolding g_def interior_closed_interval by auto thus ?case by auto
+ qed
+
+ have *:"p = insert {c..d} (p - {{c..d}})" using p by auto
+ have **:"g integrable_on {c..d}" apply(rule integrable_spike_interior[where f=f])
+ unfolding g_def defer apply(rule has_integral_integrable) using assms(1) by auto
+ moreover have "integral {c..d} g = i" apply(rule has_integral_unique[OF _ assms(1)])
+ apply(rule has_integral_spike_interior[where f=g]) defer
+ apply(rule integrable_integral[OF **]) unfolding g_def by auto
+ ultimately show ?P unfolding operat apply- apply(subst *) apply(subst iterate_insert) apply rule+
+ unfolding iterate defer apply(subst if_not_P) defer using p by auto qed
+
+lemma has_integral_restrict_closed_subinterval: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ assumes "(f has_integral i) ({c..d})" "{c..d} \<subseteq> {a..b}"
+ shows "((\<lambda>x. if x \<in> {c..d} then f x else 0) has_integral i) {a..b}"
+proof- note has_integral_restrict_open_subinterval[OF assms]
+ note * = has_integral_spike[OF negligible_frontier_interval _ this]
+ show ?thesis apply(rule *[of c d]) using interval_open_subset_closed[of c d] by auto qed
+
+lemma has_integral_restrict_closed_subintervals_eq: fixes f::"real^'n \<Rightarrow> 'a::banach" assumes "{c..d} \<subseteq> {a..b}"
+ shows "((\<lambda>x. if x \<in> {c..d} then f x else 0) has_integral i) {a..b} \<longleftrightarrow> (f has_integral i) {c..d}" (is "?l = ?r")
+proof(cases "{c..d} = {}") case False let ?g = "\<lambda>x. if x \<in> {c..d} then f x else 0"
+ show ?thesis apply rule defer apply(rule has_integral_restrict_closed_subinterval[OF _ assms])
+ proof assumption assume ?l hence "?g integrable_on {c..d}"
+ apply-apply(rule integrable_subinterval[OF _ assms]) by auto
+ hence *:"f integrable_on {c..d}"apply-apply(rule integrable_eq) by auto
+ hence "i = integral {c..d} f" apply-apply(rule has_integral_unique)
+ apply(rule `?l`) apply(rule has_integral_restrict_closed_subinterval[OF _ assms]) by auto
+ thus ?r using * by auto qed qed auto
+
+subsection {* Hence we can apply the limit process uniformly to all integrals. *}
+
+lemma has_integral': fixes f::"real^'n \<Rightarrow> 'a::banach" shows
+ "(f has_integral i) s \<longleftrightarrow> (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b}
+ \<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> s then f(x) else 0) has_integral z) {a..b} \<and> norm(z - i) < e))" (is "?l \<longleftrightarrow> (\<forall>e>0. ?r e)")
+proof- { presume *:"\<exists>a b. s = {a..b} \<Longrightarrow> ?thesis"
+ show ?thesis apply(cases,rule *,assumption)
+ apply(subst has_integral_alt) by auto }
+ assume "\<exists>a b. s = {a..b}" then guess a b apply-by(erule exE)+ note s=this
+ from bounded_interval[of a b, THEN conjunct1, unfolded bounded_pos] guess B ..
+ note B = conjunctD2[OF this,rule_format] show ?thesis apply safe
+ proof- fix e assume ?l "e>(0::real)"
+ show "?r e" apply(rule_tac x="B+1" in exI) apply safe defer apply(rule_tac x=i in exI)
+ proof fix c d assume as:"ball 0 (B+1) \<subseteq> {c..d::real^'n}"
+ thus "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) {c..d}" unfolding s
+ apply-apply(rule has_integral_restrict_closed_subinterval) apply(rule `?l`[unfolded s])
+ apply safe apply(drule B(2)[rule_format]) unfolding subset_eq apply(erule_tac x=x in ballE)
+ by(auto simp add:vector_dist_norm)
+ qed(insert B `e>0`, auto)
+ next assume as:"\<forall>e>0. ?r e"
+ from this[rule_format,OF zero_less_one] guess C .. note C=conjunctD2[OF this,rule_format]
+ def c \<equiv> "(\<chi> i. - max B C)::real^'n" and d \<equiv> "(\<chi> i. max B C)::real^'n"
+ have c_d:"{a..b} \<subseteq> {c..d}" apply safe apply(drule B(2)) unfolding mem_interval
+ proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def
+ by(auto simp add:field_simps) qed
+ have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball vector_dist_norm
+ proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
+ from C(2)[OF this] have "\<exists>y. (f has_integral y) {a..b}"
+ unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,THEN sym] unfolding s by auto
+ then guess y .. note y=this
+
+ have "y = i" proof(rule ccontr) assume "y\<noteq>i" hence "0 < norm (y - i)" by auto
+ from as[rule_format,OF this] guess C .. note C=conjunctD2[OF this,rule_format]
+ def c \<equiv> "(\<chi> i. - max B C)::real^'n" and d \<equiv> "(\<chi> i. max B C)::real^'n"
+ have c_d:"{a..b} \<subseteq> {c..d}" apply safe apply(drule B(2)) unfolding mem_interval
+ proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def
+ by(auto simp add:field_simps) qed
+ have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball vector_dist_norm
+ proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
+ note C(2)[OF this] then guess z .. note z = conjunctD2[OF this, unfolded s]
+ note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]]
+ hence "z = y" "norm (z - i) < norm (y - i)" apply- apply(rule has_integral_unique[OF _ y(1)]) .
+ thus False by auto qed
+ thus ?l using y unfolding s by auto qed qed
+
+subsection {* Hence a general restriction property. *}
+
+lemma has_integral_restrict[simp]: assumes "s \<subseteq> t" shows
+ "((\<lambda>x. if x \<in> s then f x else (0::'a::banach)) has_integral i) t \<longleftrightarrow> (f has_integral i) s"
+proof- have *:"\<And>x. (if x \<in> t then if x \<in> s then f x else 0 else 0) = (if x\<in>s then f x else 0)" using assms by auto
+ show ?thesis apply(subst(2) has_integral') apply(subst has_integral') unfolding * by rule qed
+
+lemma has_integral_restrict_univ: fixes f::"real^'n \<Rightarrow> 'a::banach" shows
+ "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) UNIV \<longleftrightarrow> (f has_integral i) s" by auto
+
+lemma has_integral_on_superset: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ assumes "\<forall>x. ~(x \<in> s) \<longrightarrow> f x = 0" "s \<subseteq> t" "(f has_integral i) s"
+ shows "(f has_integral i) t"
+proof- have "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. if x \<in> t then f x else 0)"
+ apply(rule) using assms(1-2) by auto
+ thus ?thesis apply- using assms(3) apply(subst has_integral_restrict_univ[THEN sym])
+ apply- apply(subst(asm) has_integral_restrict_univ[THEN sym]) by auto qed
+
+lemma integrable_on_superset: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ assumes "\<forall>x. ~(x \<in> s) \<longrightarrow> f x = 0" "s \<subseteq> t" "f integrable_on s"
+ shows "f integrable_on t"
+ using assms unfolding integrable_on_def by(auto intro:has_integral_on_superset)
+
+lemma integral_restrict_univ[intro]: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ shows "f integrable_on s \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> s then f x else 0) = integral s f"
+ apply(rule integral_unique) unfolding has_integral_restrict_univ by auto
+
+lemma integrable_restrict_univ: fixes f::"real^'n \<Rightarrow> 'a::banach" shows
+ "(\<lambda>x. if x \<in> s then f x else 0) integrable_on UNIV \<longleftrightarrow> f integrable_on s"
+ unfolding integrable_on_def by auto
+
+lemma negligible_on_intervals: "negligible s \<longleftrightarrow> (\<forall>a b. negligible(s \<inter> {a..b}))" (is "?l = ?r")
+proof assume ?r show ?l unfolding negligible_def
+ proof safe case goal1 show ?case apply(rule has_integral_negligible[OF `?r`[rule_format,of a b]])
+ unfolding indicator_def by auto qed qed auto
+
+lemma has_integral_spike_set_eq: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ assumes "negligible((s - t) \<union> (t - s))" shows "((f has_integral y) s \<longleftrightarrow> (f has_integral y) t)"
+ unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by auto
+
+lemma has_integral_spike_set[dest]: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ assumes "negligible((s - t) \<union> (t - s))" "(f has_integral y) s"
+ shows "(f has_integral y) t"
+ using assms has_integral_spike_set_eq by auto
+
+lemma integrable_spike_set[dest]: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ assumes "negligible((s - t) \<union> (t - s))" "f integrable_on s"
+ shows "f integrable_on t" using assms(2) unfolding integrable_on_def
+ unfolding has_integral_spike_set_eq[OF assms(1)] .
+
+lemma integrable_spike_set_eq: fixes f::"real^'n \<Rightarrow> 'a::banach"
+ assumes "negligible((s - t) \<union> (t - s))"
+ shows "(f integrable_on s \<longleftrightarrow> f integrable_on t)"
+ apply(rule,rule_tac[!] integrable_spike_set) using assms by auto
+
+(*lemma integral_spike_set:
+ "\<forall>f:real^M->real^N g s t.
+ negligible(s DIFF t \<union> t DIFF s)
+ \<longrightarrow> integral s f = integral t f"
+qed REPEAT STRIP_TAC THEN REWRITE_TAC[integral] THEN
+ AP_TERM_TAC THEN ABS_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN
+ ASM_MESON_TAC[]);;
+
+lemma has_integral_interior:
+ "\<forall>f:real^M->real^N y s.
+ negligible(frontier s)
+ \<longrightarrow> ((f has_integral y) (interior s) \<longleftrightarrow> (f has_integral y) s)"
+qed REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN
+ FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
+ NEGLIGIBLE_SUBSET)) THEN
+ REWRITE_TAC[frontier] THEN
+ MP_TAC(ISPEC `s:real^M->bool` INTERIOR_SUBSET) THEN
+ MP_TAC(ISPEC `s:real^M->bool` CLOSURE_SUBSET) THEN
+ SET_TAC[]);;
+
+lemma has_integral_closure:
+ "\<forall>f:real^M->real^N y s.
+ negligible(frontier s)
+ \<longrightarrow> ((f has_integral y) (closure s) \<longleftrightarrow> (f has_integral y) s)"
+qed REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN
+ FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
+ NEGLIGIBLE_SUBSET)) THEN
+ REWRITE_TAC[frontier] THEN
+ MP_TAC(ISPEC `s:real^M->bool` INTERIOR_SUBSET) THEN
+ MP_TAC(ISPEC `s:real^M->bool` CLOSURE_SUBSET) THEN
+ SET_TAC[]);;*)
+
+subsection {* More lemmas that are useful later. *}
+
+lemma has_integral_subset_component_le: fixes f::"real^'n \<Rightarrow> real^'m"
+ assumes "s \<subseteq> t" "(f has_integral i) s" "(f has_integral j) t" "\<forall>x\<in>t. 0 \<le> f(x)$k"
+ shows "i$k \<le> j$k"
+proof- note has_integral_restrict_univ[THEN sym, of f]
+ note assms(2-3)[unfolded this] note * = has_integral_component_le[OF this]
+ show ?thesis apply(rule *) using assms(1,4) by auto qed
+
+lemma integral_subset_component_le: fixes f::"real^'n \<Rightarrow> real^'m"
+ assumes "s \<subseteq> t" "f integrable_on s" "f integrable_on t" "\<forall>x \<in> t. 0 \<le> f(x)$k"
+ shows "(integral s f)$k \<le> (integral t f)$k"
+ apply(rule has_integral_subset_component_le) using assms by auto
+
+lemma has_integral_alt': fixes f::"real^'n \<Rightarrow> 'a::banach"
+ shows "(f has_integral i) s \<longleftrightarrow> (\<forall>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}) \<and>
+ (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e)" (is "?l = ?r")
+proof assume ?r
+ show ?l apply- apply(subst has_integral')
+ proof safe case goal1 from `?r`[THEN conjunct2,rule_format,OF this] guess B .. note B=conjunctD2[OF this]
+ show ?case apply(rule,rule,rule B,safe)
+ apply(rule_tac x="integral {a..b} (\<lambda>x. if x \<in> s then f x else 0)" in exI)
+ apply(drule B(2)[rule_format]) using integrable_integral[OF `?r`[THEN conjunct1,rule_format]] by auto
+ qed next
+ assume ?l note as = this[unfolded has_integral'[of f],rule_format]
+ let ?f = "\<lambda>x. if x \<in> s then f x else 0"
+ show ?r proof safe fix a b::"real^'n"
+ from as[OF zero_less_one] guess B .. note B=conjunctD2[OF this,rule_format]
+ let ?a = "(\<chi> i. min (a$i) (-B))::real^'n" and ?b = "(\<chi> i. max (b$i) B)::real^'n"
+ show "?f integrable_on {a..b}" apply(rule integrable_subinterval[of _ ?a ?b])
+ proof- have "ball 0 B \<subseteq> {?a..?b}" apply safe unfolding mem_ball mem_interval vector_dist_norm
+ proof case goal1 thus ?case using component_le_norm[of x i] by(auto simp add:field_simps) qed
+ from B(2)[OF this] guess z .. note conjunct1[OF this]
+ thus "?f integrable_on {?a..?b}" unfolding integrable_on_def by auto
+ show "{a..b} \<subseteq> {?a..?b}" apply safe unfolding mem_interval apply(rule,erule_tac x=i in allE) by auto qed
+
+ fix e::real assume "e>0" from as[OF this] guess B .. note B=conjunctD2[OF this,rule_format]
+ show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
+ norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
+ proof(rule,rule,rule B,safe) case goal1 from B(2)[OF this] guess z .. note z=conjunctD2[OF this]
+ from integral_unique[OF this(1)] show ?case using z(2) by auto qed qed qed
+
+
+
+declare [[smt_certificates=""]]
+
end
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Mar 12 14:04:59 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Mar 12 20:04:48 2010 +0100
@@ -464,13 +464,13 @@
theorem dataset_skew_split:
"dataset (skew t) = dataset t"
"dataset (split t) = dataset t"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
sorry
theorem wf_skew_split:
"wf t \<Longrightarrow> skew t = t"
"wf t \<Longrightarrow> split t = t"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
sorry
primrec insort\<^isub>1 where
@@ -494,11 +494,11 @@
(if x > y then insort\<^isub>2 u x else u))"
theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
sorry
theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
sorry
end
--- a/src/HOL/Probability/Borel.thy Fri Mar 12 14:04:59 2010 +0100
+++ b/src/HOL/Probability/Borel.thy Fri Mar 12 20:04:48 2010 +0100
@@ -434,6 +434,14 @@
unfolding field_divide_inverse
by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
+lemma (in measure_space) borel_measurable_vimage:
+ assumes borel: "f \<in> borel_measurable M"
+ shows "f -` {X} \<inter> space M \<in> sets M"
+proof -
+ have "{w \<in> space M. f w = X} = {w. f w = X} \<inter> space M" by auto
+ with borel_measurable_eq_borel_measurable[OF borel borel_measurable_const, of X]
+ show ?thesis unfolding vimage_def by simp
+qed
section "Monotone convergence"
--- a/src/HOL/Probability/Lebesgue.thy Fri Mar 12 14:04:59 2010 +0100
+++ b/src/HOL/Probability/Lebesgue.thy Fri Mar 12 20:04:48 2010 +0100
@@ -673,6 +673,9 @@
unfolding nnfis_def mono_convergent_def incseq_def
by (auto intro!: exI[of _ "\<lambda>n. f"] exI[of _ "\<lambda>n. a"] LIMSEQ_const)
+lemma nnfis_0: "0 \<in> nnfis (\<lambda> x. 0)"
+ by (rule psfis_nnfis[OF psfis_0])
+
lemma nnfis_times:
assumes "a \<in> nnfis f" and "0 \<le> z"
shows "z * a \<in> nnfis (\<lambda>t. z * f t)"
@@ -836,7 +839,7 @@
using assms
proof -
from assms[unfolded nnfis_def] guess u y by auto note uy = this
- hence "\<And> n. 0 \<le> u n x"
+ hence "\<And> n. 0 \<le> u n x"
unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
by auto
thus "0 \<le> f x" using uy[rule_format]
@@ -1307,6 +1310,190 @@
by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
qed
+section "Lebesgue integration on countable spaces"
+
+lemma nnfis_on_countable:
+ assumes borel: "f \<in> borel_measurable M"
+ and bij: "bij_betw enum S (f ` space M - {0})"
+ and enum_zero: "enum ` (-S) \<subseteq> {0}"
+ and nn_enum: "\<And>n. 0 \<le> enum n"
+ and sums: "(\<lambda>r. enum r * measure M (f -` {enum r} \<inter> space M)) sums x" (is "?sum sums x")
+ shows "x \<in> nnfis f"
+proof -
+ have inj_enum: "inj_on enum S"
+ and range_enum: "enum ` S = f ` space M - {0}"
+ using bij by (auto simp: bij_betw_def)
+
+ let "?x n z" = "\<Sum>i = 0..<n. enum i * indicator_fn (f -` {enum i} \<inter> space M) z"
+
+ show ?thesis
+ proof (rule nnfis_mon_conv)
+ show "(\<lambda>n. \<Sum>i = 0..<n. ?sum i) ----> x" using sums unfolding sums_def .
+ next
+ fix n
+ show "(\<Sum>i = 0..<n. ?sum i) \<in> nnfis (?x n)"
+ proof (induct n)
+ case 0 thus ?case by (simp add: nnfis_0)
+ next
+ case (Suc n) thus ?case using nn_enum
+ by (auto intro!: nnfis_add nnfis_times psfis_nnfis[OF psfis_indicator] borel_measurable_vimage[OF borel])
+ qed
+ next
+ show "mono_convergent ?x f (space M)"
+ proof (rule mono_convergentI)
+ fix x
+ show "incseq (\<lambda>n. ?x n x)"
+ by (rule incseq_SucI, auto simp: indicator_fn_def nn_enum)
+
+ have fin: "\<And>n. finite (enum ` ({0..<n} \<inter> S))" by auto
+
+ assume "x \<in> space M"
+ hence "f x \<in> enum ` S \<or> f x = 0" using range_enum by auto
+ thus "(\<lambda>n. ?x n x) ----> f x"
+ proof (rule disjE)
+ assume "f x \<in> enum ` S"
+ then obtain i where "i \<in> S" and "f x = enum i" by auto
+
+ { fix n
+ have sum_ranges:
+ "i < n \<Longrightarrow> enum`({0..<n} \<inter> S) \<inter> {z. enum i = z \<and> x\<in>space M} = {enum i}"
+ "\<not> i < n \<Longrightarrow> enum`({0..<n} \<inter> S) \<inter> {z. enum i = z \<and> x\<in>space M} = {}"
+ using `x \<in> space M` `i \<in> S` inj_enum[THEN inj_on_iff] by auto
+ have "?x n x =
+ (\<Sum>i \<in> {0..<n} \<inter> S. enum i * indicator_fn (f -` {enum i} \<inter> space M) x)"
+ using enum_zero by (auto intro!: setsum_mono_zero_cong_right)
+ also have "... =
+ (\<Sum>z \<in> enum`({0..<n} \<inter> S). z * indicator_fn (f -` {z} \<inter> space M) x)"
+ using inj_enum[THEN subset_inj_on] by (auto simp: setsum_reindex)
+ also have "... = (if i < n then f x else 0)"
+ unfolding indicator_fn_def if_distrib[where x=1 and y=0]
+ setsum_cases[OF fin]
+ using sum_ranges `f x = enum i`
+ by auto
+ finally have "?x n x = (if i < n then f x else 0)" . }
+ note sum_equals_if = this
+
+ show ?thesis unfolding sum_equals_if
+ by (rule LIMSEQ_offset[where k="i + 1"]) (auto intro!: LIMSEQ_const)
+ next
+ assume "f x = 0"
+ { fix n have "?x n x = 0"
+ unfolding indicator_fn_def if_distrib[where x=1 and y=0]
+ setsum_cases[OF finite_atLeastLessThan]
+ using `f x = 0` `x \<in> space M`
+ by (auto split: split_if) }
+ thus ?thesis using `f x = 0` by (auto intro!: LIMSEQ_const)
+ qed
+ qed
+ qed
+qed
+
+lemma integral_on_countable:
+ assumes borel: "f \<in> borel_measurable M"
+ and bij: "bij_betw enum S (f ` space M)"
+ and enum_zero: "enum ` (-S) \<subseteq> {0}"
+ and abs_summable: "summable (\<lambda>r. \<bar>enum r * measure M (f -` {enum r} \<inter> space M)\<bar>)"
+ shows "integrable f"
+ and "integral f = (\<Sum>r. enum r * measure M (f -` {enum r} \<inter> space M))" (is "_ = suminf (?sum f enum)")
+proof -
+ { fix f enum
+ assume borel: "f \<in> borel_measurable M"
+ and bij: "bij_betw enum S (f ` space M)"
+ and enum_zero: "enum ` (-S) \<subseteq> {0}"
+ and abs_summable: "summable (\<lambda>r. \<bar>enum r * measure M (f -` {enum r} \<inter> space M)\<bar>)"
+ have inj_enum: "inj_on enum S" and range_enum: "f ` space M = enum ` S"
+ using bij unfolding bij_betw_def by auto
+
+ have [simp, intro]: "\<And>X. 0 \<le> measure M (f -` {X} \<inter> space M)"
+ by (rule positive, rule borel_measurable_vimage[OF borel])
+
+ have "(\<Sum>r. ?sum (pos_part f) (pos_part enum) r) \<in> nnfis (pos_part f) \<and>
+ summable (\<lambda>r. ?sum (pos_part f) (pos_part enum) r)"
+ proof (rule conjI, rule nnfis_on_countable)
+ have pos_f_image: "pos_part f ` space M - {0} = f ` space M \<inter> {0<..}"
+ unfolding pos_part_def max_def by auto
+
+ show "bij_betw (pos_part enum) {x \<in> S. 0 < enum x} (pos_part f ` space M - {0})"
+ unfolding bij_betw_def pos_f_image
+ unfolding pos_part_def max_def range_enum
+ by (auto intro!: inj_onI simp: inj_enum[THEN inj_on_eq_iff])
+
+ show "\<And>n. 0 \<le> pos_part enum n" unfolding pos_part_def max_def by auto
+
+ show "pos_part f \<in> borel_measurable M"
+ by (rule pos_part_borel_measurable[OF borel])
+
+ show "pos_part enum ` (- {x \<in> S. 0 < enum x}) \<subseteq> {0}"
+ unfolding pos_part_def max_def using enum_zero by auto
+
+ show "summable (\<lambda>r. ?sum (pos_part f) (pos_part enum) r)"
+ proof (rule summable_comparison_test[OF _ abs_summable], safe intro!: exI[of _ 0])
+ fix n :: nat
+ have "pos_part enum n \<noteq> 0 \<Longrightarrow> (pos_part f -` {enum n} \<inter> space M) =
+ (if 0 < enum n then (f -` {enum n} \<inter> space M) else {})"
+ unfolding pos_part_def max_def by (auto split: split_if_asm)
+ thus "norm (?sum (pos_part f) (pos_part enum) n) \<le> \<bar>?sum f enum n \<bar>"
+ by (cases "pos_part enum n = 0",
+ auto simp: pos_part_def max_def abs_mult not_le split: split_if_asm intro!: mult_nonpos_nonneg)
+ qed
+ thus "(\<lambda>r. ?sum (pos_part f) (pos_part enum) r) sums (\<Sum>r. ?sum (pos_part f) (pos_part enum) r)"
+ by (rule summable_sums)
+ qed }
+ note pos = this
+
+ note pos_part = pos[OF assms(1-4)]
+ moreover
+ have neg_part_to_pos_part:
+ "\<And>f :: _ \<Rightarrow> real. neg_part f = pos_part (uminus \<circ> f)"
+ by (auto simp: pos_part_def neg_part_def min_def max_def expand_fun_eq)
+
+ have neg_part: "(\<Sum>r. ?sum (neg_part f) (neg_part enum) r) \<in> nnfis (neg_part f) \<and>
+ summable (\<lambda>r. ?sum (neg_part f) (neg_part enum) r)"
+ unfolding neg_part_to_pos_part
+ proof (rule pos)
+ show "uminus \<circ> f \<in> borel_measurable M" unfolding comp_def
+ by (rule borel_measurable_uminus_borel_measurable[OF borel])
+
+ show "bij_betw (uminus \<circ> enum) S ((uminus \<circ> f) ` space M)"
+ using bij unfolding bij_betw_def
+ by (auto intro!: comp_inj_on simp: image_compose)
+
+ show "(uminus \<circ> enum) ` (- S) \<subseteq> {0}"
+ using enum_zero by auto
+
+ have minus_image: "\<And>r. (uminus \<circ> f) -` {(uminus \<circ> enum) r} \<inter> space M = f -` {enum r} \<inter> space M"
+ by auto
+ show "summable (\<lambda>r. \<bar>(uminus \<circ> enum) r * measure_space.measure M ((uminus \<circ> f) -` {(uminus \<circ> enum) r} \<inter> space M)\<bar>)"
+ unfolding minus_image using abs_summable by simp
+ qed
+ ultimately show "integrable f" unfolding integrable_def by auto
+
+ { fix r
+ have "?sum (pos_part f) (pos_part enum) r - ?sum (neg_part f) (neg_part enum) r = ?sum f enum r"
+ proof (cases rule: linorder_cases)
+ assume "0 < enum r"
+ hence "pos_part f -` {enum r} \<inter> space M = f -` {enum r} \<inter> space M"
+ unfolding pos_part_def max_def by (auto split: split_if_asm)
+ with `0 < enum r` show ?thesis unfolding pos_part_def neg_part_def min_def max_def expand_fun_eq
+ by auto
+ next
+ assume "enum r < 0"
+ hence "neg_part f -` {- enum r} \<inter> space M = f -` {enum r} \<inter> space M"
+ unfolding neg_part_def min_def by (auto split: split_if_asm)
+ with `enum r < 0` show ?thesis unfolding pos_part_def neg_part_def min_def max_def expand_fun_eq
+ by auto
+ qed (simp add: neg_part_def pos_part_def) }
+ note sum_diff_eq_sum = this
+
+ have "(\<Sum>r. ?sum (pos_part f) (pos_part enum) r) - (\<Sum>r. ?sum (neg_part f) (neg_part enum) r)
+ = (\<Sum>r. ?sum (pos_part f) (pos_part enum) r - ?sum (neg_part f) (neg_part enum) r)"
+ using neg_part pos_part by (auto intro: suminf_diff)
+ also have "... = (\<Sum>r. ?sum f enum r)" unfolding sum_diff_eq_sum ..
+ finally show "integral f = suminf (?sum f enum)"
+ unfolding integral_def using pos_part neg_part
+ by (auto dest: the_nnfis)
+qed
+
section "Lebesgue integration on finite space"
lemma integral_finite_on_sets:
@@ -1428,219 +1615,6 @@
using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
qed fact
-section "Lebesgue integration on countable spaces"
-
-definition
- "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
-
-lemma countable_space_integral_reduce:
- assumes "positive M (measure M)" and "f \<in> borel_measurable M"
- and "countable (f ` space M)"
- and "\<not> finite (pos_part f ` space M)"
- and "\<not> finite (neg_part f ` space M)"
- and "((\<lambda>r. r * measure m (neg_part f -` {r} \<inter> space m)) o enumerate (neg_part f ` space M)) sums n"
- and "((\<lambda>r. r * measure m (pos_part f -` {r} \<inter> space m)) o enumerate (pos_part f ` space M)) sums p"
- shows "integral f = p - n"
-oops
-
-(*
-val countable_space_integral_reduce = store_thm
- ("countable_space_integral_reduce",
- "\<forall>m f p n. measure_space m \<and>
- positive m \<and>
- f \<in> borel_measurable (space m, sets m) \<and>
- countable (IMAGE f (space m)) \<and>
- ~(FINITE (IMAGE (pos_part f) (space m))) \<and>
- ~(FINITE (IMAGE (neg_part f) (space m))) \<and>
- (\<lambda>r. r *
- measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
- enumerate ((IMAGE (neg_part f) (space m))) sums n \<and>
- (\<lambda>r. r *
- measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
- enumerate ((IMAGE (pos_part f) (space m))) sums p ==>
- (integral m f = p - n)",
- RW_TAC std_ss [integral_def]
- ++ Suff `((@i. i \<in> nnfis m (pos_part f)) = p) \<and> ((@i. i \<in> nnfis m (neg_part f)) = n)`
- >> RW_TAC std_ss []
- ++ (CONJ_TAC ++ MATCH_MP_TAC SELECT_UNIQUE ++ RW_TAC std_ss [])
- >> (Suff `p \<in> nnfis m (pos_part f)` >> METIS_TAC [nnfis_unique]
- ++ MATCH_MP_TAC nnfis_mon_conv
- ++ `BIJ (enumerate(IMAGE (pos_part f) (space m))) UNIV (IMAGE (pos_part f) (space m))`
- by (`countable (IMAGE (pos_part f) (space m))`
- by (MATCH_MP_TAC COUNTABLE_SUBSET
- ++ Q.EXISTS_TAC `0 INSERT (IMAGE f (space m))`
- ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, pos_part_def, COUNTABLE_INSERT, IN_INSERT]
- ++ METIS_TAC [])
- ++ METIS_TAC [COUNTABLE_ALT])
- ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
- ++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m)))
- (pred_set$count n) then pos_part f t else 0)`
- ++ Q.EXISTS_TAC `(\<lambda>n.
- sum (0,n)
- ((\<lambda>r.
- r *
- measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
- enumerate (IMAGE (pos_part f) (space m))))`
- ++ ASM_SIMP_TAC std_ss []
- ++ CONJ_TAC
- >> (RW_TAC std_ss [mono_convergent_def]
- >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, pos_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS])
- ++ RW_TAC std_ss [SEQ]
- ++ `\<exists>N. enumerate (IMAGE (pos_part f) (space m)) N = (pos_part f) t`
- by METIS_TAC [IN_IMAGE]
- ++ Q.EXISTS_TAC `SUC N`
- ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
- ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
- ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, pos_part_def])
- ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
- ++ `(\<lambda>t. (if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m))) (pred_set$count n')
- then pos_part f t else 0)) =
- (\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
- indicator_fn ((\<lambda>i. PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i}
- \<inter> (space m)) i) t)
- (pred_set$count n'))`
- by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
- >> (`pred_set$count n' = x INSERT (pred_set$count n')`
- by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
- ++ POP_ORW
- ++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
- ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
- REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
- ++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
- ++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
- enumerate (IMAGE (pos_part f) (space m)) x' *
- (if enumerate (IMAGE (pos_part f) (space m)) x =
- enumerate (IMAGE (pos_part f) (space m)) x'
- then 1 else 0) else 0)) = (\<lambda>x. 0)`
- by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
- ++ POP_ORW
- ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
- ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
- >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
- ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
- REAL_SUM_IMAGE_IN_IF]
- ++ `(\<lambda>x. (if x \<in> pred_set$count n' then
- (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i *
- (if (pos_part f t = enumerate (IMAGE (pos_part f) (space m)) i) \<and>
- t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
- by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
- ++ POP_ORW
- ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
- ++ POP_ORW
- ++ `((\<lambda>r. r * measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
- enumerate (IMAGE (pos_part f) (space m))) =
- (\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
- measure m ((\<lambda>i.
- PREIMAGE (pos_part f)
- {enumerate (IMAGE (pos_part f) (space m)) i} \<inter>
- space m) i))`
- by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
- ++ POP_ORW
- ++ MATCH_MP_TAC psfis_intro
- ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
- ++ REVERSE CONJ_TAC
- >> (FULL_SIMP_TAC real_ss [IN_IMAGE, pos_part_def]
- ++ METIS_TAC [REAL_LE_REFL])
- ++ `(pos_part f) \<in> borel_measurable (space m, sets m)`
- by METIS_TAC [pos_part_neg_part_borel_measurable]
- ++ REPEAT STRIP_TAC
- ++ `PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i} \<inter> space m =
- {w | w \<in> space m \<and> ((pos_part f) w = (\<lambda>w. enumerate (IMAGE (pos_part f) (space m)) i) w)}`
- by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
- ++ DECIDE_TAC)
- ++ POP_ORW
- ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
- ++ METIS_TAC [borel_measurable_const, measure_space_def])
- ++ Suff `n \<in> nnfis m (neg_part f)` >> METIS_TAC [nnfis_unique]
- ++ MATCH_MP_TAC nnfis_mon_conv
- ++ `BIJ (enumerate(IMAGE (neg_part f) (space m))) UNIV (IMAGE (neg_part f) (space m))`
- by (`countable (IMAGE (neg_part f) (space m))`
- by (MATCH_MP_TAC COUNTABLE_SUBSET
- ++ Q.EXISTS_TAC `0 INSERT (IMAGE abs (IMAGE f (space m)))`
- ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, abs, neg_part_def, COUNTABLE_INSERT, IN_INSERT, COUNTABLE_IMAGE]
- ++ METIS_TAC [])
- ++ METIS_TAC [COUNTABLE_ALT])
- ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
- ++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m)))
- (pred_set$count n) then neg_part f t else 0)`
- ++ Q.EXISTS_TAC `(\<lambda>n.
- sum (0,n)
- ((\<lambda>r.
- r *
- measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
- enumerate (IMAGE (neg_part f) (space m))))`
- ++ ASM_SIMP_TAC std_ss []
- ++ CONJ_TAC
- >> (RW_TAC std_ss [mono_convergent_def]
- >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, neg_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS, REAL_LE_NEGTOTAL])
- ++ RW_TAC std_ss [SEQ]
- ++ `\<exists>N. enumerate (IMAGE (neg_part f) (space m)) N = (neg_part f) t`
- by METIS_TAC [IN_IMAGE]
- ++ Q.EXISTS_TAC `SUC N`
- ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
- ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
- ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, neg_part_def])
- ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
- ++ `(\<lambda>t. (if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m))) (pred_set$count n')
- then neg_part f t else 0)) =
- (\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
- indicator_fn ((\<lambda>i. PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i}
- \<inter> (space m)) i) t)
- (pred_set$count n'))`
- by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
- >> (`pred_set$count n' = x INSERT (pred_set$count n')`
- by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
- ++ POP_ORW
- ++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
- ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
- REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
- ++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
- ++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
- enumerate (IMAGE (neg_part f) (space m)) x' *
- (if enumerate (IMAGE (neg_part f) (space m)) x =
- enumerate (IMAGE (neg_part f) (space m)) x'
- then 1 else 0) else 0)) = (\<lambda>x. 0)`
- by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
- ++ POP_ORW
- ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
- ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
- >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
- ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
- REAL_SUM_IMAGE_IN_IF]
- ++ `(\<lambda>x. (if x \<in> pred_set$count n' then
- (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i *
- (if (neg_part f t = enumerate (IMAGE (neg_part f) (space m)) i) \<and>
- t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
- by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
- ++ POP_ORW
- ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
- ++ POP_ORW
- ++ `((\<lambda>r. r * measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
- enumerate (IMAGE (neg_part f) (space m))) =
- (\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
- measure m ((\<lambda>i.
- PREIMAGE (neg_part f)
- {enumerate (IMAGE (neg_part f) (space m)) i} \<inter>
- space m) i))`
- by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
- ++ POP_ORW
- ++ MATCH_MP_TAC psfis_intro
- ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
- ++ REVERSE CONJ_TAC
- >> (FULL_SIMP_TAC real_ss [IN_IMAGE, neg_part_def]
- ++ METIS_TAC [REAL_LE_REFL, REAL_LE_NEGTOTAL])
- ++ `(neg_part f) \<in> borel_measurable (space m, sets m)`
- by METIS_TAC [pos_part_neg_part_borel_measurable]
- ++ REPEAT STRIP_TAC
- ++ `PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i} \<inter> space m =
- {w | w \<in> space m \<and> ((neg_part f) w = (\<lambda>w. enumerate (IMAGE (neg_part f) (space m)) i) w)}`
- by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
- ++ DECIDE_TAC)
- ++ POP_ORW
- ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
- ++ METIS_TAC [borel_measurable_const, measure_space_def]);
-*)
+end
end
-
-end
\ No newline at end of file
--- a/src/HOL/SEQ.thy Fri Mar 12 14:04:59 2010 +0100
+++ b/src/HOL/SEQ.thy Fri Mar 12 20:04:48 2010 +0100
@@ -981,6 +981,24 @@
by (blast intro: eq_refl X)
qed
+lemma incseq_SucI:
+ assumes "\<And>n. X n \<le> X (Suc n)"
+ shows "incseq X" unfolding incseq_def
+proof safe
+ fix m n :: nat
+ { fix d m :: nat
+ have "X m \<le> X (m + d)"
+ proof (induct d)
+ case (Suc d)
+ also have "X (m + d) \<le> X (m + Suc d)"
+ using assms by simp
+ finally show ?case .
+ qed simp }
+ note this[of m "n - m"]
+ moreover assume "m \<le> n"
+ ultimately show "X m \<le> X n" by simp
+qed
+
lemma decseq_imp_monoseq: "decseq X \<Longrightarrow> monoseq X"
by (simp add: decseq_def monoseq_def)