1(*--------------------------------------------------------------------------- 2 Five Axioms of Alpha Conversion 3 (Andy Gordon & Tom Melham) 4 5 6 Part II: name-carrying terms 7 8 ---------------------------------------------------------------------------*) 9 10(* Interactive use: 11 app load ["bossLib", "Q", "pred_setTheory", "stringTheory", "dBTheory"]; 12*) 13 14open HolKernel Parse boolLib 15 bossLib arithmeticTheory pred_setTheory dBTheory 16 BasicProvers basic_swapTheory 17 18val _ = new_theory "nc"; 19 20 21(*--------------------------------------------------------------------------- 22 Support bumpf. 23 ---------------------------------------------------------------------------*) 24 25val FUN_EQ_TAC = CONV_TAC (ONCE_DEPTH_CONV FUN_EQ_CONV) 26 THEN GEN_TAC THEN BETA_TAC; 27 28 29(*--------------------------------------------------------------------------- 30 Definition of the type of name carrying terms. 31 ---------------------------------------------------------------------------*) 32 33val BI_nc = 34 define_new_type_bijections 35 {name = "BI_nc", 36 ABS = "ABS_nc", 37 REP = "REP_nc", 38 tyax = new_type_definition ("nc", 39 Q.prove(`?x:'a dB. dOK x`, PROVE_TAC [dOK_DEF]))}; 40 41val REP_nc_11 = prove_rep_fn_one_one BI_nc; 42val ABS_nc_11 = prove_abs_fn_one_one BI_nc; 43 44val (ABS_REP, OK_REP_ABS) = 45 let val (b1,b2) = CONJ_PAIR BI_nc 46 in (b1, GEN_ALL (fst (EQ_IMP_RULE (SPEC_ALL b2)))) 47 end; 48 49val OK_REP = Q.prove(`!u. dOK (REP_nc u)`, PROVE_TAC [BI_nc]); 50 51val OK_ss = std_ss && [OK_REP, OK_REP_ABS, dOK_DEF, ABS_REP, dOK_dSUB]; 52 53(* --------------------------------------------------------------------- *) 54(* Definition of the constructors. *) 55(* --------------------------------------------------------------------- *) 56 57val CON = Define `CON c = ABS_nc (dCON c)` 58val VARR = Define `VAR x = ABS_nc (dVAR x)` 59val LAM = Define `LAM x m = ABS_nc (dLAMBDA x (REP_nc m))`; 60val APP = xDefine 61 "APP" `$@@ m n = ABS_nc (dAPP (REP_nc m) (REP_nc n))` 62 63val _ = set_fixity "@@" (Infixl 901); 64 65 66(* --------------------------------------------------------------------- *) 67(* Definition of the free variable function. At the abstract level, this *) 68(* will satisfy the following defining property: *) 69(* *) 70(* |- (!k. FV(CON k) = {}) /\ *) 71(* (!x. FV(VAR x) = {x}) /\ *) 72(* (!t u. FV(t @@ u) = (FV t) UNION (FV u)) /\ *) 73(* (!x n. FV(LAM x n) = (FV n) DELETE x) *) 74(* *) 75(* which also forms a part of the abstract characterization of the type *) 76(* of name-carrying terms. *) 77(* --------------------------------------------------------------------- *) 78 79val FV = 80 Define 81 `FV u = dFV (REP_nc u)`; 82 83val FV_THM = Q.store_thm("FV_THM", 84 `(!k. FV (CON k:'a nc) = {}) /\ 85 (!x. FV (VAR x:'a nc) = {x}) /\ 86 (!t u. FV (t @@ u:'a nc) = (FV t) UNION (FV u)) /\ 87 (!x n. FV (LAM x n:'a nc) = (FV n) DELETE x)`, 88RW_TAC OK_ss 89 [FV, CON, VARR, APP, LAM, dFV_def, dFV_dLAMBDA]); 90val _ = export_rewrites ["FV_THM"] 91 92 93(* --------------------------------------------------------------------- *) 94(* Definition of substitution. At the abstract level, this will satisfy *) 95(* the following defining property: *) 96(* *) 97(* |- (!s k. (CON k) SUB s = CON k) /\ *) 98(* (!u x. (VAR x) SUB (u,x) = u) /\ *) 99(* (!u x y. ~(x = y) ==> ((VAR y) SUB (u,x) = VAR y)) /\ *) 100(* (!s t u. (t @@ u) SUB s = (t SUB s) @@ (u SUB s)) /\ *) 101(* (!x t u. (LAM x t) SUB (u,x) = LAM x t) /\ *) 102(* (!x y u. *) 103(* ~(x = y) /\ ~y IN (FV u) ==> *) 104(* !t. ((LAM y t) SUB (u,x) = LAM y(t SUB (u,x)))) *) 105(* *) 106(* which also forms a part of the abstract characterization of the type *) 107(* of name-carrying terms. *) 108(* --------------------------------------------------------------------- *) 109 110val SUB_DEF = 111 Define 112 `SUB new old u = ABS_nc ([old |-> REP_nc new] (REP_nc u))`; 113 114val _ = add_rule {term_name = "SUB", fixity = Closefix, 115 pp_elements = [TOK "[", TM, TOK "/", TM, TOK "]"], 116 paren_style = OnlyIfNecessary, 117 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2))}; 118 119 120val lem = Q.prove( 121`!r r'. dOK r /\ dOK r' /\ (r=r') ==> (ABS_nc r = ABS_nc r')`, 122PROVE_TAC [ABS_nc_11]); 123 124val u = Term`u:'a nc`; 125 126val SUB_THM = 127 Q.store_thm ("SUB_THM", 128 `(!^u x k. [u/x](CON k) = CON k) /\ 129 (!^u x. [u/x](VAR x) = u) /\ 130 (!^u x y. ~(x=y) ==> ([u/x](VAR y) = VAR y)) /\ 131 (!^u s t x. [u/x](s @@ t) = [u/x]s @@ [u/x]t) /\ 132 (!^u t x. [u/x](LAM x t) = LAM x t) /\ 133 (!^u x y. ~(x=y) /\ ~(y IN FV u) 134 ==> !t. [u/x](LAM y t) = LAM y ([u/x]t))`, 135RW_TAC OK_ss 136 [LAM, APP, VARR, CON, FV, SUB_DEF,lem, NEQ_dVAR_dSUB, 137 EQ_dVAR_dSUB,dCON_dSUB, dAPP_dSUB,dLAMBDA_dSUB_EQ,dLAMBDA_dSUB]); 138 139(* ADG: following should be the axiomatisation *) 140 141val SUB_VAR = Q.store_thm("SUB_VAR", 142`!x y t. [t/y](VAR x) = if x=y then t else VAR x`, 143RW_TAC std_ss [SUB_THM]); 144 145 146 147(* --------------------------------------------------------------------- *) 148(* Alpha conversion. This is also part of the characterization of name- *) 149(* carrying terms. Open question: prove the independence of ALPHA. *) 150(* --------------------------------------------------------------------- *) 151 152val ALPHA = 153 Q.store_thm ("ALPHA", 154 `!x y ^u. 155 ~(y IN (FV (LAM x u))) ==> (LAM x u = LAM y ([VAR y/x]u))`, 156RW_TAC std_ss [FV_THM,DE_MORGAN_THM,IN_DELETE,FV, LAM, SUB_DEF, VARR] 157 THEN MATCH_MP_TAC lem 158 THEN RW_TAC OK_ss [] 159 THEN Cases_on `y:string = x` 160 THEN ZAP_TAC (OK_ss && [dSUB_ID]) [dALPHA,OK_REP]); 161 162 163val ALPHA_LEMMA = Q.prove( 164 `!x u. LAM x ([VAR x/x]u) = LAM x u`, 165PROVE_TAC [ALPHA,FV_THM,IN_DELETE]); 166 167 168(* --------------------------------------------------------------------- *) 169(* Weaker version of Alpha Conversion. *) 170(* --------------------------------------------------------------------- *) 171 172val SIMPLE_ALPHA = 173 Q.store_thm ("SIMPLE_ALPHA", 174 `!y u. 175 ~(y IN FV u) ==> !x. LAM x u = LAM y ([VAR y/x]u)`, 176PROVE_TAC [ALPHA,FV_THM,IN_DELETE]); 177 178 179(* --------------------------------------------------------------------- *) 180(* Now unique iterator. *) 181(* --------------------------------------------------------------------- *) 182 183val EXISTENCE = Q.prove( 184 `!con : 'a->'b. 185 !var : string->'b. 186 !app : 'b->'b->'b. 187 !lam : (string->'b) -> 'b. 188 ?hom:'a nc -> 'b. 189 (!k. hom(CON k) = con k) /\ 190 (!x. hom(VAR x) = var x) /\ 191 (!n m. hom(n @@ m) = app (hom n) (hom m)) /\ 192 (!x n. hom(LAM x n) = lam(\y. hom([VAR y/x]n)))`, 193RW_TAC std_ss [] 194 THEN Q.EXISTS_TAC `\x. HOM (con:'a ->'b) var lam app (REP_nc x)` 195 THEN RW_TAC OK_ss [CON,VARR,APP,LAM, HOM_THM,SUB_DEF]); 196 197 198val nc_ITERATOR = 199 Q.store_thm ("nc_ITERATOR", 200 `!con : 'a->'b. 201 !var : string->'b. 202 !app : 'b->'b->'b. 203 !lam : (string->'b)->'b. 204 ?!hom :'a nc -> 'b. 205 (!k. hom(CON k) = con k) /\ 206 (!x. hom(VAR x) = var x) /\ 207 (!t u. hom(t @@ u) = app (hom t) (hom u)) /\ 208 (!x u. hom(LAM x u) = lam(\y. hom([VAR y/x]u)))`, 209CONV_TAC (ONCE_DEPTH_CONV EXISTS_UNIQUE_CONV) 210 THEN RW_TAC std_ss [EXISTENCE,CON,VARR,APP,LAM,SUB_DEF] THEN FUN_EQ_TAC 211 THEN PURE_ONCE_REWRITE_TAC [GSYM ABS_REP] THEN 212 let val th1 = Q.ISPEC `REP_nc (n:'a nc)` (UNDISCH (SPEC_ALL UNIQUE_HOM_THM)) 213 val th2 = REWRITE_RULE [OK_REP] th1 214 val th3 = itlist Q.GEN [`f`, `g`] (DISCH_ALL th2) 215 val th4 = Q.ISPECL [`(f:'a nc->'b) o ABS_nc`, 216 `(g:'a nc->'b) o ABS_nc`] th3 217 in MATCH_MP_TAC (REWRITE_RULE [combinTheory.o_THM] th4) end 218 THEN RW_TAC std_ss [] THEN IMP_RES_THEN (SUBST1_TAC o GSYM) OK_REP_ABS 219 THEN RW_TAC OK_ss []); 220 221(* --------------------------------------------------------------------- *) 222(* Abstraction function. *) 223(* --------------------------------------------------------------------- *) 224 225val lemma = 226 Q.prove(`REP_nc o (\s. [VAR s/x]^u) = \s. REP_nc([VAR s/x]u)`, 227RW_TAC std_ss 228 [combinTheory.o_DEF]); 229 230 231val ABS_EXISTS = Q.prove( 232 `?abs:(string->'a nc)->'a nc. 233 !^u x. abs (\s. [VAR s/x]u) = LAM x u`, 234STRIP_ASSUME_TAC WRAP_DB_EXISTS 235 THEN Q.EXISTS_TAC `\f. ABS_nc(wrap (REP_nc o f))` 236 THEN RW_TAC OK_ss [lemma,LAM,SUB_DEF,VARR]); 237 238 239val ABS_DEF = new_specification ("ABS_DEF", ["ABS"], ABS_EXISTS); 240 241(* ********************************************************************* *) 242(* End of characterization. *) 243(* ********************************************************************* *) 244 245(* --------------------------------------------------------------------- *) 246(* Alternative characterization, with ABS as primitive. *) 247(* --------------------------------------------------------------------- *) 248 249val (ALT_FV,ALT_SUB_THM,ALT_ALPHA,ALT_ITERATOR) 250 = let val f = REWRITE_RULE [GSYM ABS_DEF] 251 in 252 (f FV_THM, f SUB_THM, f ALPHA, f nc_ITERATOR) 253 end; 254val _ = save_thm("ALT_FV", ALT_FV); 255val _ = save_thm("ALT_SUB_THM", ALT_SUB_THM); 256val _ = save_thm("ALT_ALPHA", ALT_ALPHA); 257val _ = save_thm("ALT_ITERATOR", ALT_ITERATOR); 258 259 260(* ===================================================================== *) 261(* Distinctness. This follows easily from iterators. *) 262(* ===================================================================== *) 263 264val ethm = 265 let val sth = Q.SPECL [`\k. (F,F)`, (* map CON to zero *) 266 `\x. (F,T)`, (* map VAR to one *) 267 `\n m. (T,F)`, (* map APP to two *) 268 `\f. (T,T)`] (* map LAM to three *) 269 (INST_TYPE [beta |-> Type`:bool#bool`] nc_ITERATOR) 270 in 271 CONJUNCT1 (CONV_RULE EXISTS_UNIQUE_CONV (BETA_RULE sth)) 272 end; 273 274val nc_DISTINCT = 275 Q.store_thm ("nc_DISTINCT", 276 `(!(k:'a) x. ~(CON k = VAR x)) /\ 277 (!k x u. ~(CON k = LAM x ^u)) /\ 278 (!k t u. ~(CON k = t @@ ^u)) /\ 279 (!x t u. ~(VAR x = t @@ ^u)) /\ 280 (!x y u. ~(VAR x = LAM y ^u)) /\ 281 (!x u t p. ~(LAM x ^u = t @@ p))`, 282STRIP_ASSUME_TAC ethm THEN RW_TAC std_ss [] 283 THEN DISCH_THEN (MP_TAC o Q.AP_TERM `hom:'a nc -> bool#bool`) 284 THEN RW_TAC std_ss []); 285 286(* ===================================================================== *) 287(* Case analysis. This follows trivially from iterators. *) 288(* ===================================================================== *) 289 290val ithm = 291 let val sth = Q.SPECL [`\k. T`, `\x. T`, `\n m. T`, `\f. T`] 292 (INST_TYPE [beta |-> bool] nc_ITERATOR) 293 val uth = CONJUNCT2 (CONV_RULE EXISTS_UNIQUE_CONV (BETA_RULE sth)) 294 val thm1 = REWRITE_RULE [] (Q.SPEC `\u. T` uth) 295 val thm2 = Q.SPEC `\p:'a nc. (?k. p = CON k) 296 \/ (?x. p = VAR x) 297 \/ (?t u. p = t @@ u) 298 \/ (?x u. p = LAM x u)` thm1 299 val thm3 = CONV_RULE FUN_EQ_CONV (UNDISCH (BETA_RULE thm2)) 300 in 301 DISCH_ALL (REWRITE_RULE [] (BETA_RULE thm3)) 302 end; 303 304val nc_CASES = 305 Q.store_thm ("nc_CASES", 306 `!v:'a nc. (?k. v = CON k) 307 \/ (?x. v = VAR x) 308 \/ (?t u. v = t @@ u) 309 \/ (?x u. v = LAM x u)`, 310PROVE_TAC [ithm]); 311 312 313(* ===================================================================== *) 314(* Initiality + Wrap implies recursion! *) 315(* ===================================================================== *) 316 317(* --------------------------------------------------------------------- *) 318(* In what follows, we will need to be able to express a function: *) 319(* *) 320(* h : A -> B x C *) 321(* *) 322(* as the combination h = <f,g> of two component functions *) 323(* *) 324(* f : A -> B and g : A -> C *) 325(* *) 326(* The following lemma lets us do this. *) 327(* --------------------------------------------------------------------- *) 328 329val COMPONENT_THM = Q.prove( 330`!P. (?!f:'A->('B#'C). P f) = ?!p. P(\a.(FST p a, SND p a))`, 331GEN_TAC THEN CONV_TAC (DEPTH_CONV EXISTS_UNIQUE_CONV) 332 THEN EQ_TAC THEN RW_TAC std_ss [] THENL 333 [Q.EXISTS_TAC `FST o f, SND o f` 334 THEN RW_TAC std_ss [combinTheory.o_THM,ETA_THM], 335 Cases_on `p` THEN Cases_on `p'` 336 THEN RULE_ASSUM_TAC (REWRITE_RULE pairTheory.pair_rws) 337 THEN `(\a:'A. (q a, r a):'B#'C) = \a:'A. (q' a, r' a)` by RES_TAC 338 THEN PROVE_TAC [pairTheory.PAIR_EQ,EQ_EXT], 339 PROVE_TAC[], 340 Q.PAT_X_ASSUM `$! M` 341 (MP_TAC o Q.SPECL [`(FST o f, SND o f)`, `(FST o f', SND o f')`]) 342 THEN RW_TAC std_ss [combinTheory.o_THM, FUN_EQ_THM,ETA_THM] 343 THEN PROVE_TAC [pairTheory.PAIR_EQ,pairTheory.PAIR,FUN_EQ_THM]]); 344 345 346val wee_lemma = Q.prove( 347`(FST o \y. (f([VAR y/x]^u), g([VAR y/x]u)):'A1#'A2) 348 = 349 \y. f ([VAR y/x]u)`, 350FUN_EQ_TAC THEN RW_TAC std_ss [combinTheory.o_THM]); 351 352val COPY_BUILD_lemma = 353 let val instth = INST_TYPE [beta |-> Type`:'a nc # 'b`] nc_ITERATOR 354 val con = Term`\k:'a. (CON k, (con k:'b) )` 355 and var = Term`\s:string. (VAR s:'a nc, (var s:'b) )` 356 and app = Term`\p:'a nc # 'b. 357 \q:'a nc # 'b. 358 ((FST p) @@ (FST q):'a nc, (app p q:'b) )` 359 and lam = Term`\f:string->('a nc # 'b). 360 let u:'a nc = ABS (FST o f) in (u, (lam f:'b))` 361 val th1 = SPECL [con,var,app,lam] instth 362 val th2 = BETA_RULE (ISPEC (rand(concl th1)) COMPONENT_THM) 363 val th3 = EQ_MP th2 (BETA_RULE th1) 364 val th4 = CONV_RULE (DEPTH_CONV pairLib.let_CONV) th3 365 val th5 = REWRITE_RULE [pairTheory.PAIR_EQ,wee_lemma] (BETA_RULE th4) 366 in 367 CONV_RULE (DEPTH_CONV FORALL_AND_CONV) th5 368 end; 369 370val COPY_BUILD = Q.prove( 371`?!p:('a nc -> 'a nc) # ('a nc -> 'b). 372 ((!k. FST p(CON k) = CON k) /\ 373 (!x. FST p(VAR x) = VAR x) /\ 374 (!t u. FST p(t @@ u) = (FST p t)@@(FST p u)) /\ 375 (!x u. FST p(LAM x u) = ABS(\y. FST p([VAR y/x]u)))) 376 /\ 377 ((!k. SND p(CON k) = con k) /\ 378 (!x. SND p(VAR x) = var x) /\ 379 (!t u. SND p(t @@ u) = app(FST p t, SND p t) (FST p u, SND p u)) /\ 380 (!x u. SND p(LAM x u) = 381 lam(\y. (FST p([VAR y/x]u),SND p([VAR y/x]u)))))`, 382RW_TAC std_ss [DECIDE (Term 383 `(a /\ b /\ c /\ d) /\ (e /\ f /\ g /\ h) 384 ��� 385 (a /\ e) /\ (b /\ f) /\ (c /\ g) /\ (d /\ h)`), 386 REWRITE_RULE pairTheory.pair_rws COPY_BUILD_lemma]); 387 388val lemma = 389 let 390 val instth = INST_TYPE [beta |-> Type`:'a nc`] nc_ITERATOR 391 val con = Term`\k. CON k:'a nc` and 392 var = Term`\x:string. VAR x:'a nc` and 393 app = Term`\t:'a nc. \u:'a nc. t @@ u` and 394 lam = Term`\f:string->'a nc. ABS f` 395 val th1 = BETA_RULE (SPECL [con,var,app,lam] instth) 396 val th2 = CONJUNCT2 (CONV_RULE EXISTS_UNIQUE_CONV th1) 397 val th3 = BETA_RULE (Q.SPEC `\x:'a nc.x` th2) 398 val th4 = REWRITE_RULE [ABS_DEF] th3 399 val th5 = GSYM (UNDISCH (SPEC_ALL th4)) 400 in 401 GEN_ALL (DISCH_ALL th5) 402 end; 403 404val COPY_ID = Q.prove( 405 `!hom:'a nc->'a nc. 406 (!k. hom(CON k) = CON k) /\ 407 (!x. hom(VAR x) = VAR x) /\ 408 (!t u. hom(t @@ u) = (hom t) @@ (hom u)) /\ 409 (!x u. hom(LAM x u) = ABS(\y. hom([VAR y/x]u))) 410 ��� 411 (hom = \x.x)`, 412GEN_TAC THEN EQ_TAC THEN STRIP_TAC 413 THENL [MATCH_MP_TAC lemma, ALL_TAC] 414 THEN RW_TAC std_ss [ABS_DEF]); 415 416val messy_lemma = Q.prove( 417`!p:('a nc -> 'a nc) # ('a nc -> 'b). 418 ((FST p = \x. x) /\ 419 (!k. SND p (CON k) = con k) /\ 420 (!x. SND p (VAR x) = var x) /\ 421 (!t u. SND p (t @@ u) = app(FST p t,SND p t) (FST p u,SND p u)) /\ 422 (!x u. SND p (LAM x u) = lam(\y. (FST p([VAR y/x]u), SND p([VAR y/x]u))))) 423 = 424 ((FST p = (\x . x)) /\ 425 (!k. SND p(CON k) = con k) /\ 426 (!x. SND p(VAR x) = var x) /\ 427 (!t u. SND p(t @@ u) = app(t,SND p t)(u,SND p u)) /\ 428 (!x u. SND p(LAM x u) = lam(\y. ([VAR y/x]u, SND p([VAR y/x]u)))))`, 429GEN_TAC THEN EQ_TAC THEN RW_TAC std_ss []); 430 431val pair_lemma = Q.prove( 432`!P Q. (?!p:'a #'b. P(FST p) /\ Q(SND p)) ==> ?!s:'b. Q s`, 433CONV_TAC (ONCE_DEPTH_CONV EXISTS_UNIQUE_CONV) 434 THEN RW_TAC std_ss [] THENL 435 [PROVE_TAC [], 436 Q.PAT_X_ASSUM `$! M` 437 (MP_TAC o Q.SPECL [`(FST (p:'a#'b),s)`, `(FST (p:'a#'b),s')`]) 438 THEN RW_TAC std_ss []]); 439 440val COPY_THEOREM = 441 let val th1 = REWRITE_RULE [COPY_ID,messy_lemma] COPY_BUILD 442 val (conj1, conj2) = dest_conj(body(rand (concl th1))) 443 val p = Term `p : ('a nc -> 'a nc) # ('a nc -> 'b)` 444 val v1 = genvar (Type`:'a nc -> 'a nc`) 445 and v2 = genvar (Type`:'a nc -> 'b`) 446 val P = subst [Term`FST ^p` |-> v1] conj1 447 and Q = subst [Term`SND ^p` |-> v2] conj2 448 val lp = Term`\^v1. ^P` 449 val lq = Term`\^v2. ^Q` 450 val th2 = BETA_RULE (ISPECL [lp,lq] pair_lemma) 451 val th3_0 = Q.INST [`var` |-> `var`, `con` |-> `con`, 452 `app` |-> `\p q. app' (SND p) (SND q) (FST p) (FST q)`, 453 `lam` |-> `\f. lam' (\y. SND(f y)) (\y. FST(f y))`] 454 (MP th2 th1) 455 val th3 = Q.INST [`lam'` |-> `lam`, `app'` |-> `app`] th3_0 456 val th4 = REWRITE_RULE [] (BETA_RULE th3) 457 in 458 REWRITE_RULE pairTheory.pair_rws (BETA_RULE th4) 459 end; 460 461val nc_RECURSION = Q.store_thm ("nc_RECURSION", 462 `!con:'a -> 'b. 463 !var:string -> 'b. 464 !app:'b -> 'b -> 'a nc -> 'a nc -> 'b. 465 !lam:(string -> 'b) -> (string -> 'a nc) -> 'b. 466 ?!hom:'a nc -> 'b. 467 (!k. hom(CON k) = con k) /\ 468 (!x. hom(VAR x) = var x) /\ 469 (!t u. hom(t @@ u) = app (hom t) (hom u) t u) /\ 470 (!x u. hom(LAM x u) = lam (\y. hom([VAR y/x]u)) 471 (\y. [VAR y/x] u))`, 472 REWRITE_TAC [COPY_THEOREM]); 473 474val nc_RECURSION_WEAK = Q.store_thm( 475 "nc_RECURSION_WEAK", 476 `!con var app lam. 477 ?hom : 'a nc -> 'b. 478 (!k. hom (CON k) = con k) /\ 479 (!x. hom (VAR x) = var x) /\ 480 (!t u. hom (t @@ u) = app t u (hom t) (hom u)) /\ 481 (!x u. hom (LAM x u) = lam (\y. [VAR y /x] u) (\y. hom([VAR y /x] u)))`, 482 REPEAT GEN_TAC THEN 483 STRIP_ASSUME_TAC ((CONJUNCT1 o CONV_RULE EXISTS_UNIQUE_CONV o 484 Q.SPECL [`con`, `var`, `\ht hu t u. app t u ht hu`, 485 `\hu u. lam u hu`]) 486 nc_RECURSION) THEN 487 RULE_ASSUM_TAC BETA_RULE THEN 488 Q.EXISTS_TAC `hom` THEN ASM_REWRITE_TAC []); 489 490(* ===================================================================== *) 491(* Definition of destructors. These are derivable from recursion. *) 492(* ===================================================================== *) 493 494fun nc_recDefine s q = 495 new_recursive_definition 496 {rec_axiom = nc_RECURSION_WEAK, name=s, def=Term q}; 497 498val VNAME_DEF = nc_recDefine "VNAME_DEF" `VNAME (VAR s) = s`; 499val CNAME_DEF = nc_recDefine "CNAME_DEF" `CNAME (CON k) = k`; 500val RATOR_DEF = nc_recDefine "RATOR_DEF" `RATOR(M @@ N) = M`; 501val RAND_DEF = nc_recDefine "RAND_DEF" `RAND (M @@ N) = N`; 502 503val BODY_DEF = 504 let val instth = INST_TYPE [beta |-> Type`:string->'a nc`] nc_RECURSION 505 val vs = fst(strip_forall (concl instth)) 506 val th1 = SPECL (rev(tl(rev vs))) instth 507 val tm = Term`\(s:string->(string->'a nc)) (t:string->'a nc). t` 508 val th2 = CONJUNCT1(CONV_RULE (EXISTS_UNIQUE_CONV) (SPEC tm th1)) 509 val lemma = Q.prove( 510 `?f:'a nc -> (string->'a nc). !x u. f(LAM x ^u) = \y. [VAR y/x]u`, 511 STRIP_ASSUME_TAC th2 THEN Q.EXISTS_TAC `hom` THEN RW_TAC std_ss []) 512 in 513 new_specification ("BODY_DEF", ["BODY"], lemma) 514 end; 515 516(* --------------------------------------------------------------------- *) 517(* Note the following relations between ABS and Body. *) 518(* --------------------------------------------------------------------- *) 519 520val ABS_BODY = Q.store_thm("ABS_BODY", 521 `!x u. ABS(BODY(LAM x u)) = LAM x u`, 522REWRITE_TAC [ABS_DEF,BODY_DEF]); 523 524val BODY_ABS = Q.store_thm("BODY_ABS", 525 `!x u. BODY(ABS(\y. [VAR y/x]u)) = \y. [VAR y/x]u`, 526REWRITE_TAC [ABS_DEF,BODY_DEF]); 527 528 529(* ===================================================================== *) 530(* Injectivity. This follows from the existence of destructors. *) 531(* Question: how to strengthen the LAM case to equality? *) 532(* ===================================================================== *) 533 534val nc_INJECTIVITY = Q.store_thm ("nc_INJECTIVITY", 535`(!k:'a . !k'. (CON k = CON k') = (k = k')) /\ 536 (!x x'. (VAR x:'a nc = VAR x') = (x = x')) /\ 537 (!t u t' u'. (t @@ ^u = t' @@ u') = ((t = t') /\ (u = u'))) /\ 538 (!x u x' u'. (LAM x ^u = LAM x' u') 539 ==> 540 !y. [VAR y/x]u = [VAR y/x']u')`, 541REPEAT (STRIP_TAC ORELSE EQ_TAC) 542 THEN ZAP_TAC std_ss 543 [CNAME_DEF,VNAME_DEF,RATOR_DEF,RAND_DEF,BODY_DEF]); 544 545(* --------------------------------------------------------------------- *) 546(* Note that, from injectivity, we could derive destructors. *) 547(* --------------------------------------------------------------------- *) 548 549val lemma1 = Q.prove( 550`?vname. !s. vname(VAR s) = s`, 551Q.EXISTS_TAC`\u. @s. VAR s = u` THEN RW_TAC std_ss [nc_INJECTIVITY]); 552 553val lemma2 = Q.prove( 554`?cname. !k. cname(CON k) = k`, 555Q.EXISTS_TAC`\u. @k. CON k = u` THEN RW_TAC std_ss [nc_INJECTIVITY]); 556 557val lemma3 = Q.prove( 558`?rator. !t u. rator(t @@ u) = t`, 559Q.EXISTS_TAC`\n. @t. ?u. (t @@ u) = n` THEN RW_TAC std_ss [nc_INJECTIVITY]); 560 561val lemma4 = Q.prove( 562`?rand. !t u. rand(t @@ u) = u`, 563Q.EXISTS_TAC`\n. @u. ?t. (t @@ u) = n` THEN RW_TAC std_ss [nc_INJECTIVITY]); 564 565 566(* ===================================================================== *) 567(* Induction. This should follow from the uniqueness part of recursion. *) 568(* ===================================================================== *) 569 570(* --------------------------------------------------------------------- *) 571(* We can derive INDUCTION: *) 572(* *) 573(* |- !P. *) 574(* (!k. P(CON k)) /\ *) 575(* (!x. P(VAR x)) /\ *) 576(* (!t u. P t /\ P u ==> P(t @@ u)) /\ *) 577(* (!x u. (!y. P(u SUB (VAR y,x))) ==> P(LAM x u)) ==> *) 578(* (!u. P u) *) 579(* *) 580(* from RECURSION and ABS as follows. *) 581(* --------------------------------------------------------------------- *) 582 583val nc_INDUCTION = 584 let val instth = INST_TYPE [Type.beta |-> Type.bool] nc_RECURSION 585 val con = Term`\x:'a. T` and 586 var = Term`\x:string. T` and 587 app = Term`\p q. \n m. (p /\ q) \/ P((n @@ m):'a nc)` and 588 lam = Term`\f:string->bool. \g:string->'a nc. $! f \/ P(ABS g)` 589 val th1 = BETA_RULE (SPECL [con,var,app,lam] instth) 590 val th2 = CONJUNCT2 (CONV_RULE EXISTS_UNIQUE_CONV th1) 591 val th3 = BETA_RULE (Q.SPECL [`\x.T`, `P`] th2) 592 val th4 = AP_THM (UNDISCH (REWRITE_RULE [] th3)) (Term`u:'a nc`) 593 val th5 = GEN_ALL (REWRITE_RULE [] (BETA_RULE th4)) 594 in 595 GEN_ALL 596 (REWRITE_RULE [ABS_DEF,DECIDE (Term`(A ��� B \/ A) ��� (B ==> A)`)] 597 (DISCH_ALL th5)) 598 end; 599 600val _ = save_thm("nc_INDUCTION", nc_INDUCTION); 601 602 603(* --------------------------------------------------------------------- *) 604(* The induction tactic. *) 605(* --------------------------------------------------------------------- *) 606 607fun nc_INDUCT_TAC (A,g) = 608 let val (_,P) = dest_comb g 609 val ith = ISPEC P nc_INDUCTION 610 fun bconv tm = 611 if rator tm !~ P then 612 raise HOL_ERR{origin_structure = "ncScript.sml", 613 origin_function = "nc_INDUCT_TAC", 614 message = "function bconv failed"} 615 else BETA_CONV tm 616 val bth = CONV_RULE (ONCE_DEPTH_CONV bconv) ith 617 in 618 (MATCH_MP_TAC bth 619 THEN REPEAT CONJ_TAC THENL 620 [ALL_TAC, ALL_TAC, 621 GEN_TAC THEN GEN_TAC THEN STRIP_TAC, 622 GEN_TAC THEN GEN_TAC THEN STRIP_TAC]) (A,g) 623 end; 624 625(* --------------------------------------------------------------------- *) 626(* A useful tactic from Andy's original development. *) 627(* *) 628(* A |- P ([u/x](VAR y)) *) 629(* ======================================= VAR_SUB_TAC *) 630(* A |- P(u) A, ~(x=y) |- P(VAR y) *) 631(* --------------------------------------------------------------------- *) 632 633local val SUBconst = prim_mk_const{Thy="nc",Name="SUB"} 634 val VARconst = prim_mk_const{Thy="nc",Name="VAR"} 635in 636fun dest_sub tm = 637 case strip_comb tm 638 of (sub,[new,old,VARapp]) => 639 let val _ = assert (same_const SUBconst) sub 640 val (Rator,Rand) = dest_comb VARapp 641 val _ = assert (same_const VARconst) Rator 642 in (Rand,new,old) 643 end 644 | _ => raise mk_HOL_ERR "ncScript.sml" "dest_sub" "" 645end 646 647fun VAR_SUB_TAC (A,g) = 648 let val (v,new,old) = dest_sub (find_term (can dest_sub) g) 649 in 650 DISJ_CASES_THEN2 651 (fn eq => SUBST_ALL_TAC eq THEN 652 PURE_ONCE_REWRITE_TAC [el 2 (CONJUNCTS SUB_THM)]) 653 (fn neq => STRIP_ASSUME_TAC neq THEN 654 PURE_ONCE_REWRITE_TAC [MATCH_MP (el 3 (CONJUNCTS SUB_THM)) neq]) 655 (SPEC (mk_eq(old, v)) EXCLUDED_MIDDLE) 656 (A,g) 657 end 658 handle e => raise wrap_exn "ncScript" "VAR_SUB_TAC" e; 659 660(* ===================================================================== *) 661(* Sanity check - try to prove Lemma 1.14 from Hindley and Seldin using *) 662(* our new induction principle. It's provable, but makes use of the *) 663(* stronger form of alpha conversion. Question: does it make essential *) 664(* use of this stronger form? *) 665(* ===================================================================== *) 666 667val lemma14a = Q.store_thm ("lemma14a", 668`!u x. [VAR x/x]u = u`, 669nc_INDUCT_TAC THEN RW_TAC std_ss [SUB_THM] THENL 670 [VAR_SUB_TAC THEN REFL_TAC, 671 Cases_on `x':string = x` THENL 672 [RW_TAC std_ss [SUB_THM], 673 `~(x IN FV (VAR x'))` by RW_TAC std_ss [FV_THM,IN_SING] 674 THEN RW_TAC std_ss [SUB_THM] 675 THEN Q.PAT_X_ASSUM `$! M` 676 (MP_TAC o Q.AP_TERM `LAM x` o Q.SPECL [`x:string`, `x':string`]) 677 THEN IMP_RES_TAC (el 6 (CONJUNCTS SUB_THM)) 678 THEN Q.PAT_X_ASSUM `$! M` (ASSUME_TAC o GSYM) 679 THEN RW_TAC std_ss [ALPHA_LEMMA]]]); 680 681(* can now prove a simple version of induction, where you don't want that 682 extra strength in the LAM case *) 683val simple_induction = store_thm( 684 "simple_induction", 685 ``!P. (!s. P (VAR s)) /\ (!k. P (CON k)) /\ 686 (!t u. P t /\ P u ==> P(t @@ u)) /\ 687 (!v t. P t ==> P (LAM v t)) ==> 688 (!t. P t)``, 689 GEN_TAC THEN STRIP_TAC THEN HO_MATCH_MP_TAC nc_INDUCTION THEN 690 PROVE_TAC [lemma14a]); 691 692 693(* --------------------------------------------------------------------- *) 694(* Andy has observed that lemma14a plus weak alpha gives strong alpha. *) 695(* --------------------------------------------------------------------- *) 696val slemma = Q.prove( 697`!x y u. 698 ~(y IN (FV (LAM x u))) ==> (LAM x u = LAM y([VAR y/x]u))`, 699ZAP_TAC (std_ss && [FV_THM,IN_DELETE,IN_SING,DE_MORGAN_THM]) 700 [lemma14a,SIMPLE_ALPHA]); 701 702(* ===================================================================== *) 703(* Sanity check: set of free variables is finite. This was a postulate *) 704(* in Andy's 1993 paper. Here, it depends on induction and the strong *) 705(* alpha axiom (via lemma14a). *) 706(* ===================================================================== *) 707 708val FINITE_FV = Q.store_thm ("FINITE_FV", 709`!u. FINITE(FV u)`, 710nc_INDUCT_TAC 711 THEN RW_TAC std_ss 712 [FV_THM,FINITE_EMPTY,FINITE_SING,FINITE_UNION,FINITE_DELETE] 713 THEN PROVE_TAC [lemma14a]); 714val _ = export_rewrites ["FINITE_FV"] 715 716(* ===================================================================== *) 717(* Injectivity theorems *) 718(* ===================================================================== *) 719 720val INJECTIVITY_LEMMA1 = Q.store_thm("INJECTIVITY_LEMMA1", 721`!x u x1 u1. 722 (LAM x u = LAM x1 u1) ==> (u = [VAR x/x1]u1)`, 723PROVE_TAC [nc_INJECTIVITY,lemma14a]); 724 725val LAM_VAR_INJECTIVE = store_thm( 726 "LAM_VAR_INJECTIVE", 727 ``!x b1 b2. (LAM x b1 = LAM x b2) = (b1 = b2)``, 728 REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC std_ss [] THEN STRIP_TAC THEN 729 IMP_RES_THEN SUBST_ALL_TAC INJECTIVITY_LEMMA1 THEN 730 SIMP_TAC std_ss [lemma14a]); 731 732 733val lemma = 734 REWRITE_RULE [IN_UNION,IN_SING,DE_MORGAN_THM,IN_INSERT] 735 (Q.prove(`?gv:string. 736 ~(gv IN FV ^u UNION FV (u1:'a nc) UNION {x;x1})`, 737 MATCH_MP_TAC new_exists 738 THEN REWRITE_TAC [FINITE_UNION,FINITE_FV,FINITE_SING, 739 IN_INSERT,FINITE_INSERT,FINITE_EMPTY])); 740 741val INJECTIVITY_LEMMA2 = Q.store_thm("INJECTIVITY_LEMMA2", 742`!x u x' u1. 743 (LAM x u = LAM x' u1) 744 ==> 745 ?z. ~(z IN FV u) /\ ~(z IN FV u1) /\ ([VAR z/x] u = [VAR z/x'] u1)`, 746RW_TAC std_ss [] 747 THEN X_CHOOSE_THEN (Term`gv:string`) STRIP_ASSUME_TAC (GSYM lemma) 748 THEN let val ac1 = UNDISCH(Q.SPECL [`gv`, `u`] SIMPLE_ALPHA) 749 val ac2 = UNDISCH(Q.SPECL [`gv`,`u1`] SIMPLE_ALPHA) 750 in PURE_ONCE_REWRITE_TAC [ac1,ac2] 751 end 752 THEN RW_TAC std_ss [nc_INJECTIVITY] THEN PROVE_TAC []); 753 754val INJECTIVITY_LEMMA3 = Q.store_thm("INJECTIVITY_LEMMA3", 755`!x u x' u1. 756 (?z. ~(z IN FV ^u) /\ ~(z IN FV u1) /\ ([VAR z/x]u = [VAR z/x']u1)) 757 ==> 758 (LAM x u = LAM x' u1)`, 759PROVE_TAC [SIMPLE_ALPHA]); 760 761val LAM_INJ_ALPHA_FV = store_thm( 762 "LAM_INJ_ALPHA_FV", 763 ``!M N x y. (LAM x M = LAM y N) /\ ~(x = y) ==> 764 ~(x IN FV N) /\ ~(y IN FV M)``, 765 REPEAT STRIP_TAC THENL [ 766 `x IN FV (LAM y N)` by SRW_TAC [][FV_THM] THEN 767 `x IN FV (LAM x M)` by PROVE_TAC [], 768 `y IN FV (LAM x M)` by SRW_TAC [][FV_THM] THEN 769 `y IN FV (LAM y N)` by PROVE_TAC [] 770 ] THEN FULL_SIMP_TAC (srw_ss()) [FV_THM]); 771 772(* ===================================================================== *) 773(* Andy's second induction theorem -- follows easily. *) 774(* ===================================================================== *) 775 776val nc_INDUCTION2 = Q.store_thm ( 777 "nc_INDUCTION2", 778 `!P X. (!k. P(CON k)) /\ 779 (!x. P(VAR x)) /\ 780 (!t u. P t /\ P u ==> P(t @@ u)) /\ 781 (!y u. ~(y IN X) /\ P u ==> P(LAM y u)) /\ 782 FINITE X 783 ==> 784 !u. P u`, 785 REPEAT GEN_TAC THEN STRIP_TAC THEN nc_INDUCT_TAC THEN RW_TAC std_ss [] 786 THEN MP_TAC (Q.SPEC `FV ^u UNION X` new_exists) 787 THEN SRW_TAC [][] 788 THEN PROVE_TAC [SIMPLE_ALPHA]); 789 790(* --------------------------------------------------------------------- *) 791(* Induction tactic for this kind of induction. *) 792(* --------------------------------------------------------------------- *) 793 794fun nc_INDUCT_TAC2 q (A,g) = 795 let val (_,P) = dest_comb g 796 val ith = ISPEC P nc_INDUCTION2 797 fun bconv tm = 798 if rator tm !~ P then 799 raise mk_HOL_ERR "ncScript.sml" "nc_INDUCT_TAC2" 800 "function bconv failed" 801 else BETA_CONV tm 802 val bth = CONV_RULE (ONCE_DEPTH_CONV bconv) ith 803 in 804 (MATCH_MP_TAC bth THEN Q.EXISTS_TAC q THEN REPEAT CONJ_TAC 805 THENL [ALL_TAC, ALL_TAC, 806 GEN_TAC THEN GEN_TAC THEN STRIP_TAC, 807 GEN_TAC THEN GEN_TAC THEN 808 REWRITE_TAC [IN_UNION, IN_INSERT, IN_DELETE, 809 DE_MORGAN_THM] THEN 810 STRIP_TAC, 811 ALL_TAC]) (A,g) 812 end; 813 814(* ===================================================================== *) 815(* So, we can now prove some of Hindley and Seldin's theorems using both *) 816(* induction theorems. The comparison is interesting, as is the *) 817(* sensitivity to order of quantifiers. *) 818(* ===================================================================== *) 819 820(* --------------------------------------------------------------------- *) 821(* Andy's induction scheme. Fix both t and x. *) 822(* Compare the original proof of Andy's -- witness FV(u) + FV(t) + {x} *) 823(* --------------------------------------------------------------------- *) 824 825val lemma14b = Q.store_thm( 826 "lemma14b", 827 `!t x u. ~(x IN FV u) ==> ([t/x]u = u)`, 828 NTAC 2 GEN_TAC THEN nc_INDUCT_TAC2 `x INSERT FV t` THEN 829 SRW_TAC [][SUB_THM, SUB_VAR]); 830 831 832(* ---------------------------------------------------------------------- 833 Andy's induction scheme. Fix only t. This also works, but it does 834 force an unnecessary case split. 835 ---------------------------------------------------------------------- *) 836 837val lemma14b = Q.store_thm("lemma14b", 838 `!t u x. ~(x IN FV u) ==> ([t/x]u = u)`, 839 GEN_TAC THEN nc_INDUCT_TAC2 `FV t` THEN 840 SRW_TAC [][SUB_THM, SUB_VAR] THEN SRW_TAC [][SUB_THM] THEN 841 Cases_on `x = y` THEN SRW_TAC [][SUB_THM]); 842 843(* --------------------------------------------------------------------- *) 844(* The remaining Hindley and Seldin theorems. *) 845(* --------------------------------------------------------------------- *) 846 847val lemma14c = Q.store_thm( 848 "lemma14c", 849 `!t x u. x IN FV u ==> (FV ([t/x]u) = FV t UNION (FV u DELETE x))`, 850 NTAC 2 GEN_TAC THEN nc_INDUCT_TAC2 `x INSERT FV t` THEN 851 ASM_SIMP_TAC (srw_ss()) [SUB_THM, SUB_VAR, EXTENSION] THENL [ 852 STRIP_TAC THENL [ 853 Cases_on `x IN FV u` THEN SRW_TAC [][lemma14b] THEN METIS_TAC [], 854 Cases_on `x IN FV t'` THEN SRW_TAC [][lemma14b] THEN METIS_TAC [] 855 ], 856 METIS_TAC [] 857 ]); 858 859val lemma15a = Q.store_thm("lemma15a", 860 `!t y u. 861 ~(y IN FV u) ==> ([t/y]([VAR y/x]u) = [t/x]u)`, 862 NTAC 2 GEN_TAC THEN nc_INDUCT_TAC2 `{x;y} UNION FV t` THEN 863 SRW_TAC [][SUB_THM, SUB_VAR] THEN SRW_TAC [][SUB_VAR]); 864 865 866val lemma15b = Q.store_thm("lemma15b", 867`!y u. 868 ~(y IN FV u) ==> !x. [VAR x/y] ([VAR y/x]u) = u`, 869RW_TAC std_ss [lemma15a,lemma14a]); 870 871 872(* --------------------------------------------------------------------- *) 873(* BETA is definable given BODY. *) 874(* Needs Hindley and Seldin lemma15a. *) 875(* --------------------------------------------------------------------- *) 876 877val lemma = Q.prove( 878`!x u. (~((@y. ~(y IN (FV(LAM x u)))) IN (FV u))) 879 \/ 880 ((@y. ~(y IN (FV(LAM x u)))) = x)`, 881REWRITE_TAC [FV_THM,DE_MORGAN_THM,IN_DELETE] 882 THEN REPEAT GEN_TAC THEN CONV_TAC SELECT_CONV 883 THEN PROVE_TAC []); 884 885val BETA_EXISTS = Q.prove( 886 `?beta. 887 !u t x. beta (LAM x u) t = [t/x]u`, 888Q.EXISTS_TAC `\lam t. let x = @x. ~(x IN (FV lam)) in [t/x](BODY lam x)` 889 THEN RW_TAC std_ss [BODY_DEF, LET_THM] 890 THEN STRIP_ASSUME_TAC (SPEC_ALL lemma) 891 THEN RW_TAC std_ss [lemma15a,lemma14a]); 892 893val BETA = new_specification ("BETA_DEF", ["BETA"], BETA_EXISTS); 894 895(* --------------------------------------------------------------------- *) 896(* BODY is definable given BETA. *) 897(* --------------------------------------------------------------------- *) 898 899val lemma = Q.prove(`?body. !x u. body(LAM x ^u) = \y. [VAR y/x]u`, 900Q.EXISTS_TAC `\u y. BETA u (VAR y)` THEN RW_TAC std_ss [BETA]); 901 902 903(* ===================================================================== *) 904(* Iterated substitutions. *) 905(* ===================================================================== *) 906 907(* --------------------------------------------------------------------- *) 908(* t ISUB [(t1,x1),...,(tn,xn)] = t SUB (t1,x1) ... SUB (tn,xn) *) 909(* DOM [(t1,x1),...,(tn,xn)] = {x1,...,xn} *) 910(* FVS [(t1,x1),...,(tn,xn)] = FV t1 UNION ... UNION FV tn *) 911(* --------------------------------------------------------------------- *) 912 913val ISUB_def = 914 Define 915 `($ISUB t [] = t) 916 /\ ($ISUB t ((s,x)::rst) = $ISUB ([s/x]t) rst)`; 917 918val _ = set_fixity "ISUB" (Infixr 501); 919 920val DOM_DEF = 921 Define 922 `(DOM [] = {}) 923 /\ (DOM ((x,y)::rst) = {y} UNION DOM rst)`; 924 925val FVS_DEF = 926 Define 927 `(FVS [] = {}) 928 /\ (FVS ((t,x)::rst) = FV t UNION FVS rst)`; 929 930 931val FINITE_DOM = Q.store_thm("FINITE_DOM", 932 `!ss. FINITE (DOM ss)`, 933Induct THENL [ALL_TAC, Cases] 934 THEN RW_TAC std_ss [DOM_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_SING]); 935val _ = export_rewrites ["FINITE_DOM"] 936 937 938val FINITE_FVS = Q.store_thm("FINITE_FVS", 939`!ss. FINITE (FVS ss)`, 940Induct THENL [ALL_TAC, Cases] 941 THEN RW_TAC std_ss [FVS_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_FV]); 942val _ = export_rewrites ["FINITE_FVS"] 943 944 945(* --------------------------------------------------------------------- *) 946(* A renaming is a parallel substitution of variables for variables. *) 947(* *) 948(* RENAMING [] always *) 949(* RENAMING ((x,VAR y)::R) if RENAMING R *) 950(* --------------------------------------------------------------------- *) 951 952val (RENAMING_DEF,RENAMING_IND,RENAMING_CASES) = Hol_reln 953 `RENAMING ([]:('a nc # string) list) 954 /\ (!R x y. RENAMING R ==> RENAMING ((VAR y,x)::R))`; 955 956val _ = save_thm("RENAMING_DEF",RENAMING_DEF); 957val _ = save_thm("RENAMING_IND",RENAMING_IND); 958val _ = save_thm("RENAMING_CASES",RENAMING_CASES); 959 960val RENAME_DEF = 961 Define 962 `(RENAME [] x = x) 963 /\ (RENAME ((p,q)::ss) x = RENAME ss (if x=q then VNAME p else x))`; 964 965 966val RENAMING_LEMMA = Q.store_thm("RENAMING_LEMMA", 967`!ss. RENAMING ss 968 ==> 969 !tt. RENAMING tt ==> RENAMING (APPEND ss tt)`, 970HO_MATCH_MP_TAC RENAMING_IND 971 THEN RW_TAC list_ss [] 972 THEN PROVE_TAC [RENAMING_CASES]); 973 974(* ---------------------------------------------------------------------- 975 Simple properties of ISUB 976 ---------------------------------------------------------------------- *) 977 978val SUB_ISUB_SINGLETON = store_thm( 979 "SUB_ISUB_SINGLETON", 980 ``!t x u. [t/x]u = u ISUB [(t,x)]``, 981 SRW_TAC [][ISUB_def]); 982 983val ISUB_APPEND = store_thm( 984 "ISUB_APPEND", 985 ``!R1 R2 t. (t ISUB R1) ISUB R2 = t ISUB (APPEND R1 R2)``, 986 Induct THEN 987 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, ISUB_def]); 988 989(* ---------------------------------------------------------------------- 990 ... and of RENAMING 991 ---------------------------------------------------------------------- *) 992 993val _ = temp_type_abbrev("renaming", ``:('a nc # string) list``) 994val RENAMING_THM = store_thm( 995 "RENAMING_THM", 996 ``RENAMING ([]:'a renaming) /\ 997 (!(R:'a renaming) h. 998 RENAMING (h::R) ��� RENAMING R /\ ?y x. h = (VAR y,x)) /\ 999 (!R1 R2:'a renaming. 1000 RENAMING (APPEND R1 R2) ��� RENAMING R1 /\ RENAMING R2)``, 1001 Q.SUBGOAL_THEN 1002 `RENAMING ([]:'a renaming) /\ 1003 (!R:'a renaming h. 1004 RENAMING (h::R) ��� RENAMING R /\ ?y x. h = (VAR y,x))` 1005 (fn th => STRIP_ASSUME_TAC th THEN ASM_REWRITE_TAC []) 1006 THENL [ 1007 SIMP_TAC (srw_ss()) [RENAMING_DEF] THEN REPEAT GEN_TAC THEN 1008 CONV_TAC (LAND_CONV (REWR_CONV RENAMING_CASES)) THEN SRW_TAC [][] THEN 1009 PROVE_TAC [], 1010 Induct THEN SRW_TAC [][] THEN PROVE_TAC [] 1011 ]); 1012 1013 1014(* --------------------------------------------------------------------- *) 1015(* Interaction of ISUB with syntax constructors. *) 1016(* --------------------------------------------------------------------- *) 1017 1018val R = Term `R : ('a nc # string) list`; 1019 1020 1021val ISUB_VAR_RENAME = Q.store_thm("ISUB_VAR_RENAME", 1022`!ss. RENAMING ss 1023 ==> 1024 !x. (VAR x) ISUB ss = VAR (RENAME ss x)`, 1025HO_MATCH_MP_TAC RENAMING_IND 1026 THEN RW_TAC std_ss [ISUB_def, RENAME_DEF, VNAME_DEF, SUB_VAR] 1027 THEN RW_TAC std_ss []); 1028 1029val ISUB_CON = Q.store_thm("ISUB_CON", 1030`!^R k. (CON k) ISUB ^R = CON k`, 1031Induct THEN Ho_Rewrite.REWRITE_TAC[pairTheory.FORALL_PROD] 1032 THEN RW_TAC std_ss [ISUB_def, SUB_THM]); 1033 1034val ISUB_APP = Q.store_thm("ISUB_APP", 1035`!^R t u. (t @@ u) ISUB ^R = (t ISUB ^R) @@ (u ISUB ^R)`, 1036Induct THEN Ho_Rewrite.REWRITE_TAC[pairTheory.FORALL_PROD] 1037 THEN RW_TAC std_ss [ISUB_def, SUB_THM]); 1038 1039val ISUB_LAM = Q.store_thm("ISUB_LAM", 1040`!^R x. ~(x IN (DOM ^R UNION FVS ^R)) 1041 ==> 1042 !t. (LAM x t) ISUB ^R = LAM x (t ISUB ^R)`, 1043Induct THENL 1044 [ALL_TAC, Ho_Rewrite.REWRITE_TAC[pairTheory.FORALL_PROD] 1045 THEN Cases_on `x` THEN POP_ASSUM MP_TAC] 1046 THEN RW_TAC list_ss 1047 [ISUB_def,DOM_DEF,FVS_DEF,FV_THM,IN_UNION,IN_SING,DE_MORGAN_THM,SUB_THM]); 1048 1049val _ = export_rewrites ["nc_DISTINCT","nc_INJECTIVITY", "LAM_VAR_INJECTIVE"]; 1050 1051 1052val FV_SUB = store_thm( 1053 "FV_SUB", 1054 ``!t u v. FV ([t/v] u) = if v IN FV u then FV t UNION (FV u DELETE v) 1055 else FV u``, 1056 PROVE_TAC [lemma14b, lemma14c]); 1057 1058val nc_RECURSION2 = save_thm( 1059 "nc_RECURSION2", 1060 (SIMP_RULE bool_ss [ABS_DEF] o 1061 Q.INST [`lam'` |-> `lam`] o 1062 Q.INST [`lam` |-> `\r t. let v = NEW (FV (ABS t) UNION X) 1063 in lam' (r v) v (t v)`] o 1064 SPEC_ALL) nc_RECURSION) 1065 1066val size_def = new_specification ( 1067 "size", ["size"], 1068 (CONJUNCT1 o 1069 CONV_RULE EXISTS_UNIQUE_CONV o 1070 SIMP_RULE bool_ss [pred_setTheory.UNION_EMPTY] o 1071 Q.INST [`con` |-> `\x. 1`, `var` |-> `\s. 1`, 1072 `app` |-> `\rt ru t u. rt + ru + 1`, 1073 `lam` |-> `\rt v t. rt + 1`, 1074 `X` |-> `{}`] o 1075 INST_TYPE [beta |-> numSyntax.num]) nc_RECURSION2) 1076 1077val _ = augment_srw_ss [rewrites [LET_THM]] 1078val size_isub = store_thm( 1079 "size_isub", 1080 ``!t R. RENAMING R ==> (size (t ISUB R) = size t)``, 1081 HO_MATCH_MP_TAC nc_INDUCTION THEN REPEAT CONJ_TAC THENL [ 1082 SRW_TAC [][ISUB_CON, size_def], 1083 SRW_TAC [][ISUB_VAR_RENAME, size_def], 1084 SRW_TAC [][ISUB_APP, size_def], 1085 REPEAT STRIP_TAC THEN 1086 Q.ABBREV_TAC `avds = FVS R UNION DOM R UNION FV t` THEN 1087 `FINITE avds` 1088 by (Q.UNABBREV_TAC `avds` THEN 1089 SRW_TAC [][FINITE_FVS, FINITE_DOM, FINITE_FV]) THEN 1090 Q.ABBREV_TAC `z = NEW avds` THEN 1091 `~(z IN avds)` 1092 by (Q.UNABBREV_TAC `z` THEN SRW_TAC [][NEW_def]) THEN 1093 `~(z IN FVS R) /\ ~(z IN DOM R) /\ ~(z IN FV t)` 1094 by (Q.UNABBREV_TAC `z` THEN Q.UNABBREV_TAC `avds` THEN 1095 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []) THEN 1096 REPEAT (Q.PAT_X_ASSUM `Abbrev X` (K ALL_TAC)) THEN 1097 `LAM x t = LAM z ([VAR z/x] t)` by SRW_TAC [][SIMPLE_ALPHA] THEN 1098 SRW_TAC [][ISUB_LAM] THEN 1099 ASM_SIMP_TAC bool_ss [size_def] THEN 1100 ONCE_REWRITE_TAC [SUB_ISUB_SINGLETON] THEN 1101 ASM_SIMP_TAC bool_ss [ISUB_APPEND,RENAMING_DEF, RENAMING_LEMMA] THEN 1102 SRW_TAC [][] 1103 ]); 1104 1105val size_vsubst = store_thm( 1106 "size_vsubst", 1107 ``size ([VAR v/u] t) = size t``, 1108 SRW_TAC [][size_isub, SUB_ISUB_SINGLETON, RENAMING_DEF]); 1109val _ = export_rewrites ["size_vsubst"] 1110 1111val size_thm = save_thm( 1112 "size_thm", 1113 SIMP_RULE (srw_ss()) [size_vsubst] size_def); 1114 1115val size_nonzero = store_thm( 1116 "size_nonzero", 1117 ``!t. 0 < size t``, 1118 HO_MATCH_MP_TAC nc_INDUCTION THEN SRW_TAC [numSimps.ARITH_ss][size_thm]); 1119 1120val _ = export_theory(); 1121