1(*--------------------------------------------------------------------------- 2 Five Axioms of Alpha Conversion 3 (Andy Gordon & Tom Melham) 4 5 6 Part I: deBruijn terms 7 8 ---------------------------------------------------------------------------*) 9 10(* Interactive use: 11 app load ["bossLib", "Q", "pred_setTheory", "stringTheory"]; 12*) 13 14open HolKernel Parse boolLib 15 bossLib numLib IndDefLib 16 pred_setTheory arithmeticTheory 17 basic_swapTheory 18 19val _ = new_theory"dB"; 20 21 22(*--------------------------------------------------------------------------- 23 Support bumpf. 24 ---------------------------------------------------------------------------*) 25 26val FUN_EQ_TAC = CONV_TAC (ONCE_DEPTH_CONV FUN_EQ_CONV) 27 THEN GEN_TAC THEN BETA_TAC; 28 29val MAX_00 = Q.prove( 30 `!m n. (MAX m n = 0) = (m=0) /\ (n=0)`, RW_TAC arith_ss [MAX_DEF]); 31 32val MAX_LESS_EQ = Q.prove( 33 `!m n p. MAX m n <= p = m <= p /\ n <= p`, RW_TAC arith_ss [MAX_DEF]); 34 35 36val UNION_DELETE = Q.store_thm("UNION_DELETE", 37 `!s t x. (s UNION t) DELETE x = (s DELETE x) UNION (t DELETE x)`, 38ZAP_TAC 39 (std_ss && [EXTENSION,IN_UNION,IN_DELETE]) []); 40 41val UNION_SUBSET = Q.prove( 42 `!X Y Z. (X UNION Y) SUBSET Z = X SUBSET Z /\ Y SUBSET Z`, 43PROVE_TAC 44 [SUBSET_DEF, IN_UNION]); 45 46val GSPEC_DEF = Q.prove 47(`!f. GSPEC f = \v. ?z. f z = (v,T)`, 48 FUN_EQ_TAC 49 THEN ONCE_REWRITE_TAC 50 [BETA_RULE (ONCE_REWRITE_CONV 51 [GSYM SPECIFICATION](Term`(\x. GSPEC f x) x`))] 52 THEN CONV_TAC (ONCE_DEPTH_CONV ETA_CONV) 53 THEN PROVE_TAC [GSPECIFICATION]); 54 55(* ===================================================================== *) 56(* PART I: A type of de Bruijn terms. *) 57(* ===================================================================== *) 58 59val _ = Hol_datatype 60 `dB = dCON of 'a 61 | dVAR of string 62 | dBOUND of num 63 | dABS of dB 64 | dAPP of dB => dB`; 65 66 67(* --------------------------------------------------------------------- *) 68(* Free variables. *) 69(* --------------------------------------------------------------------- *) 70 71val dFV = 72 Define 73 `(dFV (dCON c) = {}) 74 /\ (dFV (dVAR x) = {x}) 75 /\ (dFV (dBOUND n) = {}) 76 /\ (dFV (dABS t) = dFV t) 77 /\ (dFV (dAPP t u) = (dFV t) UNION (dFV u))`; 78 79 80val FINITE_dFV = Q.store_thm("FINITE_dFV", `!t. FINITE (dFV t)`, 81Induct THEN RW_TAC std_ss [dFV, FINITE_UNION, FINITE_EMPTY, FINITE_SING]); 82 83val FRESH_VAR = Q.store_thm("FRESH_VAR", `!t. ?x. ~(x IN dFV t)`, 84 PROVE_TAC [new_exists, SPEC_ALL FINITE_dFV]); 85 86(* --------------------------------------------------------------------- *) 87(* Functions defined by recursion on de Bruijn terms. *) 88(* --------------------------------------------------------------------- *) 89 90val dDEG = 91 Define 92 `(dDEG (dCON c) = 0) 93 /\ (dDEG (dVAR x) = 0) 94 /\ (dDEG (dBOUND n) = SUC n) 95 /\ (dDEG (dABS t) = dDEG t - 1) 96 /\ (dDEG (dAPP t u) = MAX (dDEG t) (dDEG u))`; 97 98 99val Abst = 100 Define 101 `(Abst i x (dCON c) = dCON c) 102 /\ (Abst i x (dVAR y) = if x=y then dBOUND i else dVAR y) 103 /\ (Abst i x (dBOUND j) = dBOUND j) 104 /\ (Abst i x (dABS t) = dABS (Abst (SUC i) x t)) 105 /\ (Abst i x (dAPP t u) = dAPP (Abst i x t) (Abst i x u))`; 106 107val Inst = 108 Define 109 `(Inst i (dCON c) u = dCON c) 110 /\ (Inst i (dVAR x) u = dVAR x) 111 /\ (Inst i (dBOUND j) u = if i=j then u else dBOUND j) 112 /\ (Inst i (dABS t) u = dABS (Inst (SUC i) t u)) 113 /\ (Inst i (dAPP t1 t2) u = dAPP (Inst i t1 u) (Inst i t2 u))`; 114 115 116val dFV_Abst = Q.store_thm("dFV_Abst", 117`!t i x. ~(x IN dFV t) ==> (Abst i x t = t)`, 118Induct 119 THEN RW_TAC std_ss [Abst, dFV, IN_UNION, IN_SING]); 120 121val dDEG_Abst = Q.store_thm("dDEG_Abst", 122`!t x i. dDEG t <= i ==> dDEG (Abst i x t) <= (SUC i)`, 123Induct 124 THEN RW_TAC arith_ss [dDEG, Abst, MAX_LESS_EQ, GSYM ADD1]); 125 126 127val dDEG_Inst = Q.store_thm("dDEG_Inst", 128`!t i x. dDEG t <= SUC i ==> dDEG (Inst i t (dVAR x)) <= i`, 129Induct 130 THEN RW_TAC arith_ss [Inst, dDEG, MAX_LESS_EQ, GSYM ADD1]); 131 132 133val dDEG_Inst_Abst = Q.store_thm("dDEG_Inst_Abst", 134`!t i x. dDEG t <= i ==> (Inst i (Abst i x t) (dVAR x) = t)`, 135Induct 136 THEN RW_TAC arith_ss [Inst, Abst, dDEG, MAX_LESS_EQ]); 137 138 139val dDEG_Abst_Inst = Q.store_thm("dDEG_Abst_Inst", 140`!t i x. 141 ~(x IN dFV t) /\ dDEG t <= SUC i ==> (Abst i x (Inst i t (dVAR x)) = t)`, 142Induct 143 THEN RW_TAC arith_ss 144 [Inst, Abst, dFV, dDEG, MAX_LESS_EQ, IN_UNION, IN_SING]); 145 146val Rename = Q.store_thm("Rename", 147`!t i x y. 148 ~(y IN (dFV t)) /\ dDEG t <= i 149 ==> 150 (Abst i x t = Abst i y (Inst i (Abst i x t) (dVAR y)))`, 151Induct 152 THEN ZAP_TAC (arith_ss && 153 [Inst, Abst, dFV, dDEG, IN_UNION, MAX_LESS_EQ, IN_SING, GSYM ADD1]) []); 154 155 156(* --------------------------------------------------------------------- *) 157(* Lambda-abstraction. *) 158(* --------------------------------------------------------------------- *) 159 160val dLAMBDA = Define `dLAMBDA x t = dABS(Abst 0 x t)`; 161 162val dFV_dLAMBDA_lemma = Q.store_thm("dFV_dLAMBDA_lemma", 163`!t i x. dFV (Abst i x t) = (dFV t) DELETE x`, 164Induct 165 THEN ZAP_TAC (std_ss && [Abst,dFV,UNION_DELETE,EMPTY_DELETE,SING_DELETE]) 166 [DELETE_NON_ELEMENT, IN_SING]); 167 168val dFV_dLAMBDA = Q.store_thm("dFV_dLAMBDA", 169`!t x. dFV (dLAMBDA x t) = (dFV t) DELETE x`, 170RW_TAC std_ss [dFV, dLAMBDA, dFV_dLAMBDA_lemma]); 171 172 173(* --------------------------------------------------------------------- *) 174(* Inductive definition of proper terms. *) 175(* --------------------------------------------------------------------- *) 176 177val (dOK_DEF, dOK_ind, dOK_cases) = Hol_reln 178 `(!x. dOK (dVAR x)) /\ 179 (!x. dOK (dCON x)) /\ 180 (!x t. dOK t ==> dOK (dLAMBDA x t)) /\ 181 (!t u. dOK t /\ dOK u ==> dOK (dAPP t u))`; 182 183val _ = save_thm("dOK_DEF", dOK_DEF); 184val _ = save_thm("dOK_ind", dOK_ind); 185 186 187(* --------------------------------------------------------------------- *) 188(* Proof of |- !t. dOK t = (dDEG t = 0) *) 189(* --------------------------------------------------------------------- *) 190 191val Forwards = Q.store_thm("Forwards", 192 `!t. dOK t ==> (dDEG t = 0)`, 193 HO_MATCH_MP_TAC dOK_ind THEN 194 RW_TAC bool_ss [ONE, dDEG, MAX_00, dLAMBDA,SUB_EQ_0] THEN 195 MATCH_MP_TAC dDEG_Abst THEN ASM_SIMP_TAC arith_ss []); 196 197 198val dWT = 199 Define 200 `(dWT (dCON c) = 0) 201 /\ (dWT (dVAR x) = 0) 202 /\ (dWT (dBOUND n) = 0) 203 /\ (dWT (dABS t) = SUC (dWT t)) 204 /\ (dWT (dAPP t u) = SUC (dWT t + dWT u))`; 205 206val dWT_Inst = Q.store_thm("dWT_Inst", 207 `!t i x. dWT (Inst i t (dVAR x)) = dWT t`, 208Induct 209 THEN RW_TAC arith_ss [dWT, Inst]); 210 211val dDEG_dABS_dLAMBDA = Q.store_thm("dDEG_dABS_dLAMBDA", 212`!t. (dDEG t <= 1) ==> 213 ?x u. 214 (dABS t = dLAMBDA x u) /\ 215 dWT u < dWT (dABS t) /\ 216 (dDEG u = 0)`, 217RW_TAC arith_ss [dLAMBDA] 218 THEN Q.X_CHOOSE_TAC `x` (Q.SPEC `t:'a dB` FRESH_VAR) 219 THEN ID_EX_TAC THEN Q.EXISTS_TAC `Inst 0 t (dVAR x)` 220 THEN RW_TAC arith_ss [dWT,dWT_Inst,dDEG_Inst,dDEG_Abst_Inst,GSYM LESS_EQ_0]); 221 222val Backwards = Q.store_thm("Backwards", 223`!n t. (dDEG t = 0) /\ (dWT t = n) ==> dOK t`, 224completeInduct_on `n` THEN Cases 225 THEN ONCE_REWRITE_TAC [dOK_cases] 226 THEN ZAP_TAC (arith_ss && [dDEG,dWT,MAX_00]) [dDEG_dABS_dLAMBDA,dWT]); 227 228val dDEG_dOK = Q.store_thm("dDEG_dOK", `!t. dOK t = (dDEG t = 0)`, 229PROVE_TAC [Forwards,Backwards]); 230 231 232(* --------------------------------------------------------------------- *) 233(* Substitution. *) 234(* --------------------------------------------------------------------- *) 235 236val dSUB = Define `dSUB x u t = Inst 0 (Abst 0 x t) u`; 237 238val _ = add_rule {term_name = "dSUB", fixity = Parse.Closefix, 239 pp_elements = [TOK "[", TM, HardSpace 1, TOK "|->", 240 BreakSpace(1,0), TM, TOK "]"], 241 paren_style = OnlyIfNecessary, 242 block_style = (AroundEachPhrase, (PP.CONSISTENT, 2))}; 243 244 245(* --------------------------------------------------------------------- *) 246(* Substitution preserves propriety. *) 247(* --------------------------------------------------------------------- *) 248 249val dOK_dSUB_lemma = Q.store_thm("dOK_dSUB_lemma", 250`!t u i j x. 251 dDEG t <= i /\ dDEG u <= j ==> dDEG (Inst i (Abst i x t) u) <= i+j`, 252Induct 253 THEN ZAP_TAC (arith_ss && [Inst, Abst, dDEG, MAX_LESS_EQ, GSYM ADD1]) 254 [ADD_CLAUSES]); 255 256val dOK_dSUB = Q.store_thm("dOK_dSUB", 257 `!t u x. dOK t /\ dOK u ==> dOK ([x |-> u] t)`, 258ZAP_TAC (arith_ss && [dDEG_dOK, dSUB]) 259 [DECIDE (Term `(x=0) = x <= 0`), dOK_dSUB_lemma, ADD_CLAUSES]); 260 261 262(* --------------------------------------------------------------------- *) 263(* Distributive laws for substitution. *) 264(* --------------------------------------------------------------------- *) 265 266val EQ_dVAR_dSUB = Q.store_thm("EQ_dVAR_dSUB", 267 `!u x. [x |-> u] (dVAR x) = u`, 268RW_TAC arith_ss [dSUB, Inst, Abst]); 269 270val NEQ_dVAR_dSUB = Q.store_thm("NEQ_dVAR_dSUB", 271 `!u x y. ~(x=y) ==> ([x |-> u] (dVAR y) = dVAR y)`, 272RW_TAC arith_ss [dSUB, Inst, Abst]); 273 274val dCON_dSUB = Q.store_thm("dCON_dSUB", 275 `!x t c. [x |-> t] (dCON c) = dCON c`, 276RW_TAC arith_ss [dSUB, Inst, Abst]); 277 278val dAPP_dSUB = Q.store_thm("dAPP_dSUB", 279`!x M t u. [x |-> M] (dAPP t u) = dAPP ([x |-> M] t) ([x |-> M] u)`, 280RW_TAC arith_ss [Inst, Abst, dSUB]); 281 282val dLAMBDA_dSUB_lemma = Q.store_thm("dLAMBDA_dSUB_lemma", 283`!t u i x y. 284 ~(x=y) /\ ~(y IN dFV u) /\ dDEG t <= i 285 ==> 286 (Inst (SUC i) (Abst (SUC i) x (Abst i y t)) u = 287 Abst i y (Inst i (Abst i x t) u))`, 288Induct 289 THEN RW_TAC arith_ss [Inst, Abst, dFV_Abst, dDEG, MAX_LESS_EQ]); 290 291val dLAMBDA_dSUB = Q.store_thm("dLAMBDA_dSUB", 292 `!t u x y. 293 ~(x=y) /\ ~(y IN dFV u) /\ dOK t ==> 294 ([x |-> u] (dLAMBDA y t) = dLAMBDA y ([x |-> u] t))`, 295 SIMP_TAC (srw_ss()) [dLAMBDA, dSUB, Abst, Inst, dDEG_dOK] THEN 296 SIMP_TAC (bool_ss ++ ARITH_ss) [ONE, dLAMBDA_dSUB_lemma]); 297 298val dLAMBDA_dSUB_EQ_lemma = Q.store_thm("dLAMBDA_dSUB_EQ_lemma", 299`!t u x i. 300 dDEG t <= SUC i ==> 301 (Inst (SUC i) (Abst (SUC i) x (Abst i x t)) u = Abst i x t)`, 302Induct 303 THEN RW_TAC arith_ss [Abst, Inst, dDEG, MAX_LESS_EQ]); 304 305val dLAMBDA_dSUB_EQ = Q.store_thm("dLAMBDA_dSUB_EQ", 306 `!t u x. 307 dOK t ==> ([x |-> u] (dLAMBDA x t) = dLAMBDA x t)`, 308 RW_TAC bool_ss [dDEG_dOK, dLAMBDA, dSUB, Abst, Inst, DECIDE ``0 <= SUC x``, 309 dLAMBDA_dSUB_EQ_lemma]); 310 311val dSUB_ID_lemma = Q.store_thm("dSUB_ID_lemma", 312`!t i x. dDEG t <= i ==> (Inst i (Abst i x t) (dVAR x) = t)`, 313Induct THEN RW_TAC arith_ss [Inst, Abst, dDEG, MAX_LESS_EQ]); 314 315val dSUB_ID = Q.store_thm("dSUB_ID", 316`!t x. dOK t ==> ([x |-> dVAR x]t = t)`, 317RW_TAC arith_ss [dDEG_dOK, dSUB, dSUB_ID_lemma]); 318 319 320(* --------------------------------------------------------------------- *) 321(* Alpha-conversion. *) 322(* --------------------------------------------------------------------- *) 323 324val dALPHA = Q.store_thm("dALPHA", 325`!t x y. 326 ~(y IN dFV t) /\ dOK t 327 ==> 328 (dLAMBDA x t = dLAMBDA y ([x |-> dVAR y] t))`, 329ZAP_TAC (arith_ss && [dDEG_dOK, dLAMBDA, dSUB]) 330 [Rename,LESS_EQ_REFL]); 331 332val dALPHA_STRONG = Q.store_thm("dALPHA_STRONG", 333 `!t x y. 334 ~(y IN dFV (dLAMBDA x t)) /\ dOK t 335 ==> 336 (dLAMBDA x t = dLAMBDA y ([x |-> dVAR y] t))`, 337ZAP_TAC (arith_ss && [dFV_dLAMBDA,IN_DELETE]) 338 [dALPHA,dSUB_ID]); 339 340(* --------------------------------------------------------------------- *) 341(* Beta-conversion. *) 342(* --------------------------------------------------------------------- *) 343 344val dBETA = 345 Define 346 `dBETA (dABS u) t = Inst 0 u t`; 347 348val dBETA_THM = Q.store_thm("dBETA_THM", 349 `!t u x. dBETA (dLAMBDA x t) u = [x |-> u] t`, 350RW_TAC arith_ss [dBETA, dLAMBDA, dSUB]); 351 352(* --------------------------------------------------------------------- *) 353(* The length of a term: the number of occurrences of atoms. *) 354(* --------------------------------------------------------------------- *) 355 356val dLGH = 357 Define 358 `(dLGH (dCON c) = 1) 359 /\ (dLGH (dVAR x) = 1) 360 /\ (dLGH (dBOUND n) = 1) 361 /\ (dLGH (dABS t) = 1 + dLGH t) 362 /\ (dLGH (dAPP t u) = dLGH t + dLGH u)`; 363 364val dLGH_dSUB = Q.store_thm("dLGH_dSUB", 365`!t x y. dLGH([y |-> dVAR x]t) = dLGH t`, 366RW_TAC arith_ss [dSUB] THEN 367 `!t i x y. dLGH (Inst i (Abst i y t) (dVAR x)) = dLGH t` 368 suffices_by simp[] THEN 369Induct THEN RW_TAC arith_ss [Inst,Abst,dLGH]); 370 371val dLGH_Abst = Q.store_thm("dLGH_Abst", 372`!t x i. dLGH(Abst i x t) = dLGH t`, 373Induct THEN RW_TAC arith_ss [Abst, dLGH]); 374 375val dLGH_NOT_ZERO = Q.store_thm("dLGH_NOT_ZERO", 376`!t. ~(dLGH t = 0)`, 377Induct THEN RW_TAC arith_ss [dLGH]); 378 379val dLGH_dAPP_LESS_1 = Q.store_thm("dLGH_dAPP_LESS_1", 380`!t u. dLGH u < dLGH (dAPP t u)`, 381RW_TAC arith_ss [dLGH] 382 THEN MP_TAC (SPEC_ALL dLGH_NOT_ZERO) 383 THEN RW_TAC arith_ss []); 384 385val dLGH_dAPP_LESS_2 = Q.store_thm("dLGH_dAPP_LESS_2", 386`!t u. dLGH t < dLGH (dAPP t u)`, 387RW_TAC arith_ss [dLGH] 388 THEN MP_TAC (Q.SPEC`u` dLGH_NOT_ZERO) 389 THEN RW_TAC arith_ss []); 390 391val dLGH_dLAMBDA_LESS = Q.store_thm("dLGH_dLAMBDA_LESS", 392`!t x. dLGH t < dLGH (dLAMBDA x t)`, 393RW_TAC arith_ss [dLAMBDA, dLGH, dLGH_Abst]); 394 395val NTH = 396 Define 397 `(NTH 0 (h::t) = h) 398 /\ (NTH (SUC n) (h::t) = NTH n t)`; 399 400 401(* --------------------------------------------------------------------- *) 402(* Initiality......... *) 403(* --------------------------------------------------------------------- *) 404 405val CHOM = 406 Define 407 `(CHOM con var abs app xs (dCON c) = (con:'a ->'b) c) 408 /\ (CHOM con var abs app xs (dVAR x) = var x) 409 /\ (CHOM con var abs app xs (dBOUND n) = 410 if n < LENGTH xs then var (NTH n xs) else ARB) 411 /\ (CHOM con var abs app xs (dABS t) = 412 abs (\x. CHOM con var abs app (x::xs) t)) 413 /\ (CHOM con var abs app xs (dAPP t u) = 414 app (CHOM con var abs app xs t) (CHOM con var abs app xs u))`; 415 416val HOM = 417 Define 418 `HOM (con:'a ->'b) var abs app = CHOM con var abs app []`; 419 420val hom = Term`HOM (con:'a ->'b) var abs app`; 421val chom = Term`CHOM (con:'a ->'b) var abs app`; 422 423(*--------------------------------------------------------------------------- 424 Parallel substitution 425 ---------------------------------------------------------------------------*) 426 427val PSUB = 428 Define 429 `(PSUB d xs (dCON c) = dCON c) 430 /\ (PSUB d xs (dVAR x) = dVAR x) 431 /\ (PSUB d xs (dBOUND n) = if d <= n /\ n < d + LENGTH xs 432 then dVAR (NTH (n-d) xs) else dBOUND n) 433 /\ (PSUB d xs (dABS t) = dABS (PSUB (SUC d) xs t)) 434 /\ (PSUB d xs (dAPP t u) = dAPP (PSUB d xs t) (PSUB d xs u))`; 435 436val SUB_ELIM_LEM = Q.prove( 437`!x y. x < y ==> ?m. y-x = SUC m`, 438RW_TAC arith_ss [] 439 THEN Q.EXISTS_TAC `PRE(y-x)` 440 THEN RW_TAC arith_ss []); 441 442val PSUB_Lemma0 = Q.store_thm("PSUB_Lemma0", 443`!u d. PSUB d [] u = u`, 444Induct THEN RW_TAC list_ss [PSUB]); 445 446(* Awkward proof *) 447val PSUB_Lemma1 = Q.store_thm("PSUB_Lemma1", 448`!t d x xs. PSUB d (x::xs) t = Inst d (PSUB (SUC d) xs t) (dVAR x)`, 449Induct 450 THEN RW_TAC list_ss [Inst, PSUB] THENL 451 [`d < n` by DECIDE_TAC THEN 452 `?m. n-d = SUC m` by PROVE_TAC [SUB_ELIM_LEM] 453 THEN ZAP_TAC (list_ss && [NTH]) 454 [DECIDE (Term `(n-d = SUC m) ==> (n-SUC d = m)`),NTH], 455 `n - d = 0` by (REPEAT (POP_ASSUM MP_TAC) THEN CONV_TAC ARITH_CONV) 456 THEN RW_TAC list_ss [NTH]]); 457 458 459val PSUB_dCON = Q.store_thm("PSUB_dCON", 460 `(PSUB 0 xs (dCON x) = PSUB 0 ys u) = (u = dCON x)`, 461Cases_on `u` 462 THEN ZAP_TAC (list_ss && [PSUB]) []); 463 464 465val PSUB_dAPP = Q.store_thm("PSUB_dAPP", 466 `(PSUB 0 xs (dAPP t1 t2) = PSUB 0 ys u) 467 ==> 468 ?u1 u2. u = dAPP u1 u2`, 469Cases_on `u` THEN RW_TAC arith_ss [PSUB]); 470 471val PSUB_dABS = Q.store_thm("PSUB_dABS", 472 `(PSUB 0 xs (dABS t) = PSUB 0 ys u) ==> ?u1. u = dABS u1`, 473Cases_on `u` THEN RW_TAC list_ss [PSUB]); 474 475val PSUB_dVAR = Q.store_thm("PSUB_dVAR", 476`(PSUB 0 xs (dVAR s) = PSUB 0 ys u) 477 ==> 478 ((u = dVAR s) \/ 479 ?n. (u = dBOUND n) /\ (n < LENGTH ys) /\ (NTH n ys = s))`, 480Cases_on `u` THEN RW_TAC list_ss [PSUB]); 481 482val PSUB_dBOUND = Q.store_thm("PSUB_dBOUND", 483`(PSUB 0 xs (dBOUND n) = PSUB 0 ys u) 484 ==> 485 if n < LENGTH xs 486 then (u = dVAR (NTH n xs)) \/ 487 ?m. m < LENGTH ys /\ (NTH n xs = NTH m ys) /\ (u = dBOUND m) 488 else (u = dBOUND n) /\ ~(n < LENGTH ys)`, 489Cases_on `u` THEN RW_TAC list_ss [PSUB]); 490 491val PSUB_Lemma2 = Q.store_thm("PSUB_Lemma2", 492`(PSUB (SUC 0) xs t = PSUB (SUC 0) ys u') 493 ==> 494 !x. (PSUB 0 (x::xs) t = PSUB 0 (x::ys) u')`, 495PROVE_TAC [PSUB_Lemma1]); 496 497 498val PSUB_Lemma3 = Q.store_thm("PSUB_Lemma3", 499`!t xs u ys. 500 (PSUB 0 xs t = PSUB 0 ys u) 501 ==> 502 (^chom xs t = ^chom ys u)`, 503Induct THEN RW_TAC std_ss [] THENL 504 map IMP_RES_TAC [PSUB_dCON, PSUB_dVAR, PSUB_dBOUND, PSUB_dABS, PSUB_dAPP] 505 THEN BasicProvers.NORM_TAC std_ss [CHOM] 506 THEN IMP_RES_TAC (PROVE [] (Term `x ==> ~x ==> F`)) 507 THEN Q.PAT_X_ASSUM `PSUB p q r = PSUB a b c` MP_TAC 508 THEN RW_TAC std_ss [CHOM,PSUB] 509 THENL [AP_TERM_TAC THEN PROVE_TAC[PSUB_Lemma2, ONE], PROVE_TAC []]); 510 511val HOM_lemma = Q.store_thm("HOM_lemma", 512 `(!x. ^hom (dVAR x) = var x) /\ 513 (!c. ^hom (dCON c) = con c) /\ 514 (!t u. ^hom (dAPP t u) = app (^hom t) (^hom u)) /\ 515 (!t. ^hom (dABS t) = abs (\x. ^hom (Inst 0 t (dVAR x))))`, 516RW_TAC std_ss [HOM,CHOM] 517 THEN AP_TERM_TAC THEN CONV_TAC FUN_EQ_CONV 518 THEN RW_TAC arith_ss [PSUB_Lemma3,PSUB_Lemma0,PSUB_Lemma1]); 519 520 521(* --------------------------------------------------------------------- *) 522(* HOM is an iterator. *) 523(* --------------------------------------------------------------------- *) 524 525val HOM_THM = Q.store_thm("HOM_THM", 526 `(!x. ^hom (dVAR x) = var x) /\ 527 (!c. ^hom (dCON c) = con c) /\ 528 (!t u. ^hom (dAPP t u) = app (^hom t) (^hom u)) /\ 529 (!t x. ^hom (dLAMBDA x t) = abs (\y. ^hom ([x |-> dVAR y]t)))`, 530RW_TAC std_ss [dLAMBDA, HOM_lemma, dSUB]); 531 532 533(* ===================================================================== *) 534(* HOM is the unique iterator. *) 535(* ===================================================================== *) 536 537val UNIQUE_HOM = Q.store_thm("UNIQUE_HOM", 538 `!f var con app abs. 539 (!x. f (dVAR x) = var x) /\ 540 (!c. f (dCON c) = con c) /\ 541 (!t u. dOK t /\ dOK u ==> (f (dAPP t u) = app (f t) (f u))) /\ 542 (!t x. dOK t ==> (f (dLAMBDA x t) = abs (\y. f ([x |-> dVAR y]t)))) 543 ==> 544 !t. dOK t ==> (f t = ^hom t)`, 545RW_TAC std_ss [] 546 THEN measureInduct_on `dLGH t` 547 THEN ONCE_REWRITE_TAC [dOK_cases] THEN RW_TAC std_ss [] 548 THEN RW_TAC arith_ss [HOM_THM] THENL 549 [AP_TERM_TAC THEN CONV_TAC FUN_EQ_CONV THEN BETA_TAC THEN GEN_TAC THEN 550 RULE_ASSUM_TAC(REWRITE_RULE[AND_IMP_INTRO]) THEN FIRST_ASSUM MATCH_MP_TAC 551 THEN RW_TAC arith_ss [dLGH_dSUB,dLAMBDA,dLGH,dLGH_Abst,dOK_dSUB,dOK_DEF], 552 RW_TAC arith_ss [dLGH_dAPP_LESS_1, dLGH_dAPP_LESS_2]]); 553 554 555val UNIQUE_HOM_THM = Q.store_thm("UNIQUE_HOM_THM", 556`!var con app lam (f:'a dB->'b) (g:'a dB->'b). 557 (!x. f (dVAR x) = var x) /\ 558 (!c. f (dCON c) = con c) /\ 559 (!t u. (dOK t /\ dOK u) ==> (f (dAPP t u) = app (f t) (f u))) /\ 560 (!t x. dOK t ==> (f (dLAMBDA x t) = lam (\y. f ([x |-> dVAR y]t)))) /\ 561 (!x. g (dVAR x) = var x) /\ 562 (!c. g (dCON c) = con c) /\ 563 (!t u. (dOK t /\ dOK u) ==> (g (dAPP t u) = app (g t) (g u))) /\ 564 (!t x. dOK t ==> (g (dLAMBDA x t) = lam (\y. g ([x |-> dVAR y]t)))) 565 ==> 566 !t. dOK t ==> (f t = g t)`, 567REPEAT STRIP_TAC 568 THEN IMP_RES_TAC UNIQUE_HOM THEN ASM_REWRITE_TAC[]); 569 570 571(* --------------------------------------------------------------------- *) 572(* Construct a model of the wrapping function. *) 573(* --------------------------------------------------------------------- *) 574 575val lemma1 = Q.prove( 576`!f:'a->'b->bool. 577 (!x. FINITE (f x)) ==> FINITE {z | !x. z IN (f x)}`, 578REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_FINITE_I THEN 579Q.EXISTS_TAC `f a` THEN SRW_TAC [][SUBSET_DEF]); 580 581val lemma2 = Q.prove( 582`!u. dOK u 583 ==> 584 !x. FINITE {z | !y. z IN dFV ([x |-> dVAR y] u)}`, 585REPEAT STRIP_TAC 586 THEN MATCH_MP_TAC 587 (BETA_RULE (Q.ISPEC `\y:string. dFV ([x |-> dVAR y] u)` lemma1)) 588 THEN REWRITE_TAC [FINITE_dFV]); 589 590val NEW_UNION1 = prove( 591 ``FINITE (s UNION t) ==> ~(NEW (s UNION t) IN s)``, 592 STRIP_TAC THEN NEWLib.NEW_ELIM_TAC THEN 593 FULL_SIMP_TAC (srw_ss()) []); 594 595val NOT_EQ_NEW = prove( 596 ``!X. FINITE X /\ x IN X ==> ~(x = NEW X)``, 597 PROVE_TAC [NEW_def]); 598 599 600val lemma3 = 601 Q.prove( 602 `!t x y z. 603 dOK t /\ z IN dFV t /\ ~(z = x) 604 ==> 605 z IN dFV ([x |-> dVAR y] t)`, 606measureInduct_on `dLGH t` 607 THEN ONCE_REWRITE_TAC [dOK_cases] THEN RW_TAC std_ss [] THENL 608 [Q.PAT_X_ASSUM `_ IN _` MP_TAC THEN RW_TAC std_ss [dFV, IN_SING] 609 THEN RW_TAC std_ss [dFV, IN_SING, NEQ_dVAR_dSUB], 610 PROVE_TAC [dCON_dSUB, NOT_IN_EMPTY, dFV], 611 `FINITE (dFV t' UNION {x;y;z})` 612 by RW_TAC std_ss [FINITE_UNION,FINITE_INSERT, FINITE_EMPTY, FINITE_dFV] 613 THEN MP_TAC (Q.SPECL [`t'`, `x'`, `NEW (dFV t' UNION {x;y;z})`] dALPHA) 614 THEN RW_TAC std_ss [NEW_UNION1] THEN POP_ASSUM (K ALL_TAC) THEN 615 `~(x:string = NEW (dFV (t':'a dB) UNION {x;y;z})) 616 /\ ~(NEW (dFV t' UNION {x;y;z}) IN dFV (dVAR y:'a dB)) 617 /\ dOK ([x' |-> dVAR (NEW (dFV t' UNION {x;y;z}))] t')` 618 by (REPEAT CONJ_TAC THENL 619 [RW_TAC std_ss [NOT_EQ_NEW,IN_UNION,IN_INSERT], 620 RW_TAC std_ss [dFV,IN_SING,GSYM NOT_EQ_NEW,IN_UNION,IN_INSERT], 621 RW_TAC std_ss [dOK_dSUB,dOK_DEF]]) 622 THEN RW_TAC std_ss [dLAMBDA_dSUB,dFV_dLAMBDA, IN_DELETE] THENL 623 [Q.PAT_X_ASSUM `$! M` MP_TAC 624 THEN RW_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] 625 THEN FIRST_ASSUM MATCH_MP_TAC THEN RW_TAC std_ss [] THENL 626 [RW_TAC std_ss [dLGH_dSUB,dLGH_dLAMBDA_LESS], 627 FIRST_ASSUM MATCH_MP_TAC THEN RW_TAC std_ss [dLGH_dLAMBDA_LESS] 628 THEN Q.PAT_X_ASSUM `_ IN _` MP_TAC 629 THEN RW_TAC std_ss [dFV_dLAMBDA,IN_DELETE]], 630 RW_TAC std_ss [NOT_EQ_NEW, IN_UNION,IN_INSERT]], 631 Q.PAT_X_ASSUM `_ IN _` MP_TAC 632 THEN ZAP_TAC (std_ss && [dFV, IN_UNION, dAPP_dSUB]) 633 [dLGH_dAPP_LESS_2,dLGH_dAPP_LESS_1]]); 634 635val lemma4 = 636 Q.prove( 637 `!u x. 638 dOK u 639 ==> 640 dFV (dLAMBDA x u) SUBSET {z | !y. z IN dFV([x |-> dVAR y] u)}`, 641RW_TAC std_ss 642 (SUBSET_DEF::GSPEC_DEF::SPECIFICATION::dFV_dLAMBDA 643 ::map (REWRITE_RULE [SPECIFICATION]) [IN_DELETE, lemma3])); 644 645val lemma5 = Q.prove( 646 `!x s t. s SUBSET t /\ ~(x IN t) ==> ~(x IN s)`, 647 PROVE_TAC [SUBSET_DEF]); 648 649 650val WRAP_DB_EXISTS = Q.store_thm("WRAP_DB_EXISTS", 651 `?wrap. !u. dOK u ==> !x. wrap(\s:string. [x |-> dVAR s] u) = dLAMBDA x u`, 652Q.EXISTS_TAC 653 `\f:string->'a dB. 654 let vs = {z | !y. z IN dFV (f y)} in 655 let v = @v. ~(v IN vs) 656 in dLAMBDA v (f v)` 657 THEN RW_TAC std_ss [LET_THM] 658 THEN MATCH_MP_TAC (GSYM dALPHA_STRONG) THEN RW_TAC std_ss [] 659 THEN MATCH_MP_TAC lemma5 660 THEN Q.EXISTS_TAC `{z | !y. z IN dFV([x |-> dVAR y] u)}` 661 THEN RW_TAC std_ss [lemma4] 662 THEN CONV_TAC SELECT_CONV 663 THEN MATCH_MP_TAC new_exists THEN MATCH_MP_TAC lemma2 THEN 664 ASM_REWRITE_TAC []); 665 666val _ = export_theory(); 667