1open HolKernel boolLib Parse bossLib generic_termsTheory 2 3open boolSimps 4 5open nomsetTheory 6open pred_setTheory 7open binderLib 8open nomdatatype 9val _ = new_theory "term"; 10 11val _ = set_fixity "=" (Infix(NONASSOC, 450)) 12 13fun Save_thm (nm, th) = save_thm(nm,th) before export_rewrites [nm] 14fun Store_thm(nm,t,tac) = store_thm(nm,t,tac) before export_rewrites [nm] 15 16val tyname = "term" 17 18val vp = ``(��n u:unit. n = 0)`` 19val lp = ``(��n (d:unit + unit) tns uns. 20 (n = 0) ��� ISL d ��� (tns = []) ��� (uns = [0;0]) ��� 21 (n = 0) ��� ISR d ��� (tns = [0]) ��� (uns = []))`` 22 23val {term_ABS_pseudo11, term_REP_11, genind_term_REP, genind_exists, 24 termP, absrep_id, repabs_pseudo_id, term_REP_t, term_ABS_t, newty, ...} = 25 new_type_step1 tyname 0 {vp=vp, lp = lp} 26val [gvar,glam] = genind_rules |> SPEC_ALL |> CONJUNCTS 27 28val LAM_t = mk_var("LAM", ``:string -> ^newty -> ^newty``) 29val LAM_def = new_definition( 30 "LAM_def", 31 ``^LAM_t v t = ^term_ABS_t (GLAM v (INR ()) [^term_REP_t t] [])``) 32val LAM_termP = prove( 33 mk_comb(termP, LAM_def |> SPEC_ALL |> concl |> rhs |> rand), 34 match_mp_tac glam >> srw_tac [][genind_term_REP]); 35val LAM_t = defined_const LAM_def 36 37 38val APP_t = mk_var("APP", ``:^newty -> ^newty -> ^newty``) 39val APP_def = new_definition( 40 "APP_def", 41 ``^APP_t t1 t2 = 42 ^term_ABS_t (GLAM ARB (INL ()) [] [^term_REP_t t1; ^term_REP_t t2])``); 43val APP_termP = prove( 44 ``^termP (GLAM x (INL ()) [] [^term_REP_t t1; ^term_REP_t t2])``, 45 match_mp_tac glam >> srw_tac [][genind_term_REP]) 46val APP_t = defined_const APP_def 47 48val APP_def' = prove( 49 ``^term_ABS_t (GLAM v (INL ()) [] [^term_REP_t t1; ^term_REP_t t2]) = ^APP_t t1 t2``, 50 srw_tac [][APP_def, GLAM_NIL_EQ, term_ABS_pseudo11, APP_termP]); 51 52val VAR_t = mk_var("VAR", ``:string -> ^newty``) 53val VAR_def = new_definition( 54 "VAR_def", 55 ``^VAR_t s = ^term_ABS_t (GVAR s ())``); 56val VAR_termP = prove( 57 mk_comb(termP, VAR_def |> SPEC_ALL |> concl |> rhs |> rand), 58 srw_tac [][genind_rules]); 59val VAR_t = defined_const VAR_def 60 61val cons_info = 62 [{con_termP = VAR_termP, con_def = VAR_def}, 63 {con_termP = APP_termP, con_def = SYM APP_def'}, 64 {con_termP = LAM_termP, con_def = LAM_def}] 65 66val tpm_name_pfx = "t" 67val {tpm_thm, term_REP_tpm, t_pmact_t, tpm_t} = 68 define_permutation {name_pfx = "t", name = tyname, 69 term_REP_t = term_REP_t, 70 term_ABS_t = term_ABS_t, absrep_id = absrep_id, 71 repabs_pseudo_id = repabs_pseudo_id, 72 cons_info = cons_info, newty = newty, 73 genind_term_REP = genind_term_REP} 74 75(* support *) 76val term_REP_eqv = prove( 77 ``support (fn_pmact ^t_pmact_t gt_pmact) ^term_REP_t {}`` , 78 srw_tac [][support_def, fnpm_def, FUN_EQ_THM, term_REP_tpm, pmact_sing_inv]); 79 80val supp_term_REP = prove( 81 ``supp (fn_pmact ^t_pmact_t gt_pmact) ^term_REP_t = {}``, 82 REWRITE_TAC [GSYM SUBSET_EMPTY] >> MATCH_MP_TAC (GEN_ALL supp_smallest) >> 83 srw_tac [][term_REP_eqv]) 84 85val tpm_def' = 86 term_REP_tpm |> AP_TERM term_ABS_t |> PURE_REWRITE_RULE [absrep_id] 87 88val t = mk_var("t", newty) 89val supptpm_support = prove( 90 ``support ^t_pmact_t ^t (supp gt_pmact (^term_REP_t ^t))``, 91 srw_tac [][support_def, tpm_def', supp_fresh, absrep_id]); 92 93val supptpm_apart = prove( 94 ``x ��� supp gt_pmact (^term_REP_t ^t) ��� y ��� supp gt_pmact (^term_REP_t ^t) ��� 95 ^tpm_t [(x,y)] ^t ��� ^t``, 96 srw_tac [][tpm_def']>> 97 DISCH_THEN (MP_TAC o AP_TERM term_REP_t) >> 98 srw_tac [][repabs_pseudo_id, genind_gtpm_eqn, genind_term_REP, supp_apart]); 99 100val supp_tpm = prove( 101 ``supp ^t_pmact_t ^t = supp gt_pmact (^term_REP_t ^t)``, 102 match_mp_tac (GEN_ALL supp_unique_apart) >> 103 srw_tac [][supptpm_support, supptpm_apart, FINITE_GFV]) 104 105val _ = overload_on ("FV", ``supp ^t_pmact_t``) 106 107val FINITE_FV = store_thm( 108 "FINITE_FV", 109 ``FINITE (FV t)``, 110 srw_tac [][supp_tpm, FINITE_GFV]); 111val _ = export_rewrites ["FINITE_FV"] 112 113fun supp_clause {con_termP, con_def} = let 114 val t = mk_comb(``supp ^t_pmact_t``, lhand (concl (SPEC_ALL con_def))) 115in 116 t |> REWRITE_CONV [supp_tpm, con_def, MATCH_MP repabs_pseudo_id con_termP, 117 GFV_thm] 118 |> REWRITE_RULE [supp_listpm, EMPTY_DELETE, UNION_EMPTY] 119 |> REWRITE_RULE [GSYM supp_tpm] 120 |> GEN_ALL 121end 122 123val FV_thm = Save_thm( 124 "FV_thm", 125 LIST_CONJ (map supp_clause cons_info)) 126 127 128 129fun genit th = let 130 val (_, args) = strip_comb (concl th) 131 val (tm, x) = case args of [x,y] => (x,y) | _ => raise Fail "Bind" 132 val ty = type_of tm 133 val t = mk_var("t", ty) 134in 135 th |> INST [tm |-> t] |> GEN x |> GEN t 136end 137 138val LIST_REL_CONS1 = listTheory.LIST_REL_CONS1 139val LIST_REL_NIL = listTheory.LIST_REL_NIL 140 141val term_ind = 142 bvc_genind 143 |> INST_TYPE [alpha |-> ``:unit+unit``, beta |-> ``:unit``] 144 |> Q.INST [`vp` |-> `^vp`, `lp` |-> `^lp`] 145 |> SIMP_RULE std_ss [LIST_REL_CONS1, RIGHT_AND_OVER_OR, 146 LEFT_AND_OVER_OR, DISJ_IMP_THM, LIST_REL_NIL] 147 |> Q.SPEC `��n t0 x. Q t0 x` 148 |> Q.SPEC `fv` 149 |> UNDISCH |> Q.SPEC `0` |> DISCH_ALL 150 |> SIMP_RULE (std_ss ++ DNF_ss) 151 [sumTheory.FORALL_SUM, supp_listpm, 152 IN_UNION, NOT_IN_EMPTY, oneTheory.FORALL_ONE, 153 genind_exists, LIST_REL_CONS1, LIST_REL_NIL] 154 |> Q.INST [`Q` |-> `��t. P (term_ABS t)`] 155 |> SIMP_RULE std_ss [GSYM LAM_def, APP_def', GSYM VAR_def, absrep_id] 156 |> SIMP_RULE (srw_ss()) [GSYM supp_tpm] 157 |> elim_unnecessary_atoms {finite_fv = FINITE_FV} 158 [ASSUME ``!x:'c. FINITE (fv x:string set)``] 159 |> SPEC_ALL |> UNDISCH 160 |> genit |> DISCH_ALL |> Q.GEN `fv` |> Q.GEN `P` 161 162fun mkX_ind th = th |> Q.SPEC `��t x. Q t` |> Q.SPEC `��x. X` 163 |> SIMP_RULE std_ss [] |> Q.GEN `X` 164 |> Q.INST [`Q` |-> `P`] |> Q.GEN `P` 165 166(* exactly mimic historical bound variable names etc for backwards 167 compatibility *) 168val nc_INDUCTION2 = store_thm( 169 "nc_INDUCTION2", 170 ``���P X. 171 (���s. P (VAR s)) ��� 172 (���t u. P t ��� P u ==> P (APP t u)) ��� 173 (���y u. y ��� X ��� P u ==> P (LAM y u)) ��� FINITE X ==> 174 ���u. P u``, 175 metis_tac [mkX_ind term_ind]); 176 177 178val LAM_eq_thm = save_thm( 179 "LAM_eq_thm", 180 ``(LAM u t1 = LAM v t2)`` 181 |> SIMP_CONV (srw_ss()) [LAM_def, LAM_termP, term_ABS_pseudo11, 182 GLAM_eq_thm, term_REP_11, GSYM term_REP_tpm, 183 GSYM supp_tpm] 184 |> GENL [``u:string``, ``v:string``, ``t1:term``, ``t2:term``]); 185 186 187 188 189val (_, repty) = dom_rng (type_of term_REP_t) 190val repty' = ty_antiq repty 191 192val tlf = 193 ``��(v:string) (u:unit + unit) (ds1:(�� -> ��) list) (ds2:(�� -> ��) list) 194 (ts1:^repty' list) (ts2:^repty' list) (p:��). 195 if ISR u then tlf (HD ds1) v (term_ABS (HD ts1)) p: �� 196 else taf (HD ds2) (HD (TL ds2)) (term_ABS (HD ts2)) 197 (term_ABS (HD (TL ts2))) p: ��`` 198val tvf = ``��(s:string) (u:unit) (p:��). tvf s p : ��`` 199 200val LENGTH_NIL' = 201 CONV_RULE (BINDER_CONV (LAND_CONV (REWR_CONV EQ_SYM_EQ))) 202 listTheory.LENGTH_NIL 203val LENGTH1 = prove( 204 ``(1 = LENGTH l) ��� ���e. l = [e]``, 205 Cases_on `l` >> srw_tac [][listTheory.LENGTH_NIL]); 206val LENGTH2 = prove( 207 ``(2 = LENGTH l) ��� ���a b. l = [a;b]``, 208 Cases_on `l` >> srw_tac [][LENGTH1]); 209 210val termP_elim = prove( 211 ``(���g. ^termP g ��� P g) ��� (���t. P (^term_REP_t t))``, 212 srw_tac [][EQ_IMP_THM] >- srw_tac [][genind_term_REP] >> 213 first_x_assum (qspec_then `^term_ABS_t g` mp_tac) >> 214 srw_tac [][repabs_pseudo_id]); 215 216val termP_removal = 217 nomdatatype.termP_removal { 218 elimth = termP_elim, absrep_id = absrep_id, 219 tpm_def = AP_TERM term_ABS_t term_REP_tpm |> REWRITE_RULE [absrep_id], 220 termP = termP, repty = repty} 221 222val termP0 = prove( 223 ``genind ^vp ^lp n t <=> ^termP t ��� (n = 0)``, 224 EQ_TAC >> simp_tac (srw_ss()) [] >> strip_tac >> 225 qsuff_tac `n = 0` >- (strip_tac >> srw_tac [][]) >> 226 pop_assum mp_tac >> 227 Q.ISPEC_THEN `t` STRUCT_CASES_TAC gterm_cases >> 228 srw_tac [][genind_GVAR, genind_GLAM_eqn]); 229 230 231 232val parameter_tm_recursion = save_thm( 233 "parameter_tm_recursion", 234 parameter_gtm_recursion 235 |> INST_TYPE [alpha |-> ``:unit + unit``, beta |-> ``:unit``, 236 gamma |-> alpha] 237 |> Q.INST [`lf` |-> `^tlf`, `vf` |-> `^tvf`, `vp` |-> `^vp`, 238 `lp` |-> `^lp`, `n` |-> `0`] 239 |> SIMP_RULE (srw_ss()) [sumTheory.FORALL_SUM, FORALL_AND_THM, 240 GSYM RIGHT_FORALL_IMP_THM, IMP_CONJ_THM, 241 GSYM RIGHT_EXISTS_AND_THM, 242 GSYM LEFT_EXISTS_AND_THM, 243 GSYM LEFT_FORALL_IMP_THM, 244 LIST_REL_CONS1, genind_GVAR, 245 genind_GLAM_eqn, sidecond_def, 246 NEWFCB_def, relsupp_def, 247 LENGTH_NIL', LENGTH1, LENGTH2] 248 |> ONCE_REWRITE_RULE [termP0] 249 |> SIMP_RULE (srw_ss() ++ DNF_ss) [LENGTH1, LENGTH2, 250 listTheory.LENGTH_NIL] 251 |> CONV_RULE (DEPTH_CONV termP_removal) 252 |> SIMP_RULE (srw_ss()) [GSYM supp_tpm, SYM term_REP_tpm] 253 |> UNDISCH 254 |> rpt_hyp_dest_conj 255 |> lift_exfunction {repabs_pseudo_id = repabs_pseudo_id, 256 term_REP_t = term_REP_t, 257 cons_info = cons_info} 258 |> DISCH_ALL 259 |> elim_unnecessary_atoms {finite_fv = FINITE_FV} 260 [ASSUME ``FINITE (A:string set)``, 261 ASSUME ``!p:��. FINITE (supp ppm p)``] 262 |> UNDISCH_ALL |> DISCH_ALL 263 |> REWRITE_RULE [AND_IMP_INTRO] 264 |> CONV_RULE (LAND_CONV (REWRITE_CONV [GSYM CONJ_ASSOC])) 265 |> Q.INST [`tvf` |-> `vr`, `tlf` |-> `lm`, `taf` |-> `ap`, 266 `dpm` |-> `apm`] 267 |> CONV_RULE (REDEPTH_CONV sort_uvars)) 268 269val FORALL_ONE = prove( 270 ``(!u:one. P u) = P ()``, 271 SRW_TAC [][EQ_IMP_THM, oneTheory.one_induction]); 272val FORALL_ONE_FN = prove( 273 ``(!uf : one -> 'a. P uf) = !a. P (\u. a)``, 274 SRW_TAC [][EQ_IMP_THM] THEN 275 POP_ASSUM (Q.SPEC_THEN `uf ()` MP_TAC) THEN 276 Q_TAC SUFF_TAC `(\y. uf()) = uf` THEN1 SRW_TAC [][] THEN 277 SRW_TAC [][FUN_EQ_THM, oneTheory.one]); 278 279val EXISTS_ONE_FN = prove( 280 ``(?f : 'a -> one -> 'b. P f) = (?f : 'a -> 'b. P (\x u. f x))``, 281 SRW_TAC [][EQ_IMP_THM] THENL [ 282 Q.EXISTS_TAC `\a. f a ()` THEN SRW_TAC [][] THEN 283 Q_TAC SUFF_TAC `(\x u. f x ()) = f` THEN1 SRW_TAC [][] THEN 284 SRW_TAC [][FUN_EQ_THM, oneTheory.one], 285 Q.EXISTS_TAC `\a u. f a` THEN SRW_TAC [][] 286 ]); 287 288val tm_recursion = save_thm( 289 "tm_recursion", 290 parameter_tm_recursion 291 |> Q.INST_TYPE [`:��` |-> `:unit`] 292 |> Q.INST [`ppm` |-> `discrete_pmact`, `vr` |-> `��s u. vru s`, 293 `ap` |-> `��r1 r2 t1 t2 u. apu (r1()) (r2()) t1 t2`, 294 `lm` |-> `��r v t u. lmu (r()) v t`] 295 |> SIMP_RULE (srw_ss()) [FORALL_ONE, FORALL_ONE_FN, EXISTS_ONE_FN, 296 fnpm_def] 297 |> SIMP_RULE (srw_ss() ++ CONJ_ss) [supp_unitfn] 298 |> Q.INST [`apu` |-> `ap`, `lmu` |-> `lm`, `vru` |-> `vr`]) 299 300val tm_recursion_nosideset = save_thm( 301 "tm_recursion_nosideset", 302 tm_recursion |> Q.INST [`A` |-> `{}`] 303 |> REWRITE_RULE [NOT_IN_EMPTY, FINITE_EMPTY]); 304 305val FV_tpm = Save_thm("FV_tpm", 306 ``x ��� FV (tpm p t)`` 307 |> REWRITE_CONV [perm_supp,pmact_IN] 308 |> GEN_ALL); 309 310val _ = set_mapped_fixity { term_name = "APP", tok = "@@", 311 fixity = Infixl 901} 312 313val FRESH_APP = Store_thm( 314 "FRESH_APP", 315 ``v NOTIN FV (M @@ N) <=> v NOTIN FV M /\ v NOTIN FV N``, 316 SRW_TAC [][]); 317val FRESH_LAM = Store_thm( 318 "FRESH_LAM", 319 ``u NOTIN FV (LAM v M) <=> (u <> v ==> u NOTIN FV M)``, 320 SRW_TAC [][] THEN METIS_TAC []); 321val FV_EMPTY = store_thm( 322 "FV_EMPTY", 323 ``(FV t = {}) <=> !v. v NOTIN FV t``, 324 SIMP_TAC (srw_ss()) [EXTENSION]); 325 326(* quote the term in order to get the variable names specified *) 327val simple_induction = store_thm( 328 "simple_induction", 329 ``!P. (!s. P (VAR s)) /\ 330 (!M N. P M /\ P N ==> P (M @@ N)) /\ 331 (!v M. P M ==> P (LAM v M)) ==> 332 !M. P M``, 333 METIS_TAC [nc_INDUCTION2, FINITE_EMPTY, NOT_IN_EMPTY]) 334 335val tpm_eqr = store_thm( 336 "tpm_eqr", 337 ``(t = tpm pi u) = (tpm (REVERSE pi) t = u)``, 338 METIS_TAC [pmact_inverse]); 339 340val tpm_CONS = store_thm( 341 "tpm_CONS", 342 ``tpm ((x,y)::pi) t = tpm [(x,y)] (tpm pi t)``, 343 SRW_TAC [][GSYM pmact_decompose]); 344 345val tpm_ALPHA = store_thm( 346 "tpm_ALPHA", 347 ``v ��� FV u ==> (LAM x u = LAM v (tpm [(v,x)] u))``, 348 SRW_TAC [boolSimps.CONJ_ss][LAM_eq_thm, pmact_flip_args]); 349 350(* cases theorem *) 351val term_CASES = store_thm( 352 "term_CASES", 353 ``!t. (?s. t = VAR s) \/ (?t1 t2. t = t1 @@ t2) \/ (?v t0. t = LAM v t0)``, 354 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THEN METIS_TAC []); 355 356(* should derive automatically *) 357val term_distinct = Store_thm( 358 "term_distinct", 359 ``VAR s ��� APP t1 t2 ��� VAR s ��� LAM v t ��� APP t1 t2 ��� LAM v t``, 360 srw_tac [][VAR_def, APP_def, LAM_def, LAM_termP, VAR_termP, APP_termP, 361 term_ABS_pseudo11, gterm_distinct, GLAM_eq_thm]); 362 363val term_11 = Store_thm( 364 "term_11", 365 ``((VAR s1 = VAR s2) <=> (s1 = s2)) ��� 366 ((t11 @@ t12 = t21 @@ t22) <=> (t11 = t21) ��� (t12 = t22)) ��� 367 ((LAM v t1 = LAM v t2) <=> (t1 = t2))``, 368 srw_tac [][VAR_def, APP_def, LAM_def, LAM_termP, VAR_termP, APP_termP, 369 term_ABS_pseudo11, gterm_11, term_REP_11]); 370 371(* "acyclicity" *) 372val APP_acyclic = store_thm( 373 "APP_acyclic", 374 ``!t1 t2. t1 <> t1 @@ t2 /\ t1 <> t2 @@ t1``, 375 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 376 377val FORALL_TERM = store_thm( 378 "FORALL_TERM", 379 ``(���t. P t) <=> 380 (���s. P (VAR s)) ��� (���t1 t2. P (t1 @@ t2)) ��� (���v t. P (LAM v t))``, 381 EQ_TAC THEN SRW_TAC [][] THEN 382 Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN SRW_TAC [][]); 383 384(* ---------------------------------------------------------------------- 385 Establish substitution function 386 ---------------------------------------------------------------------- *) 387 388val tpm_COND = prove( 389 ``tpm pi (if P then x else y) = if P then tpm pi x else tpm pi y``, 390 SRW_TAC [][]); 391 392val tpm_apart = store_thm( 393 "tpm_apart", 394 ``!t. ~(x IN FV t) /\ (y IN FV t) ==> ~(tpm [(x,y)] t = t)``, 395 metis_tac[supp_apart, pmact_flip_args]); 396 397val tpm_fresh = store_thm( 398 "tpm_fresh", 399 ``���t x y. x ��� FV t ��� y ��� FV t ==> (tpm [(x,y)] t = t)``, 400 srw_tac [][supp_fresh]); 401 402val rewrite_pairing = prove( 403 ``(���f: term -> (string # term) -> term. P f) <=> 404 (���f: term -> string -> term -> term. P (��M (x,N). f N x M))``, 405 EQ_TAC >> strip_tac >| [ 406 qexists_tac `��N x M. f M (x,N)` >> srw_tac [][] >> 407 CONV_TAC (DEPTH_CONV pairLib.PAIRED_ETA_CONV) >> 408 srw_tac [ETA_ss][], 409 qexists_tac `��M (x,N). f N x M` >> srw_tac [][] 410 ]); 411 412val subst_exists = 413 parameter_tm_recursion 414 |> INST_TYPE [alpha |-> ``:term``, ``:��`` |-> ``:string # term``] 415 |> SPEC_ALL 416 |> Q.INST [`A` |-> `{}`, `apm` |-> `^t_pmact_t`, 417 `ppm` |-> `pair_pmact string_pmact ^t_pmact_t`, 418 `vr` |-> `\s (x,N). if s = x then N else VAR s`, 419 `ap` |-> `\r1 r2 t1 t2 p. r1 p @@ r2 p`, 420 `lm` |-> `\r v t p. LAM v (r p)`] 421 |> CONV_RULE (LAND_CONV (SIMP_CONV (srw_ss()) [pairTheory.FORALL_PROD])) 422 |> SIMP_RULE (srw_ss()) [support_def, FUN_EQ_THM, fnpm_def, 423 tpm_COND, tpm_fresh, pmact_sing_inv, 424 basic_swapTheory.swapstr_eq_left] 425 |> SIMP_RULE (srw_ss()) [rewrite_pairing, pairTheory.FORALL_PROD] 426 |> CONV_RULE (DEPTH_CONV (rename_vars [("p_1", "u"), ("p_2", "N")])) 427 |> prove_alpha_fcbhyp {ppm = ``pair_pmact string_pmact ^t_pmact_t``, 428 rwts = [], 429 alphas = [tpm_ALPHA]} 430 431val SUB_DEF = new_specification("SUB_DEF", ["SUB"], subst_exists) 432 433val _ = add_rule {term_name = "SUB", fixity = Closefix, 434 pp_elements = [TOK "[", TM, TOK "/", TM, TOK "]"], 435 paren_style = OnlyIfNecessary, 436 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2))}; 437 438(* Give substitution theorems names compatible with historical usage *) 439 440val SUB_THMv = prove( 441 ``([N/x](VAR x) = N) /\ (~(x = y) ==> ([N/y](VAR x) = VAR x))``, 442 SRW_TAC [][SUB_DEF]); 443val SUB_COMM = prove( 444 ``���N x x' y t. 445 x' ��� x ��� x' ��� FV N ��� y ��� x ��� y ��� FV N ��� 446 (tpm [(x',y)] ([N/x] t) = [N/x] (tpm [(x',y)] t))``, 447 srw_tac [][SUB_DEF, supp_fresh]); 448 449 450val SUB_THM = save_thm( 451 "SUB_THM", 452 let val (eqns,_) = CONJ_PAIR SUB_DEF 453 in 454 CONJ (REWRITE_RULE [GSYM CONJ_ASSOC] 455 (LIST_CONJ (SUB_THMv :: tl (CONJUNCTS eqns)))) 456 SUB_COMM 457 end) 458val _ = export_rewrites ["SUB_THM"] 459val SUB_VAR = save_thm("SUB_VAR", hd (CONJUNCTS SUB_DEF)) 460 461(* ---------------------------------------------------------------------- 462 Results about substitution 463 ---------------------------------------------------------------------- *) 464 465Theorem fresh_tpm_subst: 466 !t. ~(u IN FV t) ==> (tpm [(u,v)] t = [VAR u/v] t) 467Proof 468 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 469 SRW_TAC [][SUB_THM, SUB_VAR] 470QED 471 472Theorem tpm_subst: 473 !N. tpm pi ([M/v] N) = [tpm pi M/lswapstr pi v] (tpm pi N) 474Proof 475 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 476 Q.EXISTS_TAC `v INSERT FV M` THEN 477 SRW_TAC [][SUB_THM, SUB_VAR] THEN 478 MATCH_MP_TAC (SUB_THM |> CONJUNCTS |> C (curry List.nth) 3 |> GSYM) THEN 479 SRW_TAC [][stringpm_raw] 480QED 481 482Theorem tpm_subst_out: 483 [M/v] (tpm pi N) = tpm pi ([tpm (REVERSE pi) M/lswapstr (REVERSE pi) v] N) 484Proof SRW_TAC [][tpm_subst] 485QED 486 487Theorem lemma14a[simp]: 488 !t. [VAR v/v] t = t 489Proof 490 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{v}` THEN 491 SRW_TAC [][SUB_THM, SUB_VAR] 492QED 493 494Theorem lemma14b: 495 !M. ~(v IN FV M) ==> ([N/v] M = M) 496Proof 497 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `v INSERT FV N` THEN 498 SRW_TAC [][SUB_THM, SUB_VAR] 499QED 500 501Theorem lemma14c: 502 !t x u. x IN FV u ==> (FV ([t/x]u) = FV t UNION (FV u DELETE x)) 503Proof 504 NTAC 2 GEN_TAC THEN HO_MATCH_MP_TAC nc_INDUCTION2 THEN 505 Q.EXISTS_TAC `x INSERT FV t` THEN 506 SRW_TAC [][SUB_THM, SUB_VAR, EXTENSION] THEN 507 METIS_TAC [lemma14b] 508QED 509 510Theorem FV_SUB: 511 !t u v. FV ([t/v] u) = if v ��� FV u then FV t ��� (FV u DELETE v) else FV u 512Proof PROVE_TAC [lemma14b, lemma14c] 513QED 514 515Theorem lemma15a: 516 !M. v ��� FV M ==> [N/v]([VAR v/x]M) = [N/x]M 517Proof 518 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;v} UNION FV N` THEN 519 SRW_TAC [][SUB_THM, SUB_VAR] 520QED 521 522Theorem lemma15b: 523 v ��� FV M ==> [VAR u/v]([VAR v/u] M) = M 524Proof SRW_TAC [][lemma15a] 525QED 526 527(* ---------------------------------------------------------------------- 528 alpha-convertibility results 529 ---------------------------------------------------------------------- *) 530 531Theorem SIMPLE_ALPHA: 532 y ��� FV u ==> !x. LAM x u = LAM y ([VAR y/x] u) 533Proof 534 SRW_TAC [][GSYM fresh_tpm_subst] THEN 535 SRW_TAC [boolSimps.CONJ_ss][LAM_eq_thm, pmact_flip_args] 536QED 537 538 539(* ---------------------------------------------------------------------- 540 size function 541 ---------------------------------------------------------------------- *) 542 543val size_exists = 544 tm_recursion 545 |> INST_TYPE [alpha |-> ``:num``] 546 |> SPEC_ALL 547 |> Q.INST [`A` |-> `{}`, `apm` |-> `discrete_pmact`, 548 `vr` |-> `\s. 1`, `ap` |-> `\m n t1 t2. m + n + 1`, 549 `lm` |-> `\m v t. m + 1`] 550 |> SIMP_RULE (srw_ss()) [] 551 552val size_def = new_specification("size_thm", ["size"], size_exists) 553Theorem size_thm[simp] = CONJUNCT1 size_def 554 555Theorem size_tpm[simp] = GSYM (CONJUNCT2 size_def) 556 557(* ---------------------------------------------------------------------- 558 iterated substitutions (ugh) 559 ---------------------------------------------------------------------- *) 560 561Definition ISUB_def: 562 ($ISUB t [] = t) 563 /\ ($ISUB t ((s,x)::rst) = $ISUB ([s/x]t) rst) 564End 565 566val _ = set_fixity "ISUB" (Infixr 501); 567 568val DOM_DEF = 569 Define 570 `(DOM [] = {}) 571 /\ (DOM ((x,y)::rst) = {y} UNION DOM rst)`; 572 573val FVS_DEF = 574 Define 575 `(FVS [] = {}) 576 /\ (FVS ((t,x)::rst) = FV t UNION FVS rst)`; 577 578 579val FINITE_DOM = Q.store_thm("FINITE_DOM", 580 `!ss. FINITE (DOM ss)`, 581Induct THENL [ALL_TAC, Cases] 582 THEN RW_TAC std_ss [DOM_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_SING]); 583val _ = export_rewrites ["FINITE_DOM"] 584 585 586val FINITE_FVS = Q.store_thm("FINITE_FVS", 587`!ss. FINITE (FVS ss)`, 588Induct THENL [ALL_TAC, Cases] 589 THEN RW_TAC std_ss [FVS_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_FV]); 590val _ = export_rewrites ["FINITE_FVS"] 591 592val ISUB_LAM = store_thm( 593 "ISUB_LAM", 594 ``!R x. ~(x IN (DOM R UNION FVS R)) ==> 595 !t. (LAM x t) ISUB R = LAM x (t ISUB R)``, 596 Induct THEN 597 ASM_SIMP_TAC (srw_ss()) [ISUB_def, pairTheory.FORALL_PROD, 598 DOM_DEF, FVS_DEF, SUB_THM]); 599 600(* ---------------------------------------------------------------------- 601 Simultaneous substitution (using a finite map) - much more interesting 602 ---------------------------------------------------------------------- *) 603 604val strterm_fmap_supp = store_thm( 605 "strterm_fmap_supp", 606 ``supp (fm_pmact string_pmact ^t_pmact_t) fmap = 607 FDOM fmap ��� 608 supp (set_pmact ^t_pmact_t) (FRANGE fmap)``, 609 SRW_TAC [][fmap_supp]); 610 611val FINITE_strterm_fmap_supp = store_thm( 612 "FINITE_strterm_fmap_supp", 613 ``FINITE (supp (fm_pmact string_pmact ^t_pmact_t) fmap)``, 614 SRW_TAC [][strterm_fmap_supp, supp_setpm] THEN SRW_TAC [][]); 615val _ = export_rewrites ["FINITE_strterm_fmap_supp"] 616 617val lem1 = prove( 618 ``���a. ~(a ��� supp (fm_pmact string_pmact ^t_pmact_t) fm)``, 619 Q_TAC (NEW_TAC "z") `supp (fm_pmact string_pmact ^t_pmact_t) fm` THEN 620 METIS_TAC []); 621 622val supp_FRANGE = prove( 623 ``~(x ��� supp (set_pmact ^t_pmact_t) (FRANGE fm)) = 624 ���y. y ��� FDOM fm ==> ~(x ��� FV (fm ' y))``, 625 SRW_TAC [][supp_setpm, finite_mapTheory.FRANGE_DEF] THEN METIS_TAC []); 626 627fun ex_conj1 thm = let 628 val (v,c) = dest_exists (concl thm) 629 val c1 = CONJUNCT1 (ASSUME c) 630 val fm = mk_exists(v,concl c1) 631in 632 CHOOSE (v, thm) (EXISTS(fm,v) c1) 633end 634 635val supp_EMPTY = prove( 636 ``(supp (set_pmact apm) {} = {})``, 637 srw_tac [][EXTENSION] >> match_mp_tac notinsupp_I >> 638 qexists_tac `{}` >> srw_tac [][support_def]); 639 640 641val lem2 = prove( 642 ``���fm. FINITE (supp (set_pmact ^t_pmact_t) (FRANGE fm))``, 643 srw_tac [][supp_setpm] >> srw_tac [][]); 644 645val ordering = prove( 646 ``(���f. P f) <=> (���f. P (combin$C f))``, 647 srw_tac [][EQ_IMP_THM] >- 648 (qexists_tac `��x y. f y x` >> srw_tac [ETA_ss][combinTheory.C_DEF]) >> 649 metis_tac []) 650 651val notin_frange = prove( 652 ``v ��� supp (set_pmact ^t_pmact_t) (FRANGE p) <=> ���y. y ��� FDOM p ==> v ��� FV (p ' y)``, 653 srw_tac [][supp_setpm, EQ_IMP_THM, finite_mapTheory.FRANGE_DEF] >> 654 metis_tac []); 655 656val ssub_exists = 657 parameter_tm_recursion 658 |> INST_TYPE [alpha |-> ``:term``, ``:��`` |-> ``:string |-> term``] 659 |> Q.INST [`vr` |-> `\s fm. if s ��� FDOM fm then fm ' s else VAR s`, 660 `lm` |-> `\r v t fm. LAM v (r fm)`, `apm` |-> `^t_pmact_t`, 661 `ppm` |-> `fm_pmact string_pmact ^t_pmact_t`, 662 `ap` |-> `\r1 r2 t1 t2 fm. r1 fm @@ r2 fm`, 663 `A` |-> `{}`] 664 |> SIMP_RULE (srw_ss()) [tpm_COND, strterm_fmap_supp, lem2, 665 FAPPLY_eqv_lswapstr, supp_fresh, 666 pmact_sing_inv, fnpm_def, 667 fmpm_FDOM, notin_frange] 668 |> SIMP_RULE (srw_ss()) [Once ordering] 669 |> CONV_RULE (DEPTH_CONV (rename_vars [("p", "fm")])) 670 |> prove_alpha_fcbhyp {ppm = ``fm_pmact string_pmact ^t_pmact_t``, 671 rwts = [notin_frange, strterm_fmap_supp], 672 alphas = [tpm_ALPHA]} 673 674val ssub_def = new_specification ("ssub_def", ["ssub"], ssub_exists) 675val ssub_thm = Save_thm("ssub_thm", CONJUNCT1 ssub_def) 676 677val _ = overload_on ("'", ``ssub``) 678 679val tpm_ssub = save_thm("tpm_ssub", CONJUNCT2 ssub_def) 680 681val single_ssub = store_thm( 682 "single_ssub", 683 ``���N. (FEMPTY |+ (s,M)) ' N = [M/s]N``, 684 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `s INSERT FV M` THEN 685 SRW_TAC [][SUB_VAR, SUB_THM]); 686 687val in_fmap_supp = store_thm( 688 "in_fmap_supp", 689 ``x ��� supp (fm_pmact string_pmact ^t_pmact_t) fm <=> 690 x ��� FDOM fm ��� 691 ���y. y ��� FDOM fm ��� x ��� FV (fm ' y)``, 692 SRW_TAC [][strterm_fmap_supp, nomsetTheory.supp_setpm] THEN 693 SRW_TAC [boolSimps.DNF_ss][finite_mapTheory.FRANGE_DEF] THEN METIS_TAC []); 694 695val not_in_fmap_supp = store_thm( 696 "not_in_fmap_supp", 697 ``x ��� supp (fm_pmact string_pmact ^t_pmact_t) fm <=> 698 x ��� FDOM fm ��� ���y. y ��� FDOM fm ==> x ��� FV (fm ' y)``, 699 METIS_TAC [in_fmap_supp]); 700val _ = export_rewrites ["not_in_fmap_supp"] 701 702val ssub_14b = store_thm( 703 "ssub_14b", 704 ``���t. (FV t ��� FDOM phi = EMPTY) ==> ((phi : string |-> term) ' t = t)``, 705 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 706 Q.EXISTS_TAC `supp (fm_pmact string_pmact ^t_pmact_t) phi` THEN 707 SRW_TAC [][SUB_THM, SUB_VAR, pred_setTheory.EXTENSION] THEN METIS_TAC []); 708 709val ssub_value = store_thm( 710 "ssub_value", 711 ``(FV t = EMPTY) ==> ((phi : string |-> term) ' t = t)``, 712 SRW_TAC [][ssub_14b]); 713 714val ssub_FEMPTY = store_thm( 715 "ssub_FEMPTY", 716 ``���t. (FEMPTY:string|->term) ' t = t``, 717 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 718val _ = export_rewrites ["ssub_FEMPTY"] 719 720(* ---------------------------------------------------------------------- 721 Set up the recursion functionality in binderLib 722 ---------------------------------------------------------------------- *) 723 724val lemma = prove( 725 ``(���x y t. pmact apm [(x,y)] (h t) = h (tpm [(x,y)] t)) <=> 726 ���pi t. pmact apm pi (h t) = h (tpm pi t)``, 727 simp_tac (srw_ss()) [EQ_IMP_THM] >> ONCE_REWRITE_TAC [EQ_SYM_EQ] >> 728 strip_tac >> Induct_on `pi` >> 729 asm_simp_tac (srw_ss()) [pmact_nil, pairTheory.FORALL_PROD] >> 730 srw_tac [][Once tpm_CONS] >> srw_tac [][GSYM pmact_decompose]); 731 732val tm_recursion_nosideset = save_thm( 733 "tm_recursion_nosideset", 734 tm_recursion |> Q.INST [`A` |-> `{}`] |> SIMP_RULE (srw_ss()) [lemma]) 735 736val term_info_string = 737 "local\n\ 738 \fun k |-> v = {redex = k, residue = v}\n\ 739 \open binderLib\n\ 740 \val term_info = \n\ 741 \ NTI {nullfv = ``LAM \"\" (VAR \"\")``,\n\ 742 \ pm_rewrites = [],\n\ 743 \ pm_constant = ``nomset$mk_pmact term$raw_tpm``,\n\ 744 \ fv_rewrites = [],\n\ 745 \ recursion_thm = SOME tm_recursion_nosideset,\n\ 746 \ binders = [(``term$LAM``, 0, tpm_ALPHA)]}\n\ 747 \val _ = type_db :=\n\ 748 \ Binarymap.insert(!type_db,\n\ 749 \ {Name = \"term\",Thy=\"term\"},\n\ 750 \ term_info)\n\ 751 \in end;\n" 752 753val _ = adjoin_after_completion (fn _ => PP.add_string term_info_string) 754 755 756val _ = export_theory() 757