1open HolKernel bossLib boolLib Parse termTheory chap2Theory chap3Theory reductionEval binderLib relationTheory lcsymtacs 2 3val _ = new_theory "abselim" 4 5val _ = remove_ovl_mapping "LAM" {Name="LAM", Thy="labelledTerms"} 6val _ = clear_overloads_on "FV" 7val _ = overload_on ("FV", ``supp tpm``) 8val _ = remove_ovl_mapping "VAR" {Name="VAR", Thy="labelledTerms"} 9val _ = remove_ovl_mapping "APP" {Name="APP", Thy="labelledTerms"} 10 11val (absfree_rules,absfree_ind,absfree_cases) = Hol_reln` 12 (absfree S) ��� (absfree K) ��� (absfree (VAR x)) ��� 13 (absfree t1 ��� absfree t2 ��� absfree (APP t1 t2))` 14 15val (abselim_rules,abselim_ind,abselim_cases) = Hol_reln` 16 (abselim (VAR x) (VAR x)) ��� 17 (abselim t1 t1' ��� abselim t2 t2' ��� abselim (t1 @@ t2) (t1' @@ t2')) ��� 18 (abselim t t' ��� x ��� FV t ��� abselim (LAM x t) (K @@ t')) ��� 19 (abselim (LAM x (VAR x)) (S @@ K @@ K)) ��� 20 (abselim (LAM y t) r1 ��� abselim (LAM x r1) r2 21 ��� x ��� FV (LAM y t) ��� (LAM x (LAM y t) ��� S) ��� (LAM x (LAM y t) ��� K) 22 ��� abselim (LAM x (LAM y t)) r2) ��� 23 (abselim (LAM x t1) t1' ��� abselim (LAM x t2) t2' ��� x ��� FV (t1 @@ t2) 24 ��� abselim (LAM x (t1 @@ t2)) (S @@ t1' @@ t2')) ��� 25 (abselim S S) ��� (abselim K K)` 26 27val abselim_absfree = store_thm( 28"abselim_absfree", 29``���t u. abselim t u ��� absfree u``, 30ho_match_mp_tac abselim_ind >> 31srw_tac [][absfree_rules]) 32 33val absfree_abselim_id = store_thm( 34"absfree_abselim_id", 35``���t. absfree t ��� abselim t t``, 36ho_match_mp_tac absfree_ind >> 37srw_tac [][abselim_rules]); 38 39val lameq_lamext = store_thm( 40"lameq_lamext", 41``���t u. t == u ��� lamext t u``, 42ho_match_mp_tac lameq_ind >> 43metis_tac [lamext_rules]) 44 45val lamext_refl = store_thm( 46 "lamext_refl", 47 ``lamext M M``, 48 SRW_TAC [][lamext_rules]); 49val _ = export_rewrites["lamext_refl"]; 50 51val lamext_app_cong = store_thm( 52 "lamext_app_cong", 53 ``lamext M1 M2 ==> lamext N1 N2 ==> lamext (M1 @@ N1) (M2 @@ N2)``, 54 METIS_TAC [lamext_rules]); 55 56val [_,lamext_refl,lamext_sym,lamext_trans,_,_,_,lamext_ext] = CONJUNCTS lamext_rules 57val [_,conversion_sym,conversion_trans,conversion_subset,_,_] = CONJUNCTS (SPEC_ALL conversion_rules) 58 59val lamext_betaeta = store_thm( 60"lamext_betaeta", 61``lamext = conversion (�� RUNION ��)``, 62metis_tac [lemma2_14,beta_eta_lameta,FUN_EQ_THM]); 63 64val abselim_lamext = store_thm( 65"abselim_lamext", 66``���t u. abselim t u ��� lamext t u``, 67ho_match_mp_tac abselim_ind >> 68conj_tac >- srw_tac [][] >> 69conj_tac >- srw_tac [][lamext_app_cong] >> 70conj_tac >- ( 71 map_every qx_gen_tac [`t`,`u`,`x`] >> 72 strip_tac >> 73 match_mp_tac lamext_ext >> 74 Q_TAC (NEW_TAC "z") `FV (LAM x t @@ (K @@ u))` >> 75 qexists_tac `z` >> conj_tac >- fsrw_tac [][] >> 76 srw_tac [][lamext_betaeta] >> 77 match_mp_tac conversion_trans >> 78 qexists_tac `t` >> 79 conj_tac >- ( 80 match_mp_tac conversion_subset >> 81 srw_tac [][RUNION,beta_def] >> 82 disj1_tac >> 83 map_every qexists_tac [`x`,`t`] >> 84 srw_tac [][lemma14b] ) >> 85 match_mp_tac conversion_trans >> 86 qexists_tac `u` >> 87 conj_tac >- ( 88 srw_tac [][SYM lamext_betaeta] ) >> 89 srw_tac [][SYM lamext_betaeta] >> 90 match_mp_tac lameq_lamext >> 91 srw_tac [BETA_ss][] ) >> 92conj_tac >- ( 93 srw_tac [][] >> 94 match_mp_tac lamext_ext >> 95 Q_TAC (NEW_TAC "z") `FV (LAM x (VAR x) @@ (S @@ K @@ K))` >> 96 qexists_tac `z` >> srw_tac [][] >> 97 match_mp_tac lameq_lamext >> 98 srw_tac [BETA_ss][] ) >> 99conj_tac >- 100 metis_tac [lamext_rules] >> 101conj_tac >- ( 102 rpt gen_tac >> 103 strip_tac >> 104 pop_assum (K ALL_TAC) >> 105 match_mp_tac lamext_ext >> 106 Q_TAC (NEW_TAC "z") `FV (LAM x (t1 @@ t2) @@ (S @@ t1' @@ t2'))` >> 107 qexists_tac `z` >> fsrw_tac [][] >> 108 match_mp_tac lamext_sym >> 109 match_mp_tac lamext_trans >> 110 qexists_tac `S @@ (LAM x t1) @@ (LAM x t2) @@ VAR z` >> 111 conj_tac >- PROVE_TAC [lamext_rules] >> 112 match_mp_tac lameq_lamext >> 113 srw_tac [BETA_ss][] ) >> 114srw_tac [][lamext_refl]); 115 116val lemma1 = prove( 117``x ��� FV t ��� (LAM x (tpm [(x,y)] t) = LAM y t)``, 118srw_tac [][LAM_eq_thm] >> 119Cases_on `x=y` >> srw_tac [][]) 120 121val lemma2 = prove( 122``(LAM (swapstr x y v) (tpm [(x,y)] t) = S) = (LAM v t = S)``, 123srw_tac [][EQ_IMP_THM] >- ( 124 `tpm [(x,y)] (LAM (swapstr x y v) (tpm [(x,y)] t)) = tpm [(x,y)] S` by 125 metis_tac [] >> 126 fsrw_tac [][] >> srw_tac [][tpm_fresh] ) >> 127`tpm [(x,y)] (LAM v t) = tpm [(x,y)] S` by metis_tac [] >> 128fsrw_tac [][] >> srw_tac [][tpm_fresh]) 129 130val lemma3 = prove( 131``(LAM (swapstr x y v) (tpm [(x,y)] t) = K) = (LAM v t = K)``, 132srw_tac [][EQ_IMP_THM] >- ( 133 `tpm [(x,y)] (LAM (swapstr x y v) (tpm [(x,y)] t)) = tpm [(x,y)] K` by 134 metis_tac [] >> 135 fsrw_tac [][] >> srw_tac [][tpm_fresh] ) >> 136`tpm [(x,y)] (LAM v t) = tpm [(x,y)] K` by metis_tac [] >> 137fsrw_tac [][] >> srw_tac [][tpm_fresh]) 138 139val lam_count_exists = 140 tm_recursion 141|> INST_TYPE [alpha |-> ``:num``] 142|> Q.INST [`apm`|->`K I`,`A`|->`{}`, 143 `vr`|->`K 0`, 144 `ap`|->`��m n t1 t2. m + n`, 145 `lm`|->`��m v t. if (LAM v t = S) ��� (LAM v t = K) then 0 else m + 1`] 146|> SIMP_RULE (srw_ss()) [lemma1,lemma2,lemma3] 147 148val lam_count_def = new_specification ("lam_count_def",["lam_count"],lam_count_exists) 149 150val app_count_exists = 151 tm_recursion 152|> INST_TYPE [alpha |-> ``:num``] 153|> Q.INST [`apm`|->`K I`,`A`|->`{}`, 154 `vr`|->`K 0`, 155 `ap`|->`��m n t1 t2. m + n + 1`, 156 `lm`|->`��m v t. if (LAM v t = S) ��� (LAM v t = K) then 0 else m`] 157|> SIMP_RULE (srw_ss()) [lemma1,lemma2,lemma3] 158 159val app_count_def = new_specification ("app_count_def",["app_count"],app_count_exists) 160 161val _ = export_rewrites["lam_count_def","app_count_def"]; 162 163val lam_count_absfree = store_thm( 164"lam_count_absfree", 165``���t. absfree t ��� (lam_count t = 0)``, 166ho_match_mp_tac absfree_ind >> 167srw_tac [][S_def,K_def]) 168 169val abselim_total = store_thm( 170"abselim_total", 171``���t.���u. abselim t u``, 172WF_INDUCTION_THM 173 |> Q.ISPEC `inv_image ($< LEX $<) (��t. (lam_count t, app_count t))` 174 |> SIMP_RULE (srw_ss()) [pairTheory.WF_LEX,prim_recTheory.WF_LESS,relationTheory.WF_inv_image] 175 |> ho_match_mp_tac >> 176srw_tac [][relationTheory.inv_image_def,prim_recTheory.measure_def,pairTheory.LEX_DEF] >> 177FULL_STRUCT_CASES_TAC (Q.SPEC `t` term_CASES) >- ( 178 fsrw_tac [][] >> metis_tac [abselim_rules] ) 179>- ( 180 `(���u. abselim t1 u) ��� (���u. abselim t2 u)` by ( 181 srw_tac [][] >> first_x_assum match_mp_tac >> 182 srw_tac [ARITH_ss][] ) >> 183 metis_tac [abselim_rules] ) >> 184qmatch_rename_tac `���u. abselim (LAM x t) u` [] >> 185Cases_on `LAM x t = S` >- metis_tac [abselim_rules] >> 186Cases_on `LAM x t = K` >- metis_tac [abselim_rules] >> 187Cases_on `x ��� FV t` >- ( 188 `���u. abselim t u` by ( 189 first_x_assum match_mp_tac >> 190 srw_tac [ARITH_ss][] ) >> 191 metis_tac [abselim_rules] ) >> fsrw_tac [][] >> 192FULL_STRUCT_CASES_TAC (Q.SPEC `t` term_CASES) >- ( 193 fsrw_tac [][] >> metis_tac [abselim_rules] ) 194>- ( 195 `(���u. abselim (LAM x t1) u) ��� (���u. abselim (LAM x t2) u)` by ( 196 srw_tac [][] >> first_x_assum match_mp_tac >> 197 srw_tac [ARITH_ss][] ) >> 198 `x ��� FV t1 ��� FV t2` by fsrw_tac [][] >> 199 metis_tac [abselim_rules] ) >> 200qmatch_rename_tac `���u. abselim (LAM x (LAM y t)) u` [] >> 201`���r1. abselim (LAM y t) r1` by ( 202 first_x_assum match_mp_tac >> 203 srw_tac [ARITH_ss][] ) >> 204`x ��� FV t` by fsrw_tac [][] >> 205qsuff_tac `���r2. abselim (LAM x r1) r2` >- metis_tac [abselim_rules] >> 206first_x_assum match_mp_tac >> 207disj1_tac >> 208Cases_on `LAM x r1 = S` >- srw_tac [ARITH_ss][] >> 209Cases_on `LAM x r1 = K` >- srw_tac [ARITH_ss][] >> 210`absfree r1` by metis_tac [abselim_absfree] >> 211`lam_count r1 = 0` by metis_tac [lam_count_absfree] >> 212Cases_on `LAM y t = S` >- ( 213 `x ��� FV S` by metis_tac [] >> fsrw_tac [][S_def] ) >> 214Cases_on `LAM y t = K` >- ( 215 `x ��� FV K` by metis_tac [] >> fsrw_tac [][K_def] ) >> 216srw_tac [ARITH_ss][]) 217 218val [abselim_VAR,abselim_APP,abselim_LAM,abselim_LAM_VAR,abselim_LAM_LAM,abselim_LAM_APP,abselim_S,abselim_K] = CONJUNCTS abselim_rules 219 220val abselim_tpm = store_thm( 221"abselim_tpm", 222``���t u. abselim t u ��� ���x y. abselim (tpm [(x,y)] t) (tpm [(x,y)] u)``, 223ho_match_mp_tac abselim_ind >> 224conj_tac >- srw_tac [][abselim_VAR] >> 225conj_tac >- srw_tac [][abselim_APP] >> 226conj_tac >- srw_tac [][abselim_LAM,tpm_fresh] >> 227conj_tac >- srw_tac [][abselim_LAM_VAR,tpm_fresh] >> 228conj_tac >- ( 229 srw_tac [][] >> 230 match_mp_tac abselim_LAM_LAM >> 231 srw_tac [][] >> 232 qexists_tac `(tpm [(x',y')] u)` >> 233 `tpm [(x',y')] (LAM x (LAM y t)) ��� tpm [(x',y')] S` by metis_tac [tpm_inverse] >> 234 `tpm [(x',y')] (LAM x (LAM y t)) ��� tpm [(x',y')] K` by metis_tac [tpm_inverse] >> 235 fsrw_tac [][tpm_fresh] ) >> 236conj_tac >- ( 237 rpt gen_tac >> 238 strip_tac >> 239 rpt gen_tac >> 240 asm_simp_tac (srw_ss()) [tpm_fresh] >> 241 match_mp_tac abselim_LAM_APP >> 242 fsrw_tac [][] ) >> 243srw_tac [][tpm_fresh,abselim_S,abselim_K]); 244 245val abselim_FV = store_thm( 246"abselim_FV", 247``���t u. abselim t u ��� (FV t = FV u)``, 248ho_match_mp_tac abselim_ind >> 249conj_tac >- srw_tac [][] >> 250conj_tac >- srw_tac [][] >> 251conj_tac >- fsrw_tac [][pred_setTheory.DELETE_NON_ELEMENT] >> 252conj_tac >- srw_tac [][] >> 253conj_tac >- srw_tac [][] >> 254conj_tac >- fsrw_tac [][pred_setTheory.DELETE_NON_ELEMENT,pred_setTheory.UNION_DELETE] >> 255srw_tac [][]); 256 257val abselim_unique = store_thm( 258"abselim_unique", 259``���t u1 u2. abselim t u1 ��� abselim t u2 ��� (u1 = u2)``, 260qsuff_tac `���t u1. abselim t u1 ��� ���u2. abselim t u2 ��� (u1 = u2)` >- metis_tac [] >> 261ho_match_mp_tac abselim_ind >> 262conj_tac >- ( 263 srw_tac [][] >> 264 qspecl_then [`VAR x`,`u2`] mp_tac abselim_cases >> 265 fsrw_tac [][] >> 266 srw_tac [][S_def,K_def] ) >> 267conj_tac >- ( 268 map_every qx_gen_tac [`t1`,`v1`,`t2`,`v2`] >> 269 srw_tac [][] >> 270 qspecl_then [`t1@@t2`,`u2`] mp_tac abselim_cases >> 271 fsrw_tac [][S_def,K_def] >> 272 srw_tac [][] >> srw_tac [][] ) >> 273conj_tac >- ( 274 srw_tac [][] >> 275 qspecl_then [`LAM x t`,`u2`] mp_tac abselim_cases >> 276 fsrw_tac [][] >> 277 srw_tac [][] >- 278 fsrw_tac [][LAM_eq_thm,tpm_fresh] 279 >- ( 280 fsrw_tac [][LAM_eq_thm] >> 281 fsrw_tac [][] ) 282 >- ( 283 fsrw_tac [][LAM_eq_thm] >> srw_tac [][] >> 284 fsrw_tac [][] >> 285 Cases_on `x=y` >> fsrw_tac [][] ) 286 >- ( 287 fsrw_tac [][LAM_eq_thm] >> srw_tac [][] >> 288 fsrw_tac [][] ) 289 >- ( 290 fsrw_tac [][LAM_eq_thm] >> srw_tac [][] >> 291 fsrw_tac [][] ) 292 >- ( 293 fsrw_tac [][LAM_eq_thm,S_def] >> srw_tac [][] >> 294 fsrw_tac [][] >> 295 Cases_on `x = "x"` >> fsrw_tac [][] >> 296 Cases_on `x = "y"` >> fsrw_tac [][] >> 297 Cases_on `x = "z"` >> fsrw_tac [][] ) >> 298 fsrw_tac [][K_def,LAM_eq_thm] >> srw_tac [][] >> 299 fsrw_tac [][] >> 300 Cases_on `x = "x"` >> fsrw_tac [][] >> 301 Cases_on `x = "y"` >> fsrw_tac [][] ) >> 302conj_tac >- ( 303 srw_tac [][] >> 304 qspecl_then [`LAM x (VAR x)`,`u2`] mp_tac abselim_cases >> 305 fsrw_tac [][LAM_eq_thm] >> 306 srw_tac [][] >> fsrw_tac [][] >> 307 fsrw_tac [][tpm_eqr] >> srw_tac [][] >> 308 fsrw_tac [][] >> 309 fsrw_tac [][S_def,K_def,LAM_eq_thm] ) >> 310conj_tac >- ( 311 srw_tac [][] >> 312 qspecl_then [`LAM x (LAM y t)`,`u2`] mp_tac abselim_cases >> 313 full_simp_tac std_ss [term_distinct] >> 314 strip_tac >- ( 315 fsrw_tac [][LAM_eq_thm] >> 316 srw_tac [][] >> fsrw_tac [][] >> 317 fsrw_tac [][tpm_eqr] >> 318 srw_tac [][] >> 319 fsrw_tac [][] >> 320 qpat_assum `x <> x'` assume_tac >> 321 qpat_assum `x <> y` assume_tac >> 322 Cases_on`x'=y` >> fsrw_tac [][] ) 323 >- ( fsrw_tac [][LAM_eq_thm] ) 324 >- ( 325 Cases_on `x=x'` >- ( 326 qpat_assum `LAM x tt = LAM x' ttt` mp_tac >> 327 asm_simp_tac (srw_ss()) [Once LAM_eq_thm] >> 328 metis_tac [] ) >> 329 qpat_assum `LAM x tt = LAM x' ttt` mp_tac >> 330 asm_simp_tac (srw_ss()) [Once LAM_eq_thm] >> 331 `abselim (tpm [(x,x')] (LAM y' t')) (tpm [(x,x')] r1)` by metis_tac [abselim_tpm] >> 332 fsrw_tac [][] >> rpt strip_tac >> 333 fsrw_tac [][] >> 334 `u1 = tpm [(x,x')] r1` by metis_tac [] >> 335 fsrw_tac [][] >> 336 `abselim (tpm [(x,x')] (LAM x' r1)) (tpm [(x,x')] u2)` by metis_tac [abselim_tpm] >> 337 fsrw_tac [][] >> 338 `u1' = tpm [(x,x')] u2` by metis_tac [] >> 339 srw_tac [][] >> 340 match_mp_tac tpm_fresh >> 341 `FV u2 = FV (LAM x' r1)` by metis_tac [abselim_FV] >> 342 fsrw_tac [][] >> 343 `FV r1 = FV (LAM y' t')` by metis_tac [abselim_FV] >> 344 fsrw_tac [][] >> 345 Cases_on `x=y'` >> fsrw_tac [][] ) >> 346 fsrw_tac [][LAM_eq_thm] ) >> 347conj_tac >- ( 348 rpt gen_tac >> 349 strip_tac >> 350 gen_tac >> strip_tac >> 351 qspecl_then [`LAM x (t1 @@ t2)`,`u2`] mp_tac abselim_cases >> 352 qabbrev_tac `fva = (x ��� FV (t1 @@ t2))` >> 353 fsrw_tac [][] >> 354 qpat_assum `abselim (LAM x (t1 @@ t2)) u2` (K ALL_TAC) >> 355 fsrw_tac [][S_def,LAM_eq_thm,K_def] >> 356 fsrw_tac [][GSYM S_def, GSYM K_def] >> 357 qmatch_abbrev_tac `aa ��� bb ��� cc` >> 358 strip_tac >- ( 359 unabbrev_all_tac >> 360 fsrw_tac [][tpm_eqr] >> srw_tac [][] >> 361 fsrw_tac [][] ) >> 362 qunabbrev_tac `aa` >> 363 full_simp_tac std_ss [Abbr`cc`,Abbr`bb`,(GSYM pred_setTheory.IN_UNION)] >- 364 fsrw_tac [][] >> 365 qabbrev_tac `fva' = x' ��� FV t1' ��� FV t2'` >> 366 qpat_assum `Abbrev (fva = X)` assume_tac >> 367 fsrw_tac [][] >> 368 `abselim (tpm [(x,x')] (LAM x' t1')) (tpm [(x,x')] t1'')` by metis_tac [abselim_tpm] >> 369 `abselim (tpm [(x,x')] (LAM x' t2')) (tpm [(x,x')] t2'')` by metis_tac [abselim_tpm] >> 370 fsrw_tac [][] >> 371 res_tac >> 372 `(FV t1'' = FV (LAM x' t1')) ��� (FV t2'' = FV (LAM x' t2'))` by metis_tac [abselim_FV] >> 373 srw_tac [][tpm_fresh] ) >> 374conj_tac >- ( 375 srw_tac [][] >> 376 qspecl_then [`S`,`u2`] mp_tac abselim_cases >> 377 srw_tac [][] 378 >- srw_tac [][S_def] 379 >- fsrw_tac [][S_def] 380 >- ( 381 fsrw_tac [][S_def,LAM_eq_thm] >- ( 382 srw_tac [][] >> fsrw_tac [][] ) >> 383 fsrw_tac [][tpm_eqr] >> srw_tac [][] >> 384 fsrw_tac [][] >> 385 Cases_on `x="x"` >> fsrw_tac [][] >> 386 Cases_on `x="y"` >> fsrw_tac [][] >> 387 Cases_on `x="z"` >> fsrw_tac [][] ) 388 >- ( fsrw_tac [][S_def,LAM_eq_thm] ) 389 >- ( metis_tac [] ) 390 >- ( fsrw_tac [][S_def,LAM_eq_thm] ) 391 >- ( fsrw_tac [][S_def,LAM_eq_thm] ) 392 >- ( fsrw_tac [][] ) ) >> 393srw_tac [][] >> 394qspecl_then [`K`,`u2`] mp_tac abselim_cases >> 395srw_tac [][] 396>- srw_tac [][K_def] 397>- fsrw_tac [][K_def] 398>- ( 399 fsrw_tac [][K_def,LAM_eq_thm] >- ( 400 srw_tac [][] >> fsrw_tac [][] ) >> 401 fsrw_tac [][tpm_eqr] >> srw_tac [][] >> 402 fsrw_tac [][] >> 403 Cases_on `x="x"` >> fsrw_tac [][] >> 404 Cases_on `x="y"` >> fsrw_tac [][] ) 405>- ( fsrw_tac [][K_def,LAM_eq_thm] ) 406>- ( metis_tac [] ) 407>- ( fsrw_tac [][K_def,LAM_eq_thm] ) 408>- ( fsrw_tac [][K_def,LAM_eq_thm] ) 409>- ( fsrw_tac [][] ) ) 410 411val _ = export_theory () 412