1open HolKernel boolLib Parse bossLib BasicProvers 2open pred_setTheory 3 4open binderLib 5open basic_swapTheory nomsetTheory generic_termsTheory 6open nomdatatype 7open boolSimps 8 9 10val _ = new_theory "labelledTerms" 11 12val tyname = "lterm" 13 14val vp = ���(��n u: unit. n = 0)��� 15 16val lp = ���(��n (d:unit + unit + num) tns uns. 17 (n = 0) ��� ISL d ��� (tns = []) ��� (uns = [0;0]) ��� 18 (n = 0) ��� ISR d ��� ISL (OUTR d) ��� (tns = [0]) ��� (uns = []) ��� 19 (n = 0) ��� ISR d ��� ISR (OUTR d) ��� (tns = [0]) ��� (uns = [0]))��� 20 21val {term_ABS_pseudo11, term_REP_11, genind_term_REP, genind_exists, 22 termP, absrep_id, repabs_pseudo_id, newty, term_REP_t, term_ABS_t,...} = 23 new_type_step1 tyname 0 {vp=vp, lp = lp} 24 25val _ = temp_overload_on ("termP", termP) 26 27val [gvar,glam] = genind_rules |> SPEC_ALL |> CONJUNCTS 28val qnewty = ty_antiq newty 29 30fun defined_const th = th |> concl |> strip_forall |> #2 |> lhs |> repeat rator 31 32val LAM_t = mk_var("LAM", ���:string -> ^newty -> ^newty���) 33val LAM_def = new_definition( 34 "LAM_def", 35 ���^LAM_t v t = ^term_ABS_t (GLAM v (INR (INL ())) [^term_REP_t t] [])���); 36val LAM_termP = prove( 37 mk_comb(termP, LAM_def |> SPEC_ALL |> concl |> rhs |> rand), 38 match_mp_tac glam >> srw_tac [][genind_term_REP]) 39val LAM_t = defined_const LAM_def 40 41val LAMi_t = mk_var("LAMi", ���:num -> string -> ^newty -> ^newty -> ^newty���) 42val LAMi_def = new_definition( 43 "LAMi_def", 44 ���^LAMi_t n v t1 t2 = 45 ^term_ABS_t (GLAM v (INR (INR n)) [^term_REP_t t1] [^term_REP_t t2])���); 46val LAMi_termP = prove( 47 mk_comb(termP, LAMi_def |> SPEC_ALL |> concl |> rhs |> rand), 48 match_mp_tac glam >> srw_tac [][genind_term_REP]); 49val LAMi_t = defined_const LAMi_def 50 51val APP_t = mk_var("APP", ���:^newty -> ^newty -> ^newty���) 52val APP_pattern = ���GLAM v (INL ()) [] [^term_REP_t t1; ^term_REP_t t2]��� 53val APP_def = new_definition( 54 "APP_def", 55 ���^APP_t t1 t2 = 56 ^term_ABS_t ^(subst [���v:string��� |-> ���ARB:string���] APP_pattern)���); 57val APP_t = defined_const APP_def 58val APP_termP = prove( 59 mk_comb(termP, APP_pattern), 60 match_mp_tac glam >> srw_tac [][genind_term_REP]); 61 62val APP_def' = prove( 63 ���^term_ABS_t ^APP_pattern = ^APP_t t1 t2���, 64 srw_tac [][APP_def, GLAM_NIL_EQ, term_ABS_pseudo11, APP_termP]); 65 66 67val VAR_t = mk_var("VAR", ���:string -> ^newty���) 68val VAR_def = new_definition( 69 "VAR_def", 70 ���^VAR_t s = ^term_ABS_t (GVAR s ())���); 71val VAR_termP = prove( 72 mk_comb(termP, VAR_def |> SPEC_ALL |> concl |> rhs |> rand), 73 match_mp_tac gvar >> srw_tac [][genind_term_REP]); 74val VAR_t = defined_const VAR_def 75 76val cons_info = 77 [{con_termP = VAR_termP, con_def = VAR_def}, 78 {con_termP = APP_termP, con_def = SYM APP_def'}, 79 {con_termP = LAM_termP, con_def = LAM_def}, 80 {con_termP = LAMi_termP, con_def = LAMi_def}] 81 82(* tpm *) 83val name_pfx = "lt" 84val tpm_name = name_pfx ^ "pm" 85val {tpm_thm, term_REP_tpm, t_pmact_t, tpm_t} = 86 define_permutation { name_pfx = "lt", name = tyname, 87 term_REP_t = term_REP_t, 88 term_ABS_t = term_ABS_t, 89 absrep_id = absrep_id, 90 repabs_pseudo_id = repabs_pseudo_id, 91 cons_info = cons_info, newty = newty, 92 genind_term_REP = genind_term_REP} 93 94val ltpm_eqr = store_thm( 95 "ltpm_eqr", 96 ���(t = ltpm pi u) = (ltpm (REVERSE pi) t = u)���, 97 METIS_TAC [pmact_inverse]); 98 99(* support *) 100(* support *) 101val term_REP_eqv = prove( 102 ���support (fn_pmact ^t_pmact_t gt_pmact) ^term_REP_t {}��� , 103 srw_tac [][support_def, fnpm_def, FUN_EQ_THM, term_REP_tpm, pmact_sing_inv]); 104 105val supp_term_REP = prove( 106 ���supp (fn_pmact ^t_pmact_t gt_pmact) ^term_REP_t = {}���, 107 REWRITE_TAC [GSYM SUBSET_EMPTY] >> MATCH_MP_TAC (GEN_ALL supp_smallest) >> 108 srw_tac [][term_REP_eqv]) 109 110val tpm_def' = 111 term_REP_tpm |> AP_TERM term_ABS_t |> PURE_REWRITE_RULE [absrep_id] 112 113val t = mk_var("t", newty) 114val supptpm_support = prove( 115 ���support ^t_pmact_t ^t (supp gt_pmact (^term_REP_t ^t))���, 116 srw_tac [][support_def, tpm_def', supp_fresh, absrep_id]); 117 118val supptpm_apart = prove( 119 ���x ��� supp gt_pmact (^term_REP_t ^t) ��� y ��� supp gt_pmact (^term_REP_t ^t) ��� 120 ^tpm_t [(x,y)] ^t ��� ^t���, 121 srw_tac [][tpm_def']>> 122 DISCH_THEN (MP_TAC o AP_TERM term_REP_t) >> 123 srw_tac [][repabs_pseudo_id, genind_gtpm_eqn, genind_term_REP, supp_apart]); 124 125val supp_tpm = prove( 126 ���supp ^t_pmact_t ^t = supp gt_pmact (^term_REP_t ^t)���, 127 match_mp_tac (GEN_ALL supp_unique_apart) >> 128 srw_tac [][supptpm_support, supptpm_apart, FINITE_GFV]) 129 130val _ = overload_on ("FV", ���supp ^t_pmact_t���) 131 132Theorem FINITE_FV[simp]: 133 FINITE (FV ^t) 134Proof srw_tac [][supp_tpm, FINITE_GFV] 135QED 136 137fun supp_clause {con_termP, con_def} = let 138 val t = mk_comb(���supp ^t_pmact_t���, lhand (concl (SPEC_ALL con_def))) 139in 140 t |> REWRITE_CONV [supp_tpm, con_def, MATCH_MP repabs_pseudo_id con_termP, 141 GFV_thm] 142 |> REWRITE_RULE [supp_listpm, EMPTY_DELETE, UNION_EMPTY] 143 |> REWRITE_RULE [GSYM supp_tpm] 144 |> GEN_ALL 145end 146 147Theorem FV_thm[simp] = LIST_CONJ (map supp_clause cons_info) 148 149fun genit th = let 150 val (_, args) = strip_comb (concl th) 151 val (tm, x) = case args of [x,y] => (x,y) | _ => raise Fail "Bind" 152 val ty = type_of tm 153 val t = mk_var("t", ty) 154in 155 th |> INST [tm |-> t] |> GEN x |> GEN t 156end 157 158val LIST_REL_CONS1 = listTheory.LIST_REL_CONS1 159val LIST_REL_NIL = listTheory.LIST_REL_NIL 160 161val term_ind = 162 bvc_genind |> INST_TYPE [alpha |-> ���:unit+unit+num���, beta |-> ���:unit���] 163 |> Q.INST [���vp��� |-> ���^vp���, ���lp��� |-> ���^lp���] 164 |> SIMP_RULE std_ss [LIST_REL_CONS1, RIGHT_AND_OVER_OR, 165 LEFT_AND_OVER_OR, DISJ_IMP_THM, LIST_REL_NIL] 166 |> Q.SPEC �����n t0 x. Q t0 x��� 167 |> Q.SPEC ���fv��� 168 |> UNDISCH |> Q.SPEC ���0��� |> DISCH_ALL 169 |> SIMP_RULE (std_ss ++ DNF_ss) 170 [sumTheory.FORALL_SUM, supp_listpm, 171 IN_UNION, NOT_IN_EMPTY, oneTheory.FORALL_ONE, 172 genind_exists, LIST_REL_CONS1, LIST_REL_NIL] 173 |> Q.INST [���Q��� |-> �����t. P (^term_ABS_t t)���] 174 |> SIMP_RULE std_ss [GSYM LAM_def, APP_def', GSYM VAR_def, absrep_id, 175 GSYM LAMi_def, GSYM supp_tpm] 176 |> elim_unnecessary_atoms {finite_fv = FINITE_FV} 177 [ASSUME ���!x:'c. FINITE (fv x:string set)���] 178 |> SPEC_ALL |> UNDISCH 179 |> genit |> DISCH_ALL |> Q.GEN ���fv��� |> Q.GEN ���P��� 180 181fun mkX_ind th = th |> Q.SPEC �����t x. Q t��� |> Q.SPEC �����x. X��� 182 |> SIMP_RULE std_ss [] |> Q.GEN ���X��� 183 |> Q.INST [���Q��� |-> ���P���] |> Q.GEN ���P��� 184 185val LAMi_eq_thm = save_thm( 186 "lLAMi_eq_thm", 187 ���^LAMi_t n1 v1 t1 u1 = ^LAMi_t n2 v2 t2 u2��� 188 |> SIMP_CONV (srw_ss()) [LAMi_def, LAMi_termP, term_ABS_pseudo11, 189 GLAM_eq_thm, term_REP_11, GSYM term_REP_tpm, 190 GSYM supp_tpm]) 191 192val LAM_eq_thm = save_thm( 193 "lLAM_eq_thm", 194 ���^LAM_t v1 t1 = ^LAM_t v2 t2��� 195 |> SIMP_CONV (srw_ss()) [LAM_def, LAM_termP, term_ABS_pseudo11, 196 GLAM_eq_thm, term_REP_11, GSYM term_REP_tpm, 197 GSYM supp_tpm]) 198 199val (_, repty) = dom_rng (type_of term_REP_t) 200val repty' = ty_antiq repty 201 202val tlf = 203 �����(v:string) (u:unit + unit + num) 204 (ds1:(�� -> ��) list) (ds2:(�� -> ��) list) 205 (ts1:^repty' list) (ts2:^repty' list) (p:��). 206 if ISL u then ap (HD ds2) (HD (TL ds2)) (^term_ABS_t (HD ts2)) 207 (^term_ABS_t (HD (TL ts2))) p: �� 208 else if ISL (OUTR u) then 209 lm (HD ds1) v (^term_ABS_t (HD ts1)) p: �� 210 else 211 li (HD ds1) (HD ds2) (OUTR (OUTR u)) v 212 (^term_ABS_t (HD ts1)) (^term_ABS_t (HD ts2)) p��� 213val tvf = �����(s:string) (u:unit) (p:��). vr' s p: ����� 214 215val termP0 = prove( 216 ���genind ^vp ^lp n t <=> ^termP t ��� (n = 0)���, 217 EQ_TAC >> simp_tac (srw_ss()) [] >> strip_tac >> 218 qsuff_tac ���n = 0��� >- (strip_tac >> srw_tac [][]) >> 219 pop_assum mp_tac >> 220 Q.ISPEC_THEN ���t��� STRUCT_CASES_TAC gterm_cases >> 221 srw_tac [][genind_GVAR, genind_GLAM_eqn]); 222 223val LENGTH_NIL' = 224 CONV_RULE (BINDER_CONV (LAND_CONV (REWR_CONV EQ_SYM_EQ))) 225 listTheory.LENGTH_NIL 226val LENGTH1 = prove( 227 ���(1 = LENGTH l) ��� ���e. l = [e]���, 228 Cases_on ���l��� >> srw_tac [][listTheory.LENGTH_NIL]); 229val LENGTH2 = prove( 230 ���(2 = LENGTH l) ��� ���a b. l = [a;b]���, 231 Cases_on ���l��� >> srw_tac [][LENGTH1]); 232 233val termP_elim = prove( 234 ���(���g. ^termP g ��� P g) ��� (���t. P (^term_REP_t t))���, 235 srw_tac [][EQ_IMP_THM] >- srw_tac [][genind_term_REP] >> 236 first_x_assum (qspec_then ���^term_ABS_t g��� mp_tac) >> 237 srw_tac [][repabs_pseudo_id]); 238 239val termP_removal = 240 nomdatatype.termP_removal { 241 repty = repty, termP = termP, 242 elimth = termP_elim, 243 tpm_def = AP_TERM term_ABS_t term_REP_tpm |> REWRITE_RULE [absrep_id], 244 absrep_id = absrep_id} 245 246val parameter_tm_recursion = save_thm( 247 "parameter_ltm_recursion", 248 parameter_gtm_recursion 249 |> INST_TYPE [alpha |-> ���:unit + unit + num���, beta |-> ���:unit���, 250 gamma |-> alpha] 251 |> Q.INST [���lf��� |-> ���^tlf���, ���vf��� |-> ���^tvf���, ���vp��� |-> ���^vp���, 252 ���lp��� |-> ���^lp���, ���n��� |-> ���0���] 253 |> SIMP_RULE (srw_ss()) [sumTheory.FORALL_SUM, FORALL_AND_THM, 254 GSYM RIGHT_FORALL_IMP_THM, IMP_CONJ_THM, 255 GSYM RIGHT_EXISTS_AND_THM, 256 GSYM LEFT_EXISTS_AND_THM, 257 GSYM LEFT_FORALL_IMP_THM, 258 LIST_REL_CONS1, genind_GVAR, 259 genind_GLAM_eqn, NEWFCB_def, 260 sidecond_def, relsupp_def, 261 LENGTH_NIL', LENGTH1, LENGTH2] 262 |> ONCE_REWRITE_RULE [termP0] 263 |> SIMP_RULE (srw_ss() ++ DNF_ss) [LENGTH1, LENGTH2, 264 listTheory.LENGTH_NIL] 265 |> CONV_RULE (DEPTH_CONV termP_removal) 266 |> SIMP_RULE (srw_ss()) [GSYM supp_tpm, SYM term_REP_tpm] 267 |> UNDISCH 268 |> rpt_hyp_dest_conj 269 |> lift_exfunction {repabs_pseudo_id = repabs_pseudo_id, 270 term_REP_t = term_REP_t, 271 cons_info = cons_info} 272 |> DISCH_ALL 273 |> elim_unnecessary_atoms {finite_fv = FINITE_FV} 274 [ASSUME ���FINITE (A:string set)���, 275 ASSUME ���!p:��. FINITE (supp ppm p)���] 276 |> UNDISCH_ALL |> DISCH_ALL 277 |> REWRITE_RULE [AND_IMP_INTRO] 278 |> CONV_RULE (LAND_CONV (REWRITE_CONV [GSYM CONJ_ASSOC])) 279 |> Q.INST [���vr'��� |-> ���vr���, ���dpm��� |-> ���apm���] 280 |> CONV_RULE (REDEPTH_CONV sort_uvars)) 281 282val FORALL_ONE = prove( 283 ���(!u:one. P u) = P ()���, 284 SRW_TAC [][EQ_IMP_THM, oneTheory.one_induction]); 285val FORALL_ONE_FN = prove( 286 ���(!uf : one -> 'a. P uf) = !a. P (\u. a)���, 287 SRW_TAC [][EQ_IMP_THM] THEN 288 POP_ASSUM (Q.SPEC_THEN ���uf ()��� MP_TAC) THEN 289 Q_TAC SUFF_TAC ���(\y. uf()) = uf��� THEN1 SRW_TAC [][] THEN 290 SRW_TAC [][FUN_EQ_THM, oneTheory.one]); 291 292val EXISTS_ONE_FN = prove( 293 ���(?f : 'a -> one -> 'b. P f) = (?f : 'a -> 'b. P (\x u. f x))���, 294 SRW_TAC [][EQ_IMP_THM] THENL [ 295 Q.EXISTS_TAC ���\a. f a ()��� THEN SRW_TAC [][] THEN 296 Q_TAC SUFF_TAC ���(\x u. f x ()) = f��� THEN1 SRW_TAC [][] THEN 297 SRW_TAC [][FUN_EQ_THM, oneTheory.one], 298 Q.EXISTS_TAC ���\a u. f a��� THEN SRW_TAC [][] 299 ]); 300 301val tm_recursion = save_thm( 302 "tm_recursion", 303 parameter_tm_recursion 304 |> Q.INST_TYPE [���:����� |-> ���:unit���] 305 |> Q.INST [���ppm��� |-> ���discrete_pmact���, ���vr��� |-> �����s u. vru s���, 306 ���ap��� |-> �����r1 r2 t1 t2 u. apu (r1()) (r2()) t1 t2���, 307 ���lm��� |-> �����r v t u. lmu (r()) v t���, 308 ���li��� |-> �����r1 r2 n v t1 t2 u. liu (r1()) (r2()) n v t1 t2���] 309 |> SIMP_RULE (srw_ss()) [FORALL_ONE, FORALL_ONE_FN, EXISTS_ONE_FN, 310 fnpm_def] 311 |> SIMP_RULE (srw_ss() ++ CONJ_ss) [supp_unitfn] 312 |> Q.INST [���apu��� |-> ���ap���, ���lmu��� |-> ���lm���, ���vru��� |-> ���vr���, 313 ���liu��� |-> ���li���]) 314 315val simple_induction = save_thm( 316 "simple_lterm_induction", 317 term_ind |> INST_TYPE [gamma |-> oneSyntax.one_ty] 318 |> SPECL [���\t:lterm u:unit. P t:bool���, ���\x:unit. {}:string set���] 319 |> SIMP_RULE bool_ss [FINITE_EMPTY, NOT_IN_EMPTY] 320 |> GEN ���P:lterm -> bool���) 321 322val lterm_bvc_induction = store_thm( 323 "lterm_bvc_induction", 324 ���!P X. FINITE X /\ 325 (!s. P (VAR s)) /\ 326 (!M N. P M /\ P N ==> P (APP M N)) /\ 327 (!v M. ~(v IN X) /\ P M ==> P (LAM v M)) /\ 328 (!n v M N. ~(v IN X) /\ ~(v IN FV N) /\ P M /\ P N ==> 329 P (LAMi n v M N)) ==> 330 !t. P t���, 331 rpt gen_tac >> strip_tac >> ho_match_mp_tac (mkX_ind term_ind) >> 332 qexists_tac ���X��� >> srw_tac [][]); 333 334Theorem FV_tpm[simp] = 335 ���x ��� FV (ltpm p lt)��� 336 |> REWRITE_CONV [perm_supp, pmact_IN] 337 |> GEN_ALL 338 339val _ = set_mapped_fixity {tok = "@@", fixity = Infixl 901, term_name = "APP"} 340 341Theorem lterm_distinct[simp]: 342 VAR s ��� t @@ u ��� VAR s ��� LAM v t ��� VAR s ��� LAMi n v t u ��� 343 t @@ u ��� LAM v t' ��� t @@ u ��� LAMi n v t1 t2 ��� 344 LAM v t ��� LAMi n w t1 t2 345Proof 346 srw_tac [][LAM_def, LAMi_def, VAR_def, APP_def, VAR_termP, APP_termP, 347 LAM_termP, LAMi_termP, term_ABS_pseudo11, gterm_distinct, 348 GLAM_eq_thm] 349QED 350 351Theorem lterm_11[simp]: 352 ((VAR s1 = VAR s2) <=> (s1 = s2)) ��� 353 ((t11 @@ t12 = t21 @@ t22) <=> (t11 = t21) ��� (t12 = t22)) ��� 354 ((LAM v t1 = LAM v t2) <=> (t1 = t2)) ��� 355 ((LAMi n1 v t11 t12 = LAMi n2 v t21 t22) <=> 356 (n1 = n2) ��� (t11 = t21) ��� (t12 = t22)) 357Proof 358 srw_tac [][VAR_def, APP_def, LAM_def, LAM_termP, VAR_termP, APP_termP, 359 LAMi_def, LAMi_termP, 360 term_ABS_pseudo11, gterm_11, term_REP_11] 361QED 362 363val term_CASES = save_thm( 364 tyname ^ "_CASES", 365 hd (Prim_rec.prove_cases_thm simple_induction)) 366 367(* alpha-convertibility *) 368val ltpm_ALPHA = store_thm( 369 "ltpm_ALPHA", 370 ���~(v IN FV t) ==> (LAM u t = LAM v (ltpm [(v,u)] t))���, 371 SRW_TAC [boolSimps.CONJ_ss][LAM_eq_thm, pmact_flip_args]); 372val ltpm_ALPHAi = store_thm( 373 "ltpm_ALPHAi", 374 ���~(v IN FV t) ==> (LAMi n u t M = LAMi n v (ltpm [(v,u)] t) M)���, 375 SRW_TAC [boolSimps.CONJ_ss][LAMi_eq_thm, pmact_flip_args]); 376 377val ltpm_apart = store_thm( 378 "ltpm_apart", 379 ���!t. x IN FV t /\ y NOTIN FV t ==> ~(ltpm [(x,y)] t = t)���, 380 srw_tac [][supp_apart]) 381 382val tpm_COND = prove( 383 ���ltpm pi (if P then x else y) = if P then ltpm pi x else ltpm pi y���, 384 srw_tac [][]); 385 386val reordering = prove( 387 ���(?(f:lterm -> (string # lterm) -> lterm). P f) <=> 388 (?f. P (\M (v,N). f N v M))���, 389 EQ_TAC THEN STRIP_TAC THENL [ 390 Q.EXISTS_TAC �����N x M. f M (x,N)��� THEN SRW_TAC [][] THEN 391 CONV_TAC (REDEPTH_CONV pairLib.PAIRED_ETA_CONV) THEN 392 SRW_TAC [ETA_ss][], 393 Q.EXISTS_TAC �����M (x,N). f N x M��� THEN SRW_TAC [][] 394 ]); 395 396val subst_exists = 397 parameter_tm_recursion 398 |> INST_TYPE [alpha |-> ���:lterm���, ���:����� |-> ���:string # lterm���] 399 |> Q.INST [���A��� |-> ���{}���, ���apm��� |-> ���^t_pmact_t���, 400 ���ppm��� |-> ���pair_pmact string_pmact ^t_pmact_t���, 401 ���vr��� |-> ���\s (x,N). if s = x then N else VAR s���, 402 ���ap��� |-> ���\r1 r2 t1 t2 p. APP (r1 p) (r2 p)���, 403 ���lm��� |-> ���\r v t p. LAM v (r p)���, 404 ���li��� |-> ���\r1 r2 n v t1 t2 p. LAMi n v (r1 p) (r2 p)���] 405 |> SIMP_RULE (srw_ss()) [tpm_COND, basic_swapTheory.swapstr_eq_left, 406 supp_fresh, fnpm_def, supp_fresh, 407 pmact_sing_inv, pairTheory.FORALL_PROD, 408 reordering] 409 |> elim_unnecessary_atoms {finite_fv = FINITE_FV} [] 410 |> prove_alpha_fcbhyp {ppm = ���pair_pmact string_pmact ^t_pmact_t���, 411 alphas = [ltpm_ALPHA, ltpm_ALPHAi], 412 rwts = []} 413 |> CONV_RULE (DEPTH_CONV 414 (rename_vars [("p_1", "u"), ("p_2", "N")])) 415 416val SUB_DEF = new_specification("lSUB_DEF", ["SUB"], subst_exists) 417 418val _ = add_rule {term_name = "SUB", fixity = Closefix, 419 pp_elements = [TOK "[", TM, TOK "/", TM, TOK "]"], 420 paren_style = OnlyIfNecessary, 421 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2))}; 422 423val fresh_ltpm_subst = store_thm( 424 "fresh_ltpm_subst", 425 ���!t. ~(u IN FV t) ==> (ltpm [(u,v)] t = [VAR u/v] t)���, 426 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC ���{u;v}��� THEN 427 SRW_TAC [][SUB_DEF]); 428 429Theorem l14a[simp]: 430 !t : lterm. [VAR v/v] t = t 431Proof 432 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC ���{v}��� THEN 433 SRW_TAC [][SUB_DEF] 434QED 435 436val l14b = store_thm( 437 "l14b", 438 ���!t:lterm. ~(v IN FV t) ==> ([u/v]t = t)���, 439 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC ���v INSERT FV u��� THEN 440 SRW_TAC [][SUB_DEF]); 441 442val NOT_IN_FV_SUB_I = store_thm( 443 "NOT_IN_FV_SUB_I", 444 ������N u v M:lterm. v ��� FV N ��� v ��� u ��� v ��� FV M ==> v ��� FV ([N/u]M)���, 445 NTAC 3 gen_tac >> ho_match_mp_tac lterm_bvc_induction >> 446 qexists_tac ���FV N ��� {u;v}��� >> srw_tac [][SUB_DEF]); 447 448Theorem lSUB_THM[simp]: 449 ([N/x] (VAR x) = N) /\ (~(x = y) ==> ([N/x] (VAR y) = VAR y)) /\ 450 ([N/x] (M @@ P) = [N/x] M @@ [N/x] P) /\ 451 (~(v IN FV N) /\ ~(v = x) ==> ([N/x] (LAM v M) = LAM v ([N/x] M))) /\ 452 (~(v IN FV N) /\ ~(v = x) ==> 453 ([N/x] (LAMi n v M P) = LAMi n v ([N/x]M) ([N/x]P))) 454Proof SRW_TAC [][SUB_DEF] 455QED 456val lSUB_VAR = store_thm( 457 "lSUB_VAR", 458 ���[N/x] (VAR s : lterm) = if s = x then N else VAR s���, 459 SRW_TAC [][SUB_DEF]); 460 461val l15a = store_thm( 462 "l15a", 463 ���!t:lterm. ~(v IN FV t) ==> ([u/v] ([VAR v/x] t) = [u/x] t)���, 464 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC ���{x;v} UNION FV u��� THEN 465 SRW_TAC [][lSUB_VAR]); 466 467val ltm_recursion_nosideset = save_thm( 468 "ltm_recursion_nosideset", 469 tm_recursion |> Q.INST [���A��� |-> ���{}���] |> REWRITE_RULE [NOT_IN_EMPTY, FINITE_EMPTY]) 470 471val term_info_string = 472 "local\n\ 473 \fun k |-> v = {redex = k, residue = v}\n\ 474 \val term_info = \n\ 475 \ {nullfv = ``labelledTerms$LAM \"\" (VAR \"\")``,\n\ 476 \ pm_rewrites = [],\n\ 477 \ pm_constant = ``nomset$mk_pmact labelledTerms$raw_ltpm``,\n\ 478 \ fv_rewrites = [],\n\ 479 \ recursion_thm = SOME ltm_recursion_nosideset,\n\ 480 \ binders = [(``labelledTerms$LAM``, 0, ltpm_ALPHA),\n\ 481 \ (``labelledTerms$LAMi``, 1, ltpm_ALPHAi)]}\n\ 482 \val _ = binderLib.type_db :=\n\ 483 \ Binarymap.insert(!binderLib.type_db, \n\ 484 \ {Thy = \"labelledTerms\", Name=\"lterm\"},\n\ 485 \ binderLib.NTI term_info)\n\ 486 \in end;\n" 487 488val _ = adjoin_after_completion (fn _ => PP.add_string term_info_string) 489 490val _ = export_theory() 491