merged
authorblanchet
Wed, 21 Apr 2010 14:02:34 +0200
changeset 36267 26fb60d9d3f2
parent 36262 d7d1d87276b7 (diff)
parent 36266 28188e3650ee (current diff)
child 36268 65aabc2c89ae
merged
--- a/Admin/isatest/isatest-makedist	Wed Apr 21 14:02:19 2010 +0200
+++ b/Admin/isatest/isatest-makedist	Wed Apr 21 14:02:34 2010 +0200
@@ -55,7 +55,7 @@
 
 echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
 rm -rf $HOME/isabelle-*
-ssh atbroy102 "rm -rf /home/isatest/isabelle-cygwin-poly"
+ssh atbroy102 "rm -rf /home/isatest/isabelle-cygwin-poly-e"
 
 echo "### building distribution"  >> $DISTLOG 2>&1
 mkdir -p $DISTPREFIX
@@ -110,7 +110,7 @@
 sleep 15
 $SSH macbroy6 "sleep 10800; $MAKEALL $HOME/settings/at-mac-poly-5.1-para"
 sleep 15
-$SSH atbroy102 "$MAKEALL $HOME/settings/cygwin-poly"
+$SSH atbroy102 "$MAKEALL $HOME/settings/cygwin-poly-e"
 #sleep 15
 #$SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly"
 #sleep 15
--- a/Admin/isatest/settings/cygwin-poly	Wed Apr 21 14:02:19 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-  POLYML_HOME="/home/isatest/homebroy/home/polyml/polyml-5.3.0"
-  ML_SYSTEM="polyml-5.3.0"
-  ML_PLATFORM="x86-cygwin"
-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 200"
-
-ISABELLE_HOME_USER=~/isabelle-cygwin-poly
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false"
-
-init_component "$HOME/contrib_devel/kodkodi"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/settings/cygwin-poly-e	Wed Apr 21 14:02:34 2010 +0200
@@ -0,0 +1,27 @@
+# -*- shell-script -*- :mode=shellscript:
+
+  POLYML_HOME="/home/isatest/homebroy/home/polyml/polyml-5.3.0"
+  ML_SYSTEM="polyml-5.3.0"
+  ML_PLATFORM="x86-cygwin"
+  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+  ML_OPTIONS="-H 200"
+
+ISABELLE_HOME_USER=~/isabelle-cygwin-poly-e
+
+# Where to look for isabelle tools (multiple dirs separated by ':').
+ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
+
+# Location for temporary files (should be on a local file system).
+ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+
+
+# Heap input locations. ML system identifier is included in lookup.
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+
+# Heap output location. ML system identifier is appended automatically later on.
+ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
+ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
+
+ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false"
+
+init_component "$HOME/contrib_devel/kodkodi"
--- a/doc-src/Codegen/Thy/Program.thy	Wed Apr 21 14:02:19 2010 +0200
+++ b/doc-src/Codegen/Thy/Program.thy	Wed Apr 21 14:02:34 2010 +0200
@@ -571,21 +571,20 @@
 code_pred %quote lexord
 (*<*)
 proof -
-  fix r a1
-  assume lexord: "lexord r a1"
-  assume 1: "\<And> xs ys a v. a1 = (xs, ys) \<Longrightarrow> append xs (a # v) ys \<Longrightarrow> thesis"
-  assume 2: "\<And> xs ys u a v b w. a1 = (xs, ys) \<Longrightarrow> append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b) \<Longrightarrow> thesis"
-  obtain xs ys where a1: "a1 = (xs, ys)" by fastsimp
+  fix r xs ys
+  assume lexord: "lexord r (xs, ys)"
+  assume 1: "\<And> r' xs' ys' a v. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
+  assume 2: "\<And> r' xs' ys' u a v b w. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' (a, b) \<Longrightarrow> thesis"
   {
     assume "\<exists>a v. ys = xs @ a # v"
-    from this 1 a1 have thesis
+    from this 1 have thesis
         by (fastsimp simp add: append)
   } moreover
   {
     assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> ys = u @ b # w"
-    from this 2 a1 have thesis by (fastsimp simp add: append mem_def)
+    from this 2 have thesis by (fastsimp simp add: append mem_def)
   } moreover
-  note lexord[simplified a1]
+  note lexord
   ultimately show thesis
     unfolding lexord_def
     by (fastsimp simp add: Collect_def)
--- a/lib/Tools/java	Wed Apr 21 14:02:19 2010 +0200
+++ b/lib/Tools/java	Wed Apr 21 14:02:34 2010 +0200
@@ -5,4 +5,4 @@
 # DESCRIPTION: invoke Java within the Isabelle environment
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "${THIS_JAVA:-ISABELLE_JAVA}" "$@"
+exec "${THIS_JAVA:-$ISABELLE_JAVA}" "$@"
--- a/src/HOL/HOL.thy	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Apr 21 14:02:34 2010 +0200
@@ -2061,19 +2061,22 @@
   val name = "code_pred_def"
   val description = "alternative definitions of constants for the Predicate Compiler"
 )
-*}
-
-ML {*
 structure Predicate_Compile_Inline_Defs = Named_Thms
 (
   val name = "code_pred_inline"
   val description = "inlining definitions for the Predicate Compiler"
 )
+structure Predicate_Compile_Simps = Named_Thms
+(
+  val name = "code_pred_simp"
+  val description = "simplification rules for the optimisations in the Predicate Compiler"
+)
 *}
 
 setup {*
   Predicate_Compile_Alternative_Defs.setup
   #> Predicate_Compile_Inline_Defs.setup
+  #> Predicate_Compile_Simps.setup
 *}
 
 
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Apr 21 14:02:34 2010 +0200
@@ -6,6 +6,14 @@
 
 declare HOL.if_bool_eq_disj[code_pred_inline]
 
+declare bool_diff_def[code_pred_inline]
+declare inf_bool_eq_raw[code_pred_inline]
+declare less_bool_def_raw[code_pred_inline]
+declare le_bool_def_raw[code_pred_inline]
+
+lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
+by (rule eq_reflection) (auto simp add: expand_fun_eq min_def le_bool_def)
+
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
 
 section {* Pairs *}
@@ -35,6 +43,10 @@
   "(A - B) = (%x. A x \<and> \<not> B x)"
 by (auto simp add: mem_def)
 
+lemma subset_eq[code_pred_inline]:
+  "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
+by (rule eq_reflection) (fastsimp simp add: mem_def)
+
 lemma set_equality[code_pred_inline]:
   "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
 by (fastsimp simp add: mem_def)
@@ -141,7 +153,7 @@
   "less_nat 0 (Suc y)"
 | "less_nat x y ==> less_nat (Suc x) (Suc y)"
 
-lemma [code_pred_inline]:
+lemma less_nat[code_pred_inline]:
   "x < y = less_nat x y"
 apply (rule iffI)
 apply (induct x arbitrary: y)
@@ -228,6 +240,16 @@
     done
 qed
 
+section {* Simplification rules for optimisation *}
+
+lemma [code_pred_simp]: "\<not> False == True"
+by auto
+
+lemma [code_pred_simp]: "\<not> True == False"
+by auto
+
+lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
+unfolding less_nat[symmetric] by auto
 
 
 end
\ No newline at end of file
--- a/src/HOL/Multivariate_Analysis/Integration.cert	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.cert	Wed Apr 21 14:02:34 2010 +0200
@@ -3210,3 +3210,772 @@
 #228 := [unit-resolution #200 #220]: #173
 [th-lemma #228 #227 #211]: false
 unsat
+610fb185d846b293ce6bb466b6770a65def3e59c 768 0
+#2 := false
+#7 := 0::real
+decl uf_2 :: real
+#5 := uf_2
+#75 := -1::real
+#76 := (* -1::real uf_2)
+decl uf_1 :: real
+#4 := uf_1
+#77 := (+ uf_1 #76)
+#316 := (>= #77 0::real)
+#317 := (not #316)
+decl uf_8 :: real
+#39 := uf_8
+#216 := (* -1::real uf_8)
+#220 := (+ uf_1 #216)
+#221 := (<= #220 0::real)
+#86 := (* -1::real uf_1)
+#87 := (+ #86 uf_2)
+#323 := (ite #316 #77 #87)
+#331 := (* -1::real #323)
+decl uf_3 :: real
+#11 := uf_3
+#95 := 1/3::real
+#96 := (* 1/3::real uf_3)
+#332 := (+ #96 #331)
+#333 := (<= #332 0::real)
+#334 := (not #333)
+decl uf_4 :: real
+#15 := uf_4
+#111 := (* -1::real uf_4)
+#112 := (+ uf_2 #111)
+#102 := (+ #76 uf_4)
+#293 := (<= #112 0::real)
+#300 := (ite #293 #102 #112)
+#308 := (* -1::real #300)
+#309 := (+ #96 #308)
+#310 := (<= #309 0::real)
+#311 := (not #310)
+decl uf_6 :: real
+#22 := uf_6
+decl uf_5 :: real
+#21 := uf_5
+#133 := (* -1::real uf_5)
+#134 := (+ #133 uf_6)
+#123 := (* -1::real uf_6)
+#124 := (+ uf_5 #123)
+#270 := (>= #124 0::real)
+#277 := (ite #270 #124 #134)
+#285 := (* -1::real #277)
+#286 := (+ #96 #285)
+#287 := (<= #286 0::real)
+#288 := (not #287)
+decl uf_7 :: real
+#28 := uf_7
+#154 := (* -1::real uf_7)
+#155 := (+ uf_6 #154)
+#145 := (+ #123 uf_7)
+#247 := (<= #155 0::real)
+#254 := (ite #247 #145 #155)
+#262 := (* -1::real #254)
+#263 := (+ #96 #262)
+#264 := (<= #263 0::real)
+#265 := (not #264)
+#175 := (+ #76 uf_6)
+#166 := (+ uf_2 #123)
+#224 := (>= #166 0::real)
+#231 := (ite #224 #166 #175)
+#239 := (* -1::real #231)
+#240 := (+ #96 #239)
+#241 := (<= #240 0::real)
+#242 := (not #241)
+#217 := (+ uf_5 #216)
+#215 := (>= #217 0::real)
+decl uf_9 :: real
+#42 := uf_9
+#206 := (* -1::real uf_9)
+#212 := (+ uf_7 #206)
+#211 := (>= #212 0::real)
+#207 := (+ uf_4 #206)
+#208 := (<= #207 0::real)
+#363 := (and #208 #211 #215 #221 #242 #265 #288 #311 #334)
+#44 := (<= uf_9 uf_7)
+#43 := (<= uf_4 uf_9)
+#45 := (and #43 #44)
+#41 := (<= uf_8 uf_5)
+#46 := (and #41 #45)
+#40 := (<= uf_1 uf_8)
+#47 := (and #40 #46)
+#12 := 3::real
+#13 := (/ uf_3 3::real)
+#34 := (- uf_2 uf_6)
+#36 := (- #34)
+#35 := (< #34 0::real)
+#37 := (ite #35 #36 #34)
+#38 := (< #37 #13)
+#48 := (and #38 #47)
+#29 := (- uf_7 uf_6)
+#31 := (- #29)
+#30 := (< #29 0::real)
+#32 := (ite #30 #31 #29)
+#33 := (< #32 #13)
+#49 := (and #33 #48)
+#23 := (- uf_5 uf_6)
+#25 := (- #23)
+#24 := (< #23 0::real)
+#26 := (ite #24 #25 #23)
+#27 := (< #26 #13)
+#50 := (and #27 #49)
+#16 := (- uf_4 uf_2)
+#18 := (- #16)
+#17 := (< #16 0::real)
+#19 := (ite #17 #18 #16)
+#20 := (< #19 #13)
+#51 := (and #20 #50)
+#6 := (- uf_1 uf_2)
+#9 := (- #6)
+#8 := (< #6 0::real)
+#10 := (ite #8 #9 #6)
+#14 := (< #10 #13)
+#52 := (and #14 #51)
+#368 := (iff #52 #363)
+#169 := (< #166 0::real)
+#180 := (ite #169 #175 #166)
+#183 := (< #180 #96)
+#189 := (and #47 #183)
+#148 := (< #145 0::real)
+#160 := (ite #148 #155 #145)
+#163 := (< #160 #96)
+#194 := (and #163 #189)
+#127 := (< #124 0::real)
+#139 := (ite #127 #134 #124)
+#142 := (< #139 #96)
+#197 := (and #142 #194)
+#105 := (< #102 0::real)
+#117 := (ite #105 #112 #102)
+#120 := (< #117 #96)
+#200 := (and #120 #197)
+#80 := (< #77 0::real)
+#92 := (ite #80 #87 #77)
+#99 := (< #92 #96)
+#203 := (and #99 #200)
+#366 := (iff #203 #363)
+#339 := (and #208 #211)
+#342 := (and #215 #339)
+#345 := (and #221 #342)
+#348 := (and #345 #242)
+#351 := (and #265 #348)
+#354 := (and #288 #351)
+#357 := (and #311 #354)
+#360 := (and #334 #357)
+#364 := (iff #360 #363)
+#365 := [rewrite]: #364
+#361 := (iff #203 #360)
+#358 := (iff #200 #357)
+#355 := (iff #197 #354)
+#352 := (iff #194 #351)
+#349 := (iff #189 #348)
+#245 := (iff #183 #242)
+#236 := (< #231 #96)
+#243 := (iff #236 #242)
+#244 := [rewrite]: #243
+#237 := (iff #183 #236)
+#234 := (= #180 #231)
+#225 := (not #224)
+#228 := (ite #225 #175 #166)
+#232 := (= #228 #231)
+#233 := [rewrite]: #232
+#229 := (= #180 #228)
+#226 := (iff #169 #225)
+#227 := [rewrite]: #226
+#230 := [monotonicity #227]: #229
+#235 := [trans #230 #233]: #234
+#238 := [monotonicity #235]: #237
+#246 := [trans #238 #244]: #245
+#346 := (iff #47 #345)
+#343 := (iff #46 #342)
+#340 := (iff #45 #339)
+#213 := (iff #44 #211)
+#214 := [rewrite]: #213
+#209 := (iff #43 #208)
+#210 := [rewrite]: #209
+#341 := [monotonicity #210 #214]: #340
+#218 := (iff #41 #215)
+#219 := [rewrite]: #218
+#344 := [monotonicity #219 #341]: #343
+#222 := (iff #40 #221)
+#223 := [rewrite]: #222
+#347 := [monotonicity #223 #344]: #346
+#350 := [monotonicity #347 #246]: #349
+#268 := (iff #163 #265)
+#259 := (< #254 #96)
+#266 := (iff #259 #265)
+#267 := [rewrite]: #266
+#260 := (iff #163 #259)
+#257 := (= #160 #254)
+#248 := (not #247)
+#251 := (ite #248 #155 #145)
+#255 := (= #251 #254)
+#256 := [rewrite]: #255
+#252 := (= #160 #251)
+#249 := (iff #148 #248)
+#250 := [rewrite]: #249
+#253 := [monotonicity #250]: #252
+#258 := [trans #253 #256]: #257
+#261 := [monotonicity #258]: #260
+#269 := [trans #261 #267]: #268
+#353 := [monotonicity #269 #350]: #352
+#291 := (iff #142 #288)
+#282 := (< #277 #96)
+#289 := (iff #282 #288)
+#290 := [rewrite]: #289
+#283 := (iff #142 #282)
+#280 := (= #139 #277)
+#271 := (not #270)
+#274 := (ite #271 #134 #124)
+#278 := (= #274 #277)
+#279 := [rewrite]: #278
+#275 := (= #139 #274)
+#272 := (iff #127 #271)
+#273 := [rewrite]: #272
+#276 := [monotonicity #273]: #275
+#281 := [trans #276 #279]: #280
+#284 := [monotonicity #281]: #283
+#292 := [trans #284 #290]: #291
+#356 := [monotonicity #292 #353]: #355
+#314 := (iff #120 #311)
+#305 := (< #300 #96)
+#312 := (iff #305 #311)
+#313 := [rewrite]: #312
+#306 := (iff #120 #305)
+#303 := (= #117 #300)
+#294 := (not #293)
+#297 := (ite #294 #112 #102)
+#301 := (= #297 #300)
+#302 := [rewrite]: #301
+#298 := (= #117 #297)
+#295 := (iff #105 #294)
+#296 := [rewrite]: #295
+#299 := [monotonicity #296]: #298
+#304 := [trans #299 #302]: #303
+#307 := [monotonicity #304]: #306
+#315 := [trans #307 #313]: #314
+#359 := [monotonicity #315 #356]: #358
+#337 := (iff #99 #334)
+#328 := (< #323 #96)
+#335 := (iff #328 #334)
+#336 := [rewrite]: #335
+#329 := (iff #99 #328)
+#326 := (= #92 #323)
+#320 := (ite #317 #87 #77)
+#324 := (= #320 #323)
+#325 := [rewrite]: #324
+#321 := (= #92 #320)
+#318 := (iff #80 #317)
+#319 := [rewrite]: #318
+#322 := [monotonicity #319]: #321
+#327 := [trans #322 #325]: #326
+#330 := [monotonicity #327]: #329
+#338 := [trans #330 #336]: #337
+#362 := [monotonicity #338 #359]: #361
+#367 := [trans #362 #365]: #366
+#204 := (iff #52 #203)
+#201 := (iff #51 #200)
+#198 := (iff #50 #197)
+#195 := (iff #49 #194)
+#192 := (iff #48 #189)
+#186 := (and #183 #47)
+#190 := (iff #186 #189)
+#191 := [rewrite]: #190
+#187 := (iff #48 #186)
+#184 := (iff #38 #183)
+#97 := (= #13 #96)
+#98 := [rewrite]: #97
+#181 := (= #37 #180)
+#167 := (= #34 #166)
+#168 := [rewrite]: #167
+#178 := (= #36 #175)
+#172 := (- #166)
+#176 := (= #172 #175)
+#177 := [rewrite]: #176
+#173 := (= #36 #172)
+#174 := [monotonicity #168]: #173
+#179 := [trans #174 #177]: #178
+#170 := (iff #35 #169)
+#171 := [monotonicity #168]: #170
+#182 := [monotonicity #171 #179 #168]: #181
+#185 := [monotonicity #182 #98]: #184
+#188 := [monotonicity #185]: #187
+#193 := [trans #188 #191]: #192
+#164 := (iff #33 #163)
+#161 := (= #32 #160)
+#146 := (= #29 #145)
+#147 := [rewrite]: #146
+#158 := (= #31 #155)
+#151 := (- #145)
+#156 := (= #151 #155)
+#157 := [rewrite]: #156
+#152 := (= #31 #151)
+#153 := [monotonicity #147]: #152
+#159 := [trans #153 #157]: #158
+#149 := (iff #30 #148)
+#150 := [monotonicity #147]: #149
+#162 := [monotonicity #150 #159 #147]: #161
+#165 := [monotonicity #162 #98]: #164
+#196 := [monotonicity #165 #193]: #195
+#143 := (iff #27 #142)
+#140 := (= #26 #139)
+#125 := (= #23 #124)
+#126 := [rewrite]: #125
+#137 := (= #25 #134)
+#130 := (- #124)
+#135 := (= #130 #134)
+#136 := [rewrite]: #135
+#131 := (= #25 #130)
+#132 := [monotonicity #126]: #131
+#138 := [trans #132 #136]: #137
+#128 := (iff #24 #127)
+#129 := [monotonicity #126]: #128
+#141 := [monotonicity #129 #138 #126]: #140
+#144 := [monotonicity #141 #98]: #143
+#199 := [monotonicity #144 #196]: #198
+#121 := (iff #20 #120)
+#118 := (= #19 #117)
+#103 := (= #16 #102)
+#104 := [rewrite]: #103
+#115 := (= #18 #112)
+#108 := (- #102)
+#113 := (= #108 #112)
+#114 := [rewrite]: #113
+#109 := (= #18 #108)
+#110 := [monotonicity #104]: #109
+#116 := [trans #110 #114]: #115
+#106 := (iff #17 #105)
+#107 := [monotonicity #104]: #106
+#119 := [monotonicity #107 #116 #104]: #118
+#122 := [monotonicity #119 #98]: #121
+#202 := [monotonicity #122 #199]: #201
+#100 := (iff #14 #99)
+#93 := (= #10 #92)
+#78 := (= #6 #77)
+#79 := [rewrite]: #78
+#90 := (= #9 #87)
+#83 := (- #77)
+#88 := (= #83 #87)
+#89 := [rewrite]: #88
+#84 := (= #9 #83)
+#85 := [monotonicity #79]: #84
+#91 := [trans #85 #89]: #90
+#81 := (iff #8 #80)
+#82 := [monotonicity #79]: #81
+#94 := [monotonicity #82 #91 #79]: #93
+#101 := [monotonicity #94 #98]: #100
+#205 := [monotonicity #101 #202]: #204
+#369 := [trans #205 #367]: #368
+#74 := [asserted]: #52
+#370 := [mp #74 #369]: #363
+#374 := [and-elim #370]: #221
+#373 := [and-elim #370]: #215
+#504 := (+ #96 #134)
+#514 := (<= #504 0::real)
+#635 := (not #514)
+#456 := -1/3::real
+#457 := (* -1/3::real uf_3)
+#544 := (+ #457 #111)
+#545 := (+ uf_2 #544)
+#546 := (>= #545 0::real)
+#390 := (+ #216 uf_9)
+#593 := (+ uf_3 #390)
+#603 := (<= #593 0::real)
+#381 := (+ uf_8 #206)
+#404 := (>= #381 0::real)
+#594 := (+ uf_3 #381)
+#604 := (<= #594 0::real)
+#736 := (not #604)
+#477 := (+ #96 #155)
+#487 := (<= #477 0::real)
+#733 := [hypothesis]: #604
+#564 := (+ #76 #96)
+#565 := (+ uf_1 #564)
+#577 := (<= #565 0::real)
+#767 := (or #577 #736)
+#658 := (not #577)
+#673 := [hypothesis]: #658
+#478 := (+ #96 #145)
+#488 := (<= #478 0::real)
+#628 := (not #488)
+#446 := (+ #96 #123)
+#447 := (+ uf_2 #446)
+#461 := (<= #447 0::real)
+#618 := (not #461)
+#754 := (or #224 #736)
+#625 := (not #487)
+#718 := [hypothesis]: #225
+#744 := (or #577 #736 #224)
+#681 := (or #224 #618)
+#458 := (+ #457 #123)
+#459 := (+ uf_2 #458)
+#460 := (>= #459 0::real)
+#462 := (ite #224 #460 #461)
+#467 := (not #462)
+#468 := (iff #242 #467)
+#465 := (iff #241 #462)
+#444 := (+ #96 uf_6)
+#445 := (+ #76 #444)
+#448 := (ite #224 #445 #447)
+#453 := (<= #448 0::real)
+#463 := (iff #453 #462)
+#464 := [rewrite]: #463
+#454 := (iff #241 #453)
+#451 := (= #240 #448)
+#439 := (ite #224 #175 #166)
+#441 := (+ #96 #439)
+#449 := (= #441 #448)
+#450 := [rewrite]: #449
+#442 := (= #240 #441)
+#437 := (= #239 #439)
+#440 := [rewrite]: #437
+#443 := [monotonicity #440]: #442
+#452 := [trans #443 #450]: #451
+#455 := [monotonicity #452]: #454
+#466 := [trans #455 #464]: #465
+#469 := [monotonicity #466]: #468
+#375 := [and-elim #370]: #242
+#470 := [mp #375 #469]: #467
+#619 := (or #462 #224 #618)
+#620 := [def-axiom]: #619
+#682 := [unit-resolution #620 #470]: #681
+#719 := [unit-resolution #682 #718]: #618
+#737 := (or #487 #461 #736 #577)
+#372 := [and-elim #370]: #211
+#734 := [hypothesis]: #625
+#675 := [hypothesis]: #618
+#735 := [th-lemma #675 #374 #734 #372 #733 #673]: false
+#738 := [lemma #735]: #737
+#739 := [unit-resolution #738 #673 #733 #719]: #487
+#740 := (or #248 #625)
+#489 := (ite #247 #487 #488)
+#494 := (not #489)
+#495 := (iff #265 #494)
+#492 := (iff #264 #489)
+#479 := (ite #247 #477 #478)
+#484 := (<= #479 0::real)
+#490 := (iff #484 #489)
+#491 := [rewrite]: #490
+#485 := (iff #264 #484)
+#482 := (= #263 #479)
+#471 := (ite #247 #155 #145)
+#474 := (+ #96 #471)
+#480 := (= #474 #479)
+#481 := [rewrite]: #480
+#475 := (= #263 #474)
+#472 := (= #262 #471)
+#473 := [rewrite]: #472
+#476 := [monotonicity #473]: #475
+#483 := [trans #476 #481]: #482
+#486 := [monotonicity #483]: #485
+#493 := [trans #486 #491]: #492
+#496 := [monotonicity #493]: #495
+#376 := [and-elim #370]: #265
+#497 := [mp #376 #496]: #494
+#626 := (or #489 #248 #625)
+#627 := [def-axiom]: #626
+#741 := [unit-resolution #627 #497]: #740
+#742 := [unit-resolution #741 #739]: #248
+#743 := [th-lemma #673 #719 #372 #733 #742 #718 #374]: false
+#745 := [lemma #743]: #744
+#746 := [unit-resolution #745 #718 #733]: #577
+#727 := (or #316 #658)
+#574 := (+ #76 #457)
+#575 := (+ uf_1 #574)
+#576 := (>= #575 0::real)
+#578 := (ite #316 #576 #577)
+#583 := (not #578)
+#584 := (iff #334 #583)
+#581 := (iff #333 #578)
+#562 := (+ uf_2 #96)
+#563 := (+ #86 #562)
+#566 := (ite #316 #563 #565)
+#571 := (<= #566 0::real)
+#579 := (iff #571 #578)
+#580 := [rewrite]: #579
+#572 := (iff #333 #571)
+#569 := (= #332 #566)
+#556 := (ite #316 #87 #77)
+#559 := (+ #96 #556)
+#567 := (= #559 #566)
+#568 := [rewrite]: #567
+#560 := (= #332 #559)
+#557 := (= #331 #556)
+#558 := [rewrite]: #557
+#561 := [monotonicity #558]: #560
+#570 := [trans #561 #568]: #569
+#573 := [monotonicity #570]: #572
+#582 := [trans #573 #580]: #581
+#585 := [monotonicity #582]: #584
+#379 := [and-elim #370]: #334
+#586 := [mp #379 #585]: #583
+#659 := (or #578 #316 #658)
+#660 := [def-axiom]: #659
+#728 := [unit-resolution #660 #586]: #727
+#747 := [unit-resolution #728 #746]: #316
+#748 := (not #211)
+#710 := (not #221)
+#749 := (or #247 #461 #710 #748 #736 #224 #317)
+#750 := [th-lemma]: #749
+#751 := [unit-resolution #750 #718 #374 #719 #372 #747 #733]: #247
+#752 := [unit-resolution #741 #751]: #625
+#753 := [th-lemma #719 #372 #733 #718 #747 #752 #374]: false
+#755 := [lemma #753]: #754
+#756 := [unit-resolution #755 #733]: #224
+#615 := (not #460)
+#757 := (or #225 #615)
+#616 := (or #462 #225 #615)
+#617 := [def-axiom]: #616
+#758 := [unit-resolution #617 #470]: #757
+#759 := [unit-resolution #758 #756]: #615
+#760 := (or #618 #460 #225)
+#761 := [th-lemma]: #760
+#762 := [unit-resolution #761 #759 #756]: #618
+#763 := [unit-resolution #738 #673 #733 #762]: #487
+#764 := [unit-resolution #741 #763]: #248
+#701 := (or #247 #628)
+#629 := (or #489 #247 #628)
+#630 := [def-axiom]: #629
+#702 := [unit-resolution #630 #497]: #701
+#765 := [unit-resolution #702 #764]: #628
+#766 := [th-lemma #756 #374 #372 #733 #764 #765 #673]: false
+#768 := [lemma #766]: #767
+#769 := [unit-resolution #768 #733]: #577
+#770 := [unit-resolution #728 #769]: #316
+#771 := (or #487 #710 #748 #736 #225 #317 #460)
+#772 := [th-lemma]: #771
+#773 := [unit-resolution #772 #756 #374 #759 #372 #770 #733]: #487
+#774 := (or #247 #460 #225 #710 #748 #736 #317)
+#775 := [th-lemma]: #774
+#776 := [unit-resolution #775 #756 #374 #759 #372 #770 #733]: #247
+#777 := [unit-resolution #741 #776 #773]: false
+#778 := [lemma #777]: #736
+#668 := (or #404 #604)
+#605 := (ite #404 #603 #604)
+#411 := (ite #404 #381 #390)
+#419 := (* -1::real #411)
+#420 := (+ uf_3 #419)
+#421 := (<= #420 0::real)
+#608 := (iff #421 #605)
+#595 := (ite #404 #593 #594)
+#600 := (<= #595 0::real)
+#606 := (iff #600 #605)
+#607 := [rewrite]: #606
+#601 := (iff #421 #600)
+#598 := (= #420 #595)
+#587 := (ite #404 #390 #381)
+#590 := (+ uf_3 #587)
+#596 := (= #590 #595)
+#597 := [rewrite]: #596
+#591 := (= #420 #590)
+#588 := (= #419 #587)
+#589 := [rewrite]: #588
+#592 := [monotonicity #589]: #591
+#599 := [trans #592 #597]: #598
+#602 := [monotonicity #599]: #601
+#609 := [trans #602 #607]: #608
+#53 := (- uf_8 uf_9)
+#55 := (- #53)
+#54 := (< #53 0::real)
+#56 := (ite #54 #55 #53)
+#57 := (< #56 uf_3)
+#58 := (not #57)
+#434 := (iff #58 #421)
+#384 := (< #381 0::real)
+#395 := (ite #384 #390 #381)
+#398 := (< #395 uf_3)
+#401 := (not #398)
+#432 := (iff #401 #421)
+#422 := (not #421)
+#427 := (not #422)
+#430 := (iff #427 #421)
+#431 := [rewrite]: #430
+#428 := (iff #401 #427)
+#425 := (iff #398 #422)
+#416 := (< #411 uf_3)
+#423 := (iff #416 #422)
+#424 := [rewrite]: #423
+#417 := (iff #398 #416)
+#414 := (= #395 #411)
+#405 := (not #404)
+#408 := (ite #405 #390 #381)
+#412 := (= #408 #411)
+#413 := [rewrite]: #412
+#409 := (= #395 #408)
+#406 := (iff #384 #405)
+#407 := [rewrite]: #406
+#410 := [monotonicity #407]: #409
+#415 := [trans #410 #413]: #414
+#418 := [monotonicity #415]: #417
+#426 := [trans #418 #424]: #425
+#429 := [monotonicity #426]: #428
+#433 := [trans #429 #431]: #432
+#402 := (iff #58 #401)
+#399 := (iff #57 #398)
+#396 := (= #56 #395)
+#382 := (= #53 #381)
+#383 := [rewrite]: #382
+#393 := (= #55 #390)
+#387 := (- #381)
+#391 := (= #387 #390)
+#392 := [rewrite]: #391
+#388 := (= #55 #387)
+#389 := [monotonicity #383]: #388
+#394 := [trans #389 #392]: #393
+#385 := (iff #54 #384)
+#386 := [monotonicity #383]: #385
+#397 := [monotonicity #386 #394 #383]: #396
+#400 := [monotonicity #397]: #399
+#403 := [monotonicity #400]: #402
+#435 := [trans #403 #433]: #434
+#380 := [asserted]: #58
+#436 := [mp #380 #435]: #421
+#610 := [mp #436 #609]: #605
+#661 := (not #605)
+#666 := (or #404 #604 #661)
+#667 := [def-axiom]: #666
+#669 := [unit-resolution #667 #610]: #668
+#700 := [unit-resolution #669 #778]: #404
+#664 := (or #405 #603)
+#662 := (or #405 #603 #661)
+#663 := [def-axiom]: #662
+#665 := [unit-resolution #663 #610]: #664
+#703 := [unit-resolution #665 #700]: #603
+#677 := (not #603)
+#731 := (or #677 #546)
+#648 := (not #546)
+#672 := [hypothesis]: #648
+#671 := [hypothesis]: #603
+#723 := (or #224 #677 #546)
+#689 := (or #461 #546 #677 #514)
+#687 := [hypothesis]: #635
+#371 := [and-elim #370]: #208
+#688 := [th-lemma #373 #672 #371 #671 #675 #687]: false
+#690 := [lemma #688]: #689
+#720 := [unit-resolution #690 #719 #671 #672]: #514
+#692 := (or #271 #635)
+#505 := (+ #96 #124)
+#515 := (<= #505 0::real)
+#516 := (ite #270 #514 #515)
+#521 := (not #516)
+#522 := (iff #288 #521)
+#519 := (iff #287 #516)
+#506 := (ite #270 #504 #505)
+#511 := (<= #506 0::real)
+#517 := (iff #511 #516)
+#518 := [rewrite]: #517
+#512 := (iff #287 #511)
+#509 := (= #286 #506)
+#498 := (ite #270 #134 #124)
+#501 := (+ #96 #498)
+#507 := (= #501 #506)
+#508 := [rewrite]: #507
+#502 := (= #286 #501)
+#499 := (= #285 #498)
+#500 := [rewrite]: #499
+#503 := [monotonicity #500]: #502
+#510 := [trans #503 #508]: #509
+#513 := [monotonicity #510]: #512
+#520 := [trans #513 #518]: #519
+#523 := [monotonicity #520]: #522
+#377 := [and-elim #370]: #288
+#524 := [mp #377 #523]: #521
+#636 := (or #516 #271 #635)
+#637 := [def-axiom]: #636
+#693 := [unit-resolution #637 #524]: #692
+#721 := [unit-resolution #693 #720]: #271
+#722 := [th-lemma #719 #373 #371 #671 #721 #718 #672]: false
+#724 := [lemma #722]: #723
+#725 := [unit-resolution #724 #671 #672]: #224
+#716 := (or #225 #317 #546 #677)
+#704 := [hypothesis]: #224
+#708 := [hypothesis]: #316
+#709 := (not #215)
+#711 := (or #270 #709 #317 #225 #710)
+#712 := [th-lemma]: #711
+#713 := [unit-resolution #712 #704 #374 #373 #708]: #270
+#714 := [unit-resolution #693 #713]: #635
+#715 := [th-lemma #708 #672 #371 #671 #714 #373 #704 #374]: false
+#717 := [lemma #715]: #716
+#726 := [unit-resolution #717 #725 #672 #671]: #317
+#729 := [unit-resolution #728 #726]: #658
+#698 := (or #316 #546 #677 #577)
+#674 := [hypothesis]: #317
+#685 := (or #270 #316 #577 #546 #677)
+#670 := [hypothesis]: #271
+#678 := (or #461 #316 #577 #546 #677 #270)
+#676 := [th-lemma #675 #674 #673 #672 #371 #671 #670 #373]: false
+#679 := [lemma #676]: #678
+#680 := [unit-resolution #679 #670 #673 #672 #671 #674]: #461
+#683 := [unit-resolution #682 #680]: #224
+#684 := [th-lemma #674 #673 #672 #371 #671 #670 #683 #373]: false
+#686 := [lemma #684]: #685
+#691 := [unit-resolution #686 #674 #673 #672 #671]: #270
+#694 := [unit-resolution #693 #691]: #635
+#695 := [unit-resolution #690 #694 #671 #672]: #461
+#696 := [unit-resolution #682 #695]: #224
+#697 := [th-lemma #373 #672 #371 #671 #696 #674 #673 #694]: false
+#699 := [lemma #697]: #698
+#730 := [unit-resolution #699 #729 #726 #671 #672]: false
+#732 := [lemma #730]: #731
+#705 := [unit-resolution #732 #703]: #546
+#706 := (or #293 #648)
+#531 := (+ #96 #111)
+#532 := (+ uf_2 #531)
+#543 := (<= #532 0::real)
+#547 := (ite #293 #543 #546)
+#552 := (not #547)
+#553 := (iff #311 #552)
+#550 := (iff #310 #547)
+#533 := (+ #96 uf_4)
+#534 := (+ #76 #533)
+#535 := (ite #293 #532 #534)
+#540 := (<= #535 0::real)
+#548 := (iff #540 #547)
+#549 := [rewrite]: #548
+#541 := (iff #310 #540)
+#538 := (= #309 #535)
+#525 := (ite #293 #112 #102)
+#528 := (+ #96 #525)
+#536 := (= #528 #535)
+#537 := [rewrite]: #536
+#529 := (= #309 #528)
+#526 := (= #308 #525)
+#527 := [rewrite]: #526
+#530 := [monotonicity #527]: #529
+#539 := [trans #530 #537]: #538
+#542 := [monotonicity #539]: #541
+#551 := [trans #542 #549]: #550
+#554 := [monotonicity #551]: #553
+#378 := [and-elim #370]: #311
+#555 := [mp #378 #554]: #552
+#649 := (or #547 #293 #648)
+#650 := [def-axiom]: #649
+#707 := [unit-resolution #650 #555]: #706
+#779 := [unit-resolution #707 #705]: #293
+#783 := (or #224 #270 #461)
+#780 := (not #208)
+#781 := (or #294 #709 #224 #780 #677 #270 #461)
+#782 := [th-lemma]: #781
+#784 := [unit-resolution #782 #373 #703 #779 #371]: #783
+#785 := [unit-resolution #784 #719 #718]: #270
+#786 := [unit-resolution #693 #785]: #635
+#787 := [th-lemma #718 #719 #786 #373 #371 #703 #779]: false
+#788 := [lemma #787]: #224
+#798 := (or #270 #317 #225)
+#799 := [unit-resolution #712 #374 #373]: #798
+#800 := [unit-resolution #799 #708 #788]: #270
+#801 := [unit-resolution #693 #800]: #635
+#802 := [th-lemma #708 #779 #371 #703 #788 #801 #373 #374]: false
+#803 := [lemma #802]: #317
+#804 := [unit-resolution #728 #803]: #658
+#796 := (or #316 #577)
+#789 := (or #514 #294 #225 #709 #780 #677 #577 #316)
+#790 := [th-lemma]: #789
+#791 := [unit-resolution #790 #674 #788 #371 #779 #373 #673 #703]: #514
+#792 := (or #270 #577 #316 #294 #225 #709 #780 #677)
+#793 := [th-lemma]: #792
+#794 := [unit-resolution #793 #674 #788 #371 #779 #373 #673 #703]: #270
+#795 := [unit-resolution #693 #794 #791]: false
+#797 := [lemma #795]: #796
+[unit-resolution #797 #804 #803]: false
+unsat
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 21 14:02:34 2010 +0200
@@ -11,6 +11,8 @@
 declare [[smt_fixed=true]]
 declare [[z3_proofs=true]]
 
+subsection {* Sundries *}
+
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
 lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
 lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
@@ -18,6 +20,81 @@
 
 declare smult_conv_scaleR[simp]
 
+lemma simple_image: "{f x |x . x \<in> s} = f ` s" by blast
+
+lemma linear_simps:  assumes "bounded_linear f"
+  shows "f (a + b) = f a + f b" "f (a - b) = f a - f b" "f 0 = 0" "f (- a) = - f a" "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
+  apply(rule_tac[!] additive.add additive.minus additive.diff additive.zero bounded_linear.scaleR)
+  using assms unfolding bounded_linear_def additive_def by auto
+
+lemma bounded_linearI:assumes "\<And>x y. f (x + y) = f x + f y"
+  "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x" "\<And>x. norm (f x) \<le> norm x * K"
+  shows "bounded_linear f"
+  unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto
+ 
+lemma real_le_inf_subset:
+  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s" shows "Inf s <= Inf (t::real set)"
+  apply(rule isGlb_le_isLb) apply(rule Inf[OF assms(1)])
+  using assms apply-apply(erule exE) apply(rule_tac x=b in exI)
+  unfolding isLb_def setge_def by auto
+
+lemma real_ge_sup_subset:
+  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. s *<= b" shows "Sup s >= Sup (t::real set)"
+  apply(rule isLub_le_isUb) apply(rule Sup[OF assms(1)])
+  using assms apply-apply(erule exE) apply(rule_tac x=b in exI)
+  unfolding isUb_def setle_def by auto
+
+lemma dist_trans[simp]:"dist (vec1 x) (vec1 y) = dist x (y::real)"
+  unfolding dist_real_def dist_vec1 ..
+
+lemma Lim_trans[simp]: fixes f::"'a \<Rightarrow> real"
+  shows "((\<lambda>x. vec1 (f x)) ---> vec1 l) net \<longleftrightarrow> (f ---> l) net"
+  using assms unfolding Lim dist_trans ..
+
+lemma bounded_linear_component[intro]: "bounded_linear (\<lambda>x::real^'n. x $ k)"
+  apply(rule bounded_linearI[where K=1]) 
+  using component_le_norm[of _ k] unfolding real_norm_def by auto
+
+lemma bounded_vec1[intro]:  "bounded s \<Longrightarrow> bounded (vec1 ` (s::real set))"
+  unfolding bounded_def apply safe apply(rule_tac x="vec1 x" in exI,rule_tac x=e in exI) by auto
+
+lemma transitive_stepwise_lt_eq:
+  assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
+  shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))" (is "?l = ?r")
+proof(safe) assume ?r fix n m::nat assume "m < n" thus "R m n" apply-
+  proof(induct n arbitrary: m) case (Suc n) show ?case 
+    proof(cases "m < n") case True
+      show ?thesis apply(rule assms[OF Suc(1)[OF True]]) using `?r` by auto
+    next case False hence "m = n" using Suc(2) by auto
+      thus ?thesis using `?r` by auto
+    qed qed auto qed auto
+
+lemma transitive_stepwise_gt:
+  assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) "
+  shows "\<forall>n>m. R m n"
+proof- have "\<forall>m. \<forall>n>m. R m n" apply(subst transitive_stepwise_lt_eq)
+    apply(rule assms) apply(assumption,assumption) using assms(2) by auto
+  thus ?thesis by auto qed
+
+lemma transitive_stepwise_le_eq:
+  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
+  shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))" (is "?l = ?r")
+proof safe assume ?r fix m n::nat assume "m\<le>n" thus "R m n" apply-
+  proof(induct n arbitrary: m) case (Suc n) show ?case 
+    proof(cases "m \<le> n") case True show ?thesis apply(rule assms(2))
+        apply(rule Suc(1)[OF True]) using `?r` by auto
+    next case False hence "m = Suc n" using Suc(2) by auto
+      thus ?thesis using assms(1) by auto
+    qed qed(insert assms(1), auto) qed auto
+
+lemma transitive_stepwise_le:
+  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) "
+  shows "\<forall>n\<ge>m. R m n"
+proof- have "\<forall>m. \<forall>n\<ge>m. R m n" apply(subst transitive_stepwise_le_eq)
+    apply(rule assms) apply(rule assms,assumption,assumption) using assms(3) by auto
+  thus ?thesis by auto qed
+
+
 subsection {* Some useful lemmas about intervals. *}
 
 lemma empty_as_interval: "{} = {1..0::real^'n}"
