equal
deleted
inserted
replaced
33 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
33 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
34 by auto |
34 by auto |
35 |
35 |
36 lemma lets_bla: |
36 lemma lets_bla: |
37 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))" |
37 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))" |
38 apply (simp add: trm_lts.eq_iff alpha_gen2 set_sub) |
38 by (simp add: trm_lts.eq_iff alphas2 set_sub) |
39 done |
|
40 |
39 |
41 lemma lets_ok: |
40 lemma lets_ok: |
42 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
41 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
43 apply (simp add: trm_lts.eq_iff) |
42 apply (simp add: trm_lts.eq_iff) |
44 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
43 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
45 apply (simp_all add: alpha_gen2 fresh_star_def eqvts) |
44 apply (simp_all add: alphas2 fresh_star_def eqvts) |
46 done |
45 done |
47 |
46 |
48 lemma lets_ok3: |
47 lemma lets_ok3: |
49 "x \<noteq> y \<Longrightarrow> |
48 "x \<noteq> y \<Longrightarrow> |
50 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
49 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |