equal
deleted
inserted
replaced
41 lemma bi_eqvt: |
41 lemma bi_eqvt: |
42 shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)" |
42 shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)" |
43 by (rule eqvts) |
43 by (rule eqvts) |
44 |
44 |
45 lemma supp_fv: |
45 lemma supp_fv: |
46 "supp t = fv_lam t" and |
46 shows "supp t = fv_lam t" |
47 "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}" |
47 and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}" |
48 apply(induct t and bp rule: lam_bp_inducts) |
48 apply(induct t and bp rule: lam_bp_inducts) |
49 apply(simp_all add: lam_bp_fv) |
49 apply(simp_all add: lam_bp_fv) |
50 (* VAR case *) |
50 (* VAR case *) |
51 apply(simp only: supp_def) |
51 apply(simp only: supp_def) |
52 apply(simp only: lam_bp_perm) |
52 apply(simp only: lam_bp_perm) |
105 apply(blast) |
105 apply(blast) |
106 apply(simp add: supp_Abs) |
106 apply(simp add: supp_Abs) |
107 apply(blast) |
107 apply(blast) |
108 done |
108 done |
109 |
109 |
|
110 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
|
111 |
110 text {* example 2 *} |
112 text {* example 2 *} |
111 |
113 |
112 nominal_datatype trm' = |
114 nominal_datatype trm' = |
113 Var "name" |
115 Var "name" |
114 | App "trm'" "trm'" |
116 | App "trm'" "trm'" |