@@ -1246,6 +1323,10 @@
   apply(drule has_integral_linear,assumption,assumption) unfolding has_integral_integral[THEN sym]
   apply(rule integrable_linear) by assumption+
 
+lemma integral_component_eq[simp]: fixes f::"real^'n \<Rightarrow> real^'m"
+  assumes "f integrable_on s" shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
+  using integral_linear[OF assms(1) bounded_linear_component,unfolded o_def] .
+
 lemma has_integral_setsum:
   assumes "finite t" "\<forall>a\<in>t. ((f a) has_integral (i a)) s"
   shows "((\<lambda>x. setsum (\<lambda>a. f a x) t) has_integral (setsum i t)) s"
@@ -2225,22 +2306,22 @@
   shows "dest_vec1(integral s f) \<le> dest_vec1(integral s g)"
   apply(rule has_integral_dest_vec1_le) apply(rule_tac[1-2] integrable_integral) using assms by auto
 
-lemma has_integral_component_pos: fixes f::"real^'n \<Rightarrow> real^'m"
+lemma has_integral_component_nonneg: fixes f::"real^'n \<Rightarrow> real^'m"
   assumes "(f has_integral i) s" "\<forall>x\<in>s. 0 \<le> (f x)$k" shows "0 \<le> i$k"
   using has_integral_component_le[OF has_integral_0 assms(1)] using assms(2) by auto
 
-lemma integral_component_pos: fixes f::"real^'n \<Rightarrow> real^'m"
+lemma integral_component_nonneg: fixes f::"real^'n \<Rightarrow> real^'m"
   assumes "f integrable_on s" "\<forall>x\<in>s. 0 \<le> (f x)$k" shows "0 \<le> (integral s f)$k"
-  apply(rule has_integral_component_pos) using assms by auto
-
-lemma has_integral_dest_vec1_pos: fixes f::"real^'n \<Rightarrow> real^1"
+  apply(rule has_integral_component_nonneg) using assms by auto
+
+lemma has_integral_dest_vec1_nonneg: fixes f::"real^'n \<Rightarrow> real^1"
   assumes "(f has_integral i) s" "\<forall>x\<in>s. 0 \<le> f x" shows "0 \<le> i"
-  using has_integral_component_pos[OF assms(1), of 1]
+  using has_integral_component_nonneg[OF assms(1), of 1]
   using assms(2) unfolding vector_le_def by auto
 
-lemma integral_dest_vec1_pos: fixes f::"real^'n \<Rightarrow> real^1"
+lemma integral_dest_vec1_nonneg: fixes f::"real^'n \<Rightarrow> real^1"
   assumes "f integrable_on s" "\<forall>x\<in>s. 0 \<le> f x" shows "0 \<le> integral s f"
-  apply(rule has_integral_dest_vec1_pos) using assms by auto
+  apply(rule has_integral_dest_vec1_nonneg) using assms by auto
 
 lemma has_integral_component_neg: fixes f::"real^'n \<Rightarrow> real^'m"
   assumes "(f has_integral i) s" "\<forall>x\<in>s. (f x)$k \<le> 0" shows "i$k \<le> 0"
@@ -3779,6 +3860,57 @@
       thus False by auto qed
     thus ?l using y unfolding s by auto qed qed 
 
+lemma has_integral_trans[simp]: fixes f::"real^'n \<Rightarrow> real" shows
+  "((\<lambda>x. vec1 (f x)) has_integral vec1 i) s \<longleftrightarrow> (f has_integral i) s"
+  unfolding has_integral'[unfolded has_integral] 
+proof case goal1 thus ?case apply safe
+  apply(erule_tac x=e in allE,safe) apply(rule_tac x=B in exI,safe)
+  apply(erule_tac x=a in allE, erule_tac x=b in allE,safe) 
+  apply(rule_tac x="dest_vec1 z" in exI,safe) apply(erule_tac x=ea in allE,safe) 
+  apply(rule_tac x=d in exI,safe) apply(erule_tac x=p in allE,safe)
+  apply(subst(asm)(2) norm_vector_1) unfolding split_def
+  unfolding setsum_component Cart_nth.diff cond_value_iff[of dest_vec1]
+    Cart_nth.scaleR vec1_dest_vec1 zero_index apply assumption
+  apply(subst(asm)(2) norm_vector_1) by auto
+next case goal2 thus ?case apply safe
+  apply(erule_tac x=e in allE,safe) apply(rule_tac x=B in exI,safe)
+  apply(erule_tac x=a in allE, erule_tac x=b in allE,safe) 
+  apply(rule_tac x="vec1 z" in exI,safe) apply(erule_tac x=ea in allE,safe) 
+  apply(rule_tac x=d in exI,safe) apply(erule_tac x=p in allE,safe)
+  apply(subst norm_vector_1) unfolding split_def
+  unfolding setsum_component Cart_nth.diff cond_value_iff[of dest_vec1]
+    Cart_nth.scaleR vec1_dest_vec1 zero_index apply assumption
+  apply(subst norm_vector_1) by auto qed
+
+lemma integral_trans[simp]: assumes "(f::real^'n \<Rightarrow> real) integrable_on s"
+  shows "integral s (\<lambda>x. vec1 (f x)) = vec1 (integral s f)"
+  apply(rule integral_unique) using assms by auto
+
+lemma integrable_on_trans[simp]: fixes f::"real^'n \<Rightarrow> real" shows
+  "(\<lambda>x. vec1 (f x)) integrable_on s \<longleftrightarrow> (f integrable_on s)"
+  unfolding integrable_on_def
+  apply(subst(2) vec1_dest_vec1(1)[THEN sym]) unfolding has_integral_trans
+  apply safe defer apply(rule_tac x="vec1 y" in exI) by auto
+
+lemma has_integral_le: fixes f::"real^'n \<Rightarrow> real"
+  assumes "(f has_integral i) s" "(g has_integral j) s"  "\<forall>x\<in>s. (f x) \<le> (g x)"
+  shows "i \<le> j" using has_integral_component_le[of "vec1 o f" "vec1 i" s "vec1 o g" "vec1 j" 1]
+  unfolding o_def using assms by auto 
+
+lemma integral_le: fixes f::"real^'n \<Rightarrow> real"
+  assumes "f integrable_on s" "g integrable_on s" "\<forall>x\<in>s. f x \<le> g x"
+  shows "integral s f \<le> integral s g"
+  using has_integral_le[OF assms(1,2)[unfolded has_integral_integral] assms(3)] .
+
+lemma has_integral_nonneg: fixes f::"real^'n \<Rightarrow> real"
+  assumes "(f has_integral i) s" "\<forall>x\<in>s. 0 \<le> f x" shows "0 \<le> i" 
+  using has_integral_component_nonneg[of "vec1 o f" "vec1 i" s 1]
+  unfolding o_def using assms by auto
+
+lemma integral_nonneg: fixes f::"real^'n \<Rightarrow> real"
+  assumes "f integrable_on s" "\<forall>x\<in>s. 0 \<le> f x" shows "0 \<le> integral s f" 
+  using has_integral_nonneg[OF assms(1)[unfolded has_integral_integral] assms(2)] .
+
 subsection {* Hence a general restriction property. *}
 
 lemma has_integral_restrict[simp]: assumes "s \<subseteq> t" shows
@@ -3875,11 +4007,21 @@
   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 has_integral_subset_le: fixes f::"real^'n \<Rightarrow> real"
+  assumes "s \<subseteq> t" "(f has_integral i) s" "(f has_integral j) t" "\<forall>x\<in>t. 0 \<le> f(x)"
+  shows "i \<le> j" using has_integral_subset_component_le[OF assms(1), of "vec1 o f" "vec1 i" "vec1 j" 1]
+  unfolding o_def using assms by auto
+
 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 integral_subset_le: fixes f::"real^'n \<Rightarrow> real"
