equal
deleted
inserted
replaced
90 apply(induct l rule: trm_lts.inducts(2)) |
90 apply(induct l rule: trm_lts.inducts(2)) |
91 apply(rule TrueI) |
91 apply(rule TrueI) |
92 apply(simp_all add:permute_bn eqvts) |
92 apply(simp_all add:permute_bn eqvts) |
93 done |
93 done |
94 |
94 |
|
95 lemma fv_fv_bn: |
|
96 "fv_bn l - set (bn l) = fv_lts l - set (bn l)" |
|
97 apply(induct l rule: trm_lts.inducts(2)) |
|
98 apply(rule TrueI) |
|
99 apply(simp_all add:permute_bn eqvts) |
|
100 by blast |
|
101 |
95 lemma Lt_subst: |
102 lemma Lt_subst: |
96 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
103 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
97 apply (simp only: trm_lts.eq_iff) |
104 apply (simp only: trm_lts.eq_iff) |
98 apply (rule_tac x="q" in exI) |
105 apply (rule_tac x="q" in exI) |
99 apply (simp add: alphas) |
106 apply (simp add: alphas) |