src/HOL/Multivariate_Analysis/Integration.certs

--- a/src/HOL/Multivariate_Analysis/Integration.certs	Fri Dec 17 14:36:33 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.certs	Fri Dec 17 14:59:06 2010 +0100
@@ -1,275 +1,275 @@
-57b03a56df49326094be4946646336bc93948572 272 0
+8d81ff6f41bc1cff9f5c6454ee204d147f8e27b7 272 0
 #2 := false
-#46 := 0::Real
-decl f16 :: (-> S3 S9 Real)
-decl f17 :: S9
-#41 := f17
+#48 := 0::Real
+decl f17 :: (-> S3 S10 Real)
+decl f18 :: S10
+#43 := f18
 decl f4 :: S3
 #8 := f4
-#56 := (f16 f4 f17)
-#92 := -1::Real
-#136 := (* -1::Real #56)
+#58 := (f17 f4 f18)
+#94 := -1::Real
+#138 := (* -1::Real #58)
 decl f5 :: (-> S4 S5 Real)
 decl f8 :: S5
 #14 := f8
+decl f20 :: S4
+#54 := f20
+#55 := (f5 f20 f8)
+#139 := (+ #55 #138)
+#122 := (* -1::Real #55)
+#129 := (+ #122 #58)
+#189 := (<= #139 0::Real)
+#196 := (ite #189 #129 #139)
+#372 := (* -1::Real #196)
+#373 := (+ #129 #372)
+#374 := (<= #373 0::Real)
+#356 := (= #129 #196)
 decl f19 :: S4
-#52 := f19
-#53 := (f5 f19 f8)
-#137 := (+ #53 #136)
-#120 := (* -1::Real #53)
-#127 := (+ #120 #56)
-#187 := (<= #137 0::Real)
-#194 := (ite #187 #127 #137)
-#370 := (* -1::Real #194)
-#371 := (+ #127 #370)
-#372 := (<= #371 0::Real)
-#354 := (= #127 #194)
-decl f18 :: S4
-#43 := f18
-#44 := (f5 f18 f8)
+#45 := f19
+#46 := (f5 f19 f8)
 decl f9 :: S3
 #18 := f9
-#42 := (f16 f9 f17)
-#103 := (* -1::Real #42)
-#104 := (+ #103 #44)
-#93 := (* -1::Real #44)
-#94 := (+ #42 #93)
-#222 := (>= #94 0::Real)
-#229 := (ite #222 #94 #104)
-#366 := (* -1::Real #229)
-#369 := (+ #104 #366)
-#373 := (<= #369 0::Real)
-#361 := (= #104 #229)
-#223 := (not #222)
-#374 := [hypothesis]: #222
-#180 := (+ #42 #136)
-#181 := (<= #180 0::Real)
-#205 := -3::Real
-#240 := (* -3::Real #229)
-#241 := (+ #120 #240)
-#242 := (+ #44 #241)
-#243 := (<= #242 0::Real)
-#206 := (* -3::Real #194)
-#207 := (+ #120 #206)
-#208 := (+ #44 #207)
-#209 := (<= #208 0::Real)
-#184 := (not #181)
-#262 := (or #184 #209 #243)
-#267 := (not #262)
-#63 := (<= #42 #56)
-#64 := (implies #63 false)
-#54 := (- #44 #53)
-#50 := 3::Real
-#57 := (- #56 #53)
-#59 := (- #57)
-#58 := (< #57 0::Real)
-#60 := (ite #58 #59 #57)
-#61 := (* #60 3::Real)
-#62 := (< #61 #54)
-#65 := (implies #62 #64)
-#45 := (- #42 #44)
-#48 := (- #45)
-#47 := (< #45 0::Real)
-#49 := (ite #47 #48 #45)
-#51 := (* #49 3::Real)
-#55 := (< #51 #54)
-#66 := (implies #55 #65)
-#67 := (not #66)
-#270 := (iff #67 #267)
-#121 := (+ #44 #120)
-#130 := (< #127 0::Real)
-#142 := (ite #130 #137 #127)
-#148 := (* 3::Real #142)
-#153 := (< #148 #121)
-#162 := (not #153)
-#156 := (not #63)
-#163 := (or #156 #162)
-#97 := (< #94 0::Real)
-#109 := (ite #97 #104 #94)
-#115 := (* 3::Real #109)
-#124 := (< #115 #121)
-#171 := (not #124)
-#172 := (or #171 #163)
-#177 := (not #172)
-#268 := (iff #177 #267)
-#265 := (iff #172 #262)
-#256 := (or #184 #209)
-#259 := (or #243 #256)
-#263 := (iff #259 #262)
-#264 := [rewrite]: #263
-#260 := (iff #172 #259)
-#257 := (iff #163 #256)
-#220 := (iff #162 #209)
-#210 := (not #209)
-#215 := (not #210)
-#218 := (iff #215 #209)
-#219 := [rewrite]: #218
-#216 := (iff #162 #215)
-#213 := (iff #153 #210)
-#199 := (* 3::Real #194)
-#202 := (< #199 #121)
-#211 := (iff #202 #210)
-#212 := [rewrite]: #211
-#203 := (iff #153 #202)
-#200 := (= #148 #199)
-#197 := (= #142 #194)
-#188 := (not #187)
-#191 := (ite #188 #137 #127)
-#195 := (= #191 #194)
-#196 := [rewrite]: #195
-#192 := (= #142 #191)
-#189 := (iff #130 #188)
-#190 := [rewrite]: #189
-#193 := [monotonicity #190]: #192
-#198 := [trans #193 #196]: #197
-#201 := [monotonicity #198]: #200
-#204 := [monotonicity #201]: #203
-#214 := [trans #204 #212]: #213
-#217 := [monotonicity #214]: #216
-#221 := [trans #217 #219]: #220
-#185 := (iff #156 #184)
-#182 := (iff #63 #181)
-#183 := [rewrite]: #182
-#186 := [monotonicity #183]: #185
-#258 := [monotonicity #186 #221]: #257
-#254 := (iff #171 #243)
-#244 := (not #243)
-#249 := (not #244)
-#252 := (iff #249 #243)
-#253 := [rewrite]: #252
-#250 := (iff #171 #249)
-#247 := (iff #124 #244)
-#234 := (* 3::Real #229)
-#237 := (< #234 #121)
-#245 := (iff #237 #244)
-#246 := [rewrite]: #245
-#238 := (iff #124 #237)
-#235 := (= #115 #234)
-#232 := (= #109 #229)
-#226 := (ite #223 #104 #94)
-#230 := (= #226 #229)
-#231 := [rewrite]: #230
-#227 := (= #109 #226)
-#224 := (iff #97 #223)
-#225 := [rewrite]: #224
-#228 := [monotonicity #225]: #227
-#233 := [trans #228 #231]: #232
-#236 := [monotonicity #233]: #235
-#239 := [monotonicity #236]: #238
-#248 := [trans #239 #246]: #247
-#251 := [monotonicity #248]: #250
-#255 := [trans #251 #253]: #254
-#261 := [monotonicity #255 #258]: #260
-#266 := [trans #261 #264]: #265
-#269 := [monotonicity #266]: #268
-#178 := (iff #67 #177)
-#175 := (iff #66 #172)
-#168 := (implies #124 #163)
-#173 := (iff #168 #172)
-#174 := [rewrite]: #173
-#169 := (iff #66 #168)
-#166 := (iff #65 #163)
-#159 := (implies #153 #156)
-#164 := (iff #159 #163)
-#165 := [rewrite]: #164
-#160 := (iff #65 #159)
-#157 := (iff #64 #156)
-#158 := [rewrite]: #157
-#154 := (iff #62 #153)
-#122 := (= #54 #121)
-#123 := [rewrite]: #122
-#151 := (= #61 #148)
-#145 := (* #142 3::Real)
-#149 := (= #145 #148)
-#150 := [rewrite]: #149
-#146 := (= #61 #145)
-#143 := (= #60 #142)
-#128 := (= #57 #127)
-#129 := [rewrite]: #128
-#140 := (= #59 #137)
-#133 := (- #127)
-#138 := (= #133 #137)
-#139 := [rewrite]: #138
-#134 := (= #59 #133)
-#135 := [monotonicity #129]: #134
-#141 := [trans #135 #139]: #140
-#131 := (iff #58 #130)
-#132 := [monotonicity #129]: #131
-#144 := [monotonicity #132 #141 #129]: #143
-#147 := [monotonicity #144]: #146
-#152 := [trans #147 #150]: #151
-#155 := [monotonicity #152 #123]: #154
-#161 := [monotonicity #155 #158]: #160
-#167 := [trans #161 #165]: #166
-#125 := (iff #55 #124)
-#118 := (= #51 #115)
-#112 := (* #109 3::Real)
-#116 := (= #112 #115)
-#117 := [rewrite]: #116
-#113 := (= #51 #112)
-#110 := (= #49 #109)
-#95 := (= #45 #94)
-#96 := [rewrite]: #95
-#107 := (= #48 #104)
-#100 := (- #94)
-#105 := (= #100 #104)
-#106 := [rewrite]: #105
-#101 := (= #48 #100)
-#102 := [monotonicity #96]: #101
-#108 := [trans #102 #106]: #107
-#98 := (iff #47 #97)
-#99 := [monotonicity #96]: #98
-#111 := [monotonicity #99 #108 #96]: #110
-#114 := [monotonicity #111]: #113
-#119 := [trans #114 #117]: #118
-#126 := [monotonicity #119 #123]: #125
-#170 := [monotonicity #126 #167]: #169
-#176 := [trans #170 #174]: #175
-#179 := [monotonicity #176]: #178
-#271 := [trans #179 #269]: #270
-#91 := [asserted]: #67
-#272 := [mp #91 #271]: #267
-#273 := [not-or-elim #272]: #181
-#275 := [not-or-elim #272]: #244
-#367 := (+ #94 #366)
-#368 := (<= #367 0::Real)
-#360 := (= #94 #229)
-#362 := (or #223 #360)
-#363 := [def-axiom]: #362
-#386 := [unit-resolution #363 #374]: #360
-#387 := (not #360)
-#388 := (or #387 #368)
-#389 := [th-lemma arith triangle-eq]: #388
-#390 := [unit-resolution #389 #386]: #368
-#382 := (or #188 #223)
-#375 := [hypothesis]: #187
-#274 := [not-or-elim #272]: #210
-#356 := (or #188 #354)
-#357 := [def-axiom]: #356
-#376 := [unit-resolution #357 #375]: #354
-#377 := (not #354)
-#378 := (or #377 #372)
-#379 := [th-lemma arith triangle-eq]: #378
-#380 := [unit-resolution #379 #376]: #372
-#381 := [th-lemma arith farkas -1 -3 1 -2 1 #273 #380 #274 #375 #374]: false
-#383 := [lemma #381]: #382
-#391 := [unit-resolution #383 #374]: #188
-#392 := [th-lemma arith farkas 1/4 -3/4 1/4 -1/4 1 #391 #390 #275 #273 #374]: false
-#393 := [lemma #392]: #223
-#364 := (or #222 #361)
+#44 := (f17 f9 f18)
+#105 := (* -1::Real #44)
+#106 := (+ #105 #46)
+#95 := (* -1::Real #46)
+#96 := (+ #44 #95)
+#224 := (>= #96 0::Real)
+#231 := (ite #224 #96 #106)
+#368 := (* -1::Real #231)
+#371 := (+ #106 #368)
+#375 := (<= #371 0::Real)
+#363 := (= #106 #231)
+#225 := (not #224)
+#376 := [hypothesis]: #224
+#182 := (+ #44 #138)
+#183 := (<= #182 0::Real)
+#207 := -3::Real
+#242 := (* -3::Real #231)
+#243 := (+ #122 #242)
+#244 := (+ #46 #243)
+#245 := (<= #244 0::Real)
+#208 := (* -3::Real #196)
+#209 := (+ #122 #208)
+#210 := (+ #46 #209)
+#211 := (<= #210 0::Real)
+#186 := (not #183)
+#264 := (or #186 #211 #245)
+#269 := (not #264)
+#65 := (<= #44 #58)
+#66 := (implies #65 false)
+#56 := (- #46 #55)
+#52 := 3::Real
+#59 := (- #58 #55)
+#61 := (- #59)
+#60 := (< #59 0::Real)
+#62 := (ite #60 #61 #59)
+#63 := (* #62 3::Real)
+#64 := (< #63 #56)
+#67 := (implies #64 #66)
+#47 := (- #44 #46)
+#50 := (- #47)
+#49 := (< #47 0::Real)
+#51 := (ite #49 #50 #47)
+#53 := (* #51 3::Real)
+#57 := (< #53 #56)
+#68 := (implies #57 #67)
+#69 := (not #68)
+#272 := (iff #69 #269)
+#123 := (+ #46 #122)
+#132 := (< #129 0::Real)
+#144 := (ite #132 #139 #129)
+#150 := (* 3::Real #144)
+#155 := (< #150 #123)
+#164 := (not #155)
+#158 := (not #65)
+#165 := (or #158 #164)
+#99 := (< #96 0::Real)
+#111 := (ite #99 #106 #96)
+#117 := (* 3::Real #111)
+#126 := (< #117 #123)
+#173 := (not #126)
+#174 := (or #173 #165)
+#179 := (not #174)
+#270 := (iff #179 #269)
+#267 := (iff #174 #264)
+#258 := (or #186 #211)
+#261 := (or #245 #258)
+#265 := (iff #261 #264)
+#266 := [rewrite]: #265
+#262 := (iff #174 #261)
+#259 := (iff #165 #258)
+#222 := (iff #164 #211)
+#212 := (not #211)
+#217 := (not #212)
+#220 := (iff #217 #211)
+#221 := [rewrite]: #220
+#218 := (iff #164 #217)
+#215 := (iff #155 #212)
+#201 := (* 3::Real #196)
+#204 := (< #201 #123)
+#213 := (iff #204 #212)
+#214 := [rewrite]: #213
+#205 := (iff #155 #204)
+#202 := (= #150 #201)
+#199 := (= #144 #196)
+#190 := (not #189)
+#193 := (ite #190 #139 #129)
+#197 := (= #193 #196)
+#198 := [rewrite]: #197
+#194 := (= #144 #193)
+#191 := (iff #132 #190)
+#192 := [rewrite]: #191
+#195 := [monotonicity #192]: #194
+#200 := [trans #195 #198]: #199
+#203 := [monotonicity #200]: #202
+#206 := [monotonicity #203]: #205
+#216 := [trans #206 #214]: #215
+#219 := [monotonicity #216]: #218
+#223 := [trans #219 #221]: #222
+#187 := (iff #158 #186)
+#184 := (iff #65 #183)
+#185 := [rewrite]: #184
+#188 := [monotonicity #185]: #187
+#260 := [monotonicity #188 #223]: #259
+#256 := (iff #173 #245)
+#246 := (not #245)
+#251 := (not #246)
+#254 := (iff #251 #245)
+#255 := [rewrite]: #254
+#252 := (iff #173 #251)
+#249 := (iff #126 #246)
+#236 := (* 3::Real #231)
+#239 := (< #236 #123)
+#247 := (iff #239 #246)
+#248 := [rewrite]: #247
+#240 := (iff #126 #239)
+#237 := (= #117 #236)
+#234 := (= #111 #231)
+#228 := (ite #225 #106 #96)
+#232 := (= #228 #231)
+#233 := [rewrite]: #232
+#229 := (= #111 #228)
+#226 := (iff #99 #225)
+#227 := [rewrite]: #226
+#230 := [monotonicity #227]: #229
+#235 := [trans #230 #233]: #234
+#238 := [monotonicity #235]: #237
+#241 := [monotonicity #238]: #240
+#250 := [trans #241 #248]: #249
+#253 := [monotonicity #250]: #252
+#257 := [trans #253 #255]: #256
+#263 := [monotonicity #257 #260]: #262
+#268 := [trans #263 #266]: #267
+#271 := [monotonicity #268]: #270
+#180 := (iff #69 #179)
+#177 := (iff #68 #174)
+#170 := (implies #126 #165)
+#175 := (iff #170 #174)
+#176 := [rewrite]: #175
+#171 := (iff #68 #170)
+#168 := (iff #67 #165)
+#161 := (implies #155 #158)
+#166 := (iff #161 #165)
+#167 := [rewrite]: #166
+#162 := (iff #67 #161)
+#159 := (iff #66 #158)
+#160 := [rewrite]: #159
+#156 := (iff #64 #155)
+#124 := (= #56 #123)
+#125 := [rewrite]: #124
+#153 := (= #63 #150)
+#147 := (* #144 3::Real)
+#151 := (= #147 #150)
+#152 := [rewrite]: #151
+#148 := (= #63 #147)
+#145 := (= #62 #144)
+#130 := (= #59 #129)
+#131 := [rewrite]: #130
+#142 := (= #61 #139)
+#135 := (- #129)
+#140 := (= #135 #139)
+#141 := [rewrite]: #140
+#136 := (= #61 #135)
+#137 := [monotonicity #131]: #136
+#143 := [trans #137 #141]: #142
+#133 := (iff #60 #132)
+#134 := [monotonicity #131]: #133
+#146 := [monotonicity #134 #143 #131]: #145
+#149 := [monotonicity #146]: #148
+#154 := [trans #149 #152]: #153
+#157 := [monotonicity #154 #125]: #156
+#163 := [monotonicity #157 #160]: #162
+#169 := [trans #163 #167]: #168
+#127 := (iff #57 #126)
+#120 := (= #53 #117)
+#114 := (* #111 3::Real)
+#118 := (= #114 #117)
+#119 := [rewrite]: #118
+#115 := (= #53 #114)
+#112 := (= #51 #111)
+#97 := (= #47 #96)
+#98 := [rewrite]: #97
+#109 := (= #50 #106)
+#102 := (- #96)
+#107 := (= #102 #106)
+#108 := [rewrite]: #107
+#103 := (= #50 #102)
+#104 := [monotonicity #98]: #103
+#110 := [trans #104 #108]: #109
+#100 := (iff #49 #99)
+#101 := [monotonicity #98]: #100
+#113 := [monotonicity #101 #110 #98]: #112
+#116 := [monotonicity #113]: #115
+#121 := [trans #116 #119]: #120
+#128 := [monotonicity #121 #125]: #127
+#172 := [monotonicity #128 #169]: #171
+#178 := [trans #172 #176]: #177
+#181 := [monotonicity #178]: #180
+#273 := [trans #181 #271]: #272
+#93 := [asserted]: #69
+#274 := [mp #93 #273]: #269
+#275 := [not-or-elim #274]: #183
+#277 := [not-or-elim #274]: #246
+#369 := (+ #96 #368)
+#370 := (<= #369 0::Real)
+#362 := (= #96 #231)
+#364 := (or #225 #362)
 #365 := [def-axiom]: #364
