--- a/Nominal/ExLet.thy	Tue Mar 23 09:06:28 2010 +0100
+++ b/Nominal/ExLet.thy	Tue Mar 23 09:13:17 2010 +0100
@@ -11,15 +11,15 @@
   Vr "name"
 | Ap "trm" "trm"
 | Lm x::"name" t::"trm"  bind x in t
-| Lt a::"lts" t::"trm"   bind "bv a" in t
+| Lt a::"lts" t::"trm"   bind "bn a" in t
 and lts =
-  Nil
-| Cons "name" "trm" "lts"
+  Lnil
+| Lcons "name" "trm" "lts"
 binder
   bn
 where
-  "bn Nil = {}"
-| "bn (Cons x t l) = {atom x} \<union> (bn l)"
+  "bn Lnil = {}"
+| "bn (Lcons x t l) = {atom x} \<union> (bn l)"
 
 thm trm_lts.fv
 thm trm_lts.eq_iff
@@ -29,6 +29,43 @@
 thm trm_lts.distinct
 thm trm_lts.fv[simplified trm_lts.supp]
 
+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)
+
+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)
+  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+  apply (simp_all add: alphas)
+  apply (simp add: fresh_star_def eqvts)
+  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)
+  done
+
+
+lemma lets_not_ok1:
+  "(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
+   (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
+  apply (simp add: alphas trm_lts.eq_iff)
+  apply (rule_tac x="0::perm" in exI)
+  apply (simp add: fresh_star_def eqvts)
+  apply blast
+  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)
+  done
+
+
 end