28 thm trm_assn.supp |
28 thm trm_assn.supp |
29 thm trm_assn.fresh |
29 thm trm_assn.fresh |
30 thm trm_assn.exhaust |
30 thm trm_assn.exhaust |
31 thm trm_assn.strong_exhaust |
31 thm trm_assn.strong_exhaust |
32 |
32 |
33 (* |
33 |
34 lemma lets_bla: |
34 lemma lets_bla: |
35 "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))" |
35 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Let (ACons x (Var y) ANil) (Var x)) \<noteq> (Let (ACons x (Var z) ANil) (Var x))" |
36 by (simp add: trm_lts.eq_iff) |
36 by (simp add: trm_assn.eq_iff) |
|
37 |
37 |
38 |
38 lemma lets_ok: |
39 lemma lets_ok: |
39 "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
40 "(Let (ACons x (Var y) ANil) (Var x)) = (Let (ACons y (Var y) ANil) (Var y))" |
40 apply (simp add: trm_lts.eq_iff) |
41 apply (simp add: trm_assn.eq_iff Abs_eq_iff ) |
41 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
42 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
42 apply (simp_all add: alphas eqvts supp_at_base fresh_star_def) |
43 apply (simp_all add: alphas atom_eqvt supp_at_base fresh_star_def trm_assn.bn_defs trm_assn.supp) |
43 done |
44 done |
44 |
45 |
45 lemma lets_ok3: |
46 lemma lets_ok3: |
46 "x \<noteq> y \<Longrightarrow> |
47 "x \<noteq> y \<Longrightarrow> |
47 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
48 (Let (ACons x (App (Var y) (Var x)) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq> |
48 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))" |
49 (Let (ACons y (App (Var x) (Var y)) (ACons x (Var x) ANil)) (App (Var x) (Var y)))" |
49 apply (simp add: alphas trm_lts.eq_iff) |
50 apply (simp add: trm_assn.eq_iff) |
50 done |
51 done |
51 |
52 |
52 |
53 |
53 lemma lets_not_ok1: |
54 lemma lets_not_ok1: |
54 "x \<noteq> y \<Longrightarrow> |
55 "x \<noteq> y \<Longrightarrow> |
55 (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
56 (Let (ACons x (Var x) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq> |
56 (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" |
57 (Let (ACons y (Var x) (ACons x (Var y) ANil)) (App (Var x) (Var y)))" |
57 apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts) |
58 apply (simp add: alphas trm_assn.eq_iff trm_assn.supp fresh_star_def atom_eqvt Abs_eq_iff trm_assn.bn_defs) |
58 done |
59 done |
59 |
60 |
60 lemma lets_nok: |
61 lemma lets_nok: |
61 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
62 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
62 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
63 (Let (ACons x (App (Var z) (Var z)) (ACons y (Var z) ANil)) (App (Var x) (Var y))) \<noteq> |
63 (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" |
64 (Let (ACons y (Var z) (ACons x (App (Var z) (Var z)) ANil)) (App (Var x) (Var y)))" |
64 apply (simp add: alphas trm_lts.eq_iff fresh_star_def) |
65 apply (simp add: alphas trm_assn.eq_iff fresh_star_def trm_assn.bn_defs Abs_eq_iff trm_assn.supp trm_assn.distinct) |
65 done |
66 done |
66 *) |
67 |
|
68 lemma |
|
69 fixes a b c :: name |
|
70 assumes x: "a \<noteq> c" and y: "b \<noteq> c" |
|
71 shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)" |
|
72 apply (rule_tac x="(a \<leftrightarrow> b)" in exI) |
|
73 apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt) |
|
74 by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y) |
|
75 |
|
76 lemma |
|
77 assumes "atom a \<noteq> atom c \<and> atom b \<noteq> atom c" |
|
78 shows "\<exists>p. ([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c) \<and> supp p \<subseteq> (supp (Var c) \<inter> {atom a}) \<union> (supp (Var c) \<inter> {atom b})" |
|
79 apply (simp add: alphas trm_assn.supp supp_at_base assms trm_assn.eq_iff atom_eqvt fresh_star_def) |
|
80 oops |
67 |
81 |
68 end |
82 end |
69 |
83 |
70 |
84 |
71 |
85 |