equal
deleted
inserted
replaced
171 apply (simp only: alpha_gen) |
171 apply (simp only: alpha_gen) |
172 apply (simp add: permute_trm5_lts fresh_star_def) |
172 apply (simp add: permute_trm5_lts fresh_star_def) |
173 done |
173 done |
174 |
174 |
175 lemma lets_ok3: |
175 lemma lets_ok3: |
176 "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
176 assumes a: "distinct [x, y]" |
177 (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
177 shows "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
|
178 (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
178 apply (subst alpha5_INJ) |
179 apply (subst alpha5_INJ) |
179 apply (rule conjI) |
180 apply (rule conjI) |
|
181 apply (simp add: alpha_gen) |
|
182 apply (simp add: permute_trm5_lts fresh_star_def) |
180 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
183 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
181 apply (simp only: alpha_gen) |
184 apply (simp only: alpha_gen) |
182 apply (simp add: permute_trm5_lts fresh_star_def) |
185 apply (simp add: permute_trm5_lts fresh_star_def) |
183 apply (rule_tac x="0 :: perm" in exI) |
186 apply (rule_tac x="0 :: perm" in exI) |
184 apply (simp only: alpha_gen) |
187 apply (simp only: alpha_gen) |