equal
deleted
inserted
replaced
41 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
41 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
42 by auto |
42 by auto |
43 |
43 |
44 lemma lets_bla: |
44 lemma lets_bla: |
45 "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))" |
45 "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))" |
46 by (simp add: trm_lts.eq_iff alphas2 set_sub supp_at_base) |
46 apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base) |
|
47 done |
47 |
48 |
48 lemma lets_ok: |
49 lemma lets_ok: |
49 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
50 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
50 apply (simp add: trm_lts.eq_iff) |
51 apply (simp add: trm_lts.eq_iff) |
51 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
52 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
52 apply (simp_all add: alphas2 fresh_star_def eqvts supp_at_base) |
53 apply (simp_all add: alphas fresh_star_def eqvts supp_at_base) |
53 done |
54 done |
54 |
55 |
55 lemma lets_ok3: |
56 lemma lets_ok3: |
56 "x \<noteq> y \<Longrightarrow> |
57 "x \<noteq> y \<Longrightarrow> |
57 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
58 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |