--- a/Nominal/Ex/Let.thy	Tue Jan 18 11:02:57 2011 +0100
+++ b/Nominal/Ex/Let.thy	Tue Jan 18 21:12:25 2011 +0900
@@ -30,40 +30,54 @@
 thm trm_assn.exhaust
 thm trm_assn.strong_exhaust
 
-(*
+
 lemma lets_bla:
-  "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))"
-  by (simp add: trm_lts.eq_iff)
+  "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))"
+  by (simp add: trm_assn.eq_iff)
+
 
 lemma lets_ok:
-  "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
-  apply (simp add: trm_lts.eq_iff)
+  "(Let (ACons x (Var y) ANil) (Var x)) = (Let (ACons y (Var y) ANil) (Var y))"
+  apply (simp add: trm_assn.eq_iff Abs_eq_iff )
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alphas eqvts supp_at_base fresh_star_def)
+  apply (simp_all add: alphas atom_eqvt supp_at_base fresh_star_def trm_assn.bn_defs trm_assn.supp)
   done
 
 lemma lets_ok3:
   "x \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff)
+   (Let (ACons x (App (Var y) (Var x)) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq>
+   (Let (ACons y (App (Var x) (Var y)) (ACons x (Var x) ANil)) (App (Var x) (Var y)))"
+  apply (simp add: trm_assn.eq_iff)
   done
 
 
 lemma lets_not_ok1:
   "x \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
+   (Let (ACons x (Var x) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq>
+   (Let (ACons y (Var x) (ACons x (Var y) ANil)) (App (Var x) (Var y)))"
+  apply (simp add: alphas trm_assn.eq_iff trm_assn.supp fresh_star_def atom_eqvt Abs_eq_iff trm_assn.bn_defs)
   done
 
 lemma lets_nok:
   "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
+   (Let (ACons x (App (Var z) (Var z)) (ACons y (Var z) ANil)) (App (Var x) (Var y))) \<noteq>
+   (Let (ACons y (Var z) (ACons x (App (Var z) (Var z)) ANil)) (App (Var x) (Var y)))"
+  apply (simp add: alphas trm_assn.eq_iff fresh_star_def trm_assn.bn_defs Abs_eq_iff trm_assn.supp trm_assn.distinct)
   done
-*)
+
+lemma
+  fixes a b c :: name
+  assumes x: "a \<noteq> c" and y: "b \<noteq> c"
+  shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)"
+  apply (rule_tac x="(a \<leftrightarrow> b)" in exI)
+  apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt)
+  by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y)
+
+lemma
+  assumes "atom a \<noteq> atom c \<and> atom b \<noteq> atom c"
+  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})"
+  apply (simp add: alphas trm_assn.supp supp_at_base assms trm_assn.eq_iff atom_eqvt fresh_star_def)
+  oops
 
 end