1(* ------------------------------------------------------------------------- *) 2(* Group Theory -- Iterated Product. *) 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 "groupProduct"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* val _ = load "jcLib"; *) 17open jcLib; 18 19(* open dependent theories *) 20open pred_setTheory arithmeticTheory; 21 22(* Get dependent theories local *) 23(* val _ = load "groupTheory"; *) 24open groupTheory monoidTheory; 25open monoidOrderTheory; 26 27(* val _ = load "subgroupTheory"; *) 28open submonoidTheory; 29open subgroupTheory; 30 31(* Get dependent theories in lib *) 32(* (* val _ = load "helperSetTheory"; loaded by monoidTheory *) *) 33open helperSetTheory; 34 35(* Load dependent theories *) 36(* val _ = load "Satisfysimps"; *) 37(* used in coset_id_eq_subgroup: srw_tac[SatisfySimps.SATISFY_ss] *) 38 39 40(* ------------------------------------------------------------------------- *) 41(* Iterated Product Documentation *) 42(* ------------------------------------------------------------------------- *) 43(* Overloading (# is temporary): 44 FUN_COMM op f = !x y z. op (f x) (op (f y) z) = op (f y) (op (f x) z) 45# GPI f s = GROUP_IMAGE g f s 46# gfun f = group_fun g f 47*) 48(* Definitions and Theorems (# are exported): 49 50 Fermat's Little Theorem of Abelian Groups: 51 GPROD_SET_IMAGE |- !g a. Group g /\ a IN G ==> (GPROD_SET g (a * G) = GPROD_SET g G) 52 GPROD_SET_REDUCTION_INSERT |- !g s. FiniteAbelianGroup g /\ s SUBSET G ==> 53 !a x::(G). x NOTIN s ==> 54 (a * x * GPROD_SET g (a * (G DIFF (x INSERT s))) = GPROD_SET g (a * (G DIFF s))) 55 GPROD_SET_REDUCTION |- !g s. FiniteAbelianGroup g /\ s SUBSET G ==> 56 !a::(G). a ** CARD s * GPROD_SET g s * GPROD_SET g (a * (G DIFF s)) = GPROD_SET g G 57 58 Group Factorial: 59 GFACT_def |- !g. GFACT g = GPROD_SET g G 60 GFACT_element |- !g. FiniteAbelianMonoid g ==> GFACT g IN G 61 GFACT_identity |- !g a. FiniteAbelianGroup g /\ a IN G ==> (GFACT g = a ** CARD G * GFACT g) 62 finite_abelian_Fermat |- !g a. FiniteAbelianGroup g /\ a IN G ==> (a ** CARD G = #e) 63 64 Group Iterated Product over a function: 65 OP_IMAGE_DEF |- !op id f s. OP_IMAGE op id f s = ITSET (\e acc. op (f e) acc) s id 66 OP_IMAGE_EMPTY |- !op id f. OP_IMAGE op id f {} = id 67 OP_IMAGE_SING |- !op id f x. OP_IMAGE op id f {x} = op (f x) id 68 OP_IMAGE_THM |- !op id f. (OP_IMAGE op id f {} = id) /\ 69 (FUN_COMM op f ==> !s. FINITE s ==> 70 !e. OP_IMAGE op id f (e INSERT s) = op (f e) (OP_IMAGE op id f (s DELETE e))) 71 72 GROUP_IMAGE_DEF |- !g f s. GPI f s = ITSET (\e acc. f e * acc) s #e 73 group_image_as_op_image |- !g. GPI = OP_IMAGE $* #e 74 sum_image_as_op_image |- SIGMA = OP_IMAGE (\x y. x + y) 0 75 prod_image_as_op_image |- PI = OP_IMAGE (\x y. x * y) 1 76 GITSET_AS_ITSET |- !g. (\s b. GITSET g s b) = ITSET (\e acc. e * acc) 77 GPROD_SET_AS_GROUP_IMAGE |- !g. GPROD_SET g = GPI I 78 group_image_empty |- !g f. GPI f {} = #e 79 group_fun_def |- !g f. gfun f <=> !x. x IN G ==> f x IN G 80 group_image_sing |- !g. Monoid g ==> !f. gfun f ==> !x. x IN G ==> (GPI f {x} = f x) 81 82*) 83 84 85(* ------------------------------------------------------------------------- *) 86(* Fermat's Little Theorem of Abelian Groups. *) 87(* ------------------------------------------------------------------------- *) 88 89(* Theorem: For Group g, a IN G ==> GPROD_SET g a * G = GPROD_SET g G *) 90(* Proof: 91 This is trivial by group_coset_eq_itself. 92*) 93val GPROD_SET_IMAGE = store_thm( 94 "GPROD_SET_IMAGE", 95 ``!g a. Group g /\ a IN G ==> (GPROD_SET g (a * G) = GPROD_SET g G)``, 96 rw[group_coset_eq_itself]); 97 98(* ------------------------------------------------------------------------- *) 99(* An Invariant Property when reducing GPROD_SET g (IMAGE (\z. a*z) G): 100 GPROD_SET g (IMAGE (\z. a*z) G) 101 = (a*z) * GPROD_SET g ((IMAGE (\z. a*z) G) DELETE (a*z)) 102 = a * (GPROD_SET g (z INSERT {})) * GPROD_SET g (IMAGE (\z. a*z) (G DELETE z)) 103 = a * <building up a GPROD_SET> * <reducing down a GPROD_SET> 104 = a*a * <building one more> * <reducing one more> 105 = a*a*a * <building one more> * <reducing one more> 106 = a**(CARD G) * GPROD_SET g G * GPROD_SET g {} 107 = a**(CARD G) * GPROD_SET g G * #e 108 = a**(CARD G) * GPROD_SET g G 109*) 110(* ------------------------------------------------------------------------- *) 111 112(* Theorem: [INSERT for GPROD_SET_REDUCTION] 113 (a*x)* GPROD_SET g (coset g (G DIFF (x INSERT t))) 114 = GPROD_SET g (coset g (G DIFF t)) *) 115(* Proof: 116 Essentially this is to prove: 117 a * x * GPROD_SET g {a * z | z | z IN G /\ z <> x /\ z NOTIN s} = 118 GPROD_SET g {a * z | z | z IN G /\ z NOTIN s} 119 Let q = {a * z | z | z IN G /\ z <> x /\ z NOTIN s} 120 p = {a * z | z | z IN G /\ z NOTIN s} 121 Since p = (a*x) INSERT q by EXTENSION, 122 and (a*x) NOTIN q by group_lcancel, a NOTIN s. 123 and (a*x) IN G by group_op_element 124 RHS = GPROD_SET g p 125 = GPROD_SET g ((a*x) INSERT q) by p = (a*x) INSERT q 126 = (a*x) * GPROD_SET g (q DELETE (a*x)) by GPROD_SET_THM 127 = (a*x) * GPROD_SET g q by DELETE_NON_ELEMENT, (a*x) NOTIN q. 128 = LHS 129*) 130val GPROD_SET_REDUCTION_INSERT = store_thm( 131 "GPROD_SET_REDUCTION_INSERT", 132 ``!g s. FiniteAbelianGroup g /\ s SUBSET G ==> 133 !a x::(G). x NOTIN s ==> 134 (a * x * GPROD_SET g (a * (G DIFF (x INSERT s))) = GPROD_SET g (a * (G DIFF s)))``, 135 rw[coset_def, IMAGE_DEF, EXTENSION, RES_FORALL_THM] >> 136 qabbrev_tac `p = {a * z | z | z IN G /\ z NOTIN s}` >> 137 qabbrev_tac `q = {a * z | z | z IN G /\ z <> x /\ z NOTIN s}` >> 138 (`p = (a * x) INSERT q` by (rw[EXTENSION, EQ_IMP_THM, Abbr`p`, Abbr`q`] >> metis_tac[])) >> 139 `AbelianGroup g /\ Group g /\ FINITE G` by metis_tac[FiniteAbelianGroup_def, AbelianGroup_def] >> 140 `!z. z IN G /\ (a * z = a * x) <=> (z = x)` by metis_tac[group_lcancel] >> 141 (`(a * x) NOTIN q` by (rw[Abbr`q`] >> metis_tac[])) >> 142 (`q SUBSET G` by (rw[EXTENSION, SUBSET_DEF, Abbr`q`] >> rw[])) >> 143 `a * x IN G` by rw[] >> 144 `AbelianMonoid g` by rw[abelian_group_is_abelian_monoid] >> 145 `FINITE q` by metis_tac[SUBSET_FINITE] >> 146 metis_tac[GPROD_SET_THM, DELETE_NON_ELEMENT]); 147 148(* Theorem: (a ** n) * <building n-steps GPROD_SET> * <reducing n-steps GPROD_SET> = GPROD_SET g G *) 149(* Proof: 150 By complete induction on CARD s. 151 Case s = {}, 152 LHS = a ** (CARD s) * (GPROD_SET g s) * GPROD_SET g (a * (G DIFF s)) 153 = a ** 0 * (GPROD_SET g {}) * GPROD_SET g (a * (G DIFF {})) by CARD_EMPTY 154 = #e * #e * GPROD_SET g (a * G) by group_exp_0, DIFF_EMPTY, GPROD_SET_EMPTY. 155 = GPROD_SET g (a * G) by group_lid 156 = GPROD_SET g G by GPROD_SET_IMAGE 157 = RHS 158 Case s <> {}, 159 Let x = CHOICE s, t = REST s, so s = x INSERT t, x NOTIN t. 160 LHS = a ** (CARD s) * (GPROD_SET g s) * GPROD_SET g (a * (G DIFF s)) 161 = a ** SUC(CARD t) * 162 (GPROD_SET g (x INSERT t)) * 163 GPROD_SET g (a * (G DIFF (x INSERT t))) by CARD s = SUC(CARD t), s = x INSERT t. 164 = a ** SUC(CARD t) * 165 (x * GPROD_SET g (t DELETE x)) * 166 GPROD_SET g (a * (G DIFF (x INSERT t))) by GPROD_SET_THM 167 = a ** SUC(CARD t) * 168 (x * GPROD_SET g t) * 169 GPROD_SET g (a * (G DIFF (x INSERT t))) by DELETE_NON_ELEMENT, x NOTIN t. 170 = a*a ** (CARD t) * 171 x * GPROD_SET g t * 172 GPROD_SET g (a * (G DIFF (x INSERT t))) by group_exp_SUC 173 = a ** (CARD t) * 174 GPROD_SET g t * 175 (a * x) * GPROD_SET g (a * (G DIFF (x INSERT t))) by Abelian group commuting 176 = a ** (CARD t) * 177 GPROD_SET g t * 178 GPROD_SET g (a * (G DIFF t)) by GPROD_SET_REDUCTION_INSERT 179 = RHS by induction 180*) 181val GPROD_SET_REDUCTION = store_thm( 182 "GPROD_SET_REDUCTION", 183 ``!g s. FiniteAbelianGroup g /\ s SUBSET G ==> 184 !a::(G). a ** (CARD s) * (GPROD_SET g s) * GPROD_SET g (a * (G DIFF s)) = GPROD_SET g G``, 185 completeInduct_on `CARD s` >> 186 pop_assum (assume_tac o SIMP_RULE bool_ss[GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO]) >> 187 rw[RES_FORALL_THM] >> 188 `AbelianGroup g /\ Group g /\ FINITE G` by metis_tac[FiniteAbelianGroup_def, AbelianGroup_def, FiniteGroup_def] >> 189 `AbelianMonoid g` by rw[abelian_group_is_abelian_monoid] >> 190 Cases_on `s = {}` >| [ 191 rw[GPROD_SET_EMPTY] >> 192 `GPROD_SET g G IN G` by rw[GPROD_SET_PROPERTY] >> 193 rw[GPROD_SET_IMAGE], 194 `?x t. (x = CHOICE s) /\ (t = REST s) /\ (s = x INSERT t)` by rw[CHOICE_INSERT_REST] >> 195 `x IN G` by metis_tac[CHOICE_DEF, SUBSET_DEF] >> 196 `t SUBSET G /\ FINITE t` by metis_tac[REST_SUBSET, SUBSET_TRANS, SUBSET_FINITE] >> 197 `x NOTIN t` by metis_tac[CHOICE_NOT_IN_REST] >> 198 `(CARD s = SUC(CARD t)) /\ CARD t < CARD s` by rw[CARD_INSERT] >> 199 `GPROD_SET g t IN G` by rw[GPROD_SET_PROPERTY] >> 200 `GPROD_SET g (a * (G DIFF (x INSERT t))) IN G` by metis_tac[coset_property, DIFF_SUBSET, SUBSET_FINITE, GPROD_SET_PROPERTY] >> 201 qabbrev_tac `t' = a * (G DIFF (x INSERT t))` >> 202 `a ** CARD s * GPROD_SET g s * GPROD_SET g (a * (G DIFF s)) = 203 a ** SUC(CARD t) * GPROD_SET g (x INSERT t) * GPROD_SET g t'` by rw[Abbr`t'`] >> 204 `_ = a ** SUC(CARD t) * (x * GPROD_SET g (t DELETE x)) * GPROD_SET g t'` by rw[GPROD_SET_THM] >> 205 `_ = a ** SUC(CARD t) * (x * GPROD_SET g t) * GPROD_SET g t'` by metis_tac[DELETE_NON_ELEMENT] >> 206 `_ = (a * a ** (CARD t)) * (x * GPROD_SET g t) * GPROD_SET g t'` by rw[group_exp_SUC] >> 207 `_ = (a ** (CARD t) * a) * (x * GPROD_SET g t) * GPROD_SET g t'` by metis_tac[AbelianGroup_def, group_exp_element] >> 208 `_ = a ** (CARD t) * (a * (x * GPROD_SET g t)) * GPROD_SET g t'` by rw[group_assoc] >> 209 `_ = a ** (CARD t) * ((a * x) * GPROD_SET g t) * GPROD_SET g t'` by rw[group_assoc] >> 210 `_ = a ** (CARD t) * (GPROD_SET g t * (a * x)) * GPROD_SET g t'` by metis_tac[AbelianGroup_def, group_op_element] >> 211 `_ = (a ** (CARD t) * GPROD_SET g t) * (a * x) * GPROD_SET g t'` by rw[group_assoc] >> 212 `_ = a ** (CARD t) * GPROD_SET g t * ((a * x) * GPROD_SET g t')` by rw[group_assoc] >> 213 `_ = a ** (CARD t) * GPROD_SET g t * GPROD_SET g (a * (G DIFF t))` by metis_tac[GPROD_SET_REDUCTION_INSERT] >> 214 rw[] 215 ]); 216 217(* Define Group Factorial *) 218val GFACT_def = Define` 219 GFACT g = GPROD_SET g G 220`; 221 222(* Theorem: GFACT g is an element in Group g. *) 223(* Proof: 224 Since G SUBSET G by SUBSET_REFL 225 This is true by GPROD_SET_PROPERTY: 226 !g s. FiniteAbelianMonoid g /\ s SUBSET G ==> GPROD_SET g s IN G : thm 227*) 228val GFACT_element = store_thm( 229 "GFACT_element", 230 ``!g. FiniteAbelianMonoid g ==> GFACT g IN G``, 231 rw_tac std_ss[FiniteAbelianMonoid_def, GFACT_def, GPROD_SET_PROPERTY, SUBSET_REFL]); 232 233(* Theorem: For FiniteAbelian Group g, a IN G ==> GFACT g = a ** (CARD g) * GFACT g *) 234(* Proof: 235 Since G SUBSET G by SUBSET_REFL, 236 and G DIFF G = {}, 237 Put s = G in GPROD_SET_REDUCTION: 238 a ** (CARD G) * GPROD_SET g G * GPROD_SET g (a * (G DIFF G)) = GPROD_SET g G 239 ==> a ** (CARD G) * GPROD_SET g G * GPROD_SET g (a * {}) = GPROD_SET g G 240 ==> a ** (CARD G) * GPROD_SET g G * GPROD_SET g {} = GPROD_SET g G by coset_empty. 241 ==> a ** (CARD G) * GPROD_SET g G * #e = GPROD_SET g G by GPROD_SET_EMPTY. 242 ==> a ** (CARD G) * GPROD_SET g G = GPROD_SET g G by group_assoc and group_rid 243*) 244val GFACT_identity = store_thm( 245 "GFACT_identity", 246 ``!(g:'a group) a. FiniteAbelianGroup g /\ a IN G ==> (GFACT g = a ** (CARD G) * GFACT g)``, 247 rw[GFACT_def] >> 248 `G SUBSET G` by rw[] >> 249 `G DIFF G = {}` by rw[] >> 250 `AbelianGroup g /\ Group g /\ FINITE G` by metis_tac[FiniteAbelianGroup_def, AbelianGroup_def, FiniteGroup_def] >> 251 `AbelianMonoid g` by rw[abelian_group_is_abelian_monoid] >> 252 `GPROD_SET g G IN G` by rw[GPROD_SET_PROPERTY] >> 253 `GPROD_SET g G = a ** (CARD G) * GPROD_SET g G * GPROD_SET g (a * (G DIFF G))` by rw[GPROD_SET_REDUCTION] >> 254 `_ = a ** (CARD G) * GPROD_SET g G * GPROD_SET g (a * {})` by rw[] >> 255 `_ = a ** (CARD G) * GPROD_SET g G * GPROD_SET g {}` by rw[coset_empty] >> 256 `_ = a ** (CARD G) * GPROD_SET g G * #e` by metis_tac[GPROD_SET_EMPTY] >> 257 `_ = a ** (CARD G) * GPROD_SET g G` by rw[] >> 258 rw[]); 259 260(* Theorem: For FiniteAbelian Group g, a IN G ==> a ** (CARD g) = #e *) 261(* Proof: 262 Since a ** (CARD G) * GFACT g = GFACT g by GFACT_identity 263 Hence a ** (CARD G) = #e by group_lid_unique 264*) 265val finite_abelian_Fermat = store_thm( 266 "finite_abelian_Fermat", 267 ``!(g:'a group) a. FiniteAbelianGroup g /\ a IN G ==> (a ** (CARD G) = #e)``, 268 rpt strip_tac >> 269 `AbelianGroup g /\ Group g /\ FINITE G` by metis_tac[FiniteAbelianGroup_def, AbelianGroup_def, FiniteGroup_def] >> 270 `AbelianMonoid g` by rw[abelian_group_is_abelian_monoid] >> 271 `GFACT g IN G` by rw[GFACT_element] >> 272 `a ** (CARD G) * GFACT g = GFACT g` by rw[GFACT_identity] >> 273 metis_tac[group_exp_element, group_lid_unique]); 274 275 276(* ------------------------------------------------------------------------- *) 277(* Group Iterated Product over a function. *) 278(* ------------------------------------------------------------------------- *) 279 280(* 281> show_types := true; ITSET_def; show_types := false; 282val it = |- !(s :'a -> bool) (f :'a -> 'b -> 'b) (b :'b). 283 ITSET f s b = if FINITE s then if s = ({} :'a -> bool) then b 284 else ITSET f (REST s) (f (CHOICE s) b) 285 else (ARB :'b): thm 286 287> show_types := true; SUM_IMAGE_DEF; show_types := false; 288val it = |- !(f :'a -> num) (s :'a -> bool). 289 SIGMA f s = ITSET (\(e :'a) (acc :num). f e + acc) s (0 :num): thm 290 291> ITSET_def |> ISPEC ``s:'b -> bool`` |> ISPEC ``(f:'b -> 'a)`` |> ISPEC ``b:'a``; 292val it = |- GITSET g s b = if FINITE s then if s = {} then b else GITSET g (REST s) (CHOICE s * b) 293 else ARB: thm 294*) 295 296(* A general iterator for operation (op:'a -> 'a -> 'a) and (id:'a) *) 297val OP_IMAGE_DEF = Define ` 298 OP_IMAGE (op:'a -> 'a -> 'a) (id:'a) (f:'b -> 'a) (s:'b -> bool) = ITSET (\e acc. op (f e) acc) s id 299`; 300 301(* Theorem: OP_IMAGE op id f {} = id *) 302(* Proof: 303 OP_IMAGE op id f {} 304 = ITSET (\e acc. op (f e) acc) {} id by OP_IMAGE_DEF 305 = id by ITSET_EMPTY 306*) 307val OP_IMAGE_EMPTY = store_thm( 308 "OP_IMAGE_EMPTY", 309 ``!op id f. OP_IMAGE op id f {} = id``, 310 rw[OP_IMAGE_DEF, ITSET_EMPTY]); 311 312(* Theorem: OP_IMAGE op id f {x} = op (f x) id *) 313(* Proof: 314 OP_IMAGE op id f {x} 315 = ITSET (\e acc. op (f e) acc) {x} id by OP_IMAGE_DEF 316 = (\e acc. op (f e) acc) x id by ITSET_SING 317 = op (f x) id by application 318*) 319val OP_IMAGE_SING = store_thm( 320 "OP_IMAGE_SING", 321 ``!op id f x. OP_IMAGE op id f {x} = op (f x) id``, 322 rw[OP_IMAGE_DEF, ITSET_SING]); 323 324(* 325Now the hard part: show (\e acc. op (f e) acc) is an accumulative function for ITSET. 326 327val SUM_IMAGE_THM = store_thm( 328 "SUM_IMAGE_THM", 329 ``!f. (SUM_IMAGE f {} = 0) /\ 330 (!e s. FINITE s ==> 331 (SUM_IMAGE f (e INSERT s) = 332 f e + SUM_IMAGE f (s DELETE e)))``, 333 REPEAT STRIP_TAC THENL [ 334 SIMP_TAC (srw_ss()) [ITSET_THM, SUM_IMAGE_DEF], 335 SIMP_TAC (srw_ss()) [SUM_IMAGE_DEF] THEN 336 Q.ABBREV_TAC `g = \e acc. f e + acc` THEN 337 Q_TAC SUFF_TAC `ITSET g (e INSERT s) 0 = 338 g e (ITSET g (s DELETE e) 0)` THEN1 339 SRW_TAC [][Abbr`g`] THEN 340 MATCH_MP_TAC COMMUTING_ITSET_RECURSES THEN 341 SRW_TAC [ARITH_ss][Abbr`g`] 342 ]); 343 344val PROD_IMAGE_THM = store_thm( 345 "PROD_IMAGE_THM", 346 ``!f. (PROD_IMAGE f {} = 1) /\ 347 (!e s. FINITE s ==> 348 (PROD_IMAGE f (e INSERT s) = f e * PROD_IMAGE f (s DELETE e)))``, 349 REPEAT STRIP_TAC THEN1 350 SIMP_TAC (srw_ss()) [ITSET_THM, PROD_IMAGE_DEF] THEN 351 SIMP_TAC (srw_ss()) [PROD_IMAGE_DEF] THEN 352 Q.ABBREV_TAC `g = \e acc. f e * acc` THEN 353 Q_TAC SUFF_TAC `ITSET g (e INSERT s) 1 = 354 g e (ITSET g (s DELETE e) 1)` THEN1 SRW_TAC [][Abbr`g`] THEN 355 MATCH_MP_TAC COMMUTING_ITSET_RECURSES THEN 356 SRW_TAC [ARITH_ss][Abbr`g`]); 357 358*) 359 360(* Overload a communtative operation *) 361val _ = overload_on("FUN_COMM", ``\op f. !x y z. op (f x) (op (f y) z) = op (f y) (op (f x) z)``); 362 363(* Theorem: (OP_IMAGE op id f {} = id) /\ 364 (FUN_COMM op f ==> !s. FINITE s ==> 365 !e. OP_IMAGE op id f (e INSERT s) = op (f e) (OP_IMAGE op id f (s DELETE e))) *) 366(* Proof: 367 First goal: P_IMAGE op id f {} = id 368 True by OP_IMAGE_EMPTY. 369 Second goal: OP_IMAGE op id f (e INSERT s) = op (f e) (OP_IMAGE op id f (s DELETE e))) 370 Let g = \e acc. op (f e) acc, 371 Then by OP_IMAGE_DEF, the goal is: 372 to show: ITSET g (e INSERT s) id = op (f e) (ITSET g (s DELETE e) id) 373 or show: ITSET g (e INSERT s) id = g e (ITSET g (s DELETE e) id) 374 Given FUN_COMM op f, the is true by COMMUTING_ITSET_RECURSES. 375*) 376val OP_IMAGE_THM = store_thm( 377 "OP_IMAGE_THM", 378 ``!op id f. (OP_IMAGE op id f {} = id) /\ 379 (FUN_COMM op f ==> !s. FINITE s ==> 380 !e. OP_IMAGE op id f (e INSERT s) = op (f e) (OP_IMAGE op id f (s DELETE e)))``, 381 rpt strip_tac >- 382 rw[OP_IMAGE_EMPTY] >> 383 rw[OP_IMAGE_DEF] >> 384 qabbrev_tac `g = \e acc. op (f e) acc` >> 385 rw[] >> 386 rw[COMMUTING_ITSET_RECURSES, Abbr`g`]); 387 388(* A better iterator for group operation over (f:'b -> 'a) *) 389val GROUP_IMAGE_DEF = Define ` 390 GROUP_IMAGE (g:'a group) (f:'b -> 'a) (s:'b -> bool) = ITSET (\e acc. (f e) * acc) s #e 391`; 392 393(* overload GROUP_IMAGE *) 394val _ = temp_overload_on("GPI", ``GROUP_IMAGE g``); 395 396(* 397> GROUP_IMAGE_DEF; 398val it = |- !g f s. GPI f s = ITSET (\e acc. f e * acc) s #e: thm 399*) 400 401(* Theorem: GPI = OP_IMAGE (g.op) (g.id) *) 402(* Proof: by GROUP_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM *) 403val group_image_as_op_image = store_thm( 404 "group_image_as_op_image", 405 ``!g:'a group. GPI = OP_IMAGE (g.op) (g.id)``, 406 rw[GROUP_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM]); 407 408(* Theorem: SUM_IMAGE = OP_IMAGE (\(x y):num. x + y) 0 *) 409(* Proof: by SUM_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM *) 410val sum_image_as_op_image = store_thm( 411 "sum_image_as_op_image", 412 ``SIGMA = OP_IMAGE (\(x y):num. x + y) 0``, 413 rw[SUM_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM]); 414 415(* Theorem: PROD_IMAGE = OP_IMAGE (\(x y):num. x * y) 1 *) 416(* Proof: by PROD_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM *) 417val prod_image_as_op_image = store_thm( 418 "prod_image_as_op_image", 419 ``PI = OP_IMAGE (\(x y):num. x * y) 1``, 420 rw[PROD_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM]); 421 422(* 423val _ = clear_overloads_on("GITSET"); 424val _ = clear_overloads_on("GPI"); 425val _ = overload_on("GITSET", ``\g s b. ITSET g.op s b``); 426val _ = overload_on("GPI", ``GROUP_IMAGE g``); 427*) 428 429(* val _ = overload_on("GITSET", ``\g s b. ITSET g.op s b``); *) 430 431(* Theorem: GITSET g = ITSET (\e acc. g.op e acc) *) 432(* Proof: 433 Note g.op = (\e acc. e * acc) by FUN_EQ_THM 434 435 GITSET g s b 436 = ITSET g.op s b by notation 437 = ITSET (\e acc. e * acc) s b by ITSET_CONG 438 439 Hence GITSET g = ITSET (\e acc. g.op e acc) by FUN_EQ_THM 440*) 441val GITSET_AS_ITSET = store_thm( 442 "GITSET_AS_ITSET", 443 ``!g:'a group. GITSET g = ITSET (\e acc. g.op e acc)``, 444 rw[FUN_EQ_THM] >> 445 `g.op = (\e acc. e * acc)` by rw[FUN_EQ_THM] >> 446 `ITSET g.op = ITSET (\e acc. e * acc)` by rw[ITSET_CONG] >> 447 rw[]); 448 449(* 450> ITSET_def |> ISPEC ``s:'b -> bool`` |> ISPEC ``(g:'a group).op`` |> ISPEC ``b:'a``; 451val it = |- GITSET g s b = if FINITE s then if s = {} then b else GITSET g (REST s) (CHOICE s * b) 452 else ARB: thm 453*) 454 455(* Theorem: GPROD_SET g = GPI I *) 456(* Proof: 457 Note g.op = (\e acc. e * acc) by FUN_EQ_THM 458 459 GPROD_SET g x 460 = GITSET g x #e by GPROD_SET_def 461 = ITSET g.op x #e by notation 462 = ITSET (\e acc. e * acc) x #e by above 463 = GPI I x by GROUP_IMAGE_DEF 464 Hence GPROD_SET g = GPI I by FUN_EQ_THM 465*) 466val GPROD_SET_AS_GROUP_IMAGE = store_thm( 467 "GPROD_SET_AS_GROUP_IMAGE", 468 ``!g:'a group. GPROD_SET g = GPI I``, 469 rw[FUN_EQ_THM] >> 470 `g.op = (\e acc. e * acc)` by rw[FUN_EQ_THM] >> 471 `ITSET g.op = ITSET (\e acc. e * acc)` by rw[ITSET_CONG] >> 472 `GPROD_SET g x = GITSET g x #e` by rw[GPROD_SET_def] >> 473 `_ = ITSET (\e acc. e * acc) x #e` by rw[] >> 474 `_ = GPI I x` by rw[GROUP_IMAGE_DEF] >> 475 rw[]); 476 477(* Theorem: GPI f {} = #e *) 478(* Proof 479 GPI f {} 480 = GROUP_IMAGE g f {} by notation 481 = ITSET (\e acc. f e * acc) {} #e by GROUP_IMAGE_DEF 482 = #e by ITSET_EMPTY 483*) 484val group_image_empty = store_thm( 485 "group_image_empty", 486 ``!g:'a group. !f. GPI f {} = #e``, 487 rw[GROUP_IMAGE_DEF, ITSET_EMPTY]); 488 489(* Define a group function *) 490val group_fun_def = Define ` 491 group_fun (g:'a group) f = !x. x IN G ==> f x IN G 492`; 493 494(* overload on group function *) 495val _ = temp_overload_on("gfun", ``group_fun g``); 496 497(* Theorem: Monoid g ==> !f. gfun f ==> !x. x IN G ==> (GPI f {x} = f x) *) 498(* Proof: 499 Note x IN G ==> f x IN G by group_fun_def 500 GPI f {x} 501 = GROUP_IMAGE g f {x} by notation 502 = ITSET (\e acc. f e * acc) {x} #e by GROUP_IMAGE_DEF 503 = f x * #e by ITSET_SING 504 = f x by monoid_rid 505*) 506val group_image_sing = store_thm( 507 "group_image_sing", 508 ``!g:'a group. Monoid g ==> !f. gfun f ==> !x. x IN G ==> (GPI f {x} = f x)``, 509 rw[GROUP_IMAGE_DEF, group_fun_def, ITSET_SING]); 510 511 512(* ------------------------------------------------------------------------- *) 513 514(* export theory at end *) 515val _ = export_theory(); 516 517(*===========================================================================*) 518