equal
deleted
inserted
replaced
170 apply (rule_tac x="0 :: perm" in exI) |
170 apply (rule_tac x="0 :: perm" in exI) |
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: |
|
176 "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
|
177 (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 (rule conjI) |
|
180 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
181 apply (simp only: alpha_gen) |
|
182 apply (simp add: permute_trm5_lts fresh_star_def) |
|
183 apply (rule_tac x="0 :: perm" in exI) |
|
184 apply (simp only: alpha_gen) |
|
185 apply (simp add: permute_trm5_lts fresh_star_def) |
|
186 done |
175 |
187 |
176 lemma lets_not_ok1: |
188 lemma lets_not_ok1: |
177 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
189 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
178 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
190 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
179 apply (simp add: alpha5_INJ(3) alpha_gen) |
191 apply (simp add: alpha5_INJ(3) alpha_gen) |