-#394 := [unit-resolution #365 #393]: #361
-#395 := (not #361)
-#396 := (or #395 #373)
-#397 := [th-lemma arith triangle-eq]: #396
-#398 := [unit-resolution #397 #394]: #373
-#399 := (not #373)
-#400 := (or #187 #399 #243 #184 #222)
-#401 := [th-lemma arith assign-bounds 3 1 1 2]: #400
-#402 := [unit-resolution #401 #273 #393 #275 #398]: #187
-#403 := [unit-resolution #357 #402]: #354
-#404 := [unit-resolution #379 #403]: #372
-[th-lemma arith farkas 2 2/3 1 1 1/3 1 #398 #275 #273 #393 #274 #404]: false
+#388 := [unit-resolution #365 #376]: #362
+#389 := (not #362)
+#390 := (or #389 #370)
+#391 := [th-lemma arith triangle-eq]: #390
+#392 := [unit-resolution #391 #388]: #370
+#384 := (or #190 #225)
+#377 := [hypothesis]: #189
+#276 := [not-or-elim #274]: #212
+#358 := (or #190 #356)
+#359 := [def-axiom]: #358
+#378 := [unit-resolution #359 #377]: #356
+#379 := (not #356)
+#380 := (or #379 #374)
+#381 := [th-lemma arith triangle-eq]: #380
+#382 := [unit-resolution #381 #378]: #374
+#383 := [th-lemma arith farkas -1 -3 1 -2 1 #275 #382 #276 #377 #376]: false
+#385 := [lemma #383]: #384
+#393 := [unit-resolution #385 #376]: #190
+#394 := [th-lemma arith farkas 1/4 -3/4 1/4 -1/4 1 #393 #392 #277 #275 #376]: false
+#395 := [lemma #394]: #225
+#366 := (or #224 #363)
+#367 := [def-axiom]: #366
+#396 := [unit-resolution #367 #395]: #363
+#397 := (not #363)
+#398 := (or #397 #375)
+#399 := [th-lemma arith triangle-eq]: #398
+#400 := [unit-resolution #399 #396]: #375
+#401 := (not #375)
+#402 := (or #189 #401 #245 #186 #224)
+#403 := [th-lemma arith assign-bounds 3 1 1 2]: #402
+#404 := [unit-resolution #403 #275 #395 #277 #400]: #189
+#405 := [unit-resolution #359 #404]: #356
+#406 := [unit-resolution #381 #405]: #374
+[th-lemma arith farkas 2 2/3 1 1 1/3 1 #400 #277 #275 #395 #276 #406]: false
 unsat
 a66e77fbacece8ec9b71617769b478381e4da6e9 349 0
 #2 := false