287 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
287 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
288 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
288 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
289 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] |
289 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] |
290 lemmas alpha5_DIS = alpha_dis[quot_lifted] |
290 lemmas alpha5_DIS = alpha_dis[quot_lifted] |
291 |
291 |
292 (* why is this not in Isabelle? *) |
|
293 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
|
294 by auto |
|
295 |
|
296 lemma lets_bla: |
|
297 "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))" |
|
298 apply (simp only: alpha5_INJ bv5) |
|
299 apply simp |
|
300 apply (rule allI) |
|
301 apply (simp_all add: alpha_gen) |
|
302 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) |
|
303 apply (rule impI) |
|
304 apply (rule impI) |
|
305 apply (rule impI) |
|
306 apply (simp add: set_sub) |
|
307 done |
|
308 |
|
309 lemma lets_ok: |
|
310 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
|
311 thm alpha5_INJ |
|
312 apply (simp only: alpha5_INJ) |
|
313 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
314 apply (simp_all add: alpha_gen) |
|
315 apply (simp add: permute_trm5_lts fresh_star_def) |
|
316 apply (simp add: eqvts) |
|
317 done |
|
318 |
|
319 lemma lets_ok3: |
|
320 "x \<noteq> y \<Longrightarrow> |
|
321 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
322 (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
323 apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) |
|
324 done |
|
325 |
|
326 |
|
327 lemma lets_not_ok1: |
|
328 "x \<noteq> y \<Longrightarrow> |
|
329 (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
330 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
331 apply (simp add: alpha5_INJ alpha_gen) |
|
332 apply (simp add: permute_trm5_lts eqvts) |
|
333 apply (simp add: alpha5_INJ) |
|
334 done |
|
335 |
|
336 lemma lets_nok: |
|
337 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
338 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
339 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
340 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) |
|
341 apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts) |
|
342 done |
|
343 |
|
344 end |
292 end |