--- a/Nominal/Abs.thy	Thu Apr 01 08:06:01 2010 +0200
+++ b/Nominal/Abs.thy	Thu Apr 01 08:48:33 2010 +0200
@@ -444,6 +444,12 @@
   \<and> pi \<bullet> bsl = csl)"
 by (simp_all add: alphas)
 
+lemma alphas3:
+  "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and>
+     (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and>
+     R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
+by (simp add: alphas)
+
 lemma alpha_gen_compose_sym:
   fixes pi
   assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExLetMult.thy	Thu Apr 01 08:48:33 2010 +0200
@@ -0,0 +1,31 @@
+theory ExLetMult
+imports "Parser"
+begin
+
+atom_decl name
+
+ML {* val _ = recursive := true *}
+ML {* val _ = alpha_type := AlphaLst *}
+ML {* val _ = cheat_equivp := true *}
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm"
+| Lm "trm" "trm"
+| Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t, bind "bn l" in s
+and lts =
+  Lnil
+| Lcons "name" "trm" "lts"
+binder
+  bn
+where
+  "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
+
+thm trm_lts.eq_iff
+thm trm_lts.induct
+thm trm_lts.fv[simplified trm_lts.supp]
+
+end
+
+
+

--- a/Nominal/Fv.thy	Thu Apr 01 08:06:01 2010 +0200
+++ b/Nominal/Fv.thy	Thu Apr 01 08:48:33 2010 +0200
@@ -931,7 +931,7 @@
   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW

--- a/Nominal/Parser.thy	Thu Apr 01 08:06:01 2010 +0200
+++ b/Nominal/Parser.thy	Thu Apr 01 08:48:33 2010 +0200
@@ -456,9 +456,12 @@
   val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = tracing "Lifting eq-iff";
-  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff
-  val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1
-  val q_eq_iff_pre1 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
+  val _ = map tracing (map PolyML.makestring alpha_eq_iff);
+  val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
+  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
+  val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
+  val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
+  val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;

--- a/Nominal/Rsp.thy	Thu Apr 01 08:06:01 2010 +0200
+++ b/Nominal/Rsp.thy	Thu Apr 01 08:48:33 2010 +0200
@@ -83,7 +83,7 @@
    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
    simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
    asm_full_simp_tac (HOL_ss addsimps (rsp @
-     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
+     @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
   ))
 *}