--- a/Nominal/ExLet.thy	Sat Mar 27 16:17:45 2010 +0100
+++ b/Nominal/ExLet.thy	Sat Mar 27 16:20:39 2010 +0100
@@ -7,7 +7,7 @@
 atom_decl name
 
 ML {* val _ = recursive := false  *}
-
+ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -19,8 +19,8 @@
 binder
   bn
 where
-  "bn Lnil = {}"
-| "bn (Lcons x t l) = {atom x} \<union> (bn l)"
+  "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
 
 thm trm_lts.fv
 thm trm_lts.eq_iff
@@ -29,7 +29,7 @@
 thm trm_lts.induct[no_vars]
 thm trm_lts.inducts[no_vars]
 thm trm_lts.distinct
-thm trm_lts.fv[simplified trm_lts.supp]
+thm trm_lts.fv[simplified trm_lts.supp(1-2)]
 
 primrec
   permute_bn_raw
@@ -80,7 +80,7 @@
   done
 
 lemma Lt_subst:
-  "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
+  "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
   apply (simp only: trm_lts.eq_iff)
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
@@ -98,7 +98,7 @@
 
 
 lemma fin_bn:
-  "finite (bn l)"
+  "finite (set (bn l))"
   apply(induct l rule: trm_lts.inducts(2))
   apply(simp_all add:permute_bn eqvts)
   done
@@ -110,7 +110,7 @@
   assumes a1: "\<And>name c. P1 c (Vr name)"
   and     a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
   and     a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
-  and     a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
+  and     a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
   and     a5: "\<And>c. P2 c Lnil"
   and     a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
   shows "P1 c t" and "P2 c l"
@@ -142,14 +142,14 @@
     apply(simp add: fresh_def)
     apply(simp add: trm_lts.fv[simplified trm_lts.supp])
     apply(simp)
-    apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
+    apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
     apply(erule exE)
     apply(erule conjE)
     apply(subst Lt_subst)
     apply assumption
     apply(rule a4)
-    apply(simp add:perm_bn)
-    apply assumption
+    apply(simp add:perm_bn[symmetric])
+    apply(simp add: eqvts)
     apply (simp add: fresh_star_def fresh_def)
     apply(rotate_tac 1)
     apply(drule_tac x="q + p" in meta_spec)
@@ -157,8 +157,6 @@
     apply(rule at_set_avoiding2)
     apply(rule fin_bn)
     apply(simp add: finite_supp)
-    apply(simp add: supp_abs)
-    apply(rule finite_Diff)
     apply(simp add: finite_supp)
     apply(simp add: fresh_star_def fresh_def supp_abs)
     apply(simp add: eqvts permute_bn)
@@ -196,12 +194,10 @@
 
 
 lemma lets_not_ok1:
-  "(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
+  "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)
-  apply (rule_tac x="0::perm" in exI)
-  apply (simp add: fresh_star_def eqvts)
-  apply blast
+  apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
   done
 
 lemma lets_nok:

--- a/Nominal/ExLetRec.thy	Sat Mar 27 16:17:45 2010 +0100
+++ b/Nominal/ExLetRec.thy	Sat Mar 27 16:20:39 2010 +0100
@@ -2,11 +2,13 @@
 imports "Parser"
 begin
 
+
 text {* example 3 or example 5 from Terms.thy *}
 
 atom_decl name
 
 ML {* val _ = recursive := true *}
+ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -18,8 +20,8 @@
 binder
   bn
 where
-  "bn Lnil = {}"
-| "bn (Lcons x t l) = {atom x} \<union> (bn l)"
+  "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
 
 thm trm_lts.fv
 thm trm_lts.eq_iff
@@ -27,6 +29,7 @@
 thm trm_lts.perm
 thm trm_lts.induct
 thm trm_lts.distinct
+thm trm_lts.supp
 thm trm_lts.fv[simplified trm_lts.supp]
 
 (* why is this not in HOL simpset? *)
@@ -66,6 +69,13 @@
   apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
   done
 
+lemma lets_ok4:
+  "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
+   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
+  apply (simp add: alphas trm_lts.eq_iff)
+  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+  apply (simp add: atom_eqvt fresh_star_def)
+  done
 
 end
 

--- a/Nominal/Fv.thy	Sat Mar 27 16:17:45 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 16:20:39 2010 +0100
@@ -891,13 +891,9 @@
 end
 *}
 
-lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
-  apply (simp add: supp_abs supp_Pair)
-  apply blast
-  done
-
 (* TODO: this is a hack, it assumes that only one type of Abs's is present
-   in the type and chooses this supp_abs *)
+   in the type and chooses this supp_abs. Additionally single atoms are
+   treated properly. *)
 ML {*
 fun choose_alpha_abs eqiff =
 let
@@ -905,19 +901,31 @@
   val terms = map prop_of eqiff;
   fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
   val no =
-    if check @{const_name alpha_gen} then 0 else
+    if check @{const_name alpha_lst} then 2 else
     if check @{const_name alpha_res} then 1 else
-    if check @{const_name alpha_lst} then 2 else
+    if check @{const_name alpha_gen} then 0 else
     error "Failure choosing supp_abs"
 in
   nth @{thms supp_abs[symmetric]} no
 end
 *}
+lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}"
+by (rule supp_abs(1))
+
+lemma supp_abs_sum:
+  "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
+  "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
+  "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))"
+  apply (simp_all add: supp_abs supp_Pair)
+  apply blast+
+  done
+
 
 ML {*
 fun supp_eq_tac ind fv perm eqiff ctxt =
   rel_indtac ind THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW

--- a/Nominal/Lift.thy	Sat Mar 27 16:17:45 2010 +0100
+++ b/Nominal/Lift.thy	Sat Mar 27 16:20:39 2010 +0100
@@ -64,19 +64,6 @@
 *}
 
 ML {*
-fun quotient_lift_consts_export qtys spec ctxt =
-let
-  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
-  val (ts_loc, defs_loc) = split_list result;
-  val morphism = ProofContext.export_morphism ctxt' ctxt;
-  val ts = map (Morphism.term morphism) ts_loc
-  val defs = Morphism.fact morphism defs_loc
-in
-  (ts, defs, ctxt')
-end
-*}
-
-ML {*
 fun define_fv_alpha_export dt binds bns ctxt =
 let
   val ((((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), alpha), ctxt') =

--- a/Nominal/Parser.thy	Sat Mar 27 16:17:45 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 27 16:20:39 2010 +0100
@@ -594,7 +594,7 @@
   end
 
 in
-  map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type)))))
+  map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type)))))
   (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
 end
 *}