1(* this is an -*- sml -*- file *) 2(* script file establishing a type of lambda-terms on top of the 3 GM base. Does this by defining the predicate "const-free" *) 4 5open HolKernel Parse boolLib bossLib BasicProvers boolSimps NEWLib 6open ncTheory swapTheory binderLib 7 8val _ = new_theory "gmterm"; 9 10val (constfree_rules, constfree_ind, constfree_cases) = Hol_reln` 11 (!s. constfree (nc$VAR s)) /\ 12 (!M N. constfree M /\ constfree N ==> constfree (M @@ N)) /\ 13 (!v M. constfree M ==> constfree (LAM v M)) 14`; 15 16val constfree_swap_I = prove( 17 ``!M. constfree M ==> !x y. constfree (swap x y M)``, 18 HO_MATCH_MP_TAC constfree_ind THEN SRW_TAC [][constfree_rules]); 19 20val constfree_thm = store_thm( 21 "constfree_thm", 22 ``(constfree (nc$VAR s) = T) /\ 23 (constfree (M @@ N) = constfree M /\ constfree N) /\ 24 (constfree (LAM v M) = constfree M) /\ 25 (constfree (CON k) = F)``, 26 REPEAT CONJ_TAC THEN 27 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [constfree_cases])) THEN 28 SRW_TAC [][] THEN EQ_TAC THENL [ 29 SRW_TAC [][LAM_INJ_swap] THEN 30 METIS_TAC [lswap_def, constfree_swap_I], 31 METIS_TAC [] 32 ]); 33val _ = export_rewrites ["constfree_thm"] 34 35val lswap_constfree = prove( 36 ``!t. constfree (lswap pi t) = constfree t``, 37 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 38val _ = augment_srw_ss [rewrites [lswap_constfree]] 39 40val swap_constfree = prove( 41 ``constfree (swap x y t) = constfree t``, 42 MP_TAC (Q.INST [`pi` |-> `[(x,y)]`] (SPEC_ALL lswap_constfree)) THEN 43 REWRITE_TAC [lswap_def]); 44val _ = augment_srw_ss [rewrites [swap_constfree]] 45 46val term_ax = new_type_definition( 47 "term", 48 prove(``?t : one nc. constfree t``, 49 Q.EXISTS_TAC `nc$VAR s` THEN SRW_TAC [][])) 50 51val term_bij = define_new_type_bijections 52 {ABS = "to_term", REP = "from_term", 53 name = "term_bij", tyax = term_ax} 54 55val _ = app (fn s => remove_ovl_mapping s {Name = s, Thy = "nc"}) 56 ["LAM", "VAR", "CON", "@@", "FV", "SUB", "ABS", "size"] 57 58val VAR_def = Define`VAR s = to_term (nc$VAR s)` 59val APP_def = xDefine "APP" 60 `M @@ N = to_term (nc$@@ (from_term M) (from_term N))` 61val LAM_def = Define`LAM v t = to_term (nc$LAM v (from_term t))` 62 63val fromto_inverse = prove( 64 ``constfree t ==> (from_term (to_term t) = t)``, 65 METIS_TAC [term_bij]); 66 67val tofrom_inverse = prove( 68 ``to_term (from_term t) = t``, 69 SRW_TAC [][term_bij]); 70val _ = augment_srw_ss [rewrites [tofrom_inverse]] 71 72val constfree_from_term = prove( 73 ``constfree (from_term M)``, 74 SRW_TAC [][term_bij]); 75val _ = augment_srw_ss [rewrites [constfree_from_term]] 76 77val from_term_11 = prove( 78 ``(from_term t = from_term u) = (t = u)``, 79 METIS_TAC [term_bij]); 80 81val term_11 = store_thm( 82 "term_11", 83 ``((VAR s = VAR t) = (s = t)) /\ 84 ((M1 @@ N1 = M2 @@ N2) = (M1 = M2) /\ (N1 = N2)) /\ 85 ((LAM v M1 = LAM v M2) = (M1 = M2))``, 86 SRW_TAC [][VAR_def, APP_def, LAM_def, EQ_IMP_THM] THEN 87 POP_ASSUM (MP_TAC o AP_TERM ``from_term``) THEN 88 SRW_TAC [][fromto_inverse] THEN 89 FULL_SIMP_TAC (srw_ss()) [from_term_11]); 90val _ = export_rewrites ["term_11"] 91 92val term_distinct = store_thm( 93 "term_distinct", 94 ``~(VAR s = M @@ N) /\ ~(VAR s = LAM v t) /\ ~(M @@ N = LAM v t)``, 95 SRW_TAC [][VAR_def, APP_def, LAM_def] THEN STRIP_TAC THEN 96 POP_ASSUM (MP_TAC o AP_TERM ``from_term``) THEN 97 SRW_TAC [][fromto_inverse]); 98val _ = export_rewrites ["term_distinct"] 99 100val simple_induction = store_thm( 101 "simple_induction", 102 ``!P. (!s. P (VAR s)) /\ 103 (!M N. P M /\ P N ==> P (M @@ N)) /\ 104 (!v M. P M ==> P (LAM v M)) ==> 105 !M. P M``, 106 SIMP_TAC (srw_ss())[VAR_def, APP_def, LAM_def] THEN 107 GEN_TAC THEN STRIP_TAC THEN 108 Q_TAC SUFF_TAC `!M. constfree M ==> P (to_term M)` 109 THEN1 (REPEAT STRIP_TAC THEN 110 `M = to_term (from_term M)` by METIS_TAC [term_bij] THEN 111 POP_ASSUM SUBST1_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 112 SRW_TAC [][term_bij]) THEN 113 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THENL [ 114 `(M = from_term (to_term M)) /\ (M' = from_term (to_term M'))` 115 by METIS_TAC [term_bij] THEN 116 NTAC 2 (POP_ASSUM SUBST1_TAC) THEN 117 SRW_TAC [][], 118 `(M = from_term (to_term M))` by METIS_TAC [term_bij] THEN 119 POP_ASSUM SUBST1_TAC THEN SRW_TAC [][] 120 ]); 121 122val tpm_def = Define`tpm pi t = to_term (lswap pi (from_term t))` 123 124 125 126val tpm_thm = store_thm( 127 "tpm_thm", 128 ``(tpm pi (VAR s) = VAR (raw_lswapstr pi s)) /\ 129 (tpm pi (M @@ N) = tpm pi M @@ tpm pi N) /\ 130 (tpm pi (LAM v M) = LAM (raw_lswapstr pi v) (tpm pi M))``, 131 SRW_TAC [][tpm_def, LAM_def, APP_def, VAR_def, fromto_inverse]); 132val _ = export_rewrites ["tpm_thm"] 133 134val FV_def = Define`FV t = nc$FV (from_term t)` 135 136val FV_thm = store_thm( 137 "FV_thm", 138 ``(FV (VAR s) = {s}) /\ 139 (FV (M @@ N) = FV M UNION FV N) /\ 140 (FV (LAM v M) = FV M DELETE v)``, 141 SRW_TAC [][FV_def, LAM_def, APP_def, VAR_def, fromto_inverse]); 142val _ = export_rewrites ["FV_thm"] 143 144val FINITE_FV = store_thm( 145 "FINITE_FV", 146 ``FINITE (FV t)``, 147 SRW_TAC [][FV_def]); 148val _ = export_rewrites ["FINITE_FV"] 149 150val constfree_SUB = prove( 151 ``!t. constfree t /\ constfree u ==> constfree (nc$SUB u x t)``, 152 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `x INSERT nc$FV u` THEN 153 SRW_TAC [][SUB_THM, SUB_VAR]); 154val _ = augment_srw_ss [rewrites [constfree_SUB]] 155 156val SUB_def = Define`[N/v] M = to_term (nc$SUB (from_term N) v (from_term M))`; 157 158val SUB_THM = store_thm( 159 "SUB_THM", 160 ``([u/x] (VAR x) = u) /\ 161 (~(x = y) ==> ([u/x] (VAR y) = VAR y)) /\ 162 ([u/x] (s @@ t) = [u/x]s @@ [u/x] t) /\ 163 ([u/x] (LAM x t) = LAM x t) /\ 164 (~(x = y) /\ ~(y IN FV u) ==> ([u/x] (LAM y t) = LAM y ([u/x] t)))``, 165 SRW_TAC [][FV_def, SUB_def, LAM_def, VAR_def, APP_def, 166 fromto_inverse, ncTheory.SUB_THM]); 167 168val SUB_VAR = store_thm( 169 "SUB_VAR", 170 ``[t/y] (VAR x) = if x = y then t else VAR x``, 171 SRW_TAC [][VAR_def, SUB_def, fromto_inverse, SUB_VAR]); 172 173val tpm_NIL = store_thm( 174 "tpm_NIL", 175 ``!t. tpm [] t = t``, 176 HO_MATCH_MP_TAC simple_induction THEN 177 SRW_TAC [][]); 178val _ = export_rewrites ["tpm_NIL"] 179 180val LAM_eq_thm = store_thm( 181 "LAM_eq_thm", 182 ``(LAM u M = LAM v N) = ((u = v) /\ (M = N)) \/ 183 (~(u = v) /\ ~(u IN FV N) /\ (M = tpm [(u,v)] N))``, 184 SRW_TAC [][LAM_def, FV_def, tpm_def, EQ_IMP_THM] THENL [ 185 POP_ASSUM (MP_TAC o AP_TERM ``from_term``) THEN 186 SRW_TAC [][fromto_inverse, LAM_INJ_swap] THENL [ 187 Cases_on `u = v` THEN FULL_SIMP_TAC (srw_ss()) [lswap_def] THEN 188 FIRST_X_ASSUM (MP_TAC o AP_TERM ``to_term``) THEN SRW_TAC [][], 189 FULL_SIMP_TAC (srw_ss()) [from_term_11] 190 ], 191 AP_TERM_TAC THEN SRW_TAC [][fromto_inverse, LAM_INJ_swap, 192 lswap_def] 193 ]); 194 195val FV_tpm = store_thm( 196 "FV_tpm", 197 ``!t pi v. v IN FV (tpm pi t) = raw_lswapstr (REVERSE pi) v IN FV t``, 198 HO_MATCH_MP_TAC simple_induction THEN 199 SRW_TAC [][basic_swapTheory.raw_lswapstr_eql]); 200val _ = export_rewrites ["FV_tpm"] 201 202val tpm_inverse = store_thm( 203 "tpm_inverse", 204 ``!t pi. (tpm pi (tpm (REVERSE pi) t) = t) /\ 205 (tpm (REVERSE pi) (tpm pi t) = t)``, 206 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 207val _ = export_rewrites ["tpm_inverse"] 208 209val tpm_eqr = store_thm( 210 "tpm_eqr", 211 ``(t = tpm pi u) = (tpm (REVERSE pi) t = u)``, 212 METIS_TAC [tpm_inverse]); 213 214val tpm_eql = store_thm( 215 "tpm_eql", 216 ``(tpm pi t = u) = (t = tpm (REVERSE pi) u)``, 217 METIS_TAC [tpm_inverse]); 218 219val tpm_flip_args = store_thm( 220 "tpm_flip_args", 221 ``!t. tpm ((y,x)::rest) t = tpm ((x,y)::rest) t``, 222 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 223 224val tpm_APPEND = store_thm( 225 "tpm_APPEND", 226 ``!t. tpm (p1 ++ p2) t = tpm p1 (tpm p2 t)``, 227 HO_MATCH_MP_TAC simple_induction THEN 228 SRW_TAC [][basic_swapTheory.raw_lswapstr_APPEND]); 229 230val tpm_CONS = store_thm( 231 "tpm_CONS", 232 ``tpm ((x,y)::pi) t = tpm [(x,y)] (tpm pi t)``, 233 SRW_TAC [][GSYM tpm_APPEND]); 234 235val tpm_sing_inv = store_thm( 236 "tpm_sing_inv", 237 ``tpm [h] (tpm [h] t) = t``, 238 ACCEPT_TAC 239 (SIMP_RULE list_ss [] (Q.INST [`pi` |-> `[h]`] (SPEC_ALL tpm_inverse)))) 240val _ = export_rewrites ["tpm_sing_inv"] 241 242val nc_INDUCTION2 = store_thm( 243 "nc_INDUCTION2", 244 ``!P X. (!x. P (VAR x)) /\ 245 (!t u. P t /\ P u ==> P (t @@ u)) /\ 246 (!y u. ~(y IN X) /\ P u ==> P (LAM y u)) /\ FINITE X ==> 247 !u. P u``, 248 REPEAT GEN_TAC THEN STRIP_TAC THEN 249 Q_TAC SUFF_TAC `!u pi. P (tpm pi u)` THEN1 METIS_TAC [tpm_NIL] THEN 250 HO_MATCH_MP_TAC simple_induction THEN 251 SRW_TAC [][] THEN 252 Q_TAC (NEW_TAC "z") `raw_lswapstr pi v INSERT FV (tpm pi u) UNION X` THEN 253 Q_TAC SUFF_TAC `LAM (raw_lswapstr pi v) (tpm pi u) = 254 LAM z (tpm ((z,raw_lswapstr pi v)::pi) u)` 255 THEN1 SRW_TAC [][] THEN 256 SRW_TAC [][LAM_eq_thm, basic_swapTheory.raw_lswapstr_APPEND] THENL [ 257 FULL_SIMP_TAC (srw_ss()) [], 258 SRW_TAC [][tpm_eqr, tpm_flip_args, tpm_APPEND] 259 ]); 260 261val tpm_sing_to_back = store_thm( 262 "tpm_sing_to_back", 263 ``!t. tpm [(raw_lswapstr p u, raw_lswapstr p v)] (tpm p t) = tpm p (tpm [(u,v)] t)``, 264 HO_MATCH_MP_TAC simple_induction THEN 265 SRW_TAC [][basic_swapTheory.raw_lswapstr_sing_to_back]); 266 267val tpm_subst = store_thm( 268 "tpm_subst", 269 ``!N. tpm pi ([M/v] N) = [tpm pi M/raw_lswapstr pi v] (tpm pi N)``, 270 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 271 Q.EXISTS_TAC `v INSERT FV M` THEN 272 SRW_TAC [][SUB_THM, SUB_VAR]); 273 274val tpm_subst_out = store_thm( 275 "tpm_subst_out", 276 ``[M/v] (tpm pi N) = 277 tpm pi ([tpm (REVERSE pi) M/raw_lswapstr (REVERSE pi) v] N)``, 278 SRW_TAC [][tpm_subst]) 279 280val tpm_idfront = store_thm( 281 "tpm_idfront", 282 ``!t. tpm ((v,v)::rest) t = tpm rest t``, 283 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 284val _ = export_rewrites ["tpm_idfront"] 285 286val tpm_fresh = store_thm( 287 "tpm_fresh", 288 ``!t. ~(x IN FV t) /\ ~(y IN FV t) ==> (tpm [(x,y)] t = t)``, 289 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THEN 290 SRW_TAC [][] THEN SRW_TAC [CONJ_ss][LAM_eq_thm, tpm_flip_args] THEN 291 Cases_on `x = v` THEN SRW_TAC [][] THEN 292 Cases_on `y = v` THEN SRW_TAC [][] THEN 293 FULL_SIMP_TAC (srw_ss()) [tpm_flip_args]); 294 295val tpm_apart = store_thm( 296 "tpm_apart", 297 ``!t. x IN FV t /\ ~(y IN FV t) ==> ~(tpm [(x,y)] t = t)``, 298 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THENL [ 299 METIS_TAC [], 300 METIS_TAC [], 301 SRW_TAC [][LAM_eq_thm] THEN 302 Cases_on `y = v` THEN SRW_TAC [][], 303 SRW_TAC [][LAM_eq_thm] 304 ]); 305 306val fresh_tpm_subst = store_thm( 307 "fresh_tpm_subst", 308 ``!M. ~(u IN FV M) ==> (tpm [(u,v)] M = [VAR u/v] M)``, 309 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 310 SRW_TAC [][SUB_THM, SUB_VAR]); 311 312val SIMPLE_ALPHA = store_thm( 313 "SIMPLE_ALPHA", 314 ``~(y IN FV u) ==> !x. LAM x u = LAM y ([VAR y/x] u)``, 315 SRW_TAC [][GSYM fresh_tpm_subst] THEN 316 SRW_TAC [CONJ_ss][LAM_eq_thm, tpm_flip_args]); 317 318val tpm_ALPHA = store_thm( 319 "tpm_ALPHA", 320 ``~(v IN FV u) ==> !x. LAM x u = LAM v (tpm [(v,x)] u)``, 321 SRW_TAC [][fresh_tpm_subst, SIMPLE_ALPHA]); 322 323val lemma14a = store_thm( 324 "lemma14a", 325 ``!t. [VAR v/v] t = t``, 326 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{v}` THEN 327 SRW_TAC [][SUB_THM, SUB_VAR]); 328val _ = export_rewrites ["lemma14a"] 329 330val lemma14b = store_thm( 331 "lemma14b", 332 ``!M. ~(v IN FV M) ==> ([N/v] M = M)``, 333 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `v INSERT FV N` THEN 334 SRW_TAC [][SUB_THM, SUB_VAR]); 335 336open pred_setTheory 337 338val lemma14c = store_thm( 339 "lemma14c", 340 ``!t x u. x IN FV u ==> (FV ([t/x]u) = FV t UNION (FV u DELETE x))``, 341 NTAC 2 GEN_TAC THEN HO_MATCH_MP_TAC nc_INDUCTION2 THEN 342 Q.EXISTS_TAC `x INSERT FV t` THEN 343 SRW_TAC [][SUB_THM, SUB_VAR, EXTENSION] THENL [ 344 Cases_on `x IN FV u'` THEN SRW_TAC [][lemma14b] THEN METIS_TAC [], 345 Cases_on `x IN FV u` THEN SRW_TAC [][lemma14b] THEN METIS_TAC [], 346 METIS_TAC [] 347 ]); 348 349val lemma15a = store_thm( 350 "lemma15a", 351 ``!M. ~(v IN FV M) ==> ([N/v]([VAR v/x]M) = [N/x]M)``, 352 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;v} UNION FV N` THEN 353 SRW_TAC [][SUB_THM, SUB_VAR]); 354 355val lemma15b = store_thm( 356 "lemma15b", 357 ``~(v IN FV M) ==> ([VAR u/v]([VAR v/u] M) = M)``, 358 SRW_TAC [][lemma15a]); 359 360val FV_SUB = store_thm( 361 "FV_SUB", 362 ``!t u v. FV ([t/v] u) = if v IN FV u then FV t UNION (FV u DELETE v) 363 else FV u``, 364 PROVE_TAC [lemma14b, lemma14c]); 365 366(* ---------------------------------------------------------------------- 367 iterated substitutions (ugh) 368 ---------------------------------------------------------------------- *) 369 370val ISUB_def = 371 Define 372 `($ISUB t [] = t) 373 /\ ($ISUB t ((s,x)::rst) = $ISUB ([s/x]t) rst)`; 374 375val _ = set_fixity "ISUB" (Infixr 501); 376 377val DOM_DEF = 378 Define 379 `(DOM [] = {}) 380 /\ (DOM ((x,y)::rst) = {y} UNION DOM rst)`; 381 382val FVS_DEF = 383 Define 384 `(FVS [] = {}) 385 /\ (FVS ((t,x)::rst) = FV t UNION FVS rst)`; 386 387 388val FINITE_DOM = Q.store_thm("FINITE_DOM", 389 `!ss. FINITE (DOM ss)`, 390Induct THENL [ALL_TAC, Cases] 391 THEN RW_TAC std_ss [DOM_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_SING]); 392val _ = export_rewrites ["FINITE_DOM"] 393 394 395val FINITE_FVS = Q.store_thm("FINITE_FVS", 396`!ss. FINITE (FVS ss)`, 397Induct THENL [ALL_TAC, Cases] 398 THEN RW_TAC std_ss [FVS_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_FV]); 399val _ = export_rewrites ["FINITE_FVS"] 400 401val ISUB_LAM = store_thm( 402 "ISUB_LAM", 403 ``!R x. ~(x IN (DOM R UNION FVS R)) ==> 404 !t. (LAM x t) ISUB R = LAM x (t ISUB R)``, 405 Induct THEN 406 ASM_SIMP_TAC (srw_ss()) [ISUB_def, pairTheory.FORALL_PROD, 407 DOM_DEF, FVS_DEF, SUB_THM]); 408 409(* ---------------------------------------------------------------------- 410 size of a term 411 ---------------------------------------------------------------------- *) 412 413val size_def = Define`size t = nc$size (from_term t)`; 414 415val size_thm = store_thm( 416 "size_thm", 417 ``(size (VAR s) = 1) /\ 418 (size (t @@ u) = size t + size u + 1) /\ 419 (size (LAM v t) = size t + 1)``, 420 SRW_TAC [][size_def, ncTheory.size_thm, fromto_inverse, VAR_def, APP_def, 421 LAM_def]); 422val _ = export_rewrites ["size_thm"] 423 424val size_tpm = store_thm( 425 "size_tpm", 426 ``!t. size (tpm pi t) = size t``, 427 HO_MATCH_MP_TAC simple_induction THEN 428 SRW_TAC [][]); 429val _ = export_rewrites ["size_tpm"] 430 431val size_vsubst = store_thm( 432 "size_vsubst", 433 ``!t. size ([VAR v/u] t) = size t``, 434 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 435 SRW_TAC [][SUB_THM, SUB_VAR]); 436val _ = export_rewrites ["size_vsubst"] 437 438(* ---------------------------------------------------------------------- 439 proving a recursion theorem 440 ---------------------------------------------------------------------- *) 441val gm_recursion = prove( 442 ``!var app lam. 443 ?hom : term -> 'b. 444 (!s. hom (VAR s) = var s) /\ 445 (!t u. hom (t @@ u) = app (hom t) (hom u) t u) /\ 446 !v t. hom (LAM v t) = lam (\y. hom ([VAR y/v] t)) 447 (\y. [VAR y/v] t)``, 448 REPEAT GEN_TAC THEN 449 Q.SPECL_THEN [`\k. ARB`, `var`, 450 `\rt ru t u. app rt ru (to_term t) (to_term u)`, 451 `\rf tf. lam rf (to_term o tf)`] MP_TAC 452 (INST_TYPE [alpha |-> ``:one``] nc_RECURSION) THEN 453 DISCH_THEN (STRIP_ASSUME_TAC o CONJUNCT1 o CONV_RULE EXISTS_UNIQUE_CONV) THEN 454 Q.EXISTS_TAC `hom o from_term` THEN 455 SRW_TAC [][VAR_def, APP_def, LAM_def, fromto_inverse, 456 combinTheory.o_ABS_R, SUB_def]); 457 458val ABS_def = Define`ABS f = to_term (nc$ABS (from_term o f))` 459 460val ABS_axiom = prove( 461 ``gmterm$ABS (\y. [VAR y/v] t) = LAM v t``, 462 SRW_TAC [][LAM_def, ABS_def, SUB_def, combinTheory.o_ABS_R, 463 fromto_inverse, VAR_def, ncTheory.ABS_DEF]); 464 465 466val fresh_new_subst0 = prove( 467 ``FINITE X ==> 468 ((let v = NEW (FV (LAM x u) UNION X) in f v ([VAR v/x] u)) = 469 (let v = NEW (FV (LAM x u) UNION X) in f v (tpm [(v,x)] u)))``, 470 STRIP_TAC THEN NEW_ELIM_TAC THEN REPEAT STRIP_TAC THEN 471 SRW_TAC [][] THEN SRW_TAC [][fresh_tpm_subst]); 472 473val lemma = (SIMP_RULE bool_ss [ABS_axiom, fresh_new_subst0, 474 ASSUME ``FINITE (X:string set)``]o 475 Q.INST [`lam'` |-> `lam`] o 476 Q.INST [`lam` |-> 477 `\r t. let v = NEW (FV (gmterm$ABS t) UNION X) 478 in 479 lam' (r v) v (t v)`] o 480 INST_TYPE [beta |-> alpha] o 481 SPEC_ALL) gm_recursion 482 483val term_CASES = store_thm( 484 "term_CASES", 485 ``!t. (?s. t = VAR s) \/ (?t1 t2. t = t1 @@ t2) \/ 486 (?v t0. t = LAM v t0)``, 487 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THEN METIS_TAC []); 488 489val pvh_induction = prove( 490 ``!P. (!s. P (VAR s)) /\ (!t u. P t /\ P u ==> P (t @@ u)) /\ 491 (!v t. (!t'. (size t' = size t) ==> P t') ==> P (LAM v t)) ==> 492 !t. P t``, 493 REPEAT STRIP_TAC THEN measureInduct_on `size t` THEN 494 Q.SPEC_THEN `t` FULL_STRUCT_CASES_TAC term_CASES THEN 495 FULL_SIMP_TAC (srw_ss()) [] THEN 496 POP_ASSUM (fn th => FIRST_X_ASSUM MATCH_MP_TAC THEN ASSUME_TAC th) THEN 497 REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 498 SRW_TAC [numSimps.ARITH_ss][]); 499 500val swap_RECURSION = store_thm( 501 "swap_RECURSION", 502 ``swapping rswap rFV /\ FINITE X /\ 503 (!s. rFV (var s) SUBSET s INSERT X) /\ 504 (!t' u' t u. 505 rFV t' SUBSET FV t UNION X /\ rFV u' SUBSET FV u UNION X ==> 506 rFV (app t' u' t u) SUBSET FV t UNION FV u UNION X) /\ 507 (!t' v t. 508 rFV t' SUBSET FV t UNION X ==> 509 rFV (lam t' v t) SUBSET FV t DELETE v UNION X) /\ 510 (!s x y. 511 ~(x IN X) /\ ~(y IN X) ==> 512 (rswap x y (var s) = var (swapstr x y s))) /\ 513 (!t t' u u' x y. 514 ~(x IN X) /\ ~(y IN X) ==> 515 (rswap x y (app t' u' t u) = 516 app (rswap x y t') (rswap x y u') (tpm [(x,y)] t) (tpm [(x,y)] u))) /\ 517 (!t' t x y v. 518 ~(x IN X) /\ ~(y IN X) ==> 519 (rswap x y (lam t' v t) = 520 lam (rswap x y t') (swapstr x y v) (tpm[(x,y)] t))) ==> 521 ?hom. 522 ((!s. hom (VAR s) = var s) /\ 523 (!t u. hom (t @@ u) = app (hom t) (hom u) t u) /\ 524 !v t. ~(v IN X) ==> (hom (LAM v t) = lam (hom t) v t)) /\ 525 (!t x y. 526 ~(x IN X) /\ ~(y IN X) ==> 527 (hom (tpm [(x,y)] t) = rswap x y (hom t)))``, 528 REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC lemma THEN 529 Q.EXISTS_TAC `hom` THEN ASM_SIMP_TAC bool_ss [] THEN 530 `!t. rFV (hom t) SUBSET FV t UNION X` 531 by (HO_MATCH_MP_TAC pvh_induction THEN ASM_SIMP_TAC (srw_ss()) [] THEN 532 REPEAT CONJ_TAC THENL [ 533 ASM_SIMP_TAC (srw_ss()) [INSERT_UNION_EQ], 534 REPEAT STRIP_TAC THEN NEW_ELIM_TAC THEN 535 ASM_SIMP_TAC (srw_ss()) [] THEN Q.X_GEN_TAC `u` THEN 536 REPEAT STRIP_TAC THENL [ 537 SRW_TAC [][LET_THM] THEN 538 `FV t DELETE v = FV (LAM v t)` by SRW_TAC [][] THEN 539 POP_ASSUM SUBST_ALL_TAC THEN 540 `LAM v t = LAM u (tpm [(u,v)] t)` by SRW_TAC [][tpm_ALPHA] THEN 541 POP_ASSUM SUBST1_TAC THEN SRW_TAC [][], 542 SRW_TAC [][LET_THM] 543 ] 544 ]) THEN 545 ASM_REWRITE_TAC [] THEN 546 `!x r. rswap x x r = r` by FULL_SIMP_TAC (srw_ss()) [swapping_def] THEN 547 `!t x y. ~(x IN X) /\ ~(y IN X) ==> 548 (hom (tpm [(x,y)] t) = rswap x y (hom t))` 549 by (HO_MATCH_MP_TAC pvh_induction THEN REPEAT CONJ_TAC THEN 550 TRY (SRW_TAC [][] THEN NO_TAC) THEN 551 REPEAT STRIP_TAC THEN 552 Cases_on `x = y` THEN1 SRW_TAC [][] THEN 553 Q_TAC (NEW_TAC "z") `{x;y;v} UNION FV t UNION X` THEN 554 `LAM v t = LAM z ([VAR z/v] t)` by SRW_TAC [][SIMPLE_ALPHA] THEN 555 Q.ABBREV_TAC `M = [VAR z/v] t` THEN 556 `size t = size M` by SRW_TAC [][Abbr`M`] THEN 557 Q.RM_ABBREV_TAC `M` THEN 558 NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN 559 `hom (tpm [(x,y)] (LAM z M)) = rswap x y (lam (hom M) z M)` 560 by (SRW_TAC [][LET_THM] THEN 561 NEW_ELIM_TAC THEN ASM_SIMP_TAC bool_ss [] THEN 562 Q.X_GEN_TAC `a` THEN 563 REVERSE (SRW_TAC [][]) THEN1 SRW_TAC [][] THEN 564 Q.MATCH_ABBREV_TAC 565 `lam (rswap a z Y) a (tpm [(a,z)] M') = R` THEN 566 Q.UNABBREV_TAC `R` THEN 567 `lam (rswap a z Y) a (tpm [(a,z)] M') = 568 lam (rswap a z Y) (swapstr a z z) (tpm [(a,z)] M')` 569 by SRW_TAC [][] THEN 570 ` _ = rswap a z (lam Y z M')` 571 by POP_ASSUM (fn th => SRW_TAC [][] THEN ASSUME_TAC th) THEN 572 POP_ASSUM SUBST1_TAC THEN 573 MATCH_MP_TAC swapping_implies_identity_swap THEN 574 Q.EXISTS_TAC `rFV` THEN ASM_REWRITE_TAC [] THEN 575 `rFV (lam Y z M') SUBSET FV M' DELETE z UNION X` 576 by (FIRST_ASSUM MATCH_MP_TAC THEN 577 FULL_SIMP_TAC (srw_ss()) 578 [SUBSET_DEF, Abbr`Y`, Abbr`M'`, 579 swapping_def]) THEN 580 Q_TAC SUFF_TAC `~(a IN FV M' DELETE z UNION X) /\ 581 ~(z IN FV M' DELETE z UNION X)` 582 THEN1 METIS_TAC [SUBSET_DEF] THEN 583 SRW_TAC [][Abbr`M'`]) THEN 584 POP_ASSUM SUBST_ALL_TAC THEN REPEAT AP_TERM_TAC THEN 585 ASM_SIMP_TAC bool_ss [] THEN NEW_ELIM_TAC THEN 586 ASM_REWRITE_TAC [] THEN Q.X_GEN_TAC `a` THEN 587 REVERSE (SRW_TAC [][]) THEN1 SRW_TAC [][] THEN 588 MATCH_MP_TAC EQ_TRANS THEN 589 Q.EXISTS_TAC `rswap a z (lam (hom M) z M)` THEN CONJ_TAC THENL [ 590 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN 591 MATCH_MP_TAC swapping_implies_identity_swap THEN 592 Q.EXISTS_TAC `rFV` THEN ASM_REWRITE_TAC [] THEN 593 `rFV (lam (hom M) z M) SUBSET FV (LAM z M) UNION X` 594 by SRW_TAC [][] THEN 595 POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN 596 METIS_TAC [], 597 SRW_TAC [][] 598 ]) THEN 599 ASM_SIMP_TAC bool_ss [] THEN SRW_TAC [][LET_THM] THEN 600 NEW_ELIM_TAC THEN ASM_SIMP_TAC bool_ss [] THEN 601 Q.X_GEN_TAC `u` THEN STRIP_TAC THENL [ 602 `lam (rswap u v (hom t)) u (tpm [(u,v)] t) = rswap u v (lam (hom t) v t)` 603 by SRW_TAC [][] THEN 604 POP_ASSUM SUBST_ALL_TAC THEN 605 MATCH_MP_TAC swapping_implies_identity_swap THEN 606 Q.EXISTS_TAC `rFV` THEN ASM_REWRITE_TAC [] THEN 607 `rFV (lam (hom t) v t) SUBSET FV (LAM v t) UNION X` 608 by SRW_TAC [][] THEN 609 POP_ASSUM MP_TAC THEN REWRITE_TAC [SUBSET_DEF] THEN SRW_TAC [][] THEN 610 METIS_TAC [], 611 SRW_TAC [][] 612 ]); 613 614val term_swapping = store_thm( 615 "term_swapping", 616 ``swapping (\x y t. tpm [(x,y)] t) FV``, 617 SRW_TAC [][swapping_def, tpm_fresh]); 618val _ = export_rewrites ["term_swapping"] 619 620val lam_rFV = prove( 621 ``(!t' v t. rFV (lam t' v t) SUBSET ((rFV t' UNION FV t) DELETE v) UNION X) 622 ==> 623 !t' v t. rFV t' SUBSET FV t UNION X ==> 624 rFV (lam t' v t) SUBSET (FV t DELETE v) UNION X``, 625 SRW_TAC [][] THEN 626 FIRST_X_ASSUM (Q.SPECL_THEN [`t'`, `v`, `t`] ASSUME_TAC) THEN 627 REPEAT (POP_ASSUM MP_TAC) THEN 628 SRW_TAC [][SUBSET_DEF] THEN METIS_TAC []) 629val app_rFV = prove( 630 ``(!t' u' t u. rFV (app t' u' t u) SUBSET 631 rFV t' UNION rFV u' UNION FV t UNION FV u UNION X) ==> 632 !t' u' t u. 633 rFV t' SUBSET FV t UNION X /\ rFV u' SUBSET FV u UNION X ==> 634 rFV (app t' u' t u) SUBSET FV t UNION FV u UNION X``, 635 SRW_TAC [][] THEN 636 FIRST_X_ASSUM (Q.SPECL_THEN [`t'`, `u'`, `t`, `u`] MP_TAC) THEN 637 REPEAT (POP_ASSUM MP_TAC) THEN 638 SRW_TAC [][SUBSET_DEF] THEN METIS_TAC []); 639 640val swap_RECURSION_improved = save_thm( 641 "swap_RECURSION_improved", 642 REWRITE_RULE [AND_IMP_INTRO] 643 (DISCH_ALL (REWRITE_RULE [UNDISCH lam_rFV, UNDISCH app_rFV] 644 swap_RECURSION))) 645 646val swap_RECURSION_nosideset = save_thm( 647 "swap_RECURSION_nosideset", 648 SIMP_RULE (srw_ss()) [] (Q.INST [`X` |-> `{}`] swap_RECURSION_improved)) 649 650 651val _ = export_theory(); 652