1(* ------------------------------------------------------------------------- *) 2(* Helper Theorems - a collection of useful results -- for Sets. *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "helperSet"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* val _ = load "jcLib"; *) 17open jcLib; 18 19(* open dependent theories *) 20open pred_setTheory; 21 22(* val _ = load "helperNumTheory"; *) 23open helperNumTheory; 24 25(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 26(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 27open arithmeticTheory dividesTheory; 28open gcdTheory; (* for P_EUCLIDES *) 29 30 31(* ------------------------------------------------------------------------- *) 32(* HelperSet Documentation *) 33(* ------------------------------------------------------------------------- *) 34(* Overloading: 35 countFrom m n = IMAGE ($+ m) (count n) 36 s =|= u # v = split s u v 37 equiv_class R s x = {y | y IN s /\ R x y} 38 EVERY_FINITE P = !s. s IN P ==> FINITE s 39 PAIR_DISJOINT P = !s t. s IN P /\ t IN P /\ ~(s = t) ==> DISJOINT s t 40 SET_ADDITIVE f = (f {} = 0) /\ 41 (!s t. FINITE s /\ FINITE t ==> (f (s UNION t) + f (s INTER t) = f s + f t)) 42 SET_MULTIPLICATIVE f = (f {} = 1) /\ 43 (!s t. FINITE s /\ FINITE t ==> (f (s UNION t) * f (s INTER t) = f s * f t)) 44 f PERMUTES s = BIJ f s s 45 PPOW s = (POW s) DIFF {s} 46*) 47(* Definitions and Theorems (# are exported): 48 49 Logic Theorems: 50 EQ_IMP2_THM |- !A B. (A <=> B) <=> (A ==> B) /\ ((A ==> B) ==> B ==> A) 51 BOOL_EQ |- !b1 b2 f. (b1 <=> b2) ==> (f b1 = f b2) 52 IMP_IMP |- !b c d. b /\ (c ==> d) ==> (b ==> c) ==> d 53 AND_IMP_OR_NEG |- !p q. p /\ q ==> p \/ ~q 54 OR_IMP_IMP |- !p q r. (p \/ q ==> r) ==> p /\ ~q ==> r 55 PUSH_IN_INTO_IF |- !b x s t. x IN (if b then s else t) <=> if b then x IN s else x IN t 56 57 Set Theorems: 58 IN_SUBSET |- !s t. s SUBSET t <=> !x. x IN s ==> x IN t 59 DISJOINT_DIFF |- !s t. DISJOINT (s DIFF t) t /\ DISJOINT t (s DIFF t) 60 DISJOINT_DIFF_IFF |- !s t. DISJOINT s t <=> (s DIFF t = s) 61 UNION_DIFF_EQ_UNION |- !s t. s UNION (t DIFF s) = s UNION t 62 INTER_DIFF |- !s t. (s INTER (t DIFF s) = {}) /\ ((t DIFF s) INTER s = {}) 63 BIGINTER_SUBSET |- !P X. P <> {} /\ (!Y. Y IN P ==> Y SUBSET X) ==> BIGINTER P SUBSET X 64 SUBSET_SING |- !s x. {x} SUBSET s /\ SING s <=> (s = {x}) 65 INTER_SING |- !s x. x IN s ==> (s INTER {x} = {x}) 66 ONE_ELEMENT_SING |- !s a. s <> {} /\ (!k. k IN s ==> (k = a)) ==> (s = {a}) 67 SING_ONE_ELEMENT |- !s. s <> {} ==> (SING s <=> !x y. x IN s /\ y IN s ==> (x = y)) 68 SING_ELEMENT |- !s. SING s ==> !x y. x IN s /\ y IN s ==> (x = y) 69 SING_TEST |- !s. SING s <=> s <> {} /\ !x y. x IN s /\ y IN s ==> (x = y) 70 SING_INTER |- !s x. {x} INTER s = if x IN s then {x} else {} 71 IN_SING_OR_EMPTY |- !b x y. x IN (if b then {y} else {}) ==> (x = y) 72 SING_CARD_1 |- !s. SING s ==> (CARD s = 1) 73 CARD_EQ_1 |- !s. FINITE s ==> ((CARD s = 1) <=> SING s) 74 INSERT_DELETE_COMM |- !s x y. x <> y ==> ((x INSERT s) DELETE y = x INSERT s DELETE y) 75 SUBSET_INTER_SUBSET |- !s t u. s SUBSET u ==> s INTER t SUBSET u 76 DIFF_DIFF_EQ_INTER |- !s t. s DIFF (s DIFF t) = s INTER t 77 SET_EQ_BY_DIFF |- !s t. (s = t) <=> s SUBSET t /\ (t DIFF s = {}) 78 SUBSET_INSERT_SUBSET|- !s t. s SUBSET t ==> !x. x INSERT s SUBSET x INSERT t 79 INSERT_SUBSET_SUBSET|- !s t x. x NOTIN s /\ x INSERT s SUBSET t ==> s SUBSET t DELETE x 80 DIFF_DELETE |- !s t x. s DIFF t DELETE x = s DIFF (x INSERT t) 81 SUBSET_DIFF_CARD |- !a b. FINITE a /\ b SUBSET a ==> (CARD (a DIFF b) = CARD a - CARD b) 82 SUBSET_SING_IFF |- !s x. s SUBSET {x} <=> (s = {}) \/ (s = {x}) 83 84 Image and Bijection: 85 INJ_CONG |- !f g s t. (!x. x IN s ==> (f x = g x)) ==> (INJ f s t <=> INJ g s t) 86 SURJ_CONG |- !f g s t. (!x. x IN s ==> (f x = g x)) ==> (SURJ f s t <=> SURJ g s t) 87 BIJ_CONG |- !f g s t. (!x. x IN s ==> (f x = g x)) ==> (BIJ f s t <=> BIJ g s t) 88 INJ_ELEMENT |- !f s t x. INJ f s t /\ x IN s ==> f x IN t 89 SURJ_ELEMENT |- !f s t x. SURJ f s t /\ x IN s ==> f x IN t 90 BIJ_ELEMENT |- !f s t x. BIJ f s t /\ x IN s ==> f x IN t 91 INJ_UNIV |- !f s t. INJ f s t ==> INJ f s univ(:'b) 92 INJ_SUBSET_UNIV |- !f s. INJ f univ(:'a) univ(:'b) ==> INJ f s univ(:'b) 93 INJ_IMAGE_BIJ |- !f s. INJ f s univ(:'b) ==> BIJ f s (IMAGE f s) 94 INJ_IMAGE_EQ |- !P f. INJ f P univ(:'b) ==> !s t. s SUBSET P /\ t SUBSET P ==> 95 ((IMAGE f s = IMAGE f t) <=> (s = t)) 96 INJ_IMAGE_INTER |- !P f. INJ f P univ(:'b) ==> !s t. s SUBSET P /\ t SUBSET P ==> 97 (IMAGE f (s INTER t) = IMAGE f s INTER IMAGE f t) 98 INJ_IMAGE_DISJOINT |- !P f. INJ f P univ(:'b) ==> !s t. s SUBSET P /\ t SUBSET P ==> 99 (DISJOINT s t <=> DISJOINT (IMAGE f s) (IMAGE f t)) 100 INJ_I |- !s. INJ I s univ(:'a) 101 INJ_I_IMAGE |- !s f. INJ I (IMAGE f s) univ(:'b) 102 BIJ_ALT |- !f s t. BIJ f s t <=> 103 (!x. x IN s ==> f x IN t) /\ !y. y IN t ==> ?!x. x IN s /\ (f x = y) 104 BIJ_IS_INJ |- !f s t. BIJ f s t ==> 105 !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y) 106 INJ_EQ_11 |- !f s x y. INJ f s s /\ x IN s /\ y IN s ==> ((f x = f y) <=> (x = y)) 107 BIJ_I_SAME |- !s. BIJ I s s 108 # IMAGE_I |- !s. IMAGE I s = s 109 IMAGE_K |- !s. s <> {} ==> !e. IMAGE (K e) s = {e} 110 IMAGE_SING |- !f x. IMAGE f {x} = {f x} 111 IMAGE_SUBSET_TARGET |- !f s t. (!x. x IN s ==> f x IN t) <=> IMAGE f s SUBSET t 112 IMAGE_ELEMENT_CONDITION |- !f. (!x y. (f x = f y) ==> (x = y)) ==> !s e. e IN s <=> f e IN IMAGE f s 113 BIGUNION_ELEMENTS_SING |- !s. BIGUNION (IMAGE (\x. {x}) s) = s 114 IMAGE_INJ_SUBSET_DIFF |- !s t f. s SUBSET t /\ INJ f t univ(:'b) ==> 115 (IMAGE f (t DIFF s) = IMAGE f t DIFF IMAGE f s) 116 117 More Theorems and Sets for Counting: 118 COUNT_0 |- count 0 = {} 119 COUNT_1 |- count 1 = {0} 120 COUNT_NOT_SELF |- !n. n NOTIN count n 121 COUNT_EQ_EMPTY |- !n. (count n = {}) <=> (n = 0) 122 COUNT_SUBSET |- !m n. m <= n ==> count m SUBSET count n 123 COUNT_SUC_SUBSET |- !n t. count (SUC n) SUBSET t <=> count n SUBSET t /\ n IN t 124 DIFF_COUNT_SUC |- !n t. t DIFF count (SUC n) = t DIFF count n DELETE n 125 COUNT_SUC_BY_SUC |- !n. count (SUC n) = 0 INSERT IMAGE SUC (count n) 126 IMAGE_COUNT_SUC |- !f n. IMAGE f (count (SUC n)) = f n INSERT IMAGE f (count n) 127 IMAGE_COUNT_SUC_BY_SUC 128 |- !f n. IMAGE f (count (SUC n)) = f 0 INSERT IMAGE (f o SUC) (count n) 129 countFrom_0 |- !m. countFrom m 0 = {} 130 countFrom_SUC |- !m n m n. countFrom m (SUC n) = m INSERT countFrom (m + 1) n 131 countFrom_first |- !m n. 0 < n ==> m IN countFrom m n 132 countFrom_less |- !m n x. x < m ==> x NOTIN countFrom m n 133 count_by_countFrom |- !n. count n = countFrom 0 n 134 count_SUC_by_countFrom |- !n. count (SUC n) = 0 INSERT countFrom 1 n 135 136 CARD_UNION_3_EQN |- !a b c. FINITE a /\ FINITE b /\ FINITE c ==> 137 (CARD (a UNION b UNION c) = 138 CARD a + CARD b + CARD c + CARD (a INTER b INTER c) - 139 CARD (a INTER b) - CARD (b INTER c) - CARD (a INTER c)) 140 CARD_UNION_3_DISJOINT 141 |- !a b c. FINITE a /\ FINITE b /\ FINITE c /\ 142 DISJOINT a b /\ DISJOINT b c /\ DISJOINT a c ==> 143 (CARD (a UNION b UNION c) = CARD a + CARD b + CARD c) 144 145 Maximum and Minimum of a Set: 146 MAX_SET_LESS |- !s n. FINITE s /\ MAX_SET s < n ==> !x. x IN s ==> x < n 147 MAX_SET_TEST |- !s. FINITE s /\ s <> {} ==> 148 !x. x IN s /\ (!y. y IN s ==> y <= x) ==> (x = MAX_SET s) 149 MIN_SET_TEST |- !s. s <> {} ==> 150 !x. x IN s /\ (!y. y IN s ==> x <= y) ==> (x = MIN_SET s) 151 MAX_SET_TEST_IFF |- !s. FINITE s /\ s <> {} ==> !x. x IN s ==> 152 ((MAX_SET s = x) <=> !y. y IN s ==> y <= x) 153 MIN_SET_TEST_IFF |- !s. s <> {} ==> !x. x IN s ==> 154 ((MIN_SET s = x) <=> !y. y IN s ==> x <= y) 155 MAX_SET_EMPTY |- MAX_SET {} = 0 156 MAX_SET_SING |- !e. MAX_SET {e} = e 157 MAX_SET_IN_SET |- !s. FINITE s /\ s <> {} ==> MAX_SET s IN s 158 MAX_SET_PROPERTY |- !s. FINITE s ==> !x. x IN s ==> x <= MAX_SET s 159 MIN_SET_SING |- !e. MIN_SET {e} = e 160 MIN_SET_IN_SET |- !s. s <> {} ==> MIN_SET s IN s 161 MIN_SET_PROPERTY |- !s. s <> {} ==> !x. x IN s ==> MIN_SET s <= x 162 MAX_SET_DELETE |- !s. FINITE s /\ s <> {} /\ s <> {MIN_SET s} ==> 163 (MAX_SET (s DELETE MIN_SET s) = MAX_SET s) 164 MAX_SET_EQ_0 |- !s. FINITE s ==> ((MAX_SET s = 0) <=> (s = {}) \/ (s = {0})) 165 MIN_SET_EQ_0 |- !s. s <> {} ==> ((MIN_SET s = 0) <=> 0 IN s) 166 MAX_SET_IMAGE_SUC_COUNT |- !n. MAX_SET (IMAGE SUC (count n)) = n 167 MAX_SET_IMAGE_with_HALF |- !f c x. HALF x <= c ==> f x <= MAX_SET {f x | HALF x <= c} 168 MAX_SET_IMAGE_with_DIV |- !f b c x. 0 < b /\ x DIV b <= c ==> f x <= MAX_SET {f x | x DIV b <= c} 169 MAX_SET_IMAGE_with_DEC |- !f b c x. x - b <= c ==> f x <= MAX_SET {f x | x - b <= c} 170 171 Finite and Cardinality Theorems: 172 INJ_CARD_IMAGE_EQN |- !f s. INJ f s univ(:'b) /\ FINITE s ==> (CARD (IMAGE f s) = CARD s) 173 FINITE_INJ_AS_SURJ |- !f s t. INJ f s t /\ FINITE s /\ FINITE t /\ (CARD s = CARD t) ==> SURJ f s t 174 FINITE_COUNT_IMAGE |- !P n. FINITE {P x | x < n} 175 FINITE_BIJ_PROPERTY |- !f s t. FINITE s /\ BIJ f s t ==> FINITE t /\ (CARD s = CARD t) 176 FINITE_CARD_IMAGE |- !s f. (!x y. (f x = f y) <=> (x = y)) /\ FINITE s ==> (CARD (IMAGE f s) = CARD s) 177 CARD_IMAGE_SUC |- !s. FINITE s ==> (CARD (IMAGE SUC s) = CARD s) 178 CARD_UNION_DISJOINT |- !s t. FINITE s /\ FINITE t /\ DISJOINT s t ==> (CARD (s UNION t) = CARD s + CARD t) 179 image_mod_subset_count |- !s n. 0 < n ==> IMAGE (\x. x MOD n) s SUBSET count n 180 card_mod_image |- !s n. 0 < n ==> CARD (IMAGE (\x. x MOD n) s) <= n 181 card_mod_image_nonzero |- !s n. 0 < n /\ 0 NOTIN IMAGE (\x. x MOD n) s ==> 182 CARD (IMAGE (\x. x MOD n) s) < n 183 184 Partition Property: 185 finite_partition_property |- !s. FINITE s ==> !u v. s =|= u # v ==> ((u = {}) <=> (v = s)) 186 finite_partition_by_predicate |- !s. FINITE s ==> !P. (let u = {x | x IN s /\ P x} in 187 let v = {x | x IN s /\ ~P x} in 188 FINITE u /\ FINITE v /\ s =|= u # v) 189 partition_by_subset |- !s u. u SUBSET s ==> (let v = s DIFF u in s =|= u # v) 190 partition_by_element |- !s x. x IN s ==> s =|= {x} # s DELETE x 191 192 Splitting of a set: 193 SPLIT_EMPTY |- !s t. s =|= {} # t <=> s = t 194 SPLIT_UNION |- !s u v a b. s =|= u # v /\ v =|= a # b ==> s =|= u UNION a # b /\ u UNION a =|= u # a 195 SPLIT_EQ |- !s u v. s =|= u # v <=> u SUBSET s /\ v = s DIFF u 196 SPLIT_SYM |- !s u v. s =|= u # v <=> s =|= v # u 197 SPLIT_SYM_IMP |- !s u v. s =|= u # v ==> s =|= v # u 198 SPLIT_SING |- !s v x. s =|= {x} # v <=> x IN s /\ v = s DELETE x 199 SPLIT_SUBSETS |- !s u v. s =|= u # v ==> u SUBSET s /\ v SUBSET s 200 SPLIT_FINITE |- !s u v. FINITE s /\ s =|= u # v ==> FINITE u /\ FINITE v 201 SPLIT_CARD |- !s u v. FINITE s /\ s =|= u # v ==> (CARD s = CARD u + CARD v) 202 SPLIT_EQ_DIFF |- !s u v. s =|= u # v <=> (u = s DIFF v) /\ (v = s DIFF u) 203 SPLIT_BY_SUBSET |- !s u. u SUBSET s ==> (let v = s DIFF u in s =|= u # v) 204 SUBSET_DIFF_DIFF |- !s t. t SUBSET s ==> (s DIFF (s DIFF t) = t) 205 SUBSET_DIFF_EQ |- !s1 s2 t. s1 SUBSET t /\ s2 SUBSET t /\ (t DIFF s1 = t DIFF s2) ==> (s1 = s2) 206 207 Bijective Inverses: 208 BIJ_LINV_ELEMENT |- !f s t. BIJ f s t ==> !x. x IN t ==> LINV f s x IN s 209 BIJ_LINV_THM |- !f s t. BIJ f s t ==> 210 (!x. x IN s ==> (LINV f s (f x) = x)) /\ !x. x IN t ==> (f (LINV f s x) = x) 211 BIJ_RINV_INV |- !f s t. BIJ f s t /\ (!y. y IN t ==> RINV f s y IN s) ==> 212 !x. x IN s ==> (RINV f s (f x) = x) 213 BIJ_RINV_BIJ |- !f s t. BIJ f s t /\ (!y. y IN t ==> RINV f s y IN s) ==> BIJ (RINV f s) t s 214 LINV_SUBSET |- !f s t. INJ f t t /\ s SUBSET t ==> !x. x IN s ==> (LINV f t (f x) = x) 215 216 Iteration, Summation and Product: 217 ITSET_SING |- !f x b. ITSET f {x} b = f x b 218 ITSET_PROPERTY |- !s f b. FINITE s /\ s <> {} ==> 219 (ITSET f s b = ITSET f (REST s) (f (CHOICE s) b)) 220 ITSET_CONG |- !f g. (f = g) ==> (ITSET f = ITSET g) 221 ITSET_REDUCTION |- !f. (!x y z. f x (f y z) = f y (f x z)) ==> 222 !s x b. FINITE s /\ x NOTIN s ==> (ITSET f (x INSERT s) b = f x (ITSET f s b)) 223 224 Rework of ITSET Theorems: 225 closure_comm_assoc_fun_def |- !f s. closure_comm_assoc_fun f s <=> 226 (!x y. x IN s /\ y IN s ==> f x y IN s) /\ 227 !x y z. x IN s /\ y IN s /\ z IN s ==> (f x (f y z) = f y (f x z)) 228 SUBSET_COMMUTING_ITSET_INSERT |- !f s t. FINITE s /\ s SUBSET t /\ closure_comm_assoc_fun f t ==> 229 !x b::t. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b) 230 SUBSET_COMMUTING_ITSET_REDUCTION |- !f s t. FINITE s /\ s SUBSET t /\ closure_comm_assoc_fun f t ==> 231 !x b::t. ITSET f s (f x b) = f x (ITSET f s b) 232 SUBSET_COMMUTING_ITSET_RECURSES |- !f s t. FINITE s /\ s SUBSET t /\ closure_comm_assoc_fun f t ==> 233 !x b::t. ITSET f (x INSERT s) b = f x (ITSET f (s DELETE x) b) 234 235 SUM_IMAGE and PROD_IMAGE Theorems: 236 SUM_IMAGE_EMPTY |- !f. SIGMA f {} = 0 237 SUM_IMAGE_INSERT |- !f s. FINITE s ==> !e. e NOTIN s ==> (SIGMA f (e INSERT s) = f e + SIGMA f s) 238 SUM_IMAGE_AS_SUM_SET |- !s. FINITE s ==> !f. (!x y. (f x = f y) ==> (x = y)) ==> 239 (SIGMA f s = SUM_SET (IMAGE f s)) 240 SIGMA_CONSTANT |- !s. FINITE s ==> !f k. (!x. x IN s ==> (f x = k)) ==> (SIGMA f s = k * CARD s) 241 SUM_IMAGE_CONSTANT |- !s. FINITE s ==> !c. SIGMA (K c) s = c * CARD s 242 SIGMA_CARD_CONSTANT |- !n s. FINITE s ==> (!e. e IN s ==> (CARD e = n)) ==> (SIGMA CARD s = n * CARD s) 243 SIGMA_CARD_FACTOR |- !n s. FINITE s ==> (!e. e IN s ==> n divides CARD e) ==> n divides SIGMA CARD s 244 SIGMA_CONG |- !s f1 f2. (!x. x IN s ==> (f1 x = f2 x)) ==> (SIGMA f1 s = SIGMA f2 s) 245 CARD_AS_SIGMA |- !s. FINITE s ==> (CARD s = SIGMA (\x. 1) s) 246 CARD_EQ_SIGMA |- !s. FINITE s ==> (CARD s = SIGMA (K 1) s) 247 SIGMA_LE_SIGMA |- !s. FINITE s ==> !f g. (!x. x IN s ==> f x <= g x) ==> SIGMA f s <= SIGMA g s 248 SUM_IMAGE_UNION_EQN |- !s t. FINITE s /\ FINITE t ==> 249 !f. SIGMA f (s UNION t) + SIGMA f (s INTER t) = SIGMA f s + SIGMA f t 250 SUM_IMAGE_DISJOINT |- !s t. FINITE s /\ FINITE t /\ DISJOINT s t ==> 251 !f. SIGMA f (s UNION t) = SIGMA f s + SIGMA f t 252 SUM_IMAGE_MONO_LT |- !s. FINITE s /\ s <> {} ==> 253 !f g. (!x. x IN s ==> f x < g x) ==> SIGMA f s < SIGMA g s 254 SUM_IMAGE_PSUBSET_LT |- !f s t. FINITE s /\ t PSUBSET s /\ (!x. x IN s ==> f x <> 0) ==> 255 SIGMA f t < SIGMA f s 256 257 PROD_IMAGE_EMPTY |- !f. PI f {} = 1 258 PROD_IMAGE_INSERT |- !s. FINITE s ==> !f e. e NOTIN s ==> (PI f (e INSERT s) = f e * PI f s) 259 PROD_IMAGE_DELETE |- !s. FINITE s ==> !f e. 0 < f e ==> 260 (PI f (s DELETE e) = if e IN s then PI f s DIV f e else PI f s) 261 PROD_IMAGE_CONG |- !s f1 f2. (!x. x IN s ==> (f1 x = f2 x)) ==> (PI f1 s = PI f2 s) 262 PI_CONSTANT |- !s. FINITE s ==> !f k. (!x. x IN s ==> (f x = k)) ==> (PI f s = k ** CARD s) 263 PROD_IMAGE_CONSTANT |- !s. FINITE s ==> !c. PI (K c) s = c ** CARD s 264 265 SUM_SET and PROD_SET Theorems: 266 SUM_SET_INSERT |- !s x. FINITE s /\ x NOTIN s ==> (SUM_SET (x INSERT s) = x + SUM_SET s) 267 SUM_SET_IMAGE_EQN |- !s. FINITE s ==> !f. INJ f s univ(:num) ==> (SUM_SET (IMAGE f s) = SIGMA f s) 268 SUM_SET_COUNT |- !n. SUM_SET (count n) = n * (n - 1) DIV 2 269 270 PROD_SET_SING |- !x. PROD_SET {x} = x 271 PROD_SET_NONZERO |- !s. FINITE s /\ 0 NOTIN s ==> 0 < PROD_SET s 272 PROD_SET_LESS |- !s. FINITE s /\ s <> {} /\ 0 NOTIN s ==> 273 !f. INJ f s univ(:num) /\ (!x. x < f x) ==> PROD_SET s < PROD_SET (IMAGE f s) 274 PROD_SET_LESS_SUC |- !s. FINITE s /\ s <> {} /\ 0 NOTIN s ==> PROD_SET s < PROD_SET (IMAGE SUC s) 275 PROD_SET_DIVISORS |- !s. FINITE s ==> !n x. x IN s /\ n divides x ==> n divides (PROD_SET s) 276 PROD_SET_INSERT |- !x s. FINITE s /\ x NOTIN s ==> (PROD_SET (x INSERT s) = x * PROD_SET s) 277 PROD_SET_IMAGE_EQN |- !s. FINITE s ==> !f. INJ f s univ(:num) ==> (PROD_SET (IMAGE f s) = PI f s) 278 PROD_SET_IMAGE_EXP |- !n. 1 < n ==> !m. PROD_SET (IMAGE (\j. n ** j) (count m)) = n ** SUM_SET (count m) 279 PROD_SET_ELEMENT_DIVIDES |- !s x. FINITE s /\ x IN s ==> x divides PROD_SET s 280 PROD_SET_LESS_EQ |- !s. FINITE s ==> !f g. INJ f s univ(:num) /\ INJ g s univ(:num) /\ 281 (!x. x IN s ==> f x <= g x) ==> PROD_SET (IMAGE f s) <= PROD_SET (IMAGE g s) 282 PROD_SET_LE_CONSTANT |- !s. FINITE s ==> !n. (!x. x IN s ==> x <= n) ==> PROD_SET s <= n ** CARD s 283 PROD_SET_PRODUCT_GE_CONSTANT |- !s. FINITE s ==> !n f g. INJ f s univ(:num) /\ INJ g s univ(:num) /\ 284 (!x. x IN s ==> n <= f x * g x) ==> 285 n ** CARD s <= PROD_SET (IMAGE f s) * PROD_SET (IMAGE g s) 286 PROD_SET_PRODUCT_BY_PARTITION |- !s. FINITE s ==> 287 !u v. s =|= u # v ==> (PROD_SET s = PROD_SET u * PROD_SET v) 288 289 Partition and Equivalent Class: 290 equiv_class_element |- !R s x y. y IN equiv_class R s x <=> y IN s /\ R x y 291 equiv_class_eq |- !R s x y. R equiv_on s /\ x IN s /\ y IN s ==> 292 ((equiv_class R s x = equiv_class R s y) <=> R x y) 293 equiv_on_subset |- !R s t. R equiv_on s /\ t SUBSET s ==> R equiv_on t 294 partition_on_empty |- !R. partition R {} = {} 295 partition_element |- !R s t. t IN partition R s <=> ?x. x IN s /\ (t = equiv_class R s x) 296 partition_elements |- !R s. partition R s = IMAGE (\x. equiv_class R s x) s 297 partition_as_image |- !R s. partition R s = IMAGE (\x. equiv_class R s x) s 298 partition_cong |- !R1 R2 s1 s2. (R1 = R2) /\ (s1 = s2) ==> (partition R1 s1 = partition R2 s2) 299 equal_partition_card |- !R s n. FINITE s /\ R equiv_on s /\ 300 (!e. e IN partition R s ==> (CARD e = n)) ==> (CARD s = n * CARD (partition R s)) 301 equal_partition_factor |- !R s n. FINITE s /\ R equiv_on s /\ 302 (!e. e IN partition R s ==> CARD e = n) ==> n divides CARD s 303 factor_partition_card |- !R s n. FINITE s /\ R equiv_on s /\ 304 (!e. e IN partition R s ==> n divides CARD e) ==> n divides CARD s 305 306 pair_disjoint_subset |- !s t. t SUBSET s /\ PAIR_DISJOINT s ==> PAIR_DISJOINT t 307 disjoint_bigunion_add_fun |- !P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> 308 !f. SET_ADDITIVE f ==> (f (BIGUNION P) = SIGMA f P) 309 set_additive_card |- SET_ADDITIVE CARD 310 disjoint_bigunion_card |- !P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> 311 (CARD (BIGUNION P) = SIGMA CARD P) 312 set_additive_sigma |- !f. SET_ADDITIVE (SIGMA f) 313 disjoint_bigunion_sigma |- !P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> 314 !f. SIGMA f (BIGUNION P) = SIGMA (SIGMA f) P 315 set_add_fun_by_partition |- !R s. R equiv_on s /\ FINITE s ==> 316 !f. SET_ADDITIVE f ==> (f s = SIGMA f (partition R s)) 317 set_card_by_partition |- !R s. R equiv_on s /\ FINITE s ==> (CARD s = SIGMA CARD (partition R s)) 318 set_sigma_by_partition |- !R s. R equiv_on s /\ FINITE s ==> 319 !f. SIGMA f s = SIGMA (SIGMA f) (partition R s) 320 disjoint_bigunion_mult_fun |- !P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> 321 !f. SET_MULTIPLICATIVE f ==> (f (BIGUNION P) = PI f P) 322 set_mult_fun_by_partition |- !R s. R equiv_on s /\ FINITE s ==> 323 !f. SET_MULTIPLICATIVE f ==> (f s = PI f (partition R s)) 324 sum_image_by_composition |- !s. FINITE s ==> !g. INJ g s univ(:'a) ==> 325 !f. SIGMA f (IMAGE g s) = SIGMA (f o g) s 326 sum_image_by_permutation |- !s. FINITE s ==> !g. g PERMUTES s ==> !f. SIGMA (f o g) s = SIGMA f s 327 sum_image_by_composition_with_partial_inj 328 |- !s. FINITE s ==> !f. (f {} = 0) ==> 329 !g. (!t. FINITE t /\ (!x. x IN t ==> g x <> {}) ==> INJ g t univ(:'b -> bool)) ==> 330 (SIGMA f (IMAGE g s) = SIGMA (f o g) s) 331 sum_image_by_composition_without_inj 332 |- !s. FINITE s ==> 333 !f g. (!x y. x IN s /\ y IN s /\ (g x = g y) ==> (x = y) \/ (f (g x) = 0)) ==> 334 (SIGMA f (IMAGE g s) = SIGMA (f o g) s) 335 336 Pre-image Theorems: 337 preimage_def |- !f s y. preimage f s y = {x | x IN s /\ (f x = y)} 338 preimage_element |- !f s x y. x IN preimage f s y <=> x IN s /\ (f x = y) 339 in_preimage |- !f s x y. x IN preimage f s y <=> x IN s /\ (f x = y) 340 preimage_subset_of_domain |- !f s y. preimage f s y SUBSET s 341 preimage_property |- !f s y x. x IN preimage f s y ==> (f x = y) 342 preimage_of_image |- !f s x. x IN s ==> x IN preimage f s (f x) 343 preimage_choice_property |- !f s y. y IN IMAGE f s ==> 344 CHOICE (preimage f s y) IN s /\ (f (CHOICE (preimage f s y)) = y) 345 preimage_inj |- !f s. INJ f s univ(:'b) ==> !x. x IN s ==> (preimage f s (f x) = {x}) 346 preimage_inj_choice |- !f s. INJ f s univ(:'b) ==> !x. x IN s ==> (CHOICE (preimage f s (f x)) = x) 347 348 Set of Proper Subsets: 349 IN_PPOW |- !s e. e IN PPOW s ==> e PSUBSET s 350 FINITE_PPOW |- !s. FINITE s ==> FINITE (PPOW s) 351 CARD_PPOW |- !s. FINITE s ==> (CARD (PPOW s) = PRE (2 ** CARD s) 352 CARD_PPOW_EQN |- !s. FINITE s ==> (CARD (PPOW s) = 2 ** CARD s - 1) 353 354 Useful Theorems: 355 in_prime |- !p. p IN prime <=> prime p 356 PROD_SET_EUCLID |- !s. FINITE s ==> !p. prime p /\ p divides (PROD_SET s) ==> ?b. b IN s /\ p divides b 357 358*) 359 360(* ------------------------------------------------------------------------- *) 361(* Logic Theorems. *) 362(* ------------------------------------------------------------------------- *) 363 364(* Theorem: (A <=> B) <=> (A ==> B) /\ ((A ==> B) ==> (B ==> A)) *) 365(* Proof: by logic. *) 366val EQ_IMP2_THM = store_thm( 367 "EQ_IMP2_THM", 368 ``!A B. (A <=> B) <=> (A ==> B) /\ ((A ==> B) ==> (B ==> A))``, 369 metis_tac[]); 370 371(* Theorem: (b1 = b2) ==> (f b1 = f b2) *) 372(* Proof: by substitution. *) 373val BOOL_EQ = store_thm( 374 "BOOL_EQ", 375 ``!b1:bool b2:bool f. (b1 = b2) ==> (f b1 = f b2)``, 376 simp[]); 377 378(* Theorem: b /\ (c ==> d) ==> ((b ==> c) ==> d) *) 379(* Proof: by logical implication. *) 380val IMP_IMP = store_thm( 381 "IMP_IMP", 382 ``!b c d. b /\ (c ==> d) ==> ((b ==> c) ==> d)``, 383 metis_tac[]); 384 385(* Theorem: p /\ q ==> p \/ ~q *) 386(* Proof: 387 Note p /\ q ==> p by AND1_THM 388 and p ==> p \/ ~q by OR_INTRO_THM1 389 Thus p /\ q ==> p \/ ~q 390*) 391val AND_IMP_OR_NEG = store_thm( 392 "AND_IMP_OR_NEG", 393 ``!p q. p /\ q ==> p \/ ~q``, 394 metis_tac[]); 395 396(* Theorem: (p \/ q ==> r) ==> (p /\ ~q ==> r) *) 397(* Proof: 398 (p \/ q) ==> r 399 = ~(p \/ q) \/ r by IMP_DISJ_THM 400 = (~p /\ ~q) \/ r by DE_MORGAN_THM 401 ==> (~p \/ q) \/ r by AND_IMP_OR_NEG 402 = ~(p /\ ~q) \/ r by DE_MORGAN_THM 403 = (p /\ ~q) ==> r by IMP_DISJ_THM 404*) 405val OR_IMP_IMP = store_thm( 406 "OR_IMP_IMP", 407 ``!p q r. ((p \/ q) ==> r) ==> ((p /\ ~q) ==> r)``, 408 metis_tac[]); 409 410(* Theorem: x IN (if b then s else t) <=> if b then x IN s else x IN t *) 411(* Proof: by boolTheory.COND_RAND: 412 |- !f b x y. f (if b then x else y) = if b then f x else f y 413*) 414val PUSH_IN_INTO_IF = store_thm( 415 "PUSH_IN_INTO_IF", 416 ``!b x s t. x IN (if b then s else t) <=> if b then x IN s else x IN t``, 417 rw_tac std_ss[]); 418 419(* ------------------------------------------------------------------------- *) 420(* Set Theorems. *) 421(* ------------------------------------------------------------------------- *) 422 423(* use of IN_SUBSET *) 424val IN_SUBSET = save_thm("IN_SUBSET", SUBSET_DEF); 425(* 426val IN_SUBSET = |- !s t. s SUBSET t <=> !x. x IN s ==> x IN t: thm 427*) 428 429(* Theorem: DISJOINT (s DIFF t) t /\ DISJOINT t (s DIFF t) *) 430(* Proof: 431 DISJOINT (s DIFF t) t 432 <=> (s DIFF t) INTER t = {} by DISJOINT_DEF 433 <=> !x. x IN (s DIFF t) INTER t <=> F by MEMBER_NOT_EMPTY 434 x IN (s DIFF t) INTER t 435 <=> x IN (s DIFF t) /\ x IN t by IN_INTER 436 <=> (x IN s /\ x NOTIN t) /\ x IN t by IN_DIFF 437 <=> x IN s /\ (x NOTIN t /\ x IN t) 438 <=> x IN s /\ F 439 <=> F 440 Similarly for DISJOINT t (s DIFF t) 441*) 442val DISJOINT_DIFF = store_thm( 443 "DISJOINT_DIFF", 444 ``!s t. (DISJOINT (s DIFF t) t) /\ (DISJOINT t (s DIFF t))``, 445 (rw[DISJOINT_DEF, EXTENSION] >> metis_tac[])); 446 447(* Theorem: DISJOINT s t <=> ((s DIFF t) = s) *) 448(* Proof: by DISJOINT_DEF, DIFF_DEF, EXTENSION *) 449val DISJOINT_DIFF_IFF = store_thm( 450 "DISJOINT_DIFF_IFF", 451 ``!s t. DISJOINT s t <=> ((s DIFF t) = s)``, 452 rw[DISJOINT_DEF, DIFF_DEF, EXTENSION] >> 453 metis_tac[]); 454 455(* Theorem: s UNION (t DIFF s) = s UNION t *) 456(* Proof: 457 By EXTENSION, 458 x IN (s UNION (t DIFF s)) 459 = x IN s \/ x IN (t DIFF s) by IN_UNION 460 = x IN s \/ (x IN t /\ x NOTIN s) by IN_DIFF 461 = (x IN s \/ x IN t) /\ (x IN s \/ x NOTIN s) by LEFT_OR_OVER_AND 462 = (x IN s \/ x IN t) /\ T by EXCLUDED_MIDDLE 463 = x IN (s UNION t) by IN_UNION 464*) 465val UNION_DIFF_EQ_UNION = store_thm( 466 "UNION_DIFF_EQ_UNION", 467 ``!s t. s UNION (t DIFF s) = s UNION t``, 468 rw_tac std_ss[EXTENSION, IN_UNION, IN_DIFF] >> 469 metis_tac[]); 470 471(* Theorem: (s INTER (t DIFF s) = {}) /\ ((t DIFF s) INTER s = {}) *) 472(* Proof: by DISJOINT_DIFF, GSYM DISJOINT_DEF *) 473val INTER_DIFF = store_thm( 474 "INTER_DIFF", 475 ``!s t. (s INTER (t DIFF s) = {}) /\ ((t DIFF s) INTER s = {})``, 476 rw[DISJOINT_DIFF, GSYM DISJOINT_DEF]); 477 478(* Theorem: P <> {} /\ (!Y. Y IN P ==> Y SUBSET X) ==> (BIGINTER P) SUBSET X *) 479(* Proof: 480 Since P <> {}, let s IN P by MEMBER_NOT_EMPTY 481 Since s IN P, s SUBSET X by given 482 Now, x IN BIGINTER P 483 <=> !Y. Y IN P ==> x IN Y by IN_BIGINTER 484 Since s IN P, x IN s 485 Since s SUBSET X, x IN X by IN_SUBSET 486 Therefore (BIGINTER P) SUBSET X by IN_SUBSET 487*) 488val BIGINTER_SUBSET = store_thm( 489 "BIGINTER_SUBSET", 490 ``!P X. P <> {} /\ (!Y. Y IN P ==> Y SUBSET X) ==> (BIGINTER P) SUBSET X``, 491 rw[SUBSET_DEF] >> 492 metis_tac[MEMBER_NOT_EMPTY]); 493 494(* Theorem: {x} SUBSET s /\ SING s <=> (s = {x}) *) 495(* Proof: 496 Note {x} SUBSET s ==> x IN s by SUBSET_DEF 497 and SING s ==> ?y. s = {y} by SING_DEF 498 Thus x IN {y} ==> x = y by IN_SING 499*) 500val SUBSET_SING = store_thm( 501 "SUBSET_SING", 502 ``!s x. {x} SUBSET s /\ SING s <=> (s = {x})``, 503 metis_tac[SING_DEF, IN_SING, SUBSET_DEF]); 504 505(* Theorem: !x. x IN s ==> s INTER {x} = {x} *) 506(* Proof: 507 s INTER {x} 508 = {x | x IN s /\ x IN {x}} by INTER_DEF 509 = {x' | x' IN s /\ x' = x} by IN_SING 510 = {x} by EXTENSION 511*) 512val INTER_SING = store_thm( 513 "INTER_SING", 514 ``!s x. x IN s ==> (s INTER {x} = {x})``, 515 rw[INTER_DEF, EXTENSION, EQ_IMP_THM]); 516 517(* Theorem: A non-empty set with all elements equal to a is the singleton {a} *) 518(* Proof: by singleton definition. *) 519val ONE_ELEMENT_SING = store_thm( 520 "ONE_ELEMENT_SING", 521 ``!s a. s <> {} /\ (!k. k IN s ==> (k = a)) ==> (s = {a})``, 522 rw[EXTENSION, EQ_IMP_THM] >> 523 metis_tac[]); 524 525(* Theorem: s <> {} ==> (SING s <=> !x y. x IN s /\ y IN s ==> (x = y)) *) 526(* Proof: 527 If part: SING s ==> !x y. x IN s /\ y IN s ==> (x = y)) 528 SING s ==> ?t. s = {t} by SING_DEF 529 x IN s ==> x = t by IN_SING 530 y IN s ==> y = t by IN_SING 531 Hence x = y 532 Only-if part: !x y. x IN s /\ y IN s ==> (x = y)) ==> SING s 533 True by ONE_ELEMENT_SING 534*) 535val SING_ONE_ELEMENT = store_thm( 536 "SING_ONE_ELEMENT", 537 ``!s. s <> {} ==> (SING s <=> !x y. x IN s /\ y IN s ==> (x = y))``, 538 metis_tac[SING_DEF, IN_SING, ONE_ELEMENT_SING]); 539 540(* Theorem: SING s ==> (!x y. x IN s /\ y IN s ==> (x = y)) *) 541(* Proof: 542 Note SING s <=> ?z. s = {z} by SING_DEF 543 and x IN {z} <=> x = z by IN_SING 544 and y IN {z} <=> y = z by IN_SING 545 Thus x = y 546*) 547val SING_ELEMENT = store_thm( 548 "SING_ELEMENT", 549 ``!s. SING s ==> (!x y. x IN s /\ y IN s ==> (x = y))``, 550 metis_tac[SING_DEF, IN_SING]); 551(* Note: the converse really needs s <> {} *) 552 553(* Theorem: SING s <=> s <> {} /\ (!x y. x IN s /\ y IN s ==> (x = y)) *) 554(* Proof: 555 If part: SING s ==> s <> {} /\ (!x y. x IN s /\ y IN s ==> (x = y)) 556 True by SING_EMPTY, SING_ELEMENT. 557 Only-if part: s <> {} /\ (!x y. x IN s /\ y IN s ==> (x = y)) ==> SING s 558 True by SING_ONE_ELEMENT. 559*) 560val SING_TEST = store_thm( 561 "SING_TEST", 562 ``!s. SING s <=> s <> {} /\ (!x y. x IN s /\ y IN s ==> (x = y))``, 563 metis_tac[SING_EMPTY, SING_ELEMENT, SING_ONE_ELEMENT]); 564 565(* Theorem: x IN (if b then {y} else {}) ==> (x = y) *) 566(* Proof: by IN_SING, MEMBER_NOT_EMPTY *) 567val IN_SING_OR_EMPTY = store_thm( 568 "IN_SING_OR_EMPTY", 569 ``!b x y. x IN (if b then {y} else {}) ==> (x = y)``, 570 rw[]); 571 572(* Theorem: {x} INTER s = if x IN s then {x} else {} *) 573(* Proof: by EXTENSION *) 574val SING_INTER = store_thm( 575 "SING_INTER", 576 ``!s x. {x} INTER s = if x IN s then {x} else {}``, 577 rw[EXTENSION] >> 578 metis_tac[]); 579 580(* Theorem: SING s ==> (CARD s = 1) *) 581(* Proof: 582 Note s = {x} for some x by SING_DEF 583 so CARD s = 1 by CARD_SING 584*) 585Theorem SING_CARD_1: 586 !s. SING s ==> (CARD s = 1) 587Proof 588 metis_tac[SING_DEF, CARD_SING] 589QED 590 591(* Note: SING s <=> (CARD s = 1) cannot be proved. 592Only SING_IFF_CARD1 |- !s. SING s <=> (CARD s = 1) /\ FINITE s 593That is: FINITE s /\ (CARD s = 1) ==> SING s 594*) 595 596(* Theorem: FINITE s ==> ((CARD s = 1) <=> SING s) *) 597(* Proof: 598 If part: CARD s = 1 ==> SING s 599 Since CARD s = 1 600 ==> s <> {} by CARD_EMPTY 601 ==> ?x. x IN s by MEMBER_NOT_EMPTY 602 Claim: !y . y IN s ==> y = x 603 Proof: By contradiction, suppose y <> x. 604 Then y NOTIN {x} by EXTENSION 605 so CARD {y; x} = 2 by CARD_DEF 606 and {y; x} SUBSET s by SUBSET_DEF 607 thus CARD {y; x} <= CARD s by CARD_SUBSET 608 This contradicts CARD s = 1. 609 Hence SING s by SING_ONE_ELEMENT (or EXTENSION, SING_DEF) 610 Or, 611 With x IN s, {x} SUBSET s by SUBSET_DEF 612 If s <> {x}, then {x} PSUBSET s by PSUBSET_DEF 613 so CARD {x} < CARD s by CARD_PSUBSET 614 But CARD {x} = 1 by CARD_SING 615 and this contradicts CARD s = 1. 616 617 Only-if part: SING s ==> CARD s = 1 618 Since SING s 619 <=> ?x. s = {x} by SING_DEF 620 ==> CARD {x} = 1 by CARD_SING 621*) 622val CARD_EQ_1 = store_thm( 623 "CARD_EQ_1", 624 ``!s. FINITE s ==> ((CARD s = 1) <=> SING s)``, 625 rw[SING_DEF, EQ_IMP_THM] >| [ 626 `1 <> 0` by decide_tac >> 627 `s <> {} /\ ?x. x IN s` by metis_tac[CARD_EMPTY, MEMBER_NOT_EMPTY] >> 628 qexists_tac `x` >> 629 spose_not_then strip_assume_tac >> 630 `{x} PSUBSET s` by rw[PSUBSET_DEF] >> 631 `CARD {x} < CARD s` by rw[CARD_PSUBSET] >> 632 `CARD {x} = 1` by rw[CARD_SING] >> 633 decide_tac, 634 rw[CARD_SING] 635 ]); 636 637(* Theorem: x <> y ==> ((x INSERT s) DELETE y = x INSERT (s DELETE y)) *) 638(* Proof: 639 z IN (x INSERT s) DELETE y 640 <=> z IN (x INSERT s) /\ z <> y by IN_DELETE 641 <=> (z = x \/ z IN s) /\ z <> y by IN_INSERT 642 <=> (z = x /\ z <> y) \/ (z IN s /\ z <> y) by RIGHT_AND_OVER_OR 643 <=> (z = x) \/ (z IN s /\ z <> y) by x <> y 644 <=> (z = x) \/ (z IN DELETE y) by IN_DELETE 645 <=> z IN x INSERT (s DELETE y) by IN_INSERT 646*) 647val INSERT_DELETE_COMM = store_thm( 648 "INSERT_DELETE_COMM", 649 ``!s x y. x <> y ==> ((x INSERT s) DELETE y = x INSERT (s DELETE y))``, 650 (rw[EXTENSION] >> metis_tac[])); 651 652(* Theorem: s SUBSET u ==> (s INTER t) SUBSET u *) 653(* Proof: 654 Note (s INTER t) SUBSET s by INTER_SUBSET 655 ==> (s INTER t) SUBSET u by SUBSET_TRANS 656*) 657val SUBSET_INTER_SUBSET = store_thm( 658 "SUBSET_INTER_SUBSET", 659 ``!s t u. s SUBSET u ==> (s INTER t) SUBSET u``, 660 metis_tac[INTER_SUBSET, SUBSET_TRANS]); 661 662(* Theorem: s DIFF (s DIFF t) = s INTER t *) 663(* Proof: by IN_DIFF, IN_INTER *) 664val DIFF_DIFF_EQ_INTER = store_thm( 665 "DIFF_DIFF_EQ_INTER", 666 ``!s t. s DIFF (s DIFF t) = s INTER t``, 667 rw[EXTENSION] >> 668 metis_tac[]); 669 670(* Theorem: (s = t) <=> (s SUBSET t /\ (t DIFF s = {})) *) 671(* Proof: 672 s = t 673 <=> s SUBSET t /\ t SUBSET s by SET_EQ_SUBSET 674 <=> s SUBSET t /\ (t DIFF s = {}) by SUBSET_DIFF_EMPTY 675*) 676val SET_EQ_BY_DIFF = store_thm( 677 "SET_EQ_BY_DIFF", 678 ``!s t. (s = t) <=> (s SUBSET t /\ (t DIFF s = {}))``, 679 rw[SET_EQ_SUBSET, SUBSET_DIFF_EMPTY]); 680 681(* Theorem: s SUBSET t ==> !x. (x INSERT s) SUBSET (x INSERT t) *) 682(* Proof: by SUBSET_DEF *) 683val SUBSET_INSERT_SUBSET = store_thm( 684 "SUBSET_INSERT_SUBSET", 685 ``!s t. s SUBSET t ==> !x. (x INSERT s) SUBSET (x INSERT t)``, 686 rw[SUBSET_DEF]); 687 688(* Theorem: x NOTIN s /\ (x INSERT s) SUBSET t ==> s SUBSET (t DELETE x) *) 689(* Proof: by SUBSET_DEF *) 690val INSERT_SUBSET_SUBSET = store_thm( 691 "INSERT_SUBSET_SUBSET", 692 ``!s t x. x NOTIN s /\ (x INSERT s) SUBSET t ==> s SUBSET (t DELETE x)``, 693 rw[SUBSET_DEF]); 694 695(* DIFF_INSERT |- !s t x. s DIFF (x INSERT t) = s DELETE x DIFF t *) 696 697(* Theorem: (s DIFF t) DELETE x = s DIFF (x INSERT t) *) 698(* Proof: by EXTENSION *) 699val DIFF_DELETE = store_thm( 700 "DIFF_DELETE", 701 ``!s t x. (s DIFF t) DELETE x = s DIFF (x INSERT t)``, 702 (rw[EXTENSION] >> metis_tac[])); 703 704(* Theorem: FINITE a /\ b SUBSET a ==> (CARD (a DIFF b) = CARD a - CARD b) *) 705(* Proof: 706 Note FINITE b by SUBSET_FINITE 707 so a INTER b = b by SUBSET_INTER2 708 CARD (a DIFF b) 709 = CARD a - CARD (a INTER b) by CARD_DIFF 710 = CARD a - CARD b by above 711*) 712Theorem SUBSET_DIFF_CARD: 713 !a b. FINITE a /\ b SUBSET a ==> (CARD (a DIFF b) = CARD a - CARD b) 714Proof 715 metis_tac[CARD_DIFF, SUBSET_FINITE, SUBSET_INTER2] 716QED 717 718(* Theorem: s SUBSET {x} <=> ((s = {}) \/ (s = {x})) *) 719(* Proof: 720 Note !y. y IN s ==> y = x by SUBSET_DEF, IN_SING 721 If s = {}, then trivially true. 722 If s <> {}, 723 then ?y. y IN s by MEMBER_NOT_EMPTY, s <> {} 724 so y = x by above 725 ==> s = {x} by EXTENSION 726*) 727Theorem SUBSET_SING_IFF: 728 !s x. s SUBSET {x} <=> ((s = {}) \/ (s = {x})) 729Proof 730 rw[SUBSET_DEF, EXTENSION] >> 731 metis_tac[] 732QED 733 734(* ------------------------------------------------------------------------- *) 735(* Image and Bijection *) 736(* ------------------------------------------------------------------------- *) 737 738(* Theorem: (!x. x IN s ==> (f x = g x)) ==> (INJ f s t <=> INJ g s t) *) 739(* Proof: by INJ_DEF *) 740val INJ_CONG = store_thm( 741 "INJ_CONG", 742 ``!f g s t. (!x. x IN s ==> (f x = g x)) ==> (INJ f s t <=> INJ g s t)``, 743 rw[INJ_DEF]); 744 745(* Theorem: (!x. x IN s ==> (f x = g x)) ==> (SURJ f s t <=> SURJ g s t) *) 746(* Proof: by SURJ_DEF *) 747val SURJ_CONG = store_thm( 748 "SURJ_CONG", 749 ``!f g s t. (!x. x IN s ==> (f x = g x)) ==> (SURJ f s t <=> SURJ g s t)``, 750 rw[SURJ_DEF] >> 751 metis_tac[]); 752 753(* Theorem: (!x. x IN s ==> (f x = g x)) ==> (BIJ f s t <=> BIJ g s t) *) 754(* Proof: by BIJ_DEF, INJ_CONG, SURJ_CONG *) 755val BIJ_CONG = store_thm( 756 "BIJ_CONG", 757 ``!f g s t. (!x. x IN s ==> (f x = g x)) ==> (BIJ f s t <=> BIJ g s t)``, 758 rw[BIJ_DEF] >> 759 metis_tac[INJ_CONG, SURJ_CONG]); 760 761(* 762BIJ_LINV_BIJ |- !f s t. BIJ f s t ==> BIJ (LINV f s) t s 763Cannot prove |- !f s t. BIJ f s t <=> BIJ (LINV f s) t s 764because LINV f s depends on f! 765*) 766 767(* Theorem: INJ f s t /\ x IN s ==> f x IN t *) 768(* Proof: by INJ_DEF *) 769val INJ_ELEMENT = store_thm( 770 "INJ_ELEMENT", 771 ``!f s t x. INJ f s t /\ x IN s ==> f x IN t``, 772 rw_tac std_ss[INJ_DEF]); 773 774(* Theorem: SURJ f s t /\ x IN s ==> f x IN t *) 775(* Proof: by SURJ_DEF *) 776val SURJ_ELEMENT = store_thm( 777 "SURJ_ELEMENT", 778 ``!f s t x. SURJ f s t /\ x IN s ==> f x IN t``, 779 rw_tac std_ss[SURJ_DEF]); 780 781(* Theorem: BIJ f s t /\ x IN s ==> f x IN t *) 782(* Proof: by BIJ_DEF *) 783val BIJ_ELEMENT = store_thm( 784 "BIJ_ELEMENT", 785 ``!f s t x. BIJ f s t /\ x IN s ==> f x IN t``, 786 rw_tac std_ss[BIJ_DEF, INJ_DEF]); 787 788(* Theorem: INJ f s t ==> INJ f s UNIV *) 789(* Proof: 790 Note s SUBSET s by SUBSET_REFL 791 and t SUBSET univ(:'b) by SUBSET_UNIV 792 so INJ f s t ==> INJ f s univ(:'b) by INJ_SUBSET 793*) 794val INJ_UNIV = store_thm( 795 "INJ_UNIV", 796 ``!f s t. INJ f s t ==> INJ f s UNIV``, 797 metis_tac[INJ_SUBSET, SUBSET_REFL, SUBSET_UNIV]); 798 799(* Theorem: INJ f UNIV UNIV ==> INJ f s UNIV *) 800(* Proof: 801 Note s SUBSET univ(:'a) by SUBSET_UNIV 802 and univ(:'b) SUBSET univ('b) by SUBSET_REFL 803 so INJ f univ(:'a) univ(:'b) ==> INJ f s univ(:'b) by INJ_SUBSET 804*) 805val INJ_SUBSET_UNIV = store_thm( 806 "INJ_SUBSET_UNIV", 807 ``!(f:'a -> 'b) (s:'a -> bool). INJ f UNIV UNIV ==> INJ f s UNIV``, 808 metis_tac[INJ_SUBSET, SUBSET_UNIV, SUBSET_REFL]); 809 810(* Theorem: INJ f s UNIV ==> BIJ f s (IMAGE f s) *) 811(* Proof: by definitions. *) 812val INJ_IMAGE_BIJ = store_thm( 813 "INJ_IMAGE_BIJ", 814 ``!f s. INJ f s UNIV ==> BIJ f s (IMAGE f s)``, 815 rw[BIJ_DEF, INJ_DEF, SURJ_DEF]); 816 817(* Theorem: INJ f P univ(:'b) ==> 818 !s t. s SUBSET P /\ t SUBSET P ==> ((IMAGE f s = IMAGE f t) <=> (s = t)) *) 819(* Proof: 820 If part: IMAGE f s = IMAGE f t ==> s = t 821 Claim: s SUBSET t 822 Proof: by SUBSET_DEF, this is to show: x IN s ==> x IN t 823 x IN s 824 ==> f x IN (IMAGE f s) by INJ_DEF, IN_IMAGE 825 or f x IN (IMAGE f t) by given 826 ==> ?x'. x' IN t /\ (f x' = f x) by IN_IMAGE 827 But x IN P /\ x' IN P by SUBSET_DEF 828 Thus f x' = f x ==> x' = x by INJ_DEF 829 830 Claim: t SUBSET s 831 Proof: similar to above by INJ_DEF, IN_IMAGE, SUBSET_DEF 832 833 Hence s = t by SUBSET_ANTISYM 834 835 Only-if part: s = t ==> IMAGE f s = IMAGE f t 836 This is trivially true. 837*) 838val INJ_IMAGE_EQ = store_thm( 839 "INJ_IMAGE_EQ", 840 ``!P f. INJ f P univ(:'b) ==> 841 !s t. s SUBSET P /\ t SUBSET P ==> ((IMAGE f s = IMAGE f t) <=> (s = t))``, 842 rw[EQ_IMP_THM] >> 843 (irule SUBSET_ANTISYM >> rpt conj_tac) >| [ 844 rw[SUBSET_DEF] >> 845 `?x'. x' IN t /\ (f x' = f x)` by metis_tac[IMAGE_IN, IN_IMAGE] >> 846 metis_tac[INJ_DEF, SUBSET_DEF], 847 rw[SUBSET_DEF] >> 848 `?x'. x' IN s /\ (f x' = f x)` by metis_tac[IMAGE_IN, IN_IMAGE] >> 849 metis_tac[INJ_DEF, SUBSET_DEF] 850 ]); 851 852(* Note: pred_setTheory.IMAGE_INTER 853|- !f s t. IMAGE f (s INTER t) SUBSET IMAGE f s INTER IMAGE f t 854*) 855 856(* Theorem: INJ f P univ(:'b) ==> 857 !s t. s SUBSET P /\ t SUBSET P ==> (IMAGE f (s INTER t) = (IMAGE f s) INTER (IMAGE f t)) *) 858(* Proof: by EXTENSION, INJ_DEF, SUBSET_DEF *) 859val INJ_IMAGE_INTER = store_thm( 860 "INJ_IMAGE_INTER", 861 ``!P f. INJ f P univ(:'b) ==> 862 !s t. s SUBSET P /\ t SUBSET P ==> (IMAGE f (s INTER t) = (IMAGE f s) INTER (IMAGE f t))``, 863 rw[EXTENSION] >> 864 metis_tac[INJ_DEF, SUBSET_DEF]); 865 866(* tobe: helperSet, change P to P *) 867 868(* Theorem: INJ f P univ(:'b) ==> 869 !s t. s SUBSET P /\ t SUBSET P ==> (DISJOINT s t <=> DISJOINT (IMAGE f s) (IMAGE f t)) *) 870(* Proof: 871 DISJOINT (IMAGE f s) (IMAGE f t) 872 <=> (IMAGE f s) INTER (IMAGE f t) = {} by DISJOINT_DEF 873 <=> IMAGE f (s INTER t) = {} by INJ_IMAGE_INTER, INJ f P univ(:'b) 874 <=> s INTER t = {} by IMAGE_EQ_EMPTY 875 <=> DISJOINT s t by DISJOINT_DEF 876*) 877val INJ_IMAGE_DISJOINT = store_thm( 878 "INJ_IMAGE_DISJOINT", 879 ``!P f. INJ f P univ(:'b) ==> 880 !s t. s SUBSET P /\ t SUBSET P ==> (DISJOINT s t <=> DISJOINT (IMAGE f s) (IMAGE f t))``, 881 metis_tac[DISJOINT_DEF, INJ_IMAGE_INTER, IMAGE_EQ_EMPTY]); 882 883(* Theorem: INJ I s univ(:'a) *) 884(* Proof: 885 Note !x. I x = x by I_THM 886 so !x. x IN s ==> I x IN univ(:'a) by IN_UNIV 887 and !x y. x IN s /\ y IN s ==> (I x = I y) ==> (x = y) by above 888 Hence INJ I s univ(:'b) by INJ_DEF 889*) 890val INJ_I = store_thm( 891 "INJ_I", 892 ``!s:'a -> bool. INJ I s univ(:'a)``, 893 rw[INJ_DEF]); 894 895(* Theorem: INJ I (IMAGE f s) univ(:'b) *) 896(* Proof: 897 Since !x. x IN (IMAGE f s) ==> x IN univ(:'b) by IN_UNIV 898 and !x y. x IN (IMAGE f s) /\ y IN (IMAGE f s) ==> 899 (I x = I y) ==> (x = y) by I_THM 900 Hence INJ I (IMAGE f s) univ(:'b) by INJ_DEF 901*) 902val INJ_I_IMAGE = store_thm( 903 "INJ_I_IMAGE", 904 ``!s f. INJ I (IMAGE f s) univ(:'b)``, 905 rw[INJ_DEF]); 906 907(* Theorem: BIJ f s t <=> (!x. x IN s ==> f x IN t) /\ (!y. y IN t ==> ?!x. x IN s /\ (f x = y)) *) 908(* Proof: 909 This is to prove: 910 (1) y IN t ==> ?!x. x IN s /\ (f x = y) 911 x exists by SURJ_DEF, and x is unique by INJ_DEF. 912 (2) x IN s /\ y IN s /\ f x = f y ==> x = y 913 true by INJ_DEF. 914 (3) x IN t ==> ?y. y IN s /\ (f y = x) 915 true by SURJ_DEF. 916*) 917val BIJ_ALT = store_thm( 918 "BIJ_ALT", 919 ``!f s t. BIJ f s t <=> (!x. x IN s ==> f x IN t) /\ (!y. y IN t ==> ?!x. x IN s /\ (f x = y))``, 920 rw_tac std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, EQ_IMP_THM] >> metis_tac[]); 921 922(* Theorem: BIJ f s t ==> !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y) *) 923(* Proof: by BIJ_DEF, INJ_DEF *) 924Theorem BIJ_IS_INJ: 925 !f s t. BIJ f s t ==> !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y) 926Proof 927 rw[BIJ_DEF, INJ_DEF] 928QED 929 930(* Theorem: INJ f s s /\ x IN s /\ y IN s ==> ((f x = f y) <=> (x = y)) *) 931(* Proof: by INJ_DEF *) 932Theorem INJ_EQ_11: 933 !f s x y. INJ f s s /\ x IN s /\ y IN s ==> ((f x = f y) <=> (x = y)) 934Proof 935 metis_tac[INJ_DEF] 936QED 937 938(* Theorem: BIJ I s s *) 939(* Proof: by definitions. *) 940val BIJ_I_SAME = store_thm( 941 "BIJ_I_SAME", 942 ``!s. BIJ I s s``, 943 rw[BIJ_DEF, INJ_DEF, SURJ_DEF]); 944 945(* Theorem: IMAGE I s = s *) 946(* Proof: 947 IMAGE I s 948 = {f x | x IN s} by IMAGE_DEF 949 = { x | x IN s} by I_THM 950 = s by EXTENSION 951*) 952val IMAGE_I = store_thm( 953 "IMAGE_I", 954 ``!s. IMAGE I s = s``, 955 rw[IMAGE_DEF]); 956 957(* export simple result *) 958val _ = export_rewrites ["IMAGE_I"]; 959 960(* Theorem: s <> {} ==> !e. IMAGE (K e) s = {e} *) 961(* Proof: 962 IMAGE (K e) s 963 <=> {(K e) x | x IN s} by IMAGE_DEF 964 <=> {e | x IN s} by K_THM 965 <=> {e} by EXTENSION, if s <> {} 966*) 967val IMAGE_K = store_thm( 968 "IMAGE_K", 969 ``!s. s <> {} ==> !e. IMAGE (K e) s = {e}``, 970 rw[EXTENSION, EQ_IMP_THM]); 971 972(* Theorem: IMAGE f {x} = {f x} *) 973(* Proof: by IN_IMAGE, IN_SING *) 974val IMAGE_SING = store_thm( 975 "IMAGE_SING", 976 ``!f x. IMAGE f {x} = {f x}``, 977 rw[]); 978 979(* Theorem: (!x. x IN s ==> f x IN t) <=> (IMAGE f s) SUBSET t *) 980(* Proof: 981 If part: (!x. x IN s ==> f x IN t) ==> (IMAGE f s) SUBSET t 982 y IN (IMAGE f s) 983 ==> ?x. (y = f x) /\ x IN s by IN_IMAGE 984 ==> f x = y IN t by given 985 hence (IMAGE f s) SUBSET t by SUBSET_DEF 986 Only-if part: (IMAGE f s) SUBSET t ==> (!x. x IN s ==> f x IN t) 987 x IN s 988 ==> f x IN (IMAGE f s) by IN_IMAGE 989 ==> f x IN t by SUBSET_DEF 990*) 991val IMAGE_SUBSET_TARGET = store_thm( 992 "IMAGE_SUBSET_TARGET", 993 ``!f s t. (!x. x IN s ==> f x IN t) <=> (IMAGE f s) SUBSET t``, 994 metis_tac[IN_IMAGE, SUBSET_DEF]); 995 996(* Theorem: (!x y. (f x = f y) ==> (x = y)) ==> (!s e. e IN s <=> f e IN IMAGE f s) *) 997(* Proof: 998 If part: e IN s ==> f e IN IMAGE f s 999 True by IMAGE_IN. 1000 Only-if part: f e IN IMAGE f s ==> e IN s 1001 ?x. (f e = f x) /\ x IN s by IN_IMAGE 1002 f e = f x ==> e = x by given implication 1003 Hence x IN s 1004*) 1005val IMAGE_ELEMENT_CONDITION = store_thm( 1006 "IMAGE_ELEMENT_CONDITION", 1007 ``!f:'a -> 'b. (!x y. (f x = f y) ==> (x = y)) ==> (!s e. e IN s <=> f e IN IMAGE f s)``, 1008 rw[EQ_IMP_THM] >> 1009 metis_tac[]); 1010 1011(* Theorem: BIGUNION (IMAGE (\x. {x}) s) = s *) 1012(* Proof: 1013 z IN BIGUNION (IMAGE (\x. {x}) s) 1014 <=> ?t. z IN t /\ t IN (IMAGE (\x. {x}) s) by IN_BIGUNION 1015 <=> ?t. z IN t /\ (?y. y IN s /\ (t = {y})) by IN_IMAGE 1016 <=> z IN {z} /\ (?y. y IN s /\ {z} = {y}) by picking t = {z} 1017 <=> T /\ z IN s by picking y = z, IN_SING 1018 Hence BIGUNION (IMAGE (\x. {x}) s) = s by EXTENSION 1019*) 1020val BIGUNION_ELEMENTS_SING = store_thm( 1021 "BIGUNION_ELEMENTS_SING", 1022 ``!s. BIGUNION (IMAGE (\x. {x}) s) = s``, 1023 rw[EXTENSION, EQ_IMP_THM] >- 1024 metis_tac[] >> 1025 qexists_tac `{x}` >> 1026 metis_tac[IN_SING]); 1027 1028(* Theorem: s SUBSET t /\ INJ f t UNIV ==> (IMAGE f (t DIFF s) = (IMAGE f t) DIFF (IMAGE f s)) *) 1029(* Proof: by SUBSET_DEF, INJ_DEF, EXTENSION, IN_IMAGE, IN_DIFF *) 1030val IMAGE_INJ_SUBSET_DIFF = store_thm( 1031 "IMAGE_INJ_SUBSET_DIFF", 1032 ``!s t f. s SUBSET t /\ INJ f t UNIV ==> (IMAGE f (t DIFF s) = (IMAGE f t) DIFF (IMAGE f s))``, 1033 rw[SUBSET_DEF, INJ_DEF, EXTENSION] >> 1034 metis_tac[]); 1035 1036(* ------------------------------------------------------------------------- *) 1037(* More Theorems and Sets for Counting *) 1038(* ------------------------------------------------------------------------- *) 1039 1040(* Have simple (count n) *) 1041 1042(* Theorem: count 1 = {0} *) 1043(* Proof: rename COUNT_ZERO *) 1044val COUNT_0 = save_thm("COUNT_0", COUNT_ZERO); 1045(* val COUNT_0 = |- count 0 = {}: thm *) 1046 1047(* Theorem: count 1 = {0} *) 1048(* Proof: by count_def, EXTENSION *) 1049val COUNT_1 = store_thm( 1050 "COUNT_1", 1051 ``count 1 = {0}``, 1052 rw[count_def, EXTENSION]); 1053 1054(* Theorem: n NOTIN (count n) *) 1055(* Proof: by IN_COUNT *) 1056val COUNT_NOT_SELF = store_thm( 1057 "COUNT_NOT_SELF", 1058 ``!n. n NOTIN (count n)``, 1059 rw[]); 1060 1061(* Theorem: (count n = {}) <=> (n = 0) *) 1062(* Proof: 1063 Since FINITE (count n) by FINITE_COUNT 1064 and CARD (count n) = n by CARD_COUNT 1065 so count n = {} <=> n = 0 by CARD_EQ_0 1066*) 1067val COUNT_EQ_EMPTY = store_thm( 1068 "COUNT_EQ_EMPTY", 1069 ``!n. (count n = {}) <=> (n = 0)``, 1070 metis_tac[FINITE_COUNT, CARD_COUNT, CARD_EQ_0]); 1071 1072(* Theorem: m <= n ==> count m SUBSET count n *) 1073(* Proof: by LENGTH_TAKE_EQ *) 1074val COUNT_SUBSET = store_thm( 1075 "COUNT_SUBSET", 1076 ``!m n. m <= n ==> count m SUBSET count n``, 1077 rw[SUBSET_DEF]); 1078 1079(* Theorem: count (SUC n) SUBSET t <=> count n SUBSET t /\ n IN t *) 1080(* Proof: 1081 count (SUC n) SUBSET t 1082 <=> (n INSERT count n) SUBSET t by COUNT_SUC 1083 <=> n IN t /\ (count n) SUBSET t by INSERT_SUBSET 1084 <=> (count n) SUBSET t /\ n IN t by CONJ_COMM 1085*) 1086val COUNT_SUC_SUBSET = store_thm( 1087 "COUNT_SUC_SUBSET", 1088 ``!n t. count (SUC n) SUBSET t <=> count n SUBSET t /\ n IN t``, 1089 metis_tac[COUNT_SUC, INSERT_SUBSET]); 1090 1091(* Theorem: t DIFF (count (SUC n)) = t DIFF (count n) DELETE n *) 1092(* Proof: 1093 t DIFF (count (SUC n)) 1094 = t DIFF (n INSERT count n) by COUNT_SUC 1095 = t DIFF (count n) DELETE n by EXTENSION 1096*) 1097val DIFF_COUNT_SUC = store_thm( 1098 "DIFF_COUNT_SUC", 1099 ``!n t. t DIFF (count (SUC n)) = t DIFF (count n) DELETE n``, 1100 rw[EXTENSION, EQ_IMP_THM]); 1101 1102(* COUNT_SUC |- !n. count (SUC n) = n INSERT count n *) 1103 1104(* Theorem: count (SUC n) = 0 INSERT (IMAGE SUC (count n)) *) 1105(* Proof: by EXTENSION *) 1106val COUNT_SUC_BY_SUC = store_thm( 1107 "COUNT_SUC_BY_SUC", 1108 ``!n. count (SUC n) = 0 INSERT (IMAGE SUC (count n))``, 1109 rw[EXTENSION, EQ_IMP_THM] >> 1110 (Cases_on `x` >> simp[])); 1111 1112(* Theorem: IMAGE f (count (SUC n)) = (f n) INSERT IMAGE f (count n) *) 1113(* Proof: 1114 IMAGE f (count (SUC n)) 1115 = IMAGE f (n INSERT (count n)) by COUNT_SUC 1116 = f n INSERT IMAGE f (count n) by IMAGE_INSERT 1117*) 1118val IMAGE_COUNT_SUC = store_thm( 1119 "IMAGE_COUNT_SUC", 1120 ``!f n. IMAGE f (count (SUC n)) = (f n) INSERT IMAGE f (count n)``, 1121 rw[COUNT_SUC]); 1122 1123(* Theorem: IMAGE f (count (SUC n)) = (f 0) INSERT IMAGE (f o SUC) (count n) *) 1124(* Proof: 1125 IMAGE f (count (SUC n)) 1126 = IMAGE f (0 INSERT (IMAGE SUC (count n))) by COUNT_SUC_BY_SUC 1127 = f 0 INSERT IMAGE f (IMAGE SUC (count n)) by IMAGE_INSERT 1128 = f 0 INSERT IMAGE (f o SUC) (count n) by IMAGE_COMPOSE 1129*) 1130val IMAGE_COUNT_SUC_BY_SUC = store_thm( 1131 "IMAGE_COUNT_SUC_BY_SUC", 1132 ``!f n. IMAGE f (count (SUC n)) = (f 0) INSERT IMAGE (f o SUC) (count n)``, 1133 rw[COUNT_SUC_BY_SUC, IMAGE_COMPOSE]); 1134 1135(* Introduce countFrom m n, the set {m, m + 1, m + 2, ...., m + n - 1} *) 1136val _ = overload_on("countFrom", ``\m n. IMAGE ($+ m) (count n)``); 1137 1138(* Theorem: countFrom m 0 = {} *) 1139(* Proof: 1140 countFrom m 0 1141 = IMAGE ($+ m) (count 0) by notation 1142 = IMAGE ($+ m) {} by COUNT_0 1143 = {} by IMAGE_EMPTY 1144*) 1145val countFrom_0 = store_thm( 1146 "countFrom_0", 1147 ``!m. countFrom m 0 = {}``, 1148 rw[]); 1149 1150(* Theorem: countFrom m (SUC n) = m INSERT countFrom (m + 1) n *) 1151(* Proof: by IMAGE_COUNT_SUC_BY_SUC *) 1152val countFrom_SUC = store_thm( 1153 "countFrom_SUC", 1154 ``!m n. !m n. countFrom m (SUC n) = m INSERT countFrom (m + 1) n``, 1155 rpt strip_tac >> 1156 `$+ m o SUC = $+ (m + 1)` by rw[FUN_EQ_THM] >> 1157 rw[IMAGE_COUNT_SUC_BY_SUC]); 1158 1159(* Theorem: 0 < n ==> m IN countFrom m n *) 1160(* Proof: by IN_COUNT *) 1161val countFrom_first = store_thm( 1162 "countFrom_first", 1163 ``!m n. 0 < n ==> m IN countFrom m n``, 1164 rw[] >> 1165 metis_tac[ADD_0]); 1166 1167(* Theorem: x < m ==> x NOTIN countFrom m n *) 1168(* Proof: by IN_COUNT *) 1169val countFrom_less = store_thm( 1170 "countFrom_less", 1171 ``!m n x. x < m ==> x NOTIN countFrom m n``, 1172 rw[]); 1173 1174(* Theorem: count n = countFrom 0 n *) 1175(* Proof: by EXTENSION *) 1176val count_by_countFrom = store_thm( 1177 "count_by_countFrom", 1178 ``!n. count n = countFrom 0 n``, 1179 rw[EXTENSION]); 1180 1181(* Theorem: count (SUC n) = 0 INSERT countFrom 1 n *) 1182(* Proof: 1183 count (SUC n) 1184 = 0 INSERT IMAGE SUC (count n) by COUNT_SUC_BY_SUC 1185 = 0 INSERT IMAGE ($+ 1) (count n) by FUN_EQ_THM 1186 = 0 INSERT countFrom 1 n by notation 1187*) 1188val count_SUC_by_countFrom = store_thm( 1189 "count_SUC_by_countFrom", 1190 ``!n. count (SUC n) = 0 INSERT countFrom 1 n``, 1191 rpt strip_tac >> 1192 `SUC = $+ 1` by rw[FUN_EQ_THM] >> 1193 rw[COUNT_SUC_BY_SUC]); 1194 1195(* Inclusion-Exclusion for two sets: 1196 1197CARD_UNION 1198|- !s. FINITE s ==> !t. FINITE t ==> 1199 (CARD (s UNION t) + CARD (s INTER t) = CARD s + CARD t) 1200CARD_UNION_EQN 1201|- !s t. FINITE s /\ FINITE t ==> 1202 (CARD (s UNION t) = CARD s + CARD t - CARD (s INTER t)) 1203CARD_UNION_DISJOINT 1204|- !s t. FINITE s /\ FINITE t /\ DISJOINT s t ==> 1205 (CARD (s UNION t) = CARD s + CARD t) 1206*) 1207 1208(* Inclusion-Exclusion for three sets. *) 1209 1210(* Theorem: FINITE a /\ FINITE b /\ FINITE c ==> 1211 (CARD (a UNION b UNION c) = 1212 CARD a + CARD b + CARD c + CARD (a INTER b INTER c) - 1213 CARD (a INTER b) - CARD (b INTER c) - CARD (a INTER c)) *) 1214(* Proof: 1215 Note FINITE (a UNION b) by FINITE_UNION 1216 and FINITE (a INTER c) by FINITE_INTER 1217 and FINITE (b INTER c) by FINITE_INTER 1218 Also (a INTER c) INTER (b INTER c) 1219 = a INTER b INTER c by EXTENSION 1220 and CARD (a INTER b) <= CARD a by CARD_INTER_LESS_EQ 1221 and CARD (a INTER b INTER c) <= CARD (b INTER c) by CARD_INTER_LESS_EQ, INTER_COMM 1222 1223 CARD (a UNION b UNION c) 1224 = CARD (a UNION b) + CARD c - CARD ((a UNION b) INTER c) 1225 by CARD_UNION_EQN 1226 = (CARD a + CARD b - CARD (a INTER b)) + 1227 CARD c - CARD ((a UNION b) INTER c) by CARD_UNION_EQN 1228 = (CARD a + CARD b - CARD (a INTER b)) + 1229 CARD c - CARD ((a INTER c) UNION (b INTER c)) 1230 by UNION_OVER_INTER 1231 = (CARD a + CARD b - CARD (a INTER b)) + CARD c - 1232 (CARD (a INTER c) + CARD (b INTER c) - CARD ((a INTER c) INTER (b INTER c))) 1233 by CARD_UNION_EQN 1234 = CARD a + CARD b + CARD c - CARD (a INTER b) - 1235 (CARD (a INTER c) + CARD (b INTER c) - CARD (a INTER b INTER c)) 1236 by CARD (a INTER b) <= CARD a 1237 = CARD a + CARD b + CARD c - CARD (a INTER b) - 1238 (CARD (b INTER c) + CARD (a INTER c) - CARD (a INTER b INTER c)) 1239 by ADD_COMM 1240 = CARD a + CARD b + CARD c - CARD (a INTER b) 1241 + CARD (a INTER b INTER c) - CARD (b INTER c) - CARD (a INTER c) 1242 by CARD (a INTER b INTER c) <= CARD (b INTER c) 1243 = CARD a + CARD b + CARD c + CARD (a INTER b INTER c) 1244 - CARD (a INTER b) - CARD (b INTER c) - CARD (a INTER c) 1245 by arithmetic 1246*) 1247Theorem CARD_UNION_3_EQN: 1248 !a b c. FINITE a /\ FINITE b /\ FINITE c ==> 1249 (CARD (a UNION b UNION c) = 1250 CARD a + CARD b + CARD c + CARD (a INTER b INTER c) - 1251 CARD (a INTER b) - CARD (b INTER c) - CARD (a INTER c)) 1252Proof 1253 rpt strip_tac >> 1254 `FINITE (a UNION b) /\ FINITE (a INTER c) /\ FINITE (b INTER c)` by rw[] >> 1255 (`(a INTER c) INTER (b INTER c) = a INTER b INTER c` by (rw[EXTENSION] >> metis_tac[])) >> 1256 `CARD (a INTER b) <= CARD a` by rw[CARD_INTER_LESS_EQ] >> 1257 `CARD (a INTER b INTER c) <= CARD (b INTER c)` by metis_tac[INTER_COMM, CARD_INTER_LESS_EQ] >> 1258 `CARD (a UNION b UNION c) 1259 = CARD (a UNION b) + CARD c - CARD ((a UNION b) INTER c)` by rw[CARD_UNION_EQN] >> 1260 `_ = (CARD a + CARD b - CARD (a INTER b)) + 1261 CARD c - CARD ((a UNION b) INTER c)` by rw[CARD_UNION_EQN] >> 1262 `_ = (CARD a + CARD b - CARD (a INTER b)) + 1263 CARD c - CARD ((a INTER c) UNION (b INTER c))` by fs[UNION_OVER_INTER, INTER_COMM] >> 1264 `_ = (CARD a + CARD b - CARD (a INTER b)) + CARD c - 1265 (CARD (a INTER c) + CARD (b INTER c) - CARD (a INTER b INTER c))` by metis_tac[CARD_UNION_EQN] >> 1266 decide_tac 1267QED 1268 1269(* Simplification of the above result for 3 disjoint sets. *) 1270 1271(* Theorem: FINITE a /\ FINITE b /\ FINITE c /\ 1272 DISJOINT a b /\ DISJOINT b c /\ DISJOINT a c ==> 1273 (CARD (a UNION b UNION c) = CARD a + CARD b + CARD c) *) 1274(* Proof: by DISJOINT_DEF, CARD_UNION_3_EQN *) 1275Theorem CARD_UNION_3_DISJOINT: 1276 !a b c. FINITE a /\ FINITE b /\ FINITE c /\ 1277 DISJOINT a b /\ DISJOINT b c /\ DISJOINT a c ==> 1278 (CARD (a UNION b UNION c) = CARD a + CARD b + CARD c) 1279Proof 1280 rw[DISJOINT_DEF] >> 1281 rw[CARD_UNION_3_EQN] 1282QED 1283 1284(* ------------------------------------------------------------------------- *) 1285(* Maximum and Minimum of a Set *) 1286(* ------------------------------------------------------------------------- *) 1287 1288(* Theorem: FINITE s /\ MAX_SET s < n ==> !x. x IN s ==> x < n *) 1289(* Proof: 1290 Since x IN s, s <> {} by MEMBER_NOT_EMPTY 1291 Hence x <= MAX_SET s by MAX_SET_DEF 1292 Thus x < n by LESS_EQ_LESS_TRANS 1293*) 1294val MAX_SET_LESS = store_thm( 1295 "MAX_SET_LESS", 1296 ``!s n. FINITE s /\ MAX_SET s < n ==> !x. x IN s ==> x < n``, 1297 metis_tac[MEMBER_NOT_EMPTY, MAX_SET_DEF, LESS_EQ_LESS_TRANS]); 1298 1299(* Theorem: FINITE s /\ s <> {} ==> !x. x IN s /\ (!y. y IN s ==> y <= x) ==> (x = MAX_SET s) *) 1300(* Proof: 1301 Let m = MAX_SET s. 1302 Since m IN s /\ x <= m by MAX_SET_DEF 1303 and m IN s ==> m <= x by implication 1304 Hence x = m. 1305*) 1306val MAX_SET_TEST = store_thm( 1307 "MAX_SET_TEST", 1308 ``!s. FINITE s /\ s <> {} ==> !x. x IN s /\ (!y. y IN s ==> y <= x) ==> (x = MAX_SET s)``, 1309 rpt strip_tac >> 1310 qabbrev_tac `m = MAX_SET s` >> 1311 `m IN s /\ x <= m` by rw[MAX_SET_DEF, Abbr`m`] >> 1312 `m <= x` by rw[] >> 1313 decide_tac); 1314 1315(* Theorem: s <> {} ==> !x. x IN s /\ (!y. y IN s ==> x <= y) ==> (x = MIN_SET s) *) 1316(* Proof: 1317 Let m = MIN_SET s. 1318 Since m IN s /\ m <= x by MIN_SET_LEM 1319 and m IN s ==> x <= m by implication 1320 Hence x = m. 1321*) 1322val MIN_SET_TEST = store_thm( 1323 "MIN_SET_TEST", 1324 ``!s. s <> {} ==> !x. x IN s /\ (!y. y IN s ==> x <= y) ==> (x = MIN_SET s)``, 1325 rpt strip_tac >> 1326 qabbrev_tac `m = MIN_SET s` >> 1327 `m IN s /\ m <= x` by rw[MIN_SET_LEM, Abbr`m`] >> 1328 `x <= m` by rw[] >> 1329 decide_tac); 1330 1331(* Theorem: FINITE s /\ s <> {} ==> !x. x IN s ==> ((MAX_SET s = x) <=> (!y. y IN s ==> y <= x)) *) 1332(* Proof: 1333 Let m = MAX_SET s. 1334 If part: y IN s ==> y <= m, true by MAX_SET_DEF 1335 Only-if part: !y. y IN s ==> y <= x ==> m = x 1336 Note m IN s /\ x <= m by MAX_SET_DEF 1337 and m IN s ==> m <= x by implication 1338 Hence x = m. 1339*) 1340Theorem MAX_SET_TEST_IFF: 1341 !s. FINITE s /\ s <> {} ==> 1342 !x. x IN s ==> ((MAX_SET s = x) <=> (!y. y IN s ==> y <= x)) 1343Proof 1344 rpt strip_tac >> 1345 qabbrev_tac `m = MAX_SET s` >> 1346 rw[EQ_IMP_THM] >- rw[MAX_SET_DEF, Abbr���m���] >> 1347 `m IN s /\ x <= m` by rw[MAX_SET_DEF, Abbr`m`] >> 1348 `m <= x` by rw[] >> 1349 decide_tac 1350QED 1351 1352(* Theorem: s <> {} ==> !x. x IN s ==> ((MIN_SET s = x) <=> (!y. y IN s ==> x <= y)) *) 1353(* Proof: 1354 Let m = MIN_SET s. 1355 If part: y IN s ==> m <= y, true by MIN_SET_LEM 1356 Only-if part: !y. y IN s ==> x <= y ==> m = x 1357 Note m IN s /\ m <= x by MIN_SET_LEM 1358 and m IN s ==> x <= m by implication 1359 Hence x = m. 1360*) 1361Theorem MIN_SET_TEST_IFF: 1362 !s. s <> {} ==> !x. x IN s ==> ((MIN_SET s = x) <=> (!y. y IN s ==> x <= y)) 1363Proof 1364 rpt strip_tac >> 1365 qabbrev_tac `m = MIN_SET s` >> 1366 rw[EQ_IMP_THM] >- rw[MIN_SET_LEM, Abbr���m���] >> 1367 `m IN s /\ m <= x` by rw[MIN_SET_LEM, Abbr`m`] >> 1368 `x <= m` by rw[] >> decide_tac 1369QED 1370 1371(* Theorem: MAX_SET {} = 0 *) 1372(* Proof: by MAX_SET_REWRITES *) 1373val MAX_SET_EMPTY = save_thm("MAX_SET_EMPTY", MAX_SET_REWRITES |> CONJUNCT1); 1374(* val MAX_SET_EMPTY = |- MAX_SET {} = 0: thm *) 1375 1376(* Theorem: MAX_SET {e} = e *) 1377(* Proof: by MAX_SET_REWRITES *) 1378val MAX_SET_SING = save_thm("MAX_SET_SING", MAX_SET_REWRITES |> CONJUNCT2 |> GEN_ALL); 1379(* val MAX_SET_SING = |- !e. MAX_SET {e} = e: thm *) 1380 1381(* Theorem: FINITE s /\ s <> {} ==> MAX_SET s IN s *) 1382(* Proof: by MAX_SET_DEF *) 1383val MAX_SET_IN_SET = store_thm( 1384 "MAX_SET_IN_SET", 1385 ``!s. FINITE s /\ s <> {} ==> MAX_SET s IN s``, 1386 rw[MAX_SET_DEF]); 1387 1388(* Theorem: FINITE s ==> !x. x IN s ==> x <= MAX_SET s *) 1389(* Proof: by in_max_set *) 1390val MAX_SET_PROPERTY = save_thm("MAX_SET_PROPERTY", in_max_set); 1391(* val MAX_SET_PROPERTY = |- !s. FINITE s ==> !x. x IN s ==> x <= MAX_SET s: thm *) 1392 1393(* Note: MIN_SET {} is undefined. *) 1394 1395(* Theorem: MIN_SET {e} = e *) 1396(* Proof: by MIN_SET_THM *) 1397val MIN_SET_SING = save_thm("MIN_SET_SING", MIN_SET_THM |> CONJUNCT1); 1398(* val MIN_SET_SING = |- !e. MIN_SET {e} = e: thm *) 1399 1400(* Theorem: s <> {} ==> MIN_SET s IN s *) 1401(* Proof: by MIN_SET_LEM *) 1402val MIN_SET_IN_SET = save_thm("MIN_SET_IN_SET", 1403 MIN_SET_LEM |> SPEC_ALL |> UNDISCH |> CONJUNCT1 |> DISCH_ALL |> GEN_ALL); 1404(* val MIN_SET_IN_SET = |- !s. s <> {} ==> MIN_SET s IN s: thm *) 1405 1406(* Theorem: s <> {} ==> !x. x IN s ==> MIN_SET s <= x *) 1407(* Proof: by MIN_SET_LEM *) 1408val MIN_SET_PROPERTY = save_thm("MIN_SET_PROPERTY", 1409 MIN_SET_LEM |> SPEC_ALL |> UNDISCH |> CONJUNCT2 |> DISCH_ALL |> GEN_ALL); 1410(* val MIN_SET_PROPERTY =|- !s. s <> {} ==> !x. x IN s ==> MIN_SET s <= x: thm *) 1411 1412 1413(* Theorem: FINITE s /\ s <> {} /\ s <> {MIN_SET s} ==> (MAX_SET (s DELETE (MIN_SET s)) = MAX_SET s) *) 1414(* Proof: 1415 Let m = MIN_SET s, t = s DELETE m. 1416 Then t SUBSET s by DELETE_SUBSET 1417 so FINITE t by SUBSET_FINITE]); 1418 Since m IN s by MIN_SET_IN_SET 1419 so t <> {} by DELETE_EQ_SING, s <> {m} 1420 ==> ?x. x IN t by MEMBER_NOT_EMPTY 1421 and x IN s /\ x <> m by IN_DELETE 1422 From x IN s ==> m <= x by MIN_SET_PROPERTY 1423 With x <> m ==> m < x by LESS_OR_EQ 1424 Also x <= MAX_SET s by MAX_SET_PROPERTY 1425 Thus MAX_SET s <> m since m < x <= MAX_SET s 1426 But MAX_SET s IN s by MAX_SET_IN_SET 1427 Thus MAX_SET s IN t by IN_DELETE 1428 Now !y. y IN t ==> 1429 y IN s by SUBSET_DEF 1430 or y <= MAX_SET s by MAX_SET_PROPERTY 1431 Hence MAX_SET s = MAX_SET t by MAX_SET_TEST 1432*) 1433val MAX_SET_DELETE = store_thm( 1434 "MAX_SET_DELETE", 1435 ``!s. FINITE s /\ s <> {} /\ s <> {MIN_SET s} ==> (MAX_SET (s DELETE (MIN_SET s)) = MAX_SET s)``, 1436 rpt strip_tac >> 1437 qabbrev_tac `m = MIN_SET s` >> 1438 qabbrev_tac `t = s DELETE m` >> 1439 `t SUBSET s` by rw[Abbr`t`] >> 1440 `FINITE t` by metis_tac[SUBSET_FINITE] >> 1441 `t <> {}` by metis_tac[MIN_SET_IN_SET, DELETE_EQ_SING] >> 1442 `?x. x IN t /\ x IN s /\ x <> m` by metis_tac[IN_DELETE, MEMBER_NOT_EMPTY] >> 1443 `m <= x` by rw[MIN_SET_PROPERTY, Abbr`m`] >> 1444 `m < x` by decide_tac >> 1445 `x <= MAX_SET s` by rw[MAX_SET_PROPERTY] >> 1446 `MAX_SET s <> m` by decide_tac >> 1447 `MAX_SET s IN t` by rw[MAX_SET_IN_SET, Abbr`t`] >> 1448 metis_tac[SUBSET_DEF, MAX_SET_PROPERTY, MAX_SET_TEST]); 1449 1450(* Theorem: FINITE s ==> ((MAX_SET s = 0) <=> (s = {}) \/ (s = {0})) *) 1451(* Proof: 1452 If part: MAX_SET s = 0 ==> (s = {}) \/ (s = {0}) 1453 By contradiction, suppose s <> {} /\ s <> {0}. 1454 Then ?x. x IN s /\ x <> 0 by ONE_ELEMENT_SING 1455 Thus x <= MAX_SET s by in_max_set 1456 so MAX_SET s <> 0 by x <> 0 1457 This contradicts MAX_SET s = 0. 1458 Only-if part: (s = {}) \/ (s = {0}) ==> MAX_SET s = 0 1459 If s = {}, MAX_SET s = 0 by MAX_SET_EMPTY 1460 If s = {0}, MAX_SET s = 0 by MAX_SET_SING 1461*) 1462val MAX_SET_EQ_0 = store_thm( 1463 "MAX_SET_EQ_0", 1464 ``!s. FINITE s ==> ((MAX_SET s = 0) <=> (s = {}) \/ (s = {0}))``, 1465 (rw[EQ_IMP_THM] >> simp[]) >> 1466 CCONTR_TAC >> 1467 `s <> {} /\ s <> {0}` by metis_tac[] >> 1468 `?x. x IN s /\ x <> 0` by metis_tac[ONE_ELEMENT_SING] >> 1469 `x <= MAX_SET s` by rw[in_max_set] >> 1470 decide_tac); 1471 1472(* Theorem: s <> {} ==> ((MIN_SET s = 0) <=> 0 IN s) *) 1473(* Proof: 1474 If part: MIN_SET s = 0 ==> 0 IN s 1475 This is true by MIN_SET_IN_SET. 1476 Only-if part: 0 IN s ==> MIN_SET s = 0 1477 Note MIN_SET s <= 0 by MIN_SET_LEM, 0 IN s 1478 Thus MIN_SET s = 0 by arithmetic 1479*) 1480val MIN_SET_EQ_0 = store_thm( 1481 "MIN_SET_EQ_0", 1482 ``!s. s <> {} ==> ((MIN_SET s = 0) <=> 0 IN s)``, 1483 rw[EQ_IMP_THM] >- 1484 metis_tac[MIN_SET_IN_SET] >> 1485 `MIN_SET s <= 0` by rw[MIN_SET_LEM] >> 1486 decide_tac); 1487 1488(* Theorem: MAX_SET (IMAGE SUC (count n)) = n *) 1489(* Proof: 1490 By induction on n. 1491 Base case: MAX_SET (IMAGE SUC (count 0)) = 0 1492 LHS = MAX_SET (IMAGE SUC (count 0)) 1493 = MAX_SET (IMAGE SUC {}) by COUNT_ZERO 1494 = MAX_SET {} by IMAGE_EMPTY 1495 = 0 by MAX_SET_THM 1496 = RHS 1497 Step case: MAX_SET (IMAGE SUC (count n)) = n ==> 1498 MAX_SET (IMAGE SUC (count (SUC n))) = SUC n 1499 LHS = MAX_SET (IMAGE SUC (count (SUC n))) 1500 = MAX_SET (IMAGE SUC (n INSERT count n)) by COUNT_SUC 1501 = MAX_SET ((SUC n) INSERT (IMAGE SUC (count n))) by IMAGE_INSERT 1502 = MAX (SUC n) (MAX_SET (IMAGE SUC (count n))) by MAX_SET_THM 1503 = MAX (SUC n) n by induction hypothesis 1504 = SUC n by LESS_SUC, MAX_DEF 1505 = RHS 1506*) 1507val MAX_SET_IMAGE_SUC_COUNT = store_thm( 1508 "MAX_SET_IMAGE_SUC_COUNT", 1509 ``!n. MAX_SET (IMAGE SUC (count n)) = n``, 1510 Induct_on `n` >- 1511 rw[] >> 1512 `MAX_SET (IMAGE SUC (count (SUC n))) = MAX_SET (IMAGE SUC (n INSERT count n))` by rw[COUNT_SUC] >> 1513 `_ = MAX_SET ((SUC n) INSERT (IMAGE SUC (count n)))` by rw[] >> 1514 `_ = MAX (SUC n) (MAX_SET (IMAGE SUC (count n)))` by rw[MAX_SET_THM] >> 1515 `_ = MAX (SUC n) n` by rw[] >> 1516 `_ = SUC n` by metis_tac[LESS_SUC, MAX_DEF, MAX_COMM] >> 1517 rw[]); 1518 1519(* Another Proof: *) 1520(* Theorem: MAX_SET (IMAGE SUC (count n)) = n *) 1521(* Proof: 1522 By induction on n. 1523 Base case: MAX_SET (IMAGE SUC (count 0)) = 0 1524 LHS = MAX_SET (IMAGE SUC (count 0)) 1525 = MAX_SET (IMAGE SUC {}) by COUNT_ZERO 1526 = MAX_SET {} by IMAGE_EMPTY 1527 = 0 by MAX_SET_DEF 1528 = RHS 1529 Step case: MAX_SET (IMAGE SUC (count n)) = n ==> 1530 MAX_SET (IMAGE SUC (count (SUC n))) = SUC n 1531 Note: FINITE (IMAGE SUC (count n)) by FINITE_COUNT, IMAGE_FINITE 1532 LHS = MAX_SET (IMAGE SUC (count (SUC n))) 1533 = MAX_SET (IMAGE SUC (n INSERT (count n))) by COUNT_SUC 1534 = MAX_SET ((SUC n) INSERT (IMAGE SUC (count n))) by IMAGE_INSERT 1535 = MAX (SUC n) (MAX_SET (IMAGE SUC (count n))) by MAX_SET_THM 1536 = MAX (SUC n) n by induction hypothesis 1537 = SUC n by LESS_SUC, MAX_DEF 1538 = RHS 1539*) 1540val MAX_SET_IMAGE_SUC_COUNT = store_thm( 1541 "MAX_SET_IMAGE_SUC_COUNT", 1542 ``!n. MAX_SET (IMAGE SUC (count n)) = n``, 1543 Induct_on `n` >- 1544 rw[MAX_SET_DEF] >> 1545 `MAX_SET (IMAGE SUC (count (SUC n))) = MAX (SUC n) (MAX_SET (IMAGE SUC (count n)))` by rw[COUNT_SUC, MAX_SET_THM] >> 1546 metis_tac[MAX_SET_THM, LESS_SUC, MAX_DEF, MAX_COMM, FINITE_COUNT, IMAGE_FINITE]); 1547 1548(* Theorem: HALF x <= c ==> f x <= MAX_SET {f x | HALF x <= c} *) 1549(* Proof: 1550 Let s = {f x | HALF x <= c} 1551 Note !x. HALF x <= c 1552 ==> SUC (2 * HALF x) <= SUC (2 * c) by arithmetic 1553 and x <= SUC (2 * HALF x) by TWO_HALF_LESS_EQ 1554 so x <= SUC (2 * c) < 2 * c + 2 by arithmetic 1555 Thus s SUBSET (IMAGE f (count (2 * c + 2))) by SUBSET_DEF 1556 Note FINITE (count (2 * c + 2)) by FINITE_COUNT 1557 so FINITE s by IMAGE_FINITE, SUBSET_FINITE 1558 and f x IN s by HALF x <= c 1559 Thus f x <= MAX_SET s by MAX_SET_PROPERTY 1560*) 1561val MAX_SET_IMAGE_with_HALF = store_thm( 1562 "MAX_SET_IMAGE_with_HALF", 1563 ``!f c x. HALF x <= c ==> f x <= MAX_SET {f x | HALF x <= c}``, 1564 rpt strip_tac >> 1565 qabbrev_tac `s = {f x | HALF x <= c}` >> 1566 `s SUBSET (IMAGE f (count (2 * c + 2)))` by 1567 (rw[SUBSET_DEF, Abbr`s`] >> 1568 `SUC (2 * HALF x'') <= SUC (2 * c)` by rw[] >> 1569 `x'' <= SUC (2 * HALF x'')` by rw[TWO_HALF_LESS_EQ] >> 1570 `x'' < 2 * c + 2` by decide_tac >> 1571 metis_tac[]) >> 1572 `FINITE s` by metis_tac[FINITE_COUNT, IMAGE_FINITE, SUBSET_FINITE] >> 1573 (`f x IN s` by (rw[Abbr`s`] >> metis_tac[])) >> 1574 rw[MAX_SET_PROPERTY]); 1575 1576(* 1577Note: A more general version, replacing HALF x by g x, would be desirable. 1578However, there is no way to show FINITE s for arbitrary g x. 1579*) 1580 1581(* Theorem: 0 < b /\ x DIV b <= c ==> f x <= MAX_SET {f x | x DIV b <= c} *) 1582(* Proof: 1583 Let s = {f x | x DIV b <= c}. 1584 Note !x. x DIV b <= c 1585 ==> b * SUC (x DIV b) <= b * SUC c by arithmetic 1586 and x < b * SUC (x DIV b) by DIV_MULT_LESS_EQ, 0 < b 1587 so x < b * SUC c by arithmetic 1588 Thus s SUBSET (IMAGE f (count (b * SUC c))) by SUBSET_DEF 1589 Note FINITE (count (b * SUC c)) by FINITE_COUNT 1590 so FINITE s by IMAGE_FINITE, SUBSET_FINITE 1591 and f x IN s by HALF x <= c 1592 Thus f x <= MAX_SET s by MAX_SET_PROPERTY 1593*) 1594val MAX_SET_IMAGE_with_DIV = store_thm( 1595 "MAX_SET_IMAGE_with_DIV", 1596 ``!f b c x. 0 < b /\ x DIV b <= c ==> f x <= MAX_SET {f x | x DIV b <= c}``, 1597 rpt strip_tac >> 1598 qabbrev_tac `s = {f x | x DIV b <= c}` >> 1599 `s SUBSET (IMAGE f (count (b * SUC c)))` by 1600 (rw[SUBSET_DEF, Abbr`s`] >> 1601 `b * SUC (x'' DIV b) <= b * SUC c` by rw[] >> 1602 `x'' < b * SUC (x'' DIV b)` by rw[DIV_MULT_LESS_EQ] >> 1603 `x'' < b * SUC c` by decide_tac >> 1604 metis_tac[]) >> 1605 `FINITE s` by metis_tac[FINITE_COUNT, IMAGE_FINITE, SUBSET_FINITE] >> 1606 (`f x IN s` by (rw[Abbr`s`] >> metis_tac[])) >> 1607 rw[MAX_SET_PROPERTY]); 1608 1609(* Theorem: x - b <= c ==> f x <= MAX_SET {f x | x - b <= c} *) 1610(* Proof: 1611 Let s = {f x | x - b <= c} 1612 Note !x. x - b <= c ==> x <= b + c by arithmetic 1613 so x <= 1 + b + c by arithmetic 1614 Thus s SUBSET (IMAGE f (count (1 + b + c))) by SUBSET_DEF 1615 Note FINITE (count (1 + b + c)) by FINITE_COUNT 1616 so FINITE s by IMAGE_FINITE, SUBSET_FINITE 1617 and f x IN s by x - b <= c 1618 Thus f x <= MAX_SET s by MAX_SET_PROPERTY 1619*) 1620val MAX_SET_IMAGE_with_DEC = store_thm( 1621 "MAX_SET_IMAGE_with_DEC", 1622 ``!f b c x. x - b <= c ==> f x <= MAX_SET {f x | x - b <= c}``, 1623 rpt strip_tac >> 1624 qabbrev_tac `s = {f x | x - b <= c}` >> 1625 `s SUBSET (IMAGE f (count (1 + b + c)))` by 1626 (rw[SUBSET_DEF, Abbr`s`] >> 1627 `x'' < b + (c + 1)` by decide_tac >> 1628 metis_tac[]) >> 1629 `FINITE s` by metis_tac[FINITE_COUNT, IMAGE_FINITE, SUBSET_FINITE] >> 1630 `f x IN s` by 1631 (rw[Abbr`s`] >> 1632 `x <= b + c` by decide_tac >> 1633 metis_tac[]) >> 1634 rw[MAX_SET_PROPERTY]); 1635 1636(* ------------------------------------------------------------------------- *) 1637(* Finite and Cardinality Theorems *) 1638(* ------------------------------------------------------------------------- *) 1639 1640 1641(* Theorem: INJ f s UNIV /\ FINITE s ==> CARD (IMAGE f s) = CARD s *) 1642(* Proof: 1643 !x y. x IN s /\ y IN s /\ f x = f y == x = y by INJ_DEF 1644 FINITE s ==> FINITE (IMAGE f s) by IMAGE_FINITE 1645 Therefore BIJ f s (IMAGE f s) by BIJ_DEF, INJ_DEF, SURJ_DEF 1646 Hence CARD (IMAGE f s) = CARD s by FINITE_BIJ_CARD_EQ 1647*) 1648val INJ_CARD_IMAGE_EQN = store_thm( 1649 "INJ_CARD_IMAGE_EQN", 1650 ``!f s. INJ f s UNIV /\ FINITE s ==> (CARD (IMAGE f s) = CARD s)``, 1651 rw[INJ_DEF] >> 1652 `FINITE (IMAGE f s)` by rw[IMAGE_FINITE] >> 1653 `BIJ f s (IMAGE f s)` by rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >> 1654 metis_tac[FINITE_BIJ_CARD_EQ]); 1655 1656 1657(* Theorem: FINTIE s /\ FINITE t /\ CARD s = CARD t /\ INJ f s t ==> SURJ f s t *) 1658(* Proof: 1659 For any map f from s to t, 1660 (IMAGE f s) SUBSET t by IMAGE_SUBSET_TARGET 1661 FINITE s ==> FINITE (IMAGE f s) by IMAGE_FINITE 1662 CARD (IMAGE f s) = CARD s by INJ_CARD_IMAGE 1663 = CARD t by given 1664 Hence (IMAGE f s) = t by SUBSET_EQ_CARD, FINITE t 1665 or SURJ f s t by IMAGE_SURJ 1666*) 1667val FINITE_INJ_AS_SURJ = store_thm( 1668 "FINITE_INJ_AS_SURJ", 1669 ``!f s t. INJ f s t /\ FINITE s /\ FINITE t /\ (CARD s = CARD t) ==> SURJ f s t``, 1670 rw[INJ_DEF] >> 1671 `(IMAGE f s) SUBSET t` by rw[GSYM IMAGE_SUBSET_TARGET] >> 1672 `FINITE (IMAGE f s)` by rw[IMAGE_FINITE] >> 1673 `CARD (IMAGE f s) = CARD t` by metis_tac[INJ_DEF, INJ_CARD_IMAGE, INJ_SUBSET, SUBSET_REFL, SUBSET_UNIV] >> 1674 rw[SUBSET_EQ_CARD, IMAGE_SURJ]); 1675 1676(* Theorem: FINITE {P x | x < n} *) 1677(* Proof: 1678 Since IMAGE (\i. P i) (count n) = {P x | x < n}, 1679 this follows by 1680 IMAGE_FINITE |- !s. FINITE s ==> !f. FINITE (IMAGE f s) : thm 1681 FINITE_COUNT |- !n. FINITE (count n) : thm 1682*) 1683val FINITE_COUNT_IMAGE = store_thm( 1684 "FINITE_COUNT_IMAGE", 1685 ``!P n. FINITE {P x | x < n }``, 1686 rpt strip_tac >> 1687 `IMAGE (\i. P i) (count n) = {P x | x < n}` by rw[IMAGE_DEF] >> 1688 metis_tac[IMAGE_FINITE, FINITE_COUNT]); 1689 1690(* Note: no need for CARD_IMAGE: 1691 1692CARD_INJ_IMAGE |- !f s. (!x y. (f x = f y) <=> (x = y)) /\ FINITE s ==> (CARD (IMAGE f s) = CARD s) 1693FINITE_BIJ_CARD_EQ |- !S. FINITE S ==> !t f. BIJ f S t /\ FINITE t ==> (CARD S = CARD t) 1694BIJ_LINV_BIJ |- !f s t. BIJ f s t ==> BIJ (LINV f s) t s 1695*) 1696 1697(* Theorem: FINITE s /\ BIJ f s t ==> FINITE t /\ (CARD s = CARD t) *) 1698(* Proof: 1699 First, FINITE s /\ BIJ f s t ==> FINITE t 1700 BIJ f s t ==> SURJ f s t by BIJ_DEF 1701 ==> IMAGE f s = t by IMAGE_SURJ 1702 FINITE s ==> FINITE (IMAGE f s) by IMAGE_FINITE 1703 Hence FINITE t. 1704 Next, FINITE s /\ FINITE t /\ BIJ f s t ==> CARD s = CARD t 1705 by FINITE_BIJ_CARD_EQ. 1706*) 1707val FINITE_BIJ_PROPERTY = store_thm( 1708 "FINITE_BIJ_PROPERTY", 1709 ``!f s t. FINITE s /\ BIJ f s t ==> FINITE t /\ (CARD s = CARD t)``, 1710 ntac 4 strip_tac >> 1711 CONJ_ASM1_TAC >| [ 1712 `SURJ f s t` by metis_tac[BIJ_DEF] >> 1713 `IMAGE f s = t` by rw[GSYM IMAGE_SURJ] >> 1714 rw[], 1715 metis_tac[FINITE_BIJ_CARD_EQ] 1716 ]); 1717 1718(* Note: 1719> pred_setTheory.CARD_IMAGE; 1720val it = |- !s. FINITE s ==> CARD (IMAGE f s) <= CARD s: thm 1721*) 1722 1723(* Theorem: For a 1-1 map f: s -> s, s and (IMAGE f s) are of the same size. *) 1724(* Proof: 1725 By finite induction on the set s: 1726 Base case: CARD (IMAGE f {}) = CARD {} 1727 True by IMAGE f {} = {} by IMAGE_EMPTY 1728 Step case: !s. FINITE s /\ (CARD (IMAGE f s) = CARD s) ==> !e. e NOTIN s ==> (CARD (IMAGE f (e INSERT s)) = CARD (e INSERT s)) 1729 CARD (IMAGE f (e INSERT s)) 1730 = CARD (f e INSERT IMAGE f s) by IMAGE_INSERT 1731 = SUC (CARD (IMAGE f s)) by CARD_INSERT: e NOTIN s, f e NOTIN s, for 1-1 map 1732 = SUC (CARD s) by induction hypothesis 1733 = CARD (e INSERT s) by CARD_INSERT: e NOTIN s. 1734*) 1735val FINITE_CARD_IMAGE = store_thm( 1736 "FINITE_CARD_IMAGE", 1737 ``!s f. (!x y. (f x = f y) <=> (x = y)) /\ FINITE s ==> (CARD (IMAGE f s) = CARD s)``, 1738 `!f. (!x y. (f x = f y) <=> (x = y)) ==> !s. FINITE s ==> (CARD (IMAGE f s) = CARD s)` suffices_by rw[] >> 1739 gen_tac >> 1740 strip_tac >> 1741 ho_match_mp_tac FINITE_INDUCT >> 1742 rw[]); 1743(* Michael's proof *) 1744val FINITE_CARD_IMAGE = store_thm( 1745 "FINITE_CARD_IMAGE", 1746 ``!s f. (!x y. (f x = f y) <=> (x = y)) /\ FINITE s ==> (CARD (IMAGE f s) = CARD s)``, 1747 qsuff_tac `!f. (!x y. (f x = f y) = (x = y)) ==> !s. FINITE s ==> (CARD (IMAGE f s) = CARD s)` >- 1748 metis_tac[] >> 1749 gen_tac >> strip_tac >> 1750 ho_match_mp_tac FINITE_INDUCT >> rw[]); 1751 1752(* Theorem: !s. FINITE s ==> CARD (IMAGE SUC s)) = CARD s *) 1753(* Proof: 1754 Since !n m. SUC n = SUC m <=> n = m by numTheory.INV_SUC 1755 This is true by FINITE_CARD_IMAGE. 1756*) 1757val CARD_IMAGE_SUC = store_thm( 1758 "CARD_IMAGE_SUC", 1759 ``!s. FINITE s ==> (CARD (IMAGE SUC s) = CARD s)``, 1760 rw[FINITE_CARD_IMAGE]); 1761 1762(* Theorem: FINITE s /\ FINITE t /\ DISJOINT s t ==> (CARD (s UNION t) = CARD s + CARD t) *) 1763(* Proof: by CARD_UNION_EQN, DISJOINT_DEF, CARD_EMPTY *) 1764val CARD_UNION_DISJOINT = store_thm( 1765 "CARD_UNION_DISJOINT", 1766 ``!s t. FINITE s /\ FINITE t /\ DISJOINT s t ==> (CARD (s UNION t) = CARD s + CARD t)``, 1767 rw_tac std_ss[CARD_UNION_EQN, DISJOINT_DEF, CARD_EMPTY]); 1768 1769(* Theorem: !n. 0 < n ==> IMAGE (\x. x MOD n) s SUBSET (count n) *) 1770(* Proof: by SUBSET_DEF, MOD_LESS. *) 1771val image_mod_subset_count = store_thm( 1772 "image_mod_subset_count", 1773 ``!s n. 0 < n ==> IMAGE (\x. x MOD n) s SUBSET (count n)``, 1774 rw[SUBSET_DEF] >> 1775 rw[MOD_LESS]); 1776 1777(* Theorem: !n. 0 < n ==> CARD (IMAGE (\x. x MOD n) s) <= n *) 1778(* Proof: 1779 Let t = IMAGE (\x. x MOD n) s 1780 Since t SUBSET count n by SUBSET_DEF, MOD_LESS 1781 Now FINITE (count n) by FINITE_COUNT 1782 and CARD (count n) = n by CARD_COUNT 1783 So CARD t <= n by CARD_SUBSET 1784*) 1785val card_mod_image = store_thm( 1786 "card_mod_image", 1787 ``!s n. 0 < n ==> CARD (IMAGE (\x. x MOD n) s) <= n``, 1788 rpt strip_tac >> 1789 qabbrev_tac `t = IMAGE (\x. x MOD n) s` >> 1790 (`t SUBSET count n` by (rw[SUBSET_DEF, Abbr`t`] >> metis_tac[MOD_LESS])) >> 1791 metis_tac[CARD_SUBSET, FINITE_COUNT, CARD_COUNT]); 1792(* not used *) 1793 1794(* Theorem: !n. 0 < n /\ 0 NOTIN (IMAGE (\x. x MOD n) s) ==> CARD (IMAGE (\x. x MOD n) s) < n *) 1795(* Proof: 1796 Let t = IMAGE (\x. x MOD n) s 1797 Since t SUBSET count n by SUBSET_DEF, MOD_LESS 1798 Now FINITE (count n) by FINITE_COUNT 1799 and CARD (count n) = n by CARD_COUNT 1800 So CARD t <= n by CARD_SUBSET 1801 and FINITE t by SUBSET_FINITE 1802 But 0 IN (count n) by IN_COUNT 1803 yet 0 NOTIN t by given 1804 Hence t <> (count n) by NOT_EQUAL_SETS 1805 So CARD t <> n by SUBSET_EQ_CARD 1806 Thus CARD t < n 1807*) 1808val card_mod_image_nonzero = store_thm( 1809 "card_mod_image_nonzero", 1810 ``!s n. 0 < n /\ 0 NOTIN (IMAGE (\x. x MOD n) s) ==> CARD (IMAGE (\x. x MOD n) s) < n``, 1811 rpt strip_tac >> 1812 qabbrev_tac `t = IMAGE (\x. x MOD n) s` >> 1813 (`t SUBSET count n` by (rw[SUBSET_DEF, Abbr`t`] >> metis_tac[MOD_LESS])) >> 1814 `FINITE (count n) /\ (CARD (count n) = n) ` by rw[] >> 1815 `CARD t <= n` by metis_tac[CARD_SUBSET] >> 1816 `0 IN (count n)` by rw[] >> 1817 `t <> (count n)` by metis_tac[NOT_EQUAL_SETS] >> 1818 `CARD t <> n` by metis_tac[SUBSET_EQ_CARD, SUBSET_FINITE] >> 1819 decide_tac); 1820(* not used *) 1821 1822(* ------------------------------------------------------------------------- *) 1823(* Partition Property *) 1824(* ------------------------------------------------------------------------- *) 1825 1826(* Overload partition by split *) 1827val _ = overload_on("split", ``\s u v. (s = u UNION v) /\ (DISJOINT u v)``); 1828 1829(* Pretty printing of partition by split *) 1830val _ = add_rule {block_style = (AroundEachPhrase, (PP.CONSISTENT, 2)), 1831 fixity = Infix(NONASSOC, 450), 1832 paren_style = OnlyIfNecessary, 1833 term_name = "split", 1834 pp_elements = [HardSpace 1, TOK "=|=", HardSpace 1, TM, 1835 BreakSpace(1,1), TOK "#", BreakSpace(1,1)]}; 1836 1837(* Theorem: FINITE s ==> !u v. s =|= u # v ==> ((u = {}) <=> (v = s)) *) 1838(* Proof: 1839 If part: u = {} ==> v = s 1840 Note s = {} UNION v by given, u = {} 1841 = v by UNION_EMPTY 1842 Only-if part: v = s ==> u = {} 1843 Note FINITE u /\ FINITE v by FINITE_UNION 1844 ==> CARD v = CARD u + CARD v by CARD_UNION_DISJOINT 1845 ==> 0 = CARD u by arithmetic 1846 Thus u = {} by CARD_EQ_0 1847*) 1848val finite_partition_property = store_thm( 1849 "finite_partition_property", 1850 ``!s. FINITE s ==> !u v. s =|= u # v ==> ((u = {}) <=> (v = s))``, 1851 rw[EQ_IMP_THM] >> 1852 spose_not_then strip_assume_tac >> 1853 `FINITE u /\ FINITE v` by metis_tac[FINITE_UNION] >> 1854 `CARD v = CARD u + CARD v` by metis_tac[CARD_UNION_DISJOINT] >> 1855 `CARD u <> 0` by rw[CARD_EQ_0] >> 1856 decide_tac); 1857 1858(* Theorem: FINITE s ==> !P. let u = {x | x IN s /\ P x} in let v = {x | x IN s /\ ~P x} in 1859 FINITE u /\ FINITE v /\ s =|= u # v *) 1860(* Proof: 1861 This is to show: 1862 (1) FINITE u, true by SUBSET_DEF, SUBSET_FINITE 1863 (2) FINITE v, true by SUBSET_DEF, SUBSET_FINITE 1864 (3) u UNION v = s by IN_UNION 1865 (4) DISJOINT u v, true by IN_DISJOINT, MEMBER_NOT_EMPTY 1866*) 1867Theorem finite_partition_by_predicate: 1868 !s. FINITE s ==> 1869 !P. let u = {x | x IN s /\ P x} ; 1870 v = {x | x IN s /\ ~P x} 1871 in 1872 FINITE u /\ FINITE v /\ s =|= u # v 1873Proof 1874 rw_tac std_ss[] >| [ 1875 `u SUBSET s` by rw[SUBSET_DEF, Abbr`u`] >> 1876 metis_tac[SUBSET_FINITE], 1877 `v SUBSET s` by rw[SUBSET_DEF, Abbr`v`] >> 1878 metis_tac[SUBSET_FINITE], 1879 simp[EXTENSION, Abbr���u���, Abbr���v���] >> 1880 metis_tac[], 1881 simp[Abbr���u���, Abbr���v���, DISJOINT_DEF, EXTENSION] >> metis_tac[] 1882 ] 1883QED 1884 1885(* Theorem: u SUBSET s ==> let v = s DIFF u in s =|= u # v *) 1886(* Proof: 1887 This is to show: 1888 (1) u SUBSET s ==> s = u UNION (s DIFF u), true by UNION_DIFF 1889 (2) u SUBSET s ==> DISJOINT u (s DIFF u), true by DISJOINT_DIFF 1890*) 1891val partition_by_subset = store_thm( 1892 "partition_by_subset", 1893 ``!s u. u SUBSET s ==> let v = s DIFF u in s =|= u # v``, 1894 rw[UNION_DIFF, DISJOINT_DIFF]); 1895 1896(* Theorem: x IN s ==> s =|= {x} # (s DELETE x) *) 1897(* Proof: 1898 Note x IN s ==> {x} SUBSET s by SUBSET_DEF, IN_SING 1899 and s DELETE x = s DIFF {x} by DELETE_DEF 1900 Thus s =|= {x} # (s DELETE x) by partition_by_subset 1901*) 1902val partition_by_element = store_thm( 1903 "partition_by_element", 1904 ``!s x. x IN s ==> s =|= {x} # (s DELETE x)``, 1905 metis_tac[partition_by_subset, DELETE_DEF, SUBSET_DEF, IN_SING]); 1906 1907(* ------------------------------------------------------------------------- *) 1908(* Splitting of a set *) 1909(* ------------------------------------------------------------------------- *) 1910 1911(* Theorem: s =|= {} # t <=> (s = t) *) 1912(* Proof: 1913 s =|= {} # t 1914 <=> (s = {} UNION t) /\ (DISJOINT {} t) by notation 1915 <=> (s = {} UNION t) /\ T by DISJOINT_EMPTY 1916 <=> s = t by UNION_EMPTY 1917*) 1918val SPLIT_EMPTY = store_thm( 1919 "SPLIT_EMPTY", 1920 ``!s t. s =|= {} # t <=> (s = t)``, 1921 rw[]); 1922 1923(* Theorem: s =|= u # v /\ v =|= a # b ==> s =|= u UNION a # b /\ u UNION a =|= u # a *) 1924(* Proof: 1925 Note s =|= u # v <=> (s = u UNION v) /\ (DISJOINT u v) by notation 1926 and v =|= a # b <=> (v = a UNION b) /\ (DISJOINT a b) by notation 1927 Let c = u UNION a. 1928 Then s = u UNION v by above 1929 = u UNION (a UNION b) by above 1930 = (u UNION a) UNION b by UNION_ASSOC 1931 = c UNION b 1932 Note DISJOINT u v 1933 <=> DISJOINT u (a UNION b) 1934 <=> DISJOINT (a UNION b) u by DISJOINT_SYM 1935 <=> DISJOINT a u /\ DISJOINT b u by DISJOINT_UNION 1936 <=> DISJOINT u a /\ DISJOINT u b by DISJOINT_SYM 1937 1938 Thus DISJOINT c b 1939 <=> DISJOINT (u UNION a) b by above 1940 <=> DISJOINT u b /\ DISJOINT a b by DISJOINT_UNION 1941 <=> T /\ T by above 1942 <=> T 1943 Therefore, 1944 s =|= c # b by s = c UNION b /\ DISJOINT c b 1945 and c =|= u # a by c = u UNION a /\ DISJOINT u a 1946*) 1947val SPLIT_UNION = store_thm( 1948 "SPLIT_UNION", 1949 ``!s u v a b. s =|= u # v /\ v =|= a # b ==> s =|= u UNION a # b /\ u UNION a =|= u # a``, 1950 metis_tac[DISJOINT_UNION, DISJOINT_SYM, UNION_ASSOC]); 1951 1952(* Theorem: s =|= u # v <=> u SUBSET s /\ (v = s DIFF u) *) 1953(* Proof: 1954 Note s =|= u # v <=> (s = u UNION v) /\ (DISJOINT u v) by notation 1955 If part: s =|= u # v ==> u SUBSET s /\ (v = s DIFF u) 1956 Note u SUBSET (u UNION v) by SUBSET_UNION 1957 s DIFF u 1958 = (u UNION v) DIFF u by s = u UNION v 1959 = v DIFF u by DIFF_SAME_UNION 1960 = v by DISJOINT_DIFF_IFF, DISJOINT_SYM 1961 1962 Only-if part: u SUBSET s /\ (v = s DIFF u) ==> s =|= u # v 1963 Note s = u UNION (s DIFF u) by UNION_DIFF, u SUBSET s 1964 and DISJOINT u (s DIFF u) by DISJOINT_DIFF 1965 Thus s =|= u # v by notation 1966*) 1967val SPLIT_EQ = store_thm( 1968 "SPLIT_EQ", 1969 ``!s u v. s =|= u # v <=> u SUBSET s /\ (v = s DIFF u)``, 1970 rw[DISJOINT_DEF, SUBSET_DEF, EXTENSION] >> 1971 metis_tac[]); 1972 1973(* Theorem: (s =|= u # v) = (s =|= v # u) *) 1974(* Proof: 1975 s =|= u # v 1976 = (s = u UNION v) /\ DISJOINT u v by notation 1977 = (s = v UNION u) /\ DISJOINT u v by UNION_COMM 1978 = (s = v UNION u) /\ DISJOINT v u by DISJOINT_SYM 1979 = s =|= v # u by notation 1980*) 1981val SPLIT_SYM = store_thm( 1982 "SPLIT_SYM", 1983 ``!s u v. (s =|= u # v) = (s =|= v # u)``, 1984 rw_tac std_ss[UNION_COMM, DISJOINT_SYM]); 1985 1986(* Theorem: (s =|= u # v) ==> (s =|= v # u) *) 1987(* Proof: by SPLIT_SYM *) 1988val SPLIT_SYM_IMP = store_thm( 1989 "SPLIT_SYM_IMP", 1990 ``!s u v. (s =|= u # v) ==> (s =|= v # u)``, 1991 rw_tac std_ss[SPLIT_SYM]); 1992 1993(* Theorem: s =|= {x} # v <=> (x IN s /\ (v = s DELETE x)) *) 1994(* Proof: 1995 s =|= {x} # v 1996 <=> {x} SUBSET s /\ (v = s DIFF {x}) by SPLIT_EQ 1997 <=> x IN s /\ (v = s DIFF {x}) by SUBSET_DEF 1998 <=> x IN s /\ (v = s DELETE x) by DELETE_DEF 1999*) 2000val SPLIT_SING = store_thm( 2001 "SPLIT_SING", 2002 ``!s v x. s =|= {x} # v <=> (x IN s /\ (v = s DELETE x))``, 2003 rw[SPLIT_EQ, SUBSET_DEF, DELETE_DEF]); 2004 2005(* Theorem: s =|= u # v ==> u SUBSET s /\ v SUBSET s *) 2006(* Proof: by SUBSET_UNION *) 2007Theorem SPLIT_SUBSETS: 2008 !s u v. s =|= u # v ==> u SUBSET s /\ v SUBSET s 2009Proof 2010 rw[] 2011QED 2012 2013(* Theorem: FINITE s /\ s =|= u # v ==> FINITE u /\ FINITE v *) 2014(* Proof: by SPLIT_SUBSETS, SUBSET_FINITE *) 2015Theorem SPLIT_FINITE: 2016 !s u v. FINITE s /\ s =|= u # v ==> FINITE u /\ FINITE v 2017Proof 2018 simp[SPLIT_SUBSETS, SUBSET_FINITE] 2019QED 2020 2021(* Theorem: FINITE s /\ s =|= u # v ==> (CARD s = CARD u + CARD v) *) 2022(* Proof: 2023 Note FINITE u /\ FINITE v by SPLIT_FINITE 2024 CARD s 2025 = CARD (u UNION v) by notation 2026 = CARD u + CARD v by CARD_UNION_DISJOINT 2027*) 2028Theorem SPLIT_CARD: 2029 !s u v. FINITE s /\ s =|= u # v ==> (CARD s = CARD u + CARD v) 2030Proof 2031 metis_tac[CARD_UNION_DISJOINT, SPLIT_FINITE] 2032QED 2033 2034(* Theorem: s =|= u # v <=> (u = s DIFF v) /\ (v = s DIFF u) *) 2035(* Proof: 2036 If part: s =|= u # v ==> (u = s DIFF v) /\ (v = s DIFF u) 2037 True by EXTENSION, IN_UNION, IN_DISJOINT, IN_DIFF. 2038 Only-if part: (u = s DIFF v) /\ (v = s DIFF u) ==> s =|= u # v 2039 True by EXTENSION, IN_UNION, IN_DISJOINT, IN_DIFF. 2040*) 2041val SPLIT_EQ_DIFF = store_thm( 2042 "SPLIT_EQ_DIFF", 2043 ``!s u v. s =|= u # v <=> (u = s DIFF v) /\ (v = s DIFF u)``, 2044 rpt strip_tac >> 2045 eq_tac >| [ 2046 rpt strip_tac >| [ 2047 rw[EXTENSION] >> 2048 metis_tac[IN_UNION, IN_DISJOINT, IN_DIFF], 2049 rw[EXTENSION] >> 2050 metis_tac[IN_UNION, IN_DISJOINT, IN_DIFF] 2051 ], 2052 rpt strip_tac >| [ 2053 rw[EXTENSION] >> 2054 metis_tac[IN_UNION, IN_DIFF], 2055 metis_tac[IN_DISJOINT, IN_DIFF] 2056 ] 2057 ]); 2058 2059(* Theorem alias *) 2060val SPLIT_BY_SUBSET = save_thm("SPLIT_BY_SUBSET", partition_by_subset); 2061(* val SPLIT_BY_SUBSET = |- !s u. u SUBSET s ==> (let v = s DIFF u in s =|= u # v): thm *) 2062 2063(* Theorem alias *) 2064val SUBSET_DIFF_DIFF = save_thm("SUBSET_DIFF_DIFF", DIFF_DIFF_SUBSET); 2065(* val SUBSET_DIFF_DIFF = |- !s t. t SUBSET s ==> (s DIFF (s DIFF t) = t) *) 2066 2067(* Theorem: s1 SUBSET t /\ s2 SUBSET t /\ (t DIFF s1 = t DIFF s2) ==> (s1 = s2) *) 2068(* Proof: 2069 Let u = t DIFF s2. 2070 Then u = t DIFF s1 by given 2071 ==> t =|= u # s1 by SPLIT_BY_SUBSET, s1 SUBSET t 2072 Thus s1 = t DIFF u by SPLIT_EQ 2073 = t DIFF (t DIFF s2) by notation 2074 = s2 by SUBSET_DIFF_DIFF, s2 SUBSET t 2075*) 2076val SUBSET_DIFF_EQ = store_thm( 2077 "SUBSET_DIFF_EQ", 2078 ``!s1 s2 t. s1 SUBSET t /\ s2 SUBSET t /\ (t DIFF s1 = t DIFF s2) ==> (s1 = s2)``, 2079 metis_tac[SPLIT_BY_SUBSET, SPLIT_EQ, SUBSET_DIFF_DIFF]); 2080 2081(* ------------------------------------------------------------------------- *) 2082(* Bijective Inverses. *) 2083(* ------------------------------------------------------------------------- *) 2084 2085(* In pred_setTheory: 2086LINV_DEF |- !f s t. INJ f s t ==> !x. x IN s ==> (LINV f s (f x) = x) 2087BIJ_LINV_INV |- !f s t. BIJ f s t ==> !x. x IN t ==> (f (LINV f s x) = x) 2088BIJ_LINV_BIJ |- !f s t. BIJ f s t ==> BIJ (LINV f s) t s 2089RINV_DEF |- !f s t. SURJ f s t ==> !x. x IN t ==> (f (RINV f s x) = x) 2090 2091That's it, must be missing some! 2092Must assume: !y. y IN t ==> RINV f s y IN s 2093*) 2094 2095(* Theorem: BIJ f s t ==> !x. x IN t ==> (LINV f s x) IN s *) 2096(* Proof: 2097 Since BIJ f s t ==> BIJ (LINV f s) t s by BIJ_LINV_BIJ 2098 so x IN t ==> (LINV f s x) IN s by BIJ_DEF, INJ_DEF 2099*) 2100val BIJ_LINV_ELEMENT = store_thm( 2101 "BIJ_LINV_ELEMENT", 2102 ``!f s t. BIJ f s t ==> !x. x IN t ==> (LINV f s x) IN s``, 2103 metis_tac[BIJ_LINV_BIJ, BIJ_DEF, INJ_DEF]); 2104 2105(* Theorem: (!x. x IN s ==> (LINV f s (f x) = x)) /\ (!x. x IN t ==> (f (LINV f s x) = x)) *) 2106(* Proof: 2107 Since BIJ f s t ==> INJ f s t by BIJ_DEF 2108 and INJ f s t ==> !x. x IN s ==> (LINV f s (f x) = x) by LINV_DEF 2109 also BIJ f s t ==> !x. x IN t ==> (f (LINV f s x) = x) by BIJ_LINV_INV 2110*) 2111val BIJ_LINV_THM = store_thm( 2112 "BIJ_LINV_THM", 2113 ``!(f:'a -> 'b) s t. BIJ f s t ==> 2114 (!x. x IN s ==> (LINV f s (f x) = x)) /\ (!x. x IN t ==> (f (LINV f s x) = x))``, 2115 metis_tac[BIJ_DEF, LINV_DEF, BIJ_LINV_INV]); 2116 2117(* Theorem: BIJ f s t /\ (!y. y IN t ==> RINV f s y IN s) ==> 2118 !x. x IN s ==> (RINV f s (f x) = x) *) 2119(* Proof: 2120 BIJ f s t means INJ f s t /\ SURJ f s t by BIJ_DEF 2121 Hence x IN s ==> f x IN t by INJ_DEF or SURJ_DEF 2122 ==> f (RINV f s (f x)) = f x by RINV_DEF, SURJ f s t 2123 ==> RINV f s (f x) = x by INJ_DEF 2124*) 2125val BIJ_RINV_INV = store_thm( 2126 "BIJ_RINV_INV", 2127 ``!(f:'a -> 'b) s t. BIJ f s t /\ (!y. y IN t ==> RINV f s y IN s) ==> 2128 !x. x IN s ==> (RINV f s (f x) = x)``, 2129 rw[BIJ_DEF] >> 2130 `f x IN t` by metis_tac[INJ_DEF] >> 2131 `f (RINV f s (f x)) = f x` by metis_tac[RINV_DEF] >> 2132 metis_tac[INJ_DEF]); 2133 2134(* Theorem: BIJ f s t /\ (!y. y IN t ==> RINV f s y IN s) ==> BIJ (RINV f s) t s *) 2135(* Proof: 2136 By BIJ_DEF, this is to show: 2137 (1) INJ (RINV f s) t s 2138 By INJ_DEF, this is to show: 2139 x IN t /\ y IN t /\ RINV f s x = RINV f s y ==> x = y 2140 But SURJ f s t by BIJ_DEF 2141 so f (RINV f s x) = x by RINV_DEF, SURJ f s t 2142 and f (RINV f s y) = y by RINV_DEF, SURJ f s t 2143 Thus x = y. 2144 (2) SURJ (RINV f s) t s 2145 By SURJ_DEF, this is to show: 2146 x IN s ==> ?y. y IN t /\ (RINV f s y = x) 2147 But INJ f s t by BIJ_DEF 2148 so f x IN t by INJ_DEF 2149 and RINV f s (f x) = x by BIJ_RINV_INV 2150 Take y = f x to meet the criteria. 2151*) 2152val BIJ_RINV_BIJ = store_thm( 2153 "BIJ_RINV_BIJ", 2154 ``!(f:'a -> 'b) s t. BIJ f s t /\ (!y. y IN t ==> RINV f s y IN s) ==> BIJ (RINV f s) t s``, 2155 rpt strip_tac >> 2156 rw[BIJ_DEF] >- 2157 metis_tac[INJ_DEF, BIJ_DEF, RINV_DEF] >> 2158 rw[SURJ_DEF] >> 2159 metis_tac[INJ_DEF, BIJ_DEF, BIJ_RINV_INV]); 2160 2161(* Theorem: INJ f t t /\ s SUBSET t ==> !x. x IN s ==> (LINV f t (f x) = x) *) 2162(* Proof: by LINV_DEF, SUBSET_DEF *) 2163val LINV_SUBSET = store_thm( 2164 "LINV_SUBSET", 2165 ``!(f:'a -> 'a) s t. INJ f t t /\ s SUBSET t ==> !x. x IN s ==> (LINV f t (f x) = x)``, 2166 metis_tac[LINV_DEF, SUBSET_DEF]); 2167 2168(* ------------------------------------------------------------------------- *) 2169(* Iteration, Summation and Product *) 2170(* ------------------------------------------------------------------------- *) 2171 2172(* Theorem: ITSET f {x} b = f x b *) 2173(* Proof: 2174 Since FINITE {x} by FINITE_SING 2175 ITSET f {x} b 2176 = ITSET f (REST {x}) (f (CHOICE {x} b) by ITSET_THM 2177 = ITSET f {} (f x b) by CHOICE_SING, REST_SING 2178 = f x b by ITSET_EMPTY 2179*) 2180val ITSET_SING = store_thm( 2181 "ITSET_SING", 2182 ``!f x b. ITSET f {x} b = f x b``, 2183 rw[ITSET_THM]); 2184 2185(* Theorem: FINITE s /\ s <> {} ==> (ITSET f s b = ITSET f (REST s) (f (CHOICE s) b)) *) 2186(* Proof: by ITSET_THM. *) 2187val ITSET_PROPERTY = store_thm( 2188 "ITSET_PROPERTY", 2189 ``!s f b. FINITE s /\ s <> {} ==> (ITSET f s b = ITSET f (REST s) (f (CHOICE s) b))``, 2190 rw[ITSET_THM]); 2191 2192(* Theorem: (f = g) ==> (ITSET f = ITSET g) *) 2193(* Proof: by congruence rule *) 2194val ITSET_CONG = store_thm( 2195 "ITSET_CONG", 2196 ``!f g. (f = g) ==> (ITSET f = ITSET g)``, 2197 rw[]); 2198 2199(* Reduction of ITSET *) 2200 2201(* Theorem: (!x y z. f x (f y z) = f y (f x z)) ==> 2202 !s x b. FINITE s /\ x NOTIN s ==> (ITSET f (x INSERT s) b = f x (ITSET f s b)) *) 2203(* Proof: 2204 Since x NOTIN s ==> s DELETE x = s by DELETE_NON_ELEMENT 2205 The result is true by COMMUTING_ITSET_RECURSES 2206*) 2207val ITSET_REDUCTION = store_thm( 2208 "ITSET_REDUCTION", 2209 ``!f. (!x y z. f x (f y z) = f y (f x z)) ==> 2210 !s x b. FINITE s /\ x NOTIN s ==> (ITSET f (x INSERT s) b = f x (ITSET f s b))``, 2211 rw[COMMUTING_ITSET_RECURSES, DELETE_NON_ELEMENT]); 2212 2213(* ------------------------------------------------------------------------- *) 2214(* Rework of ITSET Theorems *) 2215(* ------------------------------------------------------------------------- *) 2216 2217(* Define a function that gives closure and is commute_associative *) 2218val closure_comm_assoc_fun_def = Define` 2219 closure_comm_assoc_fun f s <=> 2220 (!x y. x IN s /\ y IN s ==> f x y IN s) /\ (* closure *) 2221 (!x y z. x IN s /\ y IN s /\ z IN s ==> (f x (f y z) = f y (f x z))) (* comm_assoc *) 2222`; 2223 2224(* Theorem: FINITE s /\ s SUBSET t /\ closure_comm_assoc_fun f t ==> 2225 !(x b):: t. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b) *) 2226(* Proof: 2227 By complete induction on CARD s. 2228 The goal is to show: 2229 ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b) [1] 2230 Applying ITSET_INSERT to LHS, this is to prove: 2231 ITSET f z (f y b) = ITSET f (s DELETE x) (f x b) 2232 | | 2233 | y = CHOICE (x INSERT s) 2234 +--- z = REST (x INSERT s) 2235 Note y NOTIN z by CHOICE_NOT_IN_REST 2236 If x IN s, 2237 then x INSERT s = s by ABSORPTION 2238 thus y = CHOICE s, z = REST s by x INSERT s = s 2239 2240 If x = y, 2241 Since s = CHOICE s INSERT REST s by CHOICE_INSERT_REST 2242 = y INSERT z by above y, z 2243 Hence z = s DELETE y by DELETE_INSERT 2244 Since CARD z < CARD s, apply induction: 2245 ITSET f (y INSERT z) b = ITSET f (z DELETE y) (f y b) [2a] 2246 For the original goal [1], 2247 LHS = ITSET f (x INSERT s) b 2248 = ITSET f s b by x INSERT s = s 2249 = ITSET f (y INSERT z) b by s = y INSERT z 2250 = ITSET f (z DELETE y) (f y b) by induction hypothesis [2a] 2251 = ITSET f z (f y b) by DELETE_NON_ELEMENT, y NOTIN z 2252 = ITSET f (s DELETE y) (f y b) by z = s DELETE y 2253 = ITSET f (s DELETE x) (f x b) by x = y 2254 = RHS 2255 2256 If x <> y, let u = z DELETE x. 2257 Note REST s = z = x INSERT u by INSERT_DELETE 2258 Now s = x INSERT (y INSERT u) 2259 = x INSERT v, where v = y INSERT u, and x NOTIN z. 2260 Therefore (s DELETE x) = v by DELETE_INSERT 2261 Since CARD v < CARD s, apply induction: 2262 ITSET f (x INSERT v) b = ITSET f (v DELETE x) (f x b) [2b] 2263 For the original goal [1], 2264 LHS = ITSET f (x INSERT s) b 2265 = ITSET f s b by x INSERT s = s 2266 = ITSET f (x INSERT v) b by s = x INSERT v 2267 = ITSET f (v DELETE x) (f x b) by induction hypothesis [2b] 2268 = ITSET f v (f x b) by x NOTIN v 2269 = ITSET f (s DELETE x) (f x b) by v = s DELETE x 2270 = RHS 2271 2272 If x NOTIN s, 2273 then s DELETE x = x by DELETE_NON_ELEMENT 2274 To prove: ITSET f (x INSERT s) b = ITSET f s (f x b) by [1] 2275 The CHOICE/REST of (x INSERT s) cannot be simplified, but can be replaced by: 2276 Note (x INSERT s) <> {} by NOT_EMPTY_INSERT 2277 y INSERT z 2278 = CHOICE (x INSERT s) INSERT (REST (x INSERT s)) by y = CHOICE (x INSERT s), z = REST (x INSERT s) 2279 = x INSERT s by CHOICE_INSERT_REST 2280 2281 If y = x, 2282 Then z = s by DELETE_INSERT, y INSERT z = x INSERT s, y = x. 2283 because s = s DELETE x by DELETE_NON_ELEMENT, x NOTIN s. 2284 = (x INSERT s) DELETE x by DELETE_INSERT 2285 = (y INSERT z) DELETE x by above 2286 = (y INSERT z) DELETE y by y = x 2287 = z DELETE y by DELETE_INSERT 2288 = z by DELETE_NON_ELEMENT, y NOTIN z. 2289 For the modified goal [1], 2290 LHS = ITSET f (x INSERT s) b 2291 = ITSET f (REST (x INSERT s)) (f (CHOICE (x INSERT s)) b) by ITSET_PROPERTY 2292 = ITSET f z (f y b) by y = CHOICE (x INSERT s), z = REST (x INSERT s) 2293 = ITSET f s (f x b) by z = s, y = x 2294 = RHS 2295 2296 If y <> x, 2297 Then x IN z and y IN s by IN_INSERT, x INSERT s = y INSERT z and x <> y. 2298 and s = y INSERT (s DELETE y) by INSERT_DELETE, y IN s 2299 = y INSERT u where u = s DELETE y 2300 Then y NOTIN u by IN_DELETE 2301 and z = x INSERT u, 2302 because x INSERT u 2303 = x INSERT (s DELETE y) by u = s DELETE y 2304 = (x INSERT s) DELETE y by DELETE_INSERT, x <> y 2305 = (y INSERT z) DELETE y by x INSERT s = y INSERT z 2306 = z by INSERT_DELETE 2307 and x NOTIN u by IN_DELETE, u = s DELETE y, but x NOTIN s. 2308 Thus CARD u < CARD s by CARD_INSERT, s = y INSERT u. 2309 Apply induction: 2310 !x b. ITSET f (x INSERT u) b = ITSET f (u DELETE x) (f x b) [2c] 2311 2312 For the modified goal [1], 2313 LHS = ITSET f (x INSERT s) b 2314 = ITSET f (REST (x INSERT s)) (f (CHOICE (x INSERT s)) b) by ITSET_PROPERTY 2315 = ITSET f z (f y b) by z = REST (x INSERT s), y = CHOICE (x INSERT s) 2316 = ITSET f (x INSERT u) (f y b) by z = x INSERT u 2317 = ITSET f (u DELETE x) (f x (f y b)) by induction hypothesis, [2c] 2318 = ITSET f u (f x (f y b)) by x NOTIN u 2319 RHS = ITSET f s (f x b) 2320 = ITSET f (y INSERT u) (f x b) by s = y INSERT u 2321 = ITSET f (u DELETE y) (f y (f x b)) by induction hypothesis, [2c] 2322 = ITSET f u (f y (f x b)) by y NOTIN u 2323 Applying the commute_associativity of f, LHS = RHS. 2324*) 2325Theorem SUBSET_COMMUTING_ITSET_INSERT: 2326 !f s t. FINITE s /\ s SUBSET t /\ closure_comm_assoc_fun f t ==> 2327 !(x b)::t. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b) 2328Proof 2329 completeInduct_on `CARD s` >> 2330 rule_assum_tac(SIMP_RULE bool_ss[GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO]) >> 2331 rw[RES_FORALL_THM] >> 2332 rw[ITSET_INSERT] >> 2333 qabbrev_tac `y = CHOICE (x INSERT s)` >> 2334 qabbrev_tac `z = REST (x INSERT s)` >> 2335 `y NOTIN z` by metis_tac[CHOICE_NOT_IN_REST] >> 2336 `!x s. x IN s ==> (x INSERT s = s)` by rw[ABSORPTION] >> 2337 `!x s. x NOTIN s ==> (s DELETE x = s)` by rw[DELETE_NON_ELEMENT] >> 2338 Cases_on `x IN s` >| [ 2339 `s = y INSERT z` by metis_tac[NOT_IN_EMPTY, CHOICE_INSERT_REST] >> 2340 `FINITE z` by metis_tac[REST_SUBSET, SUBSET_FINITE] >> 2341 `CARD s = SUC (CARD z)` by rw[] >> 2342 `CARD z < CARD s` by decide_tac >> 2343 `z = s DELETE y` by metis_tac[DELETE_INSERT] >> 2344 `z SUBSET t` by metis_tac[DELETE_SUBSET, SUBSET_TRANS] >> 2345 Cases_on `x = y` >- metis_tac[] >> 2346 `x IN z` by metis_tac[IN_INSERT] >> 2347 qabbrev_tac `u = z DELETE x` >> 2348 `z = x INSERT u` by rw[INSERT_DELETE, Abbr`u`] >> 2349 `x NOTIN u` by metis_tac[IN_DELETE] >> 2350 qabbrev_tac `v = y INSERT u` >> 2351 `s = x INSERT v` by simp[INSERT_COMM, Abbr `v`] >> 2352 `x NOTIN v` by rw[Abbr `v`] >> 2353 `FINITE v` by metis_tac[FINITE_INSERT] >> 2354 `CARD s = SUC (CARD v)` by metis_tac[CARD_INSERT] >> 2355 `CARD v < CARD s` by decide_tac >> 2356 `v SUBSET t` by metis_tac[INSERT_SUBSET, SUBSET_TRANS] >> 2357 `s DELETE x = v` by rw[DELETE_INSERT, Abbr `v`] >> 2358 `v = s DELETE x` by rw[] >> 2359 `y IN t` by metis_tac[NOT_INSERT_EMPTY, CHOICE_DEF, SUBSET_DEF] >> 2360 metis_tac[], 2361 `x INSERT s <> {}` by rw[] >> 2362 `y INSERT z = x INSERT s` by rw[CHOICE_INSERT_REST, Abbr`y`, Abbr`z`] >> 2363 Cases_on `x = y` >- metis_tac[DELETE_INSERT, ITSET_PROPERTY] >> 2364 `x IN z /\ y IN s` by metis_tac[IN_INSERT] >> 2365 qabbrev_tac `u = s DELETE y` >> 2366 `s = y INSERT u` by rw[INSERT_DELETE, Abbr`u`] >> 2367 `y NOTIN u` by metis_tac[IN_DELETE] >> 2368 `z = x INSERT u` by metis_tac[DELETE_INSERT, INSERT_DELETE] >> 2369 `x NOTIN u` by metis_tac[IN_DELETE] >> 2370 `FINITE u` by metis_tac[FINITE_DELETE, SUBSET_FINITE] >> 2371 `CARD u < CARD s` by rw[] >> 2372 `u SUBSET t` by metis_tac[DELETE_SUBSET, SUBSET_TRANS] >> 2373 `y IN t` by metis_tac[CHOICE_DEF, SUBSET_DEF] >> 2374 `f y b IN t /\ f x b IN t` by prove_tac[closure_comm_assoc_fun_def] >> 2375 `ITSET f z (f y b) = ITSET f (x INSERT u) (f y b)` by rw[] >> 2376 `_ = ITSET f (u DELETE x) (f x (f y b))` by metis_tac[] >> 2377 `_ = ITSET f u (f x (f y b))` by rw[] >> 2378 `ITSET f s (f x b) = ITSET f (y INSERT u) (f x b)` by rw[] >> 2379 `_ = ITSET f (u DELETE y) (f y (f x b))` by metis_tac[] >> 2380 `_ = ITSET f u (f y (f x b))` by rw[] >> 2381 `f x (f y b) = f y (f x b)` by prove_tac[closure_comm_assoc_fun_def] >> 2382 metis_tac[] 2383 ] 2384QED 2385 2386(* This is a generalisation of COMMUTING_ITSET_INSERT, removing the requirement of commuting everywhere. *) 2387 2388(* Theorem: FINITE s /\ s SUBSET t /\ closure_comm_assoc_fun f t ==> 2389 !(x b)::t. ITSET f s (f x b) = f x (ITSET f s b) *) 2390(* Proof: 2391 By complete induction on CARD s. 2392 The goal is to show: ITSET f s (f x b) = f x (ITSET f s b) 2393 Base: s = {}, 2394 LHS = ITSET f {} (f x b) 2395 = f x b by ITSET_EMPTY 2396 = f x (ITSET f {} b) by ITSET_EMPTY 2397 = RHS 2398 Step: s <> {}, 2399 Let s = y INSERT z, where y = CHOICE s, z = REST s. 2400 Then y NOTIN z by CHOICE_NOT_IN_REST 2401 But y IN t by CHOICE_DEF, SUBSET_DEF 2402 and z SUBSET t by REST_SUBSET, SUBSET_TRANS 2403 Also FINITE z by REST_SUBSET, SUBSET_FINITE 2404 Thus CARD s = SUC (CARD z) by CARD_INSERT 2405 or CARD z < CARD s 2406 Note f x b IN t /\ f y b IN t by closure_comm_assoc_fun_def 2407 2408 LHS = ITSET f s (f x b) 2409 = ITSET f (y INSERT z) (f x b) by s = y INSERT z 2410 = ITSET f (z DELETE y) (f y (f x b)) by SUBSET_COMMUTING_ITSET_INSERT, y, f x b IN t 2411 = ITSET f z (f y (f x b)) by DELETE_NON_ELEMENT, y NOTIN z 2412 = ITSET f z (f x (f y b)) by closure_comm_assoc_fun_def, x, y, b IN t 2413 = f x (ITSET f z (f y b)) by inductive hypothesis, CARD z < CARD s, x, f y b IN t 2414 = f x (ITSET f (z DELETE y) (f y b)) by DELETE_NON_ELEMENT, y NOTIN z 2415 = f x (ITSET f (y INSERT z) b) by SUBSET_COMMUTING_ITSET_INSERT, y, f y b IN t 2416 = f x (ITSET f s b) by s = y INSERT z 2417 = RHS 2418*) 2419val SUBSET_COMMUTING_ITSET_REDUCTION = store_thm( 2420 "SUBSET_COMMUTING_ITSET_REDUCTION", 2421 ``!f s t. FINITE s /\ s SUBSET t /\ closure_comm_assoc_fun f t ==> 2422 !(x b)::t. ITSET f s (f x b) = f x (ITSET f s b)``, 2423 completeInduct_on `CARD s` >> 2424 rule_assum_tac(SIMP_RULE bool_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO]) >> 2425 rw[RES_FORALL_THM] >> 2426 Cases_on `s = {}` >- 2427 rw[ITSET_EMPTY] >> 2428 `?y z. (y = CHOICE s) /\ (z = REST s) /\ (s = y INSERT z)` by rw[CHOICE_INSERT_REST] >> 2429 `y NOTIN z` by metis_tac[CHOICE_NOT_IN_REST] >> 2430 `y IN t` by metis_tac[CHOICE_DEF, SUBSET_DEF] >> 2431 `z SUBSET t` by metis_tac[REST_SUBSET, SUBSET_TRANS] >> 2432 `FINITE z` by metis_tac[REST_SUBSET, SUBSET_FINITE] >> 2433 `CARD s = SUC (CARD z)` by rw[] >> 2434 `CARD z < CARD s` by decide_tac >> 2435 `f x b IN t /\ f y b IN t /\ (f y (f x b) = f x (f y b))` by prove_tac[closure_comm_assoc_fun_def] >> 2436 metis_tac[SUBSET_COMMUTING_ITSET_INSERT, DELETE_NON_ELEMENT]); 2437 2438(* This helps to prove the next generalisation. *) 2439 2440(* Theorem: FINITE s /\ s SUBSET t /\ closure_comm_assoc_fun f t ==> 2441 !(x b):: t. ITSET f (x INSERT s) b = f x (ITSET f (s DELETE x) b) *) 2442(* Proof: 2443 Note (s DELETE x) SUBSET t by DELETE_SUBSET, SUBSET_TRANS 2444 and FINITE (s DELETE x) by FINITE_DELETE, FINITE s 2445 ITSET f (x INSERT s) b 2446 = ITSET f (s DELETE x) (f x b) by SUBSET_COMMUTING_ITSET_INSERT 2447 = f x (ITSET f (s DELETE x) b) by SUBSET_COMMUTING_ITSET_REDUCTION, (s DELETE x) SUBSET t 2448*) 2449val SUBSET_COMMUTING_ITSET_RECURSES = store_thm( 2450 "SUBSET_COMMUTING_ITSET_RECURSES", 2451 ``!f s t. FINITE s /\ s SUBSET t /\ closure_comm_assoc_fun f t ==> 2452 !(x b):: t. ITSET f (x INSERT s) b = f x (ITSET f (s DELETE x) b)``, 2453 rw[RES_FORALL_THM] >> 2454 `(s DELETE x) SUBSET t` by metis_tac[DELETE_SUBSET, SUBSET_TRANS] >> 2455 `FINITE (s DELETE x)` by rw[] >> 2456 metis_tac[SUBSET_COMMUTING_ITSET_INSERT, SUBSET_COMMUTING_ITSET_REDUCTION]); 2457 2458(* ------------------------------------------------------------------------- *) 2459(* SUM_IMAGE and PROD_IMAGE Theorems *) 2460(* ------------------------------------------------------------------------- *) 2461 2462(* Theorem: SIGMA f {} = 0 *) 2463(* Proof: by SUM_IMAGE_THM *) 2464val SUM_IMAGE_EMPTY = store_thm( 2465 "SUM_IMAGE_EMPTY", 2466 ``!f. SIGMA f {} = 0``, 2467 rw[SUM_IMAGE_THM]); 2468 2469(* Theorem: FINITE s ==> !e. e NOTIN s ==> (SIGMA f (e INSERT s) = f e + (SIGMA f s)) *) 2470(* Proof: 2471 SIGMA f (e INSERT s) 2472 = f e + SIGMA f (s DELETE e) by SUM_IMAGE_THM 2473 = f e + SIGMA f s by DELETE_NON_ELEMENT 2474*) 2475val SUM_IMAGE_INSERT = store_thm( 2476 "SUM_IMAGE_INSERT", 2477 ``!f s. FINITE s ==> !e. e NOTIN s ==> (SIGMA f (e INSERT s) = f e + (SIGMA f s))``, 2478 rw[SUM_IMAGE_THM, DELETE_NON_ELEMENT]); 2479 2480(* Theorem: FINITE s ==> !f. (!x y. (f x = f y) ==> (x = y)) ==> (SIGMA f s = SIGMA I (IMAGE f s)) *) 2481(* Proof: 2482 By finite induction on s. 2483 Base case: SIGMA f {} = SIGMA I {} 2484 SIGMA f {} 2485 = 0 by SUM_IMAGE_THM 2486 = SIGMA I {} by SUM_IMAGE_THM 2487 = SUM_SET {} by SUM_SET_DEF 2488 Step case: !f. (!x y. (f x = f y) ==> (x = y)) ==> (SIGMA f s = SUM_SET (IMAGE f s)) ==> 2489 e NOTIN s ==> SIGMA f (e INSERT s) = SUM_SET (f e INSERT IMAGE f s) 2490 Note FINITE s ==> FINITE (IMAGE f s) by IMAGE_FINITE 2491 and e NOTIN s ==> f e NOTIN f s by the injective property 2492 SIGMA f (e INSERT s) 2493 = f e + SIGMA f (s DELETE e)) by SUM_IMAGE_THM 2494 = f e + SIGMA f s by DELETE_NON_ELEMENT 2495 = f e + SUM_SET (IMAGE f s)) by induction hypothesis 2496 = f e + SUM_SET ((IMAGE f s) DELETE (f e)) by DELETE_NON_ELEMENT, f e NOTIN f s 2497 = SUM_SET (f e INSERT IMAGE f s) by SUM_SET_THM 2498*) 2499val SUM_IMAGE_AS_SUM_SET = store_thm( 2500 "SUM_IMAGE_AS_SUM_SET", 2501 ``!s. FINITE s ==> !f. (!x y. (f x = f y) ==> (x = y)) ==> (SIGMA f s = SUM_SET (IMAGE f s))``, 2502 HO_MATCH_MP_TAC FINITE_INDUCT >> 2503 rw[SUM_SET_DEF] >- 2504 rw[SUM_IMAGE_THM] >> 2505 rw[SUM_IMAGE_THM, SUM_IMAGE_DELETE] >> 2506 metis_tac[]); 2507 2508(* Theorem: FINITE s ==> !f k. (!x. x IN s ==> (f x = k)) ==> (SIGMA f s = k * CARD s) *) 2509(* Proof: 2510 By finite induction on s. 2511 Base: SIGMA f {} = k * CARD {} 2512 SIGMA f {} 2513 = 0 by SUM_IMAGE_EMPTY 2514 = k * 0 by MULT_0 2515 = k * CARD {} by CARD_EMPTY 2516 Step: SIGMA f s = k * CARD s /\ e NOTIN s /\ !x. x IN e INSERT s /\ f x = k ==> 2517 SIGMA f (e INSERT s) = k * CARD (e INSERT s) 2518 Note f e = k /\ !x. x IN s ==> f x = k by IN_INSERT 2519 SIGMA f (e INSERT s) 2520 = f e + SIGMA f (s DELETE e) by SUM_IMAGE_THM 2521 = k + SIGMA f s by DELETE_NON_ELEMENT, f e = k 2522 = k + k * CARD s by induction hypothesis 2523 = k * (1 + CARD s) by LEFT_ADD_DISTRIB 2524 = k * SUC (CARD s) by SUC_ONE_ADD 2525 = k * CARD (e INSERT s) by CARD_INSERT 2526*) 2527val SIGMA_CONSTANT = store_thm( 2528 "SIGMA_CONSTANT", 2529 ``!s. FINITE s ==> !f k. (!x. x IN s ==> (f x = k)) ==> (SIGMA f s = k * CARD s)``, 2530 ho_match_mp_tac FINITE_INDUCT >> 2531 rpt strip_tac >- 2532 rw[SUM_IMAGE_EMPTY] >> 2533 `(f e = k) /\ !x. x IN s ==> (f x = k)` by rw[] >> 2534 `SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e)` by rw[SUM_IMAGE_THM] >> 2535 `_ = k + SIGMA f s` by metis_tac[DELETE_NON_ELEMENT] >> 2536 `_ = k + k * CARD s` by rw[] >> 2537 `_ = k * (1 + CARD s)` by rw[] >> 2538 `_ = k * SUC (CARD s)` by rw[ADD1] >> 2539 `_ = k * CARD (e INSERT s)` by rw[CARD_INSERT] >> 2540 rw[]); 2541 2542(* Theorem: FINITE s ==> !c. SIGMA (K c) s = c * CARD s *) 2543(* Proof: by SIGMA_CONSTANT. *) 2544val SUM_IMAGE_CONSTANT = store_thm( 2545 "SUM_IMAGE_CONSTANT", 2546 ``!s. FINITE s ==> !c. SIGMA (K c) s = c * CARD s``, 2547 rw[SIGMA_CONSTANT]); 2548 2549(* Theorem: If !e. e IN s, CARD e = n, SIGMA CARD s = n * CARD s. *) 2550(* Proof: 2551 By finite induction on set s. 2552 Base: SIGMA CARD {} = 0 2553 True by SUM_IMAGE_THM. 2554 Step: (!e. e IN s ==> (CARD e = n)) ==> (SIGMA CARD s = n * CARD s) ==> 2555 e NOTIN s /\ !e'. (e' = e) \/ e' IN s ==> (CARD e' = n) ==> SIGMA CARD (e INSERT s) = n * SUC (CARD s) 2556 Note CARD e = n. 2557 SIGMA CARD (e INSERT s) 2558 = CARD e + SIGMA CARD (s DELETE e) by SUM_IMAGE_THM 2559 = CARD e + SIGMA CARD s by DELETE_NON_ELEMENT 2560 = CARD e + n * CARD s by induction hypothesis 2561 = n + n * CARD s by above, CARD e = n 2562 = n * (1 + CARD s) by RIGHT_ADD_DISTRIB 2563 = n * SUC (CARD s) by arithmetic 2564 Or, 2565 directly by SIGMA_CONSTANT. 2566*) 2567val SIGMA_CARD_CONSTANT = store_thm( 2568 "SIGMA_CARD_CONSTANT", 2569 ``!n s. FINITE s ==> (!e. e IN s ==> (CARD e = n)) ==> (SIGMA CARD s = n * (CARD s))``, 2570 rw[SIGMA_CONSTANT]); 2571 2572(* Theorem: If n divides CARD e for all e in s, then n divides SIGMA CARD s. 2573 FINITE s ==> (!e. e IN s ==> n divides (CARD e)) ==> n divides (SIGMA CARD s) *) 2574(* Proof: 2575 Use finite induction and SUM_IMAGE_THM. 2576 Base: n divides SIGMA CARD {} 2577 Note SIGMA CARD {} = 0 by SUM_IMAGE_THM 2578 and n divides 0 by ALL_DIVIDES_0 2579 Step: e NOTIN s /\ n divides (CARD e) ==> n divides SIGMA CARD (e INSERT s) 2580 SIGMA CARD (e INSERT s) 2581 = CARD e + SIGMA CARD (s DELETE e) by SUM_IMAGE_THM 2582 = CARD e + SIGMA CARD s by DELETE_NON_ELEMENT 2583 Note n divides (CARD e) by given 2584 and n divides SIGMA CARD s by induction hypothesis 2585 Thus n divides SIGMA CARD (e INSERT s) by DIVIDES_ADD_1 2586*) 2587val SIGMA_CARD_FACTOR = store_thm( 2588 "SIGMA_CARD_FACTOR", 2589 ``!n s. FINITE s ==> (!e. e IN s ==> n divides (CARD e)) ==> n divides (SIGMA CARD s)``, 2590 strip_tac >> 2591 Induct_on `FINITE` >> 2592 rw[] >- 2593 rw[SUM_IMAGE_THM] >> 2594 metis_tac[SUM_IMAGE_THM, DELETE_NON_ELEMENT, DIVIDES_ADD_1]); 2595 2596(* Theorem: (!x. x IN s ==> (f1 x = f2 x)) ==> (SIGMA f1 s = SIGMA f2 s) *) 2597val SIGMA_CONG = store_thm( 2598 "SIGMA_CONG", 2599 ``!s f1 f2. (!x. x IN s ==> (f1 x = f2 x)) ==> (SIGMA f1 s = SIGMA f2 s)``, 2600 rw[SUM_IMAGE_CONG]); 2601 2602(* Theorem: FINITE s ==> (CARD s = SIGMA (\x. 1) s) *) 2603(* Proof: 2604 By finite induction: 2605 Base case: CARD {} = SIGMA (\x. 1) {} 2606 LHS = CARD {} 2607 = 0 by CARD_EMPTY 2608 RHS = SIGMA (\x. 1) {} 2609 = 0 = LHS by SUM_IMAGE_THM 2610 Step case: (CARD s = SIGMA (\x. 1) s) ==> 2611 !e. e NOTIN s ==> (CARD (e INSERT s) = SIGMA (\x. 1) (e INSERT s)) 2612 CARD (e INSERT s) 2613 = SUC (CARD s) by CARD_DEF 2614 = SUC (SIGMA (\x. 1) s) by induction hypothesis 2615 = 1 + SIGMA (\x. 1) s by ADD1, ADD_COMM 2616 = (\x. 1) e + SIGMA (\x. 1) s by function application 2617 = (\x. 1) e + SIGMA (\x. 1) (s DELETE e) by DELETE_NON_ELEMENT 2618 = SIGMA (\x. 1) (e INSERT s) by SUM_IMAGE_THM 2619*) 2620val CARD_AS_SIGMA = store_thm( 2621 "CARD_AS_SIGMA", 2622 ``!s. FINITE s ==> (CARD s = SIGMA (\x. 1) s)``, 2623 ho_match_mp_tac FINITE_INDUCT >> 2624 conj_tac >- 2625 rw[SUM_IMAGE_THM] >> 2626 rpt strip_tac >> 2627 `CARD (e INSERT s) = SUC (SIGMA (\x. 1) s)` by rw[] >> 2628 `_ = 1 + SIGMA (\x. 1) s` by rw_tac std_ss[ADD1, ADD_COMM] >> 2629 `_ = (\x. 1) e + SIGMA (\x. 1) s` by rw[] >> 2630 `_ = (\x. 1) e + SIGMA (\x. 1) (s DELETE e)` by metis_tac[DELETE_NON_ELEMENT] >> 2631 `_ = SIGMA (\x. 1) (e INSERT s)` by rw[SUM_IMAGE_THM] >> 2632 decide_tac); 2633 2634(* Theorem: FINITE s ==> (CARD s = SIGMA (K 1) s) *) 2635(* Proof: by CARD_AS_SIGMA, SIGMA_CONG *) 2636val CARD_EQ_SIGMA = store_thm( 2637 "CARD_EQ_SIGMA", 2638 ``!s. FINITE s ==> (CARD s = SIGMA (K 1) s)``, 2639 rw[CARD_AS_SIGMA, SIGMA_CONG]); 2640 2641(* Theorem: FINITE s ==> !f g. (!x. x IN s ==> f x <= g x) ==> (SIGMA f s <= SIGMA g s) *) 2642(* Proof: 2643 By finite induction: 2644 Base case: !f g. (!x. x IN {} ==> f x <= g x) ==> SIGMA f {} <= SIGMA g {} 2645 True since SIGMA f {} = 0 by SUM_IMAGE_THM 2646 Step case: !f g. (!x. x IN s ==> f x <= g x) ==> SIGMA f s <= SIGMA g s ==> 2647 e NOTIN s ==> 2648 !x. x IN e INSERT s ==> f x <= g x ==> !f g. SIGMA f (e INSERT s) <= SIGMA g (e INSERT s) 2649 SIGMA f (e INSERT s) <= SIGMA g (e INSERT s) 2650 means f e + SIGMA f (s DELETE e) <= g e + SIGMA g (s DELETE e) by SUM_IMAGE_THM 2651 or f e + SIGMA f s <= g e + SIGMA g s by DELETE_NON_ELEMENT 2652 Now, x IN e INSERT s ==> (x = e) or (x IN s) by IN_INSERT 2653 Therefore f e <= g e, and !x IN s, f x <= g x by x IN (e INSERT s) implication 2654 or f e <= g e, and SIGMA f s <= SIGMA g s by induction hypothesis 2655 Hence f e + SIGMA f s <= g e + SIGMA g s by arithmetic 2656*) 2657val SIGMA_LE_SIGMA = store_thm( 2658 "SIGMA_LE_SIGMA", 2659 ``!s. FINITE s ==> !f g. (!x. x IN s ==> f x <= g x) ==> (SIGMA f s <= SIGMA g s)``, 2660 ho_match_mp_tac FINITE_INDUCT >> 2661 conj_tac >- 2662 rw[SUM_IMAGE_THM] >> 2663 rw[SUM_IMAGE_THM, DELETE_NON_ELEMENT] >> 2664 `f e <= g e /\ SIGMA f s <= SIGMA g s` by rw[] >> 2665 decide_tac); 2666 2667(* Theorem: FINITE s /\ FINITE t ==> !f. SIGMA f (s UNION t) + SIGMA f (s INTER t) = SIGMA f s + SIGMA f t *) 2668(* Proof: 2669 Note SIGMA f (s UNION t) 2670 = SIGMA f s + SIGMA f t - SIGMA f (s INTER t) by SUM_IMAGE_UNION 2671 now s INTER t SUBSET s /\ s INTER t SUBSET t by INTER_SUBSET 2672 so SIGMA f (s INTER t) <= SIGMA f s by SUM_IMAGE_SUBSET_LE 2673 and SIGMA f (s INTER t) <= SIGMA f t by SUM_IMAGE_SUBSET_LE 2674 thus SIGMA f (s INTER t) <= SIGMA f s + SIGMA f t by arithmetic 2675 The result follows by ADD_EQ_SUB 2676*) 2677val SUM_IMAGE_UNION_EQN = store_thm( 2678 "SUM_IMAGE_UNION_EQN", 2679 ``!s t. FINITE s /\ FINITE t ==> !f. SIGMA f (s UNION t) + SIGMA f (s INTER t) = SIGMA f s + SIGMA f t``, 2680 rpt strip_tac >> 2681 `SIGMA f (s UNION t) = SIGMA f s + SIGMA f t - SIGMA f (s INTER t)` by rw[SUM_IMAGE_UNION] >> 2682 `SIGMA f (s INTER t) <= SIGMA f s` by rw[SUM_IMAGE_SUBSET_LE, INTER_SUBSET] >> 2683 `SIGMA f (s INTER t) <= SIGMA f t` by rw[SUM_IMAGE_SUBSET_LE, INTER_SUBSET] >> 2684 `SIGMA f (s INTER t) <= SIGMA f s + SIGMA f t` by decide_tac >> 2685 rw[ADD_EQ_SUB]); 2686 2687(* Theorem: FINITE s /\ FINITE t /\ DISJOINT s t ==> !f. SIGMA f (s UNION t) = SIGMA f s + SIGMA f t *) 2688(* Proof: 2689 SIGMA f (s UNION t) 2690 = SIGMA f s + SIGMA f t - SIGMA f (s INTER t) by SUM_IMAGE_UNION 2691 = SIGMA f s + SIGMA f t - SIGMA f {} by DISJOINT_DEF 2692 = SIGMA f s + SIGMA f t - 0 by SUM_IMAGE_EMPTY 2693 = SIGMA f s + SIGMA f t by arithmetic 2694*) 2695val SUM_IMAGE_DISJOINT = store_thm( 2696 "SUM_IMAGE_DISJOINT", 2697 ``!s t. FINITE s /\ FINITE t /\ DISJOINT s t ==> !f. SIGMA f (s UNION t) = SIGMA f s + SIGMA f t``, 2698 rw_tac std_ss[SUM_IMAGE_UNION, DISJOINT_DEF, SUM_IMAGE_EMPTY]); 2699 2700(* Theorem: FINITE s /\ s <> {} ==> !f g. (!x. x IN s ==> f x < g x) ==> SIGMA f s < SIGMA g s *) 2701(* Proof: 2702 Note s <> {} ==> ?x. x IN s by MEMBER_NOT_EMPTY 2703 Thus ?x. x IN s /\ f x < g x by implication 2704 and !x. x IN s ==> f x <= g x by LESS_IMP_LESS_OR_EQ 2705 ==> SIGMA f s < SIGMA g s by SUM_IMAGE_MONO_LESS 2706*) 2707val SUM_IMAGE_MONO_LT = store_thm( 2708 "SUM_IMAGE_MONO_LT", 2709 ``!s. FINITE s /\ s <> {} ==> !f g. (!x. x IN s ==> f x < g x) ==> SIGMA f s < SIGMA g s``, 2710 metis_tac[SUM_IMAGE_MONO_LESS, LESS_IMP_LESS_OR_EQ, MEMBER_NOT_EMPTY]); 2711 2712(* Theorem: FINITE s /\ t PSUBSET s /\ (!x. x IN s ==> f x <> 0) ==> SIGMA f t < SIGMA f s *) 2713(* Proof: 2714 Note t SUBSET s /\ t <> s by PSUBSET_DEF 2715 Thus SIGMA f t <= SIGMA f s by SUM_IMAGE_SUBSET_LE 2716 By contradiction, suppose ~(SIGMA f t < SIGMA f s). 2717 Then SIGMA f t = SIGMA f s by arithmetic [1] 2718 2719 Let u = s DIFF t. 2720 Then DISJOINT u t by DISJOINT_DIFF 2721 and u UNION t = s by UNION_DIFF 2722 Note FINITE u /\ FINITE t by FINITE_UNION 2723 ==> SIGMA f s = SIGMA f u + SIGMA f t by SUM_IMAGE_DISJOINT 2724 Thus SIGMA f u = 0 by arithmetic, [1] 2725 2726 Now u SUBSET s by SUBSET_UNION 2727 and u <> {} by finite_partition_property, t <> s 2728 Thus ?x. x IN u by MEMBER_NOT_EMPTY 2729 and f x <> 0 by SUBSET_DEF, implication 2730 This contradicts f x = 0 by SUM_IMAGE_ZERO 2731*) 2732val SUM_IMAGE_PSUBSET_LT = store_thm( 2733 "SUM_IMAGE_PSUBSET_LT", 2734 ``!f s t. FINITE s /\ t PSUBSET s /\ (!x. x IN s ==> f x <> 0) ==> SIGMA f t < SIGMA f s``, 2735 rw[PSUBSET_DEF] >> 2736 `SIGMA f t <= SIGMA f s` by rw[SUM_IMAGE_SUBSET_LE] >> 2737 spose_not_then strip_assume_tac >> 2738 `SIGMA f t = SIGMA f s` by decide_tac >> 2739 qabbrev_tac `u = s DIFF t` >> 2740 `DISJOINT u t` by rw[DISJOINT_DIFF, Abbr`u`] >> 2741 `u UNION t = s` by rw[UNION_DIFF, Abbr`u`] >> 2742 `FINITE u /\ FINITE t` by metis_tac[FINITE_UNION] >> 2743 `SIGMA f s = SIGMA f u + SIGMA f t` by rw[GSYM SUM_IMAGE_DISJOINT] >> 2744 `SIGMA f u = 0` by decide_tac >> 2745 `u SUBSET s` by rw[] >> 2746 `u <> {}` by metis_tac[finite_partition_property] >> 2747 metis_tac[SUM_IMAGE_ZERO, SUBSET_DEF, MEMBER_NOT_EMPTY]); 2748 2749 2750(* Theorem: PI f {} = 1 *) 2751(* Proof: by PROD_IMAGE_THM *) 2752val PROD_IMAGE_EMPTY = store_thm( 2753 "PROD_IMAGE_EMPTY", 2754 ``!f. PI f {} = 1``, 2755 rw[PROD_IMAGE_THM]); 2756 2757(* Theorem: FINITE s ==> !f e. e NOTIN s ==> (PI f (e INSERT s) = (f e) * PI f s) *) 2758(* Proof: by PROD_IMAGE_THM, DELETE_NON_ELEMENT *) 2759val PROD_IMAGE_INSERT = store_thm( 2760 "PROD_IMAGE_INSERT", 2761 ``!s. FINITE s ==> !f e. e NOTIN s ==> (PI f (e INSERT s) = (f e) * PI f s)``, 2762 rw[PROD_IMAGE_THM, DELETE_NON_ELEMENT]); 2763 2764(* Theorem: FINITE s ==> !f e. 0 < f e ==> 2765 (PI f (s DELETE e) = if e IN s then ((PI f s) DIV (f e)) else PI f s) *) 2766(* Proof: 2767 If e IN s, 2768 Note PI f (e INSERT s) = (f e) * PI f (s DELETE e) by PROD_IMAGE_THM 2769 Thus PI f (s DELETE e) = PI f (e INSERT s) DIV (f e) by DIV_SOLVE_COMM, 0 < f e 2770 = (PI f s) DIV (f e) by ABSORPTION, e IN s. 2771 If e NOTIN s, 2772 PI f (s DELETE e) = PI f e by DELETE_NON_ELEMENT 2773*) 2774val PROD_IMAGE_DELETE = store_thm( 2775 "PROD_IMAGE_DELETE", 2776 ``!s. FINITE s ==> !f e. 0 < f e ==> 2777 (PI f (s DELETE e) = if e IN s then ((PI f s) DIV (f e)) else PI f s)``, 2778 rpt strip_tac >> 2779 rw_tac std_ss[] >- 2780 metis_tac[PROD_IMAGE_THM, DIV_SOLVE_COMM, ABSORPTION] >> 2781 metis_tac[DELETE_NON_ELEMENT]); 2782(* The original proof of SUM_IMAGE_DELETE is clumsy. *) 2783 2784(* Theorem: (!x. x IN s ==> (f1 x = f2 x)) ==> (PI f1 s = PI f2 s) *) 2785(* Proof: 2786 If INFINITE s, 2787 PI f1 s 2788 = ITSET (\e acc. f e * acc) s 1 by PROD_IMAGE_DEF 2789 = ARB by ITSET_def 2790 Similarly, PI f2 s = ARB = PI f1 s. 2791 If FINITE s, 2792 Apply finite induction on s. 2793 Base: PI f1 {} = PI f2 {}, true by PROD_IMAGE_EMPTY 2794 Step: !f1 f2. (!x. x IN s ==> (f1 x = f2 x)) ==> (PI f1 s = PI f2 s) ==> 2795 e NOTIN s /\ !x. x IN e INSERT s ==> (f1 x = f2 x) ==> PI f1 (e INSERT s) = PI f2 (e INSERT s) 2796 Note !x. x IN e INSERT s ==> (f1 x = f2 x) 2797 ==> (f1 e = f2 e) \/ !x. s IN s ==> (f1 x = f2 x) by IN_INSERT 2798 PI f1 (e INSERT s) 2799 = (f1 e) * (PI f1 s) by PROD_IMAGE_INSERT, e NOTIN s 2800 = (f1 e) * (PI f2 s) by induction hypothesis 2801 = (f2 e) * (PI f2 s) by f1 e = f2 e 2802 = PI f2 (e INSERT s) by PROD_IMAGE_INSERT, e NOTIN s 2803*) 2804val PROD_IMAGE_CONG = store_thm( 2805 "PROD_IMAGE_CONG", 2806 ``!s f1 f2. (!x. x IN s ==> (f1 x = f2 x)) ==> (PI f1 s = PI f2 s)``, 2807 rpt strip_tac >> 2808 reverse (Cases_on `FINITE s`) >| [ 2809 rw[PROD_IMAGE_DEF, Once ITSET_def] >> 2810 rw[Once ITSET_def], 2811 pop_assum mp_tac >> 2812 pop_assum mp_tac >> 2813 qid_spec_tac `s` >> 2814 `!s. FINITE s ==> !f1 f2. (!x. x IN s ==> (f1 x = f2 x)) ==> (PI f1 s = PI f2 s)` suffices_by rw[] >> 2815 Induct_on `FINITE` >> 2816 rpt strip_tac >- 2817 rw[PROD_IMAGE_EMPTY] >> 2818 metis_tac[PROD_IMAGE_INSERT, IN_INSERT] 2819 ]); 2820(* proof like SUM_IMAGE_CONG *) 2821val PROD_IMAGE_CONG = Q.store_thm( 2822 "PROD_IMAGE_CONG", 2823 `!s f1 f2. (!x. x IN s ==> (f1 x = f2 x)) ==> (PI f1 s = PI f2 s)`, 2824 SRW_TAC [][] THEN 2825 REVERSE (Cases_on `FINITE s`) THEN1 ( 2826 SRW_TAC [][PROD_IMAGE_DEF, Once ITSET_def] THEN 2827 SRW_TAC [][Once ITSET_def] 2828 ) THEN 2829 Q.PAT_ASSUM `!x. P` MP_TAC THEN 2830 POP_ASSUM MP_TAC THEN 2831 Q.ID_SPEC_TAC `s` THEN 2832 HO_MATCH_MP_TAC FINITE_INDUCT THEN 2833 METIS_TAC [PROD_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT] 2834); 2835 2836(* Theorem: FINITE s ==> !f k. (!x. x IN s ==> (f x = k)) ==> (PI f s = k ** CARD s) *) 2837(* Proof: 2838 By finite induction on s. 2839 Base: PI f {} = k ** CARD {} 2840 PI f {} 2841 = 1 by PROD_IMAGE_THM 2842 = c ** 0 by EXP 2843 = c ** CARD {} by CARD_DEF 2844 Step: !f k. (!x. x IN s ==> (f x = k)) ==> (PI f s = k ** CARD s) ==> 2845 e NOTIN s ==> PI f (e INSERT s) = k ** CARD (e INSERT s) 2846 PI f (e INSERT s) 2847 = ((f e) * PI (K c) (s DELETE e) by PROD_IMAGE_THM 2848 = c * PI (K c) (s DELETE e) by function application 2849 = c * PI (K c) s by DELETE_NON_ELEMENT 2850 = c * c ** CARD s by induction hypothesis 2851 = c ** (SUC (CARD s)) by EXP 2852 = c ** CARD (e INSERT s) by CARD_INSERT, e NOTIN s 2853*) 2854val PI_CONSTANT = store_thm( 2855 "PI_CONSTANT", 2856 ``!s. FINITE s ==> !f k. (!x. x IN s ==> (f x = k)) ==> (PI f s = k ** CARD s)``, 2857 Induct_on `FINITE` >> 2858 rpt strip_tac >- 2859 rw[PROD_IMAGE_THM] >> 2860 rw[PROD_IMAGE_THM, CARD_INSERT] >> 2861 fs[] >> 2862 metis_tac[DELETE_NON_ELEMENT, EXP]); 2863 2864(* Theorem: FINITE s ==> !c. PI (K c) s = c ** (CARD s) *) 2865(* Proof: by PI_CONSTANT. *) 2866val PROD_IMAGE_CONSTANT = store_thm( 2867 "PROD_IMAGE_CONSTANT", 2868 ``!s. FINITE s ==> !c. PI (K c) s = c ** (CARD s)``, 2869 rw[PI_CONSTANT]); 2870 2871(* ------------------------------------------------------------------------- *) 2872(* SUM_SET and PROD_SET Theorems *) 2873(* ------------------------------------------------------------------------- *) 2874 2875(* Theorem: FINITE s /\ x NOTIN s ==> (SUM_SET (x INSERT s) = x + SUM_SET s) *) 2876(* Proof: 2877 SUM_SET (x INSERT s) 2878 = x + SUM_SET (s DELETE x) by SUM_SET_THM 2879 = x + SUM_SET s by DELETE_NON_ELEMENT 2880*) 2881val SUM_SET_INSERT = store_thm( 2882 "SUM_SET_INSERT", 2883 ``!s x. FINITE s /\ x NOTIN s ==> (SUM_SET (x INSERT s) = x + SUM_SET s)``, 2884 rw[SUM_SET_THM, DELETE_NON_ELEMENT]); 2885 2886(* Theorem: FINITE s ==> !f. INJ f s UNIV ==> (SUM_SET (IMAGE f s) = SIGMA f s) *) 2887(* Proof: 2888 By finite induction on s. 2889 Base: SUM_SET (IMAGE f {}) = SIGMA f {} 2890 SUM_SET (IMAGE f {}) 2891 = SUM_SET {} by IMAGE_EMPTY 2892 = 1 by SUM_SET_EMPTY 2893 = SIGMA f {} by SUM_IMAGE_EMPTY 2894 Step: !f. INJ f s univ(:num) ==> (SUM_SET (IMAGE f s) = SIGMA f s) ==> 2895 e NOTIN s /\ INJ f (e INSERT s) univ(:num) ==> SUM_SET (IMAGE f (e INSERT s)) = SIGMA f (e INSERT s) 2896 Note INJ f s univ(:num) by INJ_INSERT 2897 and f e NOTIN (IMAGE f s) by IN_IMAGE 2898 SUM_SET (IMAGE f (e INSERT s)) 2899 = SUM_SET (f e INSERT (IMAGE f s)) by IMAGE_INSERT 2900 = f e * SUM_SET (IMAGE f s) by SUM_SET_INSERT 2901 = f e * SIGMA f s by induction hypothesis 2902 = SIGMA f (e INSERT s) by SUM_IMAGE_INSERT 2903*) 2904val SUM_SET_IMAGE_EQN = store_thm( 2905 "SUM_SET_IMAGE_EQN", 2906 ``!s. FINITE s ==> !f. INJ f s UNIV ==> (SUM_SET (IMAGE f s) = SIGMA f s)``, 2907 Induct_on `FINITE` >> 2908 rpt strip_tac >- 2909 rw[SUM_SET_EMPTY, SUM_IMAGE_EMPTY] >> 2910 fs[INJ_INSERT] >> 2911 `f e NOTIN (IMAGE f s)` by metis_tac[IN_IMAGE] >> 2912 rw[SUM_SET_INSERT, SUM_IMAGE_INSERT]); 2913 2914(* Theorem: SUM_SET (count n) = (n * (n - 1)) DIV 2*) 2915(* Proof: 2916 By induction on n. 2917 Base case: SUM_SET (count 0) = 0 * (0 - 1) DIV 2 2918 LHS = SUM_SET (count 0) 2919 = SUM_SET {} by COUNT_ZERO 2920 = 0 by SUM_SET_THM 2921 = 0 DIV 2 by ZERO_DIV 2922 = 0 * (0 - 1) DIV 2 by MULT 2923 = RHS 2924 Step case: SUM_SET (count n) = n * (n - 1) DIV 2 ==> 2925 SUM_SET (count (SUC n)) = SUC n * (SUC n - 1) DIV 2 2926 If n = 0, to show: SUM_SET (count 1) = 0 2927 SUM_SET (count 1) = SUM_SET {0} = 0 by SUM_SET_SING 2928 If n <> 0, 0 < n. 2929 First, FINITE (count n) by FINITE_COUNT 2930 n NOTIN (count n) by IN_COUNT 2931 LHS = SUM_SET (count (SUC n)) 2932 = SUM_SET (n INSERT count n) by COUNT_SUC 2933 = n + SUM_SET (count n DELETE n) by SUM_SET_THM 2934 = n + SUM_SET (count n) by DELETE_NON_ELEMENT 2935 = n + n * (n - 1) DIV 2 by induction hypothesis 2936 = (n * 2 + n * (n - 1)) DIV 2 by ADD_DIV_ADD_DIV 2937 = (n * (2 + (n - 1))) DIV 2 by LEFT_ADD_DISTRIB 2938 = n * (n + 1) DIV 2 by arithmetic, 0 < n 2939 = (SUC n - 1) * (SUC n) DIV 2 by ADD1, SUC_SUB1 2940 = SUC n * (SUC n - 1) DIV 2 by MULT_COMM 2941 = RHS 2942*) 2943val SUM_SET_COUNT = store_thm( 2944 "SUM_SET_COUNT", 2945 ``!n. SUM_SET (count n) = (n * (n - 1)) DIV 2``, 2946 Induct_on `n` >- 2947 rw[] >> 2948 Cases_on `n = 0` >| [ 2949 rw[] >> 2950 EVAL_TAC, 2951 `0 < n` by decide_tac >> 2952 `FINITE (count n)` by rw[] >> 2953 `n NOTIN (count n)` by rw[] >> 2954 `SUM_SET (count (SUC n)) = SUM_SET (n INSERT count n)` by rw[COUNT_SUC] >> 2955 `_ = n + SUM_SET (count n DELETE n)` by rw[SUM_SET_THM] >> 2956 `_ = n + SUM_SET (count n)` by metis_tac[DELETE_NON_ELEMENT] >> 2957 `_ = n + n * (n - 1) DIV 2` by rw[] >> 2958 `_ = (n * 2 + n * (n - 1)) DIV 2` by rw[ADD_DIV_ADD_DIV] >> 2959 `_ = (n * (2 + (n - 1))) DIV 2` by rw[LEFT_ADD_DISTRIB] >> 2960 `_ = n * (n + 1) DIV 2` by rw_tac arith_ss[] >> 2961 `_ = (SUC n - 1) * SUC n DIV 2` by rw[ADD1, SUC_SUB1] >> 2962 `_ = SUC n * (SUC n - 1) DIV 2 ` by rw[MULT_COMM] >> 2963 decide_tac 2964 ]); 2965 2966(* Theorem: PROD_SET {x} = x *) 2967(* Proof: 2968 Since FINITE {x} by FINITE_SING 2969 PROD_SET {x} 2970 = PROD_SET (x INSERT {}) by SING_INSERT 2971 = x * PROD_SET {} by PROD_SET_THM 2972 = x by PROD_SET_EMPTY 2973*) 2974val PROD_SET_SING = store_thm( 2975 "PROD_SET_SING", 2976 ``!x. PROD_SET {x} = x``, 2977 rw[PROD_SET_THM, FINITE_SING]); 2978 2979(* Theorem: FINITE s /\ 0 NOTIN s ==> 0 < PROD_SET s *) 2980(* Proof: 2981 By FINITE_INDUCT on s. 2982 Base case: 0 NOTIN {} ==> 0 < PROD_SET {} 2983 Since PROD_SET {} = 1 by PROD_SET_THM 2984 Hence true. 2985 Step case: 0 NOTIN s ==> 0 < PROD_SET s ==> 2986 e NOTIN s /\ 0 NOTIN e INSERT s ==> 0 < PROD_SET (e INSERT s) 2987 PROD_SET (e INSERT s) 2988 = e * PROD_SET (s DELETE e) by PROD_SET_THM 2989 = e * PROD_SET s by DELETE_NON_ELEMENT 2990 But e IN e INSERT s by COMPONENT 2991 Hence e <> 0, or 0 < e by implication 2992 and !x. x IN s ==> x IN (e INSERT s) by IN_INSERT 2993 Thus 0 < PROD_SET s by induction hypothesis 2994 Henec 0 < e * PROD_SET s by ZERO_LESS_MULT 2995*) 2996val PROD_SET_NONZERO = store_thm( 2997 "PROD_SET_NONZERO", 2998 ``!s. FINITE s /\ 0 NOTIN s ==> 0 < PROD_SET s``, 2999 `!s. FINITE s ==> 0 NOTIN s ==> 0 < PROD_SET s` suffices_by rw[] >> 3000 ho_match_mp_tac FINITE_INDUCT >> 3001 rpt strip_tac >- 3002 rw[PROD_SET_THM] >> 3003 fs[] >> 3004 `0 < e` by decide_tac >> 3005 `PROD_SET (e INSERT s) = e * PROD_SET (s DELETE e)` by rw[PROD_SET_THM] >> 3006 `_ = e * PROD_SET s` by metis_tac[DELETE_NON_ELEMENT] >> 3007 rw[ZERO_LESS_MULT]); 3008 3009(* Theorem: FINITE s /\ s <> {} /\ 0 NOTIN s ==> 3010 !f. INJ f s univ(:num) /\ (!x. x < f x) ==> PROD_SET s < PROD_SET (IMAGE f s) *) 3011(* Proof: 3012 By FINITE_INDUCT on s. 3013 Base case: {} <> {} ==> PROD_SET {} < PROD_SET (IMAGE f {}) 3014 True since {} <> {} is false. 3015 Step case: s <> {} /\ 0 NOTIN s ==> !f. INJ f s univ(:num) ==> PROD_SET s < PROD_SET (IMAGE f s) ==> 3016 e NOTIN s /\ e INSERT s <> {} /\ 0 NOTIN e INSERT s /\ INJ f (e INSERT s) univ(:num) ==> 3017 PROD_SET (e INSERT s) < PROD_SET (IMAGE f (e INSERT s)) 3018 Note INJ f (e INSERT s) univ(:num) 3019 ==> INJ f s univ(:num) /\ 3020 !y. y IN s /\ (f e = f y) ==> (e = y) by INJ_INSERT 3021 First, 3022 PROD_SET (e INSERT s) 3023 = e * PROD_SET (s DELETE e) by PROD_SET_THM 3024 = e * PROD_SET s by DELETE_NON_ELEMENT 3025 Next, 3026 FINITE (IMAGE f s) by IMAGE_FINITE 3027 f e NOTIN IMAGE f s by IN_IMAGE, e NOTIN s 3028 PROD_SET (IMAGE f (e INSERT s)) 3029 = f e * PROD_SET (IMAGE f s) by PROD_SET_IMAGE_REDUCTION 3030 3031 If s = {}, 3032 to show: e * PROD_SET {} < f e * PROD_SET {} by IMAGE_EMPTY 3033 which is true since PROD_SET {} = 1 by PROD_SET_THM 3034 and e < f e by given 3035 If s <> {}, 3036 Since e IN e INSERT s by COMPONENT 3037 Hence 0 < e by e <> 0 3038 and !x. x IN s ==> x IN (e INSERT s) by IN_INSERT 3039 Thus PROD_SET s < PROD_SET (IMAGE f s) by induction hypothesis 3040 or e * PROD_SET s < e * PROD_SET (IMAGE f s) by LT_MULT_LCANCEL, 0 < e 3041 Note 0 < PROD_SET (IMAGE f s) by IN_IMAGE, !x. x < f x /\ x <> 0 3042 so e * PROD_SET (IMAGE f s) < f e * PROD_SET (IMAGE f s) by LT_MULT_LCANCEL, e < f e 3043 Hence PROD_SET (e INSERT s) < PROD_SET (IMAGE f (e INSERT s)) 3044*) 3045val PROD_SET_LESS = store_thm( 3046 "PROD_SET_LESS", 3047 ``!s. FINITE s /\ s <> {} /\ 0 NOTIN s ==> 3048 !f. INJ f s univ(:num) /\ (!x. x < f x) ==> PROD_SET s < PROD_SET (IMAGE f s)``, 3049 `!s. FINITE s ==> s <> {} /\ 0 NOTIN s ==> 3050 !f. INJ f s univ(:num) /\ (!x. x < f x) ==> PROD_SET s < PROD_SET (IMAGE f s)` suffices_by rw[] >> 3051 ho_match_mp_tac FINITE_INDUCT >> 3052 rpt strip_tac >- 3053 rw[] >> 3054 `PROD_SET (e INSERT s) = e * PROD_SET (s DELETE e)` by rw[PROD_SET_THM] >> 3055 `_ = e * PROD_SET s` by metis_tac[DELETE_NON_ELEMENT] >> 3056 fs[INJ_INSERT] >> 3057 `FINITE (IMAGE f s)` by rw[] >> 3058 `f e NOTIN IMAGE f s` by metis_tac[IN_IMAGE] >> 3059 `PROD_SET (IMAGE f (e INSERT s)) = f e * PROD_SET (IMAGE f s)` by rw[PROD_SET_IMAGE_REDUCTION] >> 3060 Cases_on `s = {}` >- 3061 rw[PROD_SET_SING, PROD_SET_THM] >> 3062 `0 < e` by decide_tac >> 3063 `PROD_SET s < PROD_SET (IMAGE f s)` by rw[] >> 3064 `e * PROD_SET s < e * PROD_SET (IMAGE f s)` by rw[] >> 3065 `e * PROD_SET (IMAGE f s) < (f e) * PROD_SET (IMAGE f s)` by rw[] >> 3066 `(IMAGE f (e INSERT s)) = (f e INSERT IMAGE f s)` by rw[] >> 3067 metis_tac[LESS_TRANS]); 3068 3069(* Theorem: FINITE s /\ s <> {} /\ 0 NOTIN s ==> PROD_SET s < PROD_SET (IMAGE SUC s) *) 3070(* Proof: 3071 Since !m n. SUC m = SUC n <=> m = n by INV_SUC 3072 thus INJ INJ SUC s univ(:num) by INJ_DEF 3073 Hence the result follows by PROD_SET_LESS 3074*) 3075val PROD_SET_LESS_SUC = store_thm( 3076 "PROD_SET_LESS_SUC", 3077 ``!s. FINITE s /\ s <> {} /\ 0 NOTIN s ==> PROD_SET s < PROD_SET (IMAGE SUC s)``, 3078 rpt strip_tac >> 3079 (irule PROD_SET_LESS >> simp[]) >> 3080 rw[INJ_DEF]); 3081 3082(* Theorem: FINITE s ==> !n x. x IN s /\ n divides x ==> n divides (PROD_SET s) *) 3083(* Proof: 3084 By FINITE_INDUCT on s. 3085 Base case: x IN {} /\ n divides x ==> n divides (PROD_SET {}) 3086 True since x IN {} is false by NOT_IN_EMPTY 3087 Step case: !n x. x IN s /\ n divides x ==> n divides (PROD_SET s) ==> 3088 e NOTIN s /\ x IN e INSERT s /\ n divides x ==> n divides (PROD_SET (e INSERT s)) 3089 PROD_SET (e INSERT s) 3090 = e * PROD_SET (s DELETE e) by PROD_SET_THM 3091 = e * PROD_SET s by DELETE_NON_ELEMENT 3092 If x = e, 3093 n divides x 3094 means n divides e 3095 hence n divides PROD_SET (e INSERT s) by DIVIDES_MULTIPLE, MULT_COMM 3096 If x <> e, x IN s by IN_INSERT 3097 n divides (PROD_SET s) by induction hypothesis 3098 hence n divides PROD_SET (e INSERT s) by DIVIDES_MULTIPLE 3099*) 3100val PROD_SET_DIVISORS = store_thm( 3101 "PROD_SET_DIVISORS", 3102 ``!s. FINITE s ==> !n x. x IN s /\ n divides x ==> n divides (PROD_SET s)``, 3103 ho_match_mp_tac FINITE_INDUCT >> 3104 rpt strip_tac >- 3105 metis_tac[NOT_IN_EMPTY] >> 3106 `PROD_SET (e INSERT s) = e * PROD_SET (s DELETE e)` by rw[PROD_SET_THM] >> 3107 `_ = e * PROD_SET s` by metis_tac[DELETE_NON_ELEMENT] >> 3108 `(x = e) \/ (x IN s)` by rw[GSYM IN_INSERT] >- 3109 metis_tac[DIVIDES_MULTIPLE, MULT_COMM] >> 3110 metis_tac[DIVIDES_MULTIPLE]); 3111 3112(* PROD_SET_IMAGE_REDUCTION |> ISPEC ``I:num -> num``; *) 3113 3114(* Theorem: FINITE s /\ x NOTIN s ==> (PROD_SET (x INSERT s) = x * PROD_SET s) *) 3115(* Proof: 3116 Since !x. I x = x by I_THM 3117 and !s. IMAGE I s = s by IMAGE_I 3118 thus the result follows by PROD_SET_IMAGE_REDUCTION 3119*) 3120val PROD_SET_INSERT = store_thm( 3121 "PROD_SET_INSERT", 3122 ``!x s. FINITE s /\ x NOTIN s ==> (PROD_SET (x INSERT s) = x * PROD_SET s)``, 3123 metis_tac[PROD_SET_IMAGE_REDUCTION, combinTheory.I_THM, IMAGE_I]); 3124 3125(* Theorem: FINITE s ==> !f. INJ f s UNIV ==> (PROD_SET (IMAGE f s) = PI f s) *) 3126(* Proof: 3127 By finite induction on s. 3128 Base: PROD_SET (IMAGE f {}) = PI f {} 3129 PROD_SET (IMAGE f {}) 3130 = PROD_SET {} by IMAGE_EMPTY 3131 = 1 by PROD_SET_EMPTY 3132 = PI f {} by PROD_IMAGE_EMPTY 3133 Step: !f. INJ f s univ(:num) ==> (PROD_SET (IMAGE f s) = PI f s) ==> 3134 e NOTIN s /\ INJ f (e INSERT s) univ(:num) ==> PROD_SET (IMAGE f (e INSERT s)) = PI f (e INSERT s) 3135 Note INJ f s univ(:num) by INJ_INSERT 3136 and f e NOTIN (IMAGE f s) by IN_IMAGE 3137 PROD_SET (IMAGE f (e INSERT s)) 3138 = PROD_SET (f e INSERT (IMAGE f s)) by IMAGE_INSERT 3139 = f e * PROD_SET (IMAGE f s) by PROD_SET_INSERT 3140 = f e * PI f s by induction hypothesis 3141 = PI f (e INSERT s) by PROD_IMAGE_INSERT 3142*) 3143val PROD_SET_IMAGE_EQN = store_thm( 3144 "PROD_SET_IMAGE_EQN", 3145 ``!s. FINITE s ==> !f. INJ f s UNIV ==> (PROD_SET (IMAGE f s) = PI f s)``, 3146 Induct_on `FINITE` >> 3147 rpt strip_tac >- 3148 rw[PROD_SET_EMPTY, PROD_IMAGE_EMPTY] >> 3149 fs[INJ_INSERT] >> 3150 `f e NOTIN (IMAGE f s)` by metis_tac[IN_IMAGE] >> 3151 rw[PROD_SET_INSERT, PROD_IMAGE_INSERT]); 3152 3153(* Theorem: PROD_SET (IMAGE (\j. n ** j) (count m)) = n ** (SUM_SET (count m)) *) 3154(* Proof: 3155 By induction on m. 3156 Base case: PROD_SET (IMAGE (\j. n ** j) (count 0)) = n ** SUM_SET (count 0) 3157 LHS = PROD_SET (IMAGE (\j. n ** j) (count 0)) 3158 = PROD_SET (IMAGE (\j. n ** j) {}) by COUNT_ZERO 3159 = PROD_SET {} by IMAGE_EMPTY 3160 = 1 by PROD_SET_THM 3161 RHS = n ** SUM_SET (count 0) 3162 = n ** SUM_SET {} by COUNT_ZERO 3163 = n ** 0 by SUM_SET_THM 3164 = 1 by EXP 3165 = LHS 3166 Step case: PROD_SET (IMAGE (\j. n ** j) (count m)) = n ** SUM_SET (count m) ==> 3167 PROD_SET (IMAGE (\j. n ** j) (count (SUC m))) = n ** SUM_SET (count (SUC m)) 3168 First, 3169 FINITE (count m) by FINITE_COUNT 3170 FINITE (IMAGE (\j. n ** j) (count m)) by IMAGE_FINITE 3171 m NOTIN count m by IN_COUNT 3172 and (\j. n ** j) m NOTIN IMAGE (\j. n ** j) (count m) by EXP_BASE_INJECTIVE, 1 < n 3173 3174 LHS = PROD_SET (IMAGE (\j. n ** j) (count (SUC m))) 3175 = PROD_SET (IMAGE (\j. n ** j) (m INSERT count m)) by COUNT_SUC 3176 = n ** m * PROD_SET (IMAGE (\j. n ** j) (count m)) by PROD_SET_IMAGE_REDUCTION 3177 = n ** m * n ** SUM_SET (count m) by induction hypothesis 3178 = n ** (m + SUM_SET (count m)) by EXP_ADD 3179 = n ** SUM_SET (m INSERT count m) by SUM_SET_INSERT 3180 = n ** SUM_SET (count (SUC m)) by COUNT_SUC 3181 = RHS 3182*) 3183val PROD_SET_IMAGE_EXP = store_thm( 3184 "PROD_SET_IMAGE_EXP", 3185 ``!n. 1 < n ==> !m. PROD_SET (IMAGE (\j. n ** j) (count m)) = n ** (SUM_SET (count m))``, 3186 rpt strip_tac >> 3187 Induct_on `m` >- 3188 rw[PROD_SET_THM] >> 3189 `FINITE (IMAGE (\j. n ** j) (count m))` by rw[] >> 3190 `(\j. n ** j) m NOTIN IMAGE (\j. n ** j) (count m)` by rw[] >> 3191 `m NOTIN count m` by rw[] >> 3192 `PROD_SET (IMAGE (\j. n ** j) (count (SUC m))) = 3193 PROD_SET (IMAGE (\j. n ** j) (m INSERT count m))` by rw[COUNT_SUC] >> 3194 `_ = n ** m * PROD_SET (IMAGE (\j. n ** j) (count m))` by rw[PROD_SET_IMAGE_REDUCTION] >> 3195 `_ = n ** m * n ** SUM_SET (count m)` by rw[] >> 3196 `_ = n ** (m + SUM_SET (count m))` by rw[EXP_ADD] >> 3197 `_ = n ** SUM_SET (m INSERT count m)` by rw[SUM_SET_INSERT] >> 3198 `_ = n ** SUM_SET (count (SUC m))` by rw[COUNT_SUC] >> 3199 decide_tac); 3200 3201(* Theorem: FINITE s /\ x IN s ==> x divides PROD_SET s *) 3202(* Proof: 3203 Note !n x. x IN s /\ n divides x 3204 ==> n divides PROD_SET s by PROD_SET_DIVISORS 3205 Put n = x, and x divides x = T by DIVIDES_REFL 3206 and the result follows. 3207*) 3208val PROD_SET_ELEMENT_DIVIDES = store_thm( 3209 "PROD_SET_ELEMENT_DIVIDES", 3210 ``!s x. FINITE s /\ x IN s ==> x divides PROD_SET s``, 3211 metis_tac[PROD_SET_DIVISORS, DIVIDES_REFL]); 3212 3213(* Theorem: FINITE s ==> !f g. INJ f s univ(:num) /\ INJ g s univ(:num) /\ 3214 (!x. x IN s ==> f x <= g x) ==> PROD_SET (IMAGE f s) <= PROD_SET (IMAGE g s) *) 3215(* Proof: 3216 By finite induction on s. 3217 Base: PROD_SET (IMAGE f {}) <= PROD_SET (IMAGE g {}) 3218 Note PROD_SET (IMAGE f {}) 3219 = PROD_SET {} by IMAGE_EMPTY 3220 = 1 by PROD_SET_EMPTY 3221 Thus true. 3222 Step: !f g. (!x. x IN s ==> f x <= g x) ==> PROD_SET (IMAGE f s) <= PROD_SET (IMAGE g s) ==> 3223 e NOTIN s /\ !x. x IN e INSERT s ==> f x <= g x ==> 3224 PROD_SET (IMAGE f (e INSERT s)) <= PROD_SET (IMAGE g (e INSERT s)) 3225 Note INJ f s univ(:num) by INJ_INSERT 3226 and INJ g s univ(:num) by INJ_INSERT 3227 and f e NOTIN (IMAGE f s) by IN_IMAGE 3228 and g e NOTIN (IMAGE g s) by IN_IMAGE 3229 Applying LE_MONO_MULT2, 3230 PROD_SET (IMAGE f (e INSERT s)) 3231 = PROD_SET (f e INSERT IMAGE f s) by INSERT_IMAGE 3232 = f e * PROD_SET (IMAGE f s) by PROD_SET_INSERT 3233 <= g e * PROD_SET (IMAGE f s) by f e <= g e 3234 <= g e * PROD_SET (IMAGE g s) by induction hypothesis 3235 = PROD_SET (g e INSERT IMAGE g s) by PROD_SET_INSERT 3236 = PROD_SET (IMAGE g (e INSERT s)) by INSERT_IMAGE 3237*) 3238val PROD_SET_LESS_EQ = store_thm( 3239 "PROD_SET_LESS_EQ", 3240 ``!s. FINITE s ==> !f g. INJ f s univ(:num) /\ INJ g s univ(:num) /\ 3241 (!x. x IN s ==> f x <= g x) ==> PROD_SET (IMAGE f s) <= PROD_SET (IMAGE g s)``, 3242 Induct_on `FINITE` >> 3243 rpt strip_tac >- 3244 rw[PROD_SET_EMPTY] >> 3245 fs[INJ_INSERT] >> 3246 `f e NOTIN (IMAGE f s)` by metis_tac[IN_IMAGE] >> 3247 `g e NOTIN (IMAGE g s)` by metis_tac[IN_IMAGE] >> 3248 `f e <= g e` by rw[] >> 3249 `PROD_SET (IMAGE f s) <= PROD_SET (IMAGE g s)` by rw[] >> 3250 rw[PROD_SET_INSERT, LE_MONO_MULT2]); 3251 3252(* Theorem: FINITE s ==> !n. (!x. x IN s ==> x <= n) ==> PROD_SET s <= n ** CARD s *) 3253(* Proof: 3254 By finite induction on s. 3255 Base: PROD_SET {} <= n ** CARD {} 3256 Note PROD_SET {} 3257 = 1 by PROD_SET_EMPTY 3258 = n ** 0 by EXP_0 3259 = n ** CARD {} by CARD_EMPTY 3260 Step: !n. (!x. x IN s ==> x <= n) ==> PROD_SET s <= n ** CARD s ==> 3261 e NOTIN s /\ !x. x IN e INSERT s ==> x <= n ==> PROD_SET (e INSERT s) <= n ** CARD (e INSERT s) 3262 Note !x. (x = e) \/ x IN s ==> x <= n by IN_INSERT 3263 PROD_SET (e INSERT s) 3264 = e * PROD_SET s by PROD_SET_INSERT 3265 <= n * PROD_SET s by e <= n 3266 <= n * (n ** CARD s) by induction hypothesis 3267 = n ** (SUC (CARD s)) by EXP 3268 = n ** CARD (e INSERT s) by CARD_INSERT, e NOTIN s 3269*) 3270val PROD_SET_LE_CONSTANT = store_thm( 3271 "PROD_SET_LE_CONSTANT", 3272 ``!s. FINITE s ==> !n. (!x. x IN s ==> x <= n) ==> PROD_SET s <= n ** CARD s``, 3273 Induct_on `FINITE` >> 3274 rpt strip_tac >- 3275 rw[PROD_SET_EMPTY, EXP_0] >> 3276 fs[] >> 3277 `e <= n /\ PROD_SET s <= n ** CARD s` by rw[] >> 3278 rw[PROD_SET_INSERT, EXP, CARD_INSERT, LE_MONO_MULT2]); 3279 3280(* Theorem: FINITE s ==> !n f g. INJ f s univ(:num) /\ INJ g s univ(:num) /\ (!x. x IN s ==> n <= f x * g x) ==> 3281 n ** CARD s <= PROD_SET (IMAGE f s) * PROD_SET (IMAGE g s) *) 3282(* Proof: 3283 By finite induction on s. 3284 Base: n ** CARD {} <= PROD_SET (IMAGE f {}) * PROD_SET (IMAGE g {}) 3285 Note n ** CARD {} 3286 = n ** 0 by CARD_EMPTY 3287 = 1 by EXP_0 3288 and PROD_SET (IMAGE f {}) 3289 = PROD_SET {} by IMAGE_EMPTY 3290 = 1 by PROD_SET_EMPTY 3291 Step: !n f. INJ f s univ(:num) /\ INJ g s univ(:num) /\ 3292 (!x. x IN s ==> n <= f x * g x) ==> 3293 n ** CARD s <= PROD_SET (IMAGE f s) * PROD_SET (IMAGE g s) ==> 3294 e NOTIN s /\ INJ f (e INSERT s) univ(:num) /\ INJ g (e INSERT s) univ(:num) /\ 3295 !x. x IN e INSERT s ==> n <= f x * g x ==> 3296 n ** CARD (e INSERT s) <= PROD_SET (IMAGE f (e INSERT s)) * PROD_SET (IMAGE g (e INSERT s)) 3297 Note INJ f s univ(:num) /\ INJ g s univ(:num) by INJ_INSERT 3298 and f e NOTIN (IMAGE f s) /\ g e NOTIN (IMAGE g s) by IN_IMAGE 3299 PROD_SET (IMAGE f (e INSERT s)) * PROD_SET (IMAGE g (e INSERT s)) 3300 = PROD_SET (f e INSERT (IMAGE f s)) * PROD_SET (g e INSERT (IMAGE g s)) by INSERT_IMAGE 3301 = (f e * PROD_SET (IMAGE f s)) * (g e * PROD_SET (IMAGE g s)) by PROD_SET_INSERT 3302 = (f e * g e) * (PROD_SET (IMAGE f s) * PROD_SET (IMAGE g s)) by MULT_ASSOC, MULT_COMM 3303 >= n * (PROD_SET (IMAGE f s) * PROD_SET (IMAGE g s)) by n <= f e * g e 3304 >= n * n ** CARD s by induction hypothesis 3305 = n ** (SUC (CARD s)) by EXP 3306 = n ** (CARD (e INSERT s)) by CARD_INSERT 3307*) 3308val PROD_SET_PRODUCT_GE_CONSTANT = store_thm( 3309 "PROD_SET_PRODUCT_GE_CONSTANT", 3310 ``!s. FINITE s ==> !n f g. INJ f s univ(:num) /\ INJ g s univ(:num) /\ (!x. x IN s ==> n <= f x * g x) ==> 3311 n ** CARD s <= PROD_SET (IMAGE f s) * PROD_SET (IMAGE g s)``, 3312 Induct_on `FINITE` >> 3313 rpt strip_tac >- 3314 rw[PROD_SET_EMPTY, EXP_0] >> 3315 fs[INJ_INSERT] >> 3316 `f e NOTIN (IMAGE f s) /\ g e NOTIN (IMAGE g s)` by metis_tac[IN_IMAGE] >> 3317 `n <= f e * g e /\ n ** CARD s <= PROD_SET (IMAGE f s) * PROD_SET (IMAGE g s)` by rw[] >> 3318 `PROD_SET (f e INSERT IMAGE f s) * PROD_SET (g e INSERT IMAGE g s) = 3319 (f e * PROD_SET (IMAGE f s)) * (g e * PROD_SET (IMAGE g s))` by rw[PROD_SET_INSERT] >> 3320 `_ = (f e * g e) * (PROD_SET (IMAGE f s) * PROD_SET (IMAGE g s))` by metis_tac[MULT_ASSOC, MULT_COMM] >> 3321 metis_tac[EXP, CARD_INSERT, LE_MONO_MULT2]); 3322 3323(* Theorem: FINITE s ==> !u v. s =|= u # v ==> (PROD_SET s = PROD_SET u * PROD_SET v) *) 3324(* Proof: 3325 By finite induction on s. 3326 Base: {} = u UNION v ==> PROD_SET {} = PROD_SET u * PROD_SET v 3327 Note u = {} and v = {} by EMPTY_UNION 3328 and PROD_SET {} = 1 by PROD_SET_EMPTY 3329 Hence true. 3330 Step: !u v. (s = u UNION v) /\ DISJOINT u v ==> (PROD_SET s = PROD_SET u * PROD_SET v) ==> 3331 e NOTIN s /\ e INSERT s = u UNION v ==> PROD_SET (e INSERT s) = PROD_SET u * PROD_SET v 3332 Note e IN u \/ e IN v by IN_INSERT, IN_UNION 3333 If e IN u, 3334 Then e NOTIN v by IN_DISJOINT 3335 Let w = u DELETE e. 3336 Then e NOTIN w by IN_DELETE 3337 and u = e INSERT w by INSERT_DELETE 3338 Note s = w UNION v by EXTENSION, IN_INSERT, IN_UNION 3339 ==> FINITE w by FINITE_UNION 3340 and DISJOINT w v by DISJOINT_INSERT 3341 PROD_SET (e INSERT s) 3342 = e * PROD_SET s by PROD_SET_INSERT, FINITE s 3343 = e * (PROD_SET w * PROD_SET v) by induction hypothesis 3344 = (e * PROD_SET w) * PROD_SET v by MULT_ASSOC 3345 = PROD_SET (e INSERT w) * PROD_SET v by PROD_SET_INSERT, FINITE w 3346 = PROD_SET u * PROD_SET v 3347 3348 Similarly for e IN v. 3349*) 3350val PROD_SET_PRODUCT_BY_PARTITION = store_thm( 3351 "PROD_SET_PRODUCT_BY_PARTITION", 3352 ``!s. FINITE s ==> !u v. s =|= u # v ==> (PROD_SET s = PROD_SET u * PROD_SET v)``, 3353 Induct_on `FINITE` >> 3354 rpt strip_tac >- 3355 fs[PROD_SET_EMPTY] >> 3356 `e IN u \/ e IN v` by metis_tac[IN_INSERT, IN_UNION] >| [ 3357 qabbrev_tac `w = u DELETE e` >> 3358 `u = e INSERT w` by rw[Abbr`w`] >> 3359 `e NOTIN w` by rw[Abbr`w`] >> 3360 `e NOTIN v` by metis_tac[IN_DISJOINT] >> 3361 `s = w UNION v` by 3362 (rw[EXTENSION] >> 3363 metis_tac[IN_INSERT, IN_UNION]) >> 3364 `FINITE w` by metis_tac[FINITE_UNION] >> 3365 `DISJOINT w v` by metis_tac[DISJOINT_INSERT] >> 3366 `PROD_SET (e INSERT s) = e * PROD_SET s` by rw[PROD_SET_INSERT] >> 3367 `_ = e * (PROD_SET w * PROD_SET v)` by rw[] >> 3368 `_ = (e * PROD_SET w) * PROD_SET v` by rw[] >> 3369 `_ = PROD_SET u * PROD_SET v` by rw[PROD_SET_INSERT] >> 3370 rw[], 3371 qabbrev_tac `w = v DELETE e` >> 3372 `v = e INSERT w` by rw[Abbr`w`] >> 3373 `e NOTIN w` by rw[Abbr`w`] >> 3374 `e NOTIN u` by metis_tac[IN_DISJOINT] >> 3375 `s = u UNION w` by 3376 (rw[EXTENSION] >> 3377 metis_tac[IN_INSERT, IN_UNION]) >> 3378 `FINITE w` by metis_tac[FINITE_UNION] >> 3379 `DISJOINT u w` by metis_tac[DISJOINT_INSERT, DISJOINT_SYM] >> 3380 `PROD_SET (e INSERT s) = e * PROD_SET s` by rw[PROD_SET_INSERT] >> 3381 `_ = e * (PROD_SET u * PROD_SET w)` by rw[] >> 3382 `_ = PROD_SET u * (e * PROD_SET w)` by rw[] >> 3383 `_ = PROD_SET u * PROD_SET v` by rw[PROD_SET_INSERT] >> 3384 rw[] 3385 ]); 3386 3387(* ------------------------------------------------------------------------- *) 3388(* Partition and Equivalent Class *) 3389(* ------------------------------------------------------------------------- *) 3390 3391(* Overload equivalence class of a relation *) 3392val _ = overload_on("equiv_class", ``\R s x. {y | y IN s /\ R x y}``); 3393 3394(* Theorem: y IN equiv_class R s x <=> y IN s /\ R x y *) 3395(* Proof: by GSPECIFICATION *) 3396val equiv_class_element = store_thm( 3397 "equiv_class_element", 3398 ``!R s x y. y IN equiv_class R s x <=> y IN s /\ R x y``, 3399 rw[]); 3400 3401(* Theorem: R equiv_on s /\ x IN s /\ y IN s ==> 3402 ((equiv_class R s x = equiv_class R s y) <=> R x y) *) 3403(* Proof: by equiv_on_def, EXTENSION. *) 3404Theorem equiv_class_eq: 3405 !R s x y. R equiv_on s /\ x IN s /\ y IN s ==> 3406 ((equiv_class R s x = equiv_class R s y) <=> R x y) 3407Proof 3408 rw[equiv_on_def, EXTENSION] >> 3409 metis_tac[] 3410QED 3411 3412(* Theorem: R equiv_on s /\ t SUBSET s ==> R equiv_on t *) 3413(* Proof: by equiv_on_def, SUBSET_DEF *) 3414val equiv_on_subset = store_thm( 3415 "equiv_on_subset", 3416 ``!R s t. R equiv_on s /\ t SUBSET s ==> R equiv_on t``, 3417 rw_tac std_ss[equiv_on_def, SUBSET_DEF] >> 3418 metis_tac[]); 3419 3420(* Theorem: partition R {} = {} *) 3421(* Proof: by partition_def *) 3422val partition_on_empty = store_thm( 3423 "partition_on_empty", 3424 ``!R. partition R {} = {}``, 3425 rw[partition_def]); 3426 3427(* 3428> partition_def; 3429val it = |- !R s. partition R s = {t | ?x. x IN s /\ (t = equiv_class R s x)}: thm 3430*) 3431 3432(* Theorem: t IN partition R s <=> ?x. x IN s /\ (t = equiv_class R s x) *) 3433(* Proof: by partition_def *) 3434Theorem partition_element: 3435 !R s t. t IN partition R s <=> ?x. x IN s /\ (t = equiv_class R s x) 3436Proof 3437 rw[partition_def] 3438QED 3439 3440(* Theorem: partition R s = IMAGE (equiv_class R s) s *) 3441(* Proof: 3442 partition R s 3443 = {t | ?x. x IN s /\ (t = {y | y IN s /\ R x y})} by partition_def 3444 = {t | ?x. x IN s /\ (t = equiv_class R s x)} by notation 3445 = IMAGE (equiv_class R s) s by IN_IMAGE 3446*) 3447val partition_elements = store_thm( 3448 "partition_elements", 3449 ``!R s. partition R s = IMAGE (equiv_class R s) s``, 3450 rw[partition_def, EXTENSION] >> 3451 metis_tac[]); 3452 3453(* Theorem alias *) 3454val partition_as_image = save_thm("partition_as_image", partition_elements); 3455(* val partition_as_image = 3456 |- !R s. partition R s = IMAGE (\x. equiv_class R s x) s: thm *) 3457 3458(* Theorem: (R1 = R2) /\ (s1 = s2) ==> (partition R1 s1 = partition R2 s2) *) 3459(* Proof: by identity *) 3460val partition_cong = store_thm( 3461 "partition_cong", 3462 ``!R1 R2 s1 s2. (R1 = R2) /\ (s1 = s2) ==> (partition R1 s1 = partition R2 s2)``, 3463 rw[]); 3464(* Just in case this is needed. *) 3465 3466(* Theorem: When the partitions are equal size of n, CARD s = n * CARD (partition of s). 3467 FINITE s /\ R equiv_on s /\ (!e. e IN partition R s ==> (CARD e = n)) ==> 3468 (CARD s = n * CARD (partition R s)) *) 3469(* Proof: 3470 Note FINITE (partition R s) by FINITE_partition 3471 so CARD s = SIGMA CARD (partition R s) by partition_CARD 3472 = n * CARD (partition R s) by SIGMA_CARD_CONSTANT 3473*) 3474val equal_partition_card = store_thm( 3475 "equal_partition_card", 3476 ``!R s n. FINITE s /\ R equiv_on s /\ (!e. e IN partition R s ==> (CARD e = n)) ==> 3477 (CARD s = n * CARD (partition R s))``, 3478 rw_tac std_ss[partition_CARD, FINITE_partition, GSYM SIGMA_CARD_CONSTANT]); 3479 3480(* Theorem: When the partitions are equal size of n, CARD s = n * CARD (partition of s). 3481 FINITE s /\ R equiv_on s /\ (!e. e IN partition R s ==> (CARD e = n)) ==> 3482 n divides (CARD s) *) 3483(* Proof: by equal_partition_card, divides_def. *) 3484Theorem equal_partition_factor: 3485 !R s n. FINITE s /\ R equiv_on s /\ (!e. e IN partition R s ==> (CARD e = n)) ==> 3486 n divides (CARD s) 3487Proof 3488 metis_tac[equal_partition_card, divides_def, MULT_COMM] 3489QED 3490 3491(* Theorem: When the partition size has a factor n, then n divides CARD s. 3492 FINITE s /\ R equiv_on s /\ 3493 (!e. e IN partition R s ==> n divides (CARD e)) ==> n divides (CARD s) *) 3494(* Proof: 3495 Note FINITE (partition R s) by FINITE_partition 3496 Thus CARD s = SIGMA CARD (partition R s) by partition_CARD 3497 But !e. e IN partition R s ==> n divides (CARD e) 3498 ==> n divides SIGMA CARD (partition R s) by SIGMA_CARD_FACTOR 3499 Hence n divdes CARD s by above 3500*) 3501val factor_partition_card = store_thm( 3502 "factor_partition_card", 3503 ``!R s n. FINITE s /\ R equiv_on s /\ 3504 (!e. e IN partition R s ==> n divides (CARD e)) ==> n divides (CARD s)``, 3505 metis_tac[FINITE_partition, partition_CARD, SIGMA_CARD_FACTOR]); 3506 3507(* Note: 3508When a set s is partitioned by an equivalence relation R, 3509partition_CARD |- !R s. R equiv_on s /\ FINITE s ==> (CARD s = SIGMA CARD (partition R s)) 3510Can this be generalized to: f s = SIGMA f (partition R s) ? 3511If so, we can have (SIGMA f) s = SIGMA (SIGMA f) (partition R s) 3512Sort of yes, but have to use BIGUNION, and for a set_additive function f. 3513*) 3514 3515(* Overload every element finite of a superset *) 3516val _ = overload_on("EVERY_FINITE", ``\P. (!s. s IN P ==> FINITE s)``); 3517 3518(* 3519> FINITE_BIGUNION; 3520val it = |- !P. FINITE P /\ EVERY_FINITE P ==> FINITE (BIGUNION P): thm 3521*) 3522 3523(* Overload pairwise disjoint of a superset *) 3524val _ = overload_on("PAIR_DISJOINT", ``\P. (!s t. s IN P /\ t IN P /\ ~(s = t) ==> DISJOINT s t)``); 3525 3526(* 3527> partition_elements_disjoint; 3528val it = |- R equiv_on s ==> PAIR_DISJOINT (partition R s): thm 3529*) 3530 3531(* Theorem: t SUBSET s /\ PAIR_DISJOINT s ==> PAIR_DISJOINT t *) 3532(* Proof: by SUBSET_DEF *) 3533Theorem pair_disjoint_subset: 3534 !s t. t SUBSET s /\ PAIR_DISJOINT s ==> PAIR_DISJOINT t 3535Proof 3536 rw[SUBSET_DEF] 3537QED 3538 3539(* Overload an additive set function *) 3540val _ = overload_on("SET_ADDITIVE", 3541 ``\f. (f {} = 0) /\ (!s t. FINITE s /\ FINITE t ==> (f (s UNION t) + f (s INTER t) = f s + f t))``); 3542 3543(* Theorem: FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> 3544 !f. SET_ADDITIVE f ==> (f (BIGUNION P) = SIGMA f P) *) 3545(* Proof: 3546 By finite induction on P. 3547 Base: f (BIGUNION {}) = SIGMA f {} 3548 f (BIGUNION {}) 3549 = f {} by BIGUNION_EMPTY 3550 = 0 by SET_ADDITIVE f 3551 = SIGMA f {} = RHS by SUM_IMAGE_EMPTY 3552 Step: e NOTIN P ==> f (BIGUNION (e INSERT P)) = SIGMA f (e INSERT P) 3553 Given !s. s IN e INSERT P ==> FINITE s 3554 thus !s. (s = e) \/ s IN P ==> FINITE s by IN_INSERT 3555 hence FINITE e by implication 3556 and EVERY_FINITE P by IN_INSERT 3557 and FINITE (BIGUNION P) by FINITE_BIGUNION 3558 Given PAIR_DISJOINT (e INSERT P) 3559 so PAIR_DISJOINT P by IN_INSERT 3560 and !s. s IN P ==> DISJOINT e s by IN_INSERT 3561 hence DISJOINT e (BIGUNION P) by DISJOINT_BIGUNION 3562 so e INTER (BIGUNION P) = {} by DISJOINT_DEF 3563 and f (e INTER (BIGUNION P)) = 0 by SET_ADDITIVE f 3564 f (BIGUNION (e INSERT P) 3565 = f (BIGUNION (e INSERT P)) + f (e INTER (BIGUNION P)) by ADD_0 3566 = f e + f (BIGUNION P) by SET_ADDITIVE f 3567 = f e + SIGMA f P by induction hypothesis 3568 = f e + SIGMA f (P DELETE e) by DELETE_NON_ELEMENT 3569 = SIGMA f (e INSERT P) by SUM_IMAGE_THM 3570*) 3571val disjoint_bigunion_add_fun = store_thm( 3572 "disjoint_bigunion_add_fun", 3573 ``!P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> 3574 !f. SET_ADDITIVE f ==> (f (BIGUNION P) = SIGMA f P)``, 3575 `!P. FINITE P ==> EVERY_FINITE P /\ PAIR_DISJOINT P ==> 3576 !f. SET_ADDITIVE f ==> (f (BIGUNION P) = SIGMA f P)` suffices_by rw[] >> 3577 ho_match_mp_tac FINITE_INDUCT >> 3578 rpt strip_tac >- 3579 rw_tac std_ss[BIGUNION_EMPTY, SUM_IMAGE_EMPTY] >> 3580 rw_tac std_ss[BIGUNION_INSERT, SUM_IMAGE_THM] >> 3581 `FINITE e /\ FINITE (BIGUNION P)` by rw[FINITE_BIGUNION] >> 3582 `EVERY_FINITE P /\ PAIR_DISJOINT P` by rw[] >> 3583 `!s. s IN P ==> DISJOINT e s` by metis_tac[IN_INSERT] >> 3584 `f (e INTER (BIGUNION P)) = 0` by metis_tac[DISJOINT_DEF, DISJOINT_BIGUNION] >> 3585 `f (e UNION BIGUNION P) = f (e UNION BIGUNION P) + f (e INTER (BIGUNION P))` by decide_tac >> 3586 `_ = f e + f (BIGUNION P)` by metis_tac[] >> 3587 `_ = f e + SIGMA f P` by prove_tac[] >> 3588 metis_tac[DELETE_NON_ELEMENT]); 3589 3590(* Theorem: SET_ADDITIVE CARD *) 3591(* Proof: 3592 Since CARD {} = 0 by CARD_EMPTY 3593 and !s t. FINITE s /\ FINITE t 3594 ==> CARD (s UNION t) + CARD (s INTER t) = CARD s + CARD t by CARD_UNION 3595 Hence SET_ADDITIVE CARD by notation 3596*) 3597val set_additive_card = store_thm( 3598 "set_additive_card", 3599 ``SET_ADDITIVE CARD``, 3600 rw[FUN_EQ_THM, CARD_UNION]); 3601 3602(* Note: DISJ_BIGUNION_CARD is only a prove_thm in pred_setTheoryScript.sml *) 3603(* 3604g `!P. FINITE P ==> EVERY_FINITE P /\ PAIR_DISJOINT P ==> (CARD (BIGUNION P) = SIGMA CARD P)` 3605e (PSet_ind.SET_INDUCT_TAC FINITE_INDUCT); 3606Q. use of this changes P to s, s to s', how? 3607*) 3608 3609(* Theorem: FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> (CARD (BIGUNION P) = SIGMA CARD P) *) 3610(* Proof: by disjoint_bigunion_add_fun, set_additive_card *) 3611val disjoint_bigunion_card = store_thm( 3612 "disjoint_bigunion_card", 3613 ``!P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> (CARD (BIGUNION P) = SIGMA CARD P)``, 3614 rw[disjoint_bigunion_add_fun, set_additive_card]); 3615 3616(* Theorem: SET_ADDITIVE (SIGMA f) *) 3617(* Proof: 3618 Since SIGMA f {} = 0 by SUM_IMAGE_EMPTY 3619 and !s t. FINITE s /\ FINITE t 3620 ==> SIGMA f (s UNION t) + SIGMA f (s INTER t) = SIGMA f s + SIGMA f t by SUM_IMAGE_UNION_EQN 3621 Hence SET_ADDITIVE (SIGMA f) 3622*) 3623val set_additive_sigma = store_thm( 3624 "set_additive_sigma", 3625 ``!f. SET_ADDITIVE (SIGMA f)``, 3626 rw[SUM_IMAGE_EMPTY, SUM_IMAGE_UNION_EQN]); 3627 3628(* Theorem: FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> !f. SIGMA f (BIGUNION P) = SIGMA (SIGMA f) P *) 3629(* Proof: by disjoint_bigunion_add_fun, set_additive_sigma *) 3630val disjoint_bigunion_sigma = store_thm( 3631 "disjoint_bigunion_sigma", 3632 ``!P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> !f. SIGMA f (BIGUNION P) = SIGMA (SIGMA f) P``, 3633 rw[disjoint_bigunion_add_fun, set_additive_sigma]); 3634 3635(* Theorem: R equiv_on s /\ FINITE s ==> !f. SET_ADDITIVE f ==> (f s = SIGMA f (partition R s)) *) 3636(* Proof: 3637 Let P = partition R s. 3638 Then FINITE s 3639 ==> FINITE P /\ !t. t IN P ==> FINITE t by FINITE_partition 3640 and R equiv_on s 3641 ==> BIGUNION P = s by BIGUNION_partition 3642 ==> PAIR_DISJOINT P by partition_elements_disjoint 3643 Hence f (BIGUNION P) = SIGMA f P by disjoint_bigunion_add_fun 3644 or f s = SIGMA f P by above, BIGUNION_partition 3645*) 3646val set_add_fun_by_partition = store_thm( 3647 "set_add_fun_by_partition", 3648 ``!R s. R equiv_on s /\ FINITE s ==> !f. SET_ADDITIVE f ==> (f s = SIGMA f (partition R s))``, 3649 rpt strip_tac >> 3650 qabbrev_tac `P = partition R s` >> 3651 `FINITE P /\ !t. t IN P ==> FINITE t` by metis_tac[FINITE_partition] >> 3652 `BIGUNION P = s` by rw[BIGUNION_partition, Abbr`P`] >> 3653 `PAIR_DISJOINT P` by metis_tac[partition_elements_disjoint] >> 3654 rw[disjoint_bigunion_add_fun]); 3655 3656(* Theorem: R equiv_on s /\ FINITE s ==> (CARD s = SIGMA CARD (partition R s)) *) 3657(* Proof: by set_add_fun_by_partition, set_additive_card *) 3658val set_card_by_partition = store_thm( 3659 "set_card_by_partition", 3660 ``!R s. R equiv_on s /\ FINITE s ==> (CARD s = SIGMA CARD (partition R s))``, 3661 rw[set_add_fun_by_partition, set_additive_card]); 3662 3663(* This is pred_setTheory.partition_CARD *) 3664 3665(* Theorem: R equiv_on s /\ FINITE s ==> !f. SIGMA f s = SIGMA (SIGMA f) (partition R s) *) 3666(* Proof: by set_add_fun_by_partition, set_additive_sigma *) 3667val set_sigma_by_partition = store_thm( 3668 "set_sigma_by_partition", 3669 ``!R s. R equiv_on s /\ FINITE s ==> !f. SIGMA f s = SIGMA (SIGMA f) (partition R s)``, 3670 rw[set_add_fun_by_partition, set_additive_sigma]); 3671 3672(* Overload a multiplicative set function *) 3673val _ = overload_on("SET_MULTIPLICATIVE", 3674 ``\f. (f {} = 1) /\ (!s t. FINITE s /\ FINITE t ==> (f (s UNION t) * f (s INTER t) = f s * f t))``); 3675 3676(* Theorem: FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> 3677 !f. SET_MULTIPLICATIVE f ==> (f (BIGUNION P) = PI f P) *) 3678(* Proof: 3679 By finite induction on P. 3680 Base: f (BIGUNION {}) = PI f {} 3681 f (BIGUNION {}) 3682 = f {} by BIGUNION_EMPTY 3683 = 1 by SET_MULTIPLICATIVE f 3684 = PI f {} = RHS by PROD_IMAGE_EMPTY 3685 Step: e NOTIN P ==> f (BIGUNION (e INSERT P)) = PI f (e INSERT P) 3686 Given !s. s IN e INSERT P ==> FINITE s 3687 thus !s. (s = e) \/ s IN P ==> FINITE s by IN_INSERT 3688 hence FINITE e by implication 3689 and EVERY_FINITE P by IN_INSERT 3690 and FINITE (BIGUNION P) by FINITE_BIGUNION 3691 Given PAIR_DISJOINT (e INSERT P) 3692 so PAIR_DISJOINT P by IN_INSERT 3693 and !s. s IN P ==> DISJOINT e s by IN_INSERT 3694 hence DISJOINT e (BIGUNION P) by DISJOINT_BIGUNION 3695 so e INTER (BIGUNION P) = {} by DISJOINT_DEF 3696 and f (e INTER (BIGUNION P)) = 1 by SET_MULTIPLICATIVE f 3697 f (BIGUNION (e INSERT P) 3698 = f (BIGUNION (e INSERT P)) * f (e INTER (BIGUNION P)) by MULT_RIGHT_1 3699 = f e * f (BIGUNION P) by SET_MULTIPLICATIVE f 3700 = f e * PI f P by induction hypothesis 3701 = f e * PI f (P DELETE e) by DELETE_NON_ELEMENT 3702 = PI f (e INSERT P) by PROD_IMAGE_THM 3703*) 3704val disjoint_bigunion_mult_fun = store_thm( 3705 "disjoint_bigunion_mult_fun", 3706 ``!P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> 3707 !f. SET_MULTIPLICATIVE f ==> (f (BIGUNION P) = PI f P)``, 3708 `!P. FINITE P ==> EVERY_FINITE P /\ PAIR_DISJOINT P ==> 3709 !f. SET_MULTIPLICATIVE f ==> (f (BIGUNION P) = PI f P)` suffices_by rw[] >> 3710 ho_match_mp_tac FINITE_INDUCT >> 3711 rpt strip_tac >- 3712 rw_tac std_ss[BIGUNION_EMPTY, PROD_IMAGE_EMPTY] >> 3713 rw_tac std_ss[BIGUNION_INSERT, PROD_IMAGE_THM] >> 3714 `FINITE e /\ FINITE (BIGUNION P)` by rw[FINITE_BIGUNION] >> 3715 `EVERY_FINITE P /\ PAIR_DISJOINT P` by rw[] >> 3716 `!s. s IN P ==> DISJOINT e s` by metis_tac[IN_INSERT] >> 3717 `f (e INTER (BIGUNION P)) = 1` by metis_tac[DISJOINT_DEF, DISJOINT_BIGUNION] >> 3718 `f (e UNION BIGUNION P) = f (e UNION BIGUNION P) * f (e INTER (BIGUNION P))` by metis_tac[MULT_RIGHT_1] >> 3719 `_ = f e * f (BIGUNION P)` by metis_tac[] >> 3720 `_ = f e * PI f P` by prove_tac[] >> 3721 metis_tac[DELETE_NON_ELEMENT]); 3722 3723(* Theorem: R equiv_on s /\ FINITE s ==> !f. SET_MULTIPLICATIVE f ==> (f s = PI f (partition R s)) *) 3724(* Proof: 3725 Let P = partition R s. 3726 Then FINITE s 3727 ==> FINITE P /\ EVERY_FINITE P by FINITE_partition 3728 and R equiv_on s 3729 ==> BIGUNION P = s by BIGUNION_partition 3730 ==> PAIR_DISJOINT P by partition_elements_disjoint 3731 Hence f (BIGUNION P) = PI f P by disjoint_bigunion_mult_fun 3732 or f s = PI f P by above, BIGUNION_partition 3733*) 3734val set_mult_fun_by_partition = store_thm( 3735 "set_mult_fun_by_partition", 3736 ``!R s. R equiv_on s /\ FINITE s ==> !f. SET_MULTIPLICATIVE f ==> (f s = PI f (partition R s))``, 3737 rpt strip_tac >> 3738 qabbrev_tac `P = partition R s` >> 3739 `FINITE P /\ !t. t IN P ==> FINITE t` by metis_tac[FINITE_partition] >> 3740 `BIGUNION P = s` by rw[BIGUNION_partition, Abbr`P`] >> 3741 `PAIR_DISJOINT P` by metis_tac[partition_elements_disjoint] >> 3742 rw[disjoint_bigunion_mult_fun]); 3743 3744(* Theorem: FINITE s ==> !g. INJ g s univ(:'a) ==> !f. SIGMA f (IMAGE g s) = SIGMA (f o g) s *) 3745(* Proof: 3746 By finite induction on s. 3747 Base: SIGMA f (IMAGE g {}) = SIGMA (f o g) {} 3748 LHS = SIGMA f (IMAGE g {}) 3749 = SIGMA f {} by IMAGE_EMPTY 3750 = 0 by SUM_IMAGE_EMPTY 3751 = SIGMA (f o g) {} = RHS by SUM_IMAGE_EMPTY 3752 Step: e NOTIN s ==> SIGMA f (IMAGE g (e INSERT s)) = SIGMA (f o g) (e INSERT s) 3753 Note INJ g (e INSERT s) univ(:'a) 3754 ==> INJ g s univ(:'a) /\ g e IN univ(:'a) /\ 3755 !y. y IN s /\ (g e = g y) ==> (e = y) by INJ_INSERT 3756 Thus g e NOTIN (IMAGE g s) by IN_IMAGE 3757 SIGMA f (IMAGE g (e INSERT s)) 3758 = SIGMA f (g e INSERT IMAGE g s) by IMAGE_INSERT 3759 = f (g e) + SIGMA f (IMAGE g s) by SUM_IMAGE_THM, g e NOTIN (IMAGE g s) 3760 = f (g e) + SIGMA (f o g) s by induction hypothesis 3761 = (f o g) e + SIGMA (f o g) s by composition 3762 = SIGMA (f o g) (e INSERT s) by SUM_IMAGE_THM, e NOTIN s 3763*) 3764val sum_image_by_composition = store_thm( 3765 "sum_image_by_composition", 3766 ``!s. FINITE s ==> !g. INJ g s univ(:'a) ==> !f. SIGMA f (IMAGE g s) = SIGMA (f o g) s``, 3767 ho_match_mp_tac FINITE_INDUCT >> 3768 rpt strip_tac >- 3769 rw[SUM_IMAGE_EMPTY] >> 3770 `INJ g s univ(:'a) /\ g e IN univ(:'a) /\ !y. y IN s /\ (g e = g y) ==> (e = y)` by metis_tac[INJ_INSERT] >> 3771 `g e NOTIN (IMAGE g s)` by metis_tac[IN_IMAGE] >> 3772 `(s DELETE e = s) /\ (IMAGE g s DELETE g e = IMAGE g s)` by metis_tac[DELETE_NON_ELEMENT] >> 3773 rw[SUM_IMAGE_THM]); 3774 3775(* Overload on permutation *) 3776val _ = overload_on("PERMUTES", ``\f s. BIJ f s s``); 3777val _ = set_fixity "PERMUTES" (Infix(NONASSOC, 450)); (* same as relation *) 3778 3779(* Theorem: FINITE s ==> !g. g PERMUTES s ==> !f. SIGMA (f o g) s = SIGMA f s *) 3780(* Proof: 3781 Given permutate g s = BIJ g s s by notation 3782 ==> INJ g s s /\ SURJ g s s by BIJ_DEF 3783 Now SURJ g s s ==> IMAGE g s = s by IMAGE_SURJ 3784 Also s SUBSET univ(:'a) by SUBSET_UNIV 3785 and s SUBSET s by SUBSET_REFL 3786 Hence INJ g s univ(:'a) by INJ_SUBSET 3787 With FINITE s, 3788 SIGMA (f o g) s 3789 = SIGMA f (IMAGE g s) by sum_image_by_composition 3790 = SIGMA f s by above 3791*) 3792val sum_image_by_permutation = store_thm( 3793 "sum_image_by_permutation", 3794 ``!s. FINITE s ==> !g. g PERMUTES s ==> !f. SIGMA (f o g) s = SIGMA f s``, 3795 rpt strip_tac >> 3796 `INJ g s s /\ SURJ g s s` by metis_tac[BIJ_DEF] >> 3797 `IMAGE g s = s` by rw[GSYM IMAGE_SURJ] >> 3798 `s SUBSET univ(:'a)` by rw[SUBSET_UNIV] >> 3799 `INJ g s univ(:'a)` by metis_tac[INJ_SUBSET, SUBSET_REFL] >> 3800 `SIGMA (f o g) s = SIGMA f (IMAGE g s)` by rw[sum_image_by_composition] >> 3801 rw[]); 3802 3803(* Theorem: FINITE s ==> !f:('b -> bool) -> num. (f {} = 0) ==> 3804 !g. (!t. FINITE t /\ (!x. x IN t ==> g x <> {}) ==> INJ g t univ(:num -> bool)) ==> 3805 (SIGMA f (IMAGE g s) = SIGMA (f o g) s) *) 3806(* Proof: 3807 Let s1 = {x | x IN s /\ (g x = {})}, 3808 s2 = {x | x IN s /\ (g x <> {})}. 3809 Then s = s1 UNION s2 by EXTENSION 3810 and DISJOINT s1 s2 by EXTENSION, DISJOINT_DEF 3811 and DISJOINT (IMAGE g s1) (IMAGE g s2) by EXTENSION, DISJOINT_DEF 3812 Now s1 SUBSET s /\ s1 SUBSET s by SUBSET_DEF 3813 Since FINITE s by given 3814 thus FINITE s1 /\ FINITE s2 by SUBSET_FINITE 3815 and FINITE (IMAGE g s1) /\ FINITE (IMAGE g s2) by IMAGE_FINITE 3816 3817 Step 1: decompose left summation 3818 SIGMA f (IMAGE g s) 3819 = SIGMA f (IMAGE g (s1 UNION s2)) by above, s = s1 UNION s2 3820 = SIGMA f ((IMAGE g s1) UNION (IMAGE g s2)) by IMAGE_UNION 3821 = SIGMA f (IMAGE g s1) + SIGMA f (IMAGE g s2) by SUM_IMAGE_DISJOINT 3822 3823 Claim: SIGMA f (IMAGE g s1) = 0 3824 Proof: If s1 = {}, 3825 SIGMA f (IMAGE g {}) 3826 = SIGMA f {} by IMAGE_EMPTY 3827 = 0 by SUM_IMAGE_EMPTY 3828 If s1 <> {}, 3829 Note !x. x IN s1 ==> (g x = {}) by definition of s1 3830 Thus !y. y IN (IMAGE g s1) ==> (y = {}) by IN_IMAGE, IMAGE_EMPTY 3831 Since s1 <> {}, IMAGE g s1 = {{}} by SING_DEF, IN_SING, SING_ONE_ELEMENT 3832 SIGMA f (IMAGE g {}) 3833 = SIGMA f {{}} by above 3834 = f {} by SUM_IMAGE_SING 3835 = 0 by given 3836 3837 Step 2: decompose right summation 3838 Also SIGMA (f o g) s 3839 = SIGMA (f o g) (s1 UNION s2) by above, s = s1 UNION s2 3840 = SIGMA (f o g) s1 + SIGMA (f o g) s2 by SUM_IMAGE_DISJOINT 3841 3842 Claim: SIGMA (f o g) s1 = 0 3843 Proof: Note !x. x IN s1 ==> (g x = {}) by definition of s1 3844 (f o g) x 3845 = f (g x) by function application 3846 = f {} by above 3847 = 0 by given 3848 Hence SIGMA (f o g) s1 3849 = 0 * CARD s1 by SIGMA_CONSTANT 3850 = 0 by MULT 3851 3852 Claim: SIGMA f (IMAGE g s2) = SIGMA (f o g) s2 3853 Proof: Note !x. x IN s2 ==> g x <> {} by definition of s2 3854 Thus INJ g s2 univ(:'b -> bool) by given 3855 Hence SIGMA f (IMAGE g s2) 3856 = SIGMA (f o g) (s2) by sum_image_by_composition 3857 3858 Result follows by combining all the claims and arithmetic. 3859*) 3860val sum_image_by_composition_with_partial_inj = store_thm( 3861 "sum_image_by_composition_with_partial_inj", 3862 ``!s. FINITE s ==> !f:('b -> bool) -> num. (f {} = 0) ==> 3863 !g. (!t. FINITE t /\ (!x. x IN t ==> g x <> {}) ==> INJ g t univ(:'b -> bool)) ==> 3864 (SIGMA f (IMAGE g s) = SIGMA (f o g) s)``, 3865 rpt strip_tac >> 3866 qabbrev_tac `s1 = {x | x IN s /\ (g x = {})}` >> 3867 qabbrev_tac `s2 = {x | x IN s /\ (g x <> {})}` >> 3868 (`s = s1 UNION s2` by (rw[Abbr`s1`, Abbr`s2`, EXTENSION] >> metis_tac[])) >> 3869 (`DISJOINT s1 s2` by (rw[Abbr`s1`, Abbr`s2`, EXTENSION, DISJOINT_DEF] >> metis_tac[])) >> 3870 (`DISJOINT (IMAGE g s1) (IMAGE g s2)` by (rw[Abbr`s1`, Abbr`s2`, EXTENSION, DISJOINT_DEF] >> metis_tac[])) >> 3871 `s1 SUBSET s /\ s2 SUBSET s` by rw[Abbr`s1`, Abbr`s2`, SUBSET_DEF] >> 3872 `FINITE s1 /\ FINITE s2` by metis_tac[SUBSET_FINITE] >> 3873 `FINITE (IMAGE g s1) /\ FINITE (IMAGE g s2)` by rw[] >> 3874 `SIGMA f (IMAGE g s) = SIGMA f ((IMAGE g s1) UNION (IMAGE g s2))` by rw[] >> 3875 `_ = SIGMA f (IMAGE g s1) + SIGMA f (IMAGE g s2)` by rw[SUM_IMAGE_DISJOINT] >> 3876 `SIGMA f (IMAGE g s1) = 0` by 3877 (Cases_on `s1 = {}` >- 3878 rw[SUM_IMAGE_EMPTY] >> 3879 `!x. x IN s1 ==> (g x = {})` by rw[Abbr`s1`] >> 3880 `!y. y IN (IMAGE g s1) ==> (y = {})` by metis_tac[IN_IMAGE, IMAGE_EMPTY] >> 3881 `{} IN {{}} /\ IMAGE g s1 <> {}` by rw[] >> 3882 `IMAGE g s1 = {{}}` by metis_tac[SING_DEF, IN_SING, SING_ONE_ELEMENT] >> 3883 `SIGMA f (IMAGE g s1) = f {}` by rw[SUM_IMAGE_SING] >> 3884 rw[] 3885 ) >> 3886 `SIGMA (f o g) s = SIGMA (f o g) s1 + SIGMA (f o g) s2` by rw[SUM_IMAGE_DISJOINT] >> 3887 `SIGMA (f o g) s1 = 0` by 3888 (`!x. x IN s1 ==> (g x = {})` by rw[Abbr`s1`] >> 3889 `!x. x IN s1 ==> ((f o g) x = 0)` by rw[] >> 3890 metis_tac[SIGMA_CONSTANT, MULT]) >> 3891 `SIGMA f (IMAGE g s2) = SIGMA (f o g) s2` by 3892 (`!x. x IN s2 ==> g x <> {}` by rw[Abbr`s2`] >> 3893 `INJ g s2 univ(:'b -> bool)` by rw[] >> 3894 rw[sum_image_by_composition]) >> 3895 decide_tac); 3896 3897(* Theorem: FINITE s ==> !f g. (!x y. x IN s /\ y IN s /\ (g x = g y) ==> (x = y) \/ (f (g x) = 0)) ==> 3898 (SIGMA f (IMAGE g s) = SIGMA (f o g) s) *) 3899(* Proof: 3900 By finite induction on s. 3901 Base: SIGMA f (IMAGE g {}) = SIGMA (f o g) {} 3902 SIGMA f (IMAGE g {}) 3903 = SIGMA f {} by IMAGE_EMPTY 3904 = 0 by SUM_IMAGE_EMPTY 3905 = SIGMA (f o g) {} by SUM_IMAGE_EMPTY 3906 Step: !f g. (!x y. x IN s /\ y IN s /\ (g x = g y) ==> (x = y) \/ (f (g x) = 0)) ==> 3907 (SIGMA f (IMAGE g s) = SIGMA (f o g) s) ==> 3908 e NOTIN s /\ !x y. x IN e INSERT s /\ y IN e INSERT s /\ (g x = g y) ==> (x = y) \/ (f (g x) = 0) 3909 ==> SIGMA f (IMAGE g (e INSERT s)) = SIGMA (f o g) (e INSERT s) 3910 Note !x y. ((x = e) \/ x IN s) /\ ((y = e) \/ y IN s) /\ (g x = g y) ==> 3911 (x = y) \/ (f (g y) = 0) by IN_INSERT 3912 If g e IN IMAGE g s, 3913 Then ?x. x IN s /\ (g x = g e) by IN_IMAGE 3914 and x <> e /\ (f (g e) = 0) by implication 3915 SIGMA f (g e INSERT IMAGE g s) 3916 = SIGMA f (IMAGE g s) by ABSORPTION, g e IN IMAGE g s 3917 = SIGMA (f o g) s by induction hypothesis 3918 = f (g x) + SIGMA (f o g) s by ADD 3919 = (f o g) e + SIGMA (f o g) s by o_THM 3920 = SIGMA (f o g) (e INSERT s) by SUM_IMAGE_INSERT, e NOTIN s 3921 If g e NOTIN IMAGE g s, 3922 SIGMA f (g e INSERT IMAGE g s) 3923 = f (g e) + SIGMA f (IMAGE g s) by SUM_IMAGE_INSERT, g e NOTIN IMAGE g s 3924 = f (g e) + SIGMA (f o g) s by induction hypothesis 3925 = (f o g) e + SIGMA (f o g) s by o_THM 3926 = SIGMA (f o g) (e INSERT s) by SUM_IMAGE_INSERT, e NOTIN s 3927*) 3928val sum_image_by_composition_without_inj = store_thm( 3929 "sum_image_by_composition_without_inj", 3930 ``!s. FINITE s ==> !f g. (!x y. x IN s /\ y IN s /\ (g x = g y) ==> (x = y) \/ (f (g x) = 0)) ==> 3931 (SIGMA f (IMAGE g s) = SIGMA (f o g) s)``, 3932 Induct_on `FINITE` >> 3933 rpt strip_tac >- 3934 rw[SUM_IMAGE_EMPTY] >> 3935 fs[] >> 3936 Cases_on `g e IN IMAGE g s` >| [ 3937 `?x. x IN s /\ (g x = g e)` by metis_tac[IN_IMAGE] >> 3938 `x <> e /\ (f (g e) = 0)` by metis_tac[] >> 3939 `SIGMA f (g e INSERT IMAGE g s) = SIGMA f (IMAGE g s)` by metis_tac[ABSORPTION] >> 3940 `_ = SIGMA (f o g) s` by rw[] >> 3941 `_ = (f o g) e + SIGMA (f o g) s` by rw[] >> 3942 `_ = SIGMA (f o g) (e INSERT s)` by rw[SUM_IMAGE_INSERT] >> 3943 rw[], 3944 `SIGMA f (g e INSERT IMAGE g s) = f (g e) + SIGMA f (IMAGE g s)` by rw[SUM_IMAGE_INSERT] >> 3945 `_ = f (g e) + SIGMA (f o g) s` by rw[] >> 3946 `_ = (f o g) e + SIGMA (f o g) s` by rw[] >> 3947 `_ = SIGMA (f o g) (e INSERT s)` by rw[SUM_IMAGE_INSERT] >> 3948 rw[] 3949 ]); 3950 3951(* ------------------------------------------------------------------------- *) 3952(* Pre-image Theorems. *) 3953(* ------------------------------------------------------------------------- *) 3954 3955(* 3956- IN_IMAGE; 3957> val it = |- !y s f. y IN IMAGE f s <=> ?x. (y = f x) /\ x IN s : thm 3958*) 3959 3960(* Define preimage *) 3961val preimage_def = Define `preimage f s y = { x | x IN s /\ (f x = y) }`; 3962 3963(* Theorem: x IN (preimage f s y) <=> x IN s /\ (f x = y) *) 3964(* Proof: by preimage_def *) 3965val preimage_element = store_thm( 3966 "preimage_element", 3967 ``!f s x y. x IN (preimage f s y) <=> x IN s /\ (f x = y)``, 3968 rw[preimage_def]); 3969 3970(* Theorem: x IN preimage f s y <=> (x IN s /\ (f x = y)) *) 3971(* Proof: by preimage_def *) 3972val in_preimage = store_thm( 3973 "in_preimage", 3974 ``!f s x y. x IN preimage f s y <=> (x IN s /\ (f x = y))``, 3975 rw[preimage_def]); 3976(* same as theorem above. *) 3977 3978(* Theorem: preimage f s y SUBSET s *) 3979(* Proof: by definition. *) 3980val preimage_subset_of_domain = store_thm( 3981 "preimage_subset_of_domain", 3982 ``!f s y. preimage f s y SUBSET s``, 3983 rw[preimage_def, SUBSET_DEF]); 3984 3985(* export trivial truth -- but not frequently used. *) 3986(* val _ = export_rewrites ["preimage_subset_of_domain"]; *) 3987 3988(* Theorem: !x. x IN preimage f s y ==> f x = y *) 3989(* Proof: by definition. *) 3990val preimage_property = store_thm( 3991 "preimage_property", 3992 ``!f s y. !x. x IN preimage f s y ==> (f x = y)``, 3993 rw[preimage_def]); 3994 3995(* This is bad: every pattern of f x = y (i.e. practically every equality!) will invoke the check: x IN preimage f s y! *) 3996(* val _ = export_rewrites ["preimage_property"]; *) 3997 3998(* Theorem: x IN s ==> x IN preimage f s (f x) *) 3999(* Proof: by IN_IMAGE. preimage_def. *) 4000val preimage_of_image = store_thm( 4001 "preimage_of_image", 4002 ``!f s x. x IN s ==> x IN preimage f s (f x)``, 4003 rw[preimage_def]); 4004 4005(* Theorem: y IN (IMAGE f s) ==> CHOICE (preimage f s y) IN s /\ f (CHOICE (preimage f s y)) = y *) 4006(* Proof: 4007 (1) prove: y IN IMAGE f s ==> CHOICE (preimage f s y) IN s 4008 By IN_IMAGE, this is to show: 4009 x IN s ==> CHOICE (preimage f s (f x)) IN s 4010 Now, preimage f s (f x) <> {} since x is a pre-image. 4011 hence CHOICE (preimage f s (f x)) IN preimage f s (f x) by CHOICE_DEF 4012 hence CHOICE (preimage f s (f x)) IN s by preimage_def 4013 (2) prove: y IN IMAGE f s /\ CHOICE (preimage f s y) IN s ==> f (CHOICE (preimage f s y)) = y 4014 By IN_IMAGE, this is to show: x IN s ==> f (CHOICE (preimage f s (f x))) = f x 4015 Now, x IN preimage f s (f x) by preimage_of_image 4016 hence preimage f s (f x) <> {} by MEMBER_NOT_EMPTY 4017 thus CHOICE (preimage f s (f x)) IN (preimage f s (f x)) by CHOICE_DEF 4018 hence f (CHOICE (preimage f s (f x))) = f x by preimage_def 4019*) 4020val preimage_choice_property = store_thm( 4021 "preimage_choice_property", 4022 ``!f s y. y IN (IMAGE f s) ==> CHOICE (preimage f s y) IN s /\ (f (CHOICE (preimage f s y)) = y)``, 4023 rpt gen_tac >> 4024 strip_tac >> 4025 conj_asm1_tac >| [ 4026 full_simp_tac std_ss [IN_IMAGE] >> 4027 `CHOICE (preimage f s (f x)) IN preimage f s (f x)` suffices_by rw[preimage_def] >> 4028 metis_tac[CHOICE_DEF, preimage_of_image, MEMBER_NOT_EMPTY], 4029 full_simp_tac std_ss [IN_IMAGE] >> 4030 `x IN preimage f s (f x)` by rw_tac std_ss[preimage_of_image] >> 4031 `CHOICE (preimage f s (f x)) IN (preimage f s (f x))` by metis_tac[CHOICE_DEF, MEMBER_NOT_EMPTY] >> 4032 full_simp_tac std_ss [preimage_def, GSPECIFICATION] 4033 ]); 4034 4035(* Theorem: INJ f s univ(:'b) ==> !x. x IN s ==> (preimage f s (f x) = {x}) *) 4036(* Proof: 4037 preimage f s (f x) 4038 = {x' | x' IN s /\ (f x' = f x)} by preimage_def 4039 = {x' | x' IN s /\ (x' = x)} by INJ_DEF 4040 = {x} by EXTENSION 4041*) 4042val preimage_inj = store_thm( 4043 "preimage_inj", 4044 ``!f s. INJ f s univ(:'b) ==> !x. x IN s ==> (preimage f s (f x) = {x})``, 4045 rw[preimage_def, EXTENSION] >> 4046 metis_tac[INJ_DEF]); 4047 4048(* Theorem: INJ f s univ(:'b) ==> !x. x IN s ==> (CHOICE (preimage f s (f x)) = x) *) 4049(* Proof: 4050 CHOICE (preimage f s (f x)) 4051 = CHOICE {x} by preimage_inj, INJ f s univ(:'b) 4052 = x by CHOICE_SING 4053*) 4054val preimage_inj_choice = store_thm( 4055 "preimage_inj_choice", 4056 ``!f s. INJ f s univ(:'b) ==> !x. x IN s ==> (CHOICE (preimage f s (f x)) = x)``, 4057 rw[preimage_inj]); 4058 4059(* ------------------------------------------------------------------------- *) 4060(* Set of Proper Subsets *) 4061(* ------------------------------------------------------------------------- *) 4062 4063(* Define the set of all proper subsets of a set *) 4064val _ = overload_on ("PPOW", ``\s. (POW s) DIFF {s}``); 4065 4066(* Theorem: !s e. e IN PPOW s ==> e PSUBSET s *) 4067(* Proof: 4068 e IN PPOW s 4069 = e IN ((POW s) DIFF {s}) by notation 4070 = (e IN POW s) /\ e NOTIN {s} by IN_DIFF 4071 = (e SUBSET s) /\ e NOTIN {s} by IN_POW 4072 = (e SUBSET s) /\ e <> s by IN_SING 4073 = e PSUBSET s by PSUBSET_DEF 4074*) 4075val IN_PPOW = store_thm( 4076 "IN_PPOW", 4077 ``!s e. e IN PPOW s ==> e PSUBSET s``, 4078 rw[PSUBSET_DEF, IN_POW]); 4079 4080(* Theorem: FINITE (PPOW s) *) 4081(* Proof: 4082 Since PPOW s = (POW s) DIFF {s}, 4083 FINITE s 4084 ==> FINITE (POW s) by FINITE_POW 4085 ==> FINITE ((POW s) DIFF {s}) by FINITE_DIFF 4086 ==> FINITE (PPOW s) by above 4087*) 4088val FINITE_PPOW = store_thm( 4089 "FINITE_PPOW", 4090 ``!s. FINITE s ==> FINITE (PPOW s)``, 4091 rw[FINITE_POW]); 4092 4093(* Theorem: FINITE s ==> CARD (PPOW s) = PRE (2 ** CARD s) *) 4094(* Proof: 4095 CARD (PPOW s) 4096 = CARD ((POW s) DIFF {s}) by notation 4097 = CARD (POW s) - CARD ((POW s) INTER {s}) by CARD_DIFF 4098 = CARD (POW s) - CARD {s} by INTER_SING, since s IN POW s 4099 = 2 ** CARD s - CARD {s} by CARD_POW 4100 = 2 ** CARD s - 1 by CARD_SING 4101 = PRE (2 ** CARD s) by PRE_SUB1 4102*) 4103val CARD_PPOW = store_thm( 4104 "CARD_PPOW", 4105 ``!s. FINITE s ==> (CARD (PPOW s) = PRE (2 ** CARD s))``, 4106 rpt strip_tac >> 4107 `FINITE {s}` by rw[FINITE_SING] >> 4108 `FINITE (POW s)` by rw[FINITE_POW] >> 4109 `s IN (POW s)` by rw[IN_POW, SUBSET_REFL] >> 4110 `CARD (PPOW s) = CARD (POW s) - CARD ((POW s) INTER {s})` by rw[CARD_DIFF] >> 4111 `_ = CARD (POW s) - CARD {s}` by rw[INTER_SING] >> 4112 `_ = 2 ** CARD s - CARD {s}` by rw[CARD_POW] >> 4113 `_ = 2 ** CARD s - 1` by rw[CARD_SING] >> 4114 `_ = PRE (2 ** CARD s)` by rw[PRE_SUB1] >> 4115 rw[]); 4116 4117(* Theorem: FINITE s ==> CARD (PPOW s) = PRE (2 ** CARD s) *) 4118(* Proof: by CARD_PPOW *) 4119val CARD_PPOW_EQN = store_thm( 4120 "CARD_PPOW_EQN", 4121 ``!s. FINITE s ==> (CARD (PPOW s) = (2 ** CARD s) - 1)``, 4122 rw[CARD_PPOW]); 4123 4124(* ------------------------------------------------------------------------- *) 4125(* Useful Theorems *) 4126(* ------------------------------------------------------------------------- *) 4127 4128(* Note: 4129> type_of ``prime``; 4130val it = ":num -> bool": hol_type 4131 4132Thus prime is also a set, or prime = {p | prime p} 4133*) 4134 4135(* Theorem: p IN prime <=> prime p *) 4136(* Proof: by IN_DEF *) 4137val in_prime = store_thm( 4138 "in_prime", 4139 ``!p. p IN prime <=> prime p``, 4140 rw[IN_DEF]); 4141 4142(* Theorem: (Generalized Euclid's Lemma) 4143 If prime p divides a PROD_SET, it divides a member of the PROD_SET. 4144 FINITE s ==> !p. prime p /\ p divides (PROD_SET s) ==> ?b. b IN s /\ p divides b *) 4145(* Proof: by induction of the PROD_SET, apply Euclid's Lemma. 4146- P_EUCLIDES; 4147> val it = 4148 |- !p a b. prime p /\ p divides (a * b) ==> p divides a \/ p divides b : thm 4149 By finite induction on s. 4150 Base case: prime p /\ p divides (PROD_SET {}) ==> F 4151 Since PROD_SET {} = 1 by PROD_SET_THM 4152 and p divides 1 <=> p = 1 by DIVIDES_ONE 4153 but prime p ==> p <> 1 by NOT_PRIME_1 4154 This gives the contradiction. 4155 Step case: FINITE s /\ (!p. prime p /\ p divides (PROD_SET s) ==> ?b. b IN s /\ p divides b) /\ 4156 e NOTIN s /\ prime p /\ p divides (PROD_SET (e INSERT s)) ==> 4157 ?b. ((b = e) \/ b IN s) /\ p divides b 4158 Note PROD_SET (e INSERT s) = e * PROD_SET s by PROD_SET_THM, DELETE_NON_ELEMENT, e NOTIN s. 4159 So prime p /\ p divides (PROD_SET (e INSERT s)) 4160 ==> p divides e, or p divides (PROD_SET s) by P_EUCLIDES 4161 If p divides e, just take b = e. 4162 If p divides (PROD_SET s), there is such b by induction hypothesis 4163*) 4164val PROD_SET_EUCLID = store_thm( 4165 "PROD_SET_EUCLID", 4166 ``!s. FINITE s ==> !p. prime p /\ p divides (PROD_SET s) ==> ?b. b IN s /\ p divides b``, 4167 ho_match_mp_tac FINITE_INDUCT >> 4168 rw[] >- 4169 metis_tac[PROD_SET_EMPTY, DIVIDES_ONE, NOT_PRIME_1] >> 4170 `PROD_SET (e INSERT s) = e * PROD_SET s` 4171 by metis_tac[PROD_SET_THM, DELETE_NON_ELEMENT] >> 4172 Cases_on `p divides e` >- 4173 metis_tac[] >> 4174 metis_tac[P_EUCLIDES]); 4175 4176(* ------------------------------------------------------------------------- *) 4177 4178(* export theory at end *) 4179val _ = export_theory(); 4180 4181(*===========================================================================*) 4182