--- a/Nominal/Abs.thy	Wed Apr 21 10:13:17 2010 +0200
+++ b/Nominal/Abs.thy	Wed Apr 21 10:20:48 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	Wed Apr 21 10:13:17 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	Wed Apr 21 10:20:48 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/FSet.thy	Wed Apr 21 10:13:17 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 10:20:48 2010 +0200
@@ -614,7 +614,7 @@
   have "fcard_raw l = 0" by fact
   then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
   then have z: "l = []" using no_memb_nil by auto
-  then have "r = []" sorry
+  then have "r = []" using `l \<approx> r` by simp
   then show ?case using z list_eq2_refl by simp
 next
   case (Suc m)

--- a/Nominal/Fv.thy	Wed Apr 21 10:13:17 2010 +0200
+++ b/Nominal/Fv.thy	Wed Apr 21 10:20:48 2010 +0200
@@ -137,7 +137,7 @@
 *)
 
 ML {*
-datatype alpha_type = AlphaGen | AlphaRes | AlphaLst;
+datatype alpha_mode = AlphaGen | AlphaRes | AlphaLst;
 *}
 
 ML {*

--- a/Nominal/Parser.thy	Wed Apr 21 10:13:17 2010 +0200
+++ b/Nominal/Parser.thy	Wed Apr 21 10:20:48 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/Perm.thy	Wed Apr 21 10:13:17 2010 +0200
+++ b/Nominal/Perm.thy	Wed Apr 21 10:20:48 2010 +0200
@@ -2,56 +2,11 @@
 imports "../Nominal-General/Nominal2_Atoms"
 begin
 
+(* definitions of the permute function for raw nominal datatypes *)
 
 
 ML {*
-fun prove_perm_zero lthy induct perm_def perm_frees =
-let
-  val perm_types = map fastype_of perm_frees;
-  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
-  fun glc ((perm, T), x) =
-    HOLogic.mk_eq (perm $ @{term "0::perm"} $ Free (x, T), Free (x, T))
-  val gl =
-    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)));
-  fun tac _ =
-    EVERY [
-      Datatype_Aux.indtac induct perm_indnames 1,
-      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def)))
-    ];
-in
-  Datatype_Aux.split_conj_thm (Goal.prove lthy perm_indnames [] gl tac)
-end;
-*}
-
-ML {*
-fun prove_perm_plus lthy induct perm_def perm_frees =
-let
-  val pi1 = Free ("pi1", @{typ perm});
-  val pi2 = Free ("pi2", @{typ perm});
-  val perm_types = map fastype_of perm_frees
-  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
-  fun glc ((perm, T), x) =
-    HOLogic.mk_eq (
-      perm $ (mk_plus pi1 pi2) $ Free (x, T),
-      perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
-  val goal =
-    (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
-  fun tac _ =
-    EVERY [
-      Datatype_Aux.indtac induct perm_indnames 1,
-      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def)))
-    ]
-in
-  Datatype_Aux.split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] goal tac)
-end;
-*}
-
-
-(* definitions of the permute function for a raw nominal datatype *)
-
-ML {*
+(* returns the type of the nth datatype *)
 fun nth_dtyp dt_descr sorts i = 
   Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i);
 *}
