1(* ************************************************************************* *) 2(* Sum of a real-valued function on a set: SIGMA f s *) 3(* ************************************************************************* *) 4 5(* interactive mode 6app load ["bossLib", "arithmeticTheory", "combinTheory", 7 "pred_setTheory", "realTheory", "realLib", 8 "res_quanTools", "pairTheory", "seqTheory"]; 9quietdec := true; 10*) 11 12open HolKernel Parse boolLib bossLib arithmeticTheory combinTheory 13 pred_setTheory realTheory realLib res_quanTools pairTheory seqTheory; 14 15(* interactive mode 16quietdec := false; 17*) 18 19val _ = new_theory "real_sigma"; 20 21val S_TAC = rpt (POP_ASSUM MP_TAC) >> rpt RESQ_STRIP_TAC; 22val Strip = S_TAC; 23 24fun K_TAC _ = ALL_TAC; 25val KILL_TAC = POP_ASSUM_LIST K_TAC; 26val Know = Q_TAC KNOW_TAC; 27val Suff = Q_TAC SUFF_TAC; 28val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 29 30 31(* ---------------------------------------------------------------------- 32 REAL_SUM_IMAGE 33 34 This constant is the same as standard mathematics \Sigma operator: 35 36 \Sigma_{x\in P}{f(x)} = SUM_IMAGE f P 37 38 Where f's range is the real numbers and P is finite. 39 ---------------------------------------------------------------------- *) 40 41val REAL_SUM_IMAGE_DEF = new_definition( 42 "REAL_SUM_IMAGE_DEF", 43 ``REAL_SUM_IMAGE f s = ITSET (\e acc. f e + acc) s (0:real)``); 44 45val REAL_SUM_IMAGE_THM = store_thm( 46 "REAL_SUM_IMAGE_THM", 47 ``!f. (REAL_SUM_IMAGE f {} = 0) /\ 48 (!e s. FINITE s ==> 49 (REAL_SUM_IMAGE f (e INSERT s) = 50 f e + REAL_SUM_IMAGE f (s DELETE e)))``, 51 REPEAT STRIP_TAC 52 >- SIMP_TAC (srw_ss()) [ITSET_THM, REAL_SUM_IMAGE_DEF] 53 >> SIMP_TAC (srw_ss()) [REAL_SUM_IMAGE_DEF] 54 >> Q.ABBREV_TAC `g = \e acc. f e + acc` 55 >> Suff `ITSET g (e INSERT s) 0 = 56 g e (ITSET g (s DELETE e) 0)` 57 >- (Q.UNABBREV_TAC `g` >> SRW_TAC [] []) 58 >> MATCH_MP_TAC COMMUTING_ITSET_RECURSES 59 >> Q.UNABBREV_TAC `g` 60 >> RW_TAC real_ss [] 61 >> REAL_ARITH_TAC); 62 63val REAL_SUM_IMAGE_SING = store_thm( 64 "REAL_SUM_IMAGE_SING", 65 ``!f e. REAL_SUM_IMAGE f {e} = f e``, 66 SRW_TAC [][REAL_SUM_IMAGE_THM]); 67 68val REAL_SUM_IMAGE_POS = store_thm 69 ("REAL_SUM_IMAGE_POS", 70 ``!f s. FINITE s /\ 71 (!x. x IN s ==> 0 <= f x) ==> 72 0 <= REAL_SUM_IMAGE f s``, 73 REPEAT STRIP_TAC 74 >> POP_ASSUM MP_TAC >> Q.SPEC_TAC (`f`, `f`) 75 >> POP_ASSUM MP_TAC >> Q.SPEC_TAC (`s`, `s`) 76 >> Q.ABBREV_TAC `Q = (\s. !f. (!x. x IN s ==> 0 <= f x) ==> 0 <= REAL_SUM_IMAGE f s)` 77 >> Suff `!s. FINITE s ==> Q s` >- (Q.UNABBREV_TAC `Q` >> RW_TAC std_ss []) 78 >> MATCH_MP_TAC FINITE_INDUCT 79 >> Q.UNABBREV_TAC `Q` 80 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM] 81 >> MATCH_MP_TAC REAL_LE_ADD 82 >> CONJ_TAC >- FULL_SIMP_TAC real_ss [IN_INSERT] 83 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT] 84 >> Q.PAT_ASSUM `!f. (!x. x IN s ==> 0 <= f x) ==> 0 <= REAL_SUM_IMAGE f s` MATCH_MP_TAC 85 >> REPEAT STRIP_TAC >> Q.PAT_ASSUM `!x. b` MATCH_MP_TAC 86 >> RW_TAC std_ss [IN_INSERT]); 87 88val REAL_SUM_IMAGE_SPOS = store_thm 89 ("REAL_SUM_IMAGE_SPOS", 90 ``!s. FINITE s /\ (~(s = {})) ==> 91 !f. (!x. x IN s ==> 0 < f x) ==> 92 0 < REAL_SUM_IMAGE f s``, 93 Suff `!s. FINITE s ==> 94 (\s. (~(s = {})) ==> 95 !f. (!x. x IN s ==> 0 < f x) ==> 96 0 < REAL_SUM_IMAGE f s) s` 97 >- RW_TAC std_ss [] 98 >> MATCH_MP_TAC FINITE_INDUCT 99 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT, DISJ_IMP_THM, 100 FORALL_AND_THM] 101 >> Cases_on `s = {}` 102 >- RW_TAC real_ss [REAL_SUM_IMAGE_THM] 103 >> MATCH_MP_TAC REAL_LT_ADD 104 >> ASM_SIMP_TAC real_ss []); 105 106val REAL_SUM_IMAGE_NONZERO_lem = prove 107 (``!P. FINITE P ==> 108 (\P. !f. (!x.x IN P ==> 0 <= f x) /\ (?x. x IN P /\ ~(f x = 0)) ==> 109 ((~(REAL_SUM_IMAGE f P = 0)) = (~(P = {})))) P``, 110 (MATCH_MP_TAC FINITE_INDUCT 111 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, NOT_INSERT_EMPTY, IN_INSERT] 112 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT]) 113 >- (ONCE_REWRITE_TAC [GSYM REAL_LE_ANTISYM] 114 >> `0 <= f e + REAL_SUM_IMAGE f s` 115 by (MATCH_MP_TAC REAL_LE_ADD 116 >> RW_TAC std_ss [] 117 >> MATCH_MP_TAC REAL_SUM_IMAGE_POS 118 >> METIS_TAC []) 119 >> ASM_REWRITE_TAC [] 120 >> RW_TAC std_ss [GSYM real_lt] 121 >> MATCH_MP_TAC REAL_LTE_TRANS 122 >> Q.EXISTS_TAC `f e + 0` 123 >> CONJ_TAC 124 >- (RW_TAC real_ss [] >> POP_ASSUM (K ALL_TAC) 125 >> POP_ASSUM MP_TAC >> POP_ASSUM (MP_TAC o Q.SPECL [`e`]) 126 >> SIMP_TAC std_ss [] 127 >> REAL_ARITH_TAC) 128 >> MATCH_MP_TAC REAL_LE_ADD2 129 >> RW_TAC real_ss [] 130 >> MATCH_MP_TAC REAL_SUM_IMAGE_POS 131 >> METIS_TAC []) 132 >> Cases_on `f e = 0` 133 >- (RW_TAC real_ss [] >> METIS_TAC [NOT_IN_EMPTY]) 134 >> ONCE_REWRITE_TAC [GSYM REAL_LE_ANTISYM] 135 >> `0 <= f e + REAL_SUM_IMAGE f s` 136 by (MATCH_MP_TAC REAL_LE_ADD 137 >> RW_TAC std_ss [] 138 >> MATCH_MP_TAC REAL_SUM_IMAGE_POS 139 >> METIS_TAC []) 140 >> ASM_REWRITE_TAC [] 141 >> RW_TAC std_ss [GSYM real_lt] 142 >> MATCH_MP_TAC REAL_LTE_TRANS 143 >> Q.EXISTS_TAC `f e + 0` 144 >> CONJ_TAC 145 >- (RW_TAC real_ss [] >> POP_ASSUM (K ALL_TAC) 146 >> POP_ASSUM MP_TAC >> POP_ASSUM (K ALL_TAC) 147 >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM (MP_TAC o Q.SPECL [`e`]) 148 >> SIMP_TAC std_ss [] 149 >> REAL_ARITH_TAC) 150 >> MATCH_MP_TAC REAL_LE_ADD2 151 >> RW_TAC real_ss [] 152 >> MATCH_MP_TAC REAL_SUM_IMAGE_POS 153 >> METIS_TAC []); 154 155val REAL_SUM_IMAGE_NONZERO = store_thm 156 ("REAL_SUM_IMAGE_NONZERO", 157 ``!P. FINITE P ==> 158 !f. (!x.x IN P ==> 0 <= f x) /\ (?x. x IN P /\ ~(f x = 0)) ==> 159 ((~(REAL_SUM_IMAGE f P = 0)) = (~(P = {})))``, 160 METIS_TAC [REAL_SUM_IMAGE_NONZERO_lem]); 161 162val REAL_SUM_IMAGE_IF_ELIM_lem = prove 163 (``!s. FINITE s ==> 164 (\s. !P f. (!x. x IN s ==> P x) ==> 165 (REAL_SUM_IMAGE (\x. if P x then f x else 0) s = 166 REAL_SUM_IMAGE f s)) s``, 167 MATCH_MP_TAC FINITE_INDUCT 168 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, IN_INSERT, DELETE_NON_ELEMENT]); 169 170val REAL_SUM_IMAGE_IF_ELIM = store_thm 171 ("REAL_SUM_IMAGE_IF_ELIM", 172 ``!s P f. FINITE s /\ (!x. x IN s ==> P x) ==> 173 (REAL_SUM_IMAGE (\x. if P x then f x else 0) s = 174 REAL_SUM_IMAGE f s)``, 175 METIS_TAC [REAL_SUM_IMAGE_IF_ELIM_lem]); 176 177val REAL_SUM_IMAGE_FINITE_SAME_lem = prove 178 (``!P. FINITE P ==> 179 (\P. !f p. 180 p IN P /\ (!q. q IN P ==> (f p = f q)) ==> (REAL_SUM_IMAGE f P = (&(CARD P)) * f p)) P``, 181 MATCH_MP_TAC FINITE_INDUCT 182 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, CARD_EMPTY, DELETE_NON_ELEMENT] 183 >> `f p = f e` by FULL_SIMP_TAC std_ss [IN_INSERT] 184 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT] >> POP_ASSUM (K ALL_TAC) 185 >> RW_TAC real_ss [CARD_INSERT, ADD1] 186 >> ONCE_REWRITE_TAC [GSYM REAL_ADD] 187 >> RW_TAC real_ss [REAL_ADD_RDISTRIB] 188 >> Suff `REAL_SUM_IMAGE f s = & (CARD s) * f e` 189 >- RW_TAC real_ss [REAL_ADD_COMM] 190 >> (MP_TAC o Q.SPECL [`s`]) SET_CASES >> RW_TAC std_ss [] 191 >- RW_TAC real_ss [REAL_SUM_IMAGE_THM, CARD_EMPTY] 192 >> `f e = f x` by FULL_SIMP_TAC std_ss [IN_INSERT] 193 >> FULL_SIMP_TAC std_ss [] >> POP_ASSUM (K ALL_TAC) 194 >> Q.PAT_ASSUM `!f p. b` MATCH_MP_TAC >> METIS_TAC [IN_INSERT]); 195 196val REAL_SUM_IMAGE_FINITE_SAME = store_thm 197 ("REAL_SUM_IMAGE_FINITE_SAME", 198 ``!P. FINITE P ==> 199 !f p. 200 p IN P /\ (!q. q IN P ==> (f p = f q)) ==> (REAL_SUM_IMAGE f P = (&(CARD P)) * f p)``, 201 MP_TAC REAL_SUM_IMAGE_FINITE_SAME_lem >> RW_TAC std_ss []); 202 203val REAL_SUM_IMAGE_FINITE_CONST = store_thm 204 ("REAL_SUM_IMAGE_FINITE_CONST", 205 ``!P. FINITE P ==> 206 !f x. (!y. f y = x) ==> (REAL_SUM_IMAGE f P = (&(CARD P)) * x)``, 207 REPEAT STRIP_TAC 208 >> (MP_TAC o Q.SPECL [`P`]) REAL_SUM_IMAGE_FINITE_SAME 209 >> RW_TAC std_ss [] 210 >> POP_ASSUM (MP_TAC o (Q.SPECL [`f`])) 211 >> RW_TAC std_ss [] 212 >> (MP_TAC o Q.SPECL [`P`]) SET_CASES 213 >> RW_TAC std_ss [] >- RW_TAC real_ss [REAL_SUM_IMAGE_THM, CARD_EMPTY] 214 >> POP_ASSUM (K ALL_TAC) 215 >> POP_ASSUM MATCH_MP_TAC 216 >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss [IN_INSERT]); 217 218val REAL_SUM_IMAGE_IN_IF_lem = prove 219 (``!P. FINITE P ==> 220 (\P.!f. REAL_SUM_IMAGE f P = REAL_SUM_IMAGE (\x. if x IN P then f x else 0) P) P``, 221 MATCH_MP_TAC FINITE_INDUCT 222 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM] 223 >> POP_ASSUM MP_TAC 224 >> ONCE_REWRITE_TAC [DELETE_NON_ELEMENT] 225 >> SIMP_TAC real_ss [IN_INSERT] 226 >> `REAL_SUM_IMAGE (\x. (if (x = e) \/ x IN s then f x else 0)) s = 227 REAL_SUM_IMAGE (\x. (if x IN s then f x else 0)) s` 228 by (POP_ASSUM (MP_TAC o Q.SPECL [`(\x. (if (x = e) \/ x IN s then f x else 0))`]) 229 >> RW_TAC std_ss []) 230 >> POP_ORW 231 >> POP_ASSUM (MP_TAC o Q.SPECL [`f`]) 232 >> RW_TAC real_ss []); 233 234val REAL_SUM_IMAGE_IN_IF = store_thm 235 ("REAL_SUM_IMAGE_IN_IF", 236 ``!P. FINITE P ==> 237 !f. REAL_SUM_IMAGE f P = REAL_SUM_IMAGE (\x. if x IN P then f x else 0) P``, 238 METIS_TAC [REAL_SUM_IMAGE_IN_IF_lem]); 239 240val REAL_SUM_IMAGE_CMUL_lem = prove 241 (``!f c P. FINITE P ==> 242 (\P. REAL_SUM_IMAGE (\x. c * f x) P = c * (REAL_SUM_IMAGE f P)) P``, 243 STRIP_TAC >> STRIP_TAC >> MATCH_MP_TAC FINITE_INDUCT 244 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, REAL_ADD_LDISTRIB, DELETE_NON_ELEMENT]); 245 246val REAL_SUM_IMAGE_CMUL = store_thm 247 ("REAL_SUM_IMAGE_CMUL", 248 ``!P. FINITE P ==> 249 !f c. (REAL_SUM_IMAGE (\x. c * f x) P = c * (REAL_SUM_IMAGE f P))``, 250 METIS_TAC [REAL_SUM_IMAGE_CMUL_lem]); 251 252val REAL_SUM_IMAGE_NEG = store_thm 253 ("REAL_SUM_IMAGE_NEG", 254 ``!P. FINITE P ==> 255 !f. (REAL_SUM_IMAGE (\x. ~ f x) P = ~ (REAL_SUM_IMAGE f P))``, 256 REPEAT STRIP_TAC 257 >> (ASSUME_TAC o Q.SPECL [`f`, `~1`] o UNDISCH o Q.SPEC `P`) REAL_SUM_IMAGE_CMUL 258 >> FULL_SIMP_TAC real_ss []); 259 260val REAL_SUM_IMAGE_IMAGE = store_thm 261 ("REAL_SUM_IMAGE_IMAGE", 262 ``!P. FINITE P ==> 263 !f'. INJ f' P (IMAGE f' P) ==> 264 !f. REAL_SUM_IMAGE f (IMAGE f' P) = REAL_SUM_IMAGE (f o f') P``, 265 Induct_on `FINITE` 266 >> SRW_TAC [][REAL_SUM_IMAGE_THM] 267 >> `IMAGE f' P DELETE f' e = IMAGE f' P` 268 by (SRW_TAC [][EXTENSION] 269 >> EQ_TAC >- (METIS_TAC[]) 270 >> POP_ASSUM MP_TAC 271 >> ASM_SIMP_TAC (srw_ss()) [INJ_DEF] 272 >> METIS_TAC[]) 273 >> `P DELETE e = P` by METIS_TAC [DELETE_NON_ELEMENT] 274 >> SRW_TAC [][] 275 >> FIRST_X_ASSUM MATCH_MP_TAC 276 >> Q.PAT_ASSUM `INJ f' SS1 SS2` MP_TAC 277 >> CONV_TAC (BINOP_CONV (SIMP_CONV (srw_ss()) [INJ_DEF])) 278 >> METIS_TAC[]); 279 280val REAL_SUM_IMAGE_DISJOINT_UNION_lem = prove 281 (``!P. 282 FINITE P ==> 283 (\P. !P'. FINITE P' ==> 284 (\P'. DISJOINT P P' ==> 285 (!f. REAL_SUM_IMAGE f (P UNION P') = 286 REAL_SUM_IMAGE f P + 287 REAL_SUM_IMAGE f P')) P') P``, 288 MATCH_MP_TAC FINITE_INDUCT 289 >> CONJ_TAC 290 >- (RW_TAC real_ss [DISJOINT_EMPTY, UNION_EMPTY, REAL_SUM_IMAGE_THM]) 291 >> REPEAT STRIP_TAC 292 >> CONV_TAC (BETA_CONV) >> MATCH_MP_TAC FINITE_INDUCT 293 >> CONJ_TAC 294 >- (RW_TAC real_ss [DISJOINT_EMPTY, UNION_EMPTY, REAL_SUM_IMAGE_THM]) 295 >> FULL_SIMP_TAC std_ss [DISJOINT_INSERT] 296 >> ONCE_REWRITE_TAC [DISJOINT_SYM] 297 >> RW_TAC std_ss [INSERT_UNION, DISJOINT_INSERT, IN_INSERT] 298 >> FULL_SIMP_TAC std_ss [DISJOINT_SYM] 299 >> ONCE_REWRITE_TAC [UNION_COMM] >> RW_TAC std_ss [INSERT_UNION] 300 >> ONCE_REWRITE_TAC [UNION_COMM] >> ONCE_REWRITE_TAC [INSERT_COMM] 301 >> `FINITE (e INSERT s UNION s')` by RW_TAC std_ss [FINITE_INSERT, FINITE_UNION] 302 >> Q.ABBREV_TAC `Q = e INSERT s UNION s'` 303 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM] 304 >> Q.UNABBREV_TAC `Q` 305 >> `~ (e' IN (e INSERT s UNION s'))` 306 by RW_TAC std_ss [IN_INSERT, IN_UNION] 307 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT] 308 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM] 309 >> REAL_ARITH_TAC); 310 311val REAL_SUM_IMAGE_DISJOINT_UNION = store_thm 312 ("REAL_SUM_IMAGE_DISJOINT_UNION", 313 ``!P P'. FINITE P /\ FINITE P' /\ DISJOINT P P' ==> 314 (!f. REAL_SUM_IMAGE f (P UNION P') = 315 REAL_SUM_IMAGE f P + 316 REAL_SUM_IMAGE f P')``, 317 METIS_TAC [REAL_SUM_IMAGE_DISJOINT_UNION_lem]); 318 319val REAL_SUM_IMAGE_EQ_CARD_lem = prove 320 (``!P. FINITE P ==> 321 (\P. REAL_SUM_IMAGE (\x. if x IN P then 1 else 0) P = (&(CARD P))) P``, 322 MATCH_MP_TAC FINITE_INDUCT 323 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, CARD_EMPTY, IN_INSERT] 324 >> (MP_TAC o Q.SPECL [`s`]) CARD_INSERT 325 >> RW_TAC real_ss [ADD1] >> ONCE_REWRITE_TAC [GSYM REAL_ADD] 326 >> Suff `REAL_SUM_IMAGE (\x. (if (x = e) \/ x IN s then 1 else 0)) (s DELETE e) = 327 REAL_SUM_IMAGE (\x. (if x IN s then 1 else 0)) s` 328 >- RW_TAC real_ss [] 329 >> Q.PAT_ASSUM `REAL_SUM_IMAGE (\x. (if x IN s then 1 else 0)) s = & (CARD s)` (K ALL_TAC) 330 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT] 331 >> `REAL_SUM_IMAGE (\x. (if (x = e) \/ x IN s then 1 else 0)) s = 332 REAL_SUM_IMAGE (\x. if x IN s then (\x. (if (x = e) \/ x IN s then 1 else 0)) x else 0) s` 333 by (METIS_TAC [REAL_SUM_IMAGE_IN_IF]) 334 >> RW_TAC std_ss []); 335 336val REAL_SUM_IMAGE_EQ_CARD = store_thm 337 ("REAL_SUM_IMAGE_EQ_CARD", 338 ``!P. FINITE P ==> 339 (REAL_SUM_IMAGE (\x. if x IN P then 1 else 0) P = (&(CARD P)))``, 340 METIS_TAC [REAL_SUM_IMAGE_EQ_CARD_lem]); 341 342val REAL_SUM_IMAGE_INV_CARD_EQ_1 = store_thm 343 ("REAL_SUM_IMAGE_INV_CARD_EQ_1", 344 ``!P. (~(P = {})) /\ FINITE P ==> 345 (REAL_SUM_IMAGE (\s. if s IN P then inv (& (CARD P)) else 0) P = 1)``, 346 REPEAT STRIP_TAC 347 >> `(\s. if s IN P then inv (& (CARD P)) else 0) = (\s. inv (& (CARD P)) * (\s. if s IN P then 1 else 0) s)` 348 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss []) 349 >> POP_ORW 350 >> `REAL_SUM_IMAGE (\s. inv (& (CARD P)) * (\s. (if s IN P then 1 else 0)) s) P = 351 (inv (& (CARD P))) * (REAL_SUM_IMAGE (\s. (if s IN P then 1 else 0)) P)` 352 by (MATCH_MP_TAC REAL_SUM_IMAGE_CMUL >> RW_TAC std_ss []) 353 >> POP_ORW 354 >> `REAL_SUM_IMAGE (\s. (if s IN P then 1 else 0)) P = (&(CARD P))` 355 by (MATCH_MP_TAC REAL_SUM_IMAGE_EQ_CARD >> RW_TAC std_ss []) 356 >> POP_ORW 357 >> MATCH_MP_TAC REAL_MUL_LINV 358 >> RW_TAC real_ss [] 359 >> METIS_TAC [CARD_EQ_0]); 360 361val REAL_SUM_IMAGE_INTER_NONZERO_lem = prove 362 (``!P. FINITE P ==> 363 (\P. !f. REAL_SUM_IMAGE f (P INTER (\p. ~(f p = 0))) = 364 REAL_SUM_IMAGE f P) P``, 365 MATCH_MP_TAC FINITE_INDUCT 366 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, INTER_EMPTY, INSERT_INTER] 367 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT] 368 >> (RW_TAC std_ss [IN_DEF] >> RW_TAC real_ss []) 369 >> `FINITE (s INTER (\p. ~(f p = 0)))` by (MATCH_MP_TAC INTER_FINITE >> RW_TAC std_ss []) 370 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM] 371 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT] 372 >> `~(e IN (s INTER (\p. ~(f p = 0))))` 373 by RW_TAC std_ss [IN_INTER] 374 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT]); 375 376val REAL_SUM_IMAGE_INTER_NONZERO = store_thm 377 ("REAL_SUM_IMAGE_INTER_NONZERO", 378 ``!P. FINITE P ==> 379 !f. REAL_SUM_IMAGE f (P INTER (\p. ~(f p = 0))) = 380 REAL_SUM_IMAGE f P``, 381 METIS_TAC [REAL_SUM_IMAGE_INTER_NONZERO_lem]); 382 383val REAL_SUM_IMAGE_INTER_ELIM_lem = prove 384 (``!P. FINITE P ==> 385 (\P. !f P'. (!x. (~(x IN P')) ==> (f x = 0)) ==> 386 (REAL_SUM_IMAGE f (P INTER P') = 387 REAL_SUM_IMAGE f P)) P``, 388 MATCH_MP_TAC FINITE_INDUCT 389 >> RW_TAC std_ss [INTER_EMPTY, REAL_SUM_IMAGE_THM, INSERT_INTER] 390 >> Cases_on `e IN P'` 391 >- (`~ (e IN (s INTER P'))` by RW_TAC std_ss [IN_INTER] 392 >> FULL_SIMP_TAC std_ss [INTER_FINITE, REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT]) 393 >> FULL_SIMP_TAC real_ss [] 394 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT]); 395 396val REAL_SUM_IMAGE_INTER_ELIM = store_thm 397 ("REAL_SUM_IMAGE_INTER_ELIM", 398 ``!P. FINITE P ==> 399 !f P'. (!x. (~(x IN P')) ==> (f x = 0)) ==> 400 (REAL_SUM_IMAGE f (P INTER P') = 401 REAL_SUM_IMAGE f P)``, 402 METIS_TAC [REAL_SUM_IMAGE_INTER_ELIM_lem]); 403 404val REAL_SUM_IMAGE_COUNT = store_thm 405 ("REAL_SUM_IMAGE_COUNT", 406 ``!f n. REAL_SUM_IMAGE f (pred_set$count n) = 407 sum (0,n) f``, 408 STRIP_TAC >> Induct 409 >- RW_TAC std_ss [pred_setTheory.count_def, REAL_SUM_IMAGE_THM, GSPEC_F, sum] 410 >> `pred_set$count (SUC n) = n INSERT pred_set$count n` 411 by (RW_TAC std_ss [EXTENSION, IN_INSERT, pred_setTheory.IN_COUNT] >> DECIDE_TAC) 412 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, sum, pred_setTheory.FINITE_COUNT] 413 >> `pred_set$count n DELETE n = pred_set$count n` 414 by RW_TAC arith_ss [DELETE_DEF, DIFF_DEF, IN_SING, pred_setTheory.IN_COUNT, 415 Once EXTENSION, pred_setTheory.IN_COUNT, GSPECIFICATION, 416 DECIDE ``!(x:num) (y:num). x < y ==> ~(x = y)``] 417 >> RW_TAC std_ss [REAL_ADD_SYM]); 418 419val REAL_SUM_IMAGE_MONO = store_thm 420 ("REAL_SUM_IMAGE_MONO", 421 ``!P. FINITE P ==> 422 !f f'. (!x. x IN P ==> f x <= f' x) ==> 423 REAL_SUM_IMAGE f P <= REAL_SUM_IMAGE f' P``, 424 Suff `!P. FINITE P ==> 425 (\P. !f f'. (!x. x IN P ==> f x <= f' x) ==> 426 REAL_SUM_IMAGE f P <= REAL_SUM_IMAGE f' P) P` 427 >- PROVE_TAC [] 428 >> MATCH_MP_TAC FINITE_INDUCT 429 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM,DELETE_NON_ELEMENT, IN_INSERT, 430 DISJ_IMP_THM, FORALL_AND_THM, REAL_LE_ADD2]); 431 432val REAL_SUM_IMAGE_POS_MEM_LE = store_thm 433 ("REAL_SUM_IMAGE_POS_MEM_LE", 434 ``!P. FINITE P ==> 435 !f. (!x. x IN P ==> 0 <= f x) ==> 436 (!x. x IN P ==> f x <= REAL_SUM_IMAGE f P)``, 437 Suff `!P. FINITE P ==> 438 (\P. !f. (!x. x IN P ==> 0 <= f x) ==> 439 (!x. x IN P ==> f x <= REAL_SUM_IMAGE f P)) P` 440 >- PROVE_TAC [] 441 >> MATCH_MP_TAC FINITE_INDUCT 442 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, NOT_IN_EMPTY, IN_INSERT, 443 DISJ_IMP_THM, FORALL_AND_THM, 444 DELETE_NON_ELEMENT] 445 >- (Suff `f e + 0 <= f e + REAL_SUM_IMAGE f s` >- RW_TAC real_ss [] 446 >> MATCH_MP_TAC REAL_LE_LADD_IMP 447 >> MATCH_MP_TAC REAL_SUM_IMAGE_POS >> ASM_REWRITE_TAC []) 448 >> Suff `0 + f x <= f e + REAL_SUM_IMAGE f s` >- RW_TAC real_ss [] 449 >> MATCH_MP_TAC REAL_LE_ADD2 >> PROVE_TAC []); 450 451val REAL_SUM_IMAGE_CONST_EQ_1_EQ_INV_CARD = store_thm 452 ("REAL_SUM_IMAGE_CONST_EQ_1_EQ_INV_CARD", 453 ``!P. FINITE P ==> 454 !f. (REAL_SUM_IMAGE f P = 1) /\ 455 (!x y. x IN P /\ y IN P ==> (f x = f y)) ==> 456 (!x. x IN P ==> (f x = inv (& (CARD P))))``, 457 Suff `!P. FINITE P ==> 458 (\P. !f. (REAL_SUM_IMAGE f P = 1) /\ 459 (!x y. x IN P /\ y IN P ==> (f x = f y)) ==> 460 (!x. x IN P ==> (f x = inv (& (CARD P))))) P` 461 >- RW_TAC std_ss [] 462 >> MATCH_MP_TAC FINITE_INDUCT 463 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, IN_INSERT, DELETE_NON_ELEMENT] 464 >- (RW_TAC std_ss [(UNDISCH o Q.SPEC `s`) CARD_INSERT] 465 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT] 466 >> Q.PAT_ASSUM `(f:'a->real) e + REAL_SUM_IMAGE f s = 1` 467 (MP_TAC o REWRITE_RULE [Once ((UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF)]) 468 >> `(\x:'a. (if (x IN s) then (f:'a -> real) x else (0:real))) = 469 (\x:'a. (if (x IN s) then (\x:'a. (f:'a -> real) e) x else (0:real)))` 470 by METIS_TAC [] 471 >> POP_ORW 472 >> ONCE_REWRITE_TAC [(GSYM o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF] 473 >> (MP_TAC o Q.SPECL [`(\x. (f:'a->real) e)`, `(f:'a->real) e`] o 474 UNDISCH o Q.ISPEC `s:'a -> bool`) REAL_SUM_IMAGE_FINITE_CONST 475 >> SIMP_TAC std_ss [] 476 >> STRIP_TAC >> POP_ASSUM (K ALL_TAC) 477 >> `f e + & (CARD s) * f e = f e *( & (CARD s) + 1)` by REAL_ARITH_TAC 478 >> POP_ORW 479 >> `1:real = &1` by RW_TAC real_ss [] 480 >> POP_ASSUM (fn thm => SIMP_TAC std_ss [thm, REAL_OF_NUM_ADD, GSYM ADD1]) 481 >> REPEAT (POP_ASSUM (K ALL_TAC)) 482 >> METIS_TAC [REAL_NZ_IMP_LT, GSYM REAL_EQ_RDIV_EQ, REAL_INV_1OVER, SUC_NOT]) 483 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT] 484 >> RW_TAC std_ss [(UNDISCH o Q.SPEC `s`) CARD_INSERT] 485 >> Q.PAT_ASSUM `f e + REAL_SUM_IMAGE f s = 1` 486 (MP_TAC o REWRITE_RULE [Once ((UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF)]) 487 >> `(\x:'a. (if (x IN s) then (f:'a -> real) x else (0:real))) = 488 (\x:'a. (if (x IN s) then (\x:'a. (f:'a -> real) e) x else (0:real)))` 489 by METIS_TAC [] 490 >> POP_ORW 491 >> ONCE_REWRITE_TAC [(GSYM o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF] 492 >> (MP_TAC o Q.SPECL [`(\x. (f:'a->real) e)`, `(f:'a->real) e`] o 493 UNDISCH o Q.ISPEC `s:'a -> bool`) REAL_SUM_IMAGE_FINITE_CONST 494 >> SIMP_TAC std_ss [] 495 >> STRIP_TAC >> POP_ASSUM (K ALL_TAC) 496 >> `f e + & (CARD s) * f e = f e *( & (CARD s) + 1)` by REAL_ARITH_TAC 497 >> POP_ORW 498 >> `1:real = &1` by RW_TAC real_ss [] 499 >> POP_ASSUM (fn thm => SIMP_TAC std_ss [thm, REAL_OF_NUM_ADD, GSYM ADD1]) 500 >> `f x = f e` by METIS_TAC [] >> POP_ORW 501 >> REPEAT (POP_ASSUM (K ALL_TAC)) 502 >> METIS_TAC [REAL_NZ_IMP_LT, GSYM REAL_EQ_RDIV_EQ, REAL_INV_1OVER, SUC_NOT]); 503 504val REAL_SUM_IMAGE_ADD = store_thm 505 ("REAL_SUM_IMAGE_ADD", 506 ``!s. FINITE s ==> !f f'. 507 (REAL_SUM_IMAGE (\x. f x + f' x) s = 508 REAL_SUM_IMAGE f s + REAL_SUM_IMAGE f' s)``, 509 Suff `!s. FINITE s ==> 510 (\s. !f f'. 511 (REAL_SUM_IMAGE (\x. f x + f' x) s = 512 REAL_SUM_IMAGE f s + REAL_SUM_IMAGE f' s)) s` 513 >- RW_TAC std_ss [] 514 >> MATCH_MP_TAC FINITE_INDUCT 515 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT] 516 >> REAL_ARITH_TAC); 517 518val REAL_SUM_IMAGE_REAL_SUM_IMAGE = store_thm 519 ("REAL_SUM_IMAGE_REAL_SUM_IMAGE", 520 ``!s s' f. FINITE s /\ FINITE s' ==> 521 (REAL_SUM_IMAGE (\x. REAL_SUM_IMAGE (f x) s') s = 522 REAL_SUM_IMAGE (\x. f (FST x) (SND x)) (s CROSS s'))``, 523 Suff `!s. FINITE s ==> 524 (\s. !s' f. FINITE s' ==> 525 (REAL_SUM_IMAGE (\x. REAL_SUM_IMAGE (f x) s') s = 526 REAL_SUM_IMAGE (\x. f (FST x) (SND x)) (s CROSS s'))) s` 527 >- RW_TAC std_ss [] 528 >> MATCH_MP_TAC FINITE_INDUCT 529 >> RW_TAC std_ss [CROSS_EMPTY, REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT] 530 >> `((e INSERT s) CROSS s') = (IMAGE (\x. (e,x)) s') UNION (s CROSS s')` 531 by (RW_TAC std_ss [Once EXTENSION, IN_INSERT, IN_SING, IN_CROSS, IN_UNION, IN_IMAGE] 532 >> (MP_TAC o Q.ISPEC `x:'a#'b`) pair_CASES 533 >> RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [FST,SND, GSYM DELETE_NON_ELEMENT] 534 >> METIS_TAC []) 535 >> POP_ORW 536 >> `DISJOINT (IMAGE (\x. (e,x)) s') (s CROSS s')` 537 by (FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT, DISJOINT_DEF, Once EXTENSION, 538 NOT_IN_EMPTY, IN_INTER, IN_CROSS, IN_SING, IN_IMAGE] 539 >> STRIP_TAC >> (MP_TAC o Q.ISPEC `x:'a#'b`) pair_CASES 540 >> RW_TAC std_ss [FST, SND] 541 >> METIS_TAC []) 542 >> (MP_TAC o REWRITE_RULE [GSYM AND_IMP_INTRO] o 543 Q.ISPECL [`IMAGE (\x. (e:'a,x)) (s':'b->bool)`, `(s:'a->bool) CROSS (s':'b->bool)`]) 544 REAL_SUM_IMAGE_DISJOINT_UNION 545 >> RW_TAC std_ss [FINITE_CROSS, IMAGE_FINITE] 546 >> POP_ASSUM (K ALL_TAC) 547 >> (MP_TAC o Q.SPEC `(\x. (e,x))` o UNDISCH o Q.SPEC `s'` o 548 INST_TYPE [``:'c``|->``:'a # 'b``] o INST_TYPE [``:'a``|->``:'b``] o 549 INST_TYPE [``:'b``|->``:'c``]) REAL_SUM_IMAGE_IMAGE 550 >> RW_TAC std_ss [INJ_DEF, IN_IMAGE, o_DEF] >> METIS_TAC []); 551 552val REAL_SUM_IMAGE_0 = store_thm 553 ("REAL_SUM_IMAGE_0", 554 ``!s. FINITE s ==> (REAL_SUM_IMAGE (\x. 0) s = 0)``, 555 REPEAT STRIP_TAC 556 >> (MP_TAC o Q.SPECL [`(\x. 0)`,`0`] o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_FINITE_CONST 557 >> RW_TAC real_ss []); 558 559val SEQ_REAL_SUM_IMAGE = store_thm 560 ("SEQ_REAL_SUM_IMAGE", 561 ``!s. FINITE s ==> 562 !f f'. (!x. x IN s ==> (\n. f n x) --> f' x) ==> 563 (\n. REAL_SUM_IMAGE (f n) s) --> 564 REAL_SUM_IMAGE f' s``, 565 Suff `!s. FINITE s ==> 566 (\s. !f f'. (!x. x IN s ==> (\n. f n x) --> f' x) ==> 567 (\n. REAL_SUM_IMAGE (f n) s) --> 568 REAL_SUM_IMAGE f' s) s` 569 >- RW_TAC std_ss [] 570 >> MATCH_MP_TAC FINITE_INDUCT 571 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, SEQ_CONST, IN_INSERT, DELETE_NON_ELEMENT] 572 >> `(\n. f n e + REAL_SUM_IMAGE (f n) s) = (\n. (\n. f n e) n + (\n. REAL_SUM_IMAGE (f n) s) n)` 573 by RW_TAC std_ss [] 574 >> POP_ORW 575 >> MATCH_MP_TAC SEQ_ADD 576 >> METIS_TAC []); 577 578val NESTED_REAL_SUM_IMAGE_REVERSE = store_thm 579 ("NESTED_REAL_SUM_IMAGE_REVERSE", 580 ``!f s s'. FINITE s /\ FINITE s' ==> 581 (REAL_SUM_IMAGE (\x. REAL_SUM_IMAGE (f x) s') s = 582 REAL_SUM_IMAGE (\x. REAL_SUM_IMAGE (\y. f y x) s) s')``, 583 RW_TAC std_ss [REAL_SUM_IMAGE_REAL_SUM_IMAGE] 584 >> `(s' CROSS s) = IMAGE (\x. (SND x, FST x)) (s CROSS s')` 585 by (RW_TAC std_ss [EXTENSION, IN_CROSS, IN_IMAGE] 586 >> EQ_TAC >- (STRIP_TAC >> Q.EXISTS_TAC `(SND x, FST x)` >> RW_TAC std_ss [PAIR]) 587 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST, SND]) 588 >> POP_ORW 589 >> `FINITE (s CROSS s')` by RW_TAC std_ss [FINITE_CROSS] 590 >> `INJ (\x. (SND x,FST x)) (s CROSS s') (IMAGE (\x. (SND x,FST x)) (s CROSS s'))` 591 by (RW_TAC std_ss [INJ_DEF, IN_IMAGE] >- METIS_TAC [] 592 >> METIS_TAC [PAIR, PAIR_EQ]) 593 >> `REAL_SUM_IMAGE (\x. f (SND x) (FST x)) (IMAGE (\x. (SND x,FST x)) (s CROSS s')) = 594 REAL_SUM_IMAGE ((\x. f (SND x) (FST x)) o (\x. (SND x,FST x))) (s CROSS s')` 595 by METIS_TAC [REAL_SUM_IMAGE_IMAGE] 596 >> POP_ORW 597 >> RW_TAC std_ss [o_DEF]); 598 599val REAL_SUM_IMAGE_EQ_sum = store_thm 600("REAL_SUM_IMAGE_EQ_sum", ``!n r. sum (0,n) r = REAL_SUM_IMAGE r (count n)``, 601 RW_TAC std_ss [] 602 >> Induct_on `n` 603 >- RW_TAC std_ss [sum,REAL_SUM_IMAGE_THM,COUNT_ZERO] 604 >> RW_TAC std_ss [sum,COUNT_SUC,REAL_SUM_IMAGE_THM,FINITE_COUNT] 605 >> Suff `count n DELETE n = count n` 606 >- RW_TAC std_ss [REAL_ADD_COMM] 607 >> RW_TAC std_ss [GSYM DELETE_NON_ELEMENT,IN_COUNT]); 608 609val REAL_SUM_IMAGE_POW = store_thm 610 ("REAL_SUM_IMAGE_POW",``!a s. FINITE s 611 ==> ((REAL_SUM_IMAGE a s) pow 2 = 612 REAL_SUM_IMAGE (\(i,j). a i * a j) (s CROSS s):real)``, 613 RW_TAC std_ss [] 614 >> `(\(i,j). a i * a j) = (\x. (\i j. a i * a j) (FST x) (SND x))` 615 by (RW_TAC std_ss [FUN_EQ_THM] 616 >> Cases_on `x` 617 >> RW_TAC std_ss []) 618 >> POP_ORW 619 >> (MP_TAC o GSYM o Q.SPECL [`s`,`s`,`(\i j. a i * a j)`] o 620 INST_TYPE [``:'b`` |-> ``:'a``]) REAL_SUM_IMAGE_REAL_SUM_IMAGE 621 >> RW_TAC std_ss [REAL_SUM_IMAGE_CMUL] 622 >> RW_TAC std_ss [Once REAL_MUL_COMM,REAL_SUM_IMAGE_CMUL,POW_2]); 623 624val REAL_SUM_IMAGE_EQ = store_thm 625 ("REAL_SUM_IMAGE_EQ", ``!s (f:'a->real) f'. FINITE s /\ (!x. x IN s ==> (f x = f' x)) 626 ==> (REAL_SUM_IMAGE f s = REAL_SUM_IMAGE f' s)``, 627 RW_TAC std_ss [] 628 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF] 629 >> RW_TAC std_ss []); 630 631val REAL_SUM_IMAGE_IN_IF_ALT = store_thm 632 ("REAL_SUM_IMAGE_IN_IF_ALT",``!s f z:real. 633 FINITE s ==> (REAL_SUM_IMAGE f s = REAL_SUM_IMAGE (\x. if x IN s then f x else z) s)``, 634 RW_TAC std_ss [] 635 >> MATCH_MP_TAC REAL_SUM_IMAGE_EQ 636 >> RW_TAC std_ss []); 637 638val REAL_SUM_IMAGE_SUB = store_thm 639 ("REAL_SUM_IMAGE_SUB", ``!s (f:'a -> real) f'. FINITE s ==> 640 (REAL_SUM_IMAGE (\x. f x - f' x) s = 641 REAL_SUM_IMAGE f s - REAL_SUM_IMAGE f' s)``, 642 RW_TAC std_ss [Once real_sub,REAL_SUM_IMAGE_ADD,Once REAL_NEG_MINUS1] 643 >> RW_TAC std_ss [Once real_sub,REAL_SUM_IMAGE_ADD,Once 644 REAL_NEG_MINUS1,REAL_SUM_IMAGE_CMUL] 645 >> RW_TAC std_ss [GSYM REAL_NEG_MINUS1,real_sub]); 646 647val REAL_SUM_IMAGE_MONO_SET = store_thm 648 ("REAL_SUM_IMAGE_MONO_SET", ``!(f:'a -> real) s t. 649 FINITE s /\ FINITE t /\ s SUBSET t /\ (!x. x IN t ==> 0 <= f x) 650 ==> REAL_SUM_IMAGE f s <= REAL_SUM_IMAGE f t``, 651 RW_TAC std_ss [] 652 >> `t = s UNION (t DIFF s)` by RW_TAC std_ss [UNION_DIFF] 653 >> `FINITE (t DIFF s)` by RW_TAC std_ss [FINITE_DIFF] 654 >> `DISJOINT s (t DIFF s)` by ( 655 RW_TAC std_ss [DISJOINT_DEF,IN_DIFF,EXTENSION,GSPECIFICATION, 656 NOT_IN_EMPTY,IN_INTER] >- 657 METIS_TAC []) 658 >> `REAL_SUM_IMAGE f t = REAL_SUM_IMAGE f s + REAL_SUM_IMAGE f (t DIFF s)` 659 by METIS_TAC [REAL_SUM_IMAGE_DISJOINT_UNION] 660 >> POP_ORW 661 >> Suff `0 <= REAL_SUM_IMAGE f (t DIFF s)` 662 >- REAL_ARITH_TAC 663 >> METIS_TAC [REAL_SUM_IMAGE_POS,IN_DIFF]); 664 665val REAL_SUM_IMAGE_CROSS_SYM = store_thm 666 ("REAL_SUM_IMAGE_CROSS_SYM", ``!f s1 s2. FINITE s1 /\ FINITE s2 ==> 667 (REAL_SUM_IMAGE (\(x,y). f (x,y)) (s1 CROSS s2) = REAL_SUM_IMAGE (\(y,x). f (x,y)) (s2 CROSS s1))``, 668 RW_TAC std_ss [] 669 >> `s2 CROSS s1 = IMAGE (\a. (SND a, FST a)) (s1 CROSS s2)` 670 by (RW_TAC std_ss [IN_IMAGE, IN_CROSS,EXTENSION] >> METIS_TAC [FST,SND,PAIR]) 671 >> POP_ORW 672 >> `INJ (\a. (SND a, FST a)) (s1 CROSS s2) (IMAGE (\a. (SND a, FST a)) (s1 CROSS s2))` 673 by (RW_TAC std_ss [INJ_DEF, IN_IMAGE, IN_CROSS] 674 >> METIS_TAC [FST,SND,PAIR]) 675 >> RW_TAC std_ss [REAL_SUM_IMAGE_IMAGE, IMAGE_FINITE, FINITE_CROSS, o_DEF] 676 >> `(\(x,y). f (x,y)) = (\a. f a)` 677 by (RW_TAC std_ss [FUN_EQ_THM] 678 >> Cases_on `a` 679 >> RW_TAC std_ss []) 680 >> RW_TAC std_ss []); 681 682val _ = overload_on ("SIGMA", ``REAL_SUM_IMAGE ``); 683 684val _ = export_theory (); 685