--- a/Nominal/Abs.thy	Tue Apr 20 11:29:00 2010 +0200
+++ b/Nominal/Abs.thy	Tue Apr 20 18:24:50 2010 +0200
@@ -423,15 +423,50 @@
 apply(simp)
 done
 
-
+lemma 
+  fixes t1 s1::"'a::fs"
+  and   t2 s2::"'b::fs"
+  shows "Abs as (t1, t2) = Abs bs (s1, s2) \<longrightarrow> (Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2)"
+apply(subst abs_eq_iff)
+apply(subst alphas_abs)
+apply(subst alphas)
+apply(rule impI)
+apply(erule exE)
+apply(simp add: supp_Pair)
+apply(simp add: Un_Diff)
+apply(simp add: fresh_star_union)
+apply(erule conjE)+
+apply(rule conjI)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+apply(simp add: supp_abs)
+apply(simp)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+apply(simp add: supp_abs)
+apply(simp)
+done
 
-(* support of concrete atom sets *)
+lemma fresh_star_eq:
+  assumes a: "as \<sharp>* p"
+  shows "\<forall>a \<in> as. p \<bullet> a = a"
+using a by (simp add: fresh_star_def fresh_def supp_perm)
+
+lemma fresh_star_set_eq:
+  assumes a: "as \<sharp>* p"
+  shows "p \<bullet> as = as"
+using a 
+apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq)
+apply(auto)
+by (metis permute_atom_def)
 
 lemma 
   fixes t1 s1::"'a::fs"
   and   t2 s2::"'b::fs"
   assumes asm: "finite as"
-  shows "(Abs as t1 = Abs as s1 \<and>  Abs as t2 = Abs as s2) \<longrightarrow> Abs as (t1, t2) = Abs as (s1, s2)"
+  shows "(Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (s1, s2)"
 apply(subst abs_eq_iff)
 apply(subst abs_eq_iff)
 apply(subst alphas_abs)

--- a/Nominal/Ex/Ex1.thy	Tue Apr 20 11:29:00 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-theory Ex1
-imports "../Parser"
-begin
-
-text {* example 1, equivalent to example 2 from Terms *}
-
-atom_decl name
-
-ML {* val _ = recursive := false *}
-nominal_datatype lam =
-  VAR "name"
-| APP "lam" "lam"
-| LAM x::"name" t::"lam" bind x in t
-| LET bp::"bp" t::"lam"   bind "bi bp" in t
-and bp =
-  BP "name" "lam"
-binder
-  bi::"bp \<Rightarrow> atom set"
-where
-  "bi (BP x t) = {atom x}"
-
-thm lam_bp.fv
-thm lam_bp.supp
-thm lam_bp.eq_iff
-thm lam_bp.bn
-thm lam_bp.perm
-thm lam_bp.induct
-thm lam_bp.inducts
-thm lam_bp.distinct
-ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
-thm lam_bp.fv[simplified lam_bp.supp]
-
-end
-
-
-

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/SingleLet.thy	Tue Apr 20 18:24:50 2010 +0200
@@ -0,0 +1,38 @@
+theory SingleLet
+imports "../Parser"
+begin
+
+atom_decl name
+
+ML {* val _ = recursive := false *}
+
+nominal_datatype trm =
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"  bind x in t
+| Let a::"assg" t::"trm"  bind "bn a" in t
+and assg =
+  As "name" "trm"
+binder
+  bn::"assg \<Rightarrow> atom set"
+where
+  "bn (As x t) = {atom x}"
+
+print_theorems
+thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
+
+thm trm_assg.fv
+thm trm_assg.supp
+thm trm_assg.eq_iff[simplified alphas_abs[symmetric]]
+thm trm_assg.bn
+thm trm_assg.perm
+thm trm_assg.induct
+thm trm_assg.inducts
+thm trm_assg.distinct
+ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
+thm trm_assg.fv[simplified trm_assg.supp]
+
+end
+
+
+

--- a/Nominal/Fv.thy	Tue Apr 20 11:29:00 2010 +0200
+++ b/Nominal/Fv.thy	Tue Apr 20 18:24:50 2010 +0200
@@ -137,7 +137,7 @@
 *)
 
 ML {*
-datatype alpha_type = AlphaGen | AlphaRes | AlphaLst;
+datatype alpha_mode = AlphaGen | AlphaRes | AlphaLst;
 *}
 
 ML {*

--- a/Nominal/Parser.thy	Tue Apr 20 11:29:00 2010 +0200
+++ b/Nominal/Parser.thy	Tue Apr 20 18:24:50 2010 +0200
@@ -296,14 +296,19 @@
 
 Parser.thy/raw_nominal_decls
   1) define the raw datatype
-  2) define the raw binding functions
+  2) define the raw binding functions 
+
 Perm.thy/define_raw_perms
-  3) define permutations of the raw datatype and show that raw type is in the pt typeclass
+  3) define permutations of the raw datatype and show that the raw type is 
+     in the pt typeclass
+      
 Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha
   4) define fv and fv_bn
   5) define alpha and alpha_bn
+
 Perm.thy/distinct_rel
   6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)
+
 Tacs.thy/build_rel_inj
   6) prove alpha_eq_iff    (C1 x = C2 y \<leftrightarrow> P x y ...)
      (left-to-right by intro rule, right-to-left by cases; simp)

--- a/Nominal/ROOT.ML	Tue Apr 20 11:29:00 2010 +0200
+++ b/Nominal/ROOT.ML	Tue Apr 20 18:24:50 2010 +0200
@@ -3,7 +3,7 @@
 no_document use_thys
    ["Ex/Lambda",
     "Ex/ExLF",
-    "Ex/Ex1",
+    "Ex/SingleLet",
     "Ex/Ex1rec",
     "Ex/Ex2",
     "Ex/Ex3",