172 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
172 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
173 lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted] |
173 lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted] |
174 lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] |
174 lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] |
175 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
175 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
176 |
176 |
177 lemma lets_bla: |
|
178 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" |
|
179 apply (simp only: alpha5_INJ) |
|
180 apply (simp only: bv5) |
|
181 apply simp |
|
182 done |
|
183 |
|
184 lemma lets_ok: |
|
185 "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
|
186 apply (simp add: alpha5_INJ) |
|
187 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
188 apply (simp_all add: alpha_gen) |
|
189 apply (simp add: permute_trm5_lts fresh_star_def eqvts) |
|
190 done |
|
191 |
|
192 lemma lets_ok3: |
|
193 "x \<noteq> y \<Longrightarrow> |
|
194 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
195 (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
196 apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) |
|
197 done |
|
198 |
|
199 |
|
200 lemma lets_not_ok1: |
|
201 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
|
202 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
203 apply (simp add: alpha5_INJ alpha_gen) |
|
204 apply (rule_tac x="0::perm" in exI) |
|
205 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) |
|
206 apply blast |
|
207 done |
|
208 |
|
209 lemma distinct_helper: |
|
210 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
|
211 apply auto |
|
212 apply (erule alpha_rtrm5.cases) |
|
213 apply (simp_all only: rtrm5.distinct) |
|
214 done |
|
215 |
|
216 lemma distinct_helper2: |
|
217 shows "(Vr5 x) \<noteq> (Ap5 y z)" |
|
218 by (lifting distinct_helper) |
|
219 |
|
220 lemma lets_nok: |
|
221 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
222 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
223 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
224 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) |
|
225 apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts) |
|
226 done |
|
227 |
|
228 end |
177 end |