@@ -93,8 +48,59 @@
 *}
 
 ML {*
+fun prove_permute_zero lthy induct perm_defs perm_fns =
+let
+  val perm_types = map (body_type o fastype_of) perm_fns
+  val perm_indnames = Datatype_Prop.make_tnames perm_types
+  
+  fun single_goal ((perm_fn, T), x) =
+    HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
+
+  val goals =
+    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
+
+  val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
+
+  val tac = (Datatype_Aux.indtac induct perm_indnames 
+             THEN_ALL_NEW asm_simp_tac simps) 1
+in
+  Goal.prove lthy perm_indnames [] goals (K tac)
+  |> Datatype_Aux.split_conj_thm
+end
+*}
+
+ML {*
+fun prove_permute_plus lthy induct perm_defs perm_fns =
+let
+  val pi1 = Free ("p", @{typ perm})
+  val pi2 = Free ("q", @{typ perm})
+  val perm_types = map (body_type o fastype_of) perm_fns
+  val perm_indnames = Datatype_Prop.make_tnames perm_types
+  
+  fun single_goal ((perm, T), x) = HOLogic.mk_eq 
+      (perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
+
+  val goals =
+    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
+
+  val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
+
+  val tac = (Datatype_Aux.indtac induct perm_indnames
+             THEN_ALL_NEW asm_simp_tac simps) 1
+in
+  Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
+  |> Datatype_Aux.split_conj_thm 
+end
+*}
+
+ML {*
 (* defines the permutation functions for raw datatypes and
    proves that they are instances of pt
+
+   dt_nos refers to the number of "un-unfolded" datatypes
+   given by the user
 *)
 fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy =
 let
@@ -117,12 +123,12 @@
   val lthy =
     Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
    
-  val ((perm_frees, perm_ldef), lthy') =
+  val ((perm_fns, perm_ldef), lthy') =
     Primrec.add_primrec
       (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
     
-  val perm_zero_thms = prove_perm_zero lthy' induct perm_ldef perm_frees
-  val perm_plus_thms = prove_perm_plus lthy' induct perm_ldef perm_frees
+  val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns
+  val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns
   val perm_zero_thms' = List.take (perm_zero_thms, dt_nos);
   val perm_plus_thms' = List.take (perm_plus_thms, dt_nos)
   val perms_name = space_implode "_" perm_fn_names
@@ -130,42 +136,20 @@
   val perms_plus_bind = Binding.name (perms_name ^ "_plus")
   
   fun tac _ (_, simps, _) =
-    (Class.intro_classes_tac []) THEN ALLGOALS (resolve_tac simps);
+    Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
   
   fun morphism phi (dfs, simps, fvs) =
     (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
-  in
-    lthy'
-    |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
-    |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
-    |> Class_Target.prove_instantiation_exit_result morphism tac 
-         (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_frees)
-  end
-*}
-
-(* Test *)
-(*atom_decl name
-
-datatype trm =
-  Var "name"
-| App "trm" "trm list"
-| Lam "name" "trm"
-| Let "bp" "trm" "trm"
-and bp =
-  BUnit
-| BVar "name"
-| BPair "bp" "bp"
-
-setup {* fn thy =>
-let 
-  val info = Datatype.the_info thy "Perm.trm"
 in
-  define_raw_perms info 2 thy |> snd
+  lthy'
+  |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
+  |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
+  |> Class_Target.prove_instantiation_exit_result morphism tac 
+       (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns)
 end
 *}
 
-print_theorems
-*)
+(* permutations for quotient types *)
 
 ML {*
 fun quotient_lift_consts_export qtys spec ctxt =
@@ -228,11 +212,12 @@
 
 
 (* Test *)
-(*atom_decl name
+(*
+atom_decl name
 
 datatype trm =
   Var "name"
-| App "trm" "trm list"
+| App "trm" "(trm list) list"
 | Lam "name" "trm"
 | Let "bp" "trm" "trm"
 and bp =
@@ -242,9 +227,9 @@
 
 setup {* fn thy =>
 let 
-  val inf = Datatype.the_info thy "Perm.trm"
+  val info = Datatype.the_info thy "Perm.trm"
 in
-  define_raw_perms inf 2 thy |> snd
+  define_raw_perms info 2 thy |> snd
 end
 *}
 

--- a/Nominal/ROOT.ML	Wed Apr 21 10:13:17 2010 +0200
+++ b/Nominal/ROOT.ML	Wed Apr 21 10:20:48 2010 +0200
@@ -3,7 +3,7 @@
 no_document use_thys
    ["Ex/Lambda",
     "Ex/ExLF",
-    "Ex/Ex1",
+    "Ex/SingleLet",
     "Ex/Ex1rec",
     "Ex/Ex2",
     "Ex/Ex3",