1(* this is an -*- sml -*- file *) 2open HolKernel Parse boolLib 3 4open bossLib binderLib 5open basic_swapTheory nomsetTheory 6open pred_setTheory 7open BasicProvers 8open quotientLib 9open boolSimps 10 11fun Store_Thm(s, t, tac) = (store_thm(s,t,tac) before export_rewrites [s]) 12fun Save_Thm(s, th) = (save_thm(s, th) before export_rewrites [s]) 13 14val _ = new_theory "generic_terms" 15 16val _ = computeLib.auto_import_definitions := false 17 18val _ = Datatype ` 19 pregterm = var string 'v 20 | lam string 'b (pregterm list) (pregterm list) 21`; 22 23val fv_def = Define ` 24 (fv (var s vv) = {s}) ��� 25 (fv (lam v bv bndts unbndts) = (fvl bndts DELETE v) ��� fvl unbndts) ��� 26 (fvl [] = ���) ��� 27 (fvl (h::ts) = fv h ��� fvl ts)` 28val _ = augment_srw_ss [rewrites [fv_def]] 29 30val oldind = TypeBase.induction_of ``:(��,��)pregterm`` 31 32val pind = prove( 33 ``���P. 34 (���s vv. P (var s vv)) ��� 35 (���v bv bndts unbndts. 36 EVERY P bndts ��� EVERY P unbndts ��� P (lam v bv bndts unbndts)) 37 ��� 38 ���t. P t``, 39 gen_tac >> strip_tac >> 40 Q_TAC suff_tac `(���t. P t) ��� (���ts. EVERY P ts)` >- metis_tac [] >> 41 ho_match_mp_tac oldind >> srw_tac [][]); 42 43val finite_fv = store_thm( 44 "finite_fv", 45 ``���t. FINITE (fv t)``, 46 Q_TAC suff_tac `(���t:(��,��)pregterm. FINITE (fv t)) ��� 47 (���l:(��,��)pregterm list. FINITE (fvl l))` >- srw_tac [][] >> 48 ho_match_mp_tac oldind >> srw_tac [][]); 49val _ = augment_srw_ss [rewrites [finite_fv]] 50 51val raw_ptpm_def = Define` 52 (raw_ptpm p (var s vv) = var (lswapstr p s) vv) ��� 53 (raw_ptpm p (lam v bv bndts unbndts) = lam (lswapstr p v) 54 bv 55 (raw_ptpml p bndts) 56 (raw_ptpml p unbndts)) ��� 57 (raw_ptpml p [] = []) ��� 58 (raw_ptpml p (h::t) = raw_ptpm p h :: raw_ptpml p t) 59`; 60 61val _ = overload_on("pt_pmact",``mk_pmact raw_ptpm``); 62val _ = overload_on("ptpm",``pmact pt_pmact``); 63val _ = overload_on("ptl_pmact",``mk_pmact raw_ptpml``); 64val _ = overload_on("ptpml",``pmact ptl_pmact``); 65 66val raw_ptpm_nil = prove( 67 ``(���t:(��,��)pregterm. raw_ptpm [] t = t) ��� 68 (���l:(��,��)pregterm list. raw_ptpml [] l = l)``, 69 ho_match_mp_tac oldind >> srw_tac [][raw_ptpm_def]) 70 71val raw_ptpm_compose = prove( 72 ``(���t:(��,��)pregterm. raw_ptpm p1 (raw_ptpm p2 t) = raw_ptpm (p1 ++ p2) t) ��� 73 (���l:(��,��)pregterm list. 74 raw_ptpml p1 (raw_ptpml p2 l) = raw_ptpml (p1 ++ p2) l)``, 75 ho_match_mp_tac oldind >> srw_tac [][raw_ptpm_def, pmact_decompose]); 76 77val raw_ptpm_permeq = prove( 78 ``(���x. lswapstr p1 x = lswapstr p2 x) ��� 79 (���t:(��,��)pregterm. raw_ptpm p1 t = raw_ptpm p2 t) ��� 80 (���l:(��,��)pregterm list. raw_ptpml p1 l = raw_ptpml p2 l)``, 81 strip_tac >> ho_match_mp_tac oldind >> srw_tac [][raw_ptpm_def]); 82 83val ptpm_raw = prove( 84 ``(ptpm = raw_ptpm) ��� (ptpml = raw_ptpml)``, 85 conj_tac >> ( 86 srw_tac [][GSYM pmact_bijections] >> 87 srw_tac [][is_pmact_def] >|[ 88 srw_tac [][raw_ptpm_nil], 89 srw_tac [][raw_ptpm_compose], 90 fsrw_tac [][raw_ptpm_permeq, permeq_thm, FUN_EQ_THM] 91])); 92val ptpm_raw = INST_TYPE[gamma|->alpha,delta|->beta] ptpm_raw; 93 94val ptpml_listpm = store_thm( 95 "ptpml_listpm", 96 ``���l. ptpml p l = listpm pt_pmact p l``, 97 Induct >> fsrw_tac[][ptpm_raw] >> 98 srw_tac [][raw_ptpm_def]); 99 100val ptpm_thm = Save_Thm( 101 "ptpm_thm", 102 raw_ptpm_def |> CONJUNCTS |> (fn l => List.take(l, 2)) 103 |> map (SUBS (map GSYM (CONJUNCTS ptpm_raw))) |> LIST_CONJ 104 |> REWRITE_RULE [ptpml_listpm] ); 105 106val ptpm_fv = store_thm( 107 "ptpm_fv", 108 ``(���t:(��,��)pregterm. fv (ptpm p t) = ssetpm p (fv t)) ��� 109 (���l:(��,��)pregterm list. fvl (ptpml p l) = ssetpm p (fvl l))``, 110 ho_match_mp_tac oldind >> srw_tac[][stringpm_raw, ptpml_listpm, pmact_INSERT, pmact_DELETE, pmact_UNION]); 111val _ = augment_srw_ss [rewrites [ptpm_fv]] 112 113val allatoms_def = Define` 114 (allatoms (var s vv) = {s}) ��� 115 (allatoms (lam v bv bndts unbndts) = 116 v INSERT allatomsl bndts ��� allatomsl unbndts) ��� 117 (allatomsl [] = ���) ��� 118 (allatomsl (t::ts) = allatoms t ��� allatomsl ts) 119`; 120 121val allatoms_finite = Store_Thm( 122 "allatoms_finite", 123 ``(���t:(��,��)pregterm. FINITE (allatoms t)) ��� 124 (���l:(��,��)pregterm list. FINITE (allatomsl l))``, 125 ho_match_mp_tac oldind >> srw_tac [][allatoms_def]); 126 127val allatoms_supports = store_thm( 128 "allatoms_supports", 129 ``(���t:(��,��)pregterm. support pt_pmact t (allatoms t)) ��� 130 (���l:(��,��)pregterm list. support (list_pmact pt_pmact) l (allatomsl l))``, 131 simp_tac (srw_ss())[support_def] >> 132 ho_match_mp_tac oldind >> srw_tac [][allatoms_def]); 133 134val allatoms_fresh = store_thm( 135 "allatoms_fresh", 136 ``x ��� allatoms t ��� y ��� allatoms t ==> (ptpm [(x,y)] t = t)``, 137 METIS_TAC [allatoms_supports, support_def]); 138 139val allatoms_apart = store_thm( 140 "allatoms_apart", 141 ``(���t:(��,��)pregterm a b. 142 a ��� allatoms t /\ b ��� allatoms t ��� ptpm [(a,b)] t ��� t) ��� 143 (���l:(��,��)pregterm list a b. 144 a ��� allatomsl l ��� b ��� allatomsl l ��� listpm pt_pmact [(a,b)] l ��� l)``, 145 ho_match_mp_tac oldind >> srw_tac [][allatoms_def] >> 146 srw_tac [][swapstr_def]); 147 148val allatoms_supp = store_thm( 149 "allatoms_supp", 150 ``supp pt_pmact t = allatoms t``, 151 MATCH_MP_TAC supp_unique THEN 152 SRW_TAC [][allatoms_supports, SUBSET_DEF] THEN 153 FULL_SIMP_TAC (srw_ss()) [support_def] THEN 154 SPOSE_NOT_THEN ASSUME_TAC THEN 155 `?y. ~(y IN allatoms t) /\ ~(y IN s')` 156 by (Q.SPEC_THEN `allatoms t UNION s'` MP_TAC NEW_def THEN 157 SRW_TAC [][] THEN METIS_TAC []) THEN 158 METIS_TAC [allatoms_apart]); 159 160val allatoms_perm = store_thm( 161 "allatoms_perm", 162 ``(���t:(��,��)pregterm. allatoms (ptpm p t) = ssetpm p (allatoms t)) ��� 163 (���l:(��,��)pregterm list. 164 allatomsl (listpm pt_pmact p l) = ssetpm p (allatomsl l))``, 165 ho_match_mp_tac oldind >> 166 srw_tac [][allatoms_def, pmact_INSERT, pmact_UNION]); 167 168val (aeq_rules, aeq_ind, aeq_cases) = Hol_reln` 169 (!s vv. aeq (var s vv) (var s vv)) /\ 170 (!u v bv z bndts1 bndts2 us1 us2. 171 aeql us1 us2 ��� 172 aeql (ptpml [(u,z)] bndts1) (ptpml [(v,z)] bndts2) ��� 173 z ��� allatomsl bndts1 ��� z ��� allatomsl bndts2 ��� z ��� u ��� z ��� v ��� 174 aeq (lam u bv bndts1 us1) (lam v bv bndts2 us2)) ��� 175 aeql [] [] ��� 176 (���h1 h2 t1 t2. aeq h1 h2 ��� aeql t1 t2 ��� aeql (h1::t1) (h2::t2)) 177`; 178 179val aeq_lam = List.nth(CONJUNCTS aeq_rules, 1) 180 181val aeq_distinct = store_thm( 182 "aeq_distinct", 183 ``~aeq (var s vv) (lam v bv ts us)``, 184 ONCE_REWRITE_TAC [aeq_cases] THEN SRW_TAC [][]); 185 186val aeq_ptpm_lemma = store_thm( 187 "aeq_ptpm_lemma", 188 ``(!t:(��,��)pregterm u. aeq t u ==> !p. aeq (ptpm p t) (ptpm p u)) ��� 189 (���ts:(��,��)pregterm list us. 190 aeql ts us ��� �����. aeql (listpm pt_pmact �� ts) (listpm pt_pmact �� us)) ``, 191 ho_match_mp_tac aeq_ind >> srw_tac [][aeq_rules, ptpml_listpm] >> 192 match_mp_tac aeq_lam >> 193 Q.EXISTS_TAC `lswapstr p z` THEN 194 srw_tac [][allatoms_perm, pmact_IN] >> 195 srw_tac [][ptpml_listpm, pmact_sing_to_back]); 196 197val aeq_ptpm_eqn = store_thm( 198 "aeq_ptpm_eqn", 199 ``aeq (ptpm p t) u = aeq t (ptpm (REVERSE p) u)``, 200 METIS_TAC [aeq_ptpm_lemma, pmact_inverse]); 201 202val aeql_ptpm_eqn = store_thm( 203 "aeql_ptpm_eqn", 204 ``aeql (ptpml p l1) l2 = aeql l1 (ptpml p����� l2)``, 205 METIS_TAC [aeq_ptpm_lemma, ptpml_listpm, pmact_inverse]); 206 207val IN_fvl = prove( 208 ``x ��� fvl tl ��� ���e. MEM e tl ��� x ��� fv e``, 209 Induct_on `tl` >> srw_tac [DNF_ss][AC DISJ_ASSOC DISJ_COMM]); 210 211val IN_allatomsl = prove( 212 ``x ��� allatomsl tl ��� ���t. MEM t tl ��� x ��� allatoms t``, 213 Induct_on `tl` >> srw_tac [DNF_ss][allatoms_def]); 214 215val fv_SUBSET_allatoms = store_thm( 216 "fv_SUBSET_allatoms", 217 ``(���t:(��,��)pregterm. fv t SUBSET allatoms t) ��� 218 (���l:(��,��)pregterm list. fvl l ��� allatomsl l)``, 219 SIMP_TAC (srw_ss()) [SUBSET_DEF] >> ho_match_mp_tac oldind>> 220 srw_tac [][allatoms_def] >> metis_tac []); 221 222val aeq_fv = store_thm( 223 "aeq_fv", 224 ``(!t:(��,��)pregterm u. aeq t u ==> (fv t = fv u)) ��� 225 (���ts:(��,��)pregterm list us. aeql ts us ��� (fvl ts = fvl us))``, 226 ho_match_mp_tac aeq_ind >> 227 srw_tac [][EXTENSION, ptpm_fv, pmact_IN, ptpml_listpm] THEN 228 Cases_on `x ��� fvl us` >> srw_tac [][] >> 229 Cases_on `x = u` >> srw_tac [][] THENL [ 230 Cases_on `u = v` THEN SRW_TAC [][] THEN 231 FIRST_X_ASSUM (Q.SPEC_THEN `swapstr v z u` (MP_TAC o SYM)) THEN 232 SRW_TAC [][] THEN SRW_TAC [][swapstr_def] THEN 233 METIS_TAC [fv_SUBSET_allatoms, SUBSET_DEF], 234 Cases_on `x = v` THEN SRW_TAC [][] THENL [ 235 FIRST_X_ASSUM (Q.SPEC_THEN `swapstr u z v` MP_TAC) THEN 236 SRW_TAC [][] THEN SRW_TAC [][swapstr_def] THEN 237 METIS_TAC [fv_SUBSET_allatoms, SUBSET_DEF], 238 Cases_on `z = x` THEN SRW_TAC [][] THENL [ 239 METIS_TAC [fv_SUBSET_allatoms, SUBSET_DEF], 240 FIRST_X_ASSUM (Q.SPEC_THEN `x` MP_TAC) THEN 241 SRW_TAC [][swapstr_def] 242 ] 243 ] 244 ]); 245 246val aeq_refl = Store_Thm( 247 "aeq_refl", 248 ``(���t:(��,��)pregterm. aeq t t) ��� (���l:(��,��)pregterm list. aeql l l)``, 249 ho_match_mp_tac oldind >> asm_simp_tac (srw_ss())[aeq_rules] >> 250 REPEAT gen_tac >> strip_tac >> 251 MAP_EVERY Q.X_GEN_TAC [`b`, `s`] >> 252 MATCH_MP_TAC aeq_lam >> 253 SRW_TAC [][aeql_ptpm_eqn, ptpml_listpm] THEN 254 Q.SPEC_THEN `s INSERT allatomsl l` MP_TAC NEW_def THEN SRW_TAC [][] THEN 255 METIS_TAC [ pmact_sing_inv]); 256 257val aeq_sym = store_thm( 258 "aeq_sym", 259 ``(���t:(��,��)pregterm u. aeq t u ==> aeq u t) ��� 260 (���l1:(��,��)pregterm list l2. aeql l1 l2 ==> aeql l2 l1)``, 261 ho_match_mp_tac aeq_ind >> srw_tac [][aeq_rules] >> 262 metis_tac [aeq_lam]); 263 264val aeq_var_inversion = store_thm( 265 "aeq_var_inversion", 266 ``aeq (var vv s) t = (t = var vv s)``, 267 srw_tac [][Once aeq_cases]); 268 269val aeq_lam_inversion = store_thm( 270 "aeq_lam_inversion", 271 ``aeq (lam v bv bndts unbndts) N = 272 ���z v' bndts' unbndts'. 273 (N = lam v' bv bndts' unbndts') ��� z ��� v' ��� z ��� v ��� 274 z ��� allatomsl bndts ��� z ��� allatomsl bndts' ��� 275 aeql (ptpml [(v,z)] bndts) (ptpml [(v',z)] bndts') ��� 276 aeql unbndts unbndts'``, 277 srw_tac [][Once aeq_cases, SimpLHS] >> metis_tac []); 278 279Theorem aeq_ptm_11: 280 (aeq (var s1 vv1) (var s2 vv2) ��� (s1 = s2) ��� (vv1 = vv2)) /\ 281 (aeq (lam v bv1 bndts1 unbndts1) (lam v bv2 bndts2 unbndts2) ��� 282 (bv1 = bv2) ��� aeql bndts1 bndts2 ��� aeql unbndts1 unbndts2) 283Proof 284 SRW_TAC [][aeq_lam_inversion, aeq_ptpm_eqn, aeq_var_inversion, EQ_IMP_THM] 285 THENL [ 286 full_simp_tac (srw_ss() ++ ETA_ss) 287 [aeql_ptpm_eqn, pmact_nil], 288 srw_tac [][], 289 Q_TAC (NEW_TAC "z") `v INSERT allatomsl bndts1 ��� allatomsl bndts2` THEN 290 Q.EXISTS_TAC `z` >> 291 srw_tac [ETA_ss][aeql_ptpm_eqn] 292 ] 293QED 294 295val ptpml_fresh = 296 allatoms_supports |> CONJUNCT2 |> 297 SIMP_RULE (srw_ss()) [support_def, GSYM ptpml_listpm] 298 299val ptpml_sing_to_back' = prove( 300 ``ptpml p (ptpml [(u,v)] tl) = 301 ptpml [(lswapstr p u, lswapstr p v)] (ptpml p tl)``, 302 simp_tac (srw_ss()) [pmact_sing_to_back]); 303 304(* proof follows that on p169 of Andy Pitts, Information and Computation 186 305 article: Nominal logic, a first order theory of names and binding *) 306val aeq_trans = store_thm( 307 "aeq_trans", 308 ``(���t:(��,��)pregterm u. aeq t u ��� ���v. aeq u v ==> aeq t v) ��� 309 (���l1:(��,��)pregterm list l2. aeql l1 l2 ��� ���l3. aeql l2 l3 ��� aeql l1 l3)``, 310 ho_match_mp_tac aeq_ind >> REPEAT conj_tac >|[ 311 srw_tac [][], 312 Q_TAC SUFF_TAC 313 `���u v bv z bt1 bt2 ut1 (ut2:(��,��)pregterm list). 314 (���l3. aeql (ptpml [(v,z)] bt2) l3 ��� aeql (ptpml [(u,z)] bt1) l3) ��� 315 (���ut3. aeql ut2 ut3 ��� aeql ut1 ut3) ��� 316 z ��� allatomsl bt1 ��� z ��� allatomsl bt2 ��� z ��� u ��� z ��� v ��� 317 ���t3. aeq (lam v bv bt2 ut2) t3 ��� aeq (lam u bv bt1 ut1) t3` 318 >- metis_tac [] >> 319 rpt gen_tac >> strip_tac >> gen_tac >> 320 simp_tac (srw_ss()) [SimpL ``$==>``, aeq_lam_inversion] >> 321 DISCH_THEN 322 (Q.X_CHOOSE_THEN `z2` 323 (Q.X_CHOOSE_THEN `w` 324 (Q.X_CHOOSE_THEN `bt3` 325 (Q.X_CHOOSE_THEN `ut3` STRIP_ASSUME_TAC)))) >> 326 Q_TAC (NEW_TAC "d") 327 `{z;z2;u;v;w} ��� allatomsl bt1 ��� allatomsl bt2 ��� allatomsl bt3` >> 328 `���bt3. 329 aeql (ptpml [(z,d)] (ptpml [(v,z)] bt2)) (ptpml [(z,d)] bt3) ==> 330 aeql (ptpml [(z,d)] (ptpml [(u,z)] bt1)) (ptpml [(z,d)] bt3)` 331 by FULL_SIMP_TAC (srw_ss()) [aeql_ptpm_eqn] THEN 332 POP_ASSUM 333 (Q.SPEC_THEN `ptpml [(z,d)] bt3` 334 (ASSUME_TAC o Q.GEN `bt3` o 335 SIMP_RULE (srw_ss() ++ ETA_ss) 336 [pmact_sing_inv, pmact_nil])) THEN 337 POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [ptpml_sing_to_back']) THEN 338 SRW_TAC [][swapstr_def, ptpml_fresh] THEN 339 `aeql (ptpml [(z2,d)] (ptpml [(v,z2)] bt2)) 340 (ptpml [(z2,d)] (ptpml [(w,z2)] bt3))` 341 by (srw_tac [ETA_ss] 342 [Once aeql_ptpm_eqn, pmact_nil]) >> 343 POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [ptpml_sing_to_back']) THEN 344 SRW_TAC [][swapstr_def, ptpml_fresh] THEN 345 `aeql (ptpml [(u,d)] bt1) (ptpml [(w,d)] bt3)` by METIS_TAC [] THEN 346 METIS_TAC [aeq_lam], 347 348 srw_tac [][], 349 rpt gen_tac >> strip_tac >> gen_tac >> 350 srw_tac [][Once aeq_cases, SimpL ``$==>``] >> 351 metis_tac [aeq_rules] 352 ]); 353 354open relationTheory 355val aeq_equiv = store_thm( 356 "aeq_equiv", 357 ``!t1 t2. aeq t1 t2 = (aeq t1 = aeq t2)``, 358 srw_tac [][FUN_EQ_THM] >> METIS_TAC [aeq_trans, aeq_sym, aeq_refl]); 359 360val alt_aeq_lam = store_thm( 361 "alt_aeq_lam", 362 ``(���z. z ��� allatomsl t1 ��� z ��� allatomsl t2 ��� z ��� u ��� z ��� v ��� 363 aeql (ptpml [(u,z)] t1) (ptpml [(v,z)] t2)) ��� 364 aeql u1 u2 ��� 365 aeq (lam u bv t1 u1) (lam v bv t2 u2)``, 366 strip_tac >> MATCH_MP_TAC aeq_lam >> 367 Q_TAC (NEW_TAC "z") 368 `allatomsl t1 ��� allatomsl t2 ��� {u;v}` >> 369 METIS_TAC []); 370 371val fresh_swap = store_thm( 372 "fresh_swap", 373 ``(���t:(��,��)pregterm x y. x ��� fv t ��� y ��� fv t ��� aeq t (ptpm [(x, y)] t)) ��� 374 (���l:(��,��)pregterm list x y. 375 x ��� fvl l ��� y ��� fvl l ��� aeql l (ptpml [(x,y)] l))``, 376 ho_match_mp_tac oldind >> 377 asm_simp_tac (srw_ss()) [aeq_rules,ptpml_listpm] >> 378 map_every qx_gen_tac [`bt`, `ut`] >> strip_tac >> 379 map_every qx_gen_tac [`b`, `s`,`x`,`y`] >> 380 strip_tac >> srw_tac [][] >> 381 match_mp_tac alt_aeq_lam >> rpt strip_tac >> 382 fsrw_tac [][pmact_id, pmact_nil, GSYM ptpml_listpm] >> 383 `z ��� fvl bt` by METIS_TAC [SUBSET_DEF, fv_SUBSET_allatoms] >| [ 384 Cases_on `s = x` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 385 ONCE_REWRITE_TAC [GSYM pmact_sing_to_back] THEN 386 SRW_TAC [][swapstr_def, aeql_ptpm_eqn, pmact_sing_inv, 387 pmact_id, pmact_nil], 388 ALL_TAC 389 ] THEN Cases_on `s = y` THENL [ 390 FULL_SIMP_TAC (srw_ss()) [] THEN 391 ONCE_REWRITE_TAC [GSYM pmact_sing_to_back] THEN 392 SRW_TAC [][swapstr_def, pmact_flip_args, aeql_ptpm_eqn, 393 pmact_sing_inv], 394 SRW_TAC [][swapstr_def, aeql_ptpm_eqn, pmact_sing_inv] 395 ], 396 Cases_on `s = x` THEN1 SRW_TAC [][pmact_id, pmact_nil] THEN 397 ONCE_REWRITE_TAC [GSYM pmact_sing_to_back] THEN 398 SRW_TAC [][swapstr_def, pmact_flip_args, aeql_ptpm_eqn, pmact_sing_inv], 399 Cases_on `s = y` THEN1 SRW_TAC [][pmact_id, pmact_nil] THEN 400 ONCE_REWRITE_TAC [GSYM pmact_sing_to_back] THEN 401 SRW_TAC [][swapstr_def, aeql_ptpm_eqn, pmact_sing_inv] 402 ]); 403 404Theorem lam_aeq_thm: 405 aeq (lam v1 bv1 t1 u1) (lam v2 bv2 t2 u2) ��� 406 (v1 = v2) ��� (bv1 = bv2) ��� aeql t1 t2 ��� aeql u1 u2 ��� 407 v1 ��� v2 ��� (bv1 = bv2) ��� v1 ��� fvl t2 ��� aeql t1 (ptpml [(v1,v2)] t2) ��� 408 aeql u1 u2 409Proof 410 SIMP_TAC (srw_ss()) [EQ_IMP_THM, DISJ_IMP_THM] THEN REPEAT CONJ_TAC THENL [ 411 srw_tac [][aeq_lam_inversion] >> 412 `z ��� fvl t1 ��� z ��� fvl t2` 413 by METIS_TAC [SUBSET_DEF, fv_SUBSET_allatoms] >> 414 Cases_on `v1 = v2` >- fsrw_tac [][aeql_ptpm_eqn, pmact_sing_inv] THEN 415 `v1 ��� fvl t2` 416 by (strip_tac >> 417 `v1 ��� fvl (ptpml [(v2,z)] t2)` 418 by SRW_TAC [][ptpm_fv, pmact_IN] THEN 419 `v1 ��� fvl (ptpml [(v1,z)] t1)` by metis_tac [aeq_fv] THEN 420 fsrw_tac [][ptpm_fv, pmact_IN, ptpml_listpm]) >> 421 fsrw_tac [][aeql_ptpm_eqn] >> 422 Q.PAT_X_ASSUM `aeql X (ptpml PPI Y)` MP_TAC THEN 423 SRW_TAC [][swapstr_def, Once ptpml_sing_to_back'] THEN 424 MATCH_MP_TAC (MP_CANON (CONJUNCT2 aeq_trans)) THEN 425 Q.EXISTS_TAC `ptpml [(v1,v2)] (ptpml [(v1,z)] t2)` THEN 426 FULL_SIMP_TAC (srw_ss()) [pmact_flip_args, aeql_ptpm_eqn, fresh_swap, 427 pmact_sing_inv], 428 429 srw_tac [][] >> match_mp_tac alt_aeq_lam >> 430 srw_tac [][aeql_ptpm_eqn, pmact_sing_inv], 431 432 srw_tac [][] >> match_mp_tac alt_aeq_lam >> 433 srw_tac [][aeql_ptpm_eqn] >> 434 `z ��� fvl t2` by metis_tac [SUBSET_DEF, fv_SUBSET_allatoms] >> 435 SRW_TAC [][swapstr_def, pmact_flip_args, Once ptpml_sing_to_back'] >> 436 match_mp_tac (MP_CANON (CONJUNCT2 aeq_trans)) >> 437 qexists_tac `ptpml [(v1,v2)] t2` >> 438 srw_tac [][aeql_ptpm_eqn, fresh_swap, pmact_sing_inv, pmact_flip_args] 439 ] 440QED 441 442val aeql_LIST_REL = prove( 443 ``aeql l1 l2 ��� LIST_REL aeq l1 l2``, 444 map_every Q.ID_SPEC_TAC [`l2`, `l1`] >> Induct >> 445 srw_tac [][Once aeq_cases] >> Cases_on `l2` >> 446 srw_tac [][]); 447 448val lam_respects_aeq = store_thm( 449 "lam_respects_aeq", 450 ``!v bv t1 t2 u1 u2. 451 aeql t1 t2 ��� aeql u1 u2 ==> aeq (lam v bv t1 u1) (lam v bv t2 u2)``, 452 srw_tac [][] >> match_mp_tac aeq_lam >> 453 srw_tac [][aeql_ptpm_eqn, pmact_sing_inv] >> 454 Q_TAC (NEW_TAC "z") `v INSERT allatomsl t1 ��� allatomsl t2` >> metis_tac []); 455 456val rmaeql = REWRITE_RULE [aeql_LIST_REL] 457 458val var_respects_aeq = store_thm( 459 "var_respects_aeq", 460 ``!s1 s2 vv1 vv2. (s1 = s2) ��� (vv1 = vv2) ==> aeq (var s1 vv1) (var s2 vv2)``, 461 SRW_TAC [][]); 462 463(* ---------------------------------------------------------------------- 464 perform quotient! 465 ---------------------------------------------------------------------- *) 466 467fun mk_def(s,t) = 468 {def_name = s ^ "_def", fixity = NONE, fname = s, func = t}; 469 470val ptpm_fv' = 471 ptpm_fv |> CONJUNCT1 |> REWRITE_RULE [EXTENSION] 472 |> CONV_RULE 473 (STRIP_QUANT_CONV (RAND_CONV (SIMP_CONV (srw_ss()) [pmact_IN]))) 474 |> SIMP_RULE std_ss [ptpm_raw] 475 476val fvl_MAP = prove( 477 ``fvl l = BIGUNION (set (MAP fv l))``, 478 Induct_on `l` >> srw_tac [][]); 479val rmfvl = REWRITE_RULE [fvl_MAP] 480 481val ptpml_MAP = prove( 482 ``ptpml p l = MAP (raw_ptpm p) l``, 483 Induct_on `l` >> fsrw_tac [][ptpm_raw,raw_ptpm_def]); 484val rmptpml = REWRITE_RULE [GSYM ptpml_listpm,ptpml_MAP,ptpm_raw] 485 486fun front n l = List.take (l, n) 487fun drop n l = List.drop(l,n) 488 489val fvl_eqrespects = prove( 490 ``���ts1 ts2:(��,��) pregterm list. (ts1 = ts2) ==> (fvl ts1 = fvl ts2)``, 491 srw_tac [][]); 492 493val pregterm_size_def = definition "pregterm_size_def"; 494 495val psize_def = tDefine "psize"` 496 (psize (var s vv) = 1) ��� 497 (psize (lam s bv ts us) = SUM (MAP psize ts) + SUM (MAP psize us) + 1)` 498(WF_REL_TAC `measure (pregterm_size (K 0) (K 0))` >> 499 conj_tac >> (ntac 3 gen_tac) >> Induct >> 500 srw_tac [ARITH_ss][pregterm_size_def] >> 501 fsrw_tac [][] >> res_tac >> DECIDE_TAC ) 502 503val psize_thm = SIMP_RULE (srw_ss()++ETA_ss) [] psize_def 504 505val psize_ptpm0 = prove( 506``(���p:(��,��)pregterm pi. psize (ptpm pi p) = psize p) /\ 507 (���pl:(��,��)pregterm list pi. MAP psize (ptpml pi pl) = MAP psize pl)``, 508ho_match_mp_tac oldind >> 509srw_tac [][psize_thm, ptpml_listpm]); 510 511val psize_raw_ptpm = psize_ptpm0 |> CONJUNCT1 |> REWRITE_RULE [ptpm_raw] 512 513val psize_respects = prove( 514 ``���t1 t2. aeq t1 t2 ��� (psize t1 = psize t2)``, 515qsuff_tac `(���(t1:('a,'b) pregterm) t2. aeq t1 t2 ��� (psize t1 = psize t2)) ��� 516 (���(l1:('a,'b) pregterm list) l2. aeql l1 l2 ��� (SUM (MAP psize l1) = SUM (MAP psize l2)))` 517 >- metis_tac [] >> 518ho_match_mp_tac aeq_ind >> 519srw_tac [][psize_thm] >> 520fsrw_tac [][psize_ptpm0]); 521 522val [GFV_thm0, gfvl_thm, GFV_raw_gtpm, simple_induction0, 523 raw_gtpm_thm, is_pmact_raw_gtpm, 524 gterm_distinct, gterm_11, 525 GLAM_eq_thm0, FRESH_swap0, 526 FINITE_GFV, gtmsize_thm, gtmsize_raw_gtpm] = 527 quotient.define_quotient_types_full 528 { 529 types = [{name = "gterm", equiv = aeq_equiv}], 530 defs = map mk_def 531 [("GLAM", ``lam:string -> �� -> (��,��)pregterm list -> 532 (��,��)pregterm list -> (��,��)pregterm``), 533 ("GVAR", ``var:string -> �� -> (��,��)pregterm``), 534 ("GFV", ``fv : (��,��)pregterm -> string set``), 535 ("gfvl", ``fvl : (��,��)pregterm list -> string set``), 536 ("raw_gtpm", ``raw_ptpm : pm -> (��,��)pregterm -> (��,��)pregterm``), 537 ("gtmsize", ``psize:(��,��)pregterm ->num``)], 538 tyop_equivs = [], 539 tyop_quotients = [], 540 tyop_simps = [], 541 respects = [rmaeql lam_respects_aeq, 542 var_respects_aeq, CONJUNCT1 aeq_fv, 543 rmaeql (CONJUNCT2 aeq_fv), 544 aeq_ptpm_lemma 545 |> CONJUNCT1 546 |> SIMP_RULE bool_ss [GSYM RIGHT_FORALL_IMP_THM, ptpm_raw], 547 (*aeq_ptpm_lemma 548 |> CONJUNCT2 549 |> SIMP_RULE bool_ss [GSYM RIGHT_FORALL_IMP_THM, GSYM ptpml_listpm] 550 |> rmptpml, *) 551 psize_respects 552 ], 553 poly_preserves = [], 554 poly_respects = [], 555 old_thms = [fv_def |> CONJUNCTS |> front 2 |> LIST_CONJ, 556 fv_def |> CONJUNCTS |> drop 2 |> LIST_CONJ, 557 ptpm_fv', pind, 558 ptpm_thm |> CONJUNCTS |> front 2 |> LIST_CONJ |> rmptpml, 559 is_pmact_pmact |> Q.ISPEC `pt_pmact` |> REWRITE_RULE [ptpm_raw,is_pmact_def], 560 aeq_distinct, rmaeql aeq_ptm_11, 561 rmptpml (rmaeql lam_aeq_thm), 562 CONJUNCT1 fresh_swap |> REWRITE_RULE [ptpm_raw], 563 finite_fv, 564 psize_thm, psize_raw_ptpm]} 565 566val simple_induction = save_thm( 567 "simple_induction", 568 REWRITE_RULE [listTheory.EVERY_MEM] simple_induction0) 569 570val _ = overload_on("gt_pmact",``mk_pmact raw_gtpm``); 571val _ = overload_on("gtpm",``pmact gt_pmact``); 572 573val gtpm_raw = store_thm( 574 "gtpm_raw", 575 ``gtpm = raw_gtpm``, 576 srw_tac [][GSYM pmact_bijections,is_pmact_def,is_pmact_raw_gtpm]); 577 578val gtpm_thm = save_thm( 579"gtpm_thm", 580raw_gtpm_thm |> SUBS [GSYM gtpm_raw]); 581 582val GFV_support = prove( 583 ``support gt_pmact t (GFV t)``, 584 srw_tac [][support_def, GSYM FRESH_swap0, gtpm_raw]) 585 586val MAP_EQ1 = prove( 587 ``(MAP f l = l) ��� ���x. MEM x l ��� (f x = x)``, 588 Induct_on `l` >> srw_tac [][DISJ_IMP_THM, FORALL_AND_THM]); 589 590val MEM_MAP = listTheory.MEM_MAP 591val EL_MAP = listTheory.EL_MAP 592val MEM_EL = listTheory.MEM_EL 593val IN_gfvl = prove( 594 ``x ��� gfvl ts ��� ���t. MEM t ts ��� x ��� GFV t``, 595 Induct_on `ts` >> srw_tac [][gfvl_thm] >> metis_tac []); 596 597val GFV_apart = prove( 598 ``���t x y. x ��� GFV t ��� y ��� GFV t ��� gtpm [(x,y)] t ��� t``, 599 ho_match_mp_tac simple_induction >> 600 srw_tac [][GFV_thm0, gtpm_thm, gterm_11, listTheory.MEM_MAP, 601 MAP_EQ1, GLAM_eq_thm0, IN_gfvl] >> 602 srw_tac [][] 603 >- metis_tac [] 604 >- (Cases_on `y = v` >> srw_tac [][] >> metis_tac []) 605 >- metis_tac [] 606 >- metis_tac [] 607 >- (Cases_on `y = v` >> srw_tac [][] >> metis_tac []) 608 >- metis_tac [] 609 >- metis_tac []) 610 611(* tempting to delete GFV and just use supp gtpm.... *) 612val GFV_supp = prove( 613 ``GFV = supp gt_pmact``, 614 srw_tac [][Once EQ_SYM_EQ, Once FUN_EQ_THM] >> 615 match_mp_tac (GEN_ALL supp_unique_apart) >> 616 srw_tac [][GFV_support, GFV_apart, FINITE_GFV]); 617 618val gfvl_listpm = prove( 619 ``gfvl = supp (list_pmact gt_pmact)``, 620 srw_tac [][Once FUN_EQ_THM] >> Induct_on `x` >> 621 srw_tac [][gfvl_thm, GFV_supp]); 622 623val rmGFV = REWRITE_RULE [GFV_supp, gfvl_listpm] 624val MAP_gtpm = prove( 625 ``MAP (gtpm pi) l = listpm gt_pmact pi l``, 626 Induct_on `l` >> srw_tac [][]); 627 628val GLAM_eq_thm1 = REWRITE_RULE [MAP_gtpm] (SUBS [GSYM gtpm_raw] GLAM_eq_thm0) 629 630val gtmsize_gtpml = prove( 631 ``MAP gtmsize (listpm gt_pmact pi pl) = MAP gtmsize pl``, 632 Induct_on `pl` >> fsrw_tac [][gtmsize_raw_gtpm, gtpm_raw]); 633 634val gtmsize_gtpm = CONJ (SUBS [GSYM gtpm_raw] gtmsize_raw_gtpm) (GEN_ALL gtmsize_gtpml) 635 636(* don't export any of these, because the intention is not to have users 637 working with this type *) 638val GFV_thm = save_thm("GFV_thm", rmGFV GFV_thm0) 639val GFV_gtpm = save_thm("GFV_gtpm", rmGFV (SUBS [GSYM gtpm_raw] GFV_raw_gtpm)) 640val gtpm_thm = save_thm("gtpm_thm", REWRITE_RULE [MAP_gtpm] gtpm_thm) 641val gterm_distinct = save_thm("gterm_distinct", gterm_distinct) 642val gterm_11 = save_thm("gterm_11", gterm_11) 643val GLAM_eq_thm = save_thm("GLAM_eq_thm", rmGFV GLAM_eq_thm1) 644val gtpm_fresh = save_thm("gtpm_fresh", rmGFV (SUBS [GSYM gtpm_raw] (GSYM FRESH_swap0))) 645val FINITE_GFV = save_thm("FINITE_GFV", rmGFV FINITE_GFV) 646val IN_GFVl = save_thm("IN_GFVl", rmGFV IN_gfvl) 647 648val _ = delete_const "gfvl" 649val _ = delete_const "GFV" 650val _ = delete_const "fv" 651 652val _ = overload_on ("GFV", ``supp gt_pmact``) 653val _ = overload_on ("GFVl", ``supp (list_pmact gt_pmact)``) 654 655val _ = augment_srw_ss [rewrites [gterm_distinct]] 656 657 658(* default rewriting of negations makes a mess of these. *) 659val NOT_IN_GFV = store_thm( 660 "NOT_IN_GFV", 661 ``(x ��� GFV (GVAR s vv) ��� x ��� s) ��� 662 (x ��� GFV (GLAM v bv ts us) ��� 663 (���u. MEM u us ��� x ��� GFV u) ��� 664 (���t. x ��� v ��� MEM t ts ��� x ��� GFV t))``, 665 srw_tac [][GFV_thm, IN_GFVl] >> metis_tac []); 666 667val GLAM_NIL_EQ = store_thm( 668 "GLAM_NIL_EQ", 669 ``(GLAM u bv1 [] ts = GLAM v bv2 [] ts') ��� (bv1 = bv2) ��� (ts = ts')``, 670 srw_tac [][GLAM_eq_thm] >> metis_tac []); 671 672val list_rel_split = prove( 673 ``LIST_REL (��x y. P x y ��� Q x y) l1 l2 ��� 674 LIST_REL P l1 l2 ��� LIST_REL Q l1 l2``, 675 qid_spec_tac `l2` >> Induct_on `l1` >> Cases_on `l2` >> srw_tac [][] >> 676 metis_tac []); 677 678val LIST_REL_ind = listTheory.LIST_REL_ind 679val LIST_REL_rules = listTheory.LIST_REL_rules 680val LIST_REL_EL_EQN = listTheory.LIST_REL_EL_EQN 681 682(* generic sub-type of a generic term, where one is only allowed to look 683 at the data attached to the GLAM and the number of arguments in the lists *) 684val (genind_rules, genind_ind, genind_cases) = Hol_reln` 685 (���n:num s vv. vp n vv ==> genind vp lp n (GVAR s vv)) ��� 686 (���n v bv ts us tns uns. 687 LIST_REL (genind vp lp) tns ts ��� 688 LIST_REL (genind vp lp) uns us ��� 689 lp n bv tns uns ��� 690 genind vp lp n (GLAM v bv ts us)) 691`; 692 693val grules' = genind_rules |> SPEC_ALL |> CONJUNCTS 694 695val genind_gtpm = store_thm( 696 "genind_gtpm", 697 ``���n t. genind vp lp n t ��� ���pi. genind vp lp n (gtpm pi t)``, 698 Induct_on `genind` >> 699 srw_tac [DNF_ss][gtpm_thm, genind_rules, list_rel_split] >> 700 match_mp_tac (List.nth(grules', 1)) >> 701 fsrw_tac [CONJ_ss][LIST_REL_EL_EQN,EL_MAP] >> 702 srw_tac [][] >> metis_tac []) 703 704val genind_gtpm_eqn = store_thm( 705 "genind_gtpm_eqn", 706 ``genind vp lp n (gtpm pi t) = genind vp lp n t``, 707 metis_tac [pmact_inverse, genind_gtpm]); 708val _ = augment_srw_ss [rewrites [genind_gtpm_eqn]] 709 710val LIST_REL_genind_gtpm_eqn = store_thm( 711 "LIST_REL_genind_gtpm_eqn", 712 ``LIST_REL (genind vp lp) ns (listpm gt_pmact pi ts) = 713 LIST_REL (genind vp lp) ns ts``, 714 qid_spec_tac `ns` >> Induct_on `ts` >> Cases_on `ns` >> 715 fsrw_tac [][]); 716 717val _ = augment_srw_ss [rewrites [FINITE_GFV, LIST_REL_genind_gtpm_eqn]] 718 719val _ = overload_on ("gtpml", ``listpm gt_pmact``) 720 721val gtpml_eqr = store_thm( 722"gtpml_eqr", 723``!t u. (t = gtpml pi u) = (gtpml (REVERSE pi) t = u)``, 724srw_tac [][pmact_eql]); 725 726val genind_GLAM_eqn = store_thm( 727 "genind_GLAM_eqn", 728 ``genind vp lp n (GLAM v bv ts us) = 729 ���tns uns. LIST_REL (genind vp lp) tns ts ��� 730 LIST_REL (genind vp lp) uns us ��� 731 lp n bv tns uns``, 732 srw_tac [DNF_ss][genind_cases, gterm_distinct, GLAM_eq_thm] >> 733 srw_tac [][gtpml_eqr, perm_supp] >> metis_tac []); 734 735val finite_gfvl = prove( 736 ``FINITE (GFVl ts)``, 737 Induct_on `ts` >> srw_tac [][MEM_MAP] >> srw_tac [][]); 738 739val _ = augment_srw_ss [rewrites [finite_gfvl]] 740 741val bvc_genind = store_thm( 742 "bvc_genind", 743 ``���P fv. 744 (���x. FINITE (fv x)) ��� 745 (���n s vv x. vp n vv ��� P n (GVAR s vv) x) ��� 746 (���n v bv tns uns ts us x. 747 LIST_REL (��n t. genind vp lp n t ��� ���x. P n t x) tns ts ��� 748 LIST_REL (��n t. genind vp lp n t ��� ���x. P n t x) uns us ��� 749 lp n bv tns uns ��� v ��� fv x ��� v ��� supp (list_pmact gt_pmact) us 750 ��� 751 P n (GLAM v bv ts us) x) 752 ��� 753 ���n t. genind vp lp n t ��� ���x. P n t x``, 754 rpt GEN_TAC >> strip_tac >> 755 qsuff_tac `���n t. genind vp lp n t ��� ���pi x. P n (gtpm pi t) x` 756 >- metis_tac [pmact_nil] >> 757 Induct_on `genind` >> srw_tac [DNF_ss][gtpm_thm, list_rel_split] >> 758 Q_TAC (NEW_TAC "z") 759 `fv x ��� {lswapstr pi v; v} ��� GFVl (gtpml pi us) ��� GFVl (gtpml pi ts)` >> 760 `GLAM (lswapstr pi v) bv (gtpml pi ts) (gtpml pi us) = 761 GLAM z bv (gtpml [(z,lswapstr pi v)] (gtpml pi ts)) (gtpml pi us)` 762 by (srw_tac [][GLAM_eq_thm, NOT_IN_supp_listpm] 763 >- fsrw_tac [DNF_ss][MEM_listpm_EXISTS, NOT_IN_supp_listpm, 764 GFV_gtpm] >> 765 srw_tac [ETA_ss][pmact_flip_args, pmact_nil]) >> 766 pop_assum SUBST1_TAC >> 767 first_x_assum match_mp_tac >> 768 map_every qexists_tac [`tns`, `uns`] >> 769 asm_simp_tac (srw_ss() ++ DNF_ss) [] >> 770 fsrw_tac [CONJ_ss][LIST_REL_EL_EQN, EL_listpm] >> 771 srw_tac [][GSYM pmact_decompose]) 772 773val genindX = 774 bvc_genind |> Q.SPEC `��n t x. Q n t` 775 |> Q.SPEC `��x. X` 776 |> SIMP_RULE (srw_ss()) [] 777 |> Q.INST [`Q` |-> `P`] |> GEN_ALL 778 779val genind_KT = prove( 780 ``���n t. genind (��n vv. T) (��n bv tns uns. T) n t``, 781 CONV_TAC SWAP_FORALL_CONV >> ho_match_mp_tac simple_induction >> 782 srw_tac [][] 783 >- (match_mp_tac (hd grules') >> srw_tac [][]) >> 784 match_mp_tac (hd (tl grules')) >> 785 map_every qexists_tac [`GENLIST (K 0) (LENGTH bndts)`, 786 `GENLIST (K 0) (LENGTH unbndts)`] >> 787 fsrw_tac[DNF_ss] [LIST_REL_EL_EQN, MEM_EL]); 788 789val vacuous_list_rel = prove( 790 ``LIST_REL (��x y. P y) xs ys ��� 791 (���y. MEM y ys ��� P y) ��� (LENGTH xs = LENGTH ys)``, 792 qid_spec_tac `ys` >> Induct_on `xs` >> Cases_on `ys` >> srw_tac [][] >> 793 metis_tac []); 794 795val silly = prove( 796 ``(���v bv tns uns ts us x. 797 LIST_REL (��n:num t. ���x. Q t x) tns ts ��� 798 LIST_REL (��n:num t. ���x. Q t x) uns us ��� v ��� fv x ��� 799 v ��� supp (list_pmact gt_pmact) us ��� 800 Q (GLAM v bv ts us) x) ��� 801 (���v bv ts us x. 802 (���t x. MEM t ts ��� Q t x) ��� (���u x. MEM u us ��� Q u x) ��� 803 v ��� fv x ��� v ��� supp (list_pmact gt_pmact) us ��� 804 Q (GLAM v bv ts us) x)``, 805 srw_tac [][EQ_IMP_THM, vacuous_list_rel] >> 806 first_x_assum (Q.SPECL_THEN [`v`,`bv`,`GENLIST (K 0) (LENGTH ts)`, 807 `GENLIST (K 0) (LENGTH us)`] MP_TAC) >> 808 srw_tac [][]); 809 810val gen_bvc_induction = 811 bvc_genind |> SPEC_ALL 812 |> Q.INST [`lp` |-> `(��n bv tns uns. T)`, 813 `vp` |-> `(��n vv. T)`, 814 `P` |-> `��n t x. Q t x`] 815 |> SIMP_RULE (srw_ss()) [genind_KT, silly] 816 |> Q.INST [`Q` |-> `P`] |> GEN_ALL 817 818val bvc_ind = 819 gen_bvc_induction |> INST_TYPE [gamma |-> ``:one``] 820 |> SPEC_ALL 821 |> Q.INST [`P` |-> `��t x. Q t`, `fv` |-> `��x. X`] 822 |> SIMP_RULE (srw_ss()) [] 823 |> Q.INST [`Q` |-> `P`] 824 |> Q.GEN `X` |> Q.GEN `P` 825 826val gterm_cases = store_thm( 827"gterm_cases", 828``���t. (���s vv. t = GVAR s vv) ��� (���s bv ts us. t = GLAM s bv ts us)``, 829ho_match_mp_tac simple_induction >> 830srw_tac [][] >> metis_tac []); 831 832Theorem FORALL_gterm: 833 (���t. P t) ��� (���s v. P (GVAR s v)) ��� (���s bv ts us. P (GLAM s bv ts us)) 834Proof 835 EQ_TAC >> srw_tac [][] >> 836 qspec_then `t` STRUCT_CASES_TAC gterm_cases >> srw_tac [][] 837QED 838 839val some_4_F = prove( 840 ``(some (w,x,y,z). F) = NONE``, 841 DEEP_INTRO_TAC optionTheory.some_intro THEN 842 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, pairTheory.EXISTS_PROD]); 843 844val SUM_MAP_MEM = Q.store_thm( 845"SUM_MAP_MEM", 846`���f x l. MEM x l ��� f x ��� SUM (MAP f l)`, 847ntac 2 gen_tac >> Induct >> srw_tac [][] >> 848fsrw_tac [ARITH_ss][]); 849 850val vf = mk_var ("vf", ``: string -> �� -> �� -> ��``) 851val lf = mk_var ("lf", ``: string -> �� -> (�� -> ��) list -> (�� -> ��) list 852 -> (��,��)gterm list -> (��,��)gterm list -> �� -> ��``) 853 854val trec = ``tmrec (A: string set) (ppm: �� pmact) ^vf ^lf : (��,��)gterm -> �� -> ��`` 855 856val tmrec_defn = Hol_defn "tmrec" ` 857 ^trec t = ��p. 858 case some(s,vv).(t = GVAR s vv) of 859 SOME (s,vv) => vf s vv p 860 | NONE => ( 861 case some(v,bv,ts,us).(t = GLAM v bv ts us) ��� v ��� supp ppm p ��� v ��� GFVl us ��� v ��� A of 862 SOME (v,bv,ts,us) => lf v bv (MAP (^trec) ts) (MAP (^trec) us) ts us p 863 | NONE => ARB)` 864 865val (tmrec_def, tmrec_ind) = Defn.tprove( 866 tmrec_defn, 867 WF_REL_TAC `measure (gtmsize o SND o SND o SND o SND)` >> 868 srw_tac [][] >> 869 qspec_then `t` FULL_STRUCT_CASES_TAC gterm_cases >> 870 fsrw_tac [][some_4_F,gterm_distinct] >> 871 fsrw_tac [][GLAM_eq_thm] >> 872 qpat_x_assum `X = SOME Y` mp_tac >> 873 DEEP_INTRO_TAC optionTheory.some_intro >> 874 simp_tac (srw_ss()) [pairTheory.EXISTS_PROD, pairTheory.FORALL_PROD] >> 875 srw_tac [][gtmsize_thm] >> 876 Q.ISPEC_THEN `gtmsize` imp_res_tac SUM_MAP_MEM >> 877 srw_tac [][gtmsize_gtpm] >> 878 DECIDE_TAC) 879 880val vp = ``vp: num -> �� -> bool`` 881val lp = ``lp: num -> �� -> num list -> num list -> bool`` 882 883val _ = temp_overload_on ("���", ``fnpm``) 884val _ = temp_set_fixity "���" (Infixr 700) 885 886val relsupp_def = Define` 887 relsupp A dpm ppm t r <=> 888 ���x. x ��� A ��� x ��� GFV t ==> x ��� supp (fn_pmact ppm dpm) r 889`; 890 891val sidecond_def = Define` 892 sidecond dpm ppm A ^vp ^lp ^vf ^lf ��� 893 FINITE A ��� (���p. FINITE (supp ppm p)) ��� 894 (���x y s vv n p. 895 x ��� A ��� y ��� A ��� genind vp lp n (GVAR s vv) ��� 896 (pmact dpm [(x,y)] (^vf s vv p) = 897 ^vf (lswapstr [(x,y)] s) vv (pmact ppm [(x,y)] p))) ��� 898 (���x y n v bv r1 r2 ts us p. 899 x ��� A ��� y ��� A ��� v ��� A ��� 900 genind vp lp n (GLAM v bv ts us) ��� 901 LIST_REL (relsupp A dpm ppm) ts r1 ��� 902 LIST_REL (relsupp A dpm ppm) us r2 ��� 903 v ��� supp ppm p ��� 904 (pmact dpm [(x,y)] (^lf v bv r1 r2 ts us p) = 905 ^lf (lswapstr [(x,y)] v) bv 906 (listpm (fn_pmact ppm dpm) [(x,y)] r1) 907 (listpm (fn_pmact ppm dpm) [(x,y)] r2) 908 (listpm gt_pmact [(x,y)] ts) 909 (listpm gt_pmact [(x,y)] us) 910 (pmact ppm [(x,y)] p)))` 911 912val FCB_def = Define` 913 FCB dpm ppm A ^vp ^lp ^lf ��� 914 ���a n v bv r1 r2 ts us p. 915 a ��� A ��� a ��� GFVl us ��� a ��� supp ppm p ��� 916 LIST_REL (relsupp A dpm ppm) ts r1 ��� 917 LIST_REL (relsupp A dpm ppm) us r2 ��� 918 genind vp lp n (GLAM v bv ts us) ��� 919 a ��� supp dpm (^lf a bv r1 r2 ts us p)` 920 921val some_2_EQ = prove( 922 ``(some (x,y). (x' = x) /\ (y' = y)) = SOME(x',y')``, 923 DEEP_INTRO_TAC optionTheory.some_intro THEN 924 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, pairTheory.EXISTS_PROD]); 925 926val some_2_F = prove( 927 ``(some (x,y). F) = NONE``, 928 DEEP_INTRO_TAC optionTheory.some_intro THEN 929 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, pairTheory.EXISTS_PROD]); 930 931val tmrec_GVAR = tmrec_def |> Q.INST [`t` |-> `GVAR s vv`] 932 |> SIMP_RULE (srw_ss()++ETA_ss) [gterm_11,some_2_EQ] 933val tmrec_GLAM = tmrec_def |> Q.INST [`t` |-> `GLAM v bv ts us`] 934 |> SIMP_RULE (srw_ss()) [gterm_distinct,some_2_F,NOT_IN_supp_listpm] 935 |> C (foldr (uncurry Q.GEN)) [`v`,`bv`,`ts`,`us`] 936 937val gtpm_GVAR = gtpm_thm |> CONJUNCT1 938val genind_GVAR = store_thm( 939 "genind_GVAR", 940 ``genind vp lp n (GVAR s vv) = vp n vv``, 941 srw_tac [][genind_cases,gterm_distinct,gterm_11]); 942val GFV_GVAR = GFV_thm |> CONJUNCT1 943 944val gtpm_eqr = store_thm( 945"gtpm_eqr", 946``(t = gtpm pi u) = (gtpm (REVERSE pi) t = u)``, 947METIS_TAC [pmact_inverse]); 948 949val lswapstr_sing = Q.prove(`lswapstr [(x,y)] z = swapstr x y z`, srw_tac [][]); 950 951val trec_fnpm = prove( 952 ``(ppm ��� apm) �� (tmrec A ppm vf lf t) = 953 ��p. pmact apm �� (tmrec A ppm vf lf t (pmact ppm ������� p))``, 954 srw_tac [][FUN_EQ_THM, fnpm_def]); 955 956val MAP_trec_fnpm = prove( 957``MAP ((ppm ��� dpm) pi o tmrec A ppm vf lf)= 958 MAP (��t p. pmact dpm pi (tmrec A ppm vf lf t (pmact ppm (REVERSE pi) p)))``, 959ONCE_REWRITE_TAC [FUN_EQ_THM] >> 960Induct >> srw_tac [][trec_fnpm]); 961 962val genind_GLAM_subterm = store_thm( 963"genind_GLAM_subterm", 964``genind vp lp n (GLAM v bv ts us) ��� (MEM u ts ��� MEM u us) ��� 965 ���n. genind vp lp n u``, 966srw_tac [][Once genind_cases,gterm_distinct] >> 967fsrw_tac [][GLAM_eq_thm] >> 968fsrw_tac [][LIST_REL_EL_EQN,MEM_EL] >> 969srw_tac [][] >> 970fsrw_tac [][EL_MAP] >> 971metis_tac []); 972 973val gtmsize_GLAM_subterm = store_thm( 974"gtmsize_GLAM_subterm", 975``(MEM t ts ��� MEM t us) ��� gtmsize t < gtmsize (GLAM s bv ts us)``, 976srw_tac [][gtmsize_thm] >> 977imp_res_tac SUM_MAP_MEM >> 978pop_assum (qspec_then `gtmsize` mp_tac) >> 979DECIDE_TAC); 980 981val LIST_REL_relsupp_gtpml = prove( 982 ``���A dpm ppm l1 l2. 983 LIST_REL (relsupp A dpm ppm) l1 l2 ==> 984 ���x y. x ��� A ��� y ��� A ==> 985 LIST_REL (relsupp A dpm ppm) 986 (gtpml [(x,y)] l1) 987 (listpm (fn_pmact ppm dpm) [(x,y)] l2)``, 988 ntac 3 gen_tac >> 989 Induct_on `LIST_REL` >> srw_tac [][relsupp_def, fnpm_def, perm_supp] >> 990 first_x_assum match_mp_tac >> srw_tac [][perm_supp] >> 991 srw_tac [][swapstr_def]) 992 993fun ih_commute_tac dir (asl,w) = 994 first_x_assum (fn rwt => 995 if free_in ``gtmsize`` (concl rwt) then 996 mp_tac (Q.GEN `n'` (PART_MATCH (lhs o #2 o strip_imp) rwt (dir w))) 997 else NO_TAC) (asl,w) 998 999fun sidecond_tac dir = 1000 qpat_x_assum `sidecond AA BB CC DD EE FF GG` 1001 (fn th => th |> SIMP_RULE (srw_ss()) [sidecond_def] |> CONJUNCTS 1002 |> last |> (fn th' => assume_tac th >> assume_tac th')) >> 1003 (fn (asl,w) => 1004 pop_assum (fn rwt => mp_tac (PART_MATCH (lhs o #2 o strip_imp) 1005 rwt 1006 (dir w))) (asl,w)) 1007 1008val _ = set_trace "Goalstack.print_goal_at_top" 0 1009 1010val listpm_tMAP = prove( 1011 ``(listpm apm pi (MAP f l) = 1012 MAP ((gt_pmact ��� apm) pi f) (gtpml pi l))``, 1013 srw_tac [][] >> Induct_on `l` >> srw_tac [][fnpm_def]); 1014 1015val tmrec_equivariant = store_thm( (* correct name? *) 1016"tmrec_equivariant", 1017``sidecond dpm ppm A ^vp ^lp ^vf ^lf ��� FCB dpm ppm A ^vp ^lp ^lf ��� 1018 ���n. genind vp lp n t ��� 1019 ���p x y. x ��� A ��� y ��� A ��� 1020 (pmact dpm [(x,y)] (tmrec A ppm vf lf t p) = 1021 tmrec A ppm vf lf (gtpm [(x,y)] t) (pmact ppm [(x,y)] p))``, 1022strip_tac >> 1023completeInduct_on `gtmsize t` >> 1024qabbrev_tac `m = v` >> markerLib.RM_ALL_ABBREVS_TAC >> 1025pop_assum (strip_assume_tac o SIMP_RULE (srw_ss() ++ DNF_ss) []) >> 1026simp_tac (srw_ss()) [Once FORALL_gterm] >> 1027conj_tac >- ( 1028 (* GVAR case *) 1029 srw_tac [][gtpm_GVAR,tmrec_GVAR] >> 1030 fsrw_tac [][sidecond_def] >> 1031 metis_tac [lswapstr_sing]) >> 1032rpt gen_tac >> 1033disch_then SUBST_ALL_TAC >> 1034gen_tac >> strip_tac >> 1035qx_gen_tac `p` >> 1036Q.SPECL_THEN [`s`,`bv`,`ts`,`us`,`p`] MP_TAC 1037 (tmrec_GLAM |> SIMP_RULE (srw_ss()) [FUN_EQ_THM]) >> 1038DEEP_INTRO_TAC optionTheory.some_intro >> 1039asm_simp_tac (srw_ss()) [pairTheory.FORALL_PROD] >> 1040`FINITE A ��� (���p. FINITE (supp ppm p))` 1041 by fsrw_tac [][sidecond_def] >> 1042reverse conj_tac >- ( 1043 (* bogus some(...) = ARB case *) 1044 Q_TAC (NEW_TAC "z") `supp ppm p ��� A ��� GFVl us ��� GFVl ts ��� {s}` >> 1045 disch_then (qspec_then `z` mp_tac) >> 1046 asm_simp_tac (srw_ss()++DNF_ss) [GLAM_eq_thm,IN_GFVl,gtpml_eqr,listpm_MAP,MEM_MAP,GFV_gtpm] >> 1047 fsrw_tac [][IN_GFVl] >> 1048 metis_tac []) >> 1049map_every qx_gen_tac [`s'`,`bv'`,`ts'`,`us'`] >> 1050strip_tac >> 1051strip_tac >> 1052`(us' = us) ��� (bv' = bv)` by fsrw_tac [][GLAM_eq_thm] >> rpt VAR_EQ_TAC >> 1053asm_simp_tac (srw_ss()++DNF_ss) [gtpm_thm,IN_GFVl,GFV_thm] >> 1054map_every qx_gen_tac [`x`, `y`] >> 1055strip_tac >> 1056qpat_x_assum `tmrec A ppm vf lf (GLAM X Y Z WW) p = XX` (K ALL_TAC) >> 1057srw_tac [][tmrec_GLAM] >> 1058DEEP_INTRO_TAC optionTheory.some_intro >> 1059asm_simp_tac (srw_ss()++ETA_ss) [pairTheory.FORALL_PROD] >> 1060reverse conj_tac >- ( 1061 (* bogus ARB case *) 1062 asm_simp_tac (srw_ss()) [GLAM_eq_thm] >> 1063 Q_TAC (NEW_TAC "z") `{swapstr x y s'} ��� A ��� supp ppm (pmact ppm [(x,y)] p) ��� GFVl (gtpml [(x,y)] us) ��� GFVl (gtpml [(x,y)] ts')` >> 1064 disch_then (qspec_then `z` mp_tac) >> 1065 fsrw_tac [DNF_ss][IN_GFVl,gtpml_eqr,listpm_MAP,MEM_MAP,GFV_gtpm] >> 1066 reverse conj_tac >- metis_tac [] >> 1067 conj_tac >- metis_tac [] >> 1068 srw_tac [][] >> metis_tac []) >> 1069qabbrev_tac `r1 = MAP (tmrec A ppm vf lf) ts'` >> 1070qabbrev_tac `r2 = MAP (tmrec A ppm vf lf) us` >> 1071fsrw_tac [][AND_IMP_INTRO] >> 1072`���tns uns. LIST_REL (genind vp lp) tns ts ��� LIST_REL (genind vp lp) uns us` 1073 by (fsrw_tac [][genind_cases, GLAM_eq_thm] >> srw_tac [][] >> 1074 metis_tac []) >> 1075`LIST_REL (genind vp lp) tns ts'` 1076 by (fsrw_tac [][GLAM_eq_thm] >> srw_tac [][] >> fsrw_tac [][]) >> 1077qabbrev_tac `GGSIZE = gtmsize (GLAM s' bv ts' us)` >> 1078`���t n' a. gtmsize t < GGSIZE ��� genind vp lp n' t ��� a ��� A ��� a ��� GFV t ==> 1079 a ��� supp (fn_pmact ppm dpm) (tmrec A ppm vf lf t)` 1080 by (srw_tac [][] >> match_mp_tac notinsupp_I >> 1081 qexists_tac `A ��� GFV t` >> 1082 srw_tac [][support_def, fnpm_def, FUN_EQ_THM] >> 1083 metis_tac [supp_fresh, pmact_sing_inv]) >> 1084`LIST_REL (relsupp A dpm ppm) ts' r1 ��� LIST_REL (relsupp A dpm ppm) us r2` 1085 by (srw_tac [][LIST_REL_EL_EQN, relsupp_def, Abbr`r1`, Abbr`r2`] >> 1086 srw_tac [][EL_MAP] >> first_x_assum match_mp_tac >| 1087 [qexists_tac `EL n' tns`, qexists_tac `EL n' uns`] >> 1088 metis_tac [LIST_REL_EL_EQN, MEM_EL, gtmsize_GLAM_subterm]) >> 1089(* COMPLETE THIS... *) 1090`���t p x y. 1091 (MEM t ts' ��� MEM t us ��� MEM t ts) ��� x ��� A ��� y ��� A ==> 1092 (pmact dpm [(x,y)] (tmrec A ppm vf lf t p) = 1093 tmrec A ppm vf lf (gtpm [(x,y)] t) (pmact ppm [(x,y)] p))` 1094 by (srw_tac [][] >> first_x_assum match_mp_tac >> 1095 fsrw_tac [][GLAM_eq_thm] >> srw_tac [][] >> 1096 fsrw_tac [][MEM_listpm_EXISTS, gtmsize_gtpm] >> 1097 metis_tac [genind_GLAM_subterm, gtmsize_GLAM_subterm]) >> 1098(* THEN COMPLETE THIS ... *) 1099`(���a b. a ��� A ��� b ��� A ==> 1100 (listpm (fn_pmact ppm dpm) [(a,b)] r1 = 1101 MAP (tmrec A ppm vf lf) (gtpml [(a,b)] ts'))) ��� 1102 (���a b. a ��� A ��� b ��� A ==> 1103 (listpm (fn_pmact ppm dpm) [(a,b)] r2 = 1104 MAP (tmrec A ppm vf lf) (gtpml [(a,b)] us)))` 1105 by (asm_simp_tac (srw_ss() ++ DNF_ss) 1106 [listpm_tMAP, listTheory.MAP_EQ_f, MEM_listpm_EXISTS, 1107 Abbr`r1`, Abbr`r2`, fnpm_def, FUN_EQ_THM, 1108 pmact_sing_inv]) >> 1109map_every qx_gen_tac [`s''`, `bv'`, `ts''`, `us'`] >> 1110srw_tac [][] >> 1111`(bv' = bv) ��� (us' = gtpml [(x,y)] us)` by fsrw_tac [][GLAM_eq_thm] >> 1112rpt VAR_EQ_TAC >> 1113sidecond_tac lhs >> 1114disch_then (fn th => asm_simp_tac (srw_ss()) [th]) >> 1115qpat_x_assum `GLAM (swapstr x y s') bv Z1 Z2 = Z3` mp_tac >> 1116srw_tac [][GLAM_eq_thm] >> 1117qabbrev_tac `u = swapstr x y s'` >> 1118fsrw_tac [][gtpml_eqr] >> 1119qpat_x_assum `XX = ts''` (SUBST_ALL_TAC o SYM) >> 1120`u ��� A` by srw_tac [][Abbr`u`,swapstr_def] >> 1121`u ��� supp ppm (pmact ppm [(x,y)] p)` by srw_tac [][Abbr`u`,perm_supp] >> 1122`s'' ��� supp (list_pmact gt_pmact) (gtpml [(x,y)] us) ��� 1123 s'' ��� supp (list_pmact gt_pmact) (gtpml [(x,y)] ts')` by ( 1124 fsrw_tac [DNF_ss][IN_GFVl,listpm_MAP,MEM_MAP,GFV_gtpm] >> 1125 metis_tac [] ) >> 1126`u ��� supp (list_pmact gt_pmact) (gtpml [(x,y)] us)` by ( 1127 fsrw_tac [DNF_ss][IN_GFVl,listpm_MAP,MEM_MAP,GFV_gtpm,Abbr`u`] >> 1128 metis_tac [] ) >> 1129`genind vp lp n (GLAM u bv (gtpml [(x,y)] ts') (gtpml [(x,y)] us))` by ( 1130 qmatch_abbrev_tac `genind vp lp n t` >> 1131 qsuff_tac `t = gtpm [(x,y)] (GLAM s' bv ts' us)` >- srw_tac [][] >> 1132 srw_tac [][Abbr`t`,gtpm_thm] ) >> 1133qmatch_abbrev_tac `LHS = RHS` >> 1134match_mp_tac EQ_TRANS >> 1135qexists_tac `pmact dpm [(u,s'')] RHS` >> 1136qabbrev_tac `usxyts = gtpml [(u,s'')] (gtpml [(x,y)] ts')` >> 1137qabbrev_tac `xyus = gtpml [(x,y)] us` >> 1138`genind vp lp n (GLAM s'' bv usxyts xyus)` 1139 by(first_x_assum (mp_tac o MATCH_MP genind_gtpm) >> 1140 disch_then (qspec_then `[(u,s'')]` mp_tac) >> 1141 CONV_TAC (LAND_CONV (RAND_CONV (REWRITE_CONV [gtpm_thm]))) >> 1142 asm_simp_tac (srw_ss()) [supp_fresh]) >> 1143`LIST_REL (relsupp A dpm ppm) usxyts (MAP (tmrec A ppm vf lf) usxyts) ��� 1144 LIST_REL (relsupp A dpm ppm) xyus (MAP (tmrec A ppm vf lf) xyus)` 1145 by (map_every qunabbrev_tac [`r1`, `r2`, `usxyts`, `xyus`] >> 1146 rpt (first_x_assum (mp_tac o MATCH_MP LIST_REL_relsupp_gtpml)) >> 1147 rpt (disch_then (qspecl_then [`x`,`y`] assume_tac)) >> 1148 ntac 2 (pop_assum mp_tac) >> asm_simp_tac (srw_ss()) [] >> 1149 rpt (disch_then (assume_tac o MATCH_MP LIST_REL_relsupp_gtpml)) >> 1150 ntac 2 (pop_assum (qspecl_then [`u`, `s''`] mp_tac)) >> 1151 asm_simp_tac (srw_ss()) [listpm_tMAP] >> 1152 rpt (disch_then assume_tac) >> 1153 qpat_x_assum `LIST_REL _ (_ (_ ts')) (MAP _ _)` mp_tac >> 1154 qmatch_abbrev_tac 1155 `LIST_REL RR TS (MAP f1 TS) ==> LIST_REL RR TS (MAP f2 TS)` >> 1156 qsuff_tac `MAP f1 TS = MAP f2 TS` >- srw_tac [][] >> 1157 srw_tac [][listTheory.MAP_EQ_f] >> 1158 map_every qunabbrev_tac [`f1`, `f2`, `TS`] >> 1159 asm_simp_tac (srw_ss()) [FUN_EQ_THM, fnpm_def] >> gen_tac >> 1160 ih_commute_tac lhs >> asm_simp_tac (srw_ss()) [pmact_sing_inv] >> 1161 disch_then match_mp_tac >> 1162 fsrw_tac [][MEM_listpm_EXISTS, gtmsize_gtpm] >> 1163 metis_tac [gtmsize_GLAM_subterm, genind_GLAM_subterm]) >> 1164reverse conj_tac >- ( 1165 match_mp_tac supp_fresh >> 1166 reverse conj_tac >- ( 1167 fsrw_tac [][FCB_def,Abbr`RHS`] >> 1168 first_x_assum match_mp_tac >> 1169 asm_simp_tac (srw_ss()) [] >> 1170 map_every qexists_tac [`n`,`s''`] >> 1171 srw_tac [][]) >> 1172 match_mp_tac notinsupp_I >> 1173 qunabbrev_tac `RHS` >> 1174 qexists_tac 1175 `A ��� {s''} ��� supp ppm (pmact ppm [(x,y)] p) ��� GFVl xyus ��� GFVl usxyts` >> 1176 `FINITE A ��� (���p. FINITE (supp ppm p))` by fsrw_tac [][sidecond_def] >> 1177 asm_simp_tac (srw_ss()) [support_def] >> 1178 map_every qx_gen_tac [`w`,`z`] >> 1179 strip_tac >> 1180 sidecond_tac lhs >> 1181 asm_simp_tac (srw_ss()) [] >> 1182 disch_then (K ALL_TAC) >> 1183 asm_simp_tac (srw_ss()) [listpm_tMAP, supp_fresh] >> 1184 rpt AP_THM_TAC >> 1185 qmatch_abbrev_tac `lf s'' bv X1 Y1 = lf s'' bv X2 Y2` >> 1186 qsuff_tac `(X1 = X2) ��� (Y1 = Y2)` >- srw_tac [][] >> 1187 map_every qunabbrev_tac [`X1`, `X2`, `Y1`, `Y2`] >> 1188 asm_simp_tac (srw_ss() ++ DNF_ss) 1189 [listTheory.MAP_EQ_f, MEM_listpm_EXISTS, FUN_EQ_THM, fnpm_def] >> 1190 srw_tac [][] >> (* two similar goals here-on *) 1191 ih_commute_tac lhs >> 1192 asm_simp_tac (srw_ss()) [gtmsize_gtpm, pmact_sing_inv] >> 1193 disch_then match_mp_tac >> 1194 map_every qunabbrev_tac [`usxyts`, `xyus`] >> 1195 fsrw_tac [][MEM_listpm_EXISTS, gtmsize_gtpm] >> 1196 metis_tac [gtmsize_GLAM_subterm, genind_GLAM_subterm]) >> 1197srw_tac [][Abbr`RHS`] >> 1198sidecond_tac rhs >> 1199asm_simp_tac (srw_ss()) [listpm_tMAP, supp_fresh] >> 1200disch_then (K ALL_TAC) >> 1201qunabbrev_tac `LHS` >> rpt AP_THM_TAC >> 1202qunabbrev_tac `usxyts` >> 1203asm_simp_tac (srw_ss() ++ ETA_ss) [pmact_sing_inv, pmact_nil] >> 1204AP_THM_TAC >> 1205qmatch_abbrev_tac `lf u bv X1 Y1 = lf u bv X2 Y2` >> 1206qsuff_tac `(X1 = X2) ��� (Y1 = Y2)` >- srw_tac [][] >> 1207map_every qunabbrev_tac [`X1`,`X2`,`Y1`, `Y2`] >> 1208conj_tac >> (* splits in two *) 1209srw_tac [][listTheory.MAP_EQ_f, FUN_EQ_THM, fnpm_def] >> 1210ih_commute_tac rhs >> 1211asm_simp_tac (srw_ss()) [pmact_sing_inv, gtmsize_gtpm] >> 1212disch_then (match_mp_tac o GSYM) >> 1213qunabbrev_tac `xyus` >> 1214fsrw_tac [][MEM_listpm_EXISTS, gtmsize_gtpm] >> 1215metis_tac [genind_GLAM_subterm, gtmsize_GLAM_subterm]); 1216 1217fun udplus th = 1218 th |> REWRITE_RULE [GSYM CONJ_ASSOC] 1219 |> repeat (UNDISCH o CONV_RULE (REWR_CONV (GSYM AND_IMP_INTRO))) 1220 |> UNDISCH 1221 1222val eqv_I = tmrec_equivariant |> udplus 1223 1224val tmrec_fresh = store_thm( 1225 "tmrec_fresh", 1226 ``sidecond dpm ppm A ^vp ^lp ^vf ^lf ��� FCB dpm ppm A vp lp lf ==> 1227 ���n t. genind vp lp n t ==> 1228 ���x. x ��� A ��� x ��� GFV t ==> 1229 x ��� supp (fn_pmact ppm dpm) (tmrec A ppm vf lf t)``, 1230 srw_tac [][] >> match_mp_tac notinsupp_I >> qexists_tac `GFV t ��� A` >> 1231 `FINITE A` by fsrw_tac [][sidecond_def] >> 1232 srw_tac [][support_def, FUN_EQ_THM, fnpm_def] >> 1233 metis_tac [tmrec_equivariant, supp_fresh, pmact_sing_inv]); 1234 1235val NEWFCB_def = Define` 1236 NEWFCB dpm ppm A vp lp lf ��� 1237 ���a1 a2 n bv r1 r2 ts us p. 1238 a1 ��� A ��� a1 ��� supp ppm p ��� a2 ��� A ��� a2 ��� GFVl ts ��� a2 ��� supp ppm p ��� 1239 LIST_REL (relsupp A dpm ppm) ts r1 ��� 1240 LIST_REL (relsupp A dpm ppm) us r2 ��� 1241 genind vp lp n (GLAM a1 bv ts us) ==> 1242 (lf a2 bv (listpm (fn_pmact ppm dpm) [(a2,a1)] r1) r2 1243 (gtpml [(a2,a1)] ts) us p = 1244 lf a1 bv r1 r2 ts us p) 1245` 1246 1247val LIST_REL_combined_supps = prove( 1248 ``LIST_REL (relsupp A dpm ppm) ts rs ��� x ��� A ��� x ��� GFVl ts ==> 1249 x ��� supp (list_pmact (fn_pmact ppm dpm)) rs``, 1250 qsuff_tac 1251 `���ts rs. LIST_REL (relsupp A dpm ppm) ts rs ==> 1252 ���x. x ��� GFVl ts ��� x ��� A ==> x ��� supp (list_pmact (fn_pmact ppm dpm)) rs` 1253 >- metis_tac [] >> 1254 Induct_on `LIST_REL` >> srw_tac [][relsupp_def]); 1255 1256val NEWFCB_OLD = prove( 1257 ``NEWFCB dpm ppm A vp lp ^lf ��� sidecond dpm ppm A vp lp vf lf ==> 1258 FCB dpm ppm A vp lp lf``, 1259 srw_tac [][FCB_def, NEWFCB_def] >> 1260 `FINITE A ��� (���p. FINITE (supp ppm p))` 1261 by fsrw_tac [][sidecond_def] >> 1262 Q_TAC (NEW_TAC "z") `A ��� GFVl ts ��� GFVl us ��� supp ppm p ��� {a}` >> 1263 `lf a bv r1 r2 ts us p = lf z bv (listpm (fn_pmact ppm dpm) [(z,a)] r1) r2 1264 (gtpml [(z,a)] ts) us p` 1265 by (fsrw_tac [][NEWFCB_def] >> ONCE_REWRITE_TAC [EQ_SYM_EQ] >> 1266 first_x_assum match_mp_tac >> 1267 fsrw_tac [][genind_GLAM_eqn] >> metis_tac []) >> 1268 pop_assum SUBST1_TAC >> 1269 match_mp_tac notinsupp_I >> 1270 qexists_tac `{z} ��� A ��� GFVl (gtpml [(z,a)] ts) ��� GFVl us ��� supp ppm p` >> 1271 srw_tac [][perm_supp]>> 1272 srw_tac [][support_def] >> 1273 sidecond_tac lhs >> 1274 `x ��� supp (list_pmact (fn_pmact ppm dpm)) r2 ��� y ��� supp (list_pmact (fn_pmact ppm dpm)) r2 ��� 1275 x ��� supp (list_pmact (fn_pmact ppm dpm)) (listpm (fn_pmact ppm dpm) [(z,a)] r1) ��� 1276 y ��� supp (list_pmact (fn_pmact ppm dpm)) (listpm (fn_pmact ppm dpm) [(z,a)] r1)` 1277 by (srw_tac [][perm_supp] >> 1278 metis_tac [LIST_REL_combined_supps, swapstr_def]) >> 1279 asm_simp_tac (srw_ss()) [LIST_REL_relsupp_gtpml, genind_GLAM_eqn, supp_fresh, 1280 perm_supp] >> 1281 disch_then match_mp_tac >> fsrw_tac [][genind_GLAM_eqn] >> metis_tac []); 1282 1283val fresh_I = PROVE_HYP (udplus NEWFCB_OLD) (udplus tmrec_fresh) 1284val eqv_I = PROVE_HYP (udplus NEWFCB_OLD) (udplus tmrec_equivariant) 1285 1286 1287fun xmatch_cond_assum dir (asl,w) = 1288 first_x_assum (fn rwt => 1289 mp_tac (PART_MATCH (lhs o #2 o strip_imp) 1290 rwt 1291 (dir w))) (asl,w) 1292 1293 1294val parameter_gtm_recursion = store_thm( 1295"parameter_gtm_recursion", 1296``sidecond dpm ppm A ^vp ^lp ^vf ^lf ��� NEWFCB dpm ppm A ^vp ^lp ^lf ��� 1297 ���f. 1298 ((���n s vv p. genind vp lp n (GVAR s vv) ��� (f (GVAR s vv) p = vf s vv p)) ��� 1299 ���n v bv ns ms ts us p. 1300 v ��� A ��� v ��� supp ppm p ��� genind vp lp n (GLAM v bv ts us) ��� 1301 (f (GLAM v bv ts us) p = lf v bv (MAP f ts) (MAP f us) ts us p)) ��� 1302 ���n t p. 1303 genind vp lp n t ==> 1304 ���x y. x ��� A ��� y ��� A ==> 1305 (pmact dpm [(x,y)] (f t p) = f (gtpm [(x,y)] t) (pmact ppm [(x,y)] p))``, 1306strip_tac >> 1307`FINITE A ��� ���p. FINITE (supp ppm p)` by fsrw_tac [][sidecond_def] >> 1308qexists_tac `tmrec A ppm vf lf` >> 1309reverse conj_tac >- 1310 (rpt strip_tac >> imp_res_tac eqv_I >> srw_tac [][]) >> 1311conj_tac >- srw_tac [][tmrec_GVAR] >> 1312srw_tac [][tmrec_GLAM] >> 1313DEEP_INTRO_TAC optionTheory.some_intro >> 1314asm_simp_tac (srw_ss()) [pairTheory.FORALL_PROD, pairTheory.EXISTS_PROD] >> 1315reverse conj_tac >- ( 1316 (* bogus ARB case *) 1317 asm_simp_tac (srw_ss()) [GLAM_eq_thm] >> 1318 Q_TAC (NEW_TAC "z") `A ��� supp ppm p ��� GFVl ts ��� GFVl us ��� {v}` >> 1319 disch_then (qspec_then `z` mp_tac) >> 1320 fsrw_tac [][gtpml_eqr] >> 1321 fsrw_tac [DNF_ss][IN_supp_listpm, MEM_listpm_EXISTS, perm_supp] >> 1322 metis_tac []) >> 1323asm_simp_tac (srw_ss()++DNF_ss++ETA_ss) [GLAM_eq_thm,gtpml_eqr,gtpm_eqr] >> 1324qx_gen_tac `u` >> strip_tac >> 1325`LIST_REL (relsupp A dpm ppm) ts (MAP (tmrec A ppm vf lf) ts) ��� 1326 LIST_REL (relsupp A dpm ppm) us (MAP (tmrec A ppm vf lf) us)` by ( 1327 assume_tac fresh_I >> 1328 fsrw_tac [DNF_ss][MEM_EL] >> 1329 srw_tac [][LIST_REL_EL_EQN,listTheory.EL_MAP, relsupp_def] >> 1330 fsrw_tac [][AND_IMP_INTRO] >> 1331 first_x_assum match_mp_tac >> 1332 fsrw_tac [][] >> 1333 match_mp_tac genind_GLAM_subterm >> 1334 srw_tac [][MEM_EL] >> 1335 metis_tac []) >> 1336asm_simp_tac (srw_ss()) [pmact_flip_args] >> 1337qsuff_tac `MAP (tmrec A ppm vf lf) (gtpml [(u,v)] ts) = 1338 listpm (fn_pmact ppm dpm) [(u,v)] (MAP (tmrec A ppm vf lf) ts)` 1339 >- (disch_then SUBST1_TAC >> fsrw_tac [][NEWFCB_def] >> 1340 first_x_assum match_mp_tac >> fsrw_tac [][perm_supp] >> metis_tac []) >> 1341srw_tac [][listpm_tMAP, listTheory.MAP_EQ_f, MEM_listpm_EXISTS, FUN_EQ_THM, 1342 fnpm_def] >> 1343srw_tac [][pmact_sing_inv] >> 1344assume_tac (eqv_I |> Q.GEN `t` 1345 |> SIMP_RULE (srw_ss() ++ DNF_ss) [AND_IMP_INTRO]) >> 1346(fn (asl,w) => pop_assum 1347 (fn rwt => 1348 mp_tac (PART_MATCH (lhs o #2 o dest_imp) rwt 1349 (rhs w) |> Q.GEN `n`)) (asl,w)) >> 1350asm_simp_tac (srw_ss()) [pmact_sing_inv] >> 1351metis_tac [genind_GLAM_subterm]); 1352 1353val _ = export_theory() 1354