1open HolKernel Parse boolLib bossLib BasicProvers boolSimps 2 3local open stringTheory in end; 4 5open pred_setTheory 6 7open basic_swapTheory NEWLib lcsymtacs 8 9val _ = new_theory "nomset"; 10 11fun Store_thm(s, t, tac) = (store_thm(s,t,tac) before 12 export_rewrites [s]) 13 14fun Save_thm(s, t) = (save_thm(s,t) before export_rewrites [s]) 15 16(* permutations are represented as lists of pairs of strings. These 17 can be lifted to bijections on strings that only move finitely many 18 strings with the perm_of function *) 19 20val _ = overload_on ("perm_of", ``raw_lswapstr``); 21val _ = overload_on ("raw_lswapstr", ``raw_lswapstr``); 22 23val perm_of_decompose = raw_lswapstr_APPEND 24val perm_of_swapstr = store_thm( 25 "perm_of_swapstr", 26 ``perm_of p (swapstr x y s) = 27 swapstr (perm_of p x) (perm_of p y) (perm_of p s)``, 28 Induct_on `p` THEN SRW_TAC [][]); 29 30val permeq_def = Define` 31 permeq l1 l2 = (perm_of l1 = perm_of l2) 32`; 33val _ = set_fixity "==" (Infix(NONASSOC, 450)); 34val _ = overload_on ("==", ``permeq``) 35 36val permeq_permeq_cong = store_thm( 37 "permeq_permeq_cong", 38 ``((==) p1 = (==) p1') ==> ((==) p2 = (==) p2') ==> 39 ((p1 == p2) = (p1' == p2'))``, 40 SRW_TAC [][permeq_def, FUN_EQ_THM] THEN METIS_TAC []); 41 42val permeq_refl = Store_thm("permeq_refl", ``x == x``, SRW_TAC [][permeq_def]); 43 44val permeq_sym = store_thm( 45 "permeq_sym", 46 ``(x == y) ==> (y == x)``, 47 SRW_TAC [][permeq_def]); 48 49val permeq_trans = store_thm( 50 "permeq_trans", 51 ``(x == y) /\ (y == z) ==> (x == z)``, 52 SRW_TAC [][permeq_def]); 53 54val app_permeq_monotone = store_thm( 55 "app_permeq_monotone", 56 ``!p1 p1' p2 p2'. 57 (p1 == p1') /\ (p2 == p2') ==> (p1 ++ p2 == p1' ++ p2')``, 58 ASM_SIMP_TAC (srw_ss()) [raw_lswapstr_APPEND, permeq_def, FUN_EQ_THM]); 59 60val halfpermeq_eliminate = prove( 61 ``((==) x = (==)y) = (x == y)``, 62 SRW_TAC [][FUN_EQ_THM, EQ_IMP_THM, permeq_def]); 63 64val app_permeq_cong = store_thm( 65 "app_permeq_cong", 66 ``((==) p1 = (==) p1') ==> ((==) p2 = (==) p2') ==> 67 ((==) (p1 ++ p2) = (==) (p1' ++ p2'))``, 68 SRW_TAC [][halfpermeq_eliminate, app_permeq_monotone]); 69 70val permof_inverse_lemma = prove( 71 ``!p. p ++ REVERSE p == []``, 72 ASM_SIMP_TAC (srw_ss()) [FUN_EQ_THM, permeq_def] THEN Induct THEN 73 SRW_TAC [][] THEN ONCE_REWRITE_TAC [raw_lswapstr_APPEND] THEN SRW_TAC [][]); 74 75val permof_inverse = store_thm( 76 "permof_inverse", 77 ``(p ++ REVERSE p == []) /\ (REVERSE p ++ p == [])``, 78 METIS_TAC [permof_inverse_lemma, listTheory.REVERSE_REVERSE]); 79 80val permof_inverse_append = store_thm ( 81 "permof_inverse_append", 82 ``(p ++ q) ++ REVERSE q == p ��� (p ++ REVERSE q) ++ q == p``, 83 SIMP_TAC bool_ss [GSYM listTheory.APPEND_ASSOC] THEN 84 CONJ_TAC THEN 85 SIMP_TAC bool_ss [Once (GSYM listTheory.APPEND_NIL), SimpR ``(==)``] THEN 86 MATCH_MP_TAC app_permeq_monotone THEN SRW_TAC [][permof_inverse]); 87 88val permof_inverse_applied = raw_lswapstr_inverse 89 90val permof_dups = store_thm( 91 "permof_dups", 92 ``h::h::t == t``, 93 SRW_TAC [][permeq_def, FUN_EQ_THM]); 94 95val permof_dups_rwt = store_thm( 96 "permof_dups_rwt", 97 ``(==) (h::h::t) = (==) t``, 98 SRW_TAC [][halfpermeq_eliminate, permof_dups]); 99 100val permof_idfront = store_thm( 101 "permof_idfront", 102 ``(x,x) :: t == t``, 103 SRW_TAC [][permeq_def, FUN_EQ_THM]); 104 105 106val permof_REVERSE_monotone = store_thm( 107 "permof_REVERSE_monotone", 108 ``(x == y) ==> (REVERSE x == REVERSE y)``, 109 STRIP_TAC THEN 110 `REVERSE x ++ x == REVERSE x ++ y` 111 by METIS_TAC [app_permeq_monotone, permeq_refl] THEN 112 `REVERSE x ++ y == []` 113 by METIS_TAC [permof_inverse, permeq_trans, permeq_sym] THEN 114 `REVERSE x ++ (y ++ REVERSE y) == REVERSE y` 115 by METIS_TAC [listTheory.APPEND, listTheory.APPEND_ASSOC, 116 app_permeq_monotone, permeq_refl] THEN 117 METIS_TAC [permof_inverse, listTheory.APPEND_NIL, 118 app_permeq_monotone, permeq_refl, permeq_trans, permeq_sym]); 119 120val permeq_cons_monotone = store_thm( 121 "permeq_cons_monotone", 122 ``(p1 == p2) ==> (h::p1 == h::p2)``, 123 SRW_TAC [][permeq_def, FUN_EQ_THM]); 124 125val permeq_swap_ends0 = store_thm( 126 "permeq_swap_ends0", 127 ``!p x y. p ++ [(x,y)] == (perm_of p x, perm_of p y)::p``, 128 Induct THEN SRW_TAC [][permeq_refl] THEN 129 Q_TAC SUFF_TAC `h::(perm_of p x, perm_of p y)::p == 130 (swapstr (FST h) (SND h) (perm_of p x), 131 swapstr (FST h) (SND h) (perm_of p y))::h::p` 132 THEN1 METIS_TAC [permeq_trans, permeq_cons_monotone] THEN 133 SRW_TAC [][FUN_EQ_THM, permeq_def]); 134 135val app_permeq_left_cancel = store_thm( 136 "app_permeq_left_cancel", 137 ``!p1 p1' p2 p2'. p1 == p1' /\ p1 ++ p2 == p1' ++ p2' ==> p2 == p2'``, 138 REPEAT STRIP_TAC THEN 139 `REVERSE p1 == REVERSE p1'` by METIS_TAC [permof_REVERSE_monotone] THEN 140 `(REVERSE p1) ++ p1 ++ p2 == (REVERSE p1') ++ p1' ++ p2'` 141 by (METIS_TAC [app_permeq_monotone, listTheory.APPEND_ASSOC]) THEN 142 `[] ++ p2 == (REVERSE p1) ++ p1 ++ p2 /\ 143 [] ++ p2' == (REVERSE p1') ++ p1' ++ p2'` 144 by (METIS_TAC [app_permeq_monotone, permeq_refl, permeq_sym, permof_inverse]) THEN 145 METIS_TAC [listTheory.APPEND, permeq_refl, permeq_sym, permeq_trans]); 146 147val app_permeq_right_cancel = store_thm( 148 "app_permeq_right_cancel", 149 ``!p1 p1' p2 p2'. p1 == p1' /\ p2 ++ p1 == p2' ++ p1' ==> p2 == p2'``, 150 REPEAT STRIP_TAC THEN 151 `REVERSE p1 == REVERSE p1'` by METIS_TAC [permof_REVERSE_monotone] THEN 152 `p2 ++ (p1 ++ (REVERSE p1)) == p2' ++ (p1' ++ (REVERSE p1'))` 153 by (METIS_TAC [app_permeq_monotone, listTheory.APPEND_ASSOC]) THEN 154 `p2 ++ [] == p2 ++ (p1 ++ (REVERSE p1)) /\ 155 p2' ++ [] == p2' ++ (p1' ++ (REVERSE p1'))` 156 by (METIS_TAC [app_permeq_monotone, permeq_refl, permeq_sym, permof_inverse]) THEN 157 METIS_TAC [listTheory.APPEND_NIL, permeq_refl, permeq_trans, permeq_sym]); 158 159(* ---------------------------------------------------------------------- 160 Define what it is to be a permutation action on a type 161 ---------------------------------------------------------------------- *) 162 163val _ = type_abbrev("pm",``:(string # string) list``); 164 165val _ = add_rule {fixity = Suffix 2100, 166 term_name = "�����", 167 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 168 paren_style = OnlyIfNecessary, 169 pp_elements = [TOK "�����"]} 170val _ = overload_on ("�����", ``REVERSE : pm -> pm``) 171val _ = TeX_notation {hol="�����", TeX= ("\\ensuremath{\\sp{-1}}", 1)} 172 173val is_pmact_def = Define` 174 is_pmact (f:pm -> 'a -> 'a) = 175 (!x. f [] x = x) /\ 176 (!p1 p2 x. f (p1 ++ p2) x = f p1 (f p2 x)) /\ 177 (!p1 p2. (p1 == p2) ==> (f p1 = f p2))`; 178 179val existence = prove( 180``?p. is_pmact p``, 181 Q.EXISTS_TAC `K I` THEN 182 SRW_TAC [][is_pmact_def]); 183 184val pmact_TY_DEF = new_type_definition ("pmact", existence); 185val pmact_bijections = define_new_type_bijections 186 {name="pmact_bijections",tyax=pmact_TY_DEF,ABS="mk_pmact",REP="pmact"}; 187val pmact_onto = prove_rep_fn_onto pmact_bijections; 188 189val is_pmact_pmact = Store_thm( 190"is_pmact_pmact", 191``!pm. is_pmact (pmact pm)``, 192METIS_TAC [pmact_onto]); 193 194val pmact_nil = Store_thm( 195 "pmact_nil", 196 ``!pm x. (pmact pm [] x = x)``, 197 MP_TAC is_pmact_pmact THEN 198 simp_tac std_ss [is_pmact_def]) 199 200val pmact_permeq = Store_thm( 201 "pmact_permeq", 202 ``p1 == p2 ==> (pmact pm p1 = pmact pm p2)``, 203 METIS_TAC [is_pmact_pmact,is_pmact_def]); 204 205val pmact_decompose = store_thm( 206 "pmact_decompose", 207 ``!pm x y a. pmact pm (x ++ y) a = pmact pm x (pmact pm y a)``, 208 MP_TAC is_pmact_pmact THEN 209 simp_tac std_ss [is_pmact_def]); 210 211val pmact_dups = Store_thm( 212 "pmact_dups", 213 ``!f h t a. pmact f (h::h::t) a = pmact f t a``, 214 MP_TAC is_pmact_pmact THEN 215 SRW_TAC [][is_pmact_def] THEN 216 Q_TAC SUFF_TAC `h::h::t == t` THEN1 METIS_TAC [pmact_permeq] THEN 217 SRW_TAC [][permof_dups]); 218 219val pmact_id = Store_thm( 220 "pmact_id", 221 ``!f x a t. pmact f ((x,x)::t) a = pmact f t a``, 222 MP_TAC is_pmact_pmact THEN 223 rpt strip_tac >> 224 Q_TAC SUFF_TAC `((x,x)::t) == t` 225 THEN1 METIS_TAC [is_pmact_def] THEN 226 SRW_TAC [][permof_idfront]); 227 228val pmact_inverse = Store_thm( 229 "pmact_inverse", 230 ``(pmact f p (pmact f p����� a) = a) /\ 231 (pmact f p����� (pmact f p a) = a)``, 232 MP_TAC is_pmact_pmact THEN 233 METIS_TAC [is_pmact_def, permof_inverse]) 234 235val pmact_sing_inv = Store_thm( 236 "pmact_sing_inv", 237 ``pmact pm [h] (pmact pm [h] x) = x``, 238 METIS_TAC [listTheory.REVERSE_DEF, listTheory.APPEND, pmact_inverse]); 239 240val pmact_eql = store_thm( 241 "pmact_eql", 242 ``(pmact pm p x = y) = (x = pmact pm p����� y)``, 243 MP_TAC is_pmact_pmact THEN 244 SRW_TAC [][is_pmact_def, EQ_IMP_THM] THEN 245 SRW_TAC [][pmact_decompose]); 246 247val pmact_eqr = save_thm( 248 "pmact_eqr", 249 pmact_eql |> Q.INST [`y` |-> `pmact pm p y`, 250 `x` |-> `pmact pm p����� x`] 251 |> REWRITE_RULE [pmact_inverse]); 252 253val pmact_injective = Store_thm( 254 "pmact_injective", 255 ``(pmact pm p x = pmact pm p y) = (x = y)``, 256 METIS_TAC [pmact_inverse]); 257 258val permeq_flip_args = store_thm( 259 "permeq_flip_args", 260 ``(x,y)::t == (y,x)::t``, 261 SRW_TAC [][permeq_def, FUN_EQ_THM]); 262 263val pmact_flip_args = store_thm( 264 "pmact_flip_args", 265 ``pmact pm ((x,y)::t) a = pmact pm ((y,x)::t) a``, 266 METIS_TAC [is_pmact_pmact, is_pmact_def, permeq_flip_args]); 267 268 269 270(* ---------------------------------------------------------------------- 271 define (possibly parameterised) permutation actions on standard 272 builtin types: functions, sets, lists, pairs, etc 273 ---------------------------------------------------------------------- *) 274 275(* two simple permutation actions: strings, and "everything else" *) 276val perm_of_is_pmact = Store_thm( 277 "perm_of_is_pmact", 278 ``is_pmact raw_lswapstr``, 279 SRW_TAC [][is_pmact_def, raw_lswapstr_APPEND, permeq_def]); 280 281val discrete_is_pmact = Store_thm( 282 "discrete_is_pmact", 283 ``is_pmact (K I)``, 284 SRW_TAC [][is_pmact_def]); 285 286val _ = overload_on("string_pmact", ``mk_pmact perm_of``); 287val _ = overload_on("stringpm",``pmact string_pmact``); 288val _ = overload_on("lswapstr", ``stringpm``); 289val _ = overload_on("discrete_pmact",``(mk_pmact (K I))``); 290val _ = overload_on("discretepm",``pmact discrete_pmact``); 291 292val stringpm_raw = store_thm( 293"stringpm_raw", 294``stringpm = perm_of``, 295srw_tac [][GSYM pmact_bijections]); 296 297val permeq_swap_ends = save_thm( 298 "permeq_swap_ends", 299 SUBS [GSYM stringpm_raw] permeq_swap_ends0); 300 301val lswapstr_swapstr = save_thm( 302 "lswapstr_swapstr", 303 ONCE_REWRITE_RULE [GSYM stringpm_raw] perm_of_swapstr); 304 305val _ = remove_ovl_mapping "perm_of" {Thy="basic_swap", Name = "raw_lswapstr"} 306 307(* l1 == l2 <=> !x. lswapstr l1 x = lswapstr l2 x *) 308val permeq_thm = save_thm( 309 "permeq_thm", 310 permeq_def |> ONCE_REWRITE_RULE [GSYM stringpm_raw] 311 |> REWRITE_RULE [FUN_EQ_THM]) 312 313val stringpm_thm = Save_thm( 314"stringpm_thm", 315SUBS [GSYM stringpm_raw] raw_lswapstr_def); 316 317val discretepm_raw = store_thm( 318"discretepm_raw", 319``discretepm = K I``, 320srw_tac [][GSYM pmact_bijections]); 321 322val discretepm_thm = Store_thm( 323"discretepm_thm", 324``discretepm pi x = x``, 325srw_tac [][discretepm_raw]); 326 327val pmact_sing_to_back = store_thm( 328 "pmact_sing_to_back", 329 ``pmact pm [(lswapstr pi a, lswapstr pi b)] (pmact pm pi v) = 330 pmact pm pi (pmact pm [(a,b)] v)``, 331 SRW_TAC [][GSYM pmact_decompose] THEN 332 Q_TAC SUFF_TAC `(lswapstr pi a,lswapstr pi b)::pi == pi ++ [(a,b)]` 333 THEN1 METIS_TAC [is_pmact_def,is_pmact_pmact] THEN 334 METIS_TAC [permeq_swap_ends, permeq_sym, stringpm_raw]); 335 336(* functions *) 337val raw_fnpm_def = Define` 338 raw_fnpm (dpm: �� pmact) (rpm: �� pmact) p f x = pmact rpm p (f (pmact dpm p����� x)) 339`; 340val _ = export_rewrites["raw_fnpm_def"]; 341 342val _ = overload_on ("fn_pmact", ``��dpm rpm. mk_pmact (raw_fnpm dpm rpm)``); 343val _ = overload_on ("fnpm", ``��dpm rpm. pmact (fn_pmact dpm rpm)``); 344 345val fnpm_raw = store_thm( 346"fnpm_raw", 347``fnpm dpm rpm = raw_fnpm dpm rpm``, 348srw_tac [][GSYM pmact_bijections] >> 349SRW_TAC [][is_pmact_def, FUN_EQ_THM, listTheory.REVERSE_APPEND, pmact_decompose] THEN 350METIS_TAC [permof_REVERSE_monotone,pmact_permeq]); 351 352val fnpm_def = save_thm( 353"fnpm_def", 354foldr (uncurry Q.GEN) (SUBS [GSYM fnpm_raw] (SPEC_ALL raw_fnpm_def)) 355[`dpm`,`rpm`,`p`,`f`,`x`]) 356 357(* sets *) 358val _ = overload_on ("set_pmact", ``��pm. mk_pmact (fnpm pm discrete_pmact) : �� set pmact``); 359val _ = overload_on ("setpm", ``��pm. pmact (set_pmact pm)``); 360 361val pmact_IN = Store_thm( 362 "pmact_IN", 363 ``(x IN (setpm pm �� s) = pmact pm ������� x IN s)``, 364 SRW_TAC [][fnpm_raw, SPECIFICATION] THEN 365 let open combinTheory in 366 METIS_TAC [pmact_bijections, K_THM, I_THM, discrete_is_pmact] 367 end); 368 369val pmact_UNIV = Store_thm( 370 "pmact_UNIV", 371 ``setpm pm �� UNIV = UNIV``, 372 SRW_TAC [][EXTENSION, SPECIFICATION, fnpm_def] THEN 373 SRW_TAC [][UNIV_DEF]); 374 375val pmact_EMPTY = Store_thm( 376 "pmact_EMPTY", 377 ``setpm pm �� {} = {}``, 378 SRW_TAC [][EXTENSION, SPECIFICATION, fnpm_def] THEN 379 SRW_TAC [][EMPTY_DEF]); 380 381val pmact_INSERT = store_thm( 382 "pmact_INSERT", 383 ``setpm pm �� (e INSERT s) = pmact pm �� e INSERT setpm pm �� s``, 384 SRW_TAC [][EXTENSION, pmact_IN, pmact_eql]); 385 386val pmact_UNION = store_thm( 387 "pmact_UNION", 388 ``setpm pm �� (s1 UNION s2) = setpm pm �� s1 UNION setpm pm �� s2``, 389 SRW_TAC [][EXTENSION, pmact_IN]); 390 391val pmact_DIFF = store_thm( 392 "pmact_DIFF", 393 ``setpm pm pi (s DIFF t) = setpm pm pi s DIFF setpm pm pi t``, 394 SRW_TAC [][EXTENSION, pmact_IN]); 395 396val pmact_DELETE = store_thm( 397 "pmact_DELETE", 398 ``setpm pm p (s DELETE e) = setpm pm p s DELETE pmact pm p e``, 399 SRW_TAC [][EXTENSION, pmact_IN, pmact_eql]); 400 401val pmact_FINITE = Store_thm( 402 "pmact_FINITE", 403 ``FINITE (setpm pm p s) = FINITE s``, 404 Q_TAC SUFF_TAC `(!s. FINITE s ==> FINITE (setpm pm p s)) /\ 405 (!s. FINITE s ==> !t p. (setpm pm p t = s) ==> FINITE t)` 406 THEN1 METIS_TAC [] THEN 407 CONJ_TAC THENL [ 408 HO_MATCH_MP_TAC FINITE_INDUCT THEN SRW_TAC [][pmact_INSERT], 409 HO_MATCH_MP_TAC FINITE_INDUCT THEN 410 SRW_TAC [][pmact_eql, pmact_INSERT] 411 ]); 412 413(* options *) 414 415val raw_optpm_def = Define` 416 (raw_optpm pm pi NONE = NONE) /\ 417 (raw_optpm pm pi (SOME x) = SOME (pmact pm pi x))`; 418val _ = export_rewrites ["raw_optpm_def"]; 419 420val _ = overload_on("opt_pmact",``��pm. mk_pmact (raw_optpm pm)``); 421val _ = overload_on("optpm",``��pm. pmact (opt_pmact pm)``); 422 423val optpm_raw = store_thm( 424"optpm_raw", 425``optpm pm = raw_optpm pm``, 426srw_tac [][GSYM pmact_bijections] >> 427srw_tac [][is_pmact_def] THENL [ 428 Cases_on `x` THEN SRW_TAC [][], 429 Cases_on `x` THEN SRW_TAC [][pmact_decompose], 430 srw_tac [][FUN_EQ_THM] >> 431 Cases_on `x` THEN SRW_TAC [][] THEN 432 AP_THM_TAC >> srw_tac [][] 433]); 434 435val optpm_thm = Save_thm( 436"optpm_thm", 437raw_optpm_def |> CONJUNCTS |> map SPEC_ALL |> map (SUBS [GSYM optpm_raw]) |> LIST_CONJ) 438 439(* pairs *) 440val raw_pairpm_def = Define` 441 raw_pairpm apm bpm pi (a,b) = (pmact apm pi a, pmact bpm pi b) 442`; 443val _ = export_rewrites ["raw_pairpm_def"] 444 445val _ = overload_on("pair_pmact",``��apm bpm. mk_pmact (raw_pairpm apm bpm)``); 446val _ = overload_on("pairpm",``��apm bpm. pmact (pair_pmact apm bpm)``); 447 448val pairpm_raw = store_thm( 449 "pairpm_raw", 450 ``pairpm apm bpm = raw_pairpm apm bpm``, 451 srw_tac [][GSYM pmact_bijections] >> 452 SIMP_TAC (srw_ss()) [is_pmact_def, pairTheory.FORALL_PROD, 453 FUN_EQ_THM, pmact_decompose] >> 454 metis_tac [pmact_permeq]); 455 456val pairpm_thm = Save_thm( 457"pairpm_thm", 458raw_pairpm_def |> SPEC_ALL |> SUBS [GSYM pairpm_raw] |> 459(rev_itlist Q.GEN) [`apm`,`bpm`,`pi`,`a`,`b`]); 460 461val FST_pairpm = Store_thm( 462 "FST_pairpm", 463 ``FST (pairpm pm1 pm2 pi v) = pmact pm1 pi (FST v)``, 464 Cases_on `v` THEN SRW_TAC [][]); 465 466val SND_pairpm = Store_thm( 467 "SND_pairpm", 468 ``SND (pairpm pm1 pm2 pi v) = pmact pm2 pi (SND v)``, 469 Cases_on `v` THEN SRW_TAC [][]); 470 471(* sums *) 472val raw_sumpm_def = Define` 473 (raw_sumpm pm1 pm2 pi (INL x) = INL (pmact pm1 pi x)) /\ 474 (raw_sumpm pm1 pm2 pi (INR y) = INR (pmact pm2 pi y)) 475`; 476val _ = export_rewrites ["raw_sumpm_def"] 477 478val _ = overload_on("sum_pmact",``��pm1 pm2. mk_pmact (raw_sumpm pm1 pm2)``); 479val _ = overload_on("sumpm",``��pm1 pm2. pmact (sum_pmact pm1 pm2)``); 480 481val sumpm_raw = store_thm( 482 "sumpm_raw", 483 ``sumpm pm1 pm2 = raw_sumpm pm1 pm2``, 484 srw_tac [][GSYM pmact_bijections] >> 485 SRW_TAC [][is_pmact_def, FUN_EQ_THM] THEN Cases_on `x` THEN 486 SRW_TAC [][pmact_decompose] >> AP_THM_TAC >> srw_tac [][pmact_permeq]); 487 488val sumpm_thm = Save_thm( 489"sumpm_thm", 490raw_sumpm_def |> CONJUNCTS 491|> map (fn th => th |> Q.SPECL [`pm1`,`pm2`] 492 |> SUBS [GSYM sumpm_raw] 493 |> (itlist Q.GEN [`pm1`,`pm2`])) 494|> LIST_CONJ); 495 496(* lists *) 497val raw_listpm_def = Define` 498 (raw_listpm apm pi [] = []) /\ 499 (raw_listpm apm pi (h::t) = pmact apm pi h :: raw_listpm apm pi t) 500`; 501val _ = export_rewrites ["raw_listpm_def"] 502 503val _ = overload_on("list_pmact",``��apm. mk_pmact (raw_listpm apm)``); 504val _ = overload_on("listpm",``��apm. pmact (list_pmact apm)``) 505 506val listpm_raw = store_thm( 507 "listpm_raw", 508 ``listpm apm = raw_listpm apm``, 509 srw_tac [][GSYM pmact_bijections] >> 510 SIMP_TAC (srw_ss()) [is_pmact_def, FUN_EQ_THM] THEN 511 STRIP_TAC THEN REPEAT CONJ_TAC THENL [ 512 Induct THEN SRW_TAC [][], 513 Induct_on `x` THEN SRW_TAC [][pmact_decompose], 514 REPEAT GEN_TAC THEN STRIP_TAC THEN Induct THEN SRW_TAC [][] >> 515 AP_THM_TAC >> srw_tac [][pmact_permeq] 516 ]); 517 518val listpm_thm = Save_thm( 519"listpm_thm", 520raw_listpm_def |> CONJUNCTS 521|> map (fn th => th |> Q.SPEC `apm` |> SUBS [GSYM listpm_raw] |> Q.GEN `apm`) 522|> LIST_CONJ) 523 524val listpm_MAP = store_thm( 525 "listpm_MAP", 526 ``!l. listpm pm pi l = MAP (pmact pm pi) l``, 527 Induct THEN fsrw_tac [][]); 528 529val listpm_APPENDlist = store_thm( 530 "listpm_APPENDlist", 531 ``listpm pm pi (l1 ++ l2) = listpm pm pi l1 ++ listpm pm pi l2``, 532 Induct_on `l1` THEN fsrw_tac [][]); 533 534val LENGTH_listpm = Store_thm( 535 "LENGTH_listpm", 536 ``LENGTH (listpm pm pi l) = LENGTH l``, 537 Induct_on `l` >> fsrw_tac [][]) 538 539val EL_listpm = Store_thm( 540 "EL_listpm", 541 ``���l n. n < LENGTH l ==> (EL n (listpm pm pi l) = pmact pm pi (EL n l))``, 542 Induct >> srw_tac [][] >> Cases_on `n` >> srw_tac [][] >> 543 fsrw_tac [][]); 544 545val MEM_listpm = store_thm( 546 "MEM_listpm", 547 ``MEM x (listpm pm pi l) ��� MEM (pmact pm pi����� x) l``, 548 Induct_on `l` >> fsrw_tac [][pmact_eql]); 549 550val MEM_listpm_EXISTS = store_thm( 551 "MEM_listpm_EXISTS", 552 ``MEM x (listpm pm pi l) ��� ���y. MEM y l ��� (x = pmact pm pi y)``, 553 Induct_on `l` >> fsrw_tac [][] >> metis_tac []); 554 555(* lists of pairs of strings, (concrete rep for permutations) *) 556val _ = overload_on("cpm_pmact", ``list_pmact (pair_pmact string_pmact string_pmact)``); 557val _ = overload_on ("cpmpm", ``pmact cpm_pmact``); 558 559(* ---------------------------------------------------------------------- 560 Notion of support, and calculating the smallest set of support 561 ---------------------------------------------------------------------- *) 562 563val support_def = Define` 564 support (pm : �� pmact) (a:��) (supp:string set) = 565 ���x y. x ��� supp /\ y ��� supp ��� (pmact pm [(x,y)] a = a) 566`; 567 568val pmact_support = store_thm( 569 "pmact_support", 570 ``(support pm (pmact pm �� x) s = 571 support pm x (setpm string_pmact ������� s))``, 572 ASM_SIMP_TAC (srw_ss()) [EQ_IMP_THM, support_def, pmact_IN] THEN 573 STRIP_TAC THEN STRIP_TAC THEN 574 MAP_EVERY Q.X_GEN_TAC [`a`,`b`] THEN STRIP_TAC THENL [ 575 `pmact pm [(stringpm �� a, stringpm �� b)] (pmact pm �� x) = pmact pm �� x` 576 by METIS_TAC [] THEN 577 `pmact pm ([(stringpm �� a, stringpm �� b)] ++ ��) x = pmact pm �� x` 578 by METIS_TAC [pmact_decompose] THEN 579 `[(stringpm �� a, stringpm �� b)] ++ �� == �� ++ [(a,b)]` 580 by METIS_TAC [permeq_swap_ends, permeq_sym, listTheory.APPEND] THEN 581 `pmact pm (�� ++ [(a,b)]) x = pmact pm �� x` 582 by METIS_TAC [pmact_permeq] THEN 583 METIS_TAC [pmact_injective, pmact_decompose], 584 `pmact pm [(a,b)] (pmact pm �� x) = pmact pm ([(a,b)] ++ ��) x` 585 by METIS_TAC [pmact_decompose] THEN 586 `[(a,b)] ++ �� == �� ++ [(stringpm ������� a, stringpm ������� b)]` 587 by (SRW_TAC [][] THEN 588 Q.SPECL_THEN [`��`, `lswapstr ������� a`, `lswapstr ������� b`] 589 (ASSUME_TAC o REWRITE_RULE [pmact_inverse]) 590 permeq_swap_ends THEN 591 METIS_TAC [permeq_sym]) THEN 592 `pmact pm [(a,b)] (pmact pm �� x) = 593 pmact pm (�� ++ [(stringpm ������� a, stringpm ������� b)]) x` 594 by METIS_TAC [pmact_permeq] THEN 595 ` _ = pmact pm �� (pmact pm [(stringpm ������� a, stringpm ������� b)] x)` 596 by METIS_TAC [pmact_decompose] THEN 597 ASM_SIMP_TAC (srw_ss()) [pmact_injective] 598 ]); 599 600val support_dwards_directed = store_thm( 601 "support_dwards_directed", 602 ``support pm e s1 /\ support pm e s2 /\ 603 FINITE s1 /\ FINITE s2 ==> 604 support pm e (s1 INTER s2)``, 605 SIMP_TAC bool_ss [support_def] THEN 606 REPEAT STRIP_TAC THEN 607 Cases_on `x = y` THEN1 METIS_TAC [pmact_id, pmact_nil] THEN 608 Q_TAC (NEW_TAC "z") `{x;y} UNION s1 UNION s2` THEN 609 `[(x,y)] == [(x,z); (y,z); (x,z)]` 610 by (SRW_TAC [][FUN_EQ_THM, permeq_def] THEN 611 CONV_TAC (RAND_CONV 612 (ONCE_REWRITE_CONV [GSYM swapstr_swapstr])) THEN 613 SIMP_TAC bool_ss [swapstr_inverse] THEN 614 SRW_TAC [][]) THEN 615 `pmact pm [(x,y)] e = pmact pm [(x,z); (y,z); (x,z)] e` 616 by METIS_TAC [pmact_permeq] THEN 617 ` _ = pmact pm [(x,z)] (pmact pm [(y,z)] (pmact pm [(x,z)] e))` 618 by METIS_TAC [pmact_decompose, listTheory.APPEND] THEN 619 METIS_TAC [IN_INTER]); 620 621val supp_def = Define` 622 supp pm x = { (a:string) | INFINITE { (b:string) | pmact pm [(a,b)] x ��� x}} 623`; 624 625val supp_supports = store_thm( 626 "supp_supports", 627 ``support pm x (supp pm x)``, 628 ASM_SIMP_TAC (srw_ss()) [support_def, supp_def, pmact_decompose] THEN 629 MAP_EVERY Q.X_GEN_TAC [`a`, `b`] THEN STRIP_TAC THEN 630 Q.ABBREV_TAC `aset = {b | ~(pmact pm [(a,b)] x = x)}` THEN 631 Q.ABBREV_TAC `bset = {c | ~(pmact pm [(b,c)] x = x)}` THEN 632 Cases_on `a = b` THEN1 SRW_TAC [][pmact_id, pmact_nil] THEN 633 `?c. ~(c IN aset) /\ ~(c IN bset) /\ ~(c = a) /\ ~(c = b)` 634 by (Q.SPEC_THEN `{a;b} UNION aset UNION bset` MP_TAC NEW_def THEN 635 SRW_TAC [][] THEN METIS_TAC []) THEN 636 `(pmact pm [(a,c)] x = x) /\ (pmact pm [(b,c)] x = x)` 637 by FULL_SIMP_TAC (srw_ss()) [Abbr`aset`, Abbr`bset`] THEN 638 `pmact pm ([(a,c)] ++ [(b,c)] ++ [(a,c)]) x = x` 639 by SRW_TAC [][pmact_decompose] THEN 640 Q_TAC SUFF_TAC `[(a,c)] ++ [(b,c)] ++ [(a,c)] == [(a,b)]` 641 THEN1 METIS_TAC [pmact_permeq] THEN 642 SIMP_TAC (srw_ss()) [permeq_def, FUN_EQ_THM] THEN 643 ONCE_REWRITE_TAC [GSYM swapstr_swapstr] THEN 644 `(swapstr a c b = b) /\ (swapstr a c c = a)` by SRW_TAC [][swapstr_def] THEN 645 ASM_REWRITE_TAC [] THEN SRW_TAC [][]); 646 647val supp_fresh = store_thm( 648 "supp_fresh", 649 ``x ��� supp apm v /\ y ��� supp apm v ��� (pmact apm [(x,y)] v = v)``, 650 METIS_TAC [support_def, supp_supports]); 651 652val setpm_postcompose = store_thm( 653 "setpm_postcompose", 654 ``!P pm p. is_pmact pm ==> ({x | P (pm p x)} = setpm (mk_pmact pm) p����� {x | P x})``, 655 SRW_TAC [][EXTENSION, pmact_IN] >> metis_tac [pmact_bijections]); 656 657val perm_supp = store_thm( 658 "perm_supp", 659 ``supp pm (pmact pm p x) = setpm string_pmact p (supp pm x)``, 660 SIMP_TAC (srw_ss()) [EXTENSION, pmact_IN, supp_def, pmact_eql] THEN 661 Q.X_GEN_TAC `a` THEN 662 `!e x y. pmact pm (REVERSE p) (pmact pm [(x,y)] e) = 663 pmact pm [(stringpm (REVERSE p) x, stringpm (REVERSE p) y)] 664 (pmact pm (REVERSE p) e)` 665 by METIS_TAC [stringpm_raw, pmact_decompose, pmact_permeq, permeq_swap_ends, listTheory.APPEND] THEN 666 SRW_TAC [][pmact_inverse] THEN 667 Q.MATCH_ABBREV_TAC `FINITE s1 = FINITE s2` THEN 668 `s1 = { b | (\s. ~(x = pmact pm [(stringpm (REVERSE p) a, s)] x)) 669 (stringpm (REVERSE p ) b)}` 670 by SRW_TAC [][Abbr`s1`] THEN 671 ` _ = setpm (mk_pmact stringpm) (REVERSE (REVERSE p)) 672 {b | (\s. ~(x = pmact pm [(stringpm (REVERSE p) a, s)] x)) b}` 673 by (MATCH_MP_TAC setpm_postcompose THEN SRW_TAC [][]) THEN 674 Q.UNABBREV_TAC `s2` THEN SRW_TAC [][]); 675 676val supp_apart = store_thm( 677 "supp_apart", 678 ``a ��� supp pm x /\ b ��� supp pm x ��� pmact pm [(a,b)] x ��� x``, 679 STRIP_TAC THEN 680 `a ��� b` by METIS_TAC [] THEN 681 `b ��� setpm string_pmact [(a,b)] (supp pm x)` 682 by SRW_TAC[][pmact_IN, swapstr_def] THEN 683 `b ��� supp pm (pmact pm [(a,b)] x)` 684 by metis_tac [perm_supp] THEN 685 `supp pm x ��� supp pm (pmact pm [(a,b)] x)` by METIS_TAC [] THEN 686 METIS_TAC []); 687 688val supp_finite_or_UNIV = store_thm( 689 "supp_finite_or_UNIV", 690 ``INFINITE (supp pm x) ��� (supp pm x = UNIV)``, 691 STRIP_TAC THEN 692 SPOSE_NOT_THEN (Q.X_CHOOSE_THEN `a` MP_TAC o 693 SIMP_RULE (srw_ss()) [EXTENSION]) THEN 694 DISCH_THEN (fn th => ASSUME_TAC th THEN MP_TAC th THEN 695 SIMP_TAC (srw_ss()) [supp_def]) THEN 696 STRIP_TAC THEN 697 `���b. b ��� {b | pmact pm [(a,b)] x ��� x} ��� b ��� supp pm x` 698 by METIS_TAC [IN_INFINITE_NOT_FINITE] THEN 699 FULL_SIMP_TAC (srw_ss()) [] THEN 700 METIS_TAC [supp_apart, pmact_flip_args]); 701 702val supp_absence_FINITE = store_thm( 703 "supp_absence_FINITE", 704 ``a ��� supp pm x ��� FINITE (supp pm x)``, 705 METIS_TAC [IN_UNIV, supp_finite_or_UNIV]); 706 707(* lemma3_4_i from Pitts & Gabbay - New Approach to Abstract Syntax *) 708val supp_smallest = store_thm( 709 "supp_smallest", 710 ``support pm x s /\ FINITE s ==> supp pm x SUBSET s``, 711 REPEAT STRIP_TAC THEN 712 REWRITE_TAC [SUBSET_DEF] THEN 713 Q.X_GEN_TAC `a` THEN 714 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 715 `!b. ~(b IN s) ==> (pmact pm [(a,b)] x = x)` 716 by METIS_TAC [support_def] THEN 717 `{b | ~(pmact pm [(a,b)] x = x)} SUBSET s` 718 by (SRW_TAC [][SUBSET_DEF] THEN METIS_TAC []) THEN 719 `FINITE {b | ~(pmact pm [(a,b)] x = x)}` by METIS_TAC [SUBSET_FINITE] THEN 720 FULL_SIMP_TAC (srw_ss()) [supp_def]); 721 722val notinsupp_I = store_thm( 723 "notinsupp_I", 724 ``���A apm e x. FINITE A ��� support apm x A ��� e ��� A ==> e ��� supp apm x``, 725 metis_tac [supp_smallest, SUBSET_DEF]); 726 727val lemma0 = prove( 728 ``COMPL (e INSERT s) = COMPL s DELETE e``, 729 SRW_TAC [][EXTENSION] THEN METIS_TAC []); 730val lemma = prove( 731 ``!s: string set. FINITE s ==> ~FINITE (COMPL s)``, 732 HO_MATCH_MP_TAC FINITE_INDUCT THEN SRW_TAC [][lemma0] THEN 733 SRW_TAC [][INFINITE_STR_UNIV]); 734 735val supp_unique = store_thm( 736 "supp_unique", 737 ``support pm x s /\ FINITE s /\ 738 (!s'. support pm x s' /\ FINITE s' ==> s SUBSET s') ==> 739 (supp pm x = s)``, 740 SRW_TAC [][] THEN 741 `FINITE (supp pm x)` by METIS_TAC [supp_smallest, SUBSET_FINITE] THEN 742 `support pm x (supp pm x)` by METIS_TAC [supp_supports] THEN 743 `!s'. support pm x s' /\ FINITE s' ==> supp pm x SUBSET s'` 744 by METIS_TAC [supp_smallest] THEN 745 METIS_TAC [SUBSET_ANTISYM]); 746 747val supp_unique_apart = store_thm( 748 "supp_unique_apart", 749 ``support pm x s /\ FINITE s /\ 750 (!a b. a IN s /\ ~(b IN s) ==> ~(pmact pm [(a,b)] x = x)) ==> 751 (supp pm x = s)``, 752 STRIP_TAC THEN MATCH_MP_TAC supp_unique THEN 753 ASM_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][SUBSET_DEF] THEN 754 SPOSE_NOT_THEN ASSUME_TAC THEN 755 `?z. ~(z IN s') /\ ~(z IN s)` 756 by (Q.SPEC_THEN `s UNION s'` MP_TAC NEW_def THEN 757 SRW_TAC [][] THEN METIS_TAC []) THEN 758 METIS_TAC [support_def]); 759 760(* some examples of supp *) 761val supp_string = Store_thm( 762 "supp_string", 763 ``supp string_pmact s = {s}``, 764 MATCH_MP_TAC supp_unique_apart THEN SRW_TAC [][support_def]); 765 766val supp_discrete = Store_thm( 767 "supp_discrete", 768 ``supp discrete_pmact x = {}``, 769 SRW_TAC [][supp_def]); 770 771val supp_unitfn = store_thm( 772 "supp_unitfn", 773 ``(supp (fn_pmact discrete_pmact apm) (��u:unit. a) = supp apm a)``, 774 Cases_on `���x. x ��� supp apm a` >| [ 775 fsrw_tac [][] >> 776 match_mp_tac (GEN_ALL supp_unique_apart) >> 777 srw_tac [][support_def, FUN_EQ_THM, fnpm_def, supp_fresh] >- 778 metis_tac [supp_absence_FINITE] >> 779 metis_tac [supp_apart], 780 fsrw_tac [][] >> 781 `supp apm a = univ(:string)` by srw_tac [][EXTENSION] >> 782 fsrw_tac [][EXTENSION, supp_def, FUN_EQ_THM, fnpm_def] 783 ]) 784 785(* options *) 786val supp_optpm = store_thm( 787 "supp_optpm", 788 ``(supp (opt_pmact pm) NONE = {}) /\ 789 (supp (opt_pmact pm) (SOME x) = supp pm x)``, 790 SRW_TAC [][supp_def]); 791val _ = export_rewrites ["supp_optpm"] 792 793(* pairs *) 794val supp_pairpm = Store_thm( 795 "supp_pairpm", 796 ``(supp (pair_pmact pm1 pm2) (x,y) = supp pm1 x UNION supp pm2 y)``, 797 SRW_TAC [][supp_def, GSPEC_OR]); 798 799(* lists *) 800val supp_listpm = Store_thm( 801 "supp_listpm", 802 ``(supp (list_pmact apm) [] = {}) /\ 803 (supp (list_pmact apm) (h::t) = supp apm h UNION supp (list_pmact apm) t)``, 804 SRW_TAC [][supp_def, GSPEC_OR]); 805 806val listsupp_APPEND = Store_thm( 807 "listsupp_APPEND", 808 ``supp (list_pmact p) (l1 ++ l2) = supp (list_pmact p) l1 ��� supp (list_pmact p) l2``, 809 Induct_on `l1` THEN SRW_TAC [][AC UNION_ASSOC UNION_COMM]); 810 811val listsupp_REVERSE = Store_thm( 812 "listsupp_REVERSE", 813 ``supp (list_pmact p) (REVERSE l) = supp (list_pmact p) l``, 814 Induct_on `l` THEN SRW_TAC [][UNION_COMM]); 815 816val IN_supp_listpm = store_thm( 817 "IN_supp_listpm", 818 ``a ��� supp (list_pmact pm) l ��� ���e. MEM e l ��� a ��� supp pm e``, 819 Induct_on `l` >> srw_tac [DNF_ss][]); 820 821val NOT_IN_supp_listpm = store_thm( 822 "NOT_IN_supp_listpm", 823 ``a ��� supp (list_pmact pm) l ��� ���e. MEM e l ��� a ��� supp pm e``, 824 metis_tac [IN_supp_listpm]) 825 826 827(* concrete permutations, which get their own overload for calculating their 828 support *) 829val _ = overload_on ("patoms", ``supp (list_pmact (pair_pmact string_pmact string_pmact))``) 830 831val FINITE_patoms = Store_thm( 832 "FINITE_patoms", 833 ``!l. FINITE (patoms l)``, 834 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 835 836val patoms_fresh = Store_thm( 837 "patoms_fresh", 838 ``!p. x ��� patoms p ��� y ��� patoms p ��� (cpmpm [(x,y)] p = p)``, 839 METIS_TAC [supp_supports, support_def]); 840 841val lswapstr_unchanged = store_thm( 842 "lswapstr_unchanged", 843 ``!p. s ��� patoms p ��� (lswapstr p s = s)``, 844 Induct THEN SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 845 SRW_TAC [][swapstr_def]); 846 847val IN_patoms_MEM = store_thm( 848 "IN_patoms_MEM", 849 ``a ��� patoms �� ��� (���b. MEM (a,b) ��) ��� (���b. MEM (b,a) ��)``, 850 Induct_on `��` THEN1 SRW_TAC [][] THEN 851 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN METIS_TAC []); 852 853val pm_cpmpm_cancel = prove( 854 ``pmact pm [(x,y)] (pmact pm (cpmpm [(x,y)] pi) (pmact pm [(x,y)] t)) = pmact pm pi t``, 855 Induct_on `pi` THEN 856 fsrw_tac [][pairTheory.FORALL_PROD, pmact_nil, 857 pmact_sing_inv] THEN 858 `!p q pi t. pmact pm ((swapstr x y p, swapstr x y q)::pi) t = 859 pmact pm [(swapstr x y p, swapstr x y q)] (pmact pm pi t)` 860 by SRW_TAC [][GSYM pmact_decompose] THEN 861 REPEAT GEN_TAC THEN 862 POP_ASSUM (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th]))) THEN 863 ONCE_REWRITE_TAC [GSYM pmact_sing_to_back] THEN 864 fsrw_tac [][GSYM pmact_decompose] >> 865 metis_tac [pmact_decompose,listTheory.APPEND]); 866 867val pmact_supp_empty = store_thm( 868 "pmact_supp_empty", 869 ``(supp (fn_pmact cpm_pmact (fn_pmact pm pm)) (pmact pm) = {})``, 870 MATCH_MP_TAC supp_unique_apart THEN SRW_TAC [][] THEN 871 SRW_TAC [][support_def, FUN_EQ_THM, fnpm_def, pm_cpmpm_cancel]); 872 873val supp_pm_fresh = store_thm( 874 "supp_pm_fresh", 875 ``(supp pm x = {}) ==> (pmact pm pi x = x)``, 876 Induct_on `pi` THEN 877 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, pmact_nil] THEN 878 REPEAT STRIP_TAC THEN 879 `pmact pm ((p_1,p_2)::pi) x = pmact pm [(p_1,p_2)] (pmact pm pi x)` 880 by SIMP_TAC (srw_ss()) [GSYM pmact_decompose] THEN 881 SRW_TAC [][supp_fresh]); 882 883val pm_pm_cpmpm = store_thm( 884 "pm_pm_cpmpm", 885 ``pmact pm pi1 (pmact pm pi2 s) = pmact pm (cpmpm pi1 pi2) (pmact pm pi1 s)``, 886 Q.MATCH_ABBREV_TAC `L = R` THEN 887 `L = fnpm pm pm pi1 (pmact pm pi2) (pmact pm pi1 s)` 888 by SRW_TAC [][fnpm_def, pmact_inverse] THEN 889 `_ = fnpm cpm_pmact 890 (fn_pmact pm pm) 891 pi1 892 (pmact pm) 893 (cpmpm pi1 pi2) 894 (pmact pm pi1 s)` 895 by (ONCE_REWRITE_TAC [fnpm_def] THEN 896 SRW_TAC [][pmact_inverse]) THEN 897 `fnpm cpm_pmact (fn_pmact pm pm) pi1 (pmact pm) = (pmact pm)` 898 by SRW_TAC [][supp_pm_fresh, pmact_supp_empty] THEN 899 METIS_TAC []); 900 901val stringpm_stringpm_cpmpm = save_thm( 902 "stringpm_stringpm_cpmpm", 903 (SIMP_RULE std_ss [] o Q.INST [`pm` |-> `string_pmact`] o 904 INST_TYPE [alpha |-> ``:string``]) pm_pm_cpmpm); 905 906val patoms_cpmpm = store_thm( 907 "patoms_cpmpm", 908 ``patoms (cpmpm pi1 pi2) = setpm string_pmact pi1 (patoms pi2)``, 909 SRW_TAC [][perm_supp]); 910 911(* support for honest to goodness permutations, not just their 912 representations *) 913val perm_supp_SUBSET_plistvars = prove( 914 ``!p. {s | ~(lswapstr p s = s)} SUBSET 915 FOLDR (\p a. {FST p; SND p} UNION a) {} p``, 916 ASM_SIMP_TAC (srw_ss()) [pred_setTheory.SUBSET_DEF] THEN Induct THEN 917 SRW_TAC [][] THEN 918 Cases_on `x = FST h` THEN SRW_TAC [][] THEN 919 Cases_on `x = SND h` THEN SRW_TAC [][] THEN 920 FULL_SIMP_TAC (srw_ss()) [swapstr_def, swapstr_eq_left]); 921 922val FINITE_plistvars = prove( 923 ``FINITE (FOLDR (\p a. {FST p; SND p} UNION a) {} p)``, 924 Induct_on `p` THEN SRW_TAC [][]); 925val lemma = MATCH_MP pred_setTheory.SUBSET_FINITE FINITE_plistvars 926 927val perm_supp_finite = store_thm( 928 "perm_supp_finite", 929 ``FINITE {s | ~(lswapstr p s = s)}``, 930 MATCH_MP_TAC lemma THEN SRW_TAC [][perm_supp_SUBSET_plistvars]); 931 932val supp_perm_of = store_thm( 933 "supp_perm_of", 934 ``supp (fn_pmact string_pmact string_pmact) (lswapstr p) = 935 { s | ~(lswapstr p s = s) }``, 936 HO_MATCH_MP_TAC supp_unique THEN 937 ASM_SIMP_TAC (srw_ss()) [perm_supp_finite] THEN CONJ_TAC THENL [ 938 SRW_TAC [][support_def, FUN_EQ_THM, fnpm_def, lswapstr_swapstr], 939 940 Q.X_GEN_TAC `s` THEN 941 SRW_TAC [][pred_setTheory.SUBSET_DEF] THEN 942 SPOSE_NOT_THEN ASSUME_TAC THEN 943 Q_TAC (NEW_TAC "y") `{x; lswapstr p����� x} UNION s` THEN 944 `!a. fnpm string_pmact string_pmact [(x,y)] (lswapstr p) a = lswapstr p a` 945 by METIS_TAC [support_def] THEN 946 `p ++ [(x,y)] == [(x,y)] ++ p` 947 by (POP_ASSUM (ASSUME_TAC o SIMP_RULE (srw_ss()) [fnpm_def]) THEN 948 SRW_TAC [][permeq_thm, pmact_decompose, GSYM swapstr_eq_left]) THEN 949 `(x,y) :: p == (lswapstr p x, lswapstr p y) :: p` 950 by METIS_TAC [permeq_swap_ends, permeq_trans, permeq_sym, 951 listTheory.APPEND] THEN 952 `(x,y) :: (p ++ p�����) == (lswapstr p x, lswapstr p y) :: (p ++ p�����)` 953 by METIS_TAC [app_permeq_monotone, listTheory.APPEND, permeq_refl] THEN 954 `!h. [h] == h :: (p ++ p�����)` 955 by METIS_TAC [permeq_cons_monotone, permof_inverse, permeq_sym] THEN 956 `[(x,y)] == [(lswapstr p x, lswapstr p y)]` 957 by METIS_TAC [permeq_trans, permeq_sym] THEN 958 `lswapstr [(x,y)] x = lswapstr [(lswapstr p x, lswapstr p y)] x` 959 by METIS_TAC [permeq_thm] THEN 960 POP_ASSUM MP_TAC THEN 961 SIMP_TAC (srw_ss()) [] THEN 962 `x ��� lswapstr p y` by METIS_TAC [pmact_inverse] THEN 963 SRW_TAC [][swapstr_def] 964 ]); 965 966val support_FINITE_supp = store_thm( 967 "support_FINITE_supp", 968 ``support pm v A /\ FINITE A ==> FINITE (supp pm v)``, 969 METIS_TAC [supp_smallest, SUBSET_FINITE]); 970 971val support_fnapp = store_thm( 972 "support_fnapp", 973 ``support (fn_pmact dpm rpm) f A /\ support dpm d B ==> 974 support rpm (f d) (A UNION B)``, 975 SRW_TAC [][support_def] THEN 976 fsrw_tac [][fnpm_def,FUN_EQ_THM] >> 977 metis_tac []); 978 979val supp_fnapp = store_thm( 980 "supp_fnapp", 981 ``supp rpm (f x) SUBSET supp (fn_pmact dpm rpm) f UNION supp dpm x``, 982 METIS_TAC [supp_smallest, FINITE_UNION, supp_supports, support_fnapp, 983 supp_finite_or_UNIV, SUBSET_UNIV, UNION_UNIV]); 984 985val notinsupp_fnapp = store_thm( 986 "notinsupp_fnapp", 987 ``v ��� supp (fn_pmact dpm rpm) f ��� v ��� supp dpm x ==> 988 v ��� supp rpm (f x)``, 989 prove_tac [supp_fnapp, SUBSET_DEF, IN_UNION]); 990 991open finite_mapTheory 992val raw_fmpm_def = Define` 993 raw_fmpm (dpm : 'd pmact) (rpm : 'r pmact) pi fmap = 994 pmact rpm pi o_f fmap f_o pmact dpm (REVERSE pi) 995`; 996val _ = export_rewrites["raw_fmpm_def"]; 997 998val _ = overload_on("fm_pmact",``��dpm rpm. mk_pmact (raw_fmpm dpm rpm)``); 999val _ = overload_on("fmpm",``��dpm rpm. pmact (fm_pmact dpm rpm)``); 1000 1001val lemma0 = prove( 1002 ``(pmact pm pi x ��� X = x ��� setpm pm (REVERSE pi) X)``, 1003 SRW_TAC [][pmact_IN]) 1004val lemma1 = prove(``{x | x ��� X} = X``, SRW_TAC [][pred_setTheory.EXTENSION]) 1005val lemma = prove( 1006 ``FINITE { x | pmact pm pi x ��� FDOM f}``, 1007 SIMP_TAC bool_ss [lemma0, lemma1, pmact_FINITE, 1008 finite_mapTheory.FDOM_FINITE]); 1009 1010val fmpm_def = store_thm( 1011 "fmpm_def", 1012 ``fmpm dpm rpm = raw_fmpm dpm rpm``, 1013 srw_tac [][GSYM pmact_bijections] >> 1014 SRW_TAC [][is_pmact_def] THENL [ 1015 `(!d. pmact dpm [] d = d) ��� (!r. pmact rpm [] r = r)` by METIS_TAC [pmact_nil] THEN 1016 SRW_TAC [][fmap_EXT, pred_setTheory.EXTENSION, FDOM_f_o, lemma, 1017 FAPPLY_f_o, o_f_FAPPLY], 1018 1019 `(!d pi1 pi2. pmact dpm (pi1 ++ pi2) d = pmact dpm pi1 (pmact dpm pi2 d)) ��� 1020 (!r pi1 pi2. pmact rpm (pi1 ++ pi2) r = pmact rpm pi1 (pmact rpm pi2 r))` 1021 by METIS_TAC [pmact_decompose] THEN 1022 SRW_TAC [][fmap_EXT, FDOM_f_o, lemma, o_f_FAPPLY, 1023 listTheory.REVERSE_APPEND, FAPPLY_f_o], 1024 1025 `REVERSE p1 == REVERSE p2` by METIS_TAC [permof_REVERSE_monotone] THEN 1026 `(pmact rpm p1 = pmact rpm p2) ��� (pmact dpm (REVERSE p1) = pmact dpm (REVERSE p2))` 1027 by METIS_TAC [pmact_permeq] THEN 1028 SRW_TAC [][fmap_EXT, FUN_EQ_THM, FDOM_f_o, lemma] 1029 ]); 1030 1031val fmpm_applied = store_thm( 1032 "fmpm_applied", 1033 ``pmact dpm (REVERSE pi) x ��� FDOM fm ==> 1034 (fmpm dpm rpm pi fm ' x = pmact rpm pi (fm ' (pmact dpm (REVERSE pi) x)))``, 1035 SRW_TAC [][fmpm_def, FAPPLY_f_o, FDOM_f_o, lemma, o_f_FAPPLY]); 1036 1037val fmpm_FDOM = store_thm( 1038 "fmpm_FDOM", 1039 ``x IN FDOM (fmpm dpm rpm pi fmap) = pmact dpm (REVERSE pi) x IN FDOM fmap``, 1040 SRW_TAC [][fmpm_def, lemma, FDOM_f_o]) 1041 1042val supp_setpm = store_thm( 1043 "supp_setpm", 1044 ``FINITE s ��� (���x. x ��� s ��� FINITE (supp pm x)) ��� 1045 (supp (set_pmact pm) s = BIGUNION (IMAGE (supp pm) s))``, 1046 STRIP_TAC THEN MATCH_MP_TAC supp_unique_apart THEN SRW_TAC [][] THENL [ 1047 SRW_TAC [][support_def] THEN 1048 SRW_TAC [][pred_setTheory.EXTENSION] THEN 1049 Cases_on `x ��� supp pm x'` THENL [ 1050 `x' ��� s` by METIS_TAC [] THEN 1051 `y ��� supp pm (pmact pm [(x,y)] x')` by SRW_TAC [][perm_supp] THEN 1052 METIS_TAC [], 1053 ALL_TAC 1054 ] THEN Cases_on `y ��� supp pm x'` THENL [ 1055 `x' ��� s` by METIS_TAC [] THEN 1056 `x ��� supp pm (pmact pm [(x,y)] x')` by SRW_TAC [][perm_supp] THEN 1057 METIS_TAC [], 1058 ALL_TAC 1059 ] THEN SRW_TAC [][supp_fresh], 1060 1061 METIS_TAC [], 1062 1063 SRW_TAC [][pred_setTheory.EXTENSION] THEN 1064 `���x. b ��� supp pm x ==> ��(x ��� s)` by METIS_TAC [] THEN 1065 `��(b ��� supp pm x)` by METIS_TAC [] THEN 1066 `b ��� supp pm (pmact pm [(a,b)] x)` by SRW_TAC [][perm_supp] THEN 1067 METIS_TAC [] 1068 ]); 1069 1070val supp_FINITE_strings = store_thm( 1071 "supp_FINITE_strings", 1072 ``FINITE s ��� (supp (set_pmact string_pmact) s = s)``, 1073 SRW_TAC [][supp_setpm, pred_setTheory.EXTENSION] THEN EQ_TAC THEN 1074 STRIP_TAC THENL [ 1075 METIS_TAC [], 1076 Q.EXISTS_TAC `{x}` THEN SRW_TAC [][] THEN METIS_TAC [] 1077 ]); 1078val _ = export_rewrites ["supp_FINITE_strings"] 1079 1080val rwt = prove( 1081 ``(!x. ~P x \/ Q x) = (!x. P x ==> Q x)``, 1082 METIS_TAC []); 1083 1084val fmap_supp = store_thm( 1085 "fmap_supp", 1086 ``(���d. FINITE (supp dpm d)) ��� (���r. FINITE (supp rpm r)) ==> 1087 (supp (fm_pmact dpm rpm) fmap = 1088 supp (set_pmact dpm) (FDOM fmap) ��� 1089 supp (set_pmact rpm) (FRANGE fmap))``, 1090 STRIP_TAC THEN MATCH_MP_TAC supp_unique_apart THEN 1091 SRW_TAC [][FINITE_FRANGE, supp_setpm, rwt, 1092 GSYM RIGHT_FORALL_IMP_THM] 1093 THENL [ 1094 SRW_TAC [][support_def, fmap_EXT, rwt, GSYM RIGHT_FORALL_IMP_THM, 1095 fmpm_FDOM] 1096 THENL [ 1097 SRW_TAC [][pred_setTheory.EXTENSION, fmpm_FDOM] THEN 1098 Cases_on `x ��� supp dpm x'` THEN1 1099 (`y ��� supp dpm (pmact dpm [(x,y)] x')` by SRW_TAC [][perm_supp] THEN 1100 METIS_TAC []) THEN 1101 Cases_on `y ��� supp dpm x'` THEN1 1102 (`x ��� supp dpm (pmact dpm [(x,y)] x')` by SRW_TAC [][perm_supp] THEN 1103 METIS_TAC []) THEN 1104 METIS_TAC [supp_fresh], 1105 SRW_TAC [][fmpm_def, FAPPLY_f_o, lemma, FDOM_f_o, o_f_FAPPLY] THEN 1106 `��(x ��� supp dpm (pmact dpm [(x,y)] x')) ��� ��(y ��� supp dpm (pmact dpm [(x,y)] x'))` 1107 by METIS_TAC [] THEN 1108 NTAC 2 (POP_ASSUM MP_TAC) THEN 1109 SRW_TAC [][perm_supp] THEN 1110 SRW_TAC [][supp_fresh] THEN 1111 `x' ��� FDOM fmap` by METIS_TAC [supp_fresh] THEN 1112 `fmap ' x' ��� FRANGE fmap` 1113 by (SRW_TAC [][FRANGE_DEF] THEN METIS_TAC []) THEN 1114 METIS_TAC [supp_fresh] 1115 ], 1116 1117 SRW_TAC [][], 1118 SRW_TAC [][], 1119 1120 `��(b ��� supp dpm x)` by METIS_TAC [] THEN 1121 SRW_TAC [][fmap_EXT, fmpm_FDOM] THEN DISJ1_TAC THEN 1122 SRW_TAC [][pred_setTheory.EXTENSION, fmpm_FDOM] THEN 1123 `b ��� supp dpm (pmact dpm [(a,b)] x)` by SRW_TAC [][perm_supp] THEN 1124 METIS_TAC [], 1125 1126 `��(b ��� supp rpm x)` by METIS_TAC [] THEN 1127 `���y. y ��� FDOM fmap ��� (fmap ' y = x)` 1128 by (FULL_SIMP_TAC (srw_ss()) [FRANGE_DEF] THEN METIS_TAC []) THEN 1129 `��(b ��� supp dpm y)` by METIS_TAC [] THEN 1130 Cases_on `a ��� supp dpm y` THENL [ 1131 `b ��� supp dpm (pmact dpm [(a,b)] y)` by SRW_TAC [][perm_supp] THEN 1132 SRW_TAC [][fmap_EXT, fmpm_FDOM, pred_setTheory.EXTENSION] THEN 1133 METIS_TAC [], 1134 ALL_TAC 1135 ] THEN 1136 SRW_TAC [][fmap_EXT, fmpm_FDOM] THEN DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN 1137 SRW_TAC [][supp_fresh, fmpm_def, FAPPLY_f_o, o_f_FAPPLY, lemma, 1138 FDOM_f_o] THEN 1139 METIS_TAC [supp_apart] 1140 ]); 1141 1142val FAPPLY_eqv_lswapstr = store_thm( 1143 "FAPPLY_eqv_lswapstr", 1144 ``d ��� FDOM fm ��� (pmact rpm pi (fm ' d) = fmpm string_pmact rpm pi fm ' (lswapstr pi d))``, 1145 srw_tac [][fmpm_def] >> 1146 qmatch_abbrev_tac `z = (f o_f g) ' x` >> 1147 `FDOM g = { x | lswapstr pi����� x ��� FDOM fm }` 1148 by simp[FINITE_PRED_11, FDOM_f_o, Abbr`g`] >> 1149 simp[Abbr`g`, FAPPLY_f_o, FINITE_PRED_11, Abbr`x`]); 1150 1151val fmpm_FEMPTY = store_thm( 1152 "fmpm_FEMPTY", 1153 ``fmpm dpm rpm pi FEMPTY = FEMPTY``, 1154 SRW_TAC [][fmap_EXT, fmpm_applied, fmpm_FDOM, pred_setTheory.EXTENSION]); 1155val _ = export_rewrites ["fmpm_FEMPTY"] 1156 1157val fmpm_FUPDATE = store_thm( 1158 "fmpm_FUPDATE", 1159 ``fmpm dpm rpm pi (fm |+ (k,v)) = 1160 fmpm dpm rpm pi fm |+ (pmact dpm pi k, pmact rpm pi v)``, 1161 SRW_TAC [][fmap_EXT, fmpm_applied, fmpm_FDOM, pred_setTheory.EXTENSION] 1162 THENL [ 1163 SRW_TAC [][pmact_eql], 1164 SRW_TAC [][pmact_inverse], 1165 Cases_on `k = pmact dpm (REVERSE pi) x` THENL [ 1166 SRW_TAC [][pmact_inverse], 1167 SRW_TAC [][FAPPLY_FUPDATE_THM, fmpm_applied] THEN 1168 METIS_TAC [pmact_inverse] 1169 ] 1170 ]); 1171val _ = export_rewrites ["fmpm_FUPDATE"] 1172 1173val fmpm_DOMSUB = store_thm( 1174 "fmpm_DOMSUB", 1175 ``fmpm dpm rpm pi (fm \\ k) = fmpm dpm rpm pi fm \\ (pmact dpm pi k)``, 1176 SRW_TAC [][fmap_EXT,fmpm_FDOM,EXTENSION] THEN1 1177 METIS_TAC [pmact_eql] THEN 1178 SRW_TAC [][fmpm_applied,DOMSUB_FAPPLY_THM] THEN 1179 POP_ASSUM MP_TAC THEN SRW_TAC [][pmact_inverse] ) 1180val _ = export_rewrites ["fmpm_DOMSUB"]; 1181 1182val fcond_def = Define` 1183 fcond pm f = FINITE (supp (fn_pmact string_pmact pm) f) ��� 1184 (���a. a ��� supp (fn_pmact string_pmact pm) f /\ a ��� supp pm (f a)) 1185`; 1186 1187val fcond_equivariant = Store_thm( 1188 "fcond_equivariant", 1189 ``fcond pm (fnpm string_pmact pm pi f) = fcond pm f``, 1190 SIMP_TAC (srw_ss() ++ CONJ_ss) [fcond_def, EQ_IMP_THM, perm_supp, fnpm_def, 1191 pmact_IN, pmact_FINITE] THEN 1192 METIS_TAC [pmact_inverse]); 1193 1194 1195val fresh_def = Define`fresh apm f = let z = NEW (supp (fn_pmact string_pmact apm) f) 1196 in 1197 f z` 1198 1199val fresh_thm = store_thm( 1200 "fresh_thm", 1201 ``fcond apm f ==> 1202 ���a. a ��� supp (fn_pmact string_pmact apm) f ��� (f a = fresh apm f)``, 1203 SIMP_TAC (srw_ss()) [fcond_def, fresh_def] THEN STRIP_TAC THEN 1204 Q.X_GEN_TAC `b` THEN 1205 SRW_TAC [][fcond_def, fresh_def] THEN 1206 Q.UNABBREV_TAC `z` THEN 1207 NEW_ELIM_TAC THEN SRW_TAC [][] THEN 1208 Q_TAC SUFF_TAC `!c. ~(c IN supp (fn_pmact string_pmact apm) f) ==> (f c = f a)` 1209 THEN1 SRW_TAC [][] THEN 1210 REPEAT STRIP_TAC THEN 1211 Cases_on `c = a` THEN1 SRW_TAC [][] THEN 1212 `~(c IN supp string_pmact a)` by SRW_TAC [][] THEN 1213 `~(c IN supp apm (f a))` 1214 by (`supp apm (f a) SUBSET 1215 supp (fn_pmact string_pmact apm) f UNION supp string_pmact a` 1216 by SRW_TAC [][supp_fnapp] THEN 1217 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC []) THEN 1218 `pmact apm [(a,c)] (f a) = f a` by METIS_TAC [supp_supports, support_def] THEN 1219 POP_ASSUM (SUBST1_TAC o SYM) THEN 1220 `pmact apm [(a,c)] (f a) = fnpm string_pmact apm [(a,c)] f (lswapstr [(a,c)] a)` 1221 by SRW_TAC [][fnpm_def] THEN 1222 SRW_TAC [][supp_fresh]) 1223 1224val fresh_equivariant = store_thm( 1225 "fresh_equivariant", 1226 ``fcond pm f ==> 1227 (pmact pm pi (fresh pm f) = fresh pm (fnpm string_pmact pm pi f))``, 1228 STRIP_TAC THEN 1229 `fcond pm (fnpm string_pmact pm pi f)` by SRW_TAC [][fcond_equivariant] THEN 1230 `���b. b ��� supp (fn_pmact string_pmact pm) (fnpm string_pmact pm pi f)` 1231 by (Q.SPEC_THEN `supp (fn_pmact string_pmact pm) (fnpm string_pmact pm pi f)` 1232 MP_TAC NEW_def THEN METIS_TAC [fcond_def]) THEN 1233 `stringpm pi����� b ��� supp (fn_pmact string_pmact pm) f` 1234 by (POP_ASSUM MP_TAC THEN SRW_TAC [][perm_supp, pmact_IN]) THEN 1235 `fresh pm (fnpm string_pmact pm pi f) = fnpm string_pmact pm pi f b` 1236 by METIS_TAC [fresh_thm] THEN 1237 SRW_TAC [][fnpm_def, pmact_injective, GSYM fresh_thm]); 1238 1239val _ = overload_on ("sset_pmact",``set_pmact string_pmact``); 1240val _ = overload_on ("ssetpm", ``pmact sset_pmact``) 1241 1242(* 1243 given a finite set of atoms and some other set to avoid, we can 1244 exhibit a pi that maps the original set away from the avoid set, and 1245 doesn't itself contain any atoms apart from those present in the 1246 original set and its image. 1247*) 1248val gen_avoidance_lemma = store_thm( 1249 "gen_avoidance_lemma", 1250 ``FINITE atoms ��� FINITE s ��� 1251 �����. (���a. a ��� atoms ��� lswapstr �� a ��� s) ��� 1252 ���x y. MEM (x,y) �� ��� x ��� atoms ��� y ��� ssetpm �� atoms``, 1253 Q_TAC SUFF_TAC 1254 `FINITE s ��� 1255 ���limit. FINITE limit ��� 1256 ���atoms. FINITE atoms ��� 1257 atoms ��� limit ��� 1258 �����. (���a. a ��� atoms ��� lswapstr �� a ��� s ��� lswapstr �� a ��� limit) ��� 1259 ���x y. MEM (x,y) �� ��� x ��� atoms ��� y ��� ssetpm �� atoms` 1260 THEN1 METIS_TAC [SUBSET_REFL] THEN 1261 NTAC 3 STRIP_TAC THEN HO_MATCH_MP_TAC FINITE_INDUCT THEN SRW_TAC [][] THEN1 1262 (Q.EXISTS_TAC `[]` THEN SRW_TAC [][]) THEN 1263 FULL_SIMP_TAC (srw_ss () ++ DNF_ss) [] THEN 1264 `lswapstr �� e = e` 1265 by (MATCH_MP_TAC lswapstr_unchanged THEN 1266 DISCH_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [IN_patoms_MEM]) THEN1 1267 METIS_TAC [] THEN 1268 `lswapstr ������� e ��� atoms` by METIS_TAC [] THEN 1269 `lswapstr �� (lswapstr ������� e) ��� limit` by METIS_TAC [] THEN 1270 FULL_SIMP_TAC (srw_ss()) []) THEN 1271 1272 Q_TAC (NEW_TAC "e'") `s ��� patoms �� ��� limit ��� {e}` THEN 1273 `���a. a ��� atoms ��� lswapstr �� a ��� e` by METIS_TAC [] THEN 1274 `���a. a ��� atoms ��� lswapstr �� a ��� e'` 1275 by (REPEAT STRIP_TAC THEN 1276 `lswapstr ������� e' = a` by SRW_TAC [][pmact_eql] THEN 1277 METIS_TAC [lswapstr_unchanged, listsupp_REVERSE, SUBSET_DEF]) THEN 1278 Q.EXISTS_TAC `(e,e')::��` THEN SRW_TAC [][] THENL [ 1279 METIS_TAC [], 1280 1281 SRW_TAC [][pmact_decompose] THEN 1282 FIRST_ASSUM (SUBST1_TAC o SYM) THEN SRW_TAC [][], 1283 1284 FULL_SIMP_TAC (srw_ss()) [pmact_decompose] THEN 1285 `y ��� patoms ��` by METIS_TAC [IN_patoms_MEM] THEN 1286 `y ��� e'` by METIS_TAC [] THEN 1287 Cases_on `y = e` THENL [ 1288 SRW_TAC [][swapstr_def] THEN 1289 `lswapstr ������� e ��� atoms` by METIS_TAC [] THEN 1290 POP_ASSUM MP_TAC THEN 1291 FIRST_X_ASSUM (SUBST1_TAC o SYM) THEN 1292 SRW_TAC [][], 1293 SRW_TAC [][] THEN METIS_TAC [] 1294 ] 1295 ]); 1296 1297val _ = export_theory(); 1298