1(* ------------------------------------------------------------------------- *) 2(* Involution: Basic *) 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 "involute"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* open dependent theories *) 17(* arithmeticTheory -- load by default *) 18 19(* val _ = load "helperTheory"; *) 20open helperNumTheory; 21open helperSetTheory; 22open helperFunctionTheory; 23open helperTheory; (* for FUNPOW_closure *) 24 25(* arithmeticTheory -- load by default *) 26open arithmeticTheory pred_setTheory; 27 28 29(* ------------------------------------------------------------------------- *) 30(* Involution: Basic Documentation *) 31(* ------------------------------------------------------------------------- *) 32(* Overloading: 33 f endo s = !x. x IN s ==> f x IN s 34 f involute s = !x. x IN s ==> f x IN s /\ (f (f x) = x) 35*) 36(* 37 38 Helper Theorem: 39 40 Involution: 41 involute_endo |- !f s. f involute s ==> f endo s 42 involute_inj |- !f s. f involute s ==> INJ f s s 43 involute_surj |- !f s. f involute s ==> SURJ f s s 44 involute_bij |- !f s. f involute s ==> f PERMUTES s 45 involute_permutes |- !f s. f involute X ==> f PERMUTES s 46 involute_LINV |- !f s. f involute s ==> LINV f s involute s 47 involute_FUNPOW |- !f s x n. f involute s /\ x IN s ==> 48 FUNPOW f n x = if EVEN n then x else f x 49 involute_FUNPOW_LINV |- !f s x n. f involute s /\ x IN s ==> 50 FUNPOW (LINV f s) n x = FUNPOW f n x 51 involute_alt |- !f s. f involute s <=> 52 f endo s /\ !x. x IN s ==> FUNPOW f 2 x = x 53 54*) 55 56(* ------------------------------------------------------------------------- *) 57(* Helper Theorem *) 58(* ------------------------------------------------------------------------- *) 59 60(* ------------------------------------------------------------------------- *) 61(* Involution *) 62(* ------------------------------------------------------------------------- *) 63 64(* Overload on involution *) 65(* 66val _ = overload_on("involute", ``\f. f o f = I``); 67val _ = clear_overloads_on "involute"; 68*) 69 70(* An endofunction has its domain equal to its co-domain. *) 71val _ = overload_on("endo", ``\f s. !x. x IN s ==> f x IN s``); 72val _ = set_fixity "endo" (Infix(NONASSOC, 450)); (* same as relation *) 73 74val _ = overload_on("involute", ``\f s. !x. x IN s ==> f x IN s /\ (f (f x) = x)``); 75val _ = set_fixity "involute" (Infix(NONASSOC, 450)); (* same as relation *) 76 77(* Theorem: f involute s ==> f endo s *) 78(* Proof: by notation *) 79Theorem involute_endo: 80 !f s. f involute s ==> f endo s 81Proof 82 simp[] 83QED 84 85(* Theorem: f involute s ==> INJ f s s *) 86(* Proof: 87 By INJ_DEF, this is to show: 88 (1) !x. x IN s ==> f x IN s, true by f involute s. 89 (2) !x y. x IN s /\ y IN s ==> f x = f y ==> x = y 90 f x = f y 91 ==> f (f x) = f (f y) by f x IN s, f y IN s 92 ==> x = y by f involute s 93*) 94Theorem involute_inj: 95 !f s. f involute s ==> INJ f s s 96Proof 97 metis_tac[INJ_DEF] 98QED 99 100(* Theorem: f involute s ==> SURJ f s s *) 101(* Proof: 102 By SURJ_DEF, this is to show: 103 (1) !x. x IN s ==> f x IN s, true by f involute s. 104 (2) !x. x IN s ==> ?y. y IN s /\ f y = x 105 Let y = f x, then y IN s by f involute s 106 and f y = f (f x) = x by f involute s 107*) 108Theorem involute_surj: 109 !f s. f involute s ==> SURJ f s s 110Proof 111 prove_tac[SURJ_DEF] 112QED 113 114(* Theorem: f involute s ==> f PERMUTES s *) 115(* Proof: by BIJ_DEF, involute_inj, involute_surj *) 116Theorem involute_bij: 117 !f s. f involute s ==> f PERMUTES s 118Proof 119 rw[BIJ_DEF, involute_inj, involute_surj] 120QED 121 122(* Theorem alias *) 123val involute_permutes = save_thm("involute_permutes", involute_bij); 124(* val involute_permutes = |- !f s. f involute s ==> f PERMUTES s: thm *) 125 126(* Theorem: f involute s ==> (LINV f s) involute s *) 127(* Proof: 128 f involute s 129 ==> f PERMUTES s by involute_bij 130 ==> (LINV f s) PERMUTES s by BIJ_LINV_BIJ 131 Thus x IN s ==> LINV f s x IN s by BIJ_ELEMENT 132 Since f (f x) = x by involution 133 so f x = LINV f s x by BIJ_LINV_THM 134 or x = LINV f s (LINV f s x) by BIJ_LINV_THM 135*) 136Theorem involute_LINV: 137 !f s. f involute s ==> (LINV f s) involute s 138Proof 139 ntac 3 strip_tac >> 140 `f PERMUTES s /\ (LINV f s) PERMUTES s` by rw[involute_bij, BIJ_LINV_BIJ] >> 141 rpt strip_tac >- 142 metis_tac[BIJ_ELEMENT] >> 143 metis_tac[BIJ_LINV_THM] 144QED 145 146(* Theorem: f involute s /\ x IN s ==> 147 FUNPOW f n x = if EVEN n then x else f x *) 148(* Proof: 149 Note FUNPOW f 2 x 150 = f (f x) by FUNPOW_2 151 = x by involution 152 ==> FUNPOW f (2 * k) x = x by FUNPOW_MULTIPLE 153 154 If EVEN n, then n = 2 * k by EVEN_EXISTS 155 Thus FUNPOW f (2 * k) x = x by above 156 If ~EVEN n, then ODD n. by EVEN_ODD 157 Thus n = SUC (2 * k) by ODD_EXISTS 158 FUNPOW f n x 159 = FUNPOW f (SUC (2 * k)) x by above 160 = f (FUNPOW f (2 * k) x) by FUNPOW_SUC 161 = f x by above 162*) 163Theorem involute_FUNPOW: 164 !f s x n. f involute s /\ x IN s ==> 165 FUNPOW f n x = if EVEN n then x else f x 166Proof 167 rpt strip_tac >> 168 `FUNPOW f 2 x = x` by rw[FUNPOW_2] >> 169 (imp_res_tac FUNPOW_MULTIPLE >> fs[]) >> 170 (Cases_on `EVEN n` >> simp[]) >- 171 metis_tac[EVEN_EXISTS] >> 172 metis_tac[EVEN_ODD, ODD_EXISTS, FUNPOW_SUC] 173QED 174 175(* Theorem: f involute s /\ x IN s ==> 176 FUNPOW (LINV f s) n x = FUNPOW f n x *) 177(* Proof: 178 By induction on n. 179 Base: FUNPOW (LINV f s) 0 x = FUNPOW f 0 x, true by FUNPOW_0 180 Step: FUNPOW (LINV f s) n x = FUNPOW f n x ==> 181 FUNPOW (LINV f s) (SUC n) x = FUNPOW f (SUC n) x 182 Note f PERMUTES s by involute_bij 183 and FUNPOW f n x IN s by FUNPOW_closure 184 also FUNPOW f (SUC n) x IN s by FUNPOW_closure 185 FUNPOW (LINV f s) (SUC n) x 186 = LINV f s (FUNPOW (LINV f s) n x) by FUNPOW_SUC 187 = LINV f s (FUNPOW f n x) by induction hypothesis 188 = LINV f s (LINV f s (f (FUNPOW f n x))) by BIJ_LINV_THM, 189 = LINV f s (LINV f s (FUNPOW f (SUC n) x)) by FUNPOW_SUC 190 = FUNPOW f (SUC n) x by involute_LINV 191*) 192Theorem involute_FUNPOW_LINV: 193 !f s x n. f involute s /\ x IN s ==> 194 FUNPOW (LINV f s) n x = FUNPOW f n x 195Proof 196 rpt strip_tac >> 197 Induct_on `n` >- 198 rw[] >> 199 `f PERMUTES s` by rw[involute_bij] >> 200 `FUNPOW f n x IN s /\ FUNPOW f (SUC n) x IN s` by rw[FUNPOW_closure] >> 201 `FUNPOW (LINV f s) (SUC n) x = LINV f s (FUNPOW (LINV f s) n x)` by rw[FUNPOW_SUC] >> 202 `_ = LINV f s (FUNPOW f n x)` by rw[] >> 203 `_ = LINV f s (LINV f s (f (FUNPOW f n x)))` by metis_tac[BIJ_LINV_THM] >> 204 `_ = LINV f s (LINV f s (FUNPOW f (SUC n) x))` by rw[FUNPOW_SUC] >> 205 `_ = FUNPOW f (SUC n) x` by metis_tac[involute_LINV] >> 206 simp[] 207QED 208 209(* Theorem: f involute s <=> f endo s /\ !x. x IN s ==> FUNPOW f 2 x = x *) 210(* Proof: 211 f involute s 212 <=> !x. x IN s ==> f x IN s /\ f (f x) = x by notation 213 <=> !x. x IN s ==> f x IN s /\ FUNPOW 2 x = x by FUNPOW_2 214 <=> !x. x IN s ==> f x IN s /\ !x. x IN s ==> FUNPOW 2 x = x 215 <=> f endo s /\ !x. x IN s ==> FUNPOW 2 x = x by notation 216*) 217Theorem involute_alt: 218 !f s. f involute s <=> f endo s /\ !x. x IN s ==> FUNPOW f 2 x = x 219Proof 220 simp[FUNPOW_2] >> 221 metis_tac[] 222QED 223 224 225 226(* ------------------------------------------------------------------------- *) 227 228(* export theory at end *) 229val _ = export_theory(); 230 231(*===========================================================================*) 232