1(* ===================================================================== 2 Theory: GAUGE INTEGRALS 3 Description: Generalized gauge intgrals and related theorems 4 (ported from the HOL Light theory of the same) 5 6 Email: grace_gwq@163.com 7 DATE: 08-10-2012 8 9 Ported by: 10 Weiqing Gu, Zhiping Shi, Yong Guan, Shengzhen Jin, Xiaojuan Li 11 12 Beijing Engineering Research Center of High Reliable Embedded System 13 14 College of Information Engineering, Capital Normal University (CNU) 15 Beijing, China 16 ===================================================================== *) 17 18(* 19app load ["arithmeticTheory","realTheory","transcTheory","limTheory", 20 "boolTheory","hol88Lib","numLib","reduceLib","pairTheory","jrhUtils", 21 "powserTheory","Diff","mesonLib","RealArith","tautLib","pairLib", 22 "seqTheory", "numTheory","prim_recTheory","metricTheory", 23 "netsTheory","PairedLambda", "pred_setTheory"]; 24*) 25 26open boolTheory powserTheory PairedLambda Diff mesonLib RealArith 27 tautLib transcTheory limTheory 28 HolKernel Parse bossLib boolLib hol88Lib numLib reduceLib pairLib 29 pairTheory arithmeticTheory numTheory prim_recTheory 30 jrhUtils realTheory metricTheory netsTheory seqTheory pred_setTheory; 31 32val _ = new_theory "integral"; 33val _ = ParseExtras.temp_loose_equality() 34 35val _ = Parse.reveal "B"; 36 37 38(* ------------------------------------------------------------------------ *) 39(* Divisions of adjacent intervals can be combined into one *) 40(* ------------------------------------------------------------------------ *) 41 42(*lemmas about sums*) 43 44val SUM_SPLIT = store_thm("SUM_SPLIT", 45 ���!f n p. sum(m,n) f + sum(m + n,p) f = sum(m,n + p) f���, 46 REPEAT GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV)[SUM_DIFF][] THEN 47 GEN_REWRITE_TAC(LAND_CONV o RAND_CONV)[][SUM_DIFF] THEN CONV_TAC SYM_CONV THEN 48 GEN_REWRITE_TAC LAND_CONV [SUM_DIFF][] THEN RW_TAC arith_ss[] THEN 49 SUBGOAL_THEN���!a b c. b-a + (c-b)=c-a��� 50 (fn th => ONCE_REWRITE_TAC[GEN_ALL th]) THENL 51 [REAL_ARITH_TAC, REWRITE_TAC[]]); 52 53val D_tm = Term`\n. if n < dsize D1 then D1(n) else D2(n - dsize D1)` 54and p_tm = Term`\n. if n < dsize D1 then (p1:num->real)(n) else p2(n - dsize D1)`; 55 56val DIVISION_APPEND_LEMMA1 = prove( 57 Term `!a b c D1 D2. 58 division(a,b) D1 /\ division(b,c) D2 59 ==> 60 (!n. n < dsize D1 + dsize D2 61 ==> 62 (\n. if n < dsize D1 then D1(n) else D2(n - dsize D1)) (n) 63 < 64 (\n. if n < dsize D1 then D1(n) else D2(n - dsize D1)) (SUC n)) /\ 65 (!n. n >= dsize D1 + dsize D2 66 ==> 67 ((\n. if n<dsize D1 then D1(n) else D2(n - dsize D1)) (n) 68 = 69 (\n. if n<dsize D1 then D1(n) else D2(n - dsize D1)) (dsize D1 + dsize D2)))`, 70 REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THEN 71 X_GEN_TAC (Term`n:num`) THEN DISCH_TAC THEN BETA_TAC THENL 72 [ASM_CASES_TAC (Term`SUC n < dsize D1`) THEN ASM_REWRITE_TAC[] THENL 73 [SUBGOAL_THEN (Term`n < dsize D1`) ASSUME_TAC THEN 74 ASM_REWRITE_TAC[] THENL 75 [MATCH_MP_TAC LESS_TRANS THEN EXISTS_TAC (Term`SUC n`) THEN 76 ASM_REWRITE_TAC[LESS_SUC_REFL], 77 UNDISCH_TAC (Term`division(a,b) D1`) THEN REWRITE_TAC[DIVISION_THM] THEN 78 STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 79 FIRST_ASSUM ACCEPT_TAC], 80 ASM_CASES_TAC (Term`n < dsize D1`) THEN ASM_REWRITE_TAC[] THENL 81 [RULE_ASSUM_TAC(REWRITE_RULE[NOT_LESS]) THEN 82 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC (Term`b:real`) THEN 83 CONJ_TAC THENL 84 [MATCH_MP_TAC DIVISION_UBOUND_LT THEN 85 EXISTS_TAC (Term`a:real`) THEN ASM_REWRITE_TAC[], 86 MATCH_MP_TAC DIVISION_LBOUND THEN 87 EXISTS_TAC (Term`c:real`) THEN ASM_REWRITE_TAC[]], 88 UNDISCH_TAC (Term`~(n < dsize D1)`) THEN 89 REWRITE_TAC[NOT_LESS] THEN 90 DISCH_THEN(X_CHOOSE_THEN (Term`d:num`) SUBST_ALL_TAC o 91 REWRITE_RULE[LESS_EQ_EXISTS]) THEN 92 REWRITE_TAC[SUB, GSYM NOT_LESS_EQUAL, LESS_EQ_ADD] THEN 93 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[ADD_SUB] THEN 94 FIRST_ASSUM(MATCH_MP_TAC o Lib.trye el 2 o CONJUNCTS o 95 REWRITE_RULE[DIVISION_THM]) THEN 96 UNDISCH_TAC (Term`dsize D1 + d < dsize D1 + dsize D2`) THEN 97 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[LESS_MONO_ADD_EQ]]], 98 REWRITE_TAC[GSYM NOT_LESS_EQUAL, LESS_EQ_ADD] THEN 99 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[ADD_SUB] THEN 100 REWRITE_TAC[NOT_LESS_EQUAL] THEN COND_CASES_TAC THEN 101 UNDISCH_TAC (Term`n >= dsize D1 + dsize D2`) THENL 102 [CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN 103 REWRITE_TAC[GREATER_EQ, NOT_LESS_EQUAL] THEN 104 MATCH_MP_TAC LESS_IMP_LESS_ADD THEN ASM_REWRITE_TAC[], 105 REWRITE_TAC[GREATER_EQ, LESS_EQ_EXISTS] THEN 106 DISCH_THEN(X_CHOOSE_THEN (Term`d:num`) SUBST_ALL_TAC) THEN 107 REWRITE_TAC[GSYM ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN 108 REWRITE_TAC[ADD_SUB] THEN 109 FIRST_ASSUM(CHANGED_TAC o 110 (SUBST1_TAC o MATCH_MP DIVISION_RHS)) THEN 111 FIRST_ASSUM(MATCH_MP_TAC o el 3 o CONJUNCTS o 112 REWRITE_RULE[DIVISION_THM]) THEN 113 REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD]]]); 114 115 116val DIVISION_APPEND_LEMMA2 = prove( 117 Term`!a b c D1 D2. 118 division(a,b) D1 /\ division(b,c) D2 119 ==> 120 (dsize(\n. if n < dsize D1 then D1(n) else D2(n - dsize D1)) 121 = 122 dsize D1 + dsize D2)`, 123 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [] [dsize] THEN 124 MATCH_MP_TAC SELECT_UNIQUE THEN 125 X_GEN_TAC (Term`N:num`) THEN BETA_TAC THEN EQ_TAC THENL 126 [DISCH_THEN(curry op THEN (MATCH_MP_TAC LESS_EQUAL_ANTISYM) o MP_TAC) THEN 127 CONV_TAC CONTRAPOS_CONV THEN 128 REWRITE_TAC[DE_MORGAN_THM, NOT_LESS_EQUAL] THEN 129 DISCH_THEN DISJ_CASES_TAC THENL 130 [DISJ1_TAC THEN 131 DISCH_THEN(MP_TAC o SPEC (Term`dsize D1 + dsize D2`)) THEN 132 ASM_REWRITE_TAC[] THEN 133 REWRITE_TAC[GSYM NOT_LESS_EQUAL, LESS_EQ_ADD] THEN 134 SUBGOAL_THEN (Term`!x y. x <= SUC(x + y)`) ASSUME_TAC THENL 135 [REPEAT GEN_TAC THEN MATCH_MP_TAC LESS_EQ_TRANS THEN 136 EXISTS_TAC (Term`(x:num) + y`) THEN 137 REWRITE_TAC[LESS_EQ_ADD, LESS_EQ_SUC_REFL], ALL_TAC] THEN 138 ASM_REWRITE_TAC[] THEN REWRITE_TAC[SUB, GSYM NOT_LESS_EQUAL] THEN 139 REWRITE_TAC[LESS_EQ_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN 140 REWRITE_TAC[ADD_SUB] THEN 141 MP_TAC(ASSUME (Term`division(b,c) D2`)) THEN REWRITE_TAC[DIVISION_THM] 142 THEN DISCH_THEN(MP_TAC o SPEC (Term`SUC(dsize D2)`) o el 3 o CONJUNCTS) 143 THEN REWRITE_TAC[GREATER_EQ, LESS_EQ_SUC_REFL] THEN 144 DISCH_THEN SUBST1_TAC THEN 145 FIRST_ASSUM(CHANGED_TAC o SUBST1_TAC o MATCH_MP DIVISION_RHS) THEN 146 REWRITE_TAC[REAL_LT_REFL], 147 DISJ2_TAC THEN 148 DISCH_THEN(MP_TAC o SPEC (Term`dsize D1 + dsize D2`)) THEN 149 FIRST_ASSUM(ASSUME_TAC o MATCH_MP LESS_IMP_LESS_OR_EQ) THEN 150 ASM_REWRITE_TAC[GREATER_EQ] THEN 151 REWRITE_TAC[GSYM NOT_LESS_EQUAL, LESS_EQ_ADD] THEN 152 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[ADD_SUB] THEN 153 COND_CASES_TAC THENL 154 [SUBGOAL_THEN (Term`D1(N:num) < D2(dsize D2)`) MP_TAC THENL 155 [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC (Term`b:real`) THEN 156 CONJ_TAC THENL 157 [MATCH_MP_TAC DIVISION_UBOUND_LT THEN EXISTS_TAC (Term`a:real`) THEN 158 ASM_REWRITE_TAC[GSYM NOT_LESS_EQUAL], 159 MATCH_MP_TAC DIVISION_LBOUND THEN 160 EXISTS_TAC (Term`c:real`) THEN ASM_REWRITE_TAC[]], 161 CONV_TAC CONTRAPOS_CONV THEN ASM_REWRITE_TAC[] THEN 162 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[REAL_LT_REFL]], 163 RULE_ASSUM_TAC(REWRITE_RULE[]) THEN 164 SUBGOAL_THEN (Term`D2(N - dsize D1) < D2(dsize D2)`) MP_TAC THENL 165 [MATCH_MP_TAC DIVISION_LT_GEN THEN 166 MAP_EVERY EXISTS_TAC [Term`b:real`, Term`c:real`] THEN 167 ASM_REWRITE_TAC[LESS_EQ_REFL] THEN 168 REWRITE_TAC[GSYM NOT_LESS_EQUAL] THEN 169 REWRITE_TAC[SUB_LEFT_LESS_EQ, DE_MORGAN_THM] THEN 170 ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[NOT_LESS_EQUAL] THEN 171 UNDISCH_TAC (Term`dsize(D1) <= N`) THEN 172 REWRITE_TAC[LESS_EQ_EXISTS] THEN 173 DISCH_THEN(X_CHOOSE_THEN (Term`d:num`) SUBST_ALL_TAC) THEN 174 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[ADD_SYM]) THEN 175 RULE_ASSUM_TAC(REWRITE_RULE[LESS_MONO_ADD_EQ]) THEN 176 MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN EXISTS_TAC (Term`d:num`) THEN 177 ASM_REWRITE_TAC[ZERO_LESS_EQ], 178 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN 179 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[REAL_LT_REFL]]]], 180 DISCH_THEN SUBST1_TAC THEN CONJ_TAC THENL 181 [X_GEN_TAC (Term`n:num`) THEN DISCH_TAC THEN 182 ASM_CASES_TAC (Term`SUC n < dsize D1`) THEN 183 ASM_REWRITE_TAC[] THENL 184 [SUBGOAL_THEN (Term`n < dsize D1`) ASSUME_TAC THENL 185 [MATCH_MP_TAC LESS_TRANS THEN EXISTS_TAC (Term`SUC n`) THEN 186 ASM_REWRITE_TAC[LESS_SUC_REFL], ALL_TAC] THEN 187 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DIVISION_LT_GEN THEN 188 MAP_EVERY EXISTS_TAC [Term`a:real`, Term`b:real`] THEN 189 ASM_REWRITE_TAC[LESS_SUC_REFL] THEN 190 MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN ASM_REWRITE_TAC[], 191 COND_CASES_TAC THENL 192 [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC (Term`b:real`) THEN 193 CONJ_TAC THENL 194 [MATCH_MP_TAC DIVISION_UBOUND_LT THEN EXISTS_TAC (Term`a:real`) THEN 195 ASM_REWRITE_TAC[], 196 FIRST_ASSUM(MATCH_ACCEPT_TAC o MATCH_MP DIVISION_LBOUND)], 197 MATCH_MP_TAC DIVISION_LT_GEN THEN 198 MAP_EVERY EXISTS_TAC [Term`b:real`, Term`c:real`] THEN 199 ASM_REWRITE_TAC[] THEN 200 CONJ_TAC THENL [ASM_REWRITE_TAC[SUB, LESS_SUC_REFL], ALL_TAC] THEN 201 REWRITE_TAC[REWRITE_RULE[GREATER_EQ] SUB_LEFT_GREATER_EQ] THEN 202 ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[GSYM LESS_EQ]]], 203 X_GEN_TAC (Term`n:num`) THEN REWRITE_TAC[GREATER_EQ] THEN DISCH_TAC THEN 204 REWRITE_TAC[GSYM NOT_LESS_EQUAL,LESS_EQ_ADD] THEN 205 SUBGOAL_THEN (Term`dsize D1 <= n`) ASSUME_TAC THENL 206 [MATCH_MP_TAC LESS_EQ_TRANS THEN 207 EXISTS_TAC (Term `dsize D1 + dsize D2`) THEN 208 ASM_REWRITE_TAC[LESS_EQ_ADD], 209 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN 210 REWRITE_TAC[ADD_SUB] THEN 211 FIRST_ASSUM(CHANGED_TAC o SUBST1_TAC o MATCH_MP DIVISION_RHS) THEN 212 FIRST_ASSUM(MATCH_MP_TAC o el 3 o 213 CONJUNCTS o REWRITE_RULE[DIVISION_THM]) THEN 214 REWRITE_TAC[GREATER_EQ, SUB_LEFT_LESS_EQ] THEN 215 ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[]]]]); 216 217 218val DIVISION_APPEND_EXPLICIT = store_thm("DIVISION_APPEND_EXPLICIT", 219 ``!a b c g d1 p1 d2 p2. 220 tdiv(a,b) (d1,p1) /\ 221 fine g (d1,p1) /\ 222 tdiv(b,c) (d2,p2) /\ 223 fine g (d2,p2) 224 ==> tdiv(a,c) 225 ((\n. if n < dsize d1 then d1(n) else d2(n - (dsize d1))), 226 (\n. if n < dsize d1 227 then p1(n) else p2(n - (dsize d1)))) /\ 228 fine g ((\n. if n < dsize d1 then d1(n) else d2(n - (dsize d1))), 229 (\n. if n < dsize d1 230 then p1(n) else p2(n - (dsize d1)))) /\ 231 !f. rsum((\n. if n < dsize d1 then d1(n) else d2(n - (dsize d1))), 232 (\n. if n < dsize d1 233 then p1(n) else p2(n - (dsize d1)))) f = 234 rsum(d1,p1) f + rsum(d2,p2) f``, 235 MAP_EVERY X_GEN_TAC 236 [Term`a:real`, Term`b:real`, Term`c:real`, Term`g:real->real`, 237 Term`D1:num->real`, Term`p1:num->real`, Term`D2:num->real`, 238 Term`p2:num->real`] THEN 239 STRIP_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL 240 [DISJ_CASES_TAC(GSYM (SPEC ���dsize(D1)��� LESS_0_CASES)) THENL 241 [ASM_REWRITE_TAC[NOT_LESS_0, SUB_0] THEN 242 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN 243 SUBGOAL_THEN ���a:real = b��� (fn th => ASM_REWRITE_TAC[th]) THEN 244 MP_TAC(SPECL [Term`D1:num->real`,Term`a:real`,Term`b:real`] 245 DIVISION_EQ) THEN 246 RULE_ASSUM_TAC(REWRITE_RULE[tdiv]) THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 247 CONJ_TAC THENL 248 [ALL_TAC, 249 REWRITE_TAC[fine] THEN X_GEN_TAC (Term`n:num`) THEN 250 RULE_ASSUM_TAC(REWRITE_RULE[tdiv]) THEN 251 MP_TAC(SPECL [Term`a:real`, Term`b:real`, Term`c:real`, 252 Term`D1:num->real`, Term`D2:num->real`] 253 DIVISION_APPEND_LEMMA2) THEN 254 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 255 BETA_TAC THEN DISCH_TAC THEN ASM_CASES_TAC (Term`SUC n < dsize D1`) THEN 256 ASM_REWRITE_TAC[] THENL 257 [SUBGOAL_THEN (Term`n < dsize D1`) ASSUME_TAC THENL 258 [MATCH_MP_TAC LESS_TRANS THEN EXISTS_TAC (Term`SUC n`) THEN 259 ASM_REWRITE_TAC[LESS_SUC_REFL], ALL_TAC] THEN 260 ASM_REWRITE_TAC[] THEN 261 FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[fine]) THEN 262 ASM_REWRITE_TAC[],ALL_TAC] THEN 263 ASM_CASES_TAC (Term`n < dsize D1`) THEN ASM_REWRITE_TAC[] THENL 264 [SUBGOAL_THEN (Term`SUC n = dsize D1`) ASSUME_TAC THENL 265 [MATCH_MP_TAC LESS_EQUAL_ANTISYM THEN 266 ASM_REWRITE_TAC[GSYM NOT_LESS] THEN 267 REWRITE_TAC[NOT_LESS] THEN MATCH_MP_TAC LESS_OR THEN 268 ASM_REWRITE_TAC[], 269 ASM_REWRITE_TAC[SUB_EQUAL_0] THEN 270 FIRST_ASSUM(CHANGED_TAC o SUBST1_TAC o MATCH_MP DIVISION_LHS o 271 CONJUNCT1) THEN 272 FIRST_ASSUM(CHANGED_TAC o SUBST1_TAC o SYM o 273 MATCH_MP DIVISION_RHS o CONJUNCT1) THEN 274 SUBST1_TAC(SYM(ASSUME (Term`SUC n = dsize D1`))) THEN 275 FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[fine]) THEN 276 ASM_REWRITE_TAC[]], 277 ASM_REWRITE_TAC[SUB] THEN UNDISCH_TAC (Term`~(n < (dsize D1))`) THEN 278 REWRITE_TAC[LESS_EQ_EXISTS, NOT_LESS] THEN 279 DISCH_THEN(X_CHOOSE_THEN (Term`d:num`) SUBST_ALL_TAC) THEN 280 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[ADD_SUB] THEN 281 FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[fine]) THEN 282 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[ADD_SYM]) THEN 283 RULE_ASSUM_TAC(REWRITE_RULE[LESS_MONO_ADD_EQ]) THEN 284 FIRST_ASSUM ACCEPT_TAC]] THEN 285 REWRITE_TAC[tdiv] THEN BETA_TAC THEN CONJ_TAC THENL 286 [RULE_ASSUM_TAC(REWRITE_RULE[tdiv]) THEN 287 REWRITE_TAC[DIVISION_THM] THEN CONJ_TAC THENL 288 [BETA_TAC THEN ASM_REWRITE_TAC[] THEN 289 MATCH_MP_TAC DIVISION_LHS THEN EXISTS_TAC ���b:real��� THEN 290 ASM_REWRITE_TAC[], ALL_TAC] THEN 291 SUBGOAL_THEN ���c = (\n. if (n < (dsize D1)) then D1(n) else D2(n - 292 (dsize D1))) (dsize(D1) + dsize(D2))��� SUBST1_TAC THENL 293 [BETA_TAC THEN REWRITE_TAC[GSYM NOT_LESS_EQUAL, LESS_EQ_ADD] THEN 294 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[ADD_SUB] THEN 295 CONV_TAC SYM_CONV THEN MATCH_MP_TAC DIVISION_RHS THEN 296 EXISTS_TAC (Term`b:real`) THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 297 MP_TAC(SPECL [Term`a:real`, Term`b:real`, Term`c:real`, 298 Term`D1:num->real`, Term`D2:num->real`] 299 DIVISION_APPEND_LEMMA2) THEN 300 ASM_REWRITE_TAC[] THEN DISCH_THEN(fn th => REWRITE_TAC[th]) THEN 301 MATCH_MP_TAC DIVISION_APPEND_LEMMA1 THEN 302 MAP_EVERY EXISTS_TAC [Term`a:real`, Term`b:real`, Term`c:real`] THEN 303 ASM_REWRITE_TAC[], ALL_TAC] THEN 304 X_GEN_TAC (Term`n:num`) THEN RULE_ASSUM_TAC(REWRITE_RULE[tdiv]) THEN 305 ASM_CASES_TAC (Term`SUC n < dsize D1`) THEN ASM_REWRITE_TAC[] THENL 306 [SUBGOAL_THEN (Term`n < dsize D1`) ASSUME_TAC THENL 307 [MATCH_MP_TAC LESS_TRANS THEN EXISTS_TAC (Term`SUC n`) THEN 308 ASM_REWRITE_TAC[LESS_SUC_REFL], ALL_TAC] THEN 309 ASM_REWRITE_TAC[],ALL_TAC] THEN 310 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL 311 [ASM_REWRITE_TAC[SUB] THEN 312 FIRST_ASSUM(CHANGED_TAC o SUBST1_TAC o MATCH_MP DIVISION_LHS o 313 CONJUNCT1) THEN 314 FIRST_ASSUM(CHANGED_TAC o SUBST1_TAC o SYM o 315 MATCH_MP DIVISION_RHS o CONJUNCT1) THEN 316 SUBGOAL_THEN (Term`dsize D1 = SUC n`) (fn th => ASM_REWRITE_TAC[th]) THEN 317 MATCH_MP_TAC LESS_EQUAL_ANTISYM THEN 318 ASM_REWRITE_TAC[GSYM NOT_LESS] THEN REWRITE_TAC[NOT_LESS] THEN 319 MATCH_MP_TAC LESS_OR THEN ASM_REWRITE_TAC[], 320 ASM_REWRITE_TAC[SUB]], 321 GEN_TAC THEN REWRITE_TAC[rsum] THEN 322 SUBGOAL_THEN(Term`(dsize(\n. if n < dsize D1 then D1 n else D2(n- dsize D1)) 323 = dsize D1 + dsize D2)`)MP_TAC THENL 324 [UNDISCH_TAC(Term`tdiv(a,b)(D1,p1)`) THEN 325 UNDISCH_TAC(Term`tdiv(b,c)(D2,p2)`) THEN 326 REWRITE_TAC[tdiv] THEN REPEAT STRIP_TAC THEN 327 MP_TAC(SPECL [Term`a:real`, Term`b:real`, Term`c:real`, 328 Term`D1:num->real`, Term`D2:num->real`] 329 DIVISION_APPEND_LEMMA2) THEN 330 PROVE_TAC[], 331 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[GSYM SUM_SPLIT] THEN 332 REWRITE_TAC[SUM_REINDEX] THEN BINOP_TAC THENL 333 [MATCH_MP_TAC SUM_EQ THEN SIMP_TAC pure_ss[ADD_CLAUSES] THEN 334 RW_TAC arith_ss[ETA_AX] THEN 335 SUBGOAL_THEN(Term`dsize D1 = SUC r`)MP_TAC THENL 336 [POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_LESS] THEN 337 REWRITE_TAC[LESS_EQ] THEN RW_TAC arith_ss[], DISCH_TAC THEN 338 ASM_SIMP_TAC arith_ss[] THEN UNDISCH_TAC(Term`tdiv(a,b)(D1,p1)`) THEN 339 UNDISCH_TAC(Term`tdiv(b,c)(D2,p2)`) THEN REWRITE_TAC[tdiv] THEN 340 REWRITE_TAC[DIVISION_THM] THEN REPEAT STRIP_TAC THEN 341 ASM_REWRITE_TAC[] THEN 342 SUBGOAL_THEN(Term`D1(SUC r) - D1 r = D1(dsize D1) - D1 r`)MP_TAC THENL 343 [PROVE_TAC[], ASM_SIMP_TAC arith_ss[]]], 344 ASM_SIMP_TAC arith_ss[GSYM ADD]]]]); 345 346val DIVISION_APPEND_STRONG = store_thm("DIVISION_APPEND_STRONG", 347 ``!a b c D1 p1 D2 p2. 348 tdiv(a,b) (D1,p1) /\ fine(g) (D1,p1) /\ 349 tdiv(b,c) (D2,p2) /\ fine(g) (D2,p2) 350 ==> ?D p. tdiv(a,c) (D,p) /\ fine(g) (D,p) /\ 351 !f. rsum(D,p) f = rsum(D1,p1) f + rsum(D2,p2) f``, 352 REPEAT STRIP_TAC THEN MAP_EVERY EXISTS_TAC 353 [Term`\n. if n < dsize D1 then D1(n):real else D2(n - (dsize D1))`, 354 Term`\n. if n < dsize D1 then p1(n):real else p2(n - (dsize D1))`] THEN 355 MATCH_MP_TAC DIVISION_APPEND_EXPLICIT THEN ASM_MESON_TAC[]); 356 357 val DIVISION_APPEND = store_thm("DIVISION_APPEND", 358 ``!a b c. 359 (?D1 p1. tdiv(a,b) (D1,p1) /\ fine(g) (D1,p1)) /\ 360 (?D2 p2. tdiv(b,c) (D2,p2) /\ fine(g) (D2,p2)) ==> 361 ?D p. tdiv(a,c) (D,p) /\ fine(g) (D,p)``, 362 MESON_TAC[DIVISION_APPEND_STRONG]); 363 364 365(* ------------------------------------------------------------------------- *) 366(* Definition of integral and integrability. *) 367(* ------------------------------------------------------------------------- *) 368 369val integrable = Define`integrable(a,b) f = ?i. Dint(a,b) f i`; 370 371val integral = Define`integral(a,b) f = @i. Dint(a,b) f i`; 372 373val INTEGRABLE_DINT = store_thm("INTEGRABLE_DINT", 374 ���!f a b. integrable(a,b) f ==> Dint(a,b) f (integral(a,b) f)���, 375 REPEAT GEN_TAC THEN REWRITE_TAC[integrable, integral] THEN 376 CONV_TAC(RAND_CONV SELECT_CONV) THEN REWRITE_TAC[]); 377 378(* ------------------------------------------------------------------------- *) 379(* Other more or less trivial lemmas. *) 380(* ------------------------------------------------------------------------- *) 381 382val DIVISION_BOUNDS = store_thm("DIVISION_BOUNDS", 383 ���!d a b. division(a,b) d ==> !n. a <= d(n) /\ d(n) <= b���, 384 MESON_TAC[DIVISION_UBOUND, DIVISION_LBOUND]); 385 386val TDIV_BOUNDS = store_thm("TDIV_BOUNDS", 387 ���!d p a b. tdiv(a,b) (d,p) 388 ==> !n. a <= d(n) /\ d(n) <= b /\ a <= p(n) /\ p(n) <= b���, 389 REWRITE_TAC[tdiv] THEN ASM_MESON_TAC[DIVISION_BOUNDS, REAL_LE_TRANS]); 390 391val TDIV_LE = store_thm("TDIV_LE", 392 ���!d p a b. tdiv(a,b) (d,p) ==> a <= b���, 393 MESON_TAC[tdiv, DIVISION_LE]); 394 395val DINT_WRONG = store_thm("DINT_WRONG", 396 ���!a b f i. b < a ==> Dint(a,b) f i���, 397 REWRITE_TAC[Dint, gauge] THEN REPEAT STRIP_TAC THEN 398 EXISTS_TAC ���\x:real. &0��� THEN 399 ASM_SIMP_TAC std_ss[REAL_ARITH ``b < a ==> (a <= x /\ x <= b <=> F)``] THEN 400 ASM_MESON_TAC[REAL_NOT_LE, TDIV_LE]); 401 402val DINT_INTEGRAL = store_thm("DINT_INTEGRAL", 403 ���!f a b i. a <= b /\ Dint(a,b) f i ==> (integral(a,b) f = i)���, 404 REPEAT STRIP_TAC THEN REWRITE_TAC[integral] THEN 405 MATCH_MP_TAC SELECT_UNIQUE THEN ASM_MESON_TAC[DINT_UNIQ]); 406 407(* ------------------------------------------------------------------------- *) 408(* Linearity. *) 409(* ------------------------------------------------------------------------- *) 410 411val DINT_NEG = store_thm("DINT_NEG", 412 ���!f a b i. Dint(a,b) f i ==> Dint(a,b) (\x. ~f x) (~i)���, 413 REPEAT GEN_TAC THEN REWRITE_TAC[Dint] THEN 414 SIMP_TAC arith_ss[rsum, REAL_MUL_LNEG, SUM_NEG] THEN 415 SIMP_TAC arith_ss[REAL_SUB_LNEG, ABS_NEG, real_sub]); 416 417val DINT_0 = store_thm("DINT_0", 418 ���!a b. Dint(a,b) (\x. &0) (&0)���, 419 REPEAT GEN_TAC THEN REWRITE_TAC[Dint] THEN GEN_TAC THEN DISCH_TAC THEN 420 EXISTS_TAC (Term`\x:real. &1`) THEN REWRITE_TAC[gauge,REAL_LT_01] THEN 421 REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_SUB_RZERO] THEN 422 REWRITE_TAC[rsum, REAL_MUL_LZERO, SUM_0, ABS_0] THEN RW_TAC arith_ss[]); 423 424val DINT_ADD = store_thm("DINT_ADD", 425���!f g a b i j. 426 Dint(a,b) f i /\ Dint(a,b) g j 427 ==> Dint(a,b) (\x. f x + g x) (i + j)���, 428 REPEAT GEN_TAC THEN REWRITE_TAC[Dint] THEN STRIP_TAC THEN 429 X_GEN_TAC (Term`e:real`) THEN DISCH_TAC THEN 430 REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC ``e / &2``)) THEN 431 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT] THEN 432 DISCH_THEN(X_CHOOSE_THEN (Term`g1:real->real`) STRIP_ASSUME_TAC) THEN 433 DISCH_THEN(X_CHOOSE_THEN (Term`g2:real->real`) STRIP_ASSUME_TAC) THEN 434 EXISTS_TAC ���\x:real. if g1(x) < g2(x) then g1(x) else g2(x)��� THEN 435 ASM_SIMP_TAC arith_ss[GAUGE_MIN, rsum] THEN REPEAT STRIP_TAC THEN 436 SIMP_TAC arith_ss[REAL_ADD_RDISTRIB, SUM_ADD] THEN 437 SIMP_TAC arith_ss[REAL_ADD2_SUB2] THEN REWRITE_TAC[GSYM rsum] THEN 438 FIRST_ASSUM(STRIP_ASSUME_TAC o MATCH_MP FINE_MIN) THEN 439 REPEAT(FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN 440 DISCH_THEN(MP_TAC o SPECL [Term`D:num->real`, Term`p:num->real`]) THEN 441 ASM_REWRITE_TAC[] THEN DISCH_TAC) THEN 442 SUBGOAL_THEN (Term`abs(rsum(D,p) f -i) + abs(rsum(D,p) g - j) < e`) 443 MP_TAC THENL 444 [GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_HALF_DOUBLE] THEN 445 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[], 446 STRIP_TAC THEN 447 KNOW_TAC``abs (rsum (D,p) f - i + (rsum (D,p) g - j)) <= 448 abs (rsum (D,p) f - i) + abs (rsum (D,p) g - j) /\ (abs (rsum (D,p) f - i) + 449 abs (rsum (D,p) g - j)< e)`` THENL 450 [CONJ_TAC THEN REWRITE_TAC[ABS_TRIANGLE], ASM_REWRITE_TAC[]] 451 THEN PROVE_TAC [REAL_LET_TRANS]]); 452 453val DINT_SUB = store_thm("DINT_SUB", 454 ���!f g a b i j. 455 Dint(a,b) f i /\ Dint(a,b) g j 456 ==> Dint(a,b) (\x. f x - g x) (i - j)���, 457 SIMP_TAC arith_ss[real_sub, DINT_ADD, DINT_NEG]); 458 459val DSIZE_EQ = store_thm("DSIZE_EQ", 460���!a b D. division(a,b) D ==> 461 (sum(0,dsize D)(\n. D(SUC n) - D n) - (b - a) = 0)���, 462 REPEAT GEN_TAC THEN STRIP_TAC THEN SIMP_TAC arith_ss[SUM_CANCEL] THEN 463 RW_TAC arith_ss[REAL_SUB_0] THEN MP_TAC DIVISION_LHS THEN 464 MP_TAC DIVISION_RHS THEN PROVE_TAC []); 465 466val DINT_CONST = store_thm("DINT_CONST", 467 ���!a b c. Dint(a,b) (\x. c) (c * (b - a))���, 468 REPEAT GEN_TAC THEN REWRITE_TAC[Dint] THEN REPEAT STRIP_TAC THEN 469 EXISTS_TAC (Term`\x:real. &1`) THEN REWRITE_TAC[gauge,REAL_LT_01] THEN 470 REPEAT STRIP_TAC THEN REWRITE_TAC[rsum] THEN 471 SIMP_TAC arith_ss[SUM_CMUL] THEN 472 SIMP_TAC arith_ss[GSYM REAL_SUB_LDISTRIB] THEN REWRITE_TAC[ABS_MUL] THEN 473 UNDISCH_TAC(Term`tdiv(a,b)(D,p)`) THEN REWRITE_TAC[tdiv] THEN 474 STRIP_TAC THEN UNDISCH_TAC(Term`division(a,b) D`) THEN 475 SIMP_TAC arith_ss[DSIZE_EQ] THEN REWRITE_TAC[ABS_0] THEN STRIP_TAC THEN 476 RW_TAC arith_ss[REAL_MUL_RZERO]); 477 478val DINT_CMUL = store_thm("DINT_CMUL", 479���!f a b c i. Dint(a,b) f i ==> Dint(a,b) (\x. c * f x) (c * i)���, 480 REPEAT GEN_TAC THEN ASM_CASES_TAC (Term`c = &0`) THENL 481 [MP_TAC(SPECL [Term`a:real`, Term`b:real`, Term`c:real`] DINT_CONST) THEN 482 ASM_SIMP_TAC arith_ss[REAL_MUL_LZERO], 483 REWRITE_TAC[Dint] THEN STRIP_TAC THEN X_GEN_TAC(Term`e:real`) THEN 484 DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC ���e / abs(c)���) THEN 485 SUBGOAL_THEN(Term`0 < abs(c)`) MP_TAC THENL 486 [UNDISCH_TAC(Term`c<>0`) THEN SIMP_TAC arith_ss[ABS_NZ], 487 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT] THEN STRIP_TAC THEN 488 DISCH_THEN(X_CHOOSE_THEN (Term`g1:real->real`) STRIP_ASSUME_TAC) THEN 489 EXISTS_TAC���g1:real->real��� THEN ASM_SIMP_TAC arith_ss[] THEN 490 REPEAT STRIP_TAC THEN REWRITE_TAC[rsum] THEN 491 RW_TAC arith_ss[ETA_AX] THEN 492 SUBGOAL_THEN���!a b c d. a*b*(c-d) = a*(b*(c-d))��� 493 (fn th => ONCE_REWRITE_TAC[GEN_ALL th]) THENL 494 [RW_TAC arith_ss[GSYM REAL_MUL_ASSOC], 495 SIMP_TAC arith_ss[SUM_CMUL] THEN 496 SIMP_TAC arith_ss[GSYM REAL_SUB_LDISTRIB] THEN REWRITE_TAC[ABS_MUL] THEN 497 REWRITE_TAC[GSYM rsum] THEN 498 REPEAT(FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN 499 DISCH_THEN(MP_TAC o SPECL [Term`D:num->real`, Term`p:num->real`]) THEN 500 ASM_REWRITE_TAC[] THEN DISCH_TAC) THEN 501 POP_ASSUM MP_TAC THEN UNDISCH_TAC(Term`0 < abs c`) THEN 502 RW_TAC arith_ss[REAL_LT_RDIV_EQ] THEN PROVE_TAC[REAL_MUL_SYM]]]]); 503 504val DINT_LINEAR = store_thm("DINT_LINEAR", 505 ``!f g a b i j. 506 Dint(a,b) f i /\ Dint(a,b) g j 507 ==> Dint(a,b) (\x. m*(f x) + n*(g x)) (m*i + n*j)``, 508 REPEAT STRIP_TAC THEN HO_MATCH_MP_TAC DINT_ADD THEN CONJ_TAC THEN 509 MATCH_MP_TAC DINT_CMUL THEN ASM_REWRITE_TAC[]); 510 511(* ------------------------------------------------------------------------- *) 512(* Ordering properties of integral. *) 513(* ------------------------------------------------------------------------- *) 514 515(*Auxiliary lemmas.*) 516val LT = store_thm("LT", 517 ``(!(m:num). m < 0 = F) /\ (!m n. m < SUC n = ((m = n) \/ m < n))``, 518 SIMP_TAC arith_ss[ZERO_LESS_EQ, LESS_OR_EQ]); 519 520val LE_0 = store_thm ("LE_0",``!(n:num). 0 <= n``, 521 INDUCT_TAC THEN ASM_REWRITE_TAC[LE]); 522 523val LT_0 = store_thm("LT_0",``!(n:num). 0 < SUC n``, 524 SIMP_TAC arith_ss[SUC_ONE_ADD]); 525val EQ_SUC = store_thm("EQ_SUC", ``!(m:num) (n:num). (SUC m = SUC n) = (m = n)``, 526 SIMP_TAC arith_ss[]); 527 528val LE_LT = store_thm("LE_LT", 529 ``!(m:num) (n:num). (m <= n) <=> (m < n) \/ (m = n)``, 530 REPEAT INDUCT_TAC THEN 531 ASM_SIMP_TAC arith_ss[LESS_EQ_MONO, LESS_MONO_EQ, EQ_SUC, ZERO_LESS_EQ, LT_0] 532 THEN REWRITE_TAC[LE, LT]); 533 534val LT_LE = store_thm("LT_LE", 535 ``!(m:num) (n:num). (m < n) <=> (m <= n) /\ ~(m = n)``, 536 REWRITE_TAC[LE_LT] THEN REPEAT GEN_TAC THEN EQ_TAC THENL 537 [DISCH_TAC THEN ASM_SIMP_TAC arith_ss[], 538 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN 539 ASM_REWRITE_TAC[]]); 540 541val REAL_LT_MIN = store_thm("REAL_LT_MIN", 542 ``!x y z. z < min x y <=> z < x /\ z < y``, 543 RW_TAC boolSimps.bool_ss [min_def] THENL [PROVE_TAC[REAL_LTE_TRANS], 544 RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN PROVE_TAC[REAL_LT_TRANS]]); 545 546val REAL_LE_RMUL1 = store_thm("REAL_LE_RMUL1", 547 ``!x y z. x <= y /\ &0 <= z ==> x * z <= y * z``, 548 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LE] THEN 549 REWRITE_TAC[GSYM REAL_SUB_RDISTRIB, REAL_SUB_RZERO, REAL_LE_MUL]); 550 551val REAL_LE_LMUL1 = store_thm("REAL_LE_LMUL1", 552 ``!x y z. &0 <= x /\ y <= z ==> x * y <= x * z``, 553 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LE] THEN 554 REWRITE_TAC[GSYM REAL_SUB_LDISTRIB, REAL_SUB_RZERO, REAL_LE_MUL]); 555 556val INTEGRAL_LE = store_thm("INTEGRAL_LE", 557 ``!f g a b i j. 558 a <= b /\ integrable(a,b) f /\ integrable(a,b) g /\ 559 (!x. a <= x /\ x <= b ==> f(x) <= g(x)) 560 ==> integral(a,b) f <= integral(a,b) g``, 561 REPEAT STRIP_TAC THEN 562 REPEAT(FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP INTEGRABLE_DINT)) THEN 563 MATCH_MP_TAC(REAL_ARITH ``~(&0 < x - y) ==> x <= y``) THEN 564 ABBREV_TAC ``e = integral(a,b) f - integral(a,b) g`` THEN DISCH_TAC THEN 565 NTAC 2(FIRST_X_ASSUM(MP_TAC o SPEC ``e / &2`` o REWRITE_RULE [Dint])) THEN 566 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN 567 DISCH_THEN(X_CHOOSE_THEN ``g1:real->real`` STRIP_ASSUME_TAC) THEN 568 DISCH_THEN(X_CHOOSE_THEN ``g2:real->real`` STRIP_ASSUME_TAC) THEN 569 MP_TAC(SPECL [Term`\x. a <= x /\ x <= b`, 570 Term`g1:real->real`, Term`g2:real->real`] GAUGE_MIN) THEN 571 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 572 MP_TAC(SPECL [``a:real``, ``b:real``, 573 ``\x:real. if g1(x) < g2(x) then g1(x) else g2(x)``] 574 DIVISION_EXISTS) THEN 575 ASM_REWRITE_TAC[] THEN 576 DISCH_THEN(X_CHOOSE_THEN (Term`D:num->real`) 577 (X_CHOOSE_THEN(Term`p:num->real`) STRIP_ASSUME_TAC)) THEN 578 FIRST_ASSUM(STRIP_ASSUME_TAC o MATCH_MP FINE_MIN) THEN 579 REPEAT(FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN 580 DISCH_THEN(MP_TAC o SPECL [Term`D:num->real`, Term`p:num->real`]) THEN 581 ASM_REWRITE_TAC[] THEN DISCH_TAC) THEN 582 SUBGOAL_THEN (Term`abs((rsum(D,p) g - integral(a,b) g) - 583 (rsum(D,p) f - integral(a,b) f)) < e`) MP_TAC THENL 584 [MATCH_MP_TAC REAL_LET_TRANS THEN 585 EXISTS_TAC (Term`abs(rsum(D,p) g - integral(a,b) g) + 586 abs(rsum(D,p) f - integral(a,b) f)`) THEN 587 CONJ_TAC THENL 588 [GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [] [real_sub] THEN 589 GEN_REWRITE_TAC (funpow 2 RAND_CONV) [] [GSYM ABS_NEG] THEN 590 MATCH_ACCEPT_TAC ABS_TRIANGLE, 591 GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_HALF_DOUBLE] THEN 592 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[]], 593 REWRITE_TAC[real_sub, REAL_NEG_ADD, REAL_NEG_SUB] THEN 594 ONCE_REWRITE_TAC[AC (REAL_ADD_ASSOC,REAL_ADD_SYM) 595 (Term`(a + b) + (c + d) = (d + a) + (c + b)`)] THEN 596 REWRITE_TAC[GSYM real_sub] THEN ASM_REWRITE_TAC[] THEN 597 ONCE_REWRITE_TAC[GSYM ABS_NEG] THEN 598 REWRITE_TAC[real_sub, REAL_NEG_ADD, REAL_NEGNEG] THEN 599 REWRITE_TAC[GSYM real_sub] THEN DISCH_TAC THEN 600 SUBGOAL_THEN``0<rsum(D,p) f - rsum(D,p) g``MP_TAC THENL 601 [PROVE_TAC[ABS_SIGN], REWRITE_TAC[] THEN 602 ONCE_REWRITE_TAC[REAL_NOT_LT] THEN REWRITE_TAC[real_sub] THEN 603 ONCE_REWRITE_TAC[GSYM REAL_LE_RNEG] THEN REWRITE_TAC[REAL_NEGNEG] THEN 604 REWRITE_TAC[rsum] THEN MATCH_MP_TAC SUM_LE THEN 605 X_GEN_TAC``r:num`` THEN REWRITE_TAC[ADD_CLAUSES] THEN 606 STRIP_TAC THEN BETA_TAC THEN MATCH_MP_TAC REAL_LE_RMUL1 THEN 607 REWRITE_TAC[REAL_SUB_LE] THEN 608 ASM_MESON_TAC[TDIV_BOUNDS, REAL_LT_IMP_LE, DIVISION_THM, tdiv]]]); 609 610val DINT_LE = store_thm("DINT_LE", 611 ``!f g a b i j. a <= b /\ Dint(a,b) f i /\ Dint(a,b) g j /\ 612 (!x. a <= x /\ x <= b ==> f(x) <= g(x)) 613 ==> i <= j``, 614 REPEAT GEN_TAC THEN MP_TAC(SPEC_ALL INTEGRAL_LE) THEN 615 MESON_TAC[integrable, DINT_INTEGRAL]); 616 617 val DINT_TRIANGLE = store_thm("DINT_TRIANGLE", 618 ``!f a b i j. a <= b /\ Dint(a,b) f i /\ Dint(a,b) (\x. abs(f x)) j 619 ==> abs(i) <= j``, 620 REPEAT STRIP_TAC THEN 621 MATCH_MP_TAC(REAL_ARITH``~a <= b /\ b <= a ==> abs(b) <= a``) THEN 622 CONJ_TAC THEN MATCH_MP_TAC DINT_LE THENL 623 [MAP_EVERY EXISTS_TAC [``\x:real. ~abs(f x)``, ``f:real->real``], 624 MAP_EVERY EXISTS_TAC [``f:real->real``, ``\x:real. abs(f x)``]] THEN 625 MAP_EVERY EXISTS_TAC [``a:real``, ``b:real``] THEN 626 ASM_SIMP_TAC arith_ss[DINT_NEG] THEN REAL_ARITH_TAC); 627 628val DINT_EQ = store_thm("DINT_EQ", 629 ``!f g a b i j. a <= b /\ Dint(a,b) f i /\ Dint(a,b) g j /\ 630 (!x. a <= x /\ x <= b ==> (f(x) = g(x))) 631 ==> (i = j)``, 632 REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN MESON_TAC[DINT_LE]); 633 634val INTEGRAL_EQ = store_thm("INTEGRAL_EQ", 635 ``!f g a b i. Dint(a,b) f i /\ 636 (!x. a <= x /\ x <= b ==> (f(x) = g(x))) 637 ==> Dint(a,b) g i``, 638 REPEAT STRIP_TAC THEN ASM_CASES_TAC ``a <= b`` THENL 639 [UNDISCH_TAC``Dint(a,b) f i`` THEN REWRITE_TAC[Dint] THEN 640 HO_MATCH_MP_TAC MONO_ALL THEN X_GEN_TAC ``e:real`` THEN 641 ASM_CASES_TAC ``&0 < e`` THEN ASM_REWRITE_TAC[] THEN 642 HO_MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC ``d:real->real`` THEN 643 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 644 ASM_REWRITE_TAC[] THEN 645 HO_MATCH_MP_TAC MONO_ALL THEN X_GEN_TAC ``D:num->real`` THEN 646 HO_MATCH_MP_TAC MONO_ALL THEN X_GEN_TAC ``p:num->real`` THEN 647 DISCH_THEN(fn th => STRIP_TAC THEN MP_TAC th) THEN 648 ASM_REWRITE_TAC[] THEN 649 MATCH_MP_TAC(REAL_ARITH ``(x = y) ==> (abs(x - i) < e) ==> 650 (abs(y - i) < e)``) THEN 651 REWRITE_TAC[rsum] THEN MATCH_MP_TAC SUM_EQ THEN 652 REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN BETA_TAC THEN 653 AP_THM_TAC THEN AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 654 ASM_MESON_TAC[tdiv, DIVISION_LBOUND, DIVISION_UBOUND, 655 DIVISION_THM, REAL_LE_TRANS], 656 ASM_MESON_TAC[REAL_NOT_LE, DINT_WRONG]]); 657 658(* ------------------------------------------------------------------------- *) 659(* Integration by parts. *) 660(* ------------------------------------------------------------------------- *) 661 662val INTEGRATION_BY_PARTS = store_thm("INTEGRATION_BY_PARTS", 663 ``!f g f' g' a b. 664 a <= b /\ 665 (!x. a <= x /\ x <= b ==> (f diffl f'(x))(x)) /\ 666 (!x. a <= x /\ x <= b ==> (g diffl g'(x))(x)) 667 ==> Dint(a,b) (\x. f'(x) * g(x) + f(x) * g'(x)) 668 (f(b) * g(b) - f(a) * g(a))``, 669 REPEAT STRIP_TAC THEN HO_MATCH_MP_TAC FTC1 THEN ASM_REWRITE_TAC[] THEN 670 ONCE_REWRITE_TAC[REAL_ARITH ``a + b * c = a + c * b``] THEN 671 ASM_SIMP_TAC arith_ss[DIFF_MUL]); 672 673 (* ------------------------------------------------------------------------- *) 674(* Various simple lemmas about divisions. *) 675(* ------------------------------------------------------------------------- *) 676 677val DIVISION_LE_SUC = store_thm("DIVISION_LE_SUC", 678 ���!d a b. division(a,b) d ==> !n. d(n) <= d(SUC n)���, 679 REWRITE_TAC[DIVISION_THM, GREATER_EQ] THEN 680 MESON_TAC[LESS_CASES, LE, REAL_LE_REFL, REAL_LT_IMP_LE]); 681 682val DIVISION_MONO_LE = store_thm("DIVISION_MONO_LE", 683 ``!d a b. division(a,b) d ==> !m n. m <= n ==> d(m) <= d(n)``, 684 REPEAT GEN_TAC THEN DISCH_THEN(ASSUME_TAC o MATCH_MP DIVISION_LE_SUC) THEN 685 SIMP_TAC arith_ss[LESS_EQ_EXISTS] THEN GEN_TAC THEN 686 SIMP_TAC arith_ss[GSYM LEFT_FORALL_IMP_THM] THEN INDUCT_TAC THEN 687 REWRITE_TAC[ADD_CLAUSES, REAL_LE_REFL] THEN REWRITE_TAC[GSYM ADD_SUC] THEN 688 MATCH_MP_TAC REAL_LE_TRANS THEN 689 EXISTS_TAC(Term`(d:num ->real)(m + p)`) THEN ASM_REWRITE_TAC[]); 690 691val DIVISION_MONO_LE_SUC = store_thm("DIVISION_MONO_LE_SUC", 692 ``!d a b. division(a,b) d ==> !n. d(n) <= d(SUC n)``, 693 MESON_TAC[DIVISION_MONO_LE, LE, LESS_EQ_REFL]); 694 695val DIVISION_DSIZE_LE = store_thm("DIVISION_DSIZE_LE", 696 ``!a b d n. division(a,b) d /\ (d(SUC n) = d(n)) ==> (dsize d <= n)``, 697 REWRITE_TAC[DIVISION_THM] THEN MESON_TAC[REAL_LT_REFL, NOT_LESS]); 698 699val DIVISION_DSIZE_GE = store_thm("DIVISION_DSIZE_GE", 700 ``!a b d n. division(a,b) d /\ d(n) < d(SUC n) ==> SUC n <= dsize d``, 701 REWRITE_TAC[DIVISION_THM, GSYM LESS_EQ, GREATER_EQ] THEN 702 MESON_TAC[REAL_LT_REFL, LE, NOT_LESS]); 703 704val DIVISION_DSIZE_EQ = store_thm("DIVISION_DSIZE_EQ", 705 ``!a b d n. division(a,b) d /\ (d(n) < d(SUC n)) /\ (d(SUC(SUC n)) = d(SUC n)) 706 ==> (dsize d = SUC n)``, 707 REWRITE_TAC[EQ_LESS_EQ] THEN MESON_TAC[DIVISION_DSIZE_LE, DIVISION_DSIZE_GE]); 708 709val DIVISION_DSIZE_EQ_ALT = store_thm("DIVISION_DSIZE_EQ_ALT", 710 ``!a b d n. division(a,b) d /\ (d(SUC n) = d(n)) /\ 711 (!i. i < n ==> (d(i) < d(SUC i))) 712 ==> (dsize d = n)``, 713 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THENL 714 [SUBGOAL_THEN(Term`dsize d <=0 ==> (dsize d = 0)`)MP_TAC THENL 715 [ASM_MESON_TAC[DIVISION_DSIZE_LE, DIVISION_DSIZE_GE, LE], 716 MESON_TAC[DIVISION_DSIZE_LE]], REPEAT STRIP_TAC THEN 717 REWRITE_TAC[EQ_LESS_EQ] THEN 718 ASM_MESON_TAC[DIVISION_DSIZE_LE, DIVISION_DSIZE_GE, LT]]); 719 720 721val num_MAX = store_thm("num_MAX", 722 ``!P. (?(x:num). P x) /\ (?(M:num). !x. P x ==> x <= M) <=> 723 ?m. P m /\ (!x. P x ==> x <= m)``, 724 GEN_TAC THEN EQ_TAC THENL 725 [DISCH_THEN (CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN 726 SUBGOAL_THEN 727 (Term`(?(M:num). !(x:num). P x ==> x <= M) = 728 (?M. (\M. !x. P x ==> x <= M) M)`) SUBST1_TAC THENL 729 [BETA_TAC THEN REFL_TAC, 730 DISCH_THEN (MP_TAC o MATCH_MP WOP) THEN 731 BETA_TAC THEN CONV_TAC (DEPTH_CONV NOT_FORALL_CONV) THEN 732 STRIP_TAC THEN EXISTS_TAC ``n:num`` THEN ASM_REWRITE_TAC[] THEN 733 NTAC 2 (POP_ASSUM MP_TAC) THEN 734 STRUCT_CASES_TAC (SPEC (Term`n:num`) num_CASES) THEN 735 REPEAT STRIP_TAC THENL 736 [UNDISCH_THEN (Term`!(x:num). P x ==> x <= (0:num)`) 737 (MP_TAC o CONV_RULE (ONCE_DEPTH_CONV CONTRAPOS_CONV)) THEN 738 REWRITE_TAC[NOT_LESS_EQUAL] THEN STRIP_TAC THEN 739 POP_ASSUM(MP_TAC o CONV_RULE (ONCE_DEPTH_CONV CONTRAPOS_CONV)) THEN 740 REWRITE_TAC[] THEN STRIP_TAC THEN RES_TAC THEN 741 MP_TAC (SPEC (Term`x:num`) LESS_0_CASES) THEN 742 ASM_REWRITE_TAC[] THEN DISCH_THEN (SUBST_ALL_TAC o SYM) THEN 743 ASM_REWRITE_TAC[], 744 POP_ASSUM (MP_TAC o SPEC (Term`n':num`)) THEN 745 REWRITE_TAC [prim_recTheory.LESS_SUC_REFL] THEN 746 SUBGOAL_THEN (Term`!x y. ~(x ==> y) = x /\ ~y`) 747 (fn th => REWRITE_TAC[th] THEN STRIP_TAC) THENL 748 [REWRITE_TAC [NOT_IMP], 749 UNDISCH_THEN (Term`!(x:num). P x ==> x <= SUC n'`) 750 (MP_TAC o SPEC (Term`x':num`)) THEN 751 ASM_REWRITE_TAC[LESS_OR_EQ] THEN 752 DISCH_THEN (DISJ_CASES_THEN2 ASSUME_TAC SUBST_ALL_TAC) THENL 753 [NTAC 2 (POP_ASSUM MP_TAC) THEN REWRITE_TAC[NOT_LESS_EQUAL] THEN 754 REPEAT STRIP_TAC THEN IMP_RES_TAC LESS_LESS_SUC, 755 ASM_REWRITE_TAC[]]]]], 756 REPEAT STRIP_TAC THEN EXISTS_TAC``m:num`` THEN ASM_REWRITE_TAC[] THEN 757 EXISTS_TAC``m:num`` THEN ASM_REWRITE_TAC[]]); 758 759val DIVISION_INTERMEDIATE = store_thm("DIVISION_INTERMEDIATE", 760 ``!d a b c. division(a,b) d /\ a <= c /\ c <= b 761 ==> ?n. n <= dsize d /\ d(n) <= c /\ c <= d(SUC n)``, 762 REPEAT STRIP_TAC THEN 763 MP_TAC(SPEC (Term`\n. n <= dsize d /\ (d:num->real)(n) <= c`) num_MAX) THEN 764 DISCH_THEN(MP_TAC o fst o EQ_IMP_RULE) THEN 765 SUBGOAL_THEN``(?x. (\n. n <= dsize d /\ d n <= c) x) /\ 766 (?M. !x. (\n. n <= dsize d /\ d n <= c) x ==> x <= M)``MP_TAC THENL 767 [CONJ_TAC THEN BETA_TAC THENL 768 [EXISTS_TAC``0:num`` THEN UNDISCH_TAC``division(a,b) d`` THEN 769 REWRITE_TAC[DIVISION_THM] THEN STRIP_TAC THEN 770 ASM_MESON_TAC[ZERO_LESS_EQ], 771 EXISTS_TAC``dsize (d:num -> real)`` THEN 772 X_GEN_TAC``x:num`` THEN STRIP_TAC], 773 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN HO_MATCH_MP_TAC MONO_EXISTS THEN 774 X_GEN_TAC ``n:num`` THEN SIMP_TAC bool_ss[] THEN STRIP_TAC THEN 775 FIRST_X_ASSUM(MP_TAC o SPEC ``SUC n``) THEN 776 SUBGOAL_THEN``~(SUC n <= n)``ASSUME_TAC THENL 777 [SIMP_TAC arith_ss[LESS_OR], 778 CONV_TAC CONTRAPOS_CONV THEN 779 REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN 780 ASM_SIMP_TAC arith_ss[REAL_LT_IMP_LE, GSYM LESS_EQ, LT_LE] THEN 781 DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC``division(a,b) d`` THEN 782 REWRITE_TAC[DIVISION_THM] THEN 783 DISCH_THEN(MP_TAC o SPEC ``SUC(dsize d)`` o repeat CONJUNCT2) THEN 784 REWRITE_TAC[GREATER_EQ, LE, LESS_EQ_REFL] THEN 785 SUBGOAL_THEN``d(SUC (dsize d)) < b``ASSUME_TAC THENL 786 [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC``c:real`` THEN 787 ASM_REWRITE_TAC[], 788 POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_LT_IMP_NE]]]]); 789 790 791(* ------------------------------------------------------------------------- *) 792(* Combination of adjacent intervals (quite painful in the details). *) 793(* ------------------------------------------------------------------------- *) 794 795val DINT_COMBINE = store_thm("DINT_COMBINE", 796 ``!f a b c i j. a <= b /\ b <= c /\ (Dint(a,b) f i) /\ (Dint(b,c) f j) 797 ==> (Dint(a,c) f (i + j))``, 798 REPEAT GEN_TAC THEN 799 NTAC 2(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN 800 MP_TAC(ASSUME ���a <= b���) THEN REWRITE_TAC[REAL_LE_LT] THEN 801 ASM_CASES_TAC ���a:real = b��� THEN ASM_REWRITE_TAC[] THENL 802 [ASM_MESON_TAC[INTEGRAL_NULL, DINT_UNIQ, REAL_LE_TRANS, REAL_ADD_LID], 803 DISCH_TAC] THEN 804 MP_TAC(ASSUME ���b <= c���) THEN REWRITE_TAC[REAL_LE_LT] THEN 805 ASM_CASES_TAC ���b:real = c��� THEN ASM_REWRITE_TAC[] THENL 806 [ASM_MESON_TAC[INTEGRAL_NULL, DINT_UNIQ, REAL_LE_TRANS, REAL_ADD_RID], 807 DISCH_TAC] THEN 808 SIMP_TAC arith_ss[Dint, GSYM FORALL_AND_THM] THEN 809 DISCH_THEN(fn th => X_GEN_TAC ���e:real��� THEN DISCH_TAC THEN MP_TAC th) THEN 810 DISCH_THEN(MP_TAC o SPEC ���e / &2���) THEN 811 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT] THEN 812 DISCH_THEN(CONJUNCTS_THEN2 813 (X_CHOOSE_THEN ���g1:real->real��� STRIP_ASSUME_TAC) 814 (X_CHOOSE_THEN ���g2:real->real��� STRIP_ASSUME_TAC)) THEN 815 EXISTS_TAC 816 ���\x. if x < b then min (g1 x) (b - x) 817 else if b < x then min (g2 x) (x - b) 818 else min (g1 x) (g2 x)��� THEN 819 CONJ_TAC THENL 820 [REPEAT(FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[gauge])) THEN 821 REWRITE_TAC[gauge] THEN BETA_TAC THEN REPEAT STRIP_TAC THEN 822 REPEAT COND_CASES_TAC THEN 823 ASM_SIMP_TAC arith_ss[REAL_LT_MIN, REAL_SUB_LT] THEN 824 TRY CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 825 ASM_SIMP_TAC arith_ss[REAL_LT_IMP_LE,real_lte], ALL_TAC] THEN 826 MAP_EVERY X_GEN_TAC [Term`d:num->real`, Term`p:num->real`] THEN 827 REWRITE_TAC[tdiv, rsum] THEN STRIP_TAC THEN 828 MP_TAC(SPECL [Term`d:num->real`, Term`a:real`, Term`c:real`, 829 Term`b:real`]DIVISION_INTERMEDIATE) THEN ASM_REWRITE_TAC[] THEN 830 DISCH_THEN(X_CHOOSE_THEN ``m:num`` 831 (CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC)) THEN 832 REWRITE_TAC[LESS_EQ_EXISTS] THEN 833 DISCH_THEN(X_CHOOSE_TAC ``n:num``) THEN ASM_REWRITE_TAC[] THEN 834 ASM_CASES_TAC ``(n:num) = 0`` THENL 835 [FIRST_X_ASSUM SUBST_ALL_TAC THEN 836 RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES]) THEN 837 FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN 838 ASM_MESON_TAC[DIVISION_THM, GREATER_EQ, LESS_EQ_REFL, REAL_NOT_LT], 839 ALL_TAC] THEN 840 REWRITE_TAC[GSYM SUM_SPLIT, ADD_CLAUSES] THEN 841 SUBGOAL_THEN``n= 1 + PRE n``ASSUME_TAC THENL 842 [ASM_SIMP_TAC arith_ss[PRE_SUB1], ALL_TAC] THEN 843 ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[GSYM SUM_SPLIT, SUM_1] THEN 844 BETA_TAC THEN 845 SUBGOAL_THEN ``(p:num->real) m = b`` ASSUME_TAC THENL 846 [FIRST_X_ASSUM(MP_TAC o SPEC ``m:num`` o REWRITE_RULE [fine]) THEN 847 SUBGOAL_THEN``m < dsize d``ASSUME_TAC THENL 848 [ONCE_ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LESS_ADD_NONZERO THEN 849 ASM_REWRITE_TAC[],ALL_TAC] THEN 850 ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MP_TAC o SPEC ``m:num``) THEN 851 MAP_EVERY UNDISCH_TAC [``(d:num->real) m <= b``, 852 ``b:real <= d(SUC m)``] THEN BETA_TAC THEN 853 REPEAT STRIP_TAC THEN 854 SUBGOAL_THEN``(d:num->real)(SUC m) - d m < 855 min((g1:real->real)(p m)) (g2(p m))``MP_TAC THENL 856 [POP_ASSUM MP_TAC THEN RW_TAC std_ss[] THEN 857 POP_ASSUM MP_TAC THEN CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN 858 REWRITE_TAC[GSYM real_lte,REAL_MIN_LE] THEN DISJ2_TAC THEN 859 REWRITE_TAC[real_sub] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN 860 ASM_REWRITE_TAC[REAL_LE_NEG],ALL_TAC] THEN 861 POP_ASSUM MP_TAC THEN RW_TAC std_ss[] THENL 862 [UNDISCH_TAC``(d:num->real) (SUC m) - d m < 863 min ((g1:real->real) (p m)) (b - p m)`` THEN 864 CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN 865 REWRITE_TAC[GSYM real_lte,REAL_MIN_LE] THEN DISJ2_TAC THEN 866 REWRITE_TAC[real_sub] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN 867 ASM_REWRITE_TAC[REAL_LE_NEG], 868 UNDISCH_TAC``(d:num->real) (SUC m) - d m < 869 min ((g2:real->real) (p m)) (p m - b)``THEN 870 CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN 871 REWRITE_TAC[GSYM real_lte,REAL_MIN_LE] THEN DISJ2_TAC THEN 872 REWRITE_TAC[real_sub] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN 873 ASM_REWRITE_TAC[REAL_LE_NEG], 874 ASM_SIMP_TAC arith_ss[GSYM REAL_LE_ANTISYM,real_lte]],ALL_TAC] THEN 875 ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC arith_ss[PRE_SUB1] THEN 876 REWRITE_TAC[GSYM PRE_SUB1] THEN 877 ABBREV_TAC``s1 = sum(0,m)(\n. 878 (f:real->real)((p:num->real) n) * (d(SUC n) - d n))`` THEN 879 ABBREV_TAC``s2 = sum(m + 1, PRE n) 880 (\n. (f:real->real)((p:num->real) n) * (d(SUC n) - d n))`` THEN 881 ONCE_REWRITE_TAC[REAL_ARITH 882 ``(s1 + (f b * (d (SUC m) - d m) + s2) - (i + j)) = 883 (s1 + (f b * (b - d m)) - i) + (s2 + (f b * (d(SUC m) - b)) - j)``] THEN 884 MATCH_MP_TAC REAL_LET_TRANS THEN 885 EXISTS_TAC``abs((s1 + f b * (b - d m)) - i) + 886 abs((s2 + f b * (d(SUC m) - b)) - j)`` THEN 887 REWRITE_TAC[REAL_ABS_TRIANGLE] THEN 888 GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_HALF_DOUBLE] THEN 889 MATCH_MP_TAC REAL_LT_ADD2 THEN CONJ_TAC THENL 890 [UNDISCH_TAC 891 ``!D p. tdiv(a,b) (D,p) /\ fine g1 (D,p) 892 ==> abs(rsum(D,p) f - i) < e / &2`` THEN 893 DISCH_THEN(MP_TAC o SPEC ``\i. 894 if i <= m then (d:num->real)(i) else b``) THEN 895 DISCH_THEN(MP_TAC o SPEC ``\i. 896 if i <= m then (p:num->real)(i) else b``) THEN 897 MATCH_MP_TAC(TAUT_CONV ``a /\ (a ==> b) /\ (a /\ c ==> d) 898 ==> (a /\ b ==> c) ==> d``) THEN 899 CONJ_TAC THENL 900 [REWRITE_TAC[tdiv, division] THEN REPEAT CONJ_TAC THENL 901 [BETA_TAC THEN REWRITE_TAC[LE_0] THEN ASM_MESON_TAC[division], 902 ASM_CASES_TAC ``(d:num->real) m = b`` THENL 903 [EXISTS_TAC ``m:num`` THEN 904 SIMP_TAC arith_ss[ARITH_CONV ``n < m ==> n <= m /\ SUC n <= m``] THEN 905 CONJ_TAC THENL 906 [UNDISCH_TAC``division(a,c) d`` THEN REWRITE_TAC[DIVISION_THM] THEN 907 STRIP_TAC THEN ASM_MESON_TAC[ARITH_CONV``(i:num) < m ==> i < m + n``], 908 RW_TAC arith_ss[] THEN SUBGOAL_THEN``(n':num) = m``ASSUME_TAC THENL 909 [ASM_SIMP_TAC arith_ss[REAL_LE_ANTISYM], ASM_SIMP_TAC arith_ss[]]], 910 EXISTS_TAC ``SUC m`` THEN 911 SIMP_TAC arith_ss[ARITH_CONV ``n >= SUC m ==> ~(n <= m)``] THEN 912 RW_TAC arith_ss[] THENL 913 [UNDISCH_TAC``division(a,c) d`` THEN 914 REWRITE_TAC[DIVISION_THM] THEN STRIP_TAC THEN 915 SUBGOAL_THEN``(n':num) < dsize d``ASSUME_TAC THENL 916 [MATCH_MP_TAC LESS_LESS_EQ_TRANS THEN EXISTS_TAC``m:num`` THEN 917 CONJ_TAC THENL 918 [MATCH_MP_TAC OR_LESS THEN ASM_REWRITE_TAC[], 919 ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC [LESS_EQ_ADD]], 920 ASM_SIMP_TAC arith_ss[]], 921 SUBGOAL_THEN``(n':num) = m``ASSUME_TAC THENL 922 [ASM_SIMP_TAC arith_ss[],ONCE_ASM_REWRITE_TAC[] THEN 923 ONCE_REWRITE_TAC[REAL_LT_LE] THEN ASM_REWRITE_TAC[]]]], 924 BETA_TAC THEN GEN_TAC THEN RW_TAC std_ss[] THENL 925 [REWRITE_TAC[REAL_LE_REFL], 926 SUBGOAL_THEN``(n':num) = m``ASSUME_TAC THENL 927 [ASM_SIMP_TAC arith_ss[], 928 MATCH_MP_TAC REAL_EQ_IMP_LE THEN RW_TAC arith_ss[]], 929 SUBGOAL_THEN``~(SUC n' <= m)``ASSUME_TAC THENL 930 [RW_TAC arith_ss[],ASM_MESON_TAC[]], 931 REWRITE_TAC[REAL_LE_REFL]]],ALL_TAC] THEN 932 CONJ_TAC THENL 933 [REWRITE_TAC[tdiv, fine] THEN BETA_TAC THEN 934 STRIP_TAC THEN X_GEN_TAC ``k:num`` THEN 935 UNDISCH_TAC``fine 936 (\x. 937 if x < b then 938 min (g1 x) (b - x) 939 else if b < x then 940 min (g2 x) (x - b) 941 else 942 min (g1 x) (g2 x)) (d,p)`` THEN REWRITE_TAC[fine] THEN 943 DISCH_THEN(MP_TAC o SPEC ``k:num``) THEN MATCH_MP_TAC MONO_IMP THEN 944 ASM_CASES_TAC ``k:num = m`` THENL 945 [ASM_SIMP_TAC arith_ss[LESS_EQ_REFL, REAL_LT_REFL] THEN DISCH_TAC THEN 946 MATCH_MP_TAC REAL_LET_TRANS THEN 947 EXISTS_TAC``(d:num->real) (SUC m) - d m`` THEN CONJ_TAC THENL 948 [REWRITE_TAC[real_sub] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN 949 ASM_REWRITE_TAC[REAL_LE_REFL], 950 MATCH_MP_TAC REAL_LTE_TRANS THEN 951 EXISTS_TAC``min ((g1:real->real) b) ((g2:real->real) b)`` THEN 952 ASM_REWRITE_TAC[REAL_MIN_LE1]],ALL_TAC] THEN 953 ASM_CASES_TAC ``k:num <= m`` THEN ONCE_ASM_REWRITE_TAC[] THENL 954 [ASM_SIMP_TAC arith_ss[] THEN 955 SUBGOAL_THEN ``(p:num->real) k <= b`` MP_TAC THENL 956 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ``(d:num->real) m`` THEN 957 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN 958 EXISTS_TAC ``(d:num->real) (SUC k)`` THEN ASM_REWRITE_TAC[] THEN 959 ASM_MESON_TAC[DIVISION_MONO_LE, ARITH_CONV 960 ``k <= m /\ ~(k = m) ==> SUC k <= m``],ALL_TAC] THEN 961 COND_CASES_TAC THENL 962 [REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN 963 EXISTS_TAC``min ((g1 :real -> real) 964 ((p :num -> real) k)) ((b :real) - p k)`` THEN 965 ASM_SIMP_TAC arith_ss[REAL_MIN_LE1], 966 DISCH_TAC THEN 967 SUBGOAL_THEN``(p :num -> real) k = b``ASSUME_TAC THENL 968 [ASM_SIMP_TAC arith_ss[REAL_ARITH 969 ``~(a < b) /\ (a <= b) ==> (a = b)``], 970 ASM_SIMP_TAC arith_ss[REAL_LT_REFL] THEN DISCH_TAC THEN 971 MATCH_MP_TAC REAL_LTE_TRANS THEN 972 EXISTS_TAC``min ((g1 :real -> real) b) (g2 b)`` THEN 973 ASM_SIMP_TAC arith_ss[REAL_MIN_LE1]]],ALL_TAC] THEN 974 CONJ_TAC THENL 975 [DISCH_TAC THEN 976 SUBGOAL_THEN``dsize 977 (\(i :num). if i <= (m :num) then (d :num -> real) i 978 else (b :real)) <= SUC (m:num)``MP_TAC THENL 979 [MATCH_MP_TAC DIVISION_DSIZE_LE THEN 980 MAP_EVERY EXISTS_TAC [``a:real``, ``b:real``] THEN 981 ASM_REWRITE_TAC[] THEN SIMP_TAC arith_ss[], 982 ASM_SIMP_TAC arith_ss[]], 983 UNDISCH_TAC ``gauge (\x. a <= x /\ x <= b) g1`` THEN 984 ASM_SIMP_TAC arith_ss[REAL_SUB_REFL, gauge, REAL_LE_REFL]], 985 ALL_TAC] THEN 986 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 987 HO_MATCH_MP_TAC(REAL_ARITH 988 ``(x = y) ==> abs(x - i) < e ==> abs(y - i) < e``) THEN 989 REWRITE_TAC[rsum] THEN ASM_CASES_TAC ``(d:num->real) m = b`` THENL 990 [SUBGOAL_THEN ``dsize (\i. if i <= m then d i else b) = m`` ASSUME_TAC THENL 991 [MATCH_MP_TAC DIVISION_DSIZE_EQ_ALT THEN 992 MAP_EVERY EXISTS_TAC [``a:real``, ``b:real``] THEN CONJ_TAC THENL 993 [ASM_MESON_TAC[tdiv], ALL_TAC] THEN 994 BETA_TAC THEN 995 ASM_SIMP_TAC arith_ss[LESS_EQ_REFL, ARITH_CONV ``~(SUC m <= m)``] THEN 996 UNDISCH_TAC``division (a,c) d`` THEN REWRITE_TAC[DIVISION_THM] THEN 997 ONCE_ASM_REWRITE_TAC[] THEN 998 MESON_TAC[ARITH_CONV ``i < m:num ==> i < m + n``], ALL_TAC] THEN 999 ONCE_ASM_REWRITE_TAC[] THEN 1000 ASM_SIMP_TAC arith_ss[REAL_SUB_REFL, REAL_MUL_RZERO, REAL_ADD_RID] THEN 1001 UNDISCH_TAC``sum (0,m) (\n. (f:real->real) (p n) * 1002 ((d:num->real) (SUC n) - d n)) = s1`` THEN 1003 CONV_TAC(LAND_CONV SYM_CONV) THEN SIMP_TAC arith_ss[] THEN 1004 DISCH_TAC THEN MATCH_MP_TAC SUM_EQ THEN 1005 SIMP_TAC arith_ss[ADD_CLAUSES, LESS_IMP_LESS_OR_EQ, GSYM LESS_EQ], 1006 ALL_TAC] THEN 1007 SUBGOAL_THEN ``dsize (\i. if i <= m then d i else b) = SUC m`` 1008 ASSUME_TAC THENL 1009 [MATCH_MP_TAC DIVISION_DSIZE_EQ THEN 1010 MAP_EVERY EXISTS_TAC [``a:real``, ``b:real``] THEN CONJ_TAC THENL 1011 [ASM_MESON_TAC[tdiv], 1012 BETA_TAC THEN 1013 ASM_SIMP_TAC arith_ss[LESS_EQ_REFL, ARITH_CONV ``~(SUC m <= m)``] THEN 1014 ASM_REWRITE_TAC[REAL_LT_LE]],ALL_TAC] THEN 1015 ASM_SIMP_TAC arith_ss[sum, ADD_CLAUSES, LESS_EQ_REFL, 1016 ARITH_CONV ``~(SUC m <= m)``] THEN 1017 UNDISCH_TAC``sum (0,m) (\n. (f:real->real) (p n) * 1018 ((d:num->real) (SUC n) - d n)) = s1`` THEN 1019 CONV_TAC(LAND_CONV SYM_CONV) THEN SIMP_TAC arith_ss[] THEN 1020 DISCH_TAC THEN ONCE_REWRITE_TAC[REAL_EQ_RADD] THEN 1021 MATCH_MP_TAC SUM_EQ THEN 1022 SIMP_TAC arith_ss[ADD_CLAUSES, LESS_IMP_LESS_OR_EQ, GSYM LESS_EQ], 1023 ALL_TAC] THEN 1024 ASM_CASES_TAC ``d(SUC m):real = b`` THEN ASM_REWRITE_TAC[] THENL 1025 [ASM_REWRITE_TAC[REAL_SUB_REFL, REAL_MUL_RZERO, REAL_ADD_RID] THEN 1026 UNDISCH_TAC``sum (m + 1,PRE n) 1027 (\n. (f:real->real) ((p:num->real) n) * 1028 ((d:num->real) (SUC n) - d n)) = s2`` THEN 1029 CONV_TAC(LAND_CONV SYM_CONV) THEN SIMP_TAC arith_ss[] THEN DISCH_TAC THEN 1030 UNDISCH_TAC 1031 ``!D p. tdiv(b,c) (D,p) /\ fine g2 (D,p) 1032 ==> abs(rsum(D,p) f - j) < e / &2`` THEN 1033 DISCH_THEN(MP_TAC o SPEC ``\i. (d:num->real) (i + SUC m)``) THEN 1034 DISCH_THEN(MP_TAC o SPEC ``\i. (p:num->real) (i + SUC m)``) THEN 1035 MATCH_MP_TAC(TAUT_CONV ``a /\ (a ==> b /\ (b /\ c ==> d)) 1036 ==> (a /\ b ==> c) ==> d``) THEN 1037 CONJ_TAC THENL 1038 [ASM_SIMP_TAC arith_ss[tdiv, division, ADD_CLAUSES] THEN 1039 EXISTS_TAC ``PRE n`` THEN 1040 UNDISCH_TAC``division(a,c) d`` THEN REWRITE_TAC[DIVISION_THM] THEN 1041 ASM_MESON_TAC[ARITH_CONV 1042 ``~(n = 0) /\ k < PRE n ==> SUC(k + m) < m + n``, 1043 ARITH_CONV 1044 ``~(n = 0) /\ k >= PRE n ==> SUC(k + m) >= m + n``], 1045 DISCH_TAC] THEN 1046 SUBGOAL_THEN ``dsize(\i. d (i + SUC m)) = PRE n`` ASSUME_TAC THENL 1047 [MATCH_MP_TAC DIVISION_DSIZE_EQ_ALT THEN 1048 MAP_EVERY EXISTS_TAC [``b:real``, ``c:real``] THEN 1049 CONJ_TAC THENL 1050 [ASM_MESON_TAC[tdiv], 1051 BETA_TAC THEN SIMP_TAC arith_ss[] THEN 1052 UNDISCH_TAC``division(a,c) d`` THEN REWRITE_TAC[DIVISION_THM] THEN 1053 DISCH_THEN(MP_TAC o CONJUNCT2) THEN 1054 ASM_SIMP_TAC arith_ss[ADD_CLAUSES]],ALL_TAC] THEN 1055 CONJ_TAC THENL 1056 [ASM_SIMP_TAC arith_ss[fine] THEN X_GEN_TAC ``k:num`` THEN 1057 DISCH_TAC THEN 1058 UNDISCH_TAC``fine 1059 (\x. 1060 if x < b then 1061 min ((g1:real->real) x) (b - x) 1062 else if b < x then 1063 min ((g2:real->real) x) (x - b) 1064 else 1065 min (g1 x) (g2 x)) (d,p)`` THEN 1066 REWRITE_TAC[fine] THEN DISCH_THEN(MP_TAC o SPEC ``k + SUC m``) THEN 1067 UNDISCH_TAC ``b <= d (SUC m)`` THEN 1068 ASM_SIMP_TAC arith_ss[ADD_CLAUSES] THEN REWRITE_TAC[REAL_LE_REFL] THEN 1069 MATCH_MP_TAC(REAL_ARITH ``b <= a ==> x < b ==> x < a``) THEN 1070 SUBGOAL_THEN ``~(p(SUC (k + m)) < b)``ASSUME_TAC THENL 1071 [RW_TAC arith_ss[GSYM real_lte] THEN MATCH_MP_TAC REAL_LE_TRANS THEN 1072 EXISTS_TAC``(d:num->real)(SUC (k + m))`` THEN CONJ_TAC THENL 1073 [SUBGOAL_THEN``SUC m <= SUC (k+m)``MP_TAC THENL 1074 [SIMP_TAC arith_ss[], MATCH_MP_TAC DIVISION_MONO_LE THEN 1075 MAP_EVERY EXISTS_TAC [``a:real``, ``c:real``] THEN 1076 ASM_REWRITE_TAC[]], 1077 UNDISCH_TAC``tdiv (d (SUC m),c) 1078 ((\i. d (i + SUC m)),(\i. p (i + SUC m)))`` THEN 1079 REWRITE_TAC[tdiv] THEN BETA_TAC THEN STRIP_TAC THEN 1080 ASM_SIMP_TAC arith_ss[]],ASM_SIMP_TAC arith_ss[]] THEN 1081 RW_TAC arith_ss[] THENL 1082 [REWRITE_TAC[REAL_MIN_LE1],REWRITE_TAC[REAL_MIN_LE2]],ALL_TAC] THEN 1083 REWRITE_TAC[rsum] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1084 SUBGOAL_THEN``(m:num) + 1 = 0 + SUC m``ASSUME_TAC THENL 1085 [SIMP_TAC arith_ss[],ALL_TAC] THEN 1086 ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[SUM_REINDEX] THEN 1087 SIMP_TAC arith_ss[PRE_SUB1] THEN 1088 SIMP_TAC arith_ss[ADD1, ADD_CLAUSES],ALL_TAC] THEN 1089 UNDISCH_TAC 1090 ``!D p. tdiv(b,c) (D,p) /\ fine g2 (D,p) 1091 ==> abs(rsum(D,p) f - j) < e / &2`` THEN 1092 DISCH_THEN(MP_TAC o SPEC ``\i. if i = 0 then (b:real) 1093 else (d:num->real)(i + m)``) THEN 1094 DISCH_THEN(MP_TAC o SPEC ``\i. if i = 0 then (b:real) 1095 else (p:num->real)(i + m)``) THEN 1096 MATCH_MP_TAC(TAUT_CONV ``a /\ (a ==> b /\ (b /\ c ==> d)) 1097 ==> (a /\ b ==> c) ==> d``) THEN 1098 CONJ_TAC THENL 1099 [SIMP_TAC arith_ss[tdiv, division, ADD_CLAUSES] THEN CONJ_TAC THENL 1100 [EXISTS_TAC ``n:num`` THEN UNDISCH_TAC``division(a,c) d`` THEN 1101 REWRITE_TAC[DIVISION_THM] THEN DISCH_THEN(MP_TAC o CONJUNCT2) THEN 1102 MATCH_MP_TAC MONO_AND THEN ASM_SIMP_TAC arith_ss[] THEN 1103 DISCH_THEN(fn th => 1104 X_GEN_TAC ``k:num`` THEN MP_TAC(SPEC ``k + m:num`` th)) THEN 1105 ASM_CASES_TAC ``k:num < n`` THENL 1106 [ASM_SIMP_TAC arith_ss[ARITH_CONV 1107 ``(k + (m:num) < m + n) = (k < n)``] THEN 1108 COND_CASES_TAC THENL 1109 [ASM_SIMP_TAC arith_ss[ADD_CLAUSES,REAL_LT_LE],REWRITE_TAC[]], 1110 ASM_SIMP_TAC arith_ss[ADD_CLAUSES]],ALL_TAC] THEN 1111 GEN_TAC THEN COND_CASES_TAC THENL 1112 [ASM_SIMP_TAC arith_ss[REAL_LE_REFL], 1113 ASM_SIMP_TAC arith_ss[REAL_LE_REFL]], ALL_TAC] THEN DISCH_TAC THEN 1114 SUBGOAL_THEN ``dsize(\i. if i = 0 then b else d (i + m)) = n`` 1115 ASSUME_TAC THENL 1116 [MATCH_MP_TAC DIVISION_DSIZE_EQ_ALT THEN 1117 MAP_EVERY EXISTS_TAC [``b:real``, ``c:real``] THEN 1118 CONJ_TAC THENL [ASM_MESON_TAC[tdiv],ALL_TAC] THEN BETA_TAC THEN 1119 UNDISCH_TAC``division(a,c) d`` THEN REWRITE_TAC[DIVISION_THM] THEN 1120 DISCH_THEN(MP_TAC o CONJUNCT2) THEN ONCE_ASM_REWRITE_TAC[ADD_CLAUSES] THEN 1121 GEN_REWRITE_TAC RAND_CONV [][CONJ_SYM] THEN MATCH_MP_TAC MONO_AND THEN 1122 CONJ_TAC THENL 1123 [DISCH_THEN(fn th => 1124 X_GEN_TAC ``k:num`` THEN MP_TAC(SPEC ``k + (m:num)`` th)) THEN 1125 ASM_CASES_TAC ``(k:num) < n`` THENL 1126 [ASM_SIMP_TAC arith_ss[ARITH_CONV ``(k + (m:num) < m + n) = (k < n)``] THEN 1127 COND_CASES_TAC THEN ASM_SIMP_TAC arith_ss[ADD_CLAUSES] THEN 1128 ASM_SIMP_TAC arith_ss[REAL_LT_LE], 1129 ASM_SIMP_TAC arith_ss[]], ASM_SIMP_TAC arith_ss[]],ALL_TAC] THEN 1130 CONJ_TAC THENL 1131 [ASM_SIMP_TAC arith_ss[fine] THEN X_GEN_TAC ``k:num`` THEN DISCH_TAC THEN 1132 UNDISCH_TAC``fine 1133 (\x. 1134 if x < b then 1135 min ((g1:real->real) x) (b - x) 1136 else if b < x then 1137 min ((g2:real->real) x) (x - b) 1138 else 1139 min (g1 x) (g2 x)) (d,p)`` THEN REWRITE_TAC[fine] THEN 1140 DISCH_THEN(MP_TAC o SPEC ``k + m:num``) THEN 1141 ASM_SIMP_TAC arith_ss[ADD_CLAUSES,ARITH_CONV 1142 ``(k + m < m + n) = ((k:num) < n)``] THEN 1143 ASM_CASES_TAC ``(k:num) = 0`` THENL 1144 [ASM_SIMP_TAC arith_ss[ADD_CLAUSES, REAL_LT_REFL] THEN DISCH_TAC THEN 1145 MATCH_MP_TAC REAL_LTE_TRANS THEN 1146 EXISTS_TAC``min (g1 b) ((g2:real->real) b)`` THEN 1147 REWRITE_TAC[REAL_MIN_LE2] THEN MATCH_MP_TAC REAL_LET_TRANS THEN 1148 EXISTS_TAC``(d:num->real) (SUC m) - d m`` THEN 1149 ASM_SIMP_TAC arith_ss[] THEN 1150 ASM_REWRITE_TAC[real_sub,REAL_LE_LADD,REAL_LE_NEG2],ALL_TAC] THEN 1151 ASM_SIMP_TAC arith_ss[] THEN 1152 MATCH_MP_TAC(REAL_ARITH ``b <= a ==> x < b ==> x < a``) THEN 1153 SUBGOAL_THEN ``~((p:num->real) (k + m) < b)``ASSUME_TAC THENL 1154 [RW_TAC arith_ss[GSYM real_lte] THEN MATCH_MP_TAC REAL_LE_TRANS THEN 1155 EXISTS_TAC``(d:num->real)(SUC m)`` THEN ASM_SIMP_TAC arith_ss[] THEN 1156 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC``(d:num->real) (k + m)`` THEN 1157 CONJ_TAC THENL 1158 [FIRST_X_ASSUM(MP_TAC o MATCH_MP DIVISION_MONO_LE) THEN 1159 DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC arith_ss[], 1160 FIRST_ASSUM(MP_TAC o CONJUNCT1 o SPEC ``(k + m):num``) THEN 1161 SIMP_TAC arith_ss[]],ALL_TAC] THEN 1162 ASM_SIMP_TAC arith_ss[] THEN RW_TAC arith_ss[] THENL 1163 [REWRITE_TAC[REAL_MIN_LE1],REWRITE_TAC[REAL_MIN_LE2]],ALL_TAC] THEN 1164 ASM_SIMP_TAC arith_ss[rsum] THEN 1165 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1166 MATCH_MP_TAC(REAL_ARITH 1167 ``(x = y) ==> abs(x - i) < e ==> abs(y - i) < e``) THEN 1168 ONCE_ASM_REWRITE_TAC[] THEN 1169 SIMP_TAC arith_ss[GSYM SUM_SPLIT, SUM_1, ADD_CLAUSES] THEN 1170 MATCH_MP_TAC(REAL_ARITH ``(a = b) ==> (x + a = b + x)``) THEN 1171 UNDISCH_TAC``sum(m + 1, PRE n) 1172 (\n. (f:real->real)((p:num->real) n) * (d(SUC n) - d n)) = s2`` THEN 1173 CONV_TAC(LAND_CONV SYM_CONV) THEN SIMP_TAC arith_ss[] THEN DISCH_TAC THEN 1174 SUBGOAL_THEN``(1:num) = 0 + 1``ASSUME_TAC THENL 1175 [SIMP_TAC arith_ss[],ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN 1176 SUBGOAL_THEN``(m:num) + (0 + 1) = 0 + m + 1``ASSUME_TAC THENL 1177 [SIMP_TAC arith_ss[],ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN 1178 REWRITE_TAC[SUM_REINDEX] THEN MATCH_MP_TAC SUM_EQ THEN 1179 SIMP_TAC arith_ss[ADD_CLAUSES, ADD_EQ_0]); 1180 1181 (* ------------------------------------------------------------------------- *) 1182(* Pointwise perturbation and spike functions. *) 1183(* ------------------------------------------------------------------------- *) 1184 1185val SUM_EQ_0 = store_thm("SUM_EQ_0", 1186 ``(!r. m <= r /\ r < m + n ==> (f(r) = &0)) ==> (sum(m,n) f = &0)``, 1187 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN 1188 EXISTS_TAC ``sum(m,n) (\r. &0)`` THEN 1189 CONJ_TAC THENL [ALL_TAC, REWRITE_TAC[SUM_0]] THEN 1190 MATCH_MP_TAC SUM_EQ THEN ASM_REWRITE_TAC[] THEN 1191 ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[]); 1192 1193val DINT_DELTA_LEFT = store_thm("DINT_DELTA_LEFT", 1194 ``!a b. Dint(a,b) (\x. if x = a then &1 else &0) (&0)``, 1195 REPEAT GEN_TAC THEN DISJ_CASES_TAC(REAL_ARITH ``b < a \/ a <= b``) THENL 1196 [ASM_SIMP_TAC arith_ss[DINT_WRONG], 1197 REWRITE_TAC[Dint] THEN X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1198 EXISTS_TAC ``(\x. e):real->real`` THEN 1199 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT, gauge, 1200 fine, rsum, tdiv, REAL_SUB_RZERO] THEN 1201 MAP_EVERY X_GEN_TAC[���d:num->real���,���p:num->real���] THEN 1202 STRIP_TAC THEN ASM_CASES_TAC(Term`dsize d = 0`) THEN 1203 ASM_REWRITE_TAC[sum, ABS_N] THEN 1204 SUBGOAL_THEN���dsize d = 1 + PRE (dsize d)���ASSUME_TAC THENL 1205 [ASM_SIMP_TAC arith_ss[PRE_SUB1], 1206 ONCE_ASM_REWRITE_TAC[] THEN 1207 REWRITE_TAC[GSYM SUM_SPLIT, SUM_1, ADD_CLAUSES] THEN 1208 MATCH_MP_TAC(REAL_ARITH 1209 ``(&0 <= x /\ x < e) /\ (y = &0) ==> (abs(x + y) < e)``) THEN 1210 CONJ_TAC THENL 1211 [BETA_TAC THEN COND_CASES_TAC THENL 1212 [REWRITE_TAC[REAL_MUL_LID, REAL_SUB_LE] THEN 1213 ASM_MESON_TAC[DIVISION_THM, ZERO_LESS_EQ, NOT_ZERO_LT_ZERO], 1214 ASM_REWRITE_TAC [REAL_MUL_LZERO, REAL_LE_REFL]], 1215 MATCH_MP_TAC SUM_EQ_0 THEN X_GEN_TAC ``r:num`` THEN STRIP_TAC THEN 1216 BETA_TAC THEN REWRITE_TAC[REAL_ENTIRE] THEN DISJ1_TAC THEN 1217 SUBGOAL_THEN``(a:real) < (p:num->real) r``MP_TAC THENL 1218 [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC``(d:num->real)r`` THEN 1219 CONJ_TAC THENL 1220 [SUBGOAL_THEN``(a:real) = (d:num->real) 0``MP_TAC THENL 1221 [UNDISCH_TAC``division (a,b) d`` THEN REWRITE_TAC[DIVISION_THM] THEN 1222 STRIP_TAC THEN UNDISCH_TAC``(d:num->real) 0 = a`` THEN 1223 CONV_TAC(LAND_CONV SYM_CONV) THEN PROVE_TAC[], 1224 DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN 1225 MATCH_MP_TAC DIVISION_LT_GEN THEN 1226 MAP_EVERY EXISTS_TAC[``a:real``,``b:real``] THEN 1227 ASM_SIMP_TAC arith_ss[LESS_EQ, GSYM ONE]], 1228 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN 1229 ASM_SIMP_TAC arith_ss[]], 1230 SIMP_TAC arith_ss[REAL_LT_IMP_NE]]]]]); 1231 1232val DINT_DELTA_RIGHT = store_thm("DINT_DELTA_RIGHT", 1233 ``!a b. Dint(a,b) (\x. if x = b then &1 else &0) (&0)``, 1234 REPEAT GEN_TAC THEN DISJ_CASES_TAC(REAL_ARITH ``b < a \/ a <= b``) THENL 1235 [ASM_SIMP_TAC arith_ss[DINT_WRONG], 1236 REWRITE_TAC[Dint] THEN 1237 X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1238 EXISTS_TAC ``(\x. e):real->real`` THEN 1239 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT, 1240 gauge, fine, rsum, tdiv, REAL_SUB_RZERO] THEN 1241 MAP_EVERY X_GEN_TAC [``d:num->real``, ``p:num->real``] THEN 1242 STRIP_TAC THEN ASM_CASES_TAC ``dsize d = 0`` THEN 1243 ASM_REWRITE_TAC[sum, ABS_N] THEN 1244 SUBGOAL_THEN``dsize d = PRE (dsize d) + 1``ASSUME_TAC THENL 1245 [ASM_SIMP_TAC arith_ss[PRE_SUB1], 1246 ONCE_ASM_REWRITE_TAC[] THEN ABBREV_TAC ``m = PRE(dsize d)`` THEN 1247 ASM_REWRITE_TAC[GSYM SUM_SPLIT, SUM_1, ADD_CLAUSES] THEN 1248 MATCH_MP_TAC(REAL_ARITH 1249 ``(&0 <= x /\ x < e) /\ (y = &0) ==> abs(y + x) < e``) THEN 1250 CONJ_TAC THENL 1251 [BETA_TAC THEN COND_CASES_TAC THENL 1252 [REWRITE_TAC[REAL_MUL_LID, REAL_SUB_LE] THEN CONJ_TAC THENL 1253 [PROVE_TAC[DIVISION_MONO_LE_SUC], ASM_SIMP_TAC arith_ss[]], 1254 ASM_REWRITE_TAC[REAL_MUL_LZERO, REAL_LE_REFL]], 1255 MATCH_MP_TAC SUM_EQ_0 THEN X_GEN_TAC ``r:num`` THEN 1256 REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC THEN BETA_TAC THEN 1257 REWRITE_TAC[REAL_ENTIRE] THEN DISJ1_TAC THEN 1258 SUBGOAL_THEN``(p:num->real) r < b``MP_TAC THENL 1259 [MATCH_MP_TAC REAL_LET_TRANS THEN 1260 EXISTS_TAC``(d:num->real)(SUC r)`` THEN CONJ_TAC THENL 1261 [ASM_REWRITE_TAC[], 1262 SUBGOAL_THEN``b = d(dsize d)``MP_TAC THENL 1263 [UNDISCH_TAC``division(a,b) (d:num->real)`` THEN 1264 REWRITE_TAC[DIVISION_THM] THEN STRIP_TAC THEN 1265 POP_ASSUM MP_TAC THEN SIMP_TAC arith_ss[], 1266 DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN 1267 ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[SUC_ONE_ADD] THEN 1268 MATCH_MP_TAC DIVISION_LT_GEN THEN 1269 MAP_EVERY EXISTS_TAC[``a:real``,``b:real``] THEN 1270 ASM_SIMP_TAC arith_ss[LESS_EQ]]], 1271 SIMP_TAC arith_ss[REAL_LT_IMP_NE]]]]]); 1272 1273val DINT_DELTA = store_thm("DINT_DELTA", 1274 ``!a b c. Dint(a,b) (\x. if x = c then &1 else &0) (&0)``, 1275 REPEAT GEN_TAC THEN ASM_CASES_TAC ``a <= b`` THENL 1276 [ALL_TAC, ASM_MESON_TAC[REAL_NOT_LE, DINT_WRONG]] THEN 1277 ASM_CASES_TAC ``a <= c /\ c <= b`` THENL 1278 [ALL_TAC, 1279 MATCH_MP_TAC INTEGRAL_EQ THEN EXISTS_TAC ``\x:real. &0`` THEN 1280 ASM_REWRITE_TAC[DINT_0] THEN RW_TAC arith_ss[]] THEN 1281 GEN_REWRITE_TAC RAND_CONV [][GSYM REAL_ADD_LID] THEN 1282 MATCH_MP_TAC DINT_COMBINE THEN EXISTS_TAC ``c:real`` THEN 1283 ASM_REWRITE_TAC[DINT_DELTA_LEFT, DINT_DELTA_RIGHT]); 1284 1285val DINT_POINT_SPIKE = store_thm("DINT_POINT_SPIKE", 1286 ``!f g a b c i. 1287 (!x. a <= x /\ x <= b /\ ~(x = c) ==> (f x = g x)) /\ Dint(a,b) f i 1288 ==> Dint(a,b) g i``, 1289 REPEAT STRIP_TAC THEN ASM_CASES_TAC ``a <= b`` THENL 1290 [ALL_TAC, ASM_MESON_TAC[REAL_NOT_LE, DINT_WRONG]] THEN 1291 MATCH_MP_TAC INTEGRAL_EQ THEN 1292 EXISTS_TAC ``\x:real. f(x) + (g c - f c) * (if x = c then &1 else &0)`` THEN 1293 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL 1294 [SUBST1_TAC(REAL_ARITH ``i = i + ((g:real->real) c - f c) * &0``) THEN 1295 HO_MATCH_MP_TAC DINT_ADD THEN ASM_REWRITE_TAC[] THEN 1296 HO_MATCH_MP_TAC DINT_CMUL THEN REWRITE_TAC[DINT_DELTA], 1297 REPEAT STRIP_TAC THEN BETA_TAC THEN COND_CASES_TAC THEN 1298 ASM_SIMP_TAC arith_ss[REAL_MUL_RZERO, REAL_ADD_RID] THEN 1299 REAL_ARITH_TAC]); 1300 1301val DINT_FINITE_SPIKE = store_thm("DINT_FINITE_SPIKE", 1302 ``!f g a b s i. 1303 FINITE s /\ 1304 (!x. a <= x /\ x <= b /\ ~(x IN s) ==> (f x = g x)) /\ 1305 Dint(a,b) f i 1306 ==> Dint(a,b) g i``, 1307 REPEAT GEN_TAC THEN 1308 REWRITE_TAC[TAUT_CONV ``a /\ b /\ c ==> d <=> c ==> a ==> b ==> d``] THEN 1309 DISCH_TAC THEN 1310 MAP_EVERY (fn t => SPEC_TAC(t,t))[``g:real->real``, ``s:real->bool``] THEN 1311 SIMP_TAC bool_ss[RIGHT_FORALL_IMP_THM] THEN 1312 HO_MATCH_MP_TAC FINITE_INDUCT THEN REWRITE_TAC[NOT_IN_EMPTY] THEN 1313 CONJ_TAC THENL [ASM_MESON_TAC[INTEGRAL_EQ], ALL_TAC] THEN 1314 X_GEN_TAC``s:real->bool`` THEN DISCH_TAC THEN X_GEN_TAC``c:real`` THEN 1315 POP_ASSUM MP_TAC THEN 1316 REWRITE_TAC[TAUT_CONV``a /\ b ==> c ==> d <=> b /\ c /\ a ==> d``] THEN 1317 STRIP_TAC THEN X_GEN_TAC ``g:real->real`` THEN 1318 REWRITE_TAC[IN_INSERT, DE_MORGAN_THM] THEN DISCH_TAC THEN 1319 MATCH_MP_TAC DINT_POINT_SPIKE THEN 1320 EXISTS_TAC ``\x. if x = c then (f:real->real) x else g x`` THEN 1321 EXISTS_TAC ``c:real`` THEN SIMP_TAC arith_ss[] THEN 1322 FIRST_X_ASSUM MATCH_MP_TAC THEN BETA_TAC THEN RW_TAC std_ss[]); 1323 1324(* ------------------------------------------------------------------------- *) 1325(* Cauchy-type integrability criterion. *) 1326(* ------------------------------------------------------------------------- *) 1327 1328val REAL_POW_LBOUND = store_thm("REAL_POW_LBOUND", 1329 ``!x n. &0 <= x ==> &1 + &n * x <= (&1 + x) pow n``, 1330 GEN_TAC THEN SIMP_TAC arith_ss[RIGHT_FORALL_IMP_THM] THEN 1331 DISCH_TAC THEN INDUCT_TAC THEN 1332 REWRITE_TAC[pow, REAL_MUL_LZERO, REAL_ADD_RID, REAL_LE_REFL] THEN 1333 REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN 1334 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ``(&1 + x) * (&1 + &n * x)`` THEN 1335 ASM_SIMP_TAC arith_ss[REAL_LE_MUL, REAL_POS, REAL_ARITH 1336 ``&1 + (n + &1) * x <= (&1 + x) * (&1 + n * x) <=> &0 <= n * x * x``] THEN 1337 REWRITE_TAC[SUC_ONE_ADD, REAL_POW_ADD, POW_1] THEN 1338 ASM_SIMP_TAC arith_ss[REAL_LE_LMUL1, REAL_ARITH ``&0 <= x ==> &0 <= &1 + x``]); 1339 1340val REAL_ARCH_POW = store_thm("REAL_ARCH_POW", 1341 ``!x y. &1 < x ==> ?n. y < x pow n``, 1342 REPEAT STRIP_TAC THEN 1343 MP_TAC(SPEC ``x - &1`` REAL_ARCH) THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN 1344 DISCH_THEN(MP_TAC o SPEC ``y:real``) THEN HO_MATCH_MP_TAC MONO_EXISTS THEN 1345 X_GEN_TAC ``n:num`` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN 1346 EXISTS_TAC ``&1 + &n * (x - &1)`` THEN 1347 ASM_SIMP_TAC arith_ss[REAL_ARITH ``x < y ==> x < &1 + y``] THEN 1348 ASM_MESON_TAC[REAL_POW_LBOUND, REAL_SUB_ADD2, REAL_ARITH 1349 ``&1 < x ==> &0 <= x - &1``]); 1350 1351val REAL_ARCH_POW2 = store_thm("REAL_ARCH_POW2", 1352 ``!x. ?n. x < &2 pow n``, 1353 SIMP_TAC arith_ss[REAL_ARCH_POW, REAL_LT]); 1354 1355val REAL_POW_LE_1 = store_thm( 1356 "REAL_POW_LE_1", 1357 ���!(n:num) (x:real). (&1:real) <= x ==> (&1:real) <= x pow n���, 1358 INDUCT_TAC THENL 1359 [REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[pow, REAL_LE_REFL], 1360 GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [pow] THEN 1361 GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] [] THEN 1362 MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[REAL_LE_01] THEN 1363 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]); 1364 1365val REAL_POW_MONO = store_thm ( 1366 "REAL_POW_MONO", 1367 ���!(m:num) n x. &1 <= x /\ m <= n ==> x pow m <= x pow n���, 1368 REPEAT GEN_TAC THEN REWRITE_TAC[LESS_EQ_EXISTS] THEN 1369 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1370 DISCH_THEN(X_CHOOSE_THEN ���d:num��� SUBST1_TAC) THEN 1371 REWRITE_TAC[REAL_POW_ADD] THEN 1372 GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] [] THEN 1373 MATCH_MP_TAC REAL_LE_LMUL_IMP THEN CONJ_TAC THENL 1374 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���&1��� THEN 1375 RW_TAC arith_ss [REAL_OF_NUM_LE] THEN 1376 MATCH_MP_TAC REAL_POW_LE_1 THEN ASM_REWRITE_TAC[], 1377 MATCH_MP_TAC REAL_POW_LE_1 THEN ASM_REWRITE_TAC[]]); 1378 1379val REAL_LE_INV2 = store_thm ("REAL_LE_INV2", 1380 ���!x y. (&0:real) < x /\ x <= y ==> inv(y) <= inv(x)���, 1381 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT] THEN 1382 ASM_CASES_TAC ���x:real = y��� THEN ASM_REWRITE_TAC[] THEN 1383 STRIP_TAC THEN DISJ1_TAC THEN MATCH_MP_TAC REAL_LT_INV THEN 1384 ASM_REWRITE_TAC[]); 1385 1386val GAUGE_MIN_FINITE = store_thm("GAUGE_MIN_FINITE", 1387 ``!s gs n. (!m:num. m <= n ==> gauge s (gs m)) 1388 ==> ?g. gauge s g /\ 1389 !d p. fine g (d,p) ==> !m. m <= n ==> fine (gs m) (d,p)``, 1390 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THENL 1391 [MESON_TAC[LE], 1392 REWRITE_TAC[LE] THEN 1393 REWRITE_TAC[TAUT_CONV ``(a \/ b ==> c) = ((a ==> c) /\ (b ==> c))``] THEN 1394 SIMP_TAC arith_ss[FORALL_AND_THM, LEFT_FORALL_IMP_THM, EXISTS_REFL] THEN 1395 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o assert (is_imp o concl)) THEN 1396 ASM_REWRITE_TAC[] THEN 1397 DISCH_THEN(X_CHOOSE_THEN ``gm:real->real`` STRIP_ASSUME_TAC) THEN 1398 EXISTS_TAC ``\x:real. if gm x < 1399 gs(SUC n) x then gm x else gs(SUC n) x`` THEN 1400 SUBGOAL_THEN``gauge s (\x:real. if gm x < 1401 gs(SUC n) x then gm x else gs(SUC n) x)``ASSUME_TAC THENL 1402 [MATCH_MP_TAC GAUGE_MIN THEN ASM_REWRITE_TAC[], 1403 ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN 1404 DISCH_THEN(MP_TAC o MATCH_MP FINE_MIN) THEN 1405 ASM_SIMP_TAC arith_ss[ETA_AX]]]); 1406 1407val INTEGRABLE_CAUCHY = store_thm("INTEGRABLE_CAUCHY", 1408 ``!f a b. integrable(a,b) f <=> 1409 !e. &0 < e 1410 ==> ?g. gauge (\x. a <= x /\ x <= b) g /\ 1411 !d1 p1 d2 p2. 1412 tdiv (a,b) (d1,p1) /\ fine g (d1,p1) /\ 1413 tdiv (a,b) (d2,p2) /\ fine g (d2,p2) 1414 ==> abs (rsum(d1,p1) f - rsum(d2,p2) f) < e``, 1415 REPEAT GEN_TAC THEN REWRITE_TAC[integrable] THEN EQ_TAC THENL 1416 [REWRITE_TAC[Dint] THEN DISCH_THEN(X_CHOOSE_TAC ``i:real``) THEN 1417 X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1418 FIRST_X_ASSUM(MP_TAC o SPEC ``e / &2``) THEN 1419 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT] THEN 1420 HO_MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC ``g:real->real`` THEN 1421 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 1422 MAP_EVERY X_GEN_TAC 1423 [``d1:num->real``, ``p1:num->real``, 1424 ``d2:num->real``, ``p2:num->real``] THEN STRIP_TAC THEN 1425 FIRST_X_ASSUM(fn th => 1426 MP_TAC(SPECL [``d1:num->real``, ``p1:num->real``] th) THEN 1427 MP_TAC(SPECL [``d2:num->real``, ``p2:num->real``] th)) THEN 1428 ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN 1429 ONCE_REWRITE_TAC[REAL_ARITH``abs(a - b) = abs(a - i + -(b - i))``] THEN 1430 MATCH_MP_TAC REAL_LET_TRANS THEN 1431 EXISTS_TAC``abs(rsum(d1,p1) f -i) + abs(-(rsum(d2,p2) f - i))`` THEN 1432 REWRITE_TAC[ABS_TRIANGLE] THEN REWRITE_TAC[ABS_NEG] THEN 1433 GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_HALF_DOUBLE] THEN 1434 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[],ALL_TAC] THEN 1435 DISCH_TAC THEN DISJ_CASES_TAC(REAL_ARITH ``b < a \/ a <= b``) THENL 1436 [ASM_MESON_TAC[DINT_WRONG], ALL_TAC] THEN 1437 FIRST_X_ASSUM(MP_TAC o GEN ``n:num`` o SPEC ``&1 / &2 pow n``) THEN 1438 SIMP_TAC arith_ss[REAL_LT_DIV, REAL_POW_LT, REAL_LT] THEN 1439 SIMP_TAC arith_ss[FORALL_AND_THM, SKOLEM_THM] THEN 1440 DISCH_THEN(X_CHOOSE_THEN ``g:num->real->real`` STRIP_ASSUME_TAC) THEN 1441 MP_TAC(GEN ``n:num`` 1442 (SPECL [``\x. a <= x /\ x <= b``, ``g:num->real->real``, ``n:num``] 1443 GAUGE_MIN_FINITE)) THEN 1444 ASM_SIMP_TAC arith_ss[SKOLEM_THM, FORALL_AND_THM] THEN 1445 DISCH_THEN(X_CHOOSE_THEN ``G:num->real->real`` STRIP_ASSUME_TAC) THEN 1446 MP_TAC(GEN ``n:num`` 1447 (SPECL [``a:real``, ``b:real``, 1448 ``(G:num->real->real) n``] DIVISION_EXISTS)) THEN 1449 ASM_SIMP_TAC bool_ss[SKOLEM_THM,GSYM LEFT_FORALL_IMP_THM, 1450 FORALL_AND_THM] THEN 1451 MAP_EVERY X_GEN_TAC [``d:num->num->real``, ``p:num->num->real``] THEN 1452 STRIP_TAC THEN 1453 SUBGOAL_THEN ``cauchy (\n. rsum(d n,p n) f)`` MP_TAC THENL 1454 [REWRITE_TAC[cauchy] THEN X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1455 MP_TAC(SPEC ``&1 / e`` REAL_ARCH_POW2) THEN 1456 HO_MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC ``N:num`` THEN 1457 ASM_SIMP_TAC arith_ss[REAL_LT_LDIV_EQ] THEN DISCH_TAC THEN 1458 REWRITE_TAC[GREATER_EQ] THEN 1459 MAP_EVERY X_GEN_TAC [``m:num``,``n:num``] THEN STRIP_TAC THEN 1460 FIRST_X_ASSUM(MP_TAC o SPECL 1461 [``N:num``, ``(d:num->num->real) m``, ``(p:num->num->real) m``, 1462 ``(d:num->num->real) n``, ``(p:num->num->real) n``]) THEN 1463 SUBGOAL_THEN 1464 ``tdiv (a,b) ((d:num->num->real) m,(p:num->num->real) m) /\ 1465 fine ((g:num->real->real) N) (d m,p m) /\ tdiv (a,b) (d n,p n) /\ 1466 fine (g N) (d n,p n)``ASSUME_TAC THENL 1467 [ASM_MESON_TAC[],ALL_TAC] THEN 1468 ASM_REWRITE_TAC[] THEN 1469 MATCH_MP_TAC(REAL_ARITH ``d < e ==> x < d ==> x < e``) THEN 1470 ASM_SIMP_TAC arith_ss[REAL_LT_LDIV_EQ, REAL_POW_LT, REAL_LT] THEN 1471 ASM_MESON_TAC[REAL_MUL_SYM], ALL_TAC] THEN 1472 REWRITE_TAC[SEQ_CAUCHY, convergent, SEQ, Dint] THEN 1473 HO_MATCH_MP_TAC MONO_EXISTS THEN 1474 X_GEN_TAC ``i:real`` THEN STRIP_TAC THEN 1475 X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1476 FIRST_X_ASSUM(MP_TAC o SPEC ``e / &2``) THEN 1477 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT] THEN 1478 DISCH_THEN(X_CHOOSE_THEN ``N1:num`` MP_TAC) THEN 1479 X_CHOOSE_TAC ``N2:num`` (SPEC ``&2 / e`` REAL_ARCH_POW2) THEN 1480 DISCH_THEN(MP_TAC o SPEC ``N1 + N2:num``) THEN 1481 REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD] THEN 1482 DISCH_TAC THEN EXISTS_TAC ``(G:num->real->real)(N1 + N2)`` THEN 1483 ASM_REWRITE_TAC[] THEN 1484 MAP_EVERY X_GEN_TAC [``dx:num->real``, ``px:num->real``] THEN 1485 STRIP_TAC THEN 1486 FIRST_X_ASSUM(MP_TAC o SPECL 1487 [``N1 + N2:num``, ``dx:num->real``, ``px:num->real``, 1488 ``(d:num->num->real)(N1 + N2)``, ``(p:num->num->real)(N1 + N2)``]) THEN 1489 SUBGOAL_THEN``tdiv (a,b) (dx,px) /\ fine (g ((N1:num) + N2)) (dx,px) /\ 1490 tdiv (a,b) (d (N1 + N2),p (N1 + N2)) /\ 1491 fine (g ((N1:num) + N2)) (d (N1 + N2),p (N1 + N2))``ASSUME_TAC THENL 1492 [ASM_MESON_TAC[LESS_EQ_REFL], ALL_TAC] THEN ASM_REWRITE_TAC[] THEN 1493 SUBGOAL_THEN``1 / 2 pow ((N1:num)+ N2) < e / &2``ASSUME_TAC THENL 1494 [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC``inv(&2 / e)`` THEN 1495 CONJ_TAC THENL 1496 [REWRITE_TAC[GSYM REAL_INV_1OVER] THEN MATCH_MP_TAC REAL_LT_INV THEN 1497 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT] THEN 1498 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC ``&2 pow N2`` THEN 1499 ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_POW_ADD] THEN 1500 GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] [] THEN 1501 MATCH_MP_TAC REAL_LE_RMUL_IMP THEN REWRITE_TAC[POW_2_LE1] THEN 1502 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC``&1`` THEN 1503 REWRITE_TAC[REAL_LE_01,POW_2_LE1], 1504 MATCH_MP_TAC REAL_EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN 1505 MATCH_MP_TAC REAL_LINV_UNIQ THEN 1506 REWRITE_TAC[REAL_DIV_INNER_CANCEL2] THEN 1507 MATCH_MP_TAC REAL_DIV_REFL THEN MATCH_MP_TAC REAL_POS_NZ THEN 1508 ASM_REWRITE_TAC[]], 1509 DISCH_TAC THEN 1510 SUBGOAL_THEN`` 1511 abs (rsum (dx,px) f - rsum ((d :num -> num -> real) (N1 + N2), 1512 p (N1 + N2)) f) < e / &2``ASSUME_TAC THENL 1513 [MATCH_MP_TAC REAL_LT_TRANS THEN 1514 EXISTS_TAC``1 / &2 pow(N1 + N2)`` THEN 1515 ASM_REWRITE_TAC[],ALL_TAC] THEN 1516 MATCH_MP_TAC REAL_LET_TRANS THEN 1517 EXISTS_TAC``abs((rsum(dx,px) f - 1518 rsum((d:num->num->real)(N1 + N2),p(N1 + N2)) f) 1519 + (rsum((d:num->num->real)(N1 + N2),p(N1 + N2)) f - i))`` THEN 1520 CONJ_TAC THENL 1521 [REWRITE_TAC[real_sub, REAL_ADD_ASSOC] THEN 1522 REWRITE_TAC[GSYM real_sub] THEN 1523 SIMP_TAC arith_ss[REAL_SUB_ADD,REAL_LE_REFL], 1524 MATCH_MP_TAC REAL_LET_TRANS THEN 1525 EXISTS_TAC``abs(rsum(dx,px) f - 1526 rsum((d:num->num->real)(N1 + N2),p(N1 + N2)) f) 1527 + abs(rsum((d:num->num->real)(N1 + N2),p(N1 + N2)) f - i)`` THEN 1528 SIMP_TAC arith_ss[REAL_ABS_TRIANGLE] THEN 1529 GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_HALF_DOUBLE] THEN 1530 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[]]]); 1531 1532(* ------------------------------------------------------------------------- *) 1533(* Limit theorem. *) 1534(* ------------------------------------------------------------------------- *) 1535 1536val SUM_DIFFS = store_thm("SUM_DIFFS", 1537 ���!m n. sum(m,n) (\i. d(SUC i) - d(i)) = d(m + n) - d m���, 1538 GEN_TAC THEN INDUCT_TAC THEN 1539 ASM_REWRITE_TAC[sum, ADD_CLAUSES, REAL_SUB_REFL] THEN REWRITE_TAC[sum] THEN 1540 RW_TAC arith_ss[ETA_AX] THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN 1541 SUBGOAL_THEN���!a b c d. a-b+(c-a) = -b+a+(c-a)��� 1542 (fn th => ONCE_REWRITE_TAC[GEN_ALL th]) THENL 1543 [REPEAT GEN_TAC THEN REWRITE_TAC[real_sub] THEN 1544 ASM_SIMP_TAC arith_ss[GSYM REAL_ADD_SYM], 1545 SUBGOAL_THEN���!a b c d. a+b+(c-b) = a+c��� 1546 (fn th => ONCE_REWRITE_TAC[GEN_ALL th]) THENL 1547 [REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN 1548 REWRITE_TAC[REAL_EQ_LADD] THEN 1549 REWRITE_TAC[REAL_SUB_ADD2], REWRITE_TAC[real_sub] THEN 1550 GEN_REWR_TAC LAND_CONV [REAL_ADD_COMM] THEN PROVE_TAC[]]]); 1551 1552val RSUM_BOUND = store_thm("RSUM_BOUND", 1553 ``!a b d p e f. 1554 tdiv(a,b) (d,p) /\ 1555 (!x. a <= x /\ x <= b ==> abs(f x) <= e) 1556 ==> abs(rsum(d,p) f) <= e * (b - a)``, 1557 REPEAT STRIP_TAC THEN REWRITE_TAC[rsum] THEN MATCH_MP_TAC REAL_LE_TRANS THEN 1558 EXISTS_TAC (Term`sum(0,dsize d) (\i. abs(f(p i :real) * (d(SUC i) - d i)))`) THEN 1559 SIMP_TAC arith_ss[SUM_ABS_LE] THEN MATCH_MP_TAC REAL_LE_TRANS THEN 1560 EXISTS_TAC (Term`sum(0,dsize d) (\i. e * abs(d(SUC i) - d(i)))`) THEN 1561 CONJ_TAC THENL 1562 [MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[ADD_CLAUSES, REAL_ABS_MUL] THEN 1563 X_GEN_TAC (Term`r:num`) THEN STRIP_TAC THEN BETA_TAC THEN 1564 MATCH_MP_TAC REAL_LE_RMUL1 THEN REWRITE_TAC[REAL_ABS_POS] THEN 1565 FIRST_X_ASSUM MATCH_MP_TAC THEN 1566 ASM_MESON_TAC[tdiv, DIVISION_UBOUND, DIVISION_LBOUND, REAL_LE_TRANS], 1567 ALL_TAC] THEN 1568 SIMP_TAC arith_ss[SUM_CMUL] THEN MATCH_MP_TAC REAL_LE_LMUL1 THEN 1569 CONJ_TAC THENL 1570 [FIRST_X_ASSUM(MP_TAC o SPEC (Term`a:real`)) THEN 1571 ASM_MESON_TAC[REAL_LE_REFL, REAL_ABS_POS, REAL_LE_TRANS, DIVISION_LE, 1572 tdiv], ALL_TAC] THEN 1573 FIRST_X_ASSUM(CONJUNCTS_THEN ASSUME_TAC o REWRITE_RULE[tdiv]) THEN 1574 FIRST_ASSUM(ASSUME_TAC o MATCH_MP DIVISION_LE_SUC) THEN 1575 ASM_REWRITE_TAC[abs, REAL_SUB_LE, SUM_DIFFS, ADD_CLAUSES] THEN 1576 PROVE_TAC[DIVISION_RHS, DIVISION_LHS, REAL_LE_REFL]); 1577 1578val RSUM_DIFF_BOUND = store_thm ("RSUM_DIFF_BOUND", 1579 ``!a b d p e f g. 1580 tdiv(a,b) (d,p) /\ 1581 (!x. a <= x /\ x <= b ==> abs(f x - g x) <= e) 1582 ==> abs(rsum (d,p) f - rsum (d,p) g) <= e * (b - a)``, 1583 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o HO_MATCH_MP RSUM_BOUND) THEN 1584 SIMP_TAC bool_ss[rsum, SUM_SUB, REAL_SUB_RDISTRIB]); 1585 1586val INTEGRABLE_LIMIT = store_thm("INTEGRABLE_LIMIT", 1587 ``!f a b. (!e. &0 < e 1588 ==> ?g. (!x. a <= x /\ x <= b ==> abs(f x - g x) <= e) /\ 1589 integrable(a,b) g) 1590 ==> integrable(a,b) f``, 1591 REPEAT STRIP_TAC THEN ASM_CASES_TAC ``a <= b`` THENL 1592 [FIRST_X_ASSUM(MP_TAC o GEN ``n:num`` o SPEC ``&1 / &2 pow n``) THEN 1593 SIMP_TAC arith_ss[REAL_LT_DIV, REAL_POW_LT, REAL_LT] THEN 1594 SIMP_TAC arith_ss[FORALL_AND_THM, SKOLEM_THM, integrable] THEN 1595 DISCH_THEN(X_CHOOSE_THEN ``g:num->real->real`` (CONJUNCTS_THEN2 1596 ASSUME_TAC (X_CHOOSE_TAC ``i:num->real``))) THEN 1597 SUBGOAL_THEN ``cauchy i`` MP_TAC THENL 1598 [REWRITE_TAC[cauchy] THEN X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1599 MP_TAC(SPEC ``(&2 * &2 * (b - a)) / e`` REAL_ARCH_POW2) THEN 1600 HO_MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC ``N:num`` THEN DISCH_TAC THEN 1601 MAP_EVERY X_GEN_TAC [``m:num``, ``n:num``] THEN REWRITE_TAC[GREATER_EQ] THEN 1602 STRIP_TAC THEN UNDISCH_TAC``!(n:num). Dint(a,b) (g n) (i n)`` THEN 1603 REWRITE_TAC[Dint] THEN SIMP_TAC bool_ss[Once SWAP_FORALL_THM] THEN 1604 DISCH_THEN(MP_TAC o SPEC ``e / &2 / &2``) THEN 1605 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT] THEN 1606 DISCH_THEN(fn th => MP_TAC(SPEC ``m:num`` th) THEN 1607 MP_TAC(SPEC ``n:num`` th)) THEN 1608 DISCH_THEN(X_CHOOSE_THEN ``gn:real->real`` STRIP_ASSUME_TAC) THEN 1609 DISCH_THEN(X_CHOOSE_THEN ``gm:real->real`` STRIP_ASSUME_TAC) THEN 1610 MP_TAC(SPECL [``a:real``, ``b:real``, 1611 ``\x:real. if gm x < gn x then gm x else gn x``] 1612 DIVISION_EXISTS) THEN 1613 ASM_SIMP_TAC arith_ss[GAUGE_MIN, GSYM LEFT_FORALL_IMP_THM] THEN 1614 MAP_EVERY X_GEN_TAC [``d:num->real``, ``p:num->real``] THEN 1615 STRIP_TAC THEN 1616 FIRST_X_ASSUM(CONJUNCTS_THEN ASSUME_TAC o MATCH_MP FINE_MIN) THEN 1617 REPEAT(FIRST_X_ASSUM(MP_TAC o SPECL [``d:num->real``, 1618 ``p:num->real``])) THEN 1619 ASM_REWRITE_TAC[] THEN 1620 SUBGOAL_THEN ``abs(rsum(d,p) (g(m:num)) - rsum(d,p) (g n)) <= e / &2`` 1621 (fn th => MP_TAC th) THENL 1622 [MATCH_MP_TAC REAL_LE_TRANS THEN 1623 EXISTS_TAC ``&2 / &2 pow N * (b - a)`` THEN 1624 CONJ_TAC THENL 1625 [MATCH_MP_TAC RSUM_DIFF_BOUND THEN ASM_REWRITE_TAC[] THEN 1626 REPEAT STRIP_TAC THEN REWRITE_TAC[real_div] THEN 1627 HO_MATCH_MP_TAC(REAL_ARITH 1628 ``!f. abs(f - gm) <= inv(k) /\ abs(f - gn) <= inv(k) 1629 ==> (abs(gm - gn) <= &2*inv(k))``) THEN 1630 EXISTS_TAC ``(f:real->real) x`` THEN CONJ_TAC THEN 1631 MATCH_MP_TAC REAL_LE_TRANS THENL 1632 [EXISTS_TAC ``&1 / &2 pow m``,EXISTS_TAC``&1 / &2 pow n``] THEN 1633 ASM_SIMP_TAC arith_ss[] THEN REWRITE_TAC[real_div, REAL_MUL_LID] THEN 1634 MATCH_MP_TAC REAL_LE_INV2 THEN 1635 ASM_SIMP_TAC arith_ss[REAL_POW_LT, REAL_POW_MONO, REAL_LE,REAL_LT], 1636 MATCH_MP_TAC REAL_LE_RDIV THEN CONJ_TAC THENL 1637 [REAL_ARITH_TAC, GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] [] THEN 1638 ONCE_REWRITE_TAC[REAL_MUL_ASSOC] THEN REWRITE_TAC [real_div] THEN 1639 REWRITE_TAC [REAL_MUL_ASSOC] THEN 1640 ONCE_REWRITE_TAC [GSYM REAL_MUL_ASSOC] THEN 1641 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [] [REAL_MUL_SYM] THEN 1642 REWRITE_TAC [REAL_MUL_ASSOC] THEN REWRITE_TAC [GSYM real_div] THEN 1643 ASM_SIMP_TAC arith_ss[REAL_LE_LDIV_EQ, REAL_POW_LT, REAL_LT] THEN 1644 GEN_REWRITE_TAC RAND_CONV [] [REAL_MUL_SYM] THEN 1645 ASM_SIMP_TAC arith_ss[GSYM REAL_LE_LDIV_EQ, REAL_LT_IMP_LE]]], 1646 REPEAT STRIP_TAC THEN 1647 SUBGOAL_THEN ``abs(rsum(d,p) (g(m:num)) - rsum(d,p) (g n) - 1648 (i m - i n)) < e / &2``(fn th => MP_TAC th) THENL 1649 [SUBGOAL_THEN���!a b c d. a-b-(c-d) = a-c - (b-d)��� 1650 (fn th => ONCE_REWRITE_TAC[GEN_ALL th]) THENL 1651 [REAL_ARITH_TAC, ALL_TAC] THEN 1652 MATCH_MP_TAC REAL_LET_TRANS THEN 1653 EXISTS_TAC``abs(rsum(d,p)(g (m:num)) - i m) 1654 + abs(rsum(d,p) (g n) - i n)`` THEN CONJ_TAC THENL 1655 [GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [] [real_sub] THEN 1656 GEN_REWRITE_TAC (funpow 2 RAND_CONV) [] [GSYM ABS_NEG] THEN 1657 MATCH_ACCEPT_TAC ABS_TRIANGLE, 1658 GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_HALF_DOUBLE] THEN 1659 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[]], 1660 DISCH_TAC THEN 1661 ABBREV_TAC``s = rsum(d,p)(g (m:num)) - rsum(d,p) (g n)`` THEN 1662 ABBREV_TAC``t= s- (i (m:num) - i n)`` THEN POP_ASSUM MP_TAC THEN 1663 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [real_sub] [] THEN 1664 ONCE_REWRITE_TAC [GSYM REAL_ADD_SYM] THEN 1665 ONCE_REWRITE_TAC [GSYM REAL_EQ_SUB_LADD] THEN 1666 ONCE_REWRITE_TAC [REAL_NEG_EQ] THEN ONCE_REWRITE_TAC [REAL_NEG_SUB] THEN 1667 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[real_sub] THEN 1668 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC``abs s + abs (-t)`` THEN 1669 REWRITE_TAC[ABS_TRIANGLE] THEN 1670 GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_HALF_DOUBLE] THEN 1671 MATCH_MP_TAC REAL_LET_ADD2 THEN PROVE_TAC[ABS_NEG]]], 1672 REWRITE_TAC[SEQ_CAUCHY, convergent] THEN 1673 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC ``s:real`` THEN DISCH_TAC THEN 1674 REWRITE_TAC[Dint] THEN X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1675 FIRST_X_ASSUM(MP_TAC o SPEC ``e / &3`` o REWRITE_RULE[SEQ]) THEN 1676 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT, GREATER_EQ] THEN 1677 DISCH_THEN(X_CHOOSE_TAC ``N1:num``) THEN 1678 MP_TAC(SPEC ``(&3 * (b - a)) / e`` REAL_ARCH_POW2) THEN 1679 DISCH_THEN(X_CHOOSE_TAC ``N2:num``) THEN 1680 UNDISCH_TAC``!(n:num). Dint(a,b) (g (n:num)) ( i n)`` THEN 1681 REWRITE_TAC[Dint] THEN 1682 DISCH_THEN(MP_TAC o SPECL [``N1 + N2:num``, ``e / &3``]) THEN 1683 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT] THEN 1684 HO_MATCH_MP_TAC MONO_EXISTS THEN 1685 X_GEN_TAC ``g:real->real`` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 1686 MAP_EVERY X_GEN_TAC [``d:num->real``, ``p:num->real``] THEN STRIP_TAC THEN 1687 FIRST_X_ASSUM(MP_TAC o SPECL [``d:num->real``, ``p:num->real``]) THEN 1688 ASM_REWRITE_TAC[] THEN SUBGOAL_THEN``N1:num <= N1 + N2``MP_TAC THENL 1689 [REWRITE_TAC[LESS_EQ_ADD], ALL_TAC] THEN DISCH_TAC THEN 1690 SUBGOAL_THEN``abs(i ((N1:num) + N2) - s) < e/3``MP_TAC THENL 1691 [ASM_MESON_TAC[], ALL_TAC] THEN REPEAT DISCH_TAC THEN 1692 SUBGOAL_THEN``abs(rsum(d,p) f - rsum(d,p) 1693 (g ((N1:num) + N2))) <= e/ &3``MP_TAC THENL 1694 [MATCH_MP_TAC REAL_LE_TRANS THEN 1695 EXISTS_TAC ``&1 / &2 pow (N1 + N2) * (b - a)`` THEN CONJ_TAC THENL 1696 [MATCH_MP_TAC RSUM_DIFF_BOUND THEN ASM_REWRITE_TAC[], 1697 MATCH_MP_TAC REAL_LE_RDIV THEN CONJ_TAC THENL 1698 [REAL_ARITH_TAC, 1699 GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] [] THEN 1700 ONCE_REWRITE_TAC[REAL_MUL_ASSOC] THEN REWRITE_TAC [real_div] THEN 1701 REWRITE_TAC [REAL_MUL_ASSOC] THEN 1702 ONCE_REWRITE_TAC [GSYM REAL_MUL_ASSOC] THEN 1703 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [] [REAL_MUL_SYM] THEN 1704 REWRITE_TAC [REAL_MUL_ASSOC] THEN REWRITE_TAC [GSYM real_div] THEN 1705 ASM_SIMP_TAC arith_ss[REAL_LE_LDIV_EQ, REAL_POW_LT, REAL_LT] THEN 1706 GEN_REWRITE_TAC RAND_CONV [] [REAL_MUL_SYM] THEN 1707 REWRITE_TAC[REAL_MUL_RID] THEN 1708 ASM_SIMP_TAC arith_ss[GSYM REAL_LE_LDIV_EQ, REAL_LT_IMP_LE] THEN 1709 SUBGOAL_THEN``N2:num <= N1 + N2``MP_TAC THENL 1710 [ONCE_REWRITE_TAC[ADD_COMM] THEN REWRITE_TAC[LESS_EQ_ADD], 1711 DISCH_TAC THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN 1712 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC``2 pow N2`` THEN 1713 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_POW_MONO THEN 1714 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]]], 1715 DISCH_TAC THEN ABBREV_TAC``sf = rsum(d,p) f`` THEN 1716 ABBREV_TAC``sg = rsum(d,p) (g ((N1:num) + N2))`` THEN 1717 SUBGOAL_THEN``abs(sf - i((N1:num) + N2)) < 2*e/3``MP_TAC THENL 1718 [MATCH_MP_TAC REAL_LET_TRANS THEN 1719 EXISTS_TAC``abs(sf - sg) + abs(sg - i((N1:num)+ N2))`` THEN 1720 CONJ_TAC THENL 1721 [MATCH_MP_TAC REAL_LE_TRANS THEN 1722 EXISTS_TAC``abs((sf - sg) + (sg - i((N1:num) + N2)))`` THEN 1723 REWRITE_TAC[ABS_TRIANGLE] THEN REAL_ARITH_TAC, 1724 REWRITE_TAC[real_div, GSYM REAL_MUL_ASSOC] THEN 1725 REWRITE_TAC[GSYM REAL_DOUBLE, GSYM real_div] THEN 1726 PROVE_TAC[REAL_LET_ADD2]], 1727 ONCE_REWRITE_TAC [GSYM REAL_NEG_THIRD] THEN DISCH_TAC THEN 1728 MATCH_MP_TAC REAL_LET_TRANS THEN 1729 EXISTS_TAC``abs((sf - i((N1:num) + N2)) + (i((N1:num) + N2) - s))`` THEN 1730 CONJ_TAC THENL 1731 [REAL_ARITH_TAC, MATCH_MP_TAC REAL_LET_TRANS THEN 1732 EXISTS_TAC``abs((sf - i((N1:num) + N2))) + 1733 abs((i((N1:num) + N2) - s))`` THEN REWRITE_TAC[ABS_TRIANGLE] THEN 1734 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC``(e - e / 3) + e/3`` THEN 1735 CONJ_TAC THENL [PROVE_TAC[REAL_LT_ADD2],REAL_ARITH_TAC]]]]], 1736 ASM_MESON_TAC[REAL_NOT_LE, DINT_WRONG, integrable]]); 1737 1738(* ------------------------------------------------------------------------- *) 1739(* Hence continuous functions are integrable. *) 1740(* ------------------------------------------------------------------------- *) 1741 1742val INTEGRABLE_CONST = store_thm("INTEGRABLE_CONST", 1743 ���!a b c. integrable(a,b) (\x. c)���, 1744 REWRITE_TAC[integrable] THEN REPEAT GEN_TAC THEN 1745 EXISTS_TAC(Term`c*(b-a):real`) THEN SIMP_TAC arith_ss[DINT_CONST]); 1746 1747val INTEGRABLE_ADD = store_thm("INTEGRABLE_ADD", 1748 ``!f g a b. a<=b /\ integrable(a,b) f /\ integrable(a,b) g ==> 1749 integrable(a,b)(\x. f x + g x)``, 1750 RW_TAC std_ss[] THEN REWRITE_TAC[integrable] THEN 1751 EXISTS_TAC``integral(a,b) f + integral(a,b) g`` THEN 1752 MATCH_MP_TAC DINT_ADD THEN CONJ_TAC THEN 1753 MATCH_MP_TAC INTEGRABLE_DINT THEN ASM_REWRITE_TAC[]); 1754 1755val INTEGRABLE_CMUL = store_thm("INTEGRABLE_CMUL", 1756 ``!f a b c. a<=b /\ integrable(a,b) f ==> integrable(a,b)(\x. c* f x)``, 1757 RW_TAC std_ss[] THEN REWRITE_TAC[integrable] THEN 1758 EXISTS_TAC``c*integral(a,b)f`` THEN HO_MATCH_MP_TAC DINT_CMUL THEN 1759 MATCH_MP_TAC INTEGRABLE_DINT THEN ASM_REWRITE_TAC[]); 1760 1761val INTEGRABLE_COMBINE = store_thm("INTEGRABLE_COMBINE", 1762 ``!f a b c. a <= b /\ b <= c /\ integrable(a,b) f /\ integrable(b,c) f 1763 ==> integrable(a,c) f``, 1764 REWRITE_TAC[integrable] THEN MESON_TAC[DINT_COMBINE]); 1765 1766val INTEGRABLE_POINT_SPIKE = store_thm("INTEGRABLE_POINT_SPIKE", 1767 ``!f g a b c. 1768 (!x. a <= x /\ x <= b /\ ~(x = c) ==> (f x = g x)) /\ integrable(a,b) f 1769 ==> integrable(a,b) g``, 1770 REWRITE_TAC[integrable] THEN MESON_TAC[DINT_POINT_SPIKE]); 1771 1772 1773(*INTEGRABLE_CONTINUOUS*) 1774 1775val SUP_INTERVAL = store_thm("SUP_INTERVAL", 1776 ``!P a b. 1777 (?x. a <= x /\ x <= b /\ P x) 1778 ==> ?s. a <= s /\ s <= b /\ 1779 !y. y < s <=> (?x. a <= x /\ x <= b /\ P x /\ y < x)``, 1780 REPEAT STRIP_TAC THEN 1781 MP_TAC(SPEC ``\x. a <= x /\ x <= b /\ P x`` REAL_SUP) THEN 1782 SUBGOAL_THEN``(?x. (\x. a <= x /\ x <= b /\ P x) x) /\ 1783 (?z. !x. (\x. a <= x /\ x <= b /\ P x) x ==> x < z)``MP_TAC THENL 1784 [CONJ_TAC THENL 1785 [BETA_TAC THEN EXISTS_TAC``x:real`` THEN ASM_REWRITE_TAC[], 1786 BETA_TAC THEN EXISTS_TAC``(b+1:real)`` THEN REPEAT STRIP_TAC THEN 1787 ASM_SIMP_TAC arith_ss[REAL_LT_ADD1]], 1788 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 1789 ABBREV_TAC ``s = sup (\x. a <= x /\ x <= b /\ P x)`` THEN 1790 DISCH_TAC THEN EXISTS_TAC ``s:real`` THEN 1791 ASM_MESON_TAC[REAL_LTE_TRANS, REAL_NOT_LE, REAL_LT_ANTISYM]]); 1792 1793val BOLZANO_LEMMA_ALT = store_thm("BOLZANO_LEMMA_ALT", 1794 ``!P. (!a b c. a <= b /\ b <= c /\ P a b /\ P b c ==> P a c) /\ 1795 (!x. ?d. &0 < d /\ (!a b. a <= x /\ x <= b /\ b - a < d ==> P a b)) 1796 ==> !a b. a <= b ==> P a b``, 1797 GEN_TAC THEN MP_TAC(SPEC ``\(x:real,y:real). P x y :bool`` BOLZANO_LEMMA) THEN 1798 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN REWRITE_TAC[]); 1799 1800val CONT_UNIFORM = store_thm("CONT_UNIFORM", 1801 ``!f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) 1802 ==> !e. &0 < e ==> ?d. &0 < d /\ 1803 !x y. a <= x /\ x <= b /\ 1804 a <= y /\ y <= b /\ 1805 abs(x - y) < d 1806 ==> abs(f(x) - f(y)) < e``, 1807 REPEAT STRIP_TAC THEN 1808 MP_TAC(SPEC ``\c. ?d. &0 < d /\ 1809 !x y. a <= x /\ x <= c /\ 1810 a <= y /\ y <= c /\ 1811 abs(x - y) < d 1812 ==> abs(f(x) - f(y)) < e`` 1813 SUP_INTERVAL) THEN 1814 DISCH_THEN(MP_TAC o SPECL [``a:real``, ``b:real``]) THEN 1815 SUBGOAL_THEN``?x. 1816 a <= x /\ x <= b /\ 1817 (\c. 1818 ?d. 1819 0 < d /\ 1820 !x y. 1821 a <= x /\ x <= c /\ a <= y /\ y <= c /\ abs (x - y) < d ==> 1822 abs (f x - f y) < e) x``ASSUME_TAC THENL 1823 [EXISTS_TAC ``a:real`` THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN 1824 BETA_TAC THEN EXISTS_TAC ``&1`` THEN SIMP_TAC arith_ss[REAL_LT] THEN 1825 ASM_MESON_TAC[REAL_LE_ANTISYM, REAL_ARITH ``abs(x - x) = &0``], 1826 ALL_TAC] THEN 1827 ASM_SIMP_TAC arith_ss[] THEN 1828 DISCH_THEN(X_CHOOSE_THEN ``s:real`` STRIP_ASSUME_TAC) THEN 1829 SUBGOAL_THEN ``?t. s < t /\ ?d. &0 < d /\ 1830 !x y. a <= x /\ x <= t /\ a <= y /\ y <= t /\ 1831 abs(x - y) < d ==> abs(f(x) - f(y)) < e`` 1832 MP_TAC THENL 1833 [UNDISCH_TAC ``!x. a <= x /\ x <= b ==> f contl x`` THEN 1834 DISCH_THEN(MP_TAC o SPEC ``s:real``) THEN ASM_REWRITE_TAC[] THEN 1835 REWRITE_TAC[CONTL_LIM, LIM] THEN DISCH_THEN(MP_TAC o SPEC ``e / &2``) THEN 1836 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT] THEN 1837 DISCH_THEN(X_CHOOSE_THEN ``d1:real`` STRIP_ASSUME_TAC) THEN 1838 SUBGOAL_THEN ``&0 < d1 / &2 /\ d1 / &2 < d1`` STRIP_ASSUME_TAC THENL 1839 [ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT, REAL_LT_LDIV_EQ, 1840 REAL_ARITH ``(d < d * &2) = (&0 < d)``], ALL_TAC] THEN 1841 SUBGOAL_THEN ``!x y. abs(x - s) < d1 /\ abs(y - s) < d1 1842 ==> abs(f(x) - f(y)) < e`` ASSUME_TAC THENL 1843 [REPEAT STRIP_TAC THEN 1844 GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_HALF_DOUBLE] THEN 1845 HO_MATCH_MP_TAC(REAL_ARITH 1846 ``!a. abs(x - a) < e / &2 /\ abs(y - a) < e / &2 1847 ==> abs(x - y) < e / &2 + e / &2``) THEN 1848 EXISTS_TAC ``(f:real->real) s`` THEN 1849 SUBGOAL_THEN ``!x. abs(x - s) < d1 ==> abs(f x - f s) < e / &2`` 1850 (fn th => ASM_MESON_TAC[th]) THEN 1851 X_GEN_TAC ``u:real`` THEN REPEAT STRIP_TAC THEN 1852 ASM_CASES_TAC ``u:real = s`` THENL 1853 [ASM_SIMP_TAC arith_ss[REAL_SUB_REFL, ABS_N, REAL_LT_DIV, REAL_LT], 1854 ALL_TAC] THEN 1855 ASM_MESON_TAC[REAL_ARITH ``&0 < abs(x - s) <=> ~(x = s)``], 1856 ALL_TAC] THEN 1857 SUBGOAL_THEN ``s - d1 / &2 < s`` MP_TAC THENL 1858 [ASM_REWRITE_TAC[REAL_ARITH ``x - y < x <=> &0 < y``],ALL_TAC] THEN 1859 DISCH_THEN(fn th => FIRST_ASSUM(fn th' => 1860 MP_TAC(GEN_REWRITE_RULE I [][th'] th))) THEN 1861 DISCH_THEN(X_CHOOSE_THEN ``r:real`` MP_TAC) THEN 1862 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1863 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1864 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 1865 DISCH_THEN(X_CHOOSE_THEN ``d2:real`` STRIP_ASSUME_TAC) THEN 1866 MP_TAC(SPECL [``d2:real``, ``d1 / &2``] REAL_DOWN2) THEN 1867 ASM_REWRITE_TAC[] THEN 1868 DISCH_THEN(X_CHOOSE_THEN ``d:real`` STRIP_ASSUME_TAC) THEN 1869 EXISTS_TAC ``s + d / &2`` THEN 1870 ASM_SIMP_TAC arith_ss[REAL_LT_DIV, REAL_LT, 1871 REAL_ARITH ``s < s + d = &0 < d``] THEN 1872 EXISTS_TAC ``d:real`` THEN ASM_REWRITE_TAC[] THEN 1873 MAP_EVERY X_GEN_TAC[``x:real``, ``y:real``] THEN STRIP_TAC THEN 1874 ASM_CASES_TAC ``x <= r /\ y <= r`` THENL 1875 [ASM_MESON_TAC[REAL_LT_TRANS], ALL_TAC] THEN 1876 MATCH_MP_TAC(ASSUME ``!x y. abs(x - s) < d1 /\ abs(y - s) < d1 ==> 1877 abs(f x - f y) < e``) THEN 1878 MATCH_MP_TAC(REAL_ARITH 1879 ``!r t d d12. 1880 ~(x <= r /\ y <= r) /\ 1881 abs(x - y) < d /\ 1882 s - d12 < r /\ t <= s + d /\ 1883 x <= t /\ y <= t /\ &2 * d12 <= e /\ 1884 &2 * d < e ==> abs(x - s) < e /\ abs(y - s) < e``) THEN 1885 MAP_EVERY EXISTS_TAC[``r:real``,``s + d / &2``,``d:real``,``d1 / &2``] THEN 1886 ASM_REWRITE_TAC[REAL_LE_LADD] THEN 1887 SIMP_TAC arith_ss[REAL_DIV_LMUL, REAL_OF_NUM_EQ] THEN 1888 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 1889 SIMP_TAC arith_ss[REAL_LE_LDIV_EQ, GSYM REAL_LT_RDIV_EQ, REAL_LT] THEN 1890 ASM_SIMP_TAC arith_ss[REAL_ARITH ``&0 < d ==> d <= d * &2``, REAL_LE_REFL], 1891 ALL_TAC] THEN 1892 DISCH_THEN(X_CHOOSE_THEN ``t:real`` (CONJUNCTS_THEN ASSUME_TAC)) THEN 1893 SUBGOAL_THEN ``b <= t`` (fn th => ASM_MESON_TAC[REAL_LE_TRANS, th]) THEN 1894 FIRST_X_ASSUM(X_CHOOSE_THEN ``d:real`` STRIP_ASSUME_TAC) THEN 1895 UNDISCH_THEN ``!x. a <= x /\ x <= b ==> f contl x`` (K ALL_TAC) THEN 1896 FIRST_X_ASSUM(MP_TAC o assert(is_eq o concl) o SPEC ``s:real``) THEN 1897 REWRITE_TAC[REAL_LT_REFL] THEN CONV_TAC CONTRAPOS_CONV THEN 1898 REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN EXISTS_TAC ``t:real`` THEN 1899 ASM_MESON_TAC[REAL_LT_IMP_LE, REAL_LE_TRANS]); 1900 1901val INTEGRABLE_CONTINUOUS = store_thm("INTEGRABLE_CONTINUOUS", 1902 ``!f a b. (!x. a <= x /\ x <= b ==> f contl x) ==> integrable(a,b) f``, 1903 REPEAT STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH ``b < a \/ a <= b``) THENL 1904 [ASM_MESON_TAC[integrable, DINT_WRONG], ALL_TAC] THEN 1905 MATCH_MP_TAC INTEGRABLE_LIMIT THEN X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1906 MP_TAC(SPECL[``f:real->real``, ``a:real``, ``b:real``] CONT_UNIFORM) THEN 1907 ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC ``e:real``) THEN 1908 ASM_REWRITE_TAC[] THEN 1909 DISCH_THEN(X_CHOOSE_THEN ``d:real`` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN 1910 UNDISCH_TAC ``a <= b`` THEN MAP_EVERY (fn t => SPEC_TAC(t,t)) 1911 [``b:real``, ``a:real``] THEN 1912 HO_MATCH_MP_TAC BOLZANO_LEMMA_ALT THEN CONJ_TAC THENL 1913 [MAP_EVERY X_GEN_TAC [``u:real``, ``v:real``, ``w:real``] THEN 1914 NTAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN 1915 DISCH_THEN(fn th => DISCH_TAC THEN MP_TAC th) THEN 1916 MATCH_MP_TAC(TAUT_CONV 1917 ``(a /\ b) /\ (c /\ d ==> e) ==> (a ==> c) /\ (b ==> d) ==> e``) THEN 1918 CONJ_TAC THENL [ASM_MESON_TAC[REAL_LE_TRANS], ALL_TAC] THEN 1919 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC ``g:real->real``) 1920 (X_CHOOSE_TAC ``h:real->real``)) THEN 1921 EXISTS_TAC ``\x. if x <= v then g(x):real else h(x)`` THEN 1922 CONJ_TAC THENL 1923 [GEN_TAC THEN DISCH_TAC THEN BETA_TAC THEN COND_CASES_TAC THENL 1924 [ASM_MESON_TAC[REAL_LE_TOTAL],ASM_MESON_TAC[REAL_LE_TOTAL]],ALL_TAC] THEN 1925 MATCH_MP_TAC INTEGRABLE_COMBINE THEN EXISTS_TAC ``v:real`` THEN 1926 ASM_REWRITE_TAC[] THEN CONJ_TAC THEN 1927 MATCH_MP_TAC INTEGRABLE_POINT_SPIKE THENL 1928 [EXISTS_TAC ``g:real->real``, EXISTS_TAC ``h:real->real``] THEN 1929 EXISTS_TAC ``v:real`` THEN ASM_REWRITE_TAC[] THEN SIMP_TAC arith_ss[] THEN 1930 GEN_TAC THEN DISCH_TAC THEN SUBGOAL_THEN``~(x<=v)``ASSUME_TAC THENL 1931 [ASM_MESON_TAC[REAL_ARITH ``b <= x /\ x <= c /\ ~(x = b) ==> ~(x <= b)``], 1932 RW_TAC std_ss[]], ALL_TAC] THEN 1933 X_GEN_TAC ``x:real`` THEN EXISTS_TAC ``d:real`` THEN ASM_REWRITE_TAC[] THEN 1934 MAP_EVERY X_GEN_TAC [``u:real``, ``v:real``] THEN REPEAT STRIP_TAC THEN 1935 EXISTS_TAC ``\x:real. (f:real->real) u`` THEN 1936 ASM_REWRITE_TAC[INTEGRABLE_CONST] THEN 1937 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN 1938 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC std_ss[REAL_LE_REFL] THEN 1939 CONJ_TAC THENL 1940 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC``x:real`` THEN 1941 ASM_REWRITE_TAC[], 1942 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC``(x'-u):real`` THEN 1943 CONJ_TAC THENL 1944 [MATCH_MP_TAC REAL_EQ_IMP_LE THEN ONCE_REWRITE_TAC[ABS_REFL] THEN 1945 ASM_SIMP_TAC arith_ss[REAL_SUB_LE], 1946 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC``(v-u):real`` THEN 1947 ASM_REWRITE_TAC[REAL_LE_SUB_CANCEL2]]]); 1948 1949(* ------------------------------------------------------------------------- *) 1950(* Integrability on a subinterval. *) 1951(* ------------------------------------------------------------------------- *) 1952 1953val INTEGRABLE_SPLIT_SIDES = store_thm("INTEGRABLE_SPLIT_SIDES", 1954 ``!f a b c. 1955 a <= c /\ c <= b /\ integrable(a,b) f 1956 ==> ?i. !e. &0 < e 1957 ==> ?g. gauge(\x. a <= x /\ x <= b) g /\ 1958 !d1 p1 d2 p2. tdiv(a,c) (d1,p1) /\ 1959 fine g (d1,p1) /\ 1960 tdiv(c,b) (d2,p2) /\ 1961 fine g (d2,p2) 1962 ==> abs((rsum(d1,p1) f + 1963 rsum(d2,p2) f) - i) < e``, 1964 REPEAT GEN_TAC THEN REWRITE_TAC[integrable, Dint] THEN 1965 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN 1966 HO_MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC ``i:real`` THEN 1967 HO_MATCH_MP_TAC MONO_ALL THEN X_GEN_TAC ``e:real`` THEN 1968 ASM_CASES_TAC ``&0 < e`` THEN ASM_REWRITE_TAC[] THEN 1969 HO_MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC ``g:real->real`` THEN 1970 ASM_MESON_TAC[DIVISION_APPEND_STRONG] THEN ASM_REWRITE_TAC[]); 1971 1972val INTEGRABLE_SUBINTERVAL_LEFT = store_thm("INTEGRABLE_SUBINTERVAL_LEFT", 1973 ``!f a b c. a <= c /\ c <= b /\ integrable(a,b) f ==> integrable(a,c) f``, 1974 REPEAT GEN_TAC THEN DISCH_TAC THEN 1975 FIRST_ASSUM(X_CHOOSE_TAC ``i:real`` o MATCH_MP INTEGRABLE_SPLIT_SIDES) THEN 1976 REWRITE_TAC[INTEGRABLE_CAUCHY] THEN X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1977 FIRST_X_ASSUM(MP_TAC o SPEC ``e / &2``) THEN 1978 SIMP_TAC arith_ss[ASSUME ``&0 < e``, REAL_LT_DIV, REAL_LT] THEN 1979 HO_MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC ``g:real->real`` THEN STRIP_TAC THEN 1980 CONJ_TAC THENL 1981 [UNDISCH_TAC ``gauge (\x. a <= x /\ x <= b) g`` THEN 1982 REWRITE_TAC[gauge] THEN ASM_MESON_TAC[REAL_LE_TRANS],ALL_TAC] THEN 1983 REPEAT STRIP_TAC THEN 1984 MP_TAC(SPECL [``c:real``, ``b:real``, ``g:real->real``] 1985 DIVISION_EXISTS) THEN 1986 SUBGOAL_THEN``c <= b /\ gauge (\x. c <= x /\ x <= b) g``ASSUME_TAC THENL 1987 [ASM_REWRITE_TAC[] THEN 1988 UNDISCH_TAC ``gauge (\x. a <= x /\ x <= b) g`` THEN 1989 REWRITE_TAC[gauge] THEN ASM_MESON_TAC[REAL_LE_TRANS],ALL_TAC] THEN 1990 ASM_REWRITE_TAC[] THEN SIMP_TAC arith_ss[GSYM LEFT_FORALL_IMP_THM] THEN 1991 MAP_EVERY X_GEN_TAC [``d:num->real``, ``p:num->real``] THEN STRIP_TAC THEN 1992 FIRST_X_ASSUM(fn th => 1993 MP_TAC(SPECL [``d1:num->real``, ``p1:num->real``] th) THEN 1994 MP_TAC(SPECL [``d2:num->real``, ``p2:num->real``] th)) THEN 1995 SIMP_TAC arith_ss[AND_IMP_INTRO, GSYM FORALL_AND_THM] THEN 1996 DISCH_THEN(MP_TAC o SPECL [``d:num->real``, ``p:num->real``]) THEN 1997 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN 1998 MATCH_MP_TAC REAL_LET_TRANS THEN 1999 EXISTS_TAC``abs ((rsum (d1,p1) f + rsum (d,p) f - i) - 2000 (rsum (d2,p2) f + rsum (d,p) f - i))`` THEN 2001 CONJ_TAC THENL 2002 [MATCH_MP_TAC REAL_EQ_IMP_LE THEN 2003 REWRITE_TAC[REAL_ARITH``a + b - i -(c + b - i) = a - c``], 2004 MATCH_MP_TAC REAL_LET_TRANS THEN 2005 EXISTS_TAC``abs (rsum (d1,p1) f + rsum (d,p) f - i) + 2006 abs(rsum (d2,p2) f + rsum (d,p) f - i)`` THEN 2007 CONJ_TAC THENL 2008 [REWRITE_TAC[REAL_ARITH``abs(a - b) <= abs a + abs b``], 2009 GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_HALF_DOUBLE] THEN 2010 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[]]]); 2011 2012val INTEGRABLE_SUBINTERVAL_RIGHT = store_thm("INTEGRABLE_SUBINTERVAL_RIGHT", 2013 ``!f a b c. a <= c /\ c <= b /\ integrable(a,b) f ==> integrable(c,b) f``, 2014 REPEAT GEN_TAC THEN DISCH_TAC THEN 2015 FIRST_ASSUM(X_CHOOSE_TAC ``i:real`` o MATCH_MP INTEGRABLE_SPLIT_SIDES) THEN 2016 REWRITE_TAC[INTEGRABLE_CAUCHY] THEN X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 2017 FIRST_X_ASSUM(MP_TAC o SPEC ``e / &2``) THEN 2018 SIMP_TAC arith_ss[ASSUME ``&0 < e``, REAL_LT_DIV, REAL_LT] THEN 2019 HO_MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC ``g:real->real`` THEN 2020 STRIP_TAC THEN CONJ_TAC THENL 2021 [UNDISCH_TAC ``gauge (\x. a <= x /\ x <= b) g`` THEN 2022 REWRITE_TAC[gauge] THEN ASM_MESON_TAC[REAL_LE_TRANS], ALL_TAC] THEN 2023 REPEAT STRIP_TAC THEN 2024 MP_TAC(SPECL [``a:real``, ``c:real``, ``g:real->real``] 2025 DIVISION_EXISTS) THEN 2026 SUBGOAL_THEN``a <= c /\ gauge (\x. a <= x /\ x <= c) g``ASSUME_TAC THENL 2027 [ASM_REWRITE_TAC[] THEN 2028 UNDISCH_TAC ``gauge (\x. a <= x /\ x <= b) g`` THEN 2029 REWRITE_TAC[gauge] THEN ASM_MESON_TAC[REAL_LE_TRANS], ALL_TAC] THEN 2030 ASM_REWRITE_TAC[] THEN SIMP_TAC arith_ss[GSYM LEFT_FORALL_IMP_THM] THEN 2031 MAP_EVERY X_GEN_TAC [``d:num->real``, ``p:num->real``] THEN STRIP_TAC THEN 2032 FIRST_X_ASSUM(MP_TAC o SPECL [``d:num->real``, ``p:num->real``]) THEN 2033 DISCH_THEN(fn th => 2034 MP_TAC(SPECL [``d1:num->real``, ``p1:num->real``] th) THEN 2035 MP_TAC(SPECL [``d2:num->real``, ``p2:num->real``] th)) THEN 2036 ASM_REWRITE_TAC[] THEN 2037 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN 2038 EXISTS_TAC``abs ((rsum (d,p) f + rsum (d1,p1) f - i) - 2039 (rsum (d,p) f + rsum (d2,p2) f - i))`` THEN 2040 CONJ_TAC THENL 2041 [MATCH_MP_TAC REAL_EQ_IMP_LE THEN 2042 REWRITE_TAC[REAL_ARITH``a + b - i -(a + c - i) = b - c``], ALL_TAC] THEN 2043 MATCH_MP_TAC REAL_LET_TRANS THEN 2044 EXISTS_TAC``abs (rsum (d,p) f + rsum (d1,p1) f - i) + 2045 abs(rsum (d,p) f + rsum (d2,p2) f - i)`` THEN 2046 CONJ_TAC THENL 2047 [REWRITE_TAC[REAL_ARITH``abs(a - b) <= abs a + abs b``], 2048 GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_HALF_DOUBLE] THEN 2049 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[]]); 2050 2051val INTEGRABLE_SUBINTERVAL = store_thm("INTEGRABLE_SUBINTERVAL", 2052 ``!f a b c d. a <= c /\ c <= d /\ d <= b /\ integrable(a,b) f 2053 ==> integrable(c,d) f``, 2054 MESON_TAC[INTEGRABLE_SUBINTERVAL_LEFT, INTEGRABLE_SUBINTERVAL_RIGHT, 2055 REAL_LE_TRANS]); 2056 2057(* ------------------------------------------------------------------------- *) 2058(* More basic lemmas about integration. *) 2059(* ------------------------------------------------------------------------- *) 2060 2061val INTEGRAL_0 = store_thm("INTEGRAL_0", 2062 ``!a b. a <= b ==> (integral(a,b) (\x. 0) = 0)``, 2063 RW_TAC std_ss[] THEN MATCH_MP_TAC DINT_INTEGRAL THEN 2064 ASM_REWRITE_TAC[DINT_0]); 2065 2066val INTEGRAL_CONST = store_thm("INTEGRAL_CONST", 2067 ���!a b c. a <= b ==> (integral(a,b) (\x. c) = c * (b - a))���, 2068 REPEAT STRIP_TAC THEN MATCH_MP_TAC DINT_INTEGRAL THEN 2069 ASM_SIMP_TAC arith_ss[DINT_CONST]); 2070 2071val INTEGRAL_CMUL = store_thm("INTEGRAL_CMUL", 2072���!f c a b. a <= b /\ integrable(a,b) f 2073 ==> (integral(a,b) (\x. c * f(x)) = c * integral(a,b) f)���, 2074 REPEAT STRIP_TAC THEN MATCH_MP_TAC DINT_INTEGRAL THEN 2075 ASM_SIMP_TAC arith_ss[DINT_CMUL, INTEGRABLE_DINT]); 2076 2077val INTEGRAL_ADD = store_thm("INTEGRAL_ADD", 2078���!f g a b. a <= b /\ integrable(a,b) f /\ integrable(a,b) g 2079 ==> (integral(a,b) (\x. f(x) + g(x)) = 2080 integral(a,b) f + integral(a,b) g)���, 2081 REPEAT STRIP_TAC THEN MATCH_MP_TAC DINT_INTEGRAL THEN 2082 ASM_SIMP_TAC arith_ss[DINT_ADD, INTEGRABLE_DINT]); 2083 2084val INTEGRAL_SUB = store_thm("INTEGRAL_SUB", 2085 ���!f g a b. a <= b /\ integrable(a,b) f /\ integrable(a,b) g 2086 ==> (integral(a,b) (\x. f(x) - g(x)) = 2087 integral(a,b) f - integral(a,b) g)���, 2088 REPEAT STRIP_TAC THEN MATCH_MP_TAC DINT_INTEGRAL THEN 2089 ASM_SIMP_TAC arith_ss[DINT_SUB, INTEGRABLE_DINT]); 2090 2091val INTEGRAL_BY_PARTS = store_thm("INTEGRAL_BY_PARTS", 2092 ``!f g f' g' a b. 2093 a <= b /\ 2094 (!x. a <= x /\ x <= b ==> (f diffl f' x) x) /\ 2095 (!x. a <= x /\ x <= b ==> (g diffl g' x) x) /\ 2096 integrable(a,b) (\x. f' x * g x) /\ 2097 integrable(a,b) (\x. f x * g' x) 2098 ==> (integral(a,b) (\x. f x * g' x) = 2099 (f b * g b - f a * g a) - integral(a,b) (\x. f' x * g x))``, 2100 MP_TAC INTEGRATION_BY_PARTS THEN REPEAT(HO_MATCH_MP_TAC MONO_ALL THEN GEN_TAC) THEN 2101 DISCH_THEN(fn th => STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN 2102 DISCH_THEN(MP_TAC o CONJ (ASSUME ``a <= b``)) THEN 2103 DISCH_THEN(SUBST1_TAC o SYM o MATCH_MP DINT_INTEGRAL) THEN 2104 ASM_SIMP_TAC arith_ss[INTEGRAL_ADD] THEN REAL_ARITH_TAC); 2105 2106val INTEGRAL_COMBINE = store_thm("INTEGRAL_COMBINE", 2107 ``!f a b c. a <= b /\ b <= c /\ (integrable (a,c) f) ==> 2108 (integral (a,c) f = (integral (a,b) f) + (integral (b,c) f))``, 2109 RW_TAC std_ss[integral] THEN SELECT_ELIM_TAC THEN RW_TAC std_ss[] THENL 2110 [FULL_SIMP_TAC std_ss[integrable] THEN EXISTS_TAC ``i:real`` THEN 2111 ASM_REWRITE_TAC[], 2112 SELECT_ELIM_TAC THEN CONJ_TAC THENL 2113 [REWRITE_TAC[GSYM integrable] THEN MATCH_MP_TAC INTEGRABLE_SUBINTERVAL THEN 2114 MAP_EVERY EXISTS_TAC[``a:real``,``c:real``] THEN 2115 RW_TAC std_ss[REAL_LE_REFL, integrable], 2116 SELECT_ELIM_TAC THEN CONJ_TAC THENL 2117 [REWRITE_TAC[GSYM integrable] THEN MATCH_MP_TAC INTEGRABLE_SUBINTERVAL THEN 2118 MAP_EVERY EXISTS_TAC[``a:real``,``c:real``] THEN 2119 RW_TAC std_ss[REAL_LE_REFL, integrable], 2120 RW_TAC std_ss[] THEN MATCH_MP_TAC DINT_UNIQ THEN 2121 MAP_EVERY EXISTS_TAC[``a:real``,``c:real``,``f:real->real``] THEN 2122 RW_TAC std_ss[] THENL 2123 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ``b:real`` THEN 2124 RW_TAC std_ss[], 2125 MATCH_MP_TAC DINT_COMBINE THEN EXISTS_TAC ``b:real`` THEN 2126 RW_TAC std_ss[]]]]]); 2127 2128(* ------------------------------------------------------------------------- *) 2129(* Mean value theorem of integral. *) 2130(* ------------------------------------------------------------------------- *) 2131 2132val INTEGRAL_MVT1 = store_thm("INTEGRAL_MVT1", 2133 ``!f a b. (a <= b /\(!x. a<=x /\ x<=b ==> f contl x)) ==> 2134 (?x. a<=x /\ x<=b /\ (integral(a,b) f = f(x)*(b-a)))``, 2135 REPEAT GEN_TAC THEN 2136 MP_TAC(SPECL[``f:real->real``,``a:real``,``b:real``]CONT_ATTAINS_ALL) THEN 2137 REWRITE_TAC[TAUT_CONV``((a ==> b) ==> (a ==> c)) = (a ==> b ==> c)``] THEN 2138 REPEAT STRIP_TAC THEN ASM_CASES_TAC``a:real=b`` THENL 2139 [EXISTS_TAC``b:real`` THEN ASM_SIMP_TAC std_ss[REAL_LE_REFL] THEN 2140 ASM_SIMP_TAC std_ss[REAL_SUB_REFL,REAL_MUL_RZERO] THEN 2141 MATCH_MP_TAC DINT_INTEGRAL THEN 2142 ASM_SIMP_TAC std_ss[REAL_LE_REFL,INTEGRAL_NULL], ALL_TAC] THEN 2143 SUBGOAL_THEN``?x:real. a<=x /\ x<=b /\ 2144 (f x = inv(b-a)* integral(a,b) f)``ASSUME_TAC THENL 2145 [UNDISCH_TAC``!y. L <= y /\ y <= M ==> ?x. a <= x /\ x<=b /\ (f x = y)`` THEN 2146 DISCH_THEN(MP_TAC o SPEC``inv(b-a)* integral(a,b)f``) THEN 2147 REPEAT STRIP_TAC THEN 2148 SUBGOAL_THEN``(L*(b-a) <= integral(a,b) f) /\ 2149 (integral(a,b) f <= M*(b-a))``ASSUME_TAC THENL 2150 [CONJ_TAC THENL 2151 [SUBGOAL_THEN``L*(b-a)=integral(a,b)(\x. L)``ASSUME_TAC THENL 2152 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC INTEGRAL_CONST THEN 2153 ASM_REWRITE_TAC[],ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INTEGRAL_LE THEN 2154 ASM_SIMP_TAC std_ss[INTEGRABLE_CONTINUOUS, 2155 INTEGRABLE_CONST,REAL_LT_IMP_LE]], 2156 SUBGOAL_THEN``M*(b-a) = integral(a,b)(\x. M)``ASSUME_TAC THENL 2157 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC INTEGRAL_CONST THEN 2158 ASM_REWRITE_TAC[], ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INTEGRAL_LE THEN 2159 ASM_SIMP_TAC std_ss[INTEGRABLE_CONTINUOUS, 2160 INTEGRABLE_CONST,REAL_LT_IMP_LE]]],ALL_TAC] THEN 2161 SUBGOAL_THEN``L <= inv(b-a) * integral(a,b) f /\ 2162 inv(b-a) * integral(a,b) f <= M``MP_TAC THENL 2163 [ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN 2164 CONJ_TAC THENL 2165 [MATCH_MP_TAC REAL_LE_RDIV THEN 2166 ASM_SIMP_TAC std_ss[REAL_SUB_LT,REAL_LT_LE], 2167 MATCH_MP_TAC REAL_LE_LDIV THEN 2168 ASM_SIMP_TAC std_ss[REAL_SUB_LT,REAL_LT_LE]],ALL_TAC] THEN 2169 ASM_SIMP_TAC std_ss[],ALL_TAC] THEN 2170 FIRST_ASSUM(X_CHOOSE_THEN``x:real``STRIP_ASSUME_TAC) THEN 2171 EXISTS_TAC``x:real``THEN ASM_SIMP_TAC std_ss[REAL_ARITH``a*b*c=c*a*b``] THEN 2172 SUBGOAL_THEN``(b:real -a)*inv(b-a)=1``ASSUME_TAC THENL 2173 [MATCH_MP_TAC REAL_MUL_RINV THEN MATCH_MP_TAC REAL_POS_NZ THEN 2174 ASM_SIMP_TAC std_ss[REAL_SUB_LT,REAL_LT_LE],ALL_TAC] THEN 2175 ASM_SIMP_TAC std_ss[REAL_MUL_LID]); 2176 2177val _ = export_theory(); 2178