21 | Lm x::"name" l::"lm" bind x in l |
21 | Lm x::"name" l::"lm" bind x in l |
22 |
22 |
23 lemma finite_fv: |
23 lemma finite_fv: |
24 shows "finite (fv_lm t)" |
24 shows "finite (fv_lm t)" |
25 apply(induct t rule: lm_induct) |
25 apply(induct t rule: lm_induct) |
26 apply(simp_all add: lm_fv) |
26 apply(simp_all) |
27 done |
27 done |
28 |
28 |
29 lemma supp_fn: |
29 lemma supp_fn: |
30 shows "supp t = fv_lm t" |
30 shows "supp t = fv_lm t" |
31 apply(induct t rule: lm_induct) |
31 apply(induct t rule: lm_induct) |
32 apply(simp_all add: lm_fv) |
32 apply(simp_all) |
33 apply(simp only: supp_def) |
33 apply(simp only: supp_def) |
34 apply(simp only: lm_perm) |
34 apply(simp only: lm_perm) |
35 apply(simp only: lm_eq_iff) |
35 apply(simp only: lm_eq_iff) |
36 apply(simp only: supp_def[symmetric]) |
36 apply(simp only: supp_def[symmetric]) |
37 apply(simp only: supp_at_base) |
37 apply(simp only: supp_at_base) |
75 apply(assumption) |
75 apply(assumption) |
76 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))") |
76 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))") |
77 apply(erule exE) |
77 apply(erule exE) |
78 apply(rule_tac t="p \<bullet> Lm name lm" and |
78 apply(rule_tac t="p \<bullet> Lm name lm" and |
79 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst) |
79 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst) |
80 apply(simp) |
80 apply(simp del: lm_perm) |
81 apply(subst lm_perm) |
81 apply(subst lm_perm) |
82 apply(subst (2) lm_perm) |
82 apply(subst (2) lm_perm) |
83 apply(rule flip_fresh_fresh) |
83 apply(rule flip_fresh_fresh) |
84 apply(simp add: fresh_def) |
84 apply(simp add: fresh_def) |
85 apply(simp only: supp_fn') |
85 apply(simp only: supp_fn') |
86 apply(simp) |
86 apply(simp) |
87 apply(simp add: fresh_Pair) |
87 apply(simp add: fresh_Pair) |
88 apply(simp add: lm_perm) |
88 apply(simp) |
89 apply(rule a3) |
89 apply(rule a3) |
90 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
90 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
91 apply(simp) |
91 apply(simp) |
92 apply(simp add: fresh_def) |
92 apply(simp add: fresh_def) |
93 apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) |
93 apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) |
128 |
128 |
129 lemma supp_fv: |
129 lemma supp_fv: |
130 shows "supp t = fv_lam t" |
130 shows "supp t = fv_lam t" |
131 and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}" |
131 and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}" |
132 apply(induct t and bp rule: lam_bp_inducts) |
132 apply(induct t and bp rule: lam_bp_inducts) |
133 apply(simp_all add: lam_bp_fv) |
133 apply(simp_all) |
134 (* VAR case *) |
134 (* VAR case *) |
135 apply(simp only: supp_def) |
135 apply(simp only: supp_def) |
136 apply(simp only: lam_bp_perm) |
136 apply(simp only: lam_bp_perm) |
137 apply(simp only: lam_bp_eq_iff) |
137 apply(simp only: lam_bp_eq_iff) |
138 apply(simp only: supp_def[symmetric]) |
138 apply(simp only: supp_def[symmetric]) |
216 |
216 |
217 lemma supp_fv': |
217 lemma supp_fv': |
218 shows "supp t = fv_lam' t" |
218 shows "supp t = fv_lam' t" |
219 and "supp bp = fv_bp' bp" |
219 and "supp bp = fv_bp' bp" |
220 apply(induct t and bp rule: lam'_bp'_inducts) |
220 apply(induct t and bp rule: lam'_bp'_inducts) |
221 apply(simp_all add: lam'_bp'_fv) |
221 apply(simp_all) |
222 (* VAR case *) |
222 (* VAR case *) |
223 apply(simp only: supp_def) |
223 apply(simp only: supp_def) |
224 apply(simp only: lam'_bp'_perm) |
224 apply(simp only: lam'_bp'_perm) |
225 apply(simp only: lam'_bp'_eq_iff) |
225 apply(simp only: lam'_bp'_eq_iff) |
226 apply(simp only: supp_def[symmetric]) |
226 apply(simp only: supp_def[symmetric]) |
302 |
302 |
303 lemma supp_fv_trm'_pat': |
303 lemma supp_fv_trm'_pat': |
304 shows "supp t = fv_trm' t" |
304 shows "supp t = fv_trm' t" |
305 and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp" |
305 and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp" |
306 apply(induct t and bp rule: trm'_pat'_inducts) |
306 apply(induct t and bp rule: trm'_pat'_inducts) |
307 apply(simp_all add: trm'_pat'_fv) |
307 apply(simp_all) |
308 (* VAR case *) |
308 (* VAR case *) |
309 apply(simp only: supp_def) |
309 apply(simp only: supp_def) |
310 apply(simp only: trm'_pat'_perm) |
310 apply(simp only: trm'_pat'_perm) |
311 apply(simp only: trm'_pat'_eq_iff) |
311 apply(simp only: trm'_pat'_eq_iff) |
312 apply(simp only: supp_def[symmetric]) |
312 apply(simp only: supp_def[symmetric]) |
437 |
437 |
438 lemma supp_fv_t_tyS: |
438 lemma supp_fv_t_tyS: |
439 shows "supp T = fv_t T" |
439 shows "supp T = fv_t T" |
440 and "supp S = fv_tyS S" |
440 and "supp S = fv_tyS S" |
441 apply(induct T and S rule: t_tyS_inducts) |
441 apply(induct T and S rule: t_tyS_inducts) |
442 apply(simp_all add: t_tyS_fv) |
442 apply(simp_all) |
443 (* VarTS case *) |
443 (* VarTS case *) |
444 apply(simp only: supp_def) |
444 apply(simp only: supp_def) |
445 apply(simp only: t_tyS_perm) |
445 apply(simp only: t_tyS_perm) |
446 apply(simp only: t_tyS_eq_iff) |
446 apply(simp only: t_tyS_eq_iff) |
447 apply(simp only: supp_def[symmetric]) |
447 apply(simp only: supp_def[symmetric]) |
516 thm trm3_rassigns3_eq_iff |
516 thm trm3_rassigns3_eq_iff |
517 thm trm3_rassigns3_bn |
517 thm trm3_rassigns3_bn |
518 thm trm3_rassigns3_perm |
518 thm trm3_rassigns3_perm |
519 thm trm3_rassigns3_induct |
519 thm trm3_rassigns3_induct |
520 thm trm3_rassigns3_distinct |
520 thm trm3_rassigns3_distinct |
521 |
|
522 (* compat should be |
|
523 compat (ANil) pi (PNil) \<equiv> TRue |
|
524 compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts' |
|
525 *) |
|
526 |
521 |
527 (* example 5 from Terms.thy *) |
522 (* example 5 from Terms.thy *) |
528 |
523 |
529 nominal_datatype trm5 = |
524 nominal_datatype trm5 = |
530 Vr5 "name" |
525 Vr5 "name" |