+  assumes "s \<subseteq> t" "f integrable_on s" "f integrable_on t" "\<forall>x \<in> t. 0 \<le> f(x)"
+  shows "(integral s f) \<le> (integral t f)"
+  apply(rule has_integral_subset_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")
@@ -3909,7 +4051,1480 @@
       from integral_unique[OF this(1)] show ?case using z(2) by auto qed qed qed 
 
 
+subsection {* Continuity of the integral (for a 1-dimensional interval). *}
+
+lemma integrable_alt: fixes f::"real^'n \<Rightarrow> 'a::banach" shows 
+  "f integrable_on 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 c d. ball 0 B \<subseteq> {a..b} \<and> ball 0 B \<subseteq> {c..d}
+  \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) -
+          integral {c..d}  (\<lambda>x. if x \<in> s then f x else 0)) < e)" (is "?l = ?r")
+proof assume ?l then guess y unfolding integrable_on_def .. note this[unfolded has_integral_alt'[of f]]
+  note y=conjunctD2[OF this,rule_format] show ?r apply safe apply(rule y)
+  proof- case goal1 hence "e/2 > 0" by auto from y(2)[OF this] guess B .. note B=conjunctD2[OF this,rule_format]
+    show ?case apply(rule,rule,rule B)
+    proof safe case goal1 show ?case apply(rule norm_triangle_half_l)
+        using B(2)[OF goal1(1)] B(2)[OF goal1(2)] by auto qed qed
+        
+next assume ?r note as = conjunctD2[OF this,rule_format]
+  have "Cauchy (\<lambda>n. integral ({(\<chi> i. - real n) .. (\<chi> i. real n)}) (\<lambda>x. if x \<in> s then f x else 0))"
+  proof(unfold Cauchy_def,safe) case goal1
+    from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format]
+    from real_arch_simple[of B] guess N .. note N = this
+    { fix n assume n:"n \<ge> N" have "ball 0 B \<subseteq> {\<chi> i. - real n..\<chi> i. real n}" apply safe
+        unfolding mem_ball mem_interval vector_dist_norm
+      proof case goal1 thus ?case using component_le_norm[of x i]
+          using n N by(auto simp add:field_simps) qed }
+    thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding vector_dist_norm apply(rule B(2)) by auto
+  qed from this[unfolded convergent_eq_cauchy[THEN sym]] guess i ..
+  note i = this[unfolded Lim_sequentially, rule_format]
+
+  show ?l unfolding integrable_on_def has_integral_alt'[of f] apply(rule_tac x=i in exI)
+    apply safe apply(rule as(1)[unfolded integrable_on_def])
+  proof- case goal1 hence *:"e/2 > 0" by auto
+    from i[OF this] guess N .. note N =this[rule_format]
+    from as(2)[OF *] guess B .. note B=conjunctD2[OF this,rule_format] let ?B = "max (real N) B"
+    show ?case apply(rule_tac x="?B" in exI)
+    proof safe show "0 < ?B" using B(1) by auto
+      fix a b assume ab:"ball 0 ?B \<subseteq> {a..b::real^'n}"
+      from real_arch_simple[of ?B] guess n .. note n=this
+      show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
+        apply(rule norm_triangle_half_l) apply(rule B(2)) defer apply(subst norm_minus_commute)
+        apply(rule N[unfolded vector_dist_norm, of n])
+      proof safe show "N \<le> n" using n by auto
+        fix x::"real^'n" assume x:"x \<in> ball 0 B" hence "x\<in> ball 0 ?B" by auto
+        thus "x\<in>{a..b}" using ab by blast 
+        show "x\<in>{\<chi> i. - real n..\<chi> i. real n}" using x unfolding mem_interval mem_ball vector_dist_norm apply-
+        proof case goal1 thus ?case using component_le_norm[of x i]
+            using n by(auto simp add:field_simps) qed qed qed qed qed
+
+lemma integrable_altD: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f integrable_on s"
+  shows "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}"
+  "\<And>e. e>0 \<Longrightarrow> \<exists>B>0. \<forall>a b c d. ball 0 B \<subseteq> {a..b} \<and> ball 0 B \<subseteq> {c..d}
+  \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d}  (\<lambda>x. if x \<in> s then f x else 0)) < e"
+  using assms[unfolded integrable_alt[of f]] by auto
+
+lemma integrable_on_subinterval: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f integrable_on s" "{a..b} \<subseteq> s" shows "f integrable_on {a..b}"
+  apply(rule integrable_eq) defer apply(rule integrable_altD(1)[OF assms(1)])
+  using assms(2) by auto
+
+subsection {* A straddling criterion for integrability. *}
+
+lemma integrable_straddle_interval: fixes f::"real^'n \<Rightarrow> real"
+  assumes "\<forall>e>0. \<exists>g  h i j. (g has_integral i) ({a..b}) \<and> (h has_integral j) ({a..b}) \<and>
+  norm(i - j) < e \<and> (\<forall>x\<in>{a..b}. (g x) \<le> (f x) \<and> (f x) \<le>(h x))"
+  shows "f integrable_on {a..b}"
+proof(subst integrable_cauchy,safe)
+  case goal1 hence e:"e/3 > 0" by auto note assms[rule_format,OF this]
+  then guess g h i j apply- by(erule exE conjE)+ note obt = this
+  from obt(1)[unfolded has_integral[of g], rule_format, OF e] guess d1 .. note d1=conjunctD2[OF this,rule_format]
+  from obt(2)[unfolded has_integral[of h], rule_format, OF e] guess d2 .. note d2=conjunctD2[OF this,rule_format]
+  show ?case apply(rule_tac x="\<lambda>x. d1 x \<inter> d2 x" in exI) apply(rule conjI gauge_inter d1 d2)+ unfolding fine_inter
+  proof safe have **:"\<And>i j g1 g2 h1 h2 f1 f2. g1 - h2 \<le> f1 - f2 \<Longrightarrow> f1 - f2 \<le> h1 - g2 \<Longrightarrow>
+      abs(i - j) < e / 3 \<Longrightarrow> abs(g2 - i) < e / 3 \<Longrightarrow>  abs(g1 - i) < e / 3 \<Longrightarrow> 
+      abs(h2 - j) < e / 3 \<Longrightarrow> abs(h1 - j) < e / 3 \<Longrightarrow> abs(f1 - f2) < e" using `e>0` by arith
+    case goal1 note tagged_division_ofD(2-4) note * = this[OF goal1(1)] this[OF goal1(4)]
+
+    have "(\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R g x) \<ge> 0"
+      "0 \<le> (\<Sum>(x, k)\<in>p2. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)" 
+      "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0"
+      "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)" 
+      unfolding setsum_subtractf[THEN sym] apply- apply(rule_tac[!] setsum_nonneg)
+      apply safe unfolding real_scaleR_def mult.diff_right[THEN sym]
+      apply(rule_tac[!] mult_nonneg_nonneg)
+    proof- fix a b assume ab:"(a,b) \<in> p1"
+      show "0 \<le> content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
+      show "0 \<le> f a - g a" "0 \<le> h a - f a" using *(1-2)[OF ab] using obt(4)[rule_format,of a] by auto
+    next fix a b assume ab:"(a,b) \<in> p2"
+      show "0 \<le> content b" using *(6)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
+      show "0 \<le> f a - g a" "0 \<le> h a - f a" using *(4-5)[OF ab] using obt(4)[rule_format,of a] by auto qed 
+
+    thus ?case apply- unfolding real_norm_def apply(rule **) defer defer
+      unfolding real_norm_def[THEN sym] apply(rule obt(3))
+      apply(rule d1(2)[OF conjI[OF goal1(4,5)]])
+      apply(rule d1(2)[OF conjI[OF goal1(1,2)]])
+      apply(rule d2(2)[OF conjI[OF goal1(4,6)]])
+      apply(rule d2(2)[OF conjI[OF goal1(1,3)]]) by auto qed qed 
+     
+lemma integrable_straddle: fixes f::"real^'n \<Rightarrow> real"
+  assumes "\<forall>e>0. \<exists>g h i j. (g has_integral i) s \<and> (h has_integral j) s \<and>
+  norm(i - j) < e \<and> (\<forall>x\<in>s. (g x) \<le>(f x) \<and>(f x) \<le>(h x))"
+  shows "f integrable_on s"
+proof- have "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}"
+  proof(rule integrable_straddle_interval,safe) case goal1 hence *:"e/4 > 0" by auto
+    from assms[rule_format,OF this] guess g h i j apply-by(erule exE conjE)+ note obt=this
+    note obt(1)[unfolded has_integral_alt'[of g]] note conjunctD2[OF this, rule_format]
+    note g = this(1) and this(2)[OF *] from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format]
+    note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format]
+    note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format]
+    def c \<equiv> "\<chi> i. min (a$i) (- (max B1 B2))" and d \<equiv> "\<chi> i. max (b$i) (max B1 B2)"
+    have *:"ball 0 B1 \<subseteq> {c..d}" "ball 0 B2 \<subseteq> {c..d}" apply safe unfolding mem_ball mem_interval vector_dist_norm
+    proof(rule_tac[!] allI)
+      case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto next
+      case goal2 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
+    have **:"\<And>ch cg ag ah::real. norm(ah - ag) \<le> norm(ch - cg) \<Longrightarrow> norm(cg - i) < e / 4 \<Longrightarrow>
+      norm(ch - j) < e / 4 \<Longrightarrow> norm(ag - ah) < e"
+      using obt(3) unfolding real_norm_def by arith 
+    show ?case apply(rule_tac x="\<lambda>x. if x \<in> s then g x else 0" in exI)
+               apply(rule_tac x="\<lambda>x. if x \<in> s then h x else 0" in exI)
+      apply(rule_tac x="integral {a..b} (\<lambda>x. if x \<in> s then g x else 0)" in exI)
+      apply(rule_tac x="integral {a..b} (\<lambda>x. if x \<in> s then h x else 0)" in exI)
+      apply safe apply(rule_tac[1-2] integrable_integral,rule g,rule h)
+      apply(rule **[OF _ B1(2)[OF *(1)] B2(2)[OF *(2)]])
+    proof- have *:"\<And>x f g. (if x \<in> s then f x else 0) - (if x \<in> s then g x else 0) =
+        (if x \<in> s then f x - g x else (0::real))" by auto
+      note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_sub, OF h g]]
+      show " norm (integral {a..b} (\<lambda>x. if x \<in> s then h x else 0) -
+                   integral {a..b} (\<lambda>x. if x \<in> s then g x else 0))
+           \<le> norm (integral {c..d} (\<lambda>x. if x \<in> s then h x else 0) -
+                   integral {c..d} (\<lambda>x. if x \<in> s then g x else 0))"
+        unfolding integral_sub[OF h g,THEN sym] real_norm_def apply(subst **) defer apply(subst **) defer
+        apply(rule has_integral_subset_le) defer apply(rule integrable_integral integrable_sub h g)+
+      proof safe fix x assume "x\<in>{a..b}" thus "x\<in>{c..d}" unfolding mem_interval c_def d_def
+          apply - apply rule apply(erule_tac x=i in allE) by auto
+      qed(insert obt(4), auto) qed(insert obt(4), auto) qed note interv = this
+
+  show ?thesis unfolding integrable_alt[of f] apply safe apply(rule interv)
+  proof- case goal1 hence *:"e/3 > 0" by auto
+    from assms[rule_format,OF this] guess g h i j apply-by(erule exE conjE)+ note obt=this
+    note obt(1)[unfolded has_integral_alt'[of g]] note conjunctD2[OF this, rule_format]
+    note g = this(1) and this(2)[OF *] from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format]
+    note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format]
+    note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format]
+    show ?case apply(rule_tac x="max B1 B2" in exI) apply safe apply(rule min_max.less_supI1,rule B1)
+    proof- fix a b c d::"real^'n" assume as:"ball 0 (max B1 B2) \<subseteq> {a..b}" "ball 0 (max B1 B2) \<subseteq> {c..d}"
+      have **:"ball 0 B1 \<subseteq> ball (0::real^'n) (max B1 B2)" "ball 0 B2 \<subseteq> ball (0::real^'n) (max B1 B2)" by auto
+      have *:"\<And>ga gc ha hc fa fc::real. abs(ga - i) < e / 3 \<and> abs(gc - i) < e / 3 \<and> abs(ha - j) < e / 3 \<and>
+        abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e" by smt
+      show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d} (\<lambda>x. if x \<in> s then f x else 0)) < e"
+        unfolding real_norm_def apply(rule *, safe) unfolding real_norm_def[THEN sym]
+        apply(rule B1(2),rule order_trans,rule **,rule as(1)) 
+        apply(rule B1(2),rule order_trans,rule **,rule as(2)) 
+        apply(rule B2(2),rule order_trans,rule **,rule as(1)) 
+        apply(rule B2(2),rule order_trans,rule **,rule as(2)) 
+        apply(rule obt) apply(rule_tac[!] integral_le) using obt
+        by(auto intro!: h g interv) qed qed qed 
+
+subsection {* Adding integrals over several sets. *}
+
+lemma has_integral_union: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "(f has_integral i) s" "(f has_integral j) t" "negligible(s \<inter> t)"
+  shows "(f has_integral (i + j)) (s \<union> t)"
+proof- note * = has_integral_restrict_univ[THEN sym, of f]
+  show ?thesis unfolding * apply(rule has_integral_spike[OF assms(3)])
+    defer apply(rule has_integral_add[OF assms(1-2)[unfolded *]]) by auto qed
+
+lemma has_integral_unions: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "finite t" "\<forall>s\<in>t. (f has_integral (i s)) s"  "\<forall>s\<in>t. \<forall>s'\<in>t. ~(s = s') \<longrightarrow> negligible(s \<inter> s')"
+  shows "(f has_integral (setsum i t)) (\<Union>t)"
+proof- note * = has_integral_restrict_univ[THEN sym, of f]
+  have **:"negligible (\<Union>((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> t \<and> b \<in> {y. y \<in> t \<and> ~(a = y)}}))"
+    apply(rule negligible_unions) apply(rule finite_imageI) apply(rule finite_subset[of _ "t \<times> t"]) defer 
+    apply(rule finite_cartesian_product[OF assms(1,1)]) using assms(3) by auto 
+  note assms(2)[unfolded *] note has_integral_setsum[OF assms(1) this]
+  thus ?thesis unfolding * apply-apply(rule has_integral_spike[OF **]) defer apply assumption
+  proof safe case goal1 thus ?case
+    proof(cases "x\<in>\<Union>t") case True then guess s unfolding Union_iff .. note s=this
+      hence *:"\<forall>b\<in>t. x \<in> b \<longleftrightarrow> b = s" using goal1(3) by blast
+      show ?thesis unfolding if_P[OF True] apply(rule trans) defer
+        apply(rule setsum_cong2) apply(subst *, assumption) apply(rule refl)
+        unfolding setsum_delta[OF assms(1)] using s by auto qed auto qed qed
+
+subsection {* In particular adding integrals over a division, maybe not of an interval. *}
+
+lemma has_integral_combine_division: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "d division_of s" "\<forall>k\<in>d. (f has_integral (i k)) k"
+  shows "(f has_integral (setsum i d)) s"
+proof- note d = division_ofD[OF assms(1)]
+  show ?thesis unfolding d(6)[THEN sym] apply(rule has_integral_unions)
+    apply(rule d assms)+ apply(rule,rule,rule)
+  proof- case goal1 from d(4)[OF this(1)] d(4)[OF this(2)]
+    guess a c b d apply-by(erule exE)+ note obt=this
+    from d(5)[OF goal1] show ?case unfolding obt interior_closed_interval
+      apply-apply(rule negligible_subset[of "({a..b}-{a<..<b}) \<union> ({c..d}-{c<..<d})"])
+      apply(rule negligible_union negligible_frontier_interval)+ by auto qed qed
+
+lemma integral_combine_division_bottomup: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "d division_of s" "\<forall>k\<in>d. f integrable_on k"
+  shows "integral s f = setsum (\<lambda>i. integral i f) d"
+  apply(rule integral_unique) apply(rule has_integral_combine_division[OF assms(1)])
+  using assms(2) unfolding has_integral_integral .
+
+lemma has_integral_combine_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f integrable_on s" "d division_of k" "k \<subseteq> s"
+  shows "(f has_integral (setsum (\<lambda>i. integral i f) d)) k"
+  apply(rule has_integral_combine_division[OF assms(2)])
+  apply safe unfolding has_integral_integral[THEN sym]
+proof- case goal1 from division_ofD(2,4)[OF assms(2) this]
+  show ?case apply safe apply(rule integrable_on_subinterval)
+    apply(rule assms) using assms(3) by auto qed
+
+lemma integral_combine_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f integrable_on s" "d division_of s"
+  shows "integral s f = setsum (\<lambda>i. integral i f) d"
+  apply(rule integral_unique,rule has_integral_combine_division_topdown) using assms by auto
+
+lemma integrable_combine_division: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "d division_of s" "\<forall>i\<in>d. f integrable_on i"
+  shows "f integrable_on s"
+  using assms(2) unfolding integrable_on_def
+  by(metis has_integral_combine_division[OF assms(1)])
+
+lemma integrable_on_subdivision: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "d division_of i" "f integrable_on s" "i \<subseteq> s"
+  shows "f integrable_on i"
+  apply(rule integrable_combine_division assms)+
+proof safe case goal1 note division_ofD(2,4)[OF assms(1) this]
+  thus ?case apply safe apply(rule integrable_on_subinterval[OF assms(2)])
+    using assms(3) by auto qed
+
+subsection {* Also tagged divisions. *}
+
+lemma has_integral_combine_tagged_division: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "p tagged_division_of s" "\<forall>(x,k) \<in> p. (f has_integral (i k)) k"
+  shows "(f has_integral (setsum (\<lambda>(x,k). i k) p)) s"
+proof- have *:"(f has_integral (setsum (\<lambda>k. integral k f) (snd ` p))) s"
+    apply(rule has_integral_combine_division) apply(rule division_of_tagged_division[OF assms(1)])
+    using assms(2) unfolding has_integral_integral[THEN sym] by(safe,auto)
+  thus ?thesis apply- apply(rule subst[where P="\<lambda>i. (f has_integral i) s"]) defer apply assumption
+    apply(rule trans[of _ "setsum (\<lambda>(x,k). integral k f) p"]) apply(subst eq_commute)
+    apply(rule setsum_over_tagged_division_lemma[OF assms(1)]) apply(rule integral_null,assumption)
+    apply(rule setsum_cong2) using assms(2) by auto qed
+
+lemma integral_combine_tagged_division_bottomup: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "p tagged_division_of {a..b}" "\<forall>(x,k)\<in>p. f integrable_on k"
+  shows "integral {a..b} f = setsum (\<lambda>(x,k). integral k f) p"
+  apply(rule integral_unique) apply(rule has_integral_combine_tagged_division[OF assms(1)])
+  using assms(2) by auto
+
+lemma has_integral_combine_tagged_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f integrable_on {a..b}" "p tagged_division_of {a..b}"
+  shows "(f has_integral (setsum (\<lambda>(x,k). integral k f) p)) {a..b}"
+  apply(rule has_integral_combine_tagged_division[OF assms(2)])
+proof safe case goal1 note tagged_division_ofD(3-4)[OF assms(2) this]
+  thus ?case using integrable_subinterval[OF assms(1)] by auto qed
+
+lemma integral_combine_tagged_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f integrable_on {a..b}" "p tagged_division_of {a..b}"
+  shows "integral {a..b} f = setsum (\<lambda>(x,k). integral k f) p"
+  apply(rule integral_unique,rule has_integral_combine_tagged_division_topdown) using assms by auto
+
+subsection {* Henstock's lemma. *}
+
+lemma henstock_lemma_part1: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f integrable_on {a..b}" "0 < e" "gauge d"
+  "(\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral({a..b}) f) < e)"
+  and p:"p tagged_partial_division_of {a..b}" "d fine p"
+  shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e")
+proof-  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by arith }
+  fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)]
+  have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastsimp
+  note partial_division_of_tagged_division[OF p(1)] this
+  from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)]
+  def r \<equiv> "q - snd ` p" have "snd ` p \<inter> r = {}" unfolding r_def by auto
+  have r:"finite r" using q' unfolding r_def by auto
+
+  have "\<forall>i\<in>r. \<exists>p. p tagged_division_of i \<and> d fine p \<and>
+    norm(setsum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
+  proof safe case goal1 hence i:"i \<in> q" unfolding r_def by auto
+    from q'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this
+    have *:"k / (real (card r) + 1) > 0" apply(rule divide_pos_pos,rule k) by auto
+    have "f integrable_on {u..v}" apply(rule integrable_subinterval[OF assms(1)])
+      using q'(2)[OF i] unfolding uv by auto
+    note integrable_integral[OF this, unfolded has_integral[of f]]
+    from this[rule_format,OF *] guess dd .. note dd=conjunctD2[OF this,rule_format]
+    note gauge_inter[OF `gauge d` dd(1)] from fine_division_exists[OF this,of u v] guess qq .
+    thus ?case apply(rule_tac x=qq in exI) using dd(2)[of qq] unfolding fine_inter uv by auto qed
+  from bchoice[OF this] guess qq .. note qq=this[rule_format]
+
+  let ?p = "p \<union> \<Union>qq ` r" have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral {a..b} f) < e"
+    apply(rule assms(4)[rule_format])
+  proof show "d fine ?p" apply(rule fine_union,rule p) apply(rule fine_unions) using qq by auto 
+    note * = tagged_partial_division_of_union_self[OF p(1)]
+    have "p \<union> \<Union>qq ` r tagged_division_of \<Union>snd ` p \<union> \<Union>r"
+    proof(rule tagged_division_union[OF * tagged_division_unions])
+      show "finite r" by fact case goal2 thus ?case using qq by auto
+    next case goal3 thus ?case apply(rule,rule,rule) apply(rule q'(5)) unfolding r_def by auto
+    next case goal4 thus ?case apply(rule inter_interior_unions_intervals) apply(fact,rule)
+        apply(rule,rule q') defer apply(rule,subst Int_commute) 
+        apply(rule inter_interior_unions_intervals) apply(rule finite_imageI,rule p',rule) defer
+        apply(rule,rule q') using q(1) p' unfolding r_def by auto qed
+    moreover have "\<Union>snd ` p \<union> \<Union>r = {a..b}" "{qq i |i. i \<in> r} = qq ` r"
+      unfolding Union_Un_distrib[THEN sym] r_def using q by auto
+    ultimately show "?p tagged_division_of {a..b}" by fastsimp qed
+
+  hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>qq ` r. content k *\<^sub>R f x) -
+    integral {a..b} f) < e" apply(subst setsum_Un_zero[THEN sym]) apply(rule p') prefer 3 
+    apply assumption apply rule apply(rule finite_imageI,rule r) apply safe apply(drule qq)
+  proof- fix x l k assume as:"(x,l)\<in>p" "(x,l)\<in>qq k" "k\<in>r"
+    note qq[OF this(3)] note tagged_division_ofD(3,4)[OF conjunct1[OF this] as(2)]
+    from this(2) guess u v apply-by(erule exE)+ note uv=this
+    have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto
+    hence "l\<in>q" "k\<in>q" "l\<noteq>k" using as(1,3) q(1) unfolding r_def by auto
+    note q'(5)[OF this] hence "interior l = {}" using subset_interior[OF `l \<subseteq> k`] by blast
+    thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto qed auto
+
+  hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x))
+    (qq ` r) - integral {a..b} f) < e" apply(subst(asm) setsum_UNION_zero)
+    prefer 4 apply assumption apply(rule finite_imageI,fact)
+    unfolding split_paired_all split_conv image_iff defer apply(erule bexE)+
+  proof- fix x m k l T1 T2 assume "(x,m)\<in>T1" "(x,m)\<in>T2" "T1\<noteq>T2" "k\<in>r" "l\<in>r" "T1 = qq k" "T2 = qq l"
+    note as = this(1-5)[unfolded this(6-)] note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]]
+    from this(2)[OF as(4,1)] guess u v apply-by(erule exE)+ note uv=this
+    have *:"interior (k \<inter> l) = {}" unfolding interior_inter apply(rule q')
+      using as unfolding r_def by auto
+    have "interior m = {}" unfolding subset_empty[THEN sym] unfolding *[THEN sym]
+      apply(rule subset_interior) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
+    thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto 
+  qed(insert qq, auto)
+
+  hence **:"norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r -
+    integral {a..b} f) < e" apply(subst(asm) setsum_reindex_nonzero) apply fact
+    apply(rule setsum_0',rule) unfolding split_paired_all split_conv defer apply assumption
+  proof- fix k l x m assume as:"k\<in>r" "l\<in>r" "k\<noteq>l" "qq k = qq l" "(x,m)\<in>qq k"
+    note tagged_division_ofD(6)[OF qq[THEN conjunct1]] from this[OF as(1)] this[OF as(2)] 
+    show "content m *\<^sub>R f x = 0"  using as(3) unfolding as by auto qed
+  
+  have *:"\<And>ir ip i cr cp. norm((cp + cr) - i) < e \<Longrightarrow> norm(cr - ir) < k \<Longrightarrow> 
+    ip + ir = i \<Longrightarrow> norm(cp - ip) \<le> e + k" 
+  proof- case goal1 thus ?case  using norm_triangle_le[of "cp + cr - i" "- (cr - ir)"]  
+      unfolding goal1(3)[THEN sym] norm_minus_cancel by(auto simp add:group_simps) qed
+  
+  have "?x =  norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))"
+    unfolding split_def setsum_subtractf ..
+  also have "... \<le> e + k" apply(rule *[OF **, where ir="setsum (\<lambda>k. integral k f) r"])
+  proof- case goal2 have *:"(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
+      apply(subst setsum_reindex_nonzero) apply fact
+      unfolding split_paired_all snd_conv split_def o_def
+    proof- fix x l y m assume as:"(x,l)\<in>p" "(y,m)\<in>p" "(x,l)\<noteq>(y,m)" "l = m"
+      from p'(4)[OF as(1)] guess u v apply-by(erule exE)+ note uv=this
+      show "integral l f = 0" unfolding uv apply(rule integral_unique)
+        apply(rule has_integral_null) unfolding content_eq_0_interior
+        using p'(5)[OF as(1-3)] unfolding uv as(4)[THEN sym] by auto
+    qed auto 
+    show ?case unfolding integral_combine_division_topdown[OF assms(1) q(2)] * r_def
+      apply(rule setsum_Un_disjoint'[THEN sym]) using q(1) q'(1) p'(1) by auto
+  next  case goal1 have *:"k * real (card r) / (1 + real (card r)) < k" using k by(auto simp add:field_simps)
+    show ?case apply(rule le_less_trans[of _ "setsum (\<lambda>x. k / (real (card r) + 1)) r"])
+      unfolding setsum_subtractf[THEN sym] apply(rule setsum_norm_le,fact)
+      apply rule apply(drule qq) defer unfolding real_divide_def setsum_left_distrib[THEN sym]
+      unfolding real_divide_def[THEN sym] using * by(auto simp add:field_simps real_eq_of_nat)
+  qed finally show "?x \<le> e + k" . qed
+
+lemma henstock_lemma_part2: fixes f::"real^'m \<Rightarrow> real^'n"
+  assumes "f integrable_on {a..b}" "0 < e" "gauge d"
+  "\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p -
+          integral({a..b}) f) < e"    "p tagged_partial_division_of {a..b}" "d fine p"
+  shows "setsum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (CARD('n)) * e"
+  unfolding split_def apply(rule vsum_norm_allsubsets_bound) defer 
+  apply(rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)])
+  apply safe apply(rule assms[rule_format,unfolded split_def]) defer
+  apply(rule tagged_partial_division_subset,rule assms,assumption)
+  apply(rule fine_subset,assumption,rule assms) using assms(5) by auto
+  
+lemma henstock_lemma: fixes f::"real^'m \<Rightarrow> real^'n"
+  assumes "f integrable_on {a..b}" "e>0"
+  obtains d where "gauge d"
+  "\<forall>p. p tagged_partial_division_of {a..b} \<and> d fine p
+  \<longrightarrow> setsum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
+proof- have *:"e / (2 * (real CARD('n) + 1)) > 0" apply(rule divide_pos_pos) using assms(2) by auto
+  from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this]
+  guess d .. note d = conjunctD2[OF this] show thesis apply(rule that,rule d)
+  proof safe case goal1 note * = henstock_lemma_part2[OF assms(1) * d this]
+    show ?case apply(rule le_less_trans[OF *]) using `e>0` by(auto simp add:field_simps) qed qed
+
+subsection {* monotone convergence (bounded interval first). *}
+
+lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real^1"
+  assumes "\<forall>k. (f k) integrable_on {a..b}"
+  "\<forall>k. \<forall>x\<in>{a..b}. dest_vec1(f k x) \<le> dest_vec1(f (Suc k) x)"
+  "\<forall>x\<in>{a..b}. ((\<lambda>k. f k x) ---> g x) sequentially"
+  "bounded {integral {a..b} (f k) | k . k \<in> UNIV}"
+  shows "g integrable_on {a..b} \<and> ((\<lambda>k. integral ({a..b}) (f k)) ---> integral ({a..b}) g) sequentially"
+proof(case_tac[!] "content {a..b} = 0") assume as:"content {a..b} = 0"
+  show ?thesis using integrable_on_null[OF as] unfolding integral_null[OF as] using Lim_const by auto
+next assume ab:"content {a..b} \<noteq> 0"
+  have fg:"\<forall>x\<in>{a..b}. \<forall> k. (f k x)$1 \<le> (g x)$1"
+  proof safe case goal1 note assms(3)[rule_format,OF this]
+    note * = Lim_component_ge[OF this trivial_limit_sequentially]
+    show ?case apply(rule *) unfolding eventually_sequentially
+      apply(rule_tac x=k in exI) apply- apply(rule transitive_stepwise_le)
+      using assms(2)[rule_format,OF goal1] by auto qed
+  have "\<exists>i. ((\<lambda>k. integral ({a..b}) (f k)) ---> i) sequentially"
+    apply(rule bounded_increasing_convergent) defer
+    apply rule apply(rule integral_component_le) apply safe
+    apply(rule assms(1-2)[rule_format])+ using assms(4) by auto
+  then guess i .. note i=this
+  have i':"\<And>k. dest_vec1(integral({a..b}) (f k)) \<le> dest_vec1 i"
+    apply(rule Lim_component_ge,rule i) apply(rule trivial_limit_sequentially)
+    unfolding eventually_sequentially apply(rule_tac x=k in exI)
+    apply(rule transitive_stepwise_le) prefer 3 apply(rule integral_dest_vec1_le)
+    apply(rule assms(1-2)[rule_format])+ using assms(2) by auto
+
+  have "(g has_integral i) {a..b}" unfolding has_integral
+  proof safe case goal1 note e=this
+    hence "\<forall>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
+             norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral {a..b} (f k)) < e / 2 ^ (k + 2)))"
+      apply-apply(rule,rule assms(1)[unfolded has_integral_integral has_integral,rule_format])
+      apply(rule divide_pos_pos) by auto
+    from choice[OF this] guess c .. note c=conjunctD2[OF this[rule_format],rule_format]
+
+    have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i$1 - dest_vec1(integral {a..b} (f k)) \<and>
+                   i$1 - dest_vec1(integral {a..b} (f k)) < e / 4"
+    proof- case goal1 have "e/4 > 0" using e by auto
+      from i[unfolded Lim_sequentially,rule_format,OF this] guess r ..
+      thus ?case apply(rule_tac x=r in exI) apply rule
+        apply(erule_tac x=k in allE)
+      proof- case goal1 thus ?case using i'[of k] unfolding dist_real by auto qed qed
+    then guess r .. note r=conjunctD2[OF this[rule_format]]
+
+    have "\<forall>x\<in>{a..b}. \<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)$1 - (f k x)$1 \<and>
+           (g x)$1 - (f k x)$1 < e / (4 * content({a..b}))"
+    proof case goal1 have "e / (4 * content {a..b}) > 0" apply(rule divide_pos_pos,fact)
+        using ab content_pos_le[of a b] by auto
+      from assms(3)[rule_format,OF goal1,unfolded Lim_sequentially,rule_format,OF this]
+      guess n .. note n=this
+      thus ?case apply(rule_tac x="n + r" in exI) apply safe apply(erule_tac[2-3] x=k in allE)
+        unfolding dist_real using fg[rule_format,OF goal1] by(auto simp add:field_simps) qed
+    from bchoice[OF this] guess m .. note m=conjunctD2[OF this[rule_format],rule_format]
+    def d \<equiv> "\<lambda>x. c (m x) x" 
+
+    show ?case apply(rule_tac x=d in exI)
+    proof safe show "gauge d" using c(1) unfolding gauge_def d_def by auto
+    next fix p assume p:"p tagged_division_of {a..b}" "d fine p"
+      note p'=tagged_division_ofD[OF p(1)]
+      have "\<exists>a. \<forall>x\<in>p. m (fst x) \<le> a" by(rule upper_bound_finite_set,fact)
+      then guess s .. note s=this
+      have *:"\<forall>a b c d. norm(a - b) \<le> e / 4 \<and> norm(b - c) < e / 2 \<and>
+            norm(c - d) < e / 4 \<longrightarrow> norm(a - d) < e" 
+      proof safe case goal1 thus ?case using norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
+          norm_triangle_lt[of "a - b + (b - c)" "c - d" e] unfolding norm_minus_cancel
+          by(auto simp add:group_simps) qed
+      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e" apply(rule *[rule_format,where
+          b="\<Sum>(x, k)\<in>p. content k *\<^sub>R f (m x) x" and c="\<Sum>(x, k)\<in>p. integral k (f (m x))"])
+      proof safe case goal1
+         show ?case apply(rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content {a..b}))"])
+           unfolding setsum_subtractf[THEN sym] apply(rule order_trans,rule setsum_norm[OF p'(1)])
+           apply(rule setsum_mono) unfolding split_paired_all split_conv
+           unfolding split_def setsum_left_distrib[THEN sym] scaleR.diff_right[THEN sym]
+           unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
+         proof- fix x k assume xk:"(x,k) \<in> p" hence x:"x\<in>{a..b}" using p'(2-3)[OF xk] by auto
+           from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this
+           show " norm (content k *\<^sub>R (g x - f (m x) x)) \<le> content k * (e / (4 * content {a..b}))"
+             unfolding norm_scaleR uv unfolding abs_of_nonneg[OF content_pos_le] 
+             apply(rule mult_left_mono) unfolding norm_real using m(2)[OF x,of "m x"] by auto
+         qed(insert ab,auto)
+         
+       next case goal2 show ?case apply(rule le_less_trans[of _ "norm (\<Sum>j = 0..s.
+           \<Sum>(x, k)\<in>{xk\<in>p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))"])
+           apply(subst setsum_group) apply fact apply(rule finite_atLeastAtMost) defer
+           apply(subst split_def)+ unfolding setsum_subtractf apply rule
+         proof- show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p.
+             m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2"
+             apply(rule le_less_trans[of _ "setsum (\<lambda>i. e / 2^(i+2)) {0..s}"])
+             apply(rule setsum_norm_le[OF finite_atLeastAtMost])
+           proof show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
+               unfolding power_add real_divide_def inverse_mult_distrib
+               unfolding setsum_right_distrib[THEN sym] setsum_left_distrib[THEN sym]
+               unfolding power_inverse sum_gp apply(rule mult_strict_left_mono[OF _ e])
+               unfolding power2_eq_square by auto
+             fix t assume "t\<in>{0..s}"
+             show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x -
+               integral k (f (m x))) \<le> e / 2 ^ (t + 2)"apply(rule order_trans[of _
+               "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \<in> p. m (fst xk) = t})"])
+               apply(rule eq_refl) apply(rule arg_cong[where f=norm]) apply(rule setsum_cong2) defer
+               apply(rule henstock_lemma_part1) apply(rule assms(1)[rule_format])
+               apply(rule divide_pos_pos,rule e) defer  apply safe apply(rule c)+
+               apply rule apply assumption+ apply(rule tagged_partial_division_subset[of p])
+               apply(rule p(1)[unfolded tagged_division_of_def,THEN conjunct1]) defer
+               unfolding fine_def apply safe apply(drule p(2)[unfolded fine_def,rule_format])
+               unfolding d_def by auto qed
+         qed(insert s, auto)
+
+       next case goal3
+         note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)]
+         have *:"\<And>sr sx ss ks kr::real^1. kr = sr \<longrightarrow> ks = ss \<longrightarrow> ks \<le> i \<and> sr \<le> sx \<and> sx \<le> ss \<and> 0 \<le> i$1 - kr$1
+           \<and> i$1 - kr$1 < e/4 \<longrightarrow> abs(sx$1 - i$1) < e/4" unfolding Cart_eq forall_1 vector_le_def by arith
+         show ?case unfolding norm_real Cart_nth.diff apply(rule *[rule_format],safe)
+           apply(rule comb[of r],rule comb[of s]) unfolding vector_le_def forall_1 setsum_component
+           apply(rule i') apply(rule_tac[1-2] setsum_mono) unfolding split_paired_all split_conv
+           apply(rule_tac[1-2] integral_component_le[OF ])
+         proof safe show "0 \<le> i$1 - (integral {a..b} (f r))$1" using r(1) by auto
+           show "i$1 - (integral {a..b} (f r))$1 < e / 4" using r(2) by auto
+           fix x k assume xk:"(x,k)\<in>p" from p'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this
+           show "f r integrable_on k" "f s integrable_on k" "f (m x) integrable_on k" "f (m x) integrable_on k" 
+             unfolding uv apply(rule_tac[!] integrable_on_subinterval[OF assms(1)[rule_format]])
+             using p'(3)[OF xk] unfolding uv by auto 
+           fix y assume "y\<in>k" hence "y\<in>{a..b}" using p'(3)[OF xk] by auto
+           hence *:"\<And>m. \<forall>n\<ge>m. (f m y)$1 \<le> (f n y)$1" apply-apply(rule transitive_stepwise_le) using assms(2) by auto
+           show "(f r y)$1 \<le> (f (m x) y)$1" "(f (m x) y)$1 \<le> (f s y)$1"
+             apply(rule_tac[!] *[rule_format]) using s[rule_format,OF xk] m(1)[of x] p'(2-3)[OF xk] by auto
+         qed qed qed qed note * = this 
+
+   have "integral {a..b} g = i" apply(rule integral_unique) using * .
+   thus ?thesis using i * by auto qed
+
+lemma monotone_convergence_increasing: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real^1"
+  assumes "\<forall>k. (f k) integrable_on s"  "\<forall>k. \<forall>x\<in>s. (f k x)$1 \<le> (f (Suc k) x)$1"
+  "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}"
+  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+proof- have lem:"\<And>f::nat \<Rightarrow> real^'n \<Rightarrow> real^1. \<And> g s. \<forall>k.\<forall>x\<in>s. 0\<le>dest_vec1 (f k x) \<Longrightarrow> \<forall>k. (f k) integrable_on s \<Longrightarrow>
+    \<forall>k. \<forall>x\<in>s. (f k x)$1 \<le> (f (Suc k) x)$1 \<Longrightarrow> \<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially  \<Longrightarrow>
+    bounded {integral s (f k)| k. True} \<Longrightarrow> g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+  proof- case goal1 note assms=this[rule_format]
+    have "\<forall>x\<in>s. \<forall>k. dest_vec1(f k x) \<le> dest_vec1(g x)" apply safe apply(rule Lim_component_ge)
+      apply(rule goal1(4)[rule_format],assumption) apply(rule trivial_limit_sequentially)
+      unfolding eventually_sequentially apply(rule_tac x=k in exI)
+      apply(rule transitive_stepwise_le) using goal1(3) by auto note fg=this[rule_format]
+
+    have "\<exists>i. ((\<lambda>k. integral s (f k)) ---> i) sequentially" apply(rule bounded_increasing_convergent)
+      apply(rule goal1(5)) apply(rule,rule integral_component_le) apply(rule goal1(2)[rule_format])+
+      using goal1(3) by auto then guess i .. note i=this
+    have "\<And>k. \<forall>x\<in>s. \<forall>n\<ge>k. f k x \<le> f n x" apply(rule,rule transitive_stepwise_le) using goal1(3) by auto
+    hence i':"\<forall>k. (integral s (f k))$1 \<le> i$1" apply-apply(rule,rule Lim_component_ge)
+      apply(rule i,rule trivial_limit_sequentially) unfolding eventually_sequentially
+      apply(rule_tac x=k in exI,safe) apply(rule integral_dest_vec1_le)
+      apply(rule goal1(2)[rule_format])+ by auto 
+
+    note int = assms(2)[unfolded integrable_alt[of _ s],THEN conjunct1,rule_format]
+    have ifif:"\<And>k t. (\<lambda>x. if x \<in> t then if x \<in> s then f k x else 0 else 0) =
+      (\<lambda>x. if x \<in> t\<inter>s then f k x else 0)" apply(rule ext) by auto
+    have int':"\<And>k a b. f k integrable_on {a..b} \<inter> s" apply(subst integrable_restrict_univ[THEN sym])
+      apply(subst ifif[THEN sym]) apply(subst integrable_restrict_univ) using int .
+    have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on {a..b} \<and>
+      ((\<lambda>k. integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) --->
+      integral {a..b} (\<lambda>x. if x \<in> s then g x else 0)) sequentially"
+    proof(rule monotone_convergence_interval,safe)
+      case goal1 show ?case using int .
+    next case goal2 thus ?case apply-apply(cases "x\<in>s") using assms(3) by auto
+    next case goal3 thus ?case apply-apply(cases "x\<in>s") using assms(4) by auto
+    next case goal4 note * = integral_dest_vec1_nonneg[unfolded vector_le_def forall_1 zero_index]
+      have "\<And>k. norm (integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))"
+        unfolding norm_real apply(subst abs_of_nonneg) apply(rule *[OF int])
+        apply(safe,case_tac "x\<in>s") apply(drule assms(1)) prefer 3
+        apply(subst abs_of_nonneg) apply(rule *[OF assms(2) goal1(1)[THEN spec]])
+        apply(subst integral_restrict_univ[THEN sym,OF int]) 
+        unfolding ifif unfolding integral_restrict_univ[OF int']
+        apply(rule integral_subset_component_le[OF _ int' assms(2)]) using assms(1) by auto
+      thus ?case using assms(5) unfolding bounded_iff apply safe
+        apply(rule_tac x=aa in exI,safe) apply(erule_tac x="integral s (f k)" in ballE)
+        apply(rule order_trans) apply assumption by auto qed note g = conjunctD2[OF this]
+
+    have "(g has_integral i) s" unfolding has_integral_alt' apply safe apply(rule g(1))
+    proof- case goal1 hence "e/4>0" by auto
+      from i[unfolded Lim_sequentially,rule_format,OF this] guess N .. note N=this
+      note assms(2)[of N,unfolded has_integral_integral has_integral_alt'[of "f N"]]
+      from this[THEN conjunct2,rule_format,OF `e/4>0`] guess B .. note B=conjunctD2[OF this]
+      show ?case apply(rule,rule,rule B,safe)
+      proof- fix a b::"real^'n" assume ab:"ball 0 B \<subseteq> {a..b}"
+        from `e>0` have "e/2>0" by auto
+        from g(2)[unfolded Lim_sequentially,of a b,rule_format,OF this] guess M .. note M=this
+        have **:"norm (integral {a..b} (\<lambda>x. if x \<in> s then f N x else 0) - i) < e/2"
+          apply(rule norm_triangle_half_l) using B(2)[rule_format,OF ab] N[rule_format,of N]
+          unfolding vector_dist_norm apply-defer apply(subst norm_minus_commute) by auto
+        have *:"\<And>f1 f2 g. abs(f1 - i$1) < e / 2 \<longrightarrow> abs(f2 - g) < e / 2 \<longrightarrow> f1 \<le> f2 \<longrightarrow> f2 \<le> i$1
+          \<longrightarrow> abs(g - i$1) < e" by arith
+        show "norm (integral {a..b} (\<lambda>x. if x \<in> s then g x else 0) - i) < e" 
+          unfolding norm_real Cart_simps apply(rule *[rule_format])
+          apply(rule **[unfolded norm_real Cart_simps])
+          apply(rule M[rule_format,of "M + N",unfolded dist_real]) apply(rule le_add1)
+          apply(rule integral_component_le[OF int int]) defer
+          apply(rule order_trans[OF _ i'[rule_format,of "M + N"]])
+        proof safe case goal2 have "\<And>m. x\<in>s \<Longrightarrow> \<forall>n\<ge>m. (f m x)$1 \<le> (f n x)$1"
+            apply(rule transitive_stepwise_le) using assms(3) by auto thus ?case by auto
+        next case goal1 show ?case apply(subst integral_restrict_univ[THEN sym,OF int]) 
+            unfolding ifif integral_restrict_univ[OF int']
+            apply(rule integral_subset_component_le[OF _ int']) using assms by auto
+        qed qed qed 
+    thus ?case apply safe defer apply(drule integral_unique) using i by auto qed
+
+  have sub:"\<And>k. integral s (\<lambda>x. f k x - f 0 x) = integral s (f k) - integral s (f 0)"
+    apply(subst integral_sub) apply(rule assms(1)[rule_format])+ by rule
+  have "\<And>x m. x\<in>s \<Longrightarrow> \<forall>n\<ge>m. dest_vec1 (f m x) \<le> dest_vec1 (f n x)" apply(rule transitive_stepwise_le)
+    using assms(2) by auto note * = this[rule_format]
+  have "(\<lambda>x. g x - f 0 x) integrable_on s \<and>((\<lambda>k. integral s (\<lambda>x. f (Suc k) x - f 0 x)) --->
+      integral s (\<lambda>x. g x - f 0 x)) sequentially" apply(rule lem,safe)
+  proof- case goal1 thus ?case using *[of x 0 "Suc k"] by auto
+  next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto
+  next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto
+  next case goal4 thus ?case apply-apply(rule Lim_sub) 
+      using seq_offset[OF assms(3)[rule_format],of x 1] by auto
+  next case goal5 thus ?case using assms(4) unfolding bounded_iff
+      apply safe apply(rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
+      apply safe apply(erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE) unfolding sub
+      apply(rule order_trans[OF norm_triangle_ineq4]) by auto qed
+  note conjunctD2[OF this] note Lim_add[OF this(2) Lim_const[of "integral s (f 0)"]]
+    integrable_add[OF this(1) assms(1)[rule_format,of 0]]
+  thus ?thesis unfolding sub apply-apply rule defer apply(subst(asm) integral_sub)
+    using assms(1) apply auto apply(rule seq_offset_rev[where k=1]) by auto qed
+
+lemma monotone_convergence_decreasing: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real^1"
+  assumes "\<forall>k. (f k) integrable_on s"  "\<forall>k. \<forall>x\<in>s. (f (Suc k) x)$1 \<le> (f k x)$1"
+  "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}"
+  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+proof- note assm = assms[rule_format]
+  have *:"{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R -1 ` {integral s (f k)| k. True}"
+    apply safe unfolding image_iff apply(rule_tac x="integral s (f k)" in bexI) prefer 3
+    apply(rule_tac x=k in exI) unfolding integral_neg[OF assm(1)] by auto
+  have "(\<lambda>x. - g x) integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. - f k x))
+    ---> integral s (\<lambda>x. - g x))  sequentially" apply(rule monotone_convergence_increasing)
+    apply(safe,rule integrable_neg) apply(rule assm) defer apply(rule Lim_neg)
+    apply(rule assm,assumption) unfolding * apply(rule bounded_scaling) using assm by auto
+  note * = conjunctD2[OF this]
+  show ?thesis apply rule using integrable_neg[OF *(1)] defer
+    using Lim_neg[OF *(2)] apply- unfolding integral_neg[OF assm(1)]
+    unfolding integral_neg[OF *(1),THEN sym] by auto qed
+
+lemma monotone_convergence_increasing_real: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real"
+  assumes "\<forall>k. (f k) integrable_on s"  "\<forall>k. \<forall>x\<in>s. (f (Suc k) x) \<ge> (f k x)"
+  "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}"
+  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+proof- have *:"{integral s (\<lambda>x. vec1 (f k x)) |k. True} =  vec1 ` {integral s (f k) |k. True}"
+    unfolding integral_trans[OF assms(1)[rule_format]] by auto
+  have "vec1 \<circ> g integrable_on s \<and> ((\<lambda>k. integral s (vec1 \<circ> f k)) ---> integral s (vec1 \<circ> g)) sequentially"
+    apply(rule monotone_convergence_increasing) unfolding o_def integrable_on_trans
+    unfolding vec1_dest_vec1 apply(rule assms)+ unfolding Lim_trans unfolding * using assms(3,4) by auto
+  thus ?thesis unfolding o_def unfolding integral_trans[OF assms(1)[rule_format]] by auto qed
+
+lemma monotone_convergence_decreasing_real: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real"
+  assumes "\<forall>k. (f k) integrable_on s"  "\<forall>k. \<forall>x\<in>s. (f (Suc k) x) \<le> (f k x)"
+  "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}"
+  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+proof- have *:"{integral s (\<lambda>x. vec1 (f k x)) |k. True} =  vec1 ` {integral s (f k) |k. True}"
+    unfolding integral_trans[OF assms(1)[rule_format]] by auto
+  have "vec1 \<circ> g integrable_on s \<and> ((\<lambda>k. integral s (vec1 \<circ> f k)) ---> integral s (vec1 \<circ> g)) sequentially"
+    apply(rule monotone_convergence_decreasing) unfolding o_def integrable_on_trans
+    unfolding vec1_dest_vec1 apply(rule assms)+ unfolding Lim_trans unfolding * using assms(3,4) by auto
+  thus ?thesis unfolding o_def unfolding integral_trans[OF assms(1)[rule_format]] by auto qed
+
+subsection {* absolute integrability (this is the same as Lebesgue integrability). *}
+
+definition absolutely_integrable_on (infixr "absolutely'_integrable'_on" 46) where
+  "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. (norm(f x))) integrable_on s"
+
+lemma absolutely_integrable_onI[intro?]:
+  "f integrable_on s \<Longrightarrow> (\<lambda>x. (norm(f x))) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
+  unfolding absolutely_integrable_on_def by auto
+
+lemma absolutely_integrable_onD[dest]: assumes "f absolutely_integrable_on s"
+  shows "f integrable_on s" "(\<lambda>x. (norm(f x))) integrable_on s"
+  using assms unfolding absolutely_integrable_on_def by auto
+
+lemma absolutely_integrable_on_trans[simp]: fixes f::"real^'n \<Rightarrow> real" shows
+  "(vec1 o f) absolutely_integrable_on s \<longleftrightarrow> f absolutely_integrable_on s"
+  unfolding absolutely_integrable_on_def o_def by auto
+
+lemma integral_norm_bound_integral: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f integrable_on s" "g integrable_on s" "\<forall>x\<in>s. norm(f x) \<le> g x"
+  shows "norm(integral s f) \<le> (integral s g)"
+proof- have *:"\<And>x y. (\<forall>e::real. 0 < e \<longrightarrow> x < y + e) \<longrightarrow> x \<le> y" apply(safe,rule ccontr)
+    apply(erule_tac x="x - y" in allE) by auto
+  have "\<And>e sg dsa dia ig. norm(sg) \<le> dsa \<longrightarrow> abs(dsa - dia) < e / 2 \<longrightarrow> norm(sg - ig) < e / 2
+    \<longrightarrow> norm(ig) < dia + e" 
+  proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]])
+      apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a
+      apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1)
+      apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith
+  qed note norm=this[rule_format]
+  have lem:"\<And>f::real^'n \<Rightarrow> 'a. \<And> g a b. f integrable_on {a..b} \<Longrightarrow> g integrable_on {a..b} \<Longrightarrow>
+    \<forall>x\<in>{a..b}. norm(f x) \<le> (g x) \<Longrightarrow> norm(integral({a..b}) f) \<le> (integral({a..b}) g)"
+  proof(rule *[rule_format]) case goal1 hence *:"e/2>0" by auto
+    from integrable_integral[OF goal1(1),unfolded has_integral[of f],rule_format,OF *]
+    guess d1 .. note d1 = conjunctD2[OF this,rule_format]
+    from integrable_integral[OF goal1(2),unfolded has_integral[of g],rule_format,OF *]
+    guess d2 .. note d2 = conjunctD2[OF this,rule_format]
+    note gauge_inter[OF d1(1) d2(1)]
+    from fine_division_exists[OF this, of a b] guess p . note p=this
+    show ?case 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 setsum_norm_le)
+    proof safe fix x k assume "(x,k)\<in>p" note as = tagged_division_ofD(2-4)[OF p(1) this]
+      from this(3) guess u v apply-by(erule exE)+ note uv=this
+      show "norm (content k *\<^sub>R f x) \<le> 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 goal1(3) as by auto
+    qed(insert p[unfolded fine_inter],auto) qed
+
+  { presume "\<And>e. 0 < e \<Longrightarrow> norm (integral s f) < integral s g + e" 
+    thus ?thesis apply-apply(rule *[rule_format]) by auto }
+  fix e::real assume "e>0" hence e:"e/2 > 0" by auto
+  note assms(1)[unfolded integrable_alt[of f]] note f=this[THEN conjunct1,rule_format]
+  note assms(2)[unfolded integrable_alt[of g]] note g=this[THEN conjunct1,rule_format]
+  from integrable_integral[OF assms(1),unfolded has_integral'[of f],rule_format,OF e]
+  guess B1 .. note B1=conjunctD2[OF this[rule_format],rule_format]
+  from integrable_integral[OF assms(2),unfolded has_integral'[of g],rule_format,OF e]
+  guess B2 .. note B2=conjunctD2[OF this[rule_format],rule_format]
+  from bounded_subset_closed_interval[OF bounded_ball, of "0::real^'n" "max B1 B2"]
+  guess a b apply-by(erule exE)+ note ab=this[unfolded ball_max_Un]
+
+  have "ball 0 B1 \<subseteq> {a..b}" using ab by auto
+  from B1(2)[OF this] guess z .. note z=conjunctD2[OF this]
+  have "ball 0 B2 \<subseteq> {a..b}" using ab by auto
+  from B2(2)[OF this] guess w .. note w=conjunctD2[OF this]
+
+  show "norm (integral s f) < integral s g + e" apply(rule norm)
+    apply(rule lem[OF f g, of a b]) unfolding integral_unique[OF z(1)] integral_unique[OF w(1)]
+    defer apply(rule w(2)[unfolded real_norm_def],rule z(2))
+    apply safe apply(case_tac "x\<in>s") unfolding if_P apply(rule assms(3)[rule_format]) by auto qed
+
+lemma integral_norm_bound_integral_component: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f integrable_on s" "g integrable_on s"  "\<forall>x\<in>s. norm(f x) \<le> (g x)$k"
+  shows "norm(integral s f) \<le> (integral s g)$k"
+proof- have "norm (integral s f) \<le> integral s ((\<lambda>x. x $ k) o g)"
+    apply(rule integral_norm_bound_integral[OF assms(1)])
+    apply(rule integrable_linear[OF assms(2)],rule)
+    unfolding o_def by(rule assms)
+  thus ?thesis unfolding o_def integral_component_eq[OF assms(2)] . qed
+
+lemma has_integral_norm_bound_integral_component: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "(f has_integral i) s" "(g has_integral j) s" "\<forall>x\<in>s. norm(f x) \<le> (g x)$k"
+  shows "norm(i) \<le> j$k" using integral_norm_bound_integral_component[of f s g k]
+  unfolding integral_unique[OF assms(1)] integral_unique[OF assms(2)]
+  using assms by auto
+
+lemma absolutely_integrable_le: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f absolutely_integrable_on s"
+  shows "norm(integral s f) \<le> integral s (\<lambda>x. norm(f x))"
+  apply(rule integral_norm_bound_integral) using assms by auto
+
+lemma absolutely_integrable_0[intro]: "(\<lambda>x. 0) absolutely_integrable_on s"
+  unfolding absolutely_integrable_on_def by auto
+
+lemma absolutely_integrable_cmul[intro]:
+ "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on s"
+  unfolding absolutely_integrable_on_def using integrable_cmul[of f s c]
+  using integrable_cmul[of "\<lambda>x. norm (f x)" s "abs c"] by auto
+
+lemma absolutely_integrable_neg[intro]:
+ "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) absolutely_integrable_on s"
+  apply(drule absolutely_integrable_cmul[where c="-1"]) by auto
+
+lemma absolutely_integrable_norm[intro]:
+ "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. norm(f x)) absolutely_integrable_on s"
+  unfolding absolutely_integrable_on_def by auto
+
+lemma absolutely_integrable_abs[intro]:
+ "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. abs(f x::real)) absolutely_integrable_on s"
+  apply(drule absolutely_integrable_norm) unfolding real_norm_def .
+
+lemma absolutely_integrable_on_subinterval: fixes f::"real^'n \<Rightarrow> 'a::banach" shows
+  "f absolutely_integrable_on s \<Longrightarrow> {a..b} \<subseteq> s \<Longrightarrow> f absolutely_integrable_on {a..b}" 
+  unfolding absolutely_integrable_on_def by(meson integrable_on_subinterval)
+
+lemma absolutely_integrable_bounded_variation: fixes f::"real^'n \<Rightarrow> 'a::banach"
+  assumes "f absolutely_integrable_on UNIV"
+  obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
+  apply(rule that[of "integral UNIV (\<lambda>x. norm (f x))"])
+proof safe case goal1 note d = division_ofD[OF this(2)]
+  have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. integral i (\<lambda>x. norm (f x)))"
+    apply(rule setsum_mono,rule absolutely_integrable_le) apply(drule d(4),safe)
+    apply(rule absolutely_integrable_on_subinterval[OF assms]) by auto
+  also have "... \<le> integral (\<Union>d) (\<lambda>x. norm (f x))"
+    apply(subst integral_combine_division_topdown[OF _ goal1(2)])
+    using integrable_on_subdivision[OF goal1(2)] using assms by auto
+  also have "... \<le> integral UNIV (\<lambda>x. norm (f x))"
+    apply(rule integral_subset_le) 
+    using integrable_on_subdivision[OF goal1(2)] using assms by auto
+  finally show ?case . qed
+
+lemma helplemma:
+  assumes "setsum (\<lambda>x. norm(f x - g x)) s < e" "finite s"
+  shows "abs(setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s) < e"
+  unfolding setsum_subtractf[THEN sym] apply(rule le_less_trans[OF setsum_abs])
+  apply(rule le_less_trans[OF _ assms(1)]) apply(rule setsum_mono)
+  using norm_triangle_ineq3 .
+
+lemma bounded_variation_absolutely_integrable_interval:
+  fixes f::"real^'n \<Rightarrow> real^'m" assumes "f integrable_on {a..b}"
+  "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
+  shows "f absolutely_integrable_on {a..b}"
+proof- let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of {a..b} }" def i \<equiv> "Sup ?S"
+  have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup)
+    apply(rule elementary_interval) defer apply(rule_tac x=B in exI)
+    apply(rule setleI) using assms(2) by auto
+  show ?thesis apply(rule,rule assms) apply rule apply(subst has_integral[of _ i])
+  proof safe case goal1 hence "i - e / 2 \<notin> Collect (isUb UNIV (setsum (\<lambda>k. norm (integral k f)) `
+        {d. d division_of {a..b}}))" using isLub_ubs[OF i,rule_format]
+      unfolding setge_def ubs_def by auto 
+    hence " \<exists>y. y division_of {a..b} \<and> i - e / 2 < (\<Sum>k\<in>y. norm (integral k f))"
+      unfolding mem_Collect_eq isUb_def setle_def by simp then guess d .. note d=conjunctD2[OF this]
+    note d' = division_ofD[OF this(1)]
+
+    have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
+    proof case goal1 have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
+        apply(rule separate_point_closed) apply(rule closed_Union)
+        apply(rule finite_subset[OF _ d'(1)]) apply safe apply(drule d'(4)) by auto
+      thus ?case apply safe apply(rule_tac x=da in exI,safe)
+        apply(erule_tac x=xa in ballE) by auto
+    qed from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
+
+    have "e/2 > 0" using goal1 by auto
+    from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
+    let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
+    show ?case apply(rule_tac x="?g" in exI) apply safe
+    proof- show "gauge ?g" using g(1) unfolding gauge_def using k(1) by auto
+      fix p assume "p tagged_division_of {a..b}" "?g fine p"
+      note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
+      note p' = tagged_division_ofD[OF p(1)]
+      def p' \<equiv> "{(x,k) | x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x,l) \<in> p \<and> k = i \<inter> l}"
+      have gp':"g fine p'" using p(2) unfolding p'_def fine_def by auto
+      have p'':"p' tagged_division_of {a..b}" apply(rule tagged_division_ofI)
+      proof- show "finite p'" apply(rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l))
+          ` {(k,xl) | k xl. k \<in> d \<and> xl \<in> 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) by auto
+        fix x k assume "(x,k)\<in>p'"
+        hence "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l" unfolding p'_def by auto
+        then guess i l apply-by(erule exE)+ note il=conjunctD4[OF this]
+        show "x\<in>k" "k\<subseteq>{a..b}" using p'(2-3)[OF il(3)] il by auto
+        show "\<exists>a b. k = {a..b}" unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
+          apply safe unfolding inter_interval by auto
+      next fix x1 k1 assume "(x1,k1)\<in>p'"
+        hence "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l" unfolding p'_def by auto
+        then guess i1 l1 apply-by(erule exE)+ note il1=conjunctD4[OF this]
+        fix x2 k2 assume "(x2,k2)\<in>p'"
+        hence "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l" unfolding p'_def by auto
+        then guess i2 l2 apply-by(erule exE)+ note il2=conjunctD4[OF this]
+        assume "(x1, k1) \<noteq> (x2, k2)"
+        hence "interior(i1) \<inter> interior(i2) = {} \<or> interior(l1) \<inter> interior(l2) = {}"
+          using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)] unfolding il1 il2 by auto
+        thus "interior k1 \<inter> interior k2 = {}" unfolding il1 il2 by auto
+      next have *:"\<forall>(x, X) \<in> p'. X \<subseteq> {a..b}" unfolding p'_def using d' by auto
+        show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = {a..b}" apply rule apply(rule Union_least)
+          unfolding mem_Collect_eq apply(erule exE) apply(drule *[rule_format]) apply safe
+        proof- fix y assume y:"y\<in>{a..b}"
+          hence "\<exists>x l. (x, l) \<in> p \<and> y\<in>l" unfolding p'(6)[THEN sym] by auto
+          then guess x l apply-by(erule exE)+ note xl=conjunctD2[OF this]
+          hence "\<exists>k. k\<in>d \<and> y\<in>k" using y unfolding d'(6)[THEN sym] by auto
+          then guess i .. note i = conjunctD2[OF this]
+          have "x\<in>i" using fineD[OF p(3) xl(1)] using k(2)[OF i(1), of x] using i(2) xl(2) by auto
+          thus "y\<in>\<Union>{k. \<exists>x. (x, k) \<in> p'}" unfolding p'_def Union_iff apply(rule_tac x="i \<inter> l" in bexI)
+            defer unfolding mem_Collect_eq apply(rule_tac x=x in exI)+ apply(rule_tac x="i\<inter>l" in exI)
+            apply safe apply(rule_tac x=i in exI) apply(rule_tac x=l in exI) using i xl by auto 
+        qed qed 
+
+      hence "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
+        apply-apply(rule g(2)[rule_format]) unfolding tagged_division_of_def apply safe using gp' .
+      hence **:" \<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2"
+        unfolding split_def apply(rule helplemma) using p'' by auto
+
+      have p'alt:"p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> ~(i \<inter> l = {})}"
+      proof safe case goal2
+        have "x\<in>i" using fineD[OF p(3) goal2(1)] k(2)[OF goal2(2), of x] goal2(4-) by auto
+        hence "(x, i \<inter> l) \<in> p'" unfolding p'_def apply safe
+          apply(rule_tac x=x in exI,rule_tac x="i\<inter>l" in exI) apply safe using goal2 by auto
+        thus ?case using goal2(3) by auto
+      next fix x k assume "(x,k)\<in>p'"
+        hence "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l" unfolding p'_def by auto
+        then guess i l apply-by(erule exE)+ note il=conjunctD4[OF this]
+        thus "\<exists>y i l. (x, k) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
+          apply(rule_tac x=x in exI,rule_tac x=i in exI,rule_tac x=l in exI)
+          using p'(2)[OF il(3)] by auto
+      qed
+      have sum_p':"(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
+        apply(subst setsum_over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
+        unfolding norm_eq_zero apply(rule integral_null,assumption) ..
+      note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
+
+      have *:"\<And>sni sni' sf sf'. abs(sf' - sni') < e / 2 \<longrightarrow> i - e / 2 < sni \<and> sni' \<le> i \<and>
+        sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs(sf - i) < e" by arith
+      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - i) < e" 
+        unfolding real_norm_def apply(rule *[rule_format,OF **],safe) apply(rule d(2))
+      proof- case goal1 show ?case unfolding sum_p'
+          apply(rule isLubD2[OF i]) using division_of_tagged_division[OF p''] by auto
+      next case goal2 have *:"{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
+          (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}" by auto
+        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
+        proof(rule setsum_mono) case goal1 note k=this
+          from d'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this
+          def d' \<equiv> "{{u..v} \<inter> l |l. l \<in> snd ` p \<and>  ~({u..v} \<inter> l = {})}" note uvab = d'(2)[OF k[unfolded uv]]
+          have "d' division_of {u..v}" apply(subst d'_def) apply(rule division_inter_1) 
+            apply(rule division_of_tagged_division[OF p(1)]) using uvab .
+          hence "norm (integral k f) \<le> setsum (\<lambda>k. norm (integral k f)) d'"
+            unfolding uv apply(subst integral_combine_division_topdown[of _ _ d'])
+            apply(rule integrable_on_subinterval[OF assms(1) uvab]) apply assumption
+            apply(rule setsum_norm_le) by auto
+          also have "... = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
+            apply(rule setsum_mono_zero_left) apply(subst simple_image)
+            apply(rule finite_imageI)+ apply fact unfolding d'_def uv apply blast
+          proof case goal1 hence "i \<in> {{u..v} \<inter> l |l. l \<in> snd ` p}" by auto
+            from this[unfolded mem_Collect_eq] guess l .. note l=this
+            hence "{u..v} \<inter> l = {}" using goal1 by auto thus ?case using l by auto
+          qed also have "... = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))" unfolding  simple_image
+            apply(rule setsum_reindex_nonzero[unfolded o_def])apply(rule finite_imageI,rule p')
+          proof- case goal1 have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)" apply(subst(2) interior_inter)
+              apply(rule Int_greatest) defer apply(subst goal1(4)) by auto
+            hence *:"interior (k \<inter> l) = {}" using snd_p(5)[OF goal1(1-3)] by auto
+            from d'(4)[OF k] snd_p(4)[OF goal1(1)] guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this
+            show ?case using * unfolding uv inter_interval content_eq_0_interior[THEN sym] by auto
+          qed finally show ?case .
+        qed also have "... = (\<Sum>(i,l)\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (i\<inter>l) f))"
+          apply(subst sum_sum_product[THEN sym],fact) using p'(1) by auto
+        also have "... = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (split op \<inter> x) f))"
+          unfolding split_def ..
+        also have "... = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
+          unfolding * apply(rule setsum_reindex_nonzero[THEN sym,unfolded o_def])
+          apply(rule finite_product_dependent) apply(fact,rule finite_imageI,rule p')
+          unfolding split_paired_all mem_Collect_eq split_conv o_def
+        proof- note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)]
+          fix l1 l2 k1 k2 assume as:"(l1, k1) \<noteq> (l2, k2)"  "l1 \<inter> k1 = l2 \<inter> k2" 
+            "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
+            "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
+          hence "l1 \<in> d" "k1 \<in> snd ` p" by auto from d'(4)[OF this(1)] *(1)[OF this(2)]
+          guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this
+          have "l1 \<noteq> l2 \<or> k1 \<noteq> k2" using as by auto
+          hence "(interior(k1) \<inter> interior(k2) = {} \<or> interior(l1) \<inter> interior(l2) = {})" apply-
+            apply(erule disjE) apply(rule disjI2) apply(rule d'(5)) prefer 4 apply(rule disjI1)
+            apply(rule *) using as by auto
+          moreover have "interior(l1 \<inter> k1) = interior(l2 \<inter> k2)" using as(2) by auto
+          ultimately have "interior(l1 \<inter> k1) = {}" by auto
+          thus "norm (integral (l1 \<inter> k1) f) = 0" unfolding uv inter_interval
+            unfolding content_eq_0_interior[THEN sym] by auto
+        qed also have "... = (\<Sum>(x, k)\<in>p'. norm (integral k f))" unfolding sum_p'
+          apply(rule setsum_mono_zero_right) apply(subst *)
+          apply(rule finite_imageI[OF finite_product_dependent]) apply fact
+          apply(rule finite_imageI[OF p'(1)]) apply safe
+        proof- case goal2 have "ia \<inter> b = {}" using goal2 unfolding p'alt image_iff Bex_def not_ex
+            apply(erule_tac x="(a,ia\<inter>b)" in allE) by auto thus ?case by auto
+        next case goal1 thus ?case unfolding p'_def apply safe
+            apply(rule_tac x=i in exI,rule_tac x=l in exI) unfolding snd_conv image_iff 
+            apply safe apply(rule_tac x="(a,l)" in bexI) by auto
+        qed finally show ?case .
+
+      next case goal3
+        let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
+        have Sigma_alt:"\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}" by auto
+        have *:"?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)" (*{(xl,i)|xl i. xl\<in>p \<and> i\<in>d}"**)
+          apply safe unfolding image_iff apply(rule_tac x="((x,l),i)" in bexI) by auto
+        note pdfin = finite_cartesian_product[OF p'(1) d'(1)]
+        have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x, k)\<in>?S. \<bar>content k\<bar> * norm (f x))"
+          unfolding norm_scaleR apply(rule setsum_mono_zero_left)
+          apply(subst *, rule finite_imageI) apply fact unfolding p'alt apply blast
+          apply safe apply(rule_tac x=x in exI,rule_tac x=i in exI,rule_tac x=l in exI) by auto
+        also have "... = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))" unfolding *
+          apply(subst setsum_reindex_nonzero,fact) unfolding split_paired_all
+          unfolding  o_def split_def snd_conv fst_conv mem_Sigma_iff Pair_eq apply(erule_tac conjE)+
+        proof- fix x1 l1 k1 x2 l2 k2 assume as:"(x1,l1)\<in>p" "(x2,l2)\<in>p" "k1\<in>d" "k2\<in>d"
+            "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)"
+          from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this
+          from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2" by auto
+          hence "(interior(k1) \<inter> interior(k2) = {} \<or> interior(l1) \<inter> interior(l2) = {})" 
+            apply-apply(erule disjE) apply(rule disjI2) defer apply(rule disjI1)
+            apply(rule d'(5)[OF as(3-4)],assumption) apply(rule p'(5)[OF as(1-2)]) by auto
+          moreover have "interior(l1 \<inter> k1) = interior(l2 \<inter> k2)" unfolding  as ..
+          ultimately have "interior (l1 \<inter> k1) = {}" by auto
+          thus "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0" unfolding uv inter_interval
+            unfolding content_eq_0_interior[THEN sym] by auto
+        qed safe also have "... = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))" unfolding Sigma_alt
+          apply(subst sum_sum_product[THEN sym]) apply(rule p', rule,rule d')
+          apply(rule setsum_cong2) unfolding split_paired_all split_conv
+        proof- fix x l assume as:"(x,l)\<in>p"
+          note xl = p'(2-4)[OF this] from this(3) guess u v apply-by(erule exE)+ note uv=this
+          have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> {u..v}))"
+            apply(rule setsum_cong2) apply(drule d'(4),safe) apply(subst Int_commute)
+            unfolding inter_interval uv apply(subst abs_of_nonneg) by auto
+          also have "... = setsum content {k\<inter>{u..v}| k. k\<in>d}" unfolding simple_image
+            apply(rule setsum_reindex_nonzero[unfolded o_def,THEN sym]) apply(rule d')
+          proof- case goal1 from d'(4)[OF this(1)] d'(4)[OF this(2)]
+            guess u1 v1 u2 v2 apply- by(erule exE)+ note uv=this
+            have "{} = interior ((k \<inter> y) \<inter> {u..v})" apply(subst interior_inter)
+              using d'(5)[OF goal1(1-3)] by auto
+            also have "... = interior (y \<inter> (k \<inter> {u..v}))" by auto
+            also have "... = interior (k \<inter> {u..v})" unfolding goal1(4) by auto
+            finally show ?case unfolding uv inter_interval content_eq_0_interior ..
+          qed also have "... = setsum content {{u..v} \<inter> k |k. k \<in> d \<and> ~({u..v} \<inter> k = {})}"
+            apply(rule setsum_mono_zero_right) unfolding simple_image
+            apply(rule finite_imageI,rule d') apply blast apply safe
+            apply(rule_tac x=k in exI)
+          proof- case goal1 from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this
+            have "interior (k \<inter> {u..v}) \<noteq> {}" using goal1(2)
+              unfolding ab inter_interval content_eq_0_interior by auto
+            thus ?case using goal1(1) using interior_subset[of "k \<inter> {u..v}"] by auto
+          qed finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
+            unfolding setsum_left_distrib[THEN sym] real_scaleR_def apply -
+            apply(subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
+            using xl(2)[unfolded uv] unfolding uv by auto
+        qed finally show ?case . 
+      qed qed qed qed 
+
+lemma bounded_variation_absolutely_integrable:  fixes f::"real^'n \<Rightarrow> real^'m"
+  assumes "f integrable_on UNIV" "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
+  shows "f absolutely_integrable_on UNIV"
+proof(rule absolutely_integrable_onI,fact,rule)
+  let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of  (\<Union>d)}" def i \<equiv> "Sup ?S"
+  have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup)
+    apply(rule elementary_interval) defer apply(rule_tac x=B in exI)
+    apply(rule setleI) using assms(2) by auto
+  have f_int:"\<And>a b. f absolutely_integrable_on {a..b}"
+    apply(rule bounded_variation_absolutely_integrable_interval[where B=B])
+    apply(rule integrable_on_subinterval[OF assms(1)]) defer apply safe
+    apply(rule assms(2)[rule_format]) by auto 
+  show "((\<lambda>x. norm (f x)) has_integral i) UNIV" apply(subst has_integral_alt',safe)
+  proof- case goal1 show ?case using f_int[of a b] by auto
+  next case goal2 have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> i - e"
+    proof(rule ccontr) case goal1 hence "i \<le> i - e" apply-
+        apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by auto
+      thus False using goal2 by auto
+    qed then guess K .. note * = this[unfolded image_iff not_le]
+    from this(1) guess d .. note this[unfolded mem_Collect_eq]
+    note d = this(1) *(2)[unfolded this(2)] note d'=division_ofD[OF this(1)]
+    have "bounded (\<Union>d)" by(rule elementary_bounded,fact)
+    from this[unfolded bounded_pos] guess K .. note K=conjunctD2[OF this]
+    show ?case apply(rule_tac x="K + 1" in exI,safe)
+    proof- fix a b assume ab:"ball 0 (K + 1) \<subseteq> {a..b::real^'n}"
+      have *:"\<forall>s s1. i - e < s1 \<and> s1 \<le> s \<and> s < i + e \<longrightarrow> abs(s - i) < (e::real)" by arith
+      show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - i) < e"
+        unfolding real_norm_def apply(rule *[rule_format],safe) apply(rule d(2))
+      proof- case goal1 have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
+          apply(rule setsum_mono) apply(rule absolutely_integrable_le)
+          apply(drule d'(4),safe) by(rule f_int)
+        also have "... = integral (\<Union>d) (\<lambda>x. norm(f x))" 
+          apply(rule integral_combine_division_bottomup[THEN sym])
+          apply(rule d) unfolding forall_in_division[OF d(1)] using f_int by auto
+        also have "... \<le> integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)" 
+        proof- case goal1 have "\<Union>d \<subseteq> {a..b}" apply rule apply(drule K(2)[rule_format]) 
+            apply(rule ab[unfolded subset_eq,rule_format]) by(auto simp add:dist_norm)
+          thus ?case apply- apply(subst if_P,rule) apply(rule integral_subset_le) defer
+            apply(rule integrable_on_subdivision[of _ _ _ "{a..b}"])
+            apply(rule d) using f_int[of a b] by auto
+        qed finally show ?case .
+
+      next note f = absolutely_integrable_onD[OF f_int[of a b]]
+        note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
+        have "e/2>0" using `e>0` by auto from *[OF this] guess d1 .. note d1=conjunctD2[OF this]
+        from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this
+        from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p .
+        note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
+        have *:"\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> i \<longrightarrow> abs(sf - si) < e / 2
+          \<longrightarrow> abs(sf' - di) < e / 2 \<longrightarrow> di < i + e" by arith
+        show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < i + e" apply(subst if_P,rule)
+        proof(rule *[rule_format]) 
+          show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e / 2"
+            unfolding split_def apply(rule helplemma) using d2(2)[rule_format,of p]
+            using p(1,3) unfolding tagged_division_of_def split_def by auto
+          show "abs ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral {a..b} (\<lambda>x. norm(f x))) < e / 2"
+            using d1(2)[rule_format,OF conjI[OF p(1,2)]] unfolding real_norm_def .
+          show "(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) = (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x))"
+            apply(rule setsum_cong2) unfolding split_paired_all split_conv
+            apply(drule tagged_division_ofD(4)[OF p(1)]) unfolding norm_scaleR
+            apply(subst abs_of_nonneg) by auto
+          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> i"
+            apply(subst setsum_over_tagged_division_lemma[OF p(1)]) defer apply(rule isLubD2[OF i])
+            unfolding image_iff apply(rule_tac x="snd ` p" in bexI) unfolding mem_Collect_eq defer
+            apply(rule partial_division_of_tagged_division[of _ "{a..b}"])
+            using p(1) unfolding tagged_division_of_def by auto
+        qed qed qed(insert K,auto) qed qed 
+
+lemma absolutely_integrable_restrict_univ:
+ "(\<lambda>x. if x \<in> s then f x else (0::'a::banach)) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
+  unfolding absolutely_integrable_on_def if_distrib norm_zero integrable_restrict_univ ..
+
+lemma absolutely_integrable_add[intro]: fixes f g::"real^'n \<Rightarrow> real^'m"
+  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
+  shows "(\<lambda>x. f(x) + g(x)) absolutely_integrable_on s"
+proof- let ?P = "\<And>f g::real^'n \<Rightarrow> real^'m. f absolutely_integrable_on UNIV \<Longrightarrow>
+    g absolutely_integrable_on UNIV \<Longrightarrow> (\<lambda>x. f(x) + g(x)) absolutely_integrable_on UNIV"
+  { presume as:"PROP ?P" note a = absolutely_integrable_restrict_univ[THEN sym]
+    have *:"\<And>x. (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0)
+      = (if x \<in> s then f x + g x else 0)" by auto
+    show ?thesis apply(subst a) using as[OF assms[unfolded a[of f] a[of g]]] unfolding * . }
+  fix f g::"real^'n \<Rightarrow> real^'m" assume assms:"f absolutely_integrable_on UNIV"
+    "g absolutely_integrable_on UNIV" 
+  note absolutely_integrable_bounded_variation
+  from this[OF assms(1)] this[OF assms(2)] guess B1 B2 . note B=this[rule_format]
+  show "(\<lambda>x. f(x) + g(x)) absolutely_integrable_on UNIV"
+    apply(rule bounded_variation_absolutely_integrable[of _ "B1+B2"])
+    apply(rule integrable_add) prefer 3
+  proof safe case goal1 have "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k \<and> g integrable_on k"
+      apply(drule division_ofD(4)[OF goal1]) apply safe
+      apply(rule_tac[!] integrable_on_subinterval[of _ UNIV]) using assms by auto
+    hence "(\<Sum>k\<in>d. norm (integral k (\<lambda>x. f x + g x))) \<le>
+      (\<Sum>k\<in>d. norm (integral k f)) + (\<Sum>k\<in>d. norm (integral k g))" apply-
+      unfolding setsum_addf[THEN sym] apply(rule setsum_mono)
+      apply(subst integral_add) prefer 3 apply(rule norm_triangle_ineq) by auto
+    also have "... \<le> B1 + B2" using B(1)[OF goal1] B(2)[OF goal1] by auto
+    finally show ?case .
+  qed(insert assms,auto) qed
+
+lemma absolutely_integrable_sub[intro]: fixes f g::"real^'n \<Rightarrow> real^'m"
+  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
+  shows "(\<lambda>x. f(x) - g(x)) absolutely_integrable_on s"
+  using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]]
+  unfolding group_simps .
+
+lemma absolutely_integrable_linear: fixes f::"real^'m \<Rightarrow> real^'n" and h::"real^'n \<Rightarrow> real^'p"
+  assumes "f absolutely_integrable_on s" "bounded_linear h"
+  shows "(h o f) absolutely_integrable_on s"
+proof- { presume as:"\<And>f::real^'m \<Rightarrow> real^'n. \<And>h::real^'n \<Rightarrow> real^'p. 
+    f absolutely_integrable_on UNIV \<Longrightarrow> bounded_linear h \<Longrightarrow>
+    (h o f) absolutely_integrable_on UNIV" note a = absolutely_integrable_restrict_univ[THEN sym]
+    show ?thesis apply(subst a) using as[OF assms[unfolded a[of f] a[of g]]]
+      unfolding o_def if_distrib linear_simps[OF assms(2)] . }
+  fix f::"real^'m \<Rightarrow> real^'n" and h::"real^'n \<Rightarrow> real^'p"
+  assume assms:"f absolutely_integrable_on UNIV" "bounded_linear h" 
+  from absolutely_integrable_bounded_variation[OF assms(1)] guess B . note B=this
+  from bounded_linear.pos_bounded[OF assms(2)] guess b .. note b=conjunctD2[OF this]
+  show "(h o f) absolutely_integrable_on UNIV"
+    apply(rule bounded_variation_absolutely_integrable[of _ "B * b"])
+    apply(rule integrable_linear[OF _ assms(2)]) 
+  proof safe case goal2
+    have "(\<Sum>k\<in>d. norm (integral k (h \<circ> f))) \<le> setsum (\<lambda>k. norm(integral k f)) d * b"
+      unfolding setsum_left_distrib apply(rule setsum_mono)
+    proof- case goal1 from division_ofD(4)[OF goal2 this]
+      guess u v apply-by(erule exE)+ note uv=this
+      have *:"f integrable_on k" unfolding uv apply(rule integrable_on_subinterval[of _ UNIV])
+        using assms by auto note this[unfolded has_integral_integral]
+      note has_integral_linear[OF this assms(2)] integrable_linear[OF * assms(2)]
+      note * = has_integral_unique[OF this(2)[unfolded has_integral_integral] this(1)]
+      show ?case unfolding * using b by auto
+    qed also have "... \<le> B * b" apply(rule mult_right_mono) using B goal2 b by auto
+    finally show ?case .
+  qed(insert assms,auto) qed
+
+lemma absolutely_integrable_setsum: fixes f::"'a \<Rightarrow> real^'n \<Rightarrow> real^'m"
+  assumes "finite t" "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
+  shows "(\<lambda>x. setsum (\<lambda>a. f a x) t) absolutely_integrable_on s"
+  using assms(1,2) apply induct defer apply(subst setsum.insert) apply assumption+ by(rule,auto)
+
+lemma absolutely_integrable_vector_abs:
+  assumes "f absolutely_integrable_on s"
+  shows "(\<lambda>x. (\<chi> i. abs(f x$i))::real^'n) absolutely_integrable_on s"
+proof- have *:"\<And>x. ((\<chi> i. abs(f x$i))::real^'n) = (setsum (\<lambda>i.
+    (((\<lambda>y. (\<chi> j. if j = i then y$1 else 0)) o
+    (vec1 o ((\<lambda>x. (norm((\<chi> j. if j = i then x$i else 0)::real^'n))) o f))) x)) UNIV)"
+    unfolding Cart_eq setsum_component Cart_lambda_beta
+  proof case goal1 have *:"\<And>i xa. ((if i = xa then f x $ xa else 0) \<bullet> (if i = xa then f x $ xa else 0)) =
+      (if i = xa then (f x $ xa) * (f x $ xa) else 0)" by auto
+    have "\<bar>f x $ i\<bar> = (setsum (\<lambda>k. if k = i then abs ((f x)$i) else 0) UNIV)"
+      unfolding setsum_delta[OF finite_UNIV] by auto
+    also have "... = (\<Sum>xa\<in>UNIV. ((\<lambda>y. \<chi> j. if j = xa then dest_vec1 y else 0) \<circ>
+                      (\<lambda>x. vec1 (norm (\<chi> j. if j = xa then x $ xa else 0))) \<circ> f) x $ i)"
+      unfolding norm_eq_sqrt_inner inner_vector_def Cart_lambda_beta o_def *
+      apply(rule setsum_cong2) unfolding setsum_delta[OF finite_UNIV] by auto 
+    finally show ?case unfolding o_def . qed
+  show ?thesis unfolding * apply(rule absolutely_integrable_setsum) apply(rule finite_UNIV)
+    apply(rule absolutely_integrable_linear) 
+    unfolding absolutely_integrable_on_trans unfolding o_def apply(rule absolutely_integrable_norm)
+    apply(rule absolutely_integrable_linear[OF assms,unfolded o_def]) unfolding linear_linear
+    apply(rule_tac[!] linearI) unfolding Cart_eq by auto
+qed
+
+lemma absolutely_integrable_max: fixes f::"real^'m \<Rightarrow> real^'n"
+  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
+  shows "(\<lambda>x. (\<chi> i. max (f(x)$i) (g(x)$i))::real^'n) absolutely_integrable_on s"
+proof- have *:"\<And>x. (1 / 2) *\<^sub>R ((\<chi> i. \<bar>(f x - g x) $ i\<bar>) + (f x + g x)) = (\<chi> i. max (f(x)$i) (g(x)$i))"
+    unfolding Cart_eq by auto
+  note absolutely_integrable_sub[OF assms] absolutely_integrable_add[OF assms]
+  note absolutely_integrable_vector_abs[OF this(1)] this(2)
+  note absolutely_integrable_add[OF this] note absolutely_integrable_cmul[OF this,of "1/2"]
+  thus ?thesis unfolding * . qed
+
+lemma absolutely_integrable_max_real: fixes f::"real^'m \<Rightarrow> real"
+  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
+  shows "(\<lambda>x. max (f x) (g x)) absolutely_integrable_on s"
+proof- have *:"(\<lambda>x. \<chi> i. max ((vec1 \<circ> f) x $ i) ((vec1 \<circ> g) x $ i)) = vec1 o (\<lambda>x. max (f x) (g x))"
+    apply rule unfolding Cart_eq by auto note absolutely_integrable_max[of "vec1 o f" s "vec1 o g"]
+  note this[unfolded absolutely_integrable_on_trans,OF assms]
+  thus ?thesis unfolding * by auto qed
+
+lemma absolutely_integrable_min: fixes f::"real^'m \<Rightarrow> real^'n"
+  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
+  shows "(\<lambda>x. (\<chi> i. min (f(x)$i) (g(x)$i))::real^'n) absolutely_integrable_on s"
+proof- have *:"\<And>x. (1 / 2) *\<^sub>R ((f x + g x) - (\<chi> i. \<bar>(f x - g x) $ i\<bar>)) = (\<chi> i. min (f(x)$i) (g(x)$i))"
+    unfolding Cart_eq by auto
+  note absolutely_integrable_add[OF assms] absolutely_integrable_sub[OF assms]
+  note this(1) absolutely_integrable_vector_abs[OF this(2)]
+  note absolutely_integrable_sub[OF this] note absolutely_integrable_cmul[OF this,of "1/2"]
+  thus ?thesis unfolding * . qed
+
+lemma absolutely_integrable_min_real: fixes f::"real^'m \<Rightarrow> real"
+  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
+  shows "(\<lambda>x. min (f x) (g x)) absolutely_integrable_on s"
+proof- have *:"(\<lambda>x. \<chi> i. min ((vec1 \<circ> f) x $ i) ((vec1 \<circ> g) x $ i)) = vec1 o (\<lambda>x. min (f x) (g x))"
+    apply rule unfolding Cart_eq by auto note absolutely_integrable_min[of "vec1 o f" s "vec1 o g"]
+  note this[unfolded absolutely_integrable_on_trans,OF assms]
+  thus ?thesis unfolding * by auto qed
+
+lemma absolutely_integrable_abs_eq: fixes f::"real^'n \<Rightarrow> real^'m"
+  shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and>
+          (\<lambda>x. (\<chi> i. abs(f x$i))::real^'m) integrable_on s" (is "?l = ?r")
+proof assume ?l thus ?r apply-apply rule defer
+    apply(drule absolutely_integrable_vector_abs) by auto
+next assume ?r { presume lem:"\<And>f::real^'n \<Rightarrow> real^'m. f integrable_on UNIV \<Longrightarrow>
+    (\<lambda>x. (\<chi> i. abs(f(x)$i))::real^'m) integrable_on UNIV \<Longrightarrow> f absolutely_integrable_on UNIV"
+    have *:"\<And>x. (\<chi> i. \<bar>(if x \<in> s then f x else 0) $ i\<bar>) = (if x\<in>s then (\<chi> i. \<bar>f x $ i\<bar>) else 0)"
+      unfolding Cart_eq by auto
+    show ?l apply(subst absolutely_integrable_restrict_univ[THEN sym]) apply(rule lem)
+      unfolding integrable_restrict_univ * using `?r` by auto }
+  fix f::"real^'n \<Rightarrow> real^'m" assume assms:"f integrable_on UNIV"
+    "(\<lambda>x. (\<chi> i. abs(f(x)$i))::real^'m) integrable_on UNIV"
+  let ?B = "setsum (\<lambda>i. integral UNIV (\<lambda>x. (\<chi> j. abs(f x$j)) ::real^'m) $ i) UNIV"
+  show "f absolutely_integrable_on UNIV"
+    apply(rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"],safe)
+  proof- case goal1 note d=this and d'=division_ofD[OF this]
+    have "(\<Sum>k\<in>d. norm (integral k f)) \<le>
+      (\<Sum>k\<in>d. setsum (op $ (integral k (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>))) UNIV)" apply(rule setsum_mono)
+      apply(rule order_trans[OF norm_le_l1],rule setsum_mono)
+    proof- fix k and i::'m assume "k\<in>d"
+      from d'(4)[OF this] guess a b apply-by(erule exE)+ note ab=this
+      show "\<bar>integral k f $ i\<bar> \<le> integral k (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) $ i" apply(rule abs_leI)
+        unfolding vector_uminus_component[THEN sym] defer apply(subst integral_neg[THEN sym])
+        defer apply(rule_tac[1-2] integral_component_le) apply(rule integrable_neg)
+        using integrable_on_subinterval[OF assms(1),of a b]
+          integrable_on_subinterval[OF assms(2),of a b] unfolding ab by auto
+    qed also have "... \<le> setsum (op $ (integral UNIV (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>))) UNIV"
+      apply(subst setsum_commute,rule setsum_mono)
+    proof- case goal1 have *:"(\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) integrable_on \<Union>d"
+        using integrable_on_subdivision[OF d assms(2)] by auto
+      have "(\<Sum>i\<in>d. integral i (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) $ j)
+        = integral (\<Union>d) (\<lambda>x. (\<chi> j. abs(f x$j)) ::real^'m) $ j"
+        unfolding setsum_component[THEN sym]
+        apply(subst integral_combine_division_topdown[THEN sym,OF * d]) by auto
+      also have "... \<le> integral UNIV (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) $ j"
+        apply(rule integral_subset_component_le) using assms * by auto
+      finally show ?case .
+    qed finally show ?case . qed qed
+
+lemma nonnegative_absolutely_integrable: fixes f::"real^'n \<Rightarrow> real^'m"
+  assumes "\<forall>x\<in>s. \<forall>i. 0 \<le> f(x)$i" "f integrable_on s"
+  shows "f absolutely_integrable_on s"
+  unfolding absolutely_integrable_abs_eq apply rule defer
+  apply(rule integrable_eq[of _ f]) unfolding Cart_eq using assms by auto
+
+lemma absolutely_integrable_integrable_bound: fixes f::"real^'n \<Rightarrow> real^'m"
+  assumes "\<forall>x\<in>s. norm(f x) \<le> g x" "f integrable_on s" "g integrable_on s"
+  shows "f absolutely_integrable_on s"
+proof- { presume *:"\<And>f::real^'n \<Rightarrow> real^'m. \<And> g. \<forall>x. norm(f x) \<le> g x \<Longrightarrow> f integrable_on UNIV
+    \<Longrightarrow> g integrable_on UNIV \<Longrightarrow> f absolutely_integrable_on UNIV"
+    show ?thesis apply(subst absolutely_integrable_restrict_univ[THEN sym])
+      apply(rule *[of _ "\<lambda>x. if x\<in>s then g x else 0"])
+      using assms unfolding integrable_restrict_univ by auto }
+  fix g and f :: "real^'n \<Rightarrow> real^'m"
+  assume assms:"\<forall>x. norm(f x) \<le> g x" "f integrable_on UNIV" "g integrable_on UNIV"
+  show "f absolutely_integrable_on UNIV"
+    apply(rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"])
+  proof safe case goal1 note d=this and d'=division_ofD[OF this]
+    have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>k\<in>d. integral k g)"
+      apply(rule setsum_mono) apply(rule integral_norm_bound_integral) apply(drule_tac[!] d'(4),safe) 
+      apply(rule_tac[1-2] integrable_on_subinterval) using assms by auto
+    also have "... = integral (\<Union>d) g" apply(rule integral_combine_division_bottomup[THEN sym])
+      apply(rule d,safe) apply(drule d'(4),safe)
+      apply(rule integrable_on_subinterval[OF assms(3)]) by auto
+    also have "... \<le> integral UNIV g" apply(rule integral_subset_le) defer
+      apply(rule integrable_on_subdivision[OF d,of _ UNIV]) prefer 4
+      apply(rule,rule_tac y="norm (f x)" in order_trans) using assms by auto
+    finally show ?case . qed qed
+
+lemma absolutely_integrable_integrable_bound_real: fixes f::"real^'n \<Rightarrow> real"
+  assumes "\<forall>x\<in>s. norm(f x) \<le> g x" "f integrable_on s" "g integrable_on s"
+  shows "f absolutely_integrable_on s"
+  apply(subst absolutely_integrable_on_trans[THEN sym])
+  apply(rule absolutely_integrable_integrable_bound[where g=g])
+  using assms unfolding o_def by auto
+
+lemma absolutely_integrable_absolutely_integrable_bound:
+  fixes f::"real^'n \<Rightarrow> real^'m" and g::"real^'n \<Rightarrow> real^'p"
+  assumes "\<forall>x\<in>s. norm(f x) \<le> norm(g x)" "f integrable_on s" "g absolutely_integrable_on s"
+  shows "f absolutely_integrable_on s"
+  apply(rule absolutely_integrable_integrable_bound[of s f "\<lambda>x. norm (g x)"])
+  using assms by auto
+
+lemma absolutely_integrable_inf_real:
+  assumes "finite k" "k \<noteq> {}"
+  "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
+  shows "(\<lambda>x. (Inf ((fs x) ` k))) absolutely_integrable_on s" using assms
+proof induct case (insert a k) let ?P = " (\<lambda>x. if fs x ` k = {} then fs x a
+         else min (fs x a) (Inf (fs x ` k))) absolutely_integrable_on s"
+  show ?case unfolding image_insert
+    apply(subst Inf_insert_finite) apply(rule finite_imageI[OF insert(1)])
+  proof(cases "k={}") case True
+    thus ?P apply(subst if_P) defer apply(rule insert(5)[rule_format]) by auto
+  next case False thus ?P apply(subst if_not_P) defer
+      apply(rule absolutely_integrable_min_real) 
+      defer apply(rule insert(3)[OF False]) using insert(5) by auto
+  qed qed auto
+
+lemma absolutely_integrable_sup_real:
+  assumes "finite k" "k \<noteq> {}"
+  "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
+  shows "(\<lambda>x. (Sup ((fs x) ` k))) absolutely_integrable_on s" using assms
+proof induct case (insert a k) let ?P = " (\<lambda>x. if fs x ` k = {} then fs x a
+         else max (fs x a) (Sup (fs x ` k))) absolutely_integrable_on s"
+  show ?case unfolding image_insert
+    apply(subst Sup_insert_finite) apply(rule finite_imageI[OF insert(1)])
+  proof(cases "k={}") case True
+    thus ?P apply(subst if_P) defer apply(rule insert(5)[rule_format]) by auto
+  next case False thus ?P apply(subst if_not_P) defer
+      apply(rule absolutely_integrable_max_real) 
+      defer apply(rule insert(3)[OF False]) using insert(5) by auto
+  qed qed auto
+
+subsection {* Dominated convergence. *}
+
+lemma dominated_convergence: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real"
+  assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
+  "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
+  "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
+  shows "g integrable_on s" "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+proof- have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
+    ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
+    integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
+  proof(rule monotone_convergence_decreasing_real,safe) fix m::nat
+    show "bounded {integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) |k. True}"
+      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
+    proof safe fix k::nat
+      show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
+        apply(rule integral_norm_bound_integral) unfolding simple_image
+        apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_inf_real)
+        prefer 5 unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge)
+        prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real)
+        using assms unfolding real_norm_def by auto
+    qed fix k::nat show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
+      unfolding simple_image apply(rule absolutely_integrable_onD)
+      apply(rule absolutely_integrable_inf_real) prefer 3 
+      using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto
+    fix x assume x:"x\<in>s" show "Inf {f j x |j. j \<in> {m..m + Suc k}}
+      \<le> Inf {f j x |j. j \<in> {m..m + k}}" apply(rule Inf_ge) unfolding setge_def
+      defer apply rule apply(subst Inf_finite_le_iff) prefer 3
+      apply(rule_tac x=xa in bexI) by auto
+    let ?S = "{f j x| j.  m \<le> j}" def i \<equiv> "Inf ?S"
+    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
+      unfolding Lim_sequentially
+    proof safe case goal1 note e=this have i:"isGlb UNIV ?S i" unfolding i_def apply(rule Inf)
+        defer apply(rule_tac x="- h x - 1" in exI) unfolding setge_def
+      proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto
+      qed auto
+
+      have "\<exists>y\<in>?S. \<not> y \<ge> i + e"
+      proof(rule ccontr) case goal1 hence "i \<ge> i + e" apply-
+          apply(rule isGlb_le_isLb[OF i]) apply(rule isLbI) unfolding setge_def by fastsimp+
+        thus False using e by auto
+      qed then guess y .. note y=this[unfolded not_le]
+      from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
+      
+      show ?case apply(rule_tac x=N in exI)
+      proof safe case goal1
+        have *:"\<And>y ix. y < i + e \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < e" by arith
+        show ?case unfolding dist_real_def apply(rule *[rule_format,OF y(2)])
+          unfolding i_def apply(rule real_le_inf_subset) prefer 3
+          apply(rule,rule isGlbD1[OF i]) prefer 3 apply(subst Inf_finite_le_iff)
+          prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto
+      qed qed qed note dec1 = conjunctD2[OF this]
+
+  have "\<And>m. (\<lambda>x. Sup {f j x |j. m \<le> j}) integrable_on s \<and>
+    ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) --->
+    integral s (\<lambda>x. Sup {f j x |j. m \<le> j})) sequentially"
+  proof(rule monotone_convergence_increasing_real,safe) fix m::nat
+    show "bounded {integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) |k. True}"
+      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
+    proof safe fix k::nat
+      show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
+        apply(rule integral_norm_bound_integral) unfolding simple_image
+        apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_sup_real)
+        prefer 5 unfolding real_norm_def apply(rule) apply(rule Sup_abs_le)
+        prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real)
+        using assms unfolding real_norm_def by auto
+    qed fix k::nat show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
+      unfolding simple_image apply(rule absolutely_integrable_onD)
+      apply(rule absolutely_integrable_sup_real) prefer 3 
+      using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto
+    fix x assume x:"x\<in>s" show "Sup {f j x |j. j \<in> {m..m + Suc k}}
+      \<ge> Sup {f j x |j. j \<in> {m..m + k}}" apply(rule Sup_le) unfolding setle_def
+      defer apply rule apply(subst Sup_finite_ge_iff) prefer 3 apply(rule_tac x=y in bexI) by auto
+    let ?S = "{f j x| j.  m \<le> j}" def i \<equiv> "Sup ?S"
+    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
+      unfolding Lim_sequentially
+    proof safe case goal1 note e=this have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup)
+        defer apply(rule_tac x="h x" in exI) unfolding setle_def
+      proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto
+      qed auto
+      
+      have "\<exists>y\<in>?S. \<not> y \<le> i - e"
+      proof(rule ccontr) case goal1 hence "i \<le> i - e" apply-
+          apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by fastsimp+
+        thus False using e by auto
+      qed then guess y .. note y=this[unfolded not_le]
+      from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
+      
+      show ?case apply(rule_tac x=N in exI)
+      proof safe case goal1
+        have *:"\<And>y ix. i - e < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < e" by arith
+        show ?case unfolding dist_real_def apply(rule *[rule_format,OF y(2)])
+          unfolding i_def apply(rule real_ge_sup_subset) prefer 3
+          apply(rule,rule isLubD1[OF i]) prefer 3 apply(subst Sup_finite_ge_iff)
+          prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto
+      qed qed qed note inc1 = conjunctD2[OF this]
+
+  have "g integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) ---> integral s g) sequentially"
+  apply(rule monotone_convergence_increasing_real,safe) apply fact 
+  proof- show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}"
+      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
+    proof safe fix k::nat
+      show "norm (integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<le> integral s h"
+        apply(rule integral_norm_bound_integral) apply fact+
+        unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge) using assms(3) by auto
+    qed fix k::nat and x assume x:"x\<in>s"
+
+    have *:"\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
+    show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}" apply-
+      apply(rule real_le_inf_subset) prefer 3 unfolding setge_def
+      apply(rule_tac x="- h x" in exI) apply safe apply(rule *)
+      using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
+    show "((\<lambda>k. Inf {f j x |j. k \<le> j}) ---> g x) sequentially" unfolding Lim_sequentially
+    proof safe case goal1 hence "0<e/2" by auto
+      from assms(4)[unfolded Lim_sequentially,rule_format,OF x this] guess N .. note N=this
+      show ?case apply(rule_tac x=N in exI,safe) unfolding dist_real_def
+        apply(rule le_less_trans[of _ "e/2"]) apply(rule Inf_asclose) apply safe
+        defer apply(rule less_imp_le) using N goal1 unfolding dist_real_def by auto
+    qed qed note inc2 = conjunctD2[OF this]
+
+  have "g integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) ---> integral s g) sequentially"
+  apply(rule monotone_convergence_decreasing_real,safe) apply fact 
+  proof- show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}"
+      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
+    proof safe fix k::nat
+      show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h"
+        apply(rule integral_norm_bound_integral) apply fact+
+        unfolding real_norm_def apply(rule) apply(rule Sup_abs_le) using assms(3) by auto
+    qed fix k::nat and x assume x:"x\<in>s"
+
+    show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}" apply-
+      apply(rule real_ge_sup_subset) prefer 3 unfolding setle_def
+      apply(rule_tac x="h x" in exI) apply safe
+      using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
+    show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially" unfolding Lim_sequentially
+    proof safe case goal1 hence "0<e/2" by auto
+      from assms(4)[unfolded Lim_sequentially,rule_format,OF x this] guess N .. note N=this
+      show ?case apply(rule_tac x=N in exI,safe) unfolding dist_real_def
+        apply(rule le_less_trans[of _ "e/2"]) apply(rule Sup_asclose) apply safe
+        defer apply(rule less_imp_le) using N goal1 unfolding dist_real_def by auto
+    qed qed note dec2 = conjunctD2[OF this]
+
+  show "g integrable_on s" by fact
+  show "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially" unfolding Lim_sequentially
+  proof safe case goal1
+    from inc2(2)[unfolded Lim_sequentially,rule_format,OF goal1] guess N1 .. note N1=this[unfolded dist_real_def]
+    from dec2(2)[unfolded Lim_sequentially,rule_format,OF goal1] guess N2 .. note N2=this[unfolded dist_real_def]
+    show ?case apply(rule_tac x="N1+N2" in exI,safe)
+    proof- fix n assume n:"n \<ge> N1 + N2"
+      have *:"\<And>i0 i i1 g. \<bar>i0 - g\<bar> < e \<longrightarrow> \<bar>i1 - g\<bar> < e \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < e" by arith
+      show "dist (integral s (f n)) (integral s g) < e" unfolding dist_real_def
+        apply(rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
+      proof- show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
+        proof(rule integral_le[OF dec1(1) assms(1)],safe) 
+          fix x assume x:"x \<in> s" have *:"\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
+          show "Inf {f j x |j. n \<le> j} \<le> f n x" apply(rule Inf_lower[where z="- h x"]) defer
+            apply(rule *) using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
+        qed show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
+        proof(rule integral_le[OF assms(1) inc1(1)],safe) 
+          fix x assume x:"x \<in> s"
+          show "f n x \<le> Sup {f j x |j. n \<le> j}" apply(rule Sup_upper[where z="h x"]) defer
+            using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
+        qed qed(insert n,auto) qed qed qed
 
 declare [[smt_certificates=""]]
+declare [[smt_fixed=false]]
 
 end
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -49,8 +49,8 @@
 val max_mutants = 4
 val num_mutations = 1
 (* soundness check: *)
-val max_mutants = 1
-val num_mutations = 0
+(*val max_mutants = 1
+val num_mutations = 0*)
 
 (* quickcheck options *)
 (*val quickcheck_generator = "SML"*)
@@ -197,7 +197,14 @@
   (@{const_name induct_conj}, "'a"),*)
   (@{const_name "undefined"}, "'a"),
   (@{const_name "default"}, "'a"),
-  (@{const_name "dummy_pattern"}, "'a::{}") (*,
+  (@{const_name "dummy_pattern"}, "'a::{}"),
+  (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
+  (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
+  (@{const_name "top_fun_inst.top_fun"}, "'a"),
+  (@{const_name "Pure.term"}, "'a"),
+  (@{const_name "top_class.top"}, "'a"),
+  (@{const_name "eq_class.eq"}, "'a"),
+  (@{const_name "Quotient.Quot_True"}, "'a")(*,
   (@{const_name "uminus"}, "'a"),
   (@{const_name "Nat.size"}, "'a"),
   (@{const_name "Groups.abs"}, "'a") *)]
@@ -219,10 +226,28 @@
     String.isSuffix "_raw" s
   end
 
+val forbidden_mutant_constnames =
+ ["HOL.induct_equal",
+  "HOL.induct_implies",
+  "HOL.induct_conj",
+ @{const_name undefined},
+ @{const_name default},
+ @{const_name dummy_pattern},
+ @{const_name "HOL.simp_implies"},
+ @{const_name "bot_fun_inst.bot_fun"},
+ @{const_name "top_fun_inst.top_fun"},
+ @{const_name "Pure.term"},
+ @{const_name "top_class.top"},
+ @{const_name "eq_class.eq"},
+ @{const_name "Quotient.Quot_True"}]
+
 fun is_forbidden_mutant t =
-  let val consts = Term.add_const_names t [] in
+  let
+    val consts = Term.add_const_names t []
+  in
     exists (String.isPrefix "Nitpick") consts orelse
-    exists (String.isSubstring "_sumC") consts (* internal function *)
+    exists (String.isSubstring "_sumC") consts orelse
+    exists (member (op =) forbidden_mutant_constnames) consts
   end
 
 fun is_executable_term thy t = can (TimeLimit.timeLimit (Time.fromMilliseconds 2000) (Quickcheck.test_term
@@ -340,6 +365,12 @@
     (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
   "\n"
 
+(* XML.tree -> string *)
+fun plain_string_from_xml_tree t =
+  Buffer.empty |> XML.add_content t |> Buffer.content
+(* string -> string *)
+val unyxml = plain_string_from_xml_tree o YXML.parse
+
 fun string_of_mutant_subentry' thy thm_name (t, results) =
   let
     fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
@@ -352,16 +383,28 @@
     fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) =
       mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^
       space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)
-      ^ "\n" ^ string_of_reports reports
+      (*^ "\n" ^ string_of_reports reports*)
   in
-    "mutant of " ^ thm_name ^ ":\n" ^ cat_lines (map string_of_mtd_result results)
+    "mutant of " ^ thm_name ^ ":\n"
+    ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ cat_lines (map string_of_mtd_result results)
   end
 
 fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
    thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
-   Syntax.string_of_term_global thy t ^ "\n" ^
+   Syntax.string_of_term_global thy t ^ "\n" ^                                    
    cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
 
+fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
+  "lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
+  "\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
+  "\" \nquickcheck[generator = SML]\nquickcheck[generator = predicate_compile_wo_ff]\n" ^
+  "quickcheck[generator = predicate_compile_ff_nofs]\noops\n"
+
+fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
+  "subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
+  cat_lines (map_index
+    (theoryfile_string_of_mutant_subentry thy thm_name) mutant_subentries) ^ "\n"
+
 (* subentry -> string *)
 fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
                          timeout, error) =
@@ -390,6 +433,8 @@
     (*for detailled report: *)
     val (gen_create_entry, gen_string_for_entry) =
       (create_detailed_entry, string_of_detailed_entry thy)
+    val (gen_create_entry, gen_string_for_entry) =
+      (create_detailed_entry, theoryfile_string_of_detailed_entry thy)
   in
     File.write path (
     "Mutation options = "  ^
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 21 14:02:34 2010 +0200
@@ -789,7 +789,6 @@
 
 code_pred [inductify, skip_proof] case_f .
 thm case_fP.equation
-thm case_fP.intros
 
 fun fold_map_idx where
   "fold_map_idx f i y [] = (y, [])"
@@ -935,10 +934,10 @@
 code_pred [inductify] avl .
 thm avl.equation*)
 
-code_pred [random_dseq inductify] avl .
-thm avl.random_dseq_equation
+code_pred [new_random_dseq inductify] avl .
+thm avl.new_random_dseq_equation
 
-values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
+values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
 
 fun set_of
 where
@@ -1392,6 +1391,100 @@
 values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
 values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}"
 
+subsection {* minus on bool *}
+
+inductive All :: "nat => bool"
+where
+  "All x"
+
+inductive None :: "nat => bool"
+
+definition "test_minus_bool x = (None x - All x)"
+
+code_pred [inductify] test_minus_bool .
+thm test_minus_bool.equation
+
+values "{x. test_minus_bool x}"
+
+subsection {* Examples for detecting switches *}
+
+inductive detect_switches1 where
+  "detect_switches1 [] []"
+| "detect_switches1 (x # xs) (y # ys)"
+
+code_pred [detect_switches, skip_proof] detect_switches1 .
+
+thm detect_switches1.equation
+
+inductive detect_switches2 :: "('a => bool) => bool"
+where
+  "detect_switches2 P"
+
+code_pred [detect_switches, skip_proof] detect_switches2 .
+thm detect_switches2.equation
+
+inductive detect_switches3 :: "('a => bool) => 'a list => bool"
+where
+  "detect_switches3 P []"
+| "detect_switches3 P (x # xs)" 
+
+code_pred [detect_switches, skip_proof] detect_switches3 .
+
+thm detect_switches3.equation
+
+inductive detect_switches4 :: "('a => bool) => 'a list => 'a list => bool"
+where
+  "detect_switches4 P [] []"
+| "detect_switches4 P (x # xs) (y # ys)"
+
+code_pred [detect_switches, skip_proof] detect_switches4 .
+thm detect_switches4.equation
+
+inductive detect_switches5 :: "('a => 'a => bool) => 'a list => 'a list => bool"
+where
+  "detect_switches5 P [] []"
+| "detect_switches5 P xs ys ==> P x y ==> detect_switches5 P (x # xs) (y # ys)"
+
+code_pred [detect_switches, skip_proof] detect_switches5 .
+
+thm detect_switches5.equation
+
+inductive detect_switches6 :: "(('a => 'b => bool) * 'a list * 'b list) => bool"
+where
+  "detect_switches6 (P, [], [])"
+| "detect_switches6 (P, xs, ys) ==> P x y ==> detect_switches6 (P, x # xs, y # ys)"
+
+code_pred [detect_switches, skip_proof] detect_switches6 .
+
+inductive detect_switches7 :: "('a => bool) => ('b => bool) => ('a * 'b list) => bool"
+where
+  "detect_switches7 P Q (a, [])"
+| "P a ==> Q x ==> detect_switches7 P Q (a, x#xs)"
+
+code_pred [skip_proof] detect_switches7 .
+
+thm detect_switches7.equation
+
+inductive detect_switches8 :: "nat => bool"
+where
+  "detect_switches8 0"
+| "x mod 2 = 0 ==> detect_switches8 (Suc x)"
+
+code_pred [detect_switches, skip_proof] detect_switches8 .
+
+thm detect_switches8.equation
+
+inductive detect_switches9 :: "nat => nat => bool"
+where
+  "detect_switches9 0 0"
+| "detect_switches9 0 (Suc x)"
+| "detect_switches9 (Suc x) 0"
+| "x = y ==> detect_switches9 (Suc x) (Suc y)"
+| "c1 = c2 ==> detect_switches9 c1 c2"
+
+code_pred [detect_switches, skip_proof] detect_switches9 .
+
+thm detect_switches9.equation
 
 
 
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Apr 21 14:02:34 2010 +0200
@@ -12,7 +12,7 @@
 definition
   "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
 
-code_pred (expected_modes: i => bool) [inductify] greater_than_index .
+code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
 ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
 
 thm greater_than_index.equation
@@ -38,7 +38,7 @@
 
 text {* In this example, max is specialised, hence the mode o => i => bool is possible *}
 
-code_pred (modes: o => i => bool) [inductify] max_of_my_Suc .
+code_pred (modes: o => i => bool) [inductify, specialise, skip_proof] max_of_my_Suc .
 
 thm max_of_my_SucP.equation
 
@@ -218,7 +218,7 @@
     \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
 | T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
 
-code_pred [inductify, skip_proof] typing .
+code_pred [inductify, skip_proof, specialise] typing .
 
 thm typing.equation
 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -18,17 +18,9 @@
 val present_graph = Unsynchronized.ref false
 
 val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref
-  
 
 open Predicate_Compile_Aux;
 
-(* Some last processing *)
-
-fun remove_pointless_clauses intro =
-  if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
-    []
-  else [intro]
-
 fun print_intross options thy msg intross =
   if show_intermediate_results options then
     tracing (msg ^ 
@@ -120,10 +112,15 @@
       val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7
       val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())
       val _ = print_step options ("Looking for specialisations in " ^ commas (map fst intross8) ^ "...")
-      val (intross9, thy3) = Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
-      val _ = print_intross options thy3 "introduction rules before registering: " intross9
+      val (intross9, thy3) =
+        if specialise options then
+          Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
+        else (intross8, thy2)
+      val _ = print_intross options thy3 "introduction rules after specialisations: " intross9
+      val intross10 = map_specs (map_filter (peephole_optimisation thy3)) intross9
+      val _ = print_intross options thy3 "introduction rules before registering: " intross10
       val _ = print_step options "Registering introduction rules..."
-      val thy4 = fold Predicate_Compile_Core.register_intros intross9 thy3
+      val thy4 = fold Predicate_Compile_Core.register_intros intross10 thy3
     in
       thy4
     end;
@@ -160,10 +157,12 @@
       show_caught_failures = false,
       skip_proof = chk "skip_proof",
       function_flattening = not (chk "no_function_flattening"),
+      specialise = chk "specialise",
       fail_safe_function_flattening = false,
       no_topmost_reordering = (chk "no_topmost_reordering"),
       no_higher_order_predicate = [],
       inductify = chk "inductify",
+      detect_switches = chk "detect_switches",
       compilation = compilation
     }
   end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -38,6 +38,8 @@
   (* premises *)
   datatype indprem = Prem of term | Negprem of term | Sidecond of term
     | Generator of (string * typ)
+  val dest_indprem : indprem -> term
+  val map_indprem : (term -> term) -> indprem -> indprem
   (* general syntactic functions *)
   val conjuncts : term -> term list
   val is_equationlike : thm -> bool
@@ -107,8 +109,10 @@
     no_topmost_reordering : bool,
     function_flattening : bool,
     fail_safe_function_flattening : bool,
+    specialise : bool,
     no_higher_order_predicate : string list,
     inductify : bool,
+    detect_switches : bool,
     compilation : compilation
   };
   val expected_modes : options -> (string * mode list) option
@@ -125,8 +129,10 @@
   val no_topmost_reordering : options -> bool
   val function_flattening : options -> bool
   val fail_safe_function_flattening : options -> bool
+  val specialise : options -> bool
   val no_higher_order_predicate : options -> string list
   val is_inductify : options -> bool
+  val detect_switches : options -> bool
   val compilation : options -> compilation
   val default_options : options
   val bool_options : string list
@@ -135,6 +141,8 @@
   val expand_tuples : theory -> thm -> thm
   val eta_contract_ho_arguments : theory -> thm -> thm
   val remove_equalities : theory -> thm -> thm
+  val remove_pointless_clauses : thm -> thm list
+  val peephole_optimisation : theory -> thm -> thm option
 end;
 
 structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
@@ -384,6 +392,16 @@
 datatype indprem = Prem of term | Negprem of term | Sidecond of term
   | Generator of (string * typ);
 
+fun dest_indprem (Prem t) = t
+  | dest_indprem (Negprem t) = t
+  | dest_indprem (Sidecond t) = t
+  | dest_indprem (Generator _) = raise Fail "cannot destruct generator"
+
+fun map_indprem f (Prem t) = Prem (f t)
+  | map_indprem f (Negprem t) = Negprem (f t)
+  | map_indprem f (Sidecond t) = Sidecond (f t)
+  | map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T))))
+
 (* general syntactic functions *)
 
 (*Like dest_conj, but flattens conjunctions however nested*)
@@ -513,6 +531,20 @@
     (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
   end;
 
+fun map_premises f intro =
+  let
+    val (premises, head) = Logic.strip_horn intro
+  in
+    Logic.list_implies (map f premises, head)
+  end
+
+fun map_filter_premises f intro =
+  let
+    val (premises, head) = Logic.strip_horn intro
+  in
+    Logic.list_implies (map_filter f premises, head)
+  end
+
 fun maps_premises f intro =
   let
     val (premises, head) = Logic.strip_horn intro
@@ -649,9 +681,11 @@
   skip_proof : bool,
   no_topmost_reordering : bool,
   function_flattening : bool,
+  specialise : bool,
   fail_safe_function_flattening : bool,
   no_higher_order_predicate : string list,
   inductify : bool,
+  detect_switches : bool,
   compilation : compilation
 };
 
@@ -672,6 +706,7 @@
 
 fun function_flattening (Options opt) = #function_flattening opt
 fun fail_safe_function_flattening (Options opt) = #fail_safe_function_flattening opt
+fun specialise (Options opt) = #specialise opt
 fun no_topmost_reordering (Options opt) = #no_topmost_reordering opt
 fun no_higher_order_predicate (Options opt) = #no_higher_order_predicate opt
 
@@ -679,6 +714,8 @@
 
 fun compilation (Options opt) = #compilation opt
 
+fun detect_switches (Options opt) = #detect_switches opt
+
 val default_options = Options {
   expected_modes = NONE,
   proposed_modes = NONE,
@@ -693,15 +730,17 @@
   skip_proof = true,
   no_topmost_reordering = false,
   function_flattening = false,
+  specialise = false,
   fail_safe_function_flattening = false,
   no_higher_order_predicate = [],
   inductify = false,
+  detect_switches = true,
   compilation = Pred
 }
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
   "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
-  "no_topmost_reordering"]
+  "detect_switches", "specialise", "no_topmost_reordering"]
 
 fun print_step options s =
   if show_steps options then tracing s else ()
@@ -810,4 +849,25 @@
     map_term thy remove_eqs intro
   end
 
+(* Some last processing *)
+
+fun remove_pointless_clauses intro =
+  if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
+    []
+  else [intro]
+
+(* some peephole optimisations *)
+
+fun peephole_optimisation thy intro =
+  let
+    val process = MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init thy))
+    fun process_False intro_t =
+      if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
+    fun process_True intro_t =
+      map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t
+  in
+    Option.map (Skip_Proof.make_thm thy)
+      (process_False (process_True (prop_of (process intro))))
+  end
+
 end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -1251,10 +1251,6 @@
   | rev_option_ord ord (SOME _, NONE) = LESS
   | rev_option_ord ord (SOME x, SOME y) = ord (x, y)
 
-fun term_of_prem (Prem t) = t
-  | term_of_prem (Negprem t) = t
-  | term_of_prem (Sidecond t) = t
-
 fun random_mode_in_deriv modes t deriv =
   case try dest_Const (fst (strip_comb t)) of
     SOME (s, _) =>
@@ -1282,8 +1278,28 @@
     EQUAL => ord2 (x, x')
   | ord => ord
 
-fun deriv_ord2' thy pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
+fun lexl_ord [] (x, x') = EQUAL
+  | lexl_ord (ord :: ords') (x, x') =
+    case ord (x, x') of
+      EQUAL => lexl_ord ords' (x, x')
+    | ord => ord
+
+fun deriv_ord' thy pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
   let
+    (* prefer functional modes if it is a function *)
+    fun fun_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+      let
+        fun is_functional t mode =
+          case try (fst o dest_Const o fst o strip_comb) t of
+            NONE => false
+          | SOME c => is_some (alternative_compilation_of thy c mode)
+      in
+        case (is_functional t1 (head_mode_of deriv1), is_functional t2 (head_mode_of deriv2)) of
+          (true, true) => EQUAL
+        | (true, false) => LESS
+        | (false, true) => GREATER
+        | (false, false) => EQUAL
+      end
     (* prefer modes without requirement for generating random values *)
     fun mvars_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
       int_ord (length mvars1, length mvars2)
@@ -1301,18 +1317,15 @@
     fun recursive_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
       int_ord (if is_rec_premise t1 then 0 else 1,
         if is_rec_premise t2 then 0 else 1)
-    val ord = lex_ord mvars_ord (lex_ord random_mode_ord (lex_ord output_mode_ord recursive_ord))
+    val ord = lexl_ord [mvars_ord, fun_ord, random_mode_ord, output_mode_ord, recursive_ord]
   in
     ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2))
   end
 
-fun deriv_ord2 thy pred modes t = deriv_ord2' thy pred modes t t
+fun deriv_ord thy pol pred modes t = deriv_ord' thy pol pred modes t t
 
-fun deriv_ord ((deriv1, mvars1), (deriv2, mvars2)) =
-  int_ord (length mvars1, length mvars2)
-
-fun premise_ord thy pred modes ((prem1, a1), (prem2, a2)) =
-  rev_option_ord (deriv_ord2' thy pred modes (term_of_prem prem1) (term_of_prem prem2)) (a1, a2)
+fun premise_ord thy pol pred modes ((prem1, a1), (prem2, a2)) =
+  rev_option_ord (deriv_ord' thy pol pred modes (dest_indprem prem1) (dest_indprem prem2)) (a1, a2)
 
 fun print_mode_list modes =
   tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
@@ -1322,15 +1335,16 @@
   pol (modes, (pos_modes, neg_modes)) vs ps =
   let
     fun choose_mode_of_prem (Prem t) = partial_hd
-        (sort (deriv_ord2 thy pred modes t) (all_derivations_of thy pos_modes vs t))
+        (sort (deriv_ord thy pol pred modes t) (all_derivations_of thy pos_modes vs t))
       | choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
       | choose_mode_of_prem (Negprem t) = partial_hd
-          (sort (deriv_ord2 thy pred modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
+          (sort (deriv_ord thy (not pol) pred modes t)
+          (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
              (all_derivations_of thy neg_modes vs t)))
       | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem thy p)
   in
     if #reorder_premises mode_analysis_options then
-      partial_hd (sort (premise_ord thy pred modes) (ps ~~ map choose_mode_of_prem ps))
+      partial_hd (sort (premise_ord thy pol pred modes) (ps ~~ map choose_mode_of_prem ps))
     else
       SOME (hd ps, choose_mode_of_prem (hd ps))
   end
@@ -1338,7 +1352,7 @@
 fun check_mode_clause' (mode_analysis_options : mode_analysis_options) thy pred param_vs (modes :
   (string * ((bool * mode) * bool) list) list) ((pol, mode) : bool * mode) (ts, ps) =
   let
-    val vTs = distinct (op =) (fold Term.add_frees (map term_of_prem ps) (fold Term.add_frees ts []))
+    val vTs = distinct (op =) (fold Term.add_frees (map dest_indprem ps) (fold Term.add_frees ts []))
     val modes' = modes @ (param_vs ~~ map (fn x => [((true, x), false), ((false, x), false)]) (ho_arg_modes_of mode))
     fun retrieve_modes_of_pol pol = map (fn (s, ms) =>
       (s, map_filter (fn ((p, m), r) => if p = pol then SOME m else NONE | _ => NONE) ms))
@@ -1464,13 +1478,26 @@
     val prednames = map fst preds
     (* extramodes contains all modes of all constants, should we only use the necessary ones
        - what is the impact on performance? *)
+    fun predname_of (Prem t) =
+        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
+      | predname_of (Negprem t) =
+        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
+      | predname_of _ = I
+    val relevant_prednames = fold (fn (_, clauses') =>
+      fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
     val extra_modes =
       if #infer_pos_and_neg_modes mode_analysis_options then
         let
           val pos_extra_modes =
-            all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name)
+            map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
+            relevant_prednames
+            (* all_modes_of compilation thy *)
+            |> filter_out (fn (name, _) => member (op =) prednames name)
           val neg_extra_modes =
-            all_modes_of (negative_compilation_of compilation) thy
+          map_filter (fn name => Option.map (pair name)
+            (try (modes_of (negative_compilation_of compilation) thy) name))
+            relevant_prednames
+          (*all_modes_of (negative_compilation_of compilation) thy*)
             |> filter_out (fn (name, _) => member (op =) prednames name)
         in
           map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
@@ -1479,7 +1506,10 @@
         end
       else
         map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)))
-          (all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name))
+          (map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
+            relevant_prednames
+          (*all_modes_of compilation thy*)
+          |> filter_out (fn (name, _) => member (op =) prednames name))
     val _ = print_extra_modes options extra_modes
     val start_modes =
       if #infer_pos_and_neg_modes mode_analysis_options then
@@ -1504,7 +1534,6 @@
     val thy' = fold (fn (s, ms) => if member (op =) (map fst preds) s then
       set_needs_random s (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms) else I)
       modes thy
-
   in
     ((moded_clauses, errors), thy')
   end;
@@ -1608,7 +1637,7 @@
     val name' = Name.variant (name :: names) "y";
     val T = HOLogic.mk_tupleT (map fastype_of out_ts);
     val U = fastype_of success_t;
-    val U' = dest_predT compfuns U;        
+    val U' = dest_predT compfuns U;
     val v = Free (name, T);
     val v' = Free (name', T);
   in
@@ -1668,13 +1697,12 @@
   end
 
 fun compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments
-  mode inp (ts, moded_ps) =
+  mode inp (in_ts, out_ts) moded_ps =
   let
     val compfuns = Comp_Mod.compfuns compilation_modifiers
-    val iss = ho_arg_modes_of mode
+    val iss = ho_arg_modes_of mode (* FIXME! *)
     val compile_match = compile_match compilation_modifiers
       additional_arguments param_vs iss ctxt
-    val (in_ts, out_ts) = split_mode mode ts;
     val (in_ts', (all_vs', eqs)) =
       fold_map (collect_non_invertible_subterms ctxt) in_ts (all_vs, []);
     fun compile_prems out_ts' vs names [] =
@@ -1742,7 +1770,171 @@
     mk_bind compfuns (mk_single compfuns inp, prem_t)
   end
 
-fun compile_pred compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
+(* switch detection *)
+
+(** argument position of an inductive predicates and the executable functions **)
+
+type position = int * int list
+
+fun input_positions_pair Input = [[]]
+  | input_positions_pair Output = []
+  | input_positions_pair (Fun _) = []
+  | input_positions_pair (Pair (m1, m2)) =
+    map (cons 1) (input_positions_pair m1) @ map (cons 2) (input_positions_pair m2)
+
+fun input_positions_of_mode mode = flat (map_index
+   (fn (i, Input) => [(i, [])]
+   | (_, Output) => []
+   | (_, Fun _) => []
+   | (i, m as Pair (m1, m2)) => map (pair i) (input_positions_pair m))
+     (Predicate_Compile_Aux.strip_fun_mode mode))
+
+fun argument_position_pair mode [] = []
+  | argument_position_pair (Pair (Fun _, m2)) (2 :: is) = argument_position_pair m2 is
+  | argument_position_pair (Pair (m1, m2)) (i :: is) =
+    (if eq_mode (m1, Output) andalso i = 2 then
+      argument_position_pair m2 is
+    else if eq_mode (m2, Output) andalso i = 1 then
+      argument_position_pair m1 is
+    else (i :: argument_position_pair (if i = 1 then m1 else m2) is))
+
+fun argument_position_of mode (i, is) =
+  (i - (length (filter (fn Output => true | Fun _ => true | _ => false)
+    (List.take (strip_fun_mode mode, i)))),
+  argument_position_pair (nth (strip_fun_mode mode) i) is)
+
+fun nth_pair [] t = t
+  | nth_pair (1 :: is) (Const (@{const_name Pair}, _) $ t1 $ _) = nth_pair is t1
+  | nth_pair (2 :: is) (Const (@{const_name Pair}, _) $ _ $ t2) = nth_pair is t2
+  | nth_pair _ _ = raise Fail "unexpected input for nth_tuple"
+
+(** switch detection analysis **)
+
+fun find_switch_test thy (i, is) (ts, prems) =
+  let
+    val t = nth_pair is (nth ts i)
+    val T = fastype_of t
+  in
+    case T of
+      TFree _ => NONE
+    | Type (Tcon, _) =>
+      (case Datatype_Data.get_constrs thy Tcon of
+        NONE => NONE
+      | SOME cs =>
+        (case strip_comb t of
+          (Var _, []) => NONE
+        | (Free _, []) => NONE
+        | (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE))
+  end
+
+fun partition_clause thy pos moded_clauses =
+  let
+    fun insert_list eq (key, value) = AList.map_default eq (key, []) (cons value)
+    fun find_switch_test' moded_clause (cases, left) =
+      case find_switch_test thy pos moded_clause of
+        SOME (c, T) => (insert_list (op =) ((c, T), moded_clause) cases, left)
+      | NONE => (cases, moded_clause :: left)
+  in
+    fold find_switch_test' moded_clauses ([], [])
+  end
+
+datatype switch_tree =
+  Atom of moded_clause list | Node of (position * ((string * typ) * switch_tree) list) * switch_tree
+
+fun mk_switch_tree thy mode moded_clauses =
+  let
+    fun select_best_switch moded_clauses input_position best_switch =
+      let
+        val ord = option_ord (rev_order o int_ord o (pairself (length o snd o snd)))
+        val partition = partition_clause thy input_position moded_clauses
+        val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE
+      in
+        case ord (switch, best_switch) of LESS => best_switch
+          | EQUAL => best_switch | GREATER => switch
+      end
+    fun detect_switches moded_clauses =
+      case fold (select_best_switch moded_clauses) (input_positions_of_mode mode) NONE of
+        SOME (best_pos, (switched_on, left_clauses)) =>
+          Node ((best_pos, map (apsnd detect_switches) switched_on),
+            detect_switches left_clauses)
+      | NONE => Atom moded_clauses
+  in
+    detect_switches moded_clauses
+  end
+
+(** compilation of detected switches **)
+
+fun destruct_constructor_pattern (pat, obj) =
+  (case strip_comb pat of
+    (f as Free _, []) => cons (pat, obj)
+  | (Const (c, T), pat_args) =>
+    (case strip_comb obj of
+      (Const (c', T'), obj_args) =>
+        (if c = c' andalso T = T' then
+          fold destruct_constructor_pattern (pat_args ~~ obj_args)
+        else raise Fail "pattern and object mismatch")
+    | _ => raise Fail "unexpected object")
+  | _ => raise Fail "unexpected pattern")
+
+
+fun compile_switch compilation_modifiers ctxt all_vs param_vs additional_arguments mode
+  in_ts' outTs switch_tree =
+  let
+    val compfuns = Comp_Mod.compfuns compilation_modifiers
+    val thy = ProofContext.theory_of ctxt
+    fun compile_switch_tree _ _ (Atom []) = NONE
+      | compile_switch_tree all_vs ctxt_eqs (Atom moded_clauses) =
+        let
+          val in_ts' = map (Pattern.rewrite_term thy ctxt_eqs []) in_ts'
+          fun compile_clause' (ts, moded_ps) =
+            let
+              val (ts, out_ts) = split_mode mode ts
+              val subst = fold destruct_constructor_pattern (in_ts' ~~ ts) []
+              val (fsubst, pat') = List.partition (fn (_, Free _) => true | _ => false) subst
+              val moded_ps' = (map o apfst o map_indprem)
+                (Pattern.rewrite_term thy (map swap fsubst) []) moded_ps
+              val inp = HOLogic.mk_tuple (map fst pat')
+              val in_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) (map snd pat')
+              val out_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) out_ts
+            in
+              compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments
+                mode inp (in_ts', out_ts') moded_ps'
+            end
+        in SOME (foldr1 (mk_sup compfuns) (map compile_clause' moded_clauses)) end
+    | compile_switch_tree all_vs ctxt_eqs (Node ((position, switched_clauses), left_clauses)) =
+      let
+        val (i, is) = argument_position_of mode position
+        val inp_var = nth_pair is (nth in_ts' i)
+        val x = Name.variant all_vs "x"
+        val xt = Free (x, fastype_of inp_var)
+        fun compile_single_case ((c, T), switched) =
+          let
+            val Ts = binder_types T
+            val argnames = Name.variant_list (x :: all_vs)
+              (map (fn i => "c" ^ string_of_int i) (1 upto length Ts))
+            val args = map2 (curry Free) argnames Ts
+            val pattern = list_comb (Const (c, T), args)
+            val ctxt_eqs' = (inp_var, pattern) :: ctxt_eqs
+            val compilation = the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
+              (compile_switch_tree (argnames @ x :: all_vs) ctxt_eqs' switched)
+        in
+          (pattern, compilation)
+        end
+        val switch = fst (Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var
+          ((map compile_single_case switched_clauses) @
+            [(xt, mk_bot compfuns (HOLogic.mk_tupleT outTs))]))
+      in
+        case compile_switch_tree all_vs ctxt_eqs left_clauses of
+          NONE => SOME switch
+        | SOME left_comp => SOME (mk_sup compfuns (switch, left_comp))
+      end
+  in
+    compile_switch_tree all_vs [] switch_tree
+  end
+
+(* compilation of predicates *)
+
+fun compile_pred options compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
   let
     val ctxt = ProofContext.init thy
     val compilation_modifiers = if pol then compilation_modifiers else
@@ -1757,7 +1949,6 @@
       (binder_types T)
     val predT = mk_predT compfuns (HOLogic.mk_tupleT outTs)
     val funT = Comp_Mod.funT_of compilation_modifiers mode T
-    
     val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
       (fn T => fn (param_vs, names) =>
         if is_param_type T then
@@ -1769,14 +1960,24 @@
         (param_vs, (all_vs @ param_vs))
     val in_ts' = map_filter (map_filter_prod
       (fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
-    val cl_ts =
-      map (compile_clause compilation_modifiers
-        ctxt all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts')) moded_cls;
-    val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns
-      s T mode additional_arguments
-      (if null cl_ts then
-        mk_bot compfuns (HOLogic.mk_tupleT outTs)
-      else foldr1 (mk_sup compfuns) cl_ts)
+    val compilation =
+      if detect_switches options then
+        the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
+          (compile_switch compilation_modifiers ctxt all_vs param_vs additional_arguments
+            mode in_ts' outTs (mk_switch_tree thy mode moded_cls))
+      else
+        let
+          val cl_ts =
+            map (fn (ts, moded_prems) => 
+              compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments
+              mode (HOLogic.mk_tuple in_ts') (split_mode mode ts) moded_prems) moded_cls;
+        in
+          Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
+            (if null cl_ts then
+              mk_bot compfuns (HOLogic.mk_tupleT outTs)
+            else
+              foldr1 (mk_sup compfuns) cl_ts)
+        end
     val fun_const =
       Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
       (ProofContext.theory_of ctxt) s mode, funT)
@@ -1785,7 +1986,7 @@
       (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
   end;
 
-(* special setup for simpset *)                  
+(** special setup for simpset **)
 val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
   setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
@@ -2426,13 +2627,13 @@
 fun join_preds_modes table1 table2 =
   map_preds_modes (fn pred => fn mode => fn value =>
     (value, the (AList.lookup (op =) (the (AList.lookup (op =) table2 pred)) mode))) table1
-    
+
 fun maps_modes preds_modes_table =
   map (fn (pred, modes) =>
     (pred, map (fn (mode, value) => value) modes)) preds_modes_table
-    
-fun compile_preds comp_modifiers thy all_vs param_vs preds moded_clauses =
-  map_preds_modes (fn pred => compile_pred comp_modifiers thy all_vs param_vs pred
+
+fun compile_preds options comp_modifiers thy all_vs param_vs preds moded_clauses =
+  map_preds_modes (fn pred => compile_pred options comp_modifiers thy all_vs param_vs pred
       (the (AList.lookup (op =) preds pred))) moded_clauses
 
 fun prove options thy clauses preds moded_clauses compiled_terms =
@@ -2445,7 +2646,6 @@
     compiled_terms
 
 (* preparation of introduction rules into special datastructures *)
-
 fun dest_prem thy params t =
   (case strip_comb t of
     (v as Free _, ts) => if member (op =) params v then Prem t else Sidecond t
@@ -2589,9 +2789,6 @@
 datatype steps = Steps of
   {
   define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory,
-  (*infer_modes : options -> (string * typ) list -> (string * mode list) list
-    -> string list -> (string * (term list * indprem list) list) list
-    -> theory -> ((moded_clause list pred_mode_table * string list) * theory),*)
   prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list
     -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
   add_code_equations : theory -> (string * typ) list
@@ -2618,32 +2815,39 @@
       prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames)
     val _ = print_step options "Infering modes..."
     val ((moded_clauses, errors), thy') =
-      (*Output.cond_timeit true "Infering modes"
-      (fn _ =>*) infer_modes mode_analysis_options
-        options compilation preds all_modes param_vs clauses thy
+      Output.cond_timeit true "Infering modes"
+      (fn _ => infer_modes mode_analysis_options
+        options compilation preds all_modes param_vs clauses thy)
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = check_expected_modes preds options modes
     (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*)
     val _ = print_modes options thy' modes
     val _ = print_step options "Defining executable functions..."
-    val thy'' = fold (#define_functions (dest_steps steps) options preds) modes thy'
-      |> Theory.checkpoint
+    val thy'' =
+      Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."
+      (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
+      |> Theory.checkpoint)
     val _ = print_step options "Compiling equations..."
     val compiled_terms =
-      compile_preds (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses
+      Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
+        compile_preds options
+          (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses)
     val _ = print_compiled_terms options thy'' compiled_terms
     val _ = print_step options "Proving equations..."
     val result_thms =
-      #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms
+      Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
+      #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
     val result_thms' = #add_code_equations (dest_steps steps) thy'' preds
       (maps_modes result_thms)
     val qname = #qname (dest_steps steps)
     val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
       (fn thm => Context.mapping (Code.add_eqn thm) I))))
-    val thy''' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
+    val thy''' =
+      Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
+      fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
       [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
         [attrib thy ])] thy))
-      result_thms' thy'' |> Theory.checkpoint
+      result_thms' thy'' |> Theory.checkpoint)
   in
     thy'''
   end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -71,17 +71,6 @@
     (Ts' @ [T']) ---> HOLogic.boolT
   end;
 
-(* FIXME: create new predicate name -- does not avoid nameclashing *)
-fun pred_of f =
-  let
-    val (name, T) = dest_Const f
-  in
-    if (body_type T = @{typ bool}) then
-      (Free (Long_Name.base_name name ^ "P", T))
-    else
-      (Free (Long_Name.base_name name ^ "P", pred_type T))
-  end
-
 (* creates the list of premises for every intro rule *)
 (* theory -> term -> (string list, term list list) *)
 
@@ -274,6 +263,17 @@
     map (apfst Envir.eta_contract) (flatten' (Pattern.eta_long [] t) (names, prems))
   end;
 
+(* FIXME: create new predicate name -- does not avoid nameclashing *)
+fun pred_of thy f =
+  let
+    val (name, T) = dest_Const f
+    val base_name' = (Long_Name.base_name name ^ "P")
+    val name' = Sign.full_bname thy base_name'
+    val T' = if (body_type T = @{typ bool}) then T else pred_type T
+  in
+    (name', Const (name', T'))
+  end
+
 (* assumption: mutual recursive predicates all have the same parameters. *)
 fun define_predicates specs thy =
   if forall (fn (const, _) => defined_const thy const) specs then
@@ -284,14 +284,17 @@
       val eqns = maps snd specs
       (* create prednames *)
       val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
+      val dst_funs = distinct (op =) funs
       val argss' = map (map transform_ho_arg) argss
       fun is_lifted (t1, t2) = (fastype_of t2 = pred_type (fastype_of t1))
-     (* FIXME: higher order arguments also occur in tuples! *)
+      (* FIXME: higher order arguments also occur in tuples! *)
       val lifted_args = distinct (op =) (filter is_lifted (flat argss ~~ flat argss'))
-      val preds = map pred_of funs
+      val (prednames, preds) = split_list (map (pred_of thy) funs)
+      val dst_preds = distinct (op =) preds
+      val dst_prednames = distinct (op =) prednames
       (* mapping from term (Free or Const) to term *)
       val net = fold Item_Net.update
-        ((funs ~~ preds) @ lifted_args)
+        ((dst_funs ~~ dst_preds) @ lifted_args)
           (Fun_Pred.get thy)
       fun lookup_pred t = lookup thy net t
       (* create intro rules *)
@@ -308,51 +311,42 @@
           end
       fun mk_rewr_thm (func, pred) = @{thm refl}
       val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
-      val (ind_result, thy') =
-        thy
-        |> Sign.map_naming Name_Space.conceal
-        |> Inductive.add_inductive_global
-          {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
-            no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
-          (map (fn (s, T) =>
-            ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
-          (map (dest_Free o snd) lifted_args)
-          (map (fn x => (Attrib.empty_binding, x)) intr_ts)
-          []
-        ||> Sign.restore_naming thy
-      val prednames = map (fst o dest_Const) (#preds ind_result)
-      (* add constants to my table *)
-      val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname)
-        (#intrs ind_result))) prednames
+      val (intrs, thy') = thy
+        |> Sign.add_consts_i
+          (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
+           dst_preds)
+        |> fold_map Specification.axiom (map (pair (Binding.empty, [])) intr_ts)
+      val specs = map (fn predname => (predname,
+          map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
+        dst_prednames
       val thy'' = Fun_Pred.map
-        (fold Item_Net.update (map (apfst Logic.varify_global)
-          (distinct (op =) funs ~~ (#preds ind_result)))) thy'
+        (fold Item_Net.update (map (pairself Logic.varify_global)
+          (dst_funs ~~ dst_preds))) thy'
       fun functional_mode_of T =
         list_fun_mode (replicate (length (binder_types T)) Input @ [Output])
       val thy''' = fold
         (fn (predname, Const (name, T)) => Predicate_Compile_Core.register_alternative_function
           predname (functional_mode_of T) name)
-      (prednames ~~ distinct (op =) funs) thy''
+      (dst_prednames ~~ dst_funs) thy''
     in
       (specs, thy''')
     end
 
 fun rewrite_intro thy intro =
   let
-    (*val _ = tracing ("Rewriting intro with registered mapping for: " ^
-      commas (Symtab.keys (Pred_Compile_Preproc.get thy)))*)
     fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
+    (*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*)
     val intro_t = Logic.unvarify_global (prop_of intro)
     val (prems, concl) = Logic.strip_horn intro_t
     val frees = map fst (Term.add_frees intro_t [])
     fun rewrite prem names =
       let
         (*val _ = tracing ("Rewriting premise " ^ Syntax.string_of_term_global thy prem ^ "...")*)
-        val t = (HOLogic.dest_Trueprop prem)
+        val t = HOLogic.dest_Trueprop prem
         val (lit, mk_lit) = case try HOLogic.dest_not t of
             SOME t => (t, HOLogic.mk_not)
           | NONE => (t, I)
-        val (P, args) = (strip_comb lit)
+        val (P, args) = strip_comb lit
       in
         folds_map (flatten thy lookup_pred) args (names, [])
         |> map (fn (resargs, (names', prems')) =>
@@ -365,6 +359,8 @@
         rewrite concl frees'
         |> map (fn (concl'::conclprems, _) =>
           Logic.list_implies ((flat prems') @ conclprems, concl')))
+    (*val _ = tracing ("Rewritten intro to " ^
+      commas (map (Syntax.string_of_term_global thy) intro_ts'))*)
   in
     map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts'
   end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -68,10 +68,12 @@
   skip_proof = false,
   compilation = Random,
   inductify = true,
+  specialise = true,
+  detect_switches = false,
   function_flattening = true,
   fail_safe_function_flattening = false,
   no_higher_order_predicate = [],
-  no_topmost_reordering = true
+  no_topmost_reordering = false
 }
 
 val debug_options = Options {
@@ -88,6 +90,8 @@
   skip_proof = false,
   compilation = Random,
   inductify = true,
+  specialise = true,
+  detect_switches = false,
   function_flattening = true,
   fail_safe_function_flattening = false,
   no_higher_order_predicate = [],
@@ -99,13 +103,13 @@
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
-    compilation = c, inductify = i, function_flattening = f_f, 
+    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
-    compilation = c, inductify = i, function_flattening = b,
+    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b,
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re})
 
@@ -113,13 +117,13 @@
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
-    compilation = c, inductify = i, function_flattening = f_f, 
+    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
-    compilation = c, inductify = i, function_flattening = f_f,
+    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
     fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re})
 
@@ -127,13 +131,13 @@
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
-    compilation = c, inductify = i, function_flattening = f_f, 
+    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
-    compilation = c, inductify = i, function_flattening = f_f,
+    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, no_topmost_reordering = re})
 
 
@@ -198,7 +202,7 @@
     val tac = fn _ => Skip_Proof.cheat_tac thy1
     val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac
     val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
-    val (thy3, preproc_time) =  cpu_time "predicate preprocessing"
+    val (thy3, preproc_time) = cpu_time "predicate preprocessing"
         (fn () => Predicate_Compile.preprocess options const thy2)
     val (thy4, core_comp_time) = cpu_time "random_dseq core compilation"
         (fn () =>
@@ -209,7 +213,9 @@
               Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3
           (*| Depth_Limited_Random =>
               Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*))
-    val _ = Predicate_Compile_Core.print_all_modes compilation thy4
+    (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*)
+    val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time))
+    val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time))
     val modes = Predicate_Compile_Core.modes_of compilation thy4 full_constname
     val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
     val prog =
@@ -228,7 +234,6 @@
           Const (name, T)
         end
       else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
-    
     val qc_term =
       case compilation of
           Pos_Random_DSeq => mk_bind (prog,
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -107,7 +107,9 @@
     val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
       [list_comb (pred, pats), list_comb (specialised_const, result_pats)]
     val thy'' = Specialisations.map (Item_Net.update (t, specialised_t)) thy'
-    val ([spec], thy''') = find_specialisations black_list [(constname, exported_intros)] thy''
+    val optimised_intros =
+      map_filter (Predicate_Compile_Aux.peephole_optimisation thy'') exported_intros
+    val ([spec], thy''') = find_specialisations black_list [(constname, optimised_intros)] thy''
     val thy'''' = Predicate_Compile_Core.register_intros spec thy'''
   in
     thy''''
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -85,7 +85,7 @@
 
     val (lub_take_thm, thy) = Specification.axiom ((lub_take_bind, []), lub_take_eqn) thy;
   in
-    (Drule.export_without_context lub_take_thm, thy)
+    (lub_take_thm, thy)
   end;
 
 fun add_axioms
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -200,7 +200,7 @@
           val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy);
         in Library.foldr mk_ex (vs, conj) end;
       val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'));
-      (* first 3 rules replace "y = UU \/ P" with "rep$y = UU \/ P" *)
+      (* first rules replace "y = UU \/ P" with "rep$y = UU \/ P" *)
       val tacs = [
           rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
           rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
@@ -210,7 +210,7 @@
       val exhaust =
           (nchotomy RS @{thm exh_casedist0})
           |> rewrite_rule @{thms exh_casedists}
-          |> Drule.export_without_context;
+          |> Drule.zero_var_indexes;
     end;
 
     (* prove compactness rules for constructors *)
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -136,7 +136,7 @@
     val rep_iso = #rep_inverse info;
     val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
   in
-    Drule.export_without_context thm
+    Drule.zero_var_indexes thm
   end
 
 (******************************************************************************)
@@ -201,7 +201,7 @@
 
     (* register unfold theorems *)
     val (unfold_thms, thy) =
-      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
+      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
         (mk_unfold_thms unfold_binds tuple_unfold_thm) thy;
   in
     ((proj_thms, unfold_thms), thy)
@@ -349,7 +349,7 @@
     val deflation_map_binds = dbinds |>
         map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map");
     val (deflation_map_thms, thy) = thy |>
-      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
+      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
         (conjuncts deflation_map_binds deflation_map_thm);
 
     (* register map functions in theory data *)
@@ -519,7 +519,7 @@
     fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy =
       let
         fun make thm =
-            Drule.export_without_context (thm OF [REP_eq, abs_def, rep_def]);
+            Drule.zero_var_indexes (thm OF [REP_eq, abs_def, rep_def]);
         val rep_iso_thm = make @{thm domain_rep_iso};
         val abs_iso_thm = make @{thm domain_abs_iso};
         val isodefl_thm = make @{thm isodefl_abs_rep};
@@ -607,7 +607,7 @@
           val thmR = thm RS @{thm conjunct2};
         in (n, thmL):: conjuncts ns thmR end;
     val (isodefl_thms, thy) = thy |>
-      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
+      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
         (conjuncts isodefl_binds isodefl_thm);
     val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
 
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -167,7 +167,7 @@
     val rep_iso = #rep_inverse info;
     val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
   in
-    Drule.export_without_context thm
+    Drule.zero_var_indexes thm
   end
 
 (******************************************************************************)
@@ -359,15 +359,15 @@
         in (n, thmL):: conjuncts ns thmR end;
     val (deflation_take_thms, thy) =
       fold_map (add_qualified_thm "deflation_take")
-        (map (apsnd Drule.export_without_context)
+        (map (apsnd Drule.zero_var_indexes)
           (conjuncts dbinds deflation_take_thm)) thy;
 
     (* prove strictness of take functions *)
     fun prove_take_strict (deflation_take, dbind) thy =
       let
         val take_strict_thm =
-            Drule.export_without_context
-            (@{thm deflation_strict} OF [deflation_take]);
+            Drule.zero_var_indexes
+              (@{thm deflation_strict} OF [deflation_take]);
       in
         add_qualified_thm "take_strict" (dbind, take_strict_thm) thy
       end;
@@ -379,8 +379,8 @@
     fun prove_take_take ((chain_take, deflation_take), dbind) thy =
       let
         val take_take_thm =
-            Drule.export_without_context
-            (@{thm deflation_chain_min} OF [chain_take, deflation_take]);
+            Drule.zero_var_indexes
+              (@{thm deflation_chain_min} OF [chain_take, deflation_take]);
       in
         add_qualified_thm "take_take" (dbind, take_take_thm) thy
       end;
@@ -392,8 +392,8 @@
     fun prove_take_below (deflation_take, dbind) thy =
       let
         val take_below_thm =
-            Drule.export_without_context
-            (@{thm deflation.below} OF [deflation_take]);
+            Drule.zero_var_indexes
+              (@{thm deflation.below} OF [deflation_take]);
       in
         add_qualified_thm "take_below" (dbind, take_below_thm) thy
       end;
@@ -542,7 +542,7 @@
     fun prove_reach_lemma ((chain_take, lub_take), dbind) thy =
       let
         val thm =
-            Drule.export_without_context
+            Drule.zero_var_indexes
               (@{thm lub_ID_reach} OF [chain_take, lub_take]);
       in
         add_qualified_thm "reach" (dbind, thm) thy
@@ -575,7 +575,7 @@
       else
         let
           fun prove_take_induct (chain_take, lub_take) =
-              Drule.export_without_context
+              Drule.zero_var_indexes
                 (@{thm lub_ID_take_induct} OF [chain_take, lub_take]);
           val take_inducts =
               map prove_take_induct (chain_take_thms ~~ lub_take_thms);
--- a/src/HOLCF/Tools/pcpodef.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -91,7 +91,7 @@
     val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy;
     (* transfer thms so that they will know about the new cpo instance *)
     val cpo_thms' = map (Thm.transfer thy) cpo_thms;
-    fun make thm = Drule.export_without_context (thm OF cpo_thms');
+    fun make thm = Drule.zero_var_indexes (thm OF cpo_thms');
     val cont_Rep = make @{thm typedef_cont_Rep};
     val cont_Abs = make @{thm typedef_cont_Abs};
     val lub = make @{thm typedef_lub};
@@ -133,7 +133,7 @@
     val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1;
     val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy;
     val pcpo_thms' = map (Thm.transfer thy) pcpo_thms;
-    fun make thm = Drule.export_without_context (thm OF pcpo_thms');
+    fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
     val Rep_strict = make @{thm typedef_Rep_strict};
     val Abs_strict = make @{thm typedef_Abs_strict};
     val Rep_strict_iff = make @{thm typedef_Rep_strict_iff};
--- a/src/HOLCF/Tools/repdef.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -141,7 +141,7 @@
       |> Sign.add_path (Binding.name_of name)
       |> PureThy.add_thm
          ((Binding.prefix_name "REP_" name,
-          Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])
+          Drule.zero_var_indexes (@{thm typedef_REP} OF typedef_thms')), [])
       ||> Sign.restore_naming thy;
 
     val rep_info =
--- a/src/Pure/Isar/locale.ML	Wed Apr 21 14:02:19 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Apr 21 14:02:34 2010 +0200
@@ -95,15 +95,9 @@
   intros: thm option * thm option,
   axioms: thm list,
   (** dynamic part **)
-(* <<<<<<< local
-  decls: (declaration * serial) list * (declaration * serial) list,
-    (* type and term syntax declarations *)
-  notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
-======= *)
   syntax_decls: (declaration * serial) list,
     (* syntax declarations *)
   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
-(* >>>>>>> other *)
     (* theorem declarations *)
   dependencies: ((string * morphism) * serial) list
     (* locale dependencies (sublocale relation) *)
@@ -148,13 +142,8 @@
   thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
     (binding,
       mk_locale ((parameters, spec, intros, axioms),
-(* <<<<<<< local
-        ((pairself (map (fn decl => (decl, serial ()))) decls, map (fn n => (n, serial ())) notes),
-          map (fn d => (d, serial ())) dependencies))) #> snd);
-======= *)
         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
           map (fn d => (d, serial ())) dependencies))) #> snd);
-(* >>>>>>> other *)
 
 fun change_locale name =
   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
@@ -527,16 +516,7 @@
 
 (* Declarations *)
 
-(* <<<<<<< local
-local
-
-fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
-
-fun add_decls add loc decl =
-  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, serial ()))) #>
-======= *)
 fun add_declaration loc decl =
-(* >>>>>>> other *)
   add_thmss loc ""
     [((Binding.conceal Binding.empty,
         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),