1open HolKernel boolLib bossLib Parse binderLib 2 3open chap3Theory 4open pred_setTheory 5open termTheory 6open boolSimps 7open normal_orderTheory 8open churchboolTheory 9open churchpairTheory 10open reductionEval 11open stepsTheory 12 13fun Store_thm(n,t,tac) = store_thm(n,t,tac) before export_rewrites [n] 14 15val _ = new_theory "churchnum" 16 17val _ = set_trace "Unicode" 1 18 19val church_def = Define` 20 church n = LAM "z" (LAM "s" (FUNPOW (APP (VAR "s")) n (VAR "z"))) 21` 22 23val FUNPOW_SUC = arithmeticTheory.FUNPOW_SUC 24 25val size_funpow = store_thm( 26 "size_funpow", 27 ``size (FUNPOW (APP f) n x) = (size f + 1) * n + size x``, 28 Induct_on `n` THEN 29 SRW_TAC [ARITH_ss][FUNPOW_SUC, arithmeticTheory.LEFT_ADD_DISTRIB, 30 arithmeticTheory.MULT_CLAUSES]); 31 32val church_11 = store_thm( 33 "church_11", 34 ``(church m = church n) ��� (m = n)``, 35 SRW_TAC [][church_def, EQ_IMP_THM] THEN 36 POP_ASSUM (MP_TAC o Q.AP_TERM `size`) THEN 37 SRW_TAC [ARITH_ss][size_funpow, arithmeticTheory.LEFT_ADD_DISTRIB]); 38val _ = export_rewrites ["church_11"] 39 40val bnf_church = store_thm( 41 "bnf_church", 42 ``���n. bnf (church n)``, 43 SRW_TAC [][church_def] THEN 44 Induct_on `n` THEN SRW_TAC [][] THEN 45 SRW_TAC [][FUNPOW_SUC]); 46val _ = export_rewrites ["bnf_church"] 47 48val is_abs_church = Store_thm( 49 "is_abs_church", 50 ``is_abs (church n)``, 51 SRW_TAC [][church_def]); 52 53val church_lameq_11 = Store_thm( 54 "church_lameq_11", 55 ``(church m == church n) ��� (m = n)``, 56 SRW_TAC [][EQ_IMP_THM, chap2Theory.lameq_rules] THEN 57 `���Z. church m -��->* Z ��� church n -��->* Z` 58 by METIS_TAC [beta_CR, theorem3_13, prop3_18] THEN 59 `church m = church n` 60 by METIS_TAC [corollary3_2_1, beta_normal_form_bnf, bnf_church] THEN 61 FULL_SIMP_TAC (srw_ss()) []); 62 63val FV_church = store_thm( 64 "FV_church", 65 ``FV (church n) = {}``, 66 SRW_TAC [][church_def] THEN 67 `(n = 0) ��� (���m. n = SUC m)` 68 by METIS_TAC [TypeBase.nchotomy_of ``:num``] THEN 69 SRW_TAC [][] THENL [ 70 SRW_TAC [CONJ_ss] [EXTENSION], 71 Q_TAC SUFF_TAC 72 `FV (FUNPOW (APP (VAR "s")) (SUC m) (VAR "z")) = {"s"; "z"}` 73 THEN1 SRW_TAC [CONJ_ss][pred_setTheory.EXTENSION] THEN 74 Induct_on `m` THEN SRW_TAC [][] THENL [ 75 SRW_TAC [][EXTENSION], 76 SRW_TAC [][Once FUNPOW_SUC] THEN 77 SRW_TAC [][EXTENSION] THEN METIS_TAC [] 78 ] 79 ]); 80val _ = export_rewrites ["FV_church"] 81 82val is_church_def = Define` 83 is_church t = 84 ���f z n. f ��� z ��� (t = LAM z (LAM f (FUNPOW (APP (VAR f)) n (VAR z)))) 85`; 86 87 88val church_is_church = Store_thm( 89 "church_is_church", 90 ``is_church (church n)``, 91 SRW_TAC [][is_church_def, church_def] THEN 92 `"z" ��� "s"` by SRW_TAC [][] THEN METIS_TAC []); 93 94val force_num_def = Define` 95 force_num t = if is_church t then (@n. t = church n) else 0 96`; 97 98val force_num_church = Store_thm( 99 "force_num_church", 100 ``force_num (church n) = n``, 101 SRW_TAC [][force_num_def]); 102 103val force_num_church_composed = Store_thm( 104 "force_num_church_composed", 105 ``(force_num o church o f = f) ��� 106 (force_num o church = I)``, 107 SRW_TAC [][FUN_EQ_THM]); 108 109val tpm_funpow_app = store_thm( 110 "tpm_funpow_app", 111 ``tpm pi (FUNPOW (APP f) n x) = FUNPOW (APP (tpm pi f)) n (tpm pi x)``, 112 Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]); 113val _ = export_rewrites ["tpm_funpow_app"] 114 115val FV_funpow_app = store_thm( 116 "FV_funpow_app", 117 ``FV (FUNPOW (APP f) n x) ��� FV f ��� FV x``, 118 Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]); 119 120val FV_funpow_app_I = store_thm( 121 "FV_funpow_app_I", 122 ``v ��� FV x ��� v ��� FV (FUNPOW (APP f) n x)``, 123 Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]); 124 125val FV_funpow_app_E = store_thm( 126 "FV_funpow_app_E", 127 ``v ��� FV (FUNPOW (APP f) n x) ��� v ��� FV f ��� v ��� FV x``, 128 MATCH_ACCEPT_TAC (REWRITE_RULE [IN_UNION, SUBSET_DEF] FV_funpow_app)); 129 130val fresh_funpow_app_I = store_thm( 131 "fresh_funpow_app_I", 132 ``v ��� FV f ��� v ��� FV x ��� v ��� FV (FUNPOW (APP f) n x)``, 133 METIS_TAC [FV_funpow_app_E]); 134val _ = export_rewrites ["fresh_funpow_app_I"] 135 136val is_church_church = store_thm( 137 "is_church_church", 138 ``is_church t ��� ���n. t = church n``, 139 SRW_TAC [][is_church_def, church_def] THEN 140 Q.EXISTS_TAC `n` THEN SRW_TAC [CONJ_ss][LAM_eq_thm] THEN 141 Cases_on `z = "z"` THEN SRW_TAC [CONJ_ss][] THEN 142 Cases_on `z = "s"` THEN SRW_TAC [CONJ_ss][]); 143 144val force_num_size = store_thm( 145 "force_num_size", 146 ``is_church t ��� (force_num t = size t DIV 2 - 1)``, 147 SRW_TAC [][force_num_def] THEN 148 `���n. t = church n` by METIS_TAC [is_church_church] THEN 149 SRW_TAC [ARITH_ss][church_def, size_funpow] THEN 150 Q_TAC SUFF_TAC `(2 * n + 3) DIV 2 = n + 1` THEN1 DECIDE_TAC THEN 151 MATCH_MP_TAC arithmeticTheory.DIV_UNIQUE THEN Q.EXISTS_TAC `1` THEN 152 DECIDE_TAC); 153 154 155 156 157val SUB_funpow_app = store_thm( 158 "SUB_funpow_app", 159 ``[M:term/v] (FUNPOW (APP f) n x) = FUNPOW (APP ([M/v]f)) n ([M/v]x)``, 160 Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]); 161val _ = export_rewrites ["SUB_funpow_app"] 162 163val church_thm = bstore_thm( 164 "church_thm", 165 ``church 0 @@ x @@ f == x ��� 166 church (SUC n) @@ x @@ f == f @@ (church n @@ x @@ f)``, 167 CONJ_TAC THENL [ 168 SIMP_TAC (bsrw_ss()) [church_def] THEN FRESH_TAC THEN 169 ASM_SIMP_TAC (bsrw_ss()) [], 170 171 SIMP_TAC (bsrw_ss()) [church_def] THEN FRESH_TAC THEN 172 ASM_SIMP_TAC (bsrw_ss()) [FUNPOW_SUC] 173 ]); 174 175val csuc_def = Define` 176 csuc = LAM "n" (LAM "z" (LAM "s" 177 (VAR "s" @@ (VAR "n" @@ VAR "z" @@ VAR "s")))) 178`; 179val FV_csuc = Store_thm( 180 "FV_csuc", 181 ``FV csuc = {}``, 182 SRW_TAC [][csuc_def, EXTENSION] THEN METIS_TAC []); 183val bnf_csuc = Store_thm( 184 "bnf_csuc", 185 ``bnf csuc``, 186 SRW_TAC [][csuc_def]); 187 188val csuc_behaviour = bstore_thm( 189 "csuc_behaviour", 190 ``���n. (csuc @@ (church n)) -n->* church (SUC n)``, 191 SIMP_TAC (bsrw_ss()) [csuc_def, church_def, FUNPOW_SUC]); 192 193val church_eq = store_thm( 194 "church_eq", 195 ``(���s. church n ��� VAR s) ��� (���M N. church n ��� M @@ N)``, 196 SRW_TAC [][church_def]); 197val _ = export_rewrites ["church_eq"] 198 199val natrec_def = Define` 200 natrec = LAM "z" (LAM "f" (LAM "n" ( 201 csnd @@ (VAR "n" 202 @@ (cpair @@ church 0 @@ VAR "z") 203 @@ (LAM "r" (cpair 204 @@ (csuc @@ (cfst @@ VAR "r")) 205 @@ (VAR "f" @@ (cfst @@ VAR "r") 206 @@ (csnd @@ VAR "r")))))))) 207`; 208 209val FV_natrec = Store_thm( 210 "FV_natrec", 211 ``FV natrec = {}``, 212 SRW_TAC [][natrec_def, EXTENSION] THEN METIS_TAC []); 213infix |> fun x |> f = f x 214val lameq_sub = chap2Theory.lemma2_12 |> CONJUNCTS 215 |> hd 216 |> UNDISCH 217 |> GEN_ALL 218 |> DISCH_ALL 219 |> GEN_ALL 220 221val natrec_behaviour = bstore_thm( 222 "natrec_behaviour", 223 ``natrec @@ z @@ f @@ church 0 == z ��� 224 natrec @@ z @@ f @@ church (SUC n) == 225 f @@ church n @@ (natrec @@ z @@ f @@ church n)``, 226 CONJ_TAC THENL [ 227 SIMP_TAC (srw_ss()) [natrec_def] THEN FRESH_TAC THEN 228 SRW_TAC [][tpm_fresh, lemma14b] THEN 229 ASM_SIMP_TAC (bsrw_ss()) [], 230 231 SIMP_TAC (srw_ss()) [natrec_def] THEN unvarify_tac lameq_sub THEN 232 ASM_SIMP_TAC (bsrw_ss()) [] THEN 233 Q.MATCH_ABBREV_TAC 234 `VAR fs @@ NN0 @@ YY == VAR fs @@ NN1 @@ YY` THEN 235 Q_TAC SUFF_TAC `NN0 == NN1` THEN1 SIMP_TAC (bsrw_ss()) [] THEN 236 markerLib.UNABBREV_ALL_TAC THEN 237 Q.ID_SPEC_TAC `n` THEN Induct THEN ASM_SIMP_TAC (bsrw_ss()) [] 238 ]); 239 240val cplus_def = Define` 241 cplus = LAM "m" (LAM "n" (VAR "m" @@ VAR "n" @@ csuc)) 242`; 243 244val FV_cplus = Store_thm( 245 "FV_cplus", 246 ``FV cplus = {}``, 247 SRW_TAC [][cplus_def, EXTENSION] THEN METIS_TAC []); 248val is_abs_cplus = Store_thm( 249 "is_abs_cplus", 250 ``is_abs cplus``, 251 SRW_TAC [][cplus_def]); 252 253val cplus_behaviour = bstore_thm( 254 "cplus_behaviour", 255 ``cplus @@ church m @@ church n -n->* church (m + n)``, 256 SIMP_TAC (bsrw_ss()) [cplus_def] THEN Induct_on `m` THEN 257 ASM_SIMP_TAC (bsrw_ss()) [arithmeticTheory.ADD_CLAUSES]); 258 259val cpred_def = Define` 260 cpred = LAM "n" (natrec @@ church 0 261 @@ (LAM "n0" (LAM "r" (VAR "n0"))) 262 @@ (VAR "n")) 263`; 264val FV_cpred = store_thm( 265 "FV_cpred", 266 ``FV cpred = {}``, 267 SRW_TAC [][cpred_def, EXTENSION] THEN 268 METIS_TAC []); 269val _ = export_rewrites ["FV_cpred"] 270 271val cpred_0 = store_thm( 272 "cpred_0", 273 ``cpred @@ church 0 -n->* church 0``, 274 SIMP_TAC (bsrw_ss()) [cpred_def]); 275 276val cpred_SUC = store_thm( 277 "cpred_SUC", 278 ``cpred @@ church (SUC n) -n->* church n``, 279 SIMP_TAC (bsrw_ss()) [cpred_def]); 280 281val cpred_behaviour = bstore_thm( 282 "cpred_behaviour", 283 ``cpred @@ church n -n->* church (PRE n)``, 284 Cases_on `n` THEN SRW_TAC [][cpred_SUC, cpred_0]); 285 286val cminus_def = Define` 287 cminus = LAM "m" (LAM "n" (VAR "n" @@ VAR "m" @@ cpred)) 288`; 289val FV_cminus = Store_thm( 290 "FV_cminus", 291 ``FV cminus = {}``, 292 SRW_TAC [][cminus_def, EXTENSION] THEN METIS_TAC []); 293val is_abs_cminus = Store_thm( 294 "is_abs_cminus", 295 ``is_abs cminus``, 296 SRW_TAC [][cminus_def]); 297 298val cminus_behaviour = bstore_thm( 299 "cminus_behaviour", 300 ``cminus @@ church m @@ church n -n->* church (m - n)``, 301 SIMP_TAC (bsrw_ss()) [cminus_def] THEN 302 Q.ID_SPEC_TAC `m` THEN Induct_on `n` THEN 303 ASM_SIMP_TAC (bsrw_ss()) [DECIDE ``m - SUC n = PRE (m - n)``]); 304 305val cmult_def = Define` 306 cmult = LAM "m" (LAM "n" (VAR "m" @@ church 0 @@ (cplus @@ VAR "n"))) 307`; 308val FV_cmult = Store_thm( 309 "FV_cmult", 310 ``FV cmult = {}``, 311 SRW_TAC [][cmult_def, EXTENSION] THEN METIS_TAC []); 312 313val cmult_behaviour = bstore_thm( 314 "cmult_behaviour", 315 ``cmult @@ church m @@ church n -n->* church (m * n)``, 316 SIMP_TAC (bsrw_ss()) [cmult_def] THEN Induct_on `m` THEN 317 ASM_SIMP_TAC (bsrw_ss() ++ ARITH_ss) [arithmeticTheory.MULT_CLAUSES]); 318 319(* predicates/relations *) 320val cis_zero_def = Define` 321 cis_zero = LAM "n" (VAR "n" @@ cB T @@ (LAM "x" (cB F))) 322`; 323val FV_cis_zero = Store_thm( 324 "FV_cis_zero", 325 ``FV cis_zero = {}``, 326 SRW_TAC [][cis_zero_def, EXTENSION]); 327val bnf_cis_zero = Store_thm( 328 "bnf_cis_zero", 329 ``bnf cis_zero``, 330 SRW_TAC [][cis_zero_def]); 331 332val cis_zero_behaviour = bstore_thm( 333 "cis_zero_behaviour", 334 ``cis_zero @@ church n -n->* cB (n = 0)``, 335 Cases_on `n` THEN 336 ASM_SIMP_TAC (bsrw_ss()) [cis_zero_def]); 337 338val wh_cis_zero = store_thm( 339 "wh_cis_zero", 340 ``cis_zero @@ church n -w->* cB (n = 0)``, 341 SRW_TAC [][cis_zero_def, church_def] THEN 342 ASM_SIMP_TAC (whfy(srw_ss())) [] THEN 343 Cases_on `n` THEN SRW_TAC [][FUNPOW_SUC] THEN 344 ASM_SIMP_TAC (whfy(srw_ss())) []); 345 346val ceqnat_def = Define` 347 ceqnat = 348 LAM "n" 349 (VAR "n" 350 @@ cis_zero 351 @@ (LAM "r" (LAM "m" 352 (cand @@ (cnot @@ (cis_zero @@ (VAR "m"))) 353 @@ (VAR "r" @@ (cpred @@ (VAR "m"))))))) 354`; 355val FV_ceqnat = Store_thm( 356 "FV_ceqnat", 357 ``FV ceqnat = {}``, 358 SRW_TAC [][ceqnat_def, EXTENSION] THEN METIS_TAC []); 359 360val ceqnat_behaviour = bstore_thm( 361 "ceqnat_behaviour", 362 ``ceqnat @@ church n @@ church m -n->* cB (n = m)``, 363 SIMP_TAC (bsrw_ss()) [ceqnat_def] THEN 364 Q.ID_SPEC_TAC `m` THEN Induct_on `n` THEN1 365 SIMP_TAC (bsrw_ss()) [EQ_SYM_EQ] THEN 366 ASM_SIMP_TAC (bsrw_ss()) [] THEN 367 Cases_on `m` THEN SRW_TAC [][]) 368 369(* $< 0 = ��n. not (is_zero n) 370 $< (SUC m) = ��n. not (is_zero n) ��� $< m (PRE n) 371*) 372val cless_def = Define` 373 cless = LAM "m" 374 (VAR "m" @@ (LAM "n" (cnot @@ (cis_zero @@ VAR "n"))) 375 @@ (LAM "r" 376 (LAM "n" (cand 377 @@ (cnot @@ (cis_zero @@ VAR "n")) 378 @@ (VAR "r" @@ (cpred @@ VAR "n")))))) 379`; 380val FV_cless = Store_thm( 381 "FV_cless", 382 ``FV cless = {}``, 383 SRW_TAC [][cless_def, EXTENSION] THEN METIS_TAC []); 384val is_abs_cless = Store_thm( 385 "is_abs_cless", 386 ``is_abs cless``, 387 SRW_TAC [][cless_def]); 388 389val cless_behaviour = bstore_thm( 390 "cless_behaviour", 391 ``cless @@ church m @@ church n -n->* cB (m < n)``, 392 SIMP_TAC (bsrw_ss()) [cless_def] THEN 393 Q.ID_SPEC_TAC `n` THEN Induct_on `m` THENL [ 394 SIMP_TAC (bsrw_ss()) [arithmeticTheory.NOT_ZERO_LT_ZERO], 395 ASM_SIMP_TAC (bsrw_ss()) [] THEN 396 Cases_on `n` THEN SRW_TAC [][] 397 ]); 398 399(* ---------------------------------------------------------------------- 400 divmod 401 402 Functional presentation would be 403 404 divmod (a,p,q) = if q = 0 then (0,0) else 405 if p < q then (a,p) 406 else divmod (a+1,p-q,q) 407 408 But this is not primitive recursive. We make it so by passing in 409 an extra argument which is the "target" value for the next recursive 410 step. The primitive recursion does nothing until it hits a target 411 value, which it then can set up appropriately for the next bit. 412 413 In this setting the "target" is parameter p, which is where the 414 recursion is happening. 415 416 divmod 0 (a,p,q) = if p < q then (a,p) else (0,0) 417 divmod (SUC n) (a,p,q) = 418 if SUC n = p then 419 if p < q then (a,p) 420 else divmod n (a+1,p-q,q) 421 else divmod n (a,p,q) 422 423 We can optimise a little by having q be lifted past the recursion. 424 425 ---------------------------------------------------------------------- *) 426 427val cdivmodt_def = Define` 428 cdivmodt = LAM "q" 429 (LAM "n" 430 (natrec 431 @@ cpair 432 @@ (LAM "n0" (LAM "r" (LAM "a" (LAM "p" 433 (ceqnat @@ (csuc @@ VAR "n0") @@ VAR "p" 434 @@ (cless @@ VAR "p" @@ VAR "q" 435 @@ (cpair @@ VAR "a" @@ VAR "p") 436 @@ (VAR "r" @@ 437 (csuc @@ VAR "a") @@ 438 (cminus @@ VAR "p" @@ VAR "q"))) 439 @@ (VAR "r" @@ VAR "a" @@ VAR "p")))))) 440 @@ VAR "n")) 441`; 442 443val FV_cdivmodt = Store_thm( 444 "FV_cdivmodt", 445 ``FV cdivmodt = {}``, 446 SRW_TAC [][cdivmodt_def, EXTENSION] THEN METIS_TAC []); 447 448val cdivmodt_behaviour = store_thm( 449 "cdivmodt_behaviour", 450 ``���p a. 451 0 < q ��� p ��� n ��� 452 cdivmodt @@ church q @@ church n @@ church a @@ church p -n->* 453 cvpr (church (a + p DIV q)) (church (p MOD q))``, 454 SIMP_TAC (bsrw_ss()) [cdivmodt_def, cpair_behaviour] THEN 455 Induct_on `n` THENL [ 456 SIMP_TAC (bsrw_ss()) [arithmeticTheory.ZERO_DIV, cpair_behaviour], 457 458 ASM_SIMP_TAC (bsrw_ss()) [] THEN 459 REPEAT STRIP_TAC THEN 460 Cases_on `p = SUC n` THEN ASM_SIMP_TAC (bsrw_ss()) [] THENL [ 461 Cases_on `SUC n < q` THEN ASM_SIMP_TAC (bsrw_ss()) [] THENL [ 462 ASM_SIMP_TAC (bsrw_ss()) [arithmeticTheory.LESS_DIV_EQ_ZERO], 463 ASM_SIMP_TAC (bsrw_ss() ++ ARITH_ss) [] THEN 464 `(SUC n - q) DIV q = SUC n DIV q - 1` 465 by (MP_TAC (Q.INST [`n` |-> `q`, `q` |-> `1`, 466 `m` |-> `SUC n`] 467 arithmeticTheory.DIV_SUB) THEN 468 SRW_TAC [ARITH_ss][]) THEN 469 `(SUC n - q) MOD q = SUC n MOD q` 470 by (MP_TAC (Q.INST [`n` |-> `q`, `q` |-> `1`, `m` |-> `SUC n`] 471 arithmeticTheory.MOD_SUB) THEN 472 SRW_TAC [ARITH_ss][]) THEN 473 SRW_TAC [ARITH_ss][] THEN 474 `���x y. (x = y) ��� x == y` by SRW_TAC [][] THEN 475 POP_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN 476 Q_TAC SUFF_TAC `0 < SUC n DIV q` THEN1 DECIDE_TAC THEN 477 SRW_TAC [ARITH_ss][arithmeticTheory.X_LT_DIV] 478 ], 479 SRW_TAC [ARITH_ss][] 480 ] 481 ]); 482 483val cdiv_def = Define` 484 cdiv = 485 LAM "p" (LAM "q" 486 (cfst @@ (cdivmodt @@ VAR "q" @@ VAR "p" @@ church 0 @@ VAR "p"))) 487` 488val FV_cdiv = Store_thm( 489 "FV_cdiv", 490 ``FV cdiv = {}``, 491 SIMP_TAC bool_ss [cdiv_def, EXTENSION, NOT_IN_EMPTY] THEN 492 SRW_TAC [][FRESH_APP, FRESH_LAM]); 493 494val cdiv_behaviour = bstore_thm( 495 "cdiv_behaviour", 496 ``0 < q ��� 497 cdiv @@ church p @@ church q -n->* church (p DIV q)``, 498 SIMP_TAC (bsrw_ss()) [cdivmodt_behaviour, cdiv_def]); 499 500val cmod_def = Define` 501 cmod = LAM "p" (LAM "q" 502 (csnd @@ (cdivmodt @@ VAR "q" @@ VAR "p" @@ church 0 @@ VAR "p"))) 503`; 504val FV_cmod = Store_thm( 505 "FV_cmod", 506 ``FV cmod = {}``, 507 SRW_TAC [][cmod_def, EXTENSION] THEN METIS_TAC []) 508 509val cmod_behaviour = bstore_thm( 510 "cmod_behaviour", 511 ``0 < q ��� 512 cmod @@ church p @@ church q -n->* church (p MOD q)``, 513 SIMP_TAC (bsrw_ss()) [cdivmodt_behaviour, cmod_def]); 514 515(* ---------------------------------------------------------------------- 516 Pairs of numbers 517 ---------------------------------------------------------------------- *) 518 519val cnvpr_def = Define` 520 cnvpr (n,m) = cvpr (church n) (church m) 521`; 522 523val bnf_cnvpr = Store_thm( 524 "bnf_cnvpr", 525 ``bnf (cnvpr p)``, 526 Cases_on `p` THEN SRW_TAC [][cnvpr_def]); 527 528val FV_cnvpr = Store_thm( 529 "FV_cnvpr", 530 ``FV (cnvpr p) = {}``, 531 Cases_on `p` THEN SRW_TAC [][cnvpr_def]); 532 533val cfst_cnvpr = bstore_thm( 534 "cfst_cnvpr", 535 ``cfst @@ cnvpr p -n->* church (FST p)``, 536 Cases_on `p` THEN SIMP_TAC (bsrw_ss())[cnvpr_def]); 537val csnd_cnvpr = bstore_thm( 538 "csnd_cnvpr", 539 ``csnd @@ cnvpr p -n->* church (SND p)``, 540 Cases_on `p` THEN SIMP_TAC (bsrw_ss())[cnvpr_def]); 541 542 543(* ---------------------------------------------------------------------- 544 Numeric pairing 545 ---------------------------------------------------------------------- *) 546 547open numpairTheory 548 549(* triangular numbers and the tri����� function *) 550val ctri_def = Define` 551 ctri = LAM "n" (natrec @@ church 0 552 @@ (LAM "n0" (cplus @@ (csuc @@ VAR "n0"))) 553 @@ VAR "n") 554`; 555 556val FV_ctri = Store_thm( 557 "FV_ctri", 558 ``FV ctri = {}``, 559 SRW_TAC [][ctri_def, EXTENSION] THEN METIS_TAC []); 560 561val ctri_behaviour = bstore_thm( 562 "ctri_behaviour", 563 ``ctri @@ church n -n->* church (tri n)``, 564 SIMP_TAC (bsrw_ss()) [ctri_def] THEN 565 Induct_on `n` THEN 566 ASM_SIMP_TAC (bsrw_ss()) [tri_def]); 567 568(* invtri0 569 |- ���n a. 570 invtri0 n a = 571 if n < a + 1 then (n,a) else invtri0 (n ��� (a + 1)) (a + 1) : thm 572 make it prim. rec. by using a target parameter, as with divmod 573*) 574 575val cinvtri0_def = Define` 576 cinvtri0 = 577 natrec 578 @@ (LAM "n" (LAM "a" (cvpr (VAR "n") (VAR "a")))) 579 @@ (LAM "t0" (LAM "r" (LAM "n" (LAM "a" 580 (ceqnat @@ (csuc @@ (VAR "t0")) @@ VAR "n" 581 @@ (cless @@ VAR "n" @@ (csuc @@ VAR "a") 582 @@ cvpr (VAR "n") (VAR "a") 583 @@ (VAR "r" 584 @@ (cminus @@ VAR "n" 585 @@ (csuc @@ VAR "a")) 586 @@ (csuc @@ VAR "a"))) 587 @@ (VAR "r" @@ VAR "n" @@ VAR "a")))))) 588`; 589(* have messed my naming up here in order to keep the "n" and "a" of the 590 original definition. "t" is the parameter that is being recursed on, 591 and "n" is the target parameter that causes things to happen when t reaches 592 it. *) 593 594val FV_cinvtri0 = Store_thm( 595 "FV_cinvtri0", 596 ``FV cinvtri0 = {}``, 597 SRW_TAC [][cinvtri0_def, EXTENSION] THEN METIS_TAC []); 598 599val cinvtri0_behaviour = store_thm( 600 "cinvtri0_behaviour", 601 ``n ��� t ��� 602 cinvtri0 @@ church t @@ church n @@ church a -n->* 603 cnvpr (invtri0 n a)``, 604 SIMP_TAC (bsrw_ss()) [cinvtri0_def] THEN 605 Q.ID_SPEC_TAC `n` THEN Q.ID_SPEC_TAC `a` THEN 606 Induct_on `t` THENL [ 607 SIMP_TAC (bsrw_ss()) [] THEN 608 ONCE_REWRITE_TAC [invtri0_def] THEN 609 SIMP_TAC (srw_ss() ++ ARITH_ss) [cnvpr_def], 610 611 SIMP_TAC (bsrw_ss()) [] THEN 612 REPEAT STRIP_TAC THEN Cases_on `n = SUC t` THEN 613 ASM_SIMP_TAC (bsrw_ss()) [] THENL [ 614 Cases_on `t < a` THENL [ 615 ASM_SIMP_TAC (bsrw_ss()) [] THEN 616 ONCE_REWRITE_TAC [invtri0_def] THEN 617 SRW_TAC [ARITH_ss][cnvpr_def], 618 619 ASM_SIMP_TAC (bsrw_ss()) [] THEN 620 CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [invtri0_def])) THEN 621 SRW_TAC [ARITH_ss][] THEN 622 `SUC t - (a + 1) = t - a` by DECIDE_TAC THEN 623 SRW_TAC [][arithmeticTheory.ADD1] 624 ], 625 626 `n ��� t` by DECIDE_TAC THEN 627 ASM_SIMP_TAC (bsrw_ss()) [] 628 ] 629 ]); 630 631val cinvtri_def = Define` 632 cinvtri = 633 LAM "n" (csnd @@ (cinvtri0 @@ VAR "n" @@ VAR "n" @@ church 0)) 634`; 635 636val FV_cinvtri = Store_thm( 637 "FV_cinvtri", 638 ``FV cinvtri = {}``, 639 SRW_TAC [][cinvtri_def, EXTENSION] THEN METIS_TAC []); 640 641val cinvtri_behaviour = bstore_thm( 642 "cinvtri_behaviour", 643 ``cinvtri @@ church n -n->* church (tri����� n)``, 644 SIMP_TAC (bsrw_ss()) [cinvtri_def, cinvtri0_behaviour, invtri_def]); 645 646(* -- The pairing function and fst and snd *) 647 648val cnpair_def = Define` 649 cnpair = 650 LAM "n" (LAM "m" 651 (cplus @@ (ctri @@ (cplus @@ VAR "n" @@ VAR "m")) @@ VAR "m")) 652`; 653 654val FV_cnpair = Store_thm( 655 "FV_cnpair", 656 ``FV cnpair = {}``, 657 SRW_TAC [][cnpair_def, EXTENSION] THEN METIS_TAC []); 658 659val cnpair_behaviour = bstore_thm( 660 "cnpair_behaviour", 661 ``cnpair @@ church n @@ church m -n->* church (n ��� m)``, 662 SIMP_TAC (bsrw_ss()) [cnpair_def, npair_def]); 663 664(* cnfst *) 665val cnfst_def = Define` 666 cnfst = LAM "n" (cminus 667 @@ (cplus @@ (ctri @@ (cinvtri @@ VAR "n")) 668 @@ (cinvtri @@ VAR "n")) 669 @@ VAR "n") 670`; 671 672val FV_cnfst = Store_thm( 673 "FV_cnfst", 674 ``FV cnfst = {}``, 675 SRW_TAC [][cnfst_def, EXTENSION] THEN METIS_TAC []); 676 677val cnfst_behaviour = bstore_thm( 678 "cnfst_behaviour", 679 ``cnfst @@ church p -n->* church (nfst p)``, 680 SIMP_TAC (bsrw_ss()) [cnfst_def, nfst_def]); 681 682(* cnsnd *) 683val cnsnd_def = Define` 684 cnsnd = LAM "n" (cminus @@ VAR "n" 685 @@ (ctri @@ (cinvtri @@ VAR "n"))) 686`; 687 688val FV_cnsnd = Store_thm( 689 "FV_cnsnd", 690 ``FV cnsnd = {}``, 691 SRW_TAC [][cnsnd_def, EXTENSION] THEN METIS_TAC []); 692 693val cnsnd_behaviour = bstore_thm( 694 "cnsnd_behaviour", 695 ``cnsnd @@ church p -n->* church (nsnd p)``, 696 SIMP_TAC (bsrw_ss()) [cnsnd_def, nsnd_def]); 697 698(* ---------------------------------------------------------------------- 699 cfindleast 700 ---------------------------------------------------------------------- *) 701 702val cfindbody_def = Define` 703 cfindbody P N k = 704 let lp = NEW (FV P ��� FV k) in 705 let nv = NEW (FV P ��� FV k ��� {lp}) 706 in 707 Yf (LAM lp (LAM nv (P @@ VAR nv 708 @@ (k @@ VAR nv) 709 @@ (VAR lp @@ (csuc @@ VAR nv))))) @@ N 710`; 711 712val fresh_cfindbody = store_thm( 713 "fresh_cfindbody", 714 ``lp ��� FV P ��� lp ��� FV k ��� nv ��� lp ��� nv ��� FV P ��� nv ��� FV k ��� 715 (cfindbody P N k = 716 Yf (LAM lp (LAM nv (P @@ VAR nv @@ (k @@ VAR nv) 717 @@ (VAR lp @@ (csuc @@ VAR nv))))) @@ 718 N)``, 719 SRW_TAC [][LET_THM, cfindbody_def] THEN 720 binderLib.NEW_ELIM_TAC THEN REPEAT STRIP_TAC THEN 721 binderLib.NEW_ELIM_TAC THEN REPEAT STRIP_TAC THEN 722 SRW_TAC [][termTheory.LAM_eq_thm, termTheory.tpm_fresh] THEN 723 Cases_on `nv = v` THEN SRW_TAC [][termTheory.tpm_fresh] THEN 724 Cases_on `lp = v'` THEN SRW_TAC [][termTheory.tpm_fresh] THEN 725 METIS_TAC []); 726 727val cfindbody_SUB = Store_thm( 728 "cfindbody_SUB", 729 ``[Q/v] (cfindbody P N k) = cfindbody ([Q/v]P) ([Q/v]N) ([Q/v]k)``, 730 Q_TAC (NEW_TAC "lp") `FV P ��� FV k ��� FV Q ��� {v}` THEN 731 Q_TAC (NEW_TAC "nv") `FV P ��� FV k ��� FV Q ��� {v;lp}` THEN 732 `cfindbody P N k = Yf (LAM lp (LAM nv (P @@ VAR nv @@ (k @@ VAR nv) 733 @@ (VAR lp @@ (csuc @@ VAR nv))))) @@ 734 N` 735 by SRW_TAC [][fresh_cfindbody] THEN 736 `cfindbody ([Q/v]P) ([Q/v]N) ([Q/v]k) = 737 Yf (LAM lp (LAM nv ([Q/v]P @@ VAR nv @@ ([Q/v]k @@ VAR nv) 738 @@ (VAR lp @@ (csuc @@ VAR nv))))) @@ [Q/v]N` 739 by (MATCH_MP_TAC (GEN_ALL fresh_cfindbody) THEN 740 SRW_TAC [][chap2Theory.NOT_IN_FV_SUB]) THEN 741 SRW_TAC [][termTheory.lemma14b]); 742 743val cfindbody_thm = store_thm( 744 "cfindbody_thm", 745 ``cfindbody P N k -w->* P @@ N @@ (k @@ N) @@ cfindbody P (csuc @@ N) k``, 746 unvarify_tac head_reductionTheory.whstar_substitutive THEN 747 SRW_TAC [][termTheory.lemma14b] THEN 748 Q_TAC (NEW_TAC "z") `{Ps; ks}` THEN 749 Q_TAC (NEW_TAC "nv") `{Ps; z; ks}` THEN 750 `���N. cfindbody (VAR Ps) N (VAR ks) = 751 Yf (LAM z (LAM nv (VAR Ps @@ VAR nv @@ (VAR ks @@ VAR nv) 752 @@ (VAR z @@ (csuc @@ VAR nv))))) 753 @@ N` 754 by SRW_TAC [][fresh_cfindbody] THEN 755 ASM_SIMP_TAC (whfy (srw_ss())) [MATCH_MP relationTheory.RTC_SUBSET 756 head_reductionTheory.whY2]); 757 758val cfindbody_cong = store_thm( 759 "cfindbody_cong", 760 ``P == P' ��� N == N' ��� k == k' ��� cfindbody P N k == cfindbody P' N' k'``, 761 Q_TAC (NEW_TAC "lp") `FV P ��� FV P' ��� FV k ��� FV k'` THEN 762 Q_TAC (NEW_TAC "nv") `FV P ��� FV P' ��� FV k ��� FV k' ��� {lp}` THEN 763 REPEAT STRIP_TAC THEN 764 `(cfindbody P N k = Yf (LAM lp (LAM nv (P @@ VAR nv @@ (k @@ VAR nv) 765 @@ (VAR lp @@ (csuc @@ VAR nv))))) @@ 766 N) ��� 767 (cfindbody P' N' k' = 768 Yf (LAM lp (LAM nv (P' @@ VAR nv @@ (k' @@ VAR nv) 769 @@ (VAR lp @@ (csuc @@ VAR nv))))) @@ 770 N')` 771 by SRW_TAC [][fresh_cfindbody] THEN 772 ASM_SIMP_TAC (bsrw_ss()) []); 773 774val bnf_cfindbody = Store_thm( 775 "bnf_cfindbody", 776 ``��bnf (cfindbody P N k)``, 777 SRW_TAC [][cfindbody_def, LET_THM]); 778 779val FV_cfindbody = Store_thm( 780 "FV_cfindbody", 781 ``FV (cfindbody P N k) = FV P ��� FV N ��� FV k``, 782 SRW_TAC [][cfindbody_def, EXTENSION, LET_THM] THEN 783 NEW_ELIM_TAC THEN SRW_TAC [][] THEN 784 NEW_ELIM_TAC THEN SRW_TAC [][] THEN METIS_TAC []); 785 786val cfindleast_def = Define` 787 cfindleast = LAM "P" (LAM "k" (cfindbody (VAR "P") (church 0) (VAR "k"))) 788`; 789 790val FV_cfindleast = Store_thm( 791 "FV_cfindleast", 792 ``FV cfindleast = {}``, 793 SRW_TAC [][cfindleast_def, pred_setTheory.EXTENSION] THEN METIS_TAC []); 794 795val cfindleast_behaviour = store_thm( 796 "cfindleast_behaviour", 797 ``cfindleast @@ P @@ k == cfindbody P (church 0) k``, 798 SIMP_TAC (bsrw_ss()) [cfindleast_def] THEN 799 Q_TAC (NEW_TAC "kk") `FV P ��� {"P"; "k"}` THEN 800 `LAM "k" (cfindbody (VAR "P") (church 0) (VAR "k")) = 801 LAM kk (cfindbody (VAR "P") (church 0) (VAR kk))` 802 by (`cfindbody (VAR "P") (church 0) (VAR kk) = 803 [VAR kk/"k"] (cfindbody (VAR "P") (church 0) (VAR "k"))` 804 by SRW_TAC [][termTheory.lemma14b] THEN 805 POP_ASSUM SUBST1_TAC THEN 806 MATCH_MP_TAC termTheory.SIMPLE_ALPHA THEN SRW_TAC [][]) THEN 807 POP_ASSUM SUBST_ALL_TAC THEN 808 ASM_SIMP_TAC (bsrw_ss()) []); 809 810val cfindleast_termI = store_thm( 811 "cfindleast_termI", 812 ``(���n. ���b. P @@ church n == cB b) ��� P @@ church n == cB T ��� 813 cfindleast @@ P @@ k == k @@ church (LEAST n. P @@ church n == cB T)``, 814 STRIP_TAC THEN numLib.LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN 815 POP_ASSUM (K ALL_TAC) THEN 816 SIMP_TAC (bsrw_ss()) [cfindleast_behaviour] THEN 817 Q_TAC SUFF_TAC 818 `���p n. p ��� n ��� 819 (���m. m < n ��� ��(P @@ church m == cB T)) ��� 820 P @@ church n == cB T ��� 821 cfindbody P (church p) k == k @@ church n` 822 THEN1 METIS_TAC [DECIDE ``0 ��� n``] THEN 823 Induct_on `n - p` THEN REPEAT STRIP_TAC THENL [ 824 `p = n` by DECIDE_TAC THEN 825 ASM_SIMP_TAC (bsrw_ss()) [Once cfindbody_thm], 826 827 `p < n` by DECIDE_TAC THEN 828 `���r. P @@ church p == cB r` by METIS_TAC [] THEN 829 `r = F` by (Cases_on `r` THEN METIS_TAC []) THEN 830 ASM_SIMP_TAC (bsrw_ss()) [Once cfindbody_thm, Cong cfindbody_cong] THEN 831 FIRST_X_ASSUM (fn th => MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] th)) THEN 832 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [] 833 ]); 834 835val cfindbody_11 = Store_thm( 836 "cfindbody_11", 837 ``(cfindbody P1 N1 k1 = cfindbody P2 N2 k2) ��� 838 (P1 = P2) ��� (N1 = N2) ��� (k1 = k2)``, 839 Q_TAC (NEW_TAC "lp") `FV P1 ��� FV P2 ��� FV k1 ��� FV k2` THEN 840 Q_TAC (NEW_TAC "nv") `FV P1 ��� FV P2 ��� FV k1 ��� FV k2 ��� {lp}` THEN 841 `(cfindbody P1 N1 k1 = Yf (LAM lp (LAM nv (P1 @@ VAR nv @@ (k1 @@ VAR nv) 842 @@ (VAR lp @@ (csuc @@ VAR nv))))) 843 @@ N1) ��� 844 (cfindbody P2 N2 k2 = Yf (LAM lp (LAM nv (P2 @@ VAR nv @@ (k2 @@ VAR nv) 845 @@ (VAR lp @@ (csuc @@ VAR nv))))) 846 @@ N2)` 847 by SRW_TAC [][fresh_cfindbody] THEN 848 SRW_TAC [][AC CONJ_ASSOC CONJ_COMM]); 849 850val lameq_triangle = store_thm( 851 "lameq_triangle", 852 ``M == N ��� M == P ��� bnf N ��� bnf P ��� (N = P)``, 853 METIS_TAC [chap3Theory.betastar_lameq_bnf, chap2Theory.lameq_rules, 854 chap3Theory.bnf_reduction_to_self]); 855 856val cfindleast_bnfE = store_thm( 857 "cfindleast_bnfE", 858 ``(���n. ���b. P @@ church n == cB b) ��� 859 cfindleast @@ P @@ k == r ��� bnf r ��� 860 ���m. (r == k @@ church m) ��� P @@ church m == cB T ��� 861 ���m���. m��� < m ��� P @@ church m��� == cB F``, 862 SIMP_TAC (bsrw_ss()) [cfindleast_behaviour] THEN 863 REPEAT STRIP_TAC THEN 864 `���N. steps N (cfindbody P (church 0) k) = r` 865 by METIS_TAC [nstar_steps, nstar_betastar_bnf, 866 chap3Theory.betastar_lameq_bnf] THEN 867 Q_TAC SUFF_TAC 868 `���N cn ct. (steps N (cfindbody P ct k) = r) ��� 869 (���c0. c0 < cn ��� P @@ church c0 == cB F) ��� 870 (ct == church cn) ��� 871 ���m. (r == k @@ church m) ��� P @@ church m == cB T ��� 872 ���m���. m��� < m ��� P @@ church m��� == cB F` 873 THEN1 METIS_TAC [DECIDE ``��(x < 0)``, chap2Theory.lameq_refl] THEN 874 REPEAT (FIRST_X_ASSUM (fn th => if free_in ``cfindbody`` (concl th) then 875 ALL_TAC 876 else NO_TAC)) THEN 877 completeInduct_on `N` THEN 878 MAP_EVERY Q.X_GEN_TAC [`cn`,`ct`] THEN REPEAT STRIP_TAC THEN 879 `cfindbody P ct k -n->* P @@ ct @@ (k @@ ct) @@ (cfindbody P (csuc @@ ct) k)` 880 by METIS_TAC [cfindbody_thm, whstar_nstar] THEN 881 `���b. P @@ church cn == cB b` by METIS_TAC [] THEN 882 Cases_on `b` THENL [ 883 `cfindbody P ct k == k @@ church cn` 884 by ASM_SIMP_TAC (bsrw_ss()) [] THEN 885 `cfindbody P ct k -n->* r` by METIS_TAC [steps_nstar] THEN 886 METIS_TAC [nstar_lameq, chap2Theory.lameq_rules], 887 888 `P @@ ct == cB F` by ASM_SIMP_TAC (bsrw_ss()) [] THEN 889 POP_ASSUM (STRIP_ASSUME_TAC o 890 MATCH_MP (GEN_ALL (CONJUNCT2 whead_tests))) THEN 891 `cfindbody P ct k -n->* cfindbody P (csuc @@ ct) k` 892 by METIS_TAC [whstar_nstar, relationTheory.RTC_CASES_RTC_TWICE] THEN 893 `���n1. cfindbody P (csuc @@ ct) k = steps n1 (cfindbody P ct k)` 894 by METIS_TAC [nstar_steps] THEN 895 `��bnf (cfindbody P (csuc @@ ct) k)` by SRW_TAC [][] THEN 896 `n1 < N` by METIS_TAC [DECIDE ``n:num < m ��� (n = m) ��� m < n``, 897 bnf_steps_upwards_closed] THEN 898 `���rest. N = rest + n1` by (Q.EXISTS_TAC `N - n1` THEN DECIDE_TAC) THEN 899 FULL_SIMP_TAC (srw_ss()) [steps_plus] THEN 900 `n1 ��� 0` by (STRIP_TAC THEN 901 FULL_SIMP_TAC (srw_ss()) [termTheory.APP_acyclic]) THEN 902 `rest < rest + n1` by DECIDE_TAC THEN 903 POP_ASSUM (fn th1 => FIRST_X_ASSUM (MP_TAC o C MATCH_MP th1)) THEN 904 DISCH_THEN (Q.SPECL_THEN [`SUC cn`, `csuc @@ ct`] MP_TAC) THEN 905 ASM_SIMP_TAC (bsrw_ss()) [] THEN 906 DISCH_THEN MATCH_MP_TAC THEN 907 REPEAT STRIP_TAC THEN 908 `(c0 = cn) ��� c0 < cn` by DECIDE_TAC THEN SRW_TAC [][] 909 ]); 910 911val _ = export_theory() 912 913