# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274727757 -3600
# Node ID 45a69c9cc4ccc460a86bb528878f53e9c538a8d2
# Parent  8aff3f3ce47fb12a85cadf9d448e93c715fbf240
alpha works now

diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal-General/nominal_library.ML	Mon May 24 20:02:37 2010 +0100
@@ -22,6 +22,7 @@
   val mk_atom: term -> term
 
   val supp_ty: typ -> typ
+  val supp_const: typ -> term
   val mk_supp_ty: typ -> term -> term
   val mk_supp: term -> term
 
@@ -29,15 +30,17 @@
   val safe_mk_equiv: thm -> thm
 
   val mk_diff: term * term -> term
+  val mk_append: term * term -> term
   val mk_union: term * term -> term
   val fold_union: term list -> term
 
   (* datatype operations *)
+  val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
   val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
   val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> 
-    (term * typ * typ list) list list
+    (term * typ * typ list * bool list) list list
   val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> 
-    (term * typ * typ list) list
+    (term * typ * typ list * bool list) list
   val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
 
 end
@@ -61,7 +64,6 @@
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM ("dest_perm", [t]);
 
-
 fun mk_sort_of t = @{term "sort_of"} $ t;
 
 fun atom_ty ty = ty --> @{typ "atom"};
@@ -70,7 +72,8 @@
 
 
 fun supp_ty ty = ty --> @{typ "atom set"};
-fun mk_supp_ty ty t = Const (@{const_name "supp"}, supp_ty ty) $ t;
+fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty)
+fun mk_supp_ty ty t = supp_const ty $ t;
 fun mk_supp t = mk_supp_ty (fastype_of t) t;
 
 
@@ -78,25 +81,35 @@
 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
 
-(* functions that construct differences and unions
-   but avoid producing empty atom sets *)
+(* functions that construct differences, appends and unions
+   but avoid producing empty atom sets or empty atom lists *)
 
 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
   | mk_diff (t1, @{term "{}::atom set"}) = t1
   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
 
+fun mk_append (@{term "[]::atom list"}, @{term "[]::atom list"}) = @{term "[]::atom list"}
+  | mk_append (t1, @{term "[]::atom list"}) = t1
+  | mk_append (@{term "[]::atom list"}, t2) = t2
+  | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) 
+
 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}
   | mk_union (t1 , @{term "{}::atom set"}) = t1
   | mk_union (@{term "{}::atom set"}, t2) = t2
-  | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2)  
+  | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)  
  
 fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}
 
 
+
+
 (** datatypes **)
 
 
 (* returns the type of the nth datatype *)
+fun all_dtyps descr sorts = 
+  map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1))
+
 fun nth_dtyp descr sorts n = 
   Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
 
@@ -113,8 +126,9 @@
     val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
     val ty = Type (ty_name, vs_tys)
     val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
+    val is_rec = map Datatype_Aux.is_rec_type args
   in
-    (Const (cname, arg_tys ---> ty), ty, arg_tys)
+    (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)
   end
 in
   map (map aux) (all_dtyp_constrs_info descr)
diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/Abs.thy	Mon May 24 20:02:37 2010 +0100
@@ -830,8 +830,14 @@
 where
   "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)"
 
+definition 
+  prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
+where
+ "prod_alpha = prod_rel"
+
+
 lemma [quot_respect]:
-  "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+  shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
   by auto
 
 lemma [quot_preserve]:
@@ -840,11 +846,13 @@
   shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
-lemma [mono]: "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
+lemma [mono]: 
+  shows "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
   by auto
 
 lemma [eqvt]: 
-  shows "p \<bullet> prod_rel A B x y = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+  shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+  unfolding prod_alpha_def
   unfolding prod_rel.simps
   by (perm_simp) (rule refl)
 
diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal/Equivp.thy
--- a/Nominal/Equivp.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/Equivp.thy	Mon May 24 20:02:37 2010 +0100
@@ -1,5 +1,5 @@
 theory Equivp
-imports "NewFv" "Tacs" "Rsp"
+imports "Abs" "Perm" "Tacs" "Rsp"
 begin
 
 ML {*
diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Mon May 24 20:02:37 2010 +0100
@@ -13,6 +13,8 @@
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind_set x in t
 | Let a::"assg" t::"trm"  bind_set "bn a" in t
+| Foo x::"name" y::"name" t::"trm" bind_set x in y t
+| Bar x::"name" y::"name" t::"trm" bind y x in t x y
 and assg =
   As "name" "trm"
 binder
@@ -20,10 +22,12 @@
 where
   "bn (As x t) = {atom x}"
 
+
 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars]
 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
 
 
+
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv
 thm trm_assg.supp
diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal/Lift.thy
--- a/Nominal/Lift.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/Lift.thy	Mon May 24 20:02:37 2010 +0100
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Atoms"
         "../Nominal-General/Nominal2_Eqvt"
         "../Nominal-General/Nominal2_Supp"
-        "Abs" "Perm" "Equivp" "Rsp"
+        "Abs" "Perm" "Rsp"
 begin
 
 
diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal/NewAlpha.thy
--- a/Nominal/NewAlpha.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/NewAlpha.thy	Mon May 24 20:02:37 2010 +0100
@@ -1,236 +1,231 @@
 theory NewAlpha
-imports "Abs" "Perm" "Nominal2_FSet"
-uses ("nominal_dt_rawperm.ML")
-     ("nominal_dt_rawfuns.ML")
+imports "Abs" "Perm"
 begin
 
-use "nominal_dt_rawperm.ML"
-use "nominal_dt_rawfuns.ML"
-
 ML {*
-open Nominal_Dt_RawPerm
-open Nominal_Dt_RawFuns
-*}
-
-
-ML {*
-fun mk_binop2 ctxt s (l, r) =
-  Syntax.check_term ctxt (Const (s, dummyT) $ l $ r)
+fun mk_prod_fv (t1, t2) =
+let
+  val ty1 = fastype_of t1
+  val ty2 = fastype_of t2 
+  val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}
+in
+  Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2
+end
 *}
 
 ML {*
-fun mk_compound_fv' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_fv})
-fun mk_compound_alpha' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_rel})
+fun mk_prod_alpha (t1, t2) =
+let
+  val ty1 = fastype_of t1
+  val ty2 = fastype_of t2 
+  val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)
+  val resT = [prodT, prodT] ---> @{typ "bool"}
+in
+  Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2
+end
 *}
 
 ML {*
-fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees
-  bn_alphabn alpha_const binds bodys =
+fun mk_binders lthy bmode args bodies = 
+let  
+  fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
+    | bind_set _ args (SOME bn, i) = bn $ (nth args i)
+  fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)
+    | bind_lst _ args (SOME bn, i) = bn $ (nth args i)
+
+  val (connect_fn, bind_fn) =
+    case bmode of
+      Lst => (mk_append, bind_lst) 
+    | Set => (mk_union,  bind_set)
+    | Res => (mk_union,  bind_set)
+in
+  foldl1 connect_fn (map (bind_fn lthy args) bodies)
+end
+*}
+
+ML {* 
+fun mk_alpha_prem bmode fv alpha args args' binders binders' =
 let
-  fun bind_set args (NONE, no) = setify lthy (nth args no)
-    | bind_set args (SOME f, no) = f $ (nth args no)
-  fun bind_lst args (NONE, no) = listify lthy (nth args no)
-    | bind_lst args (SOME f, no) = f $ (nth args no)
-  fun append (t1, t2) =
-    Const(@{const_name append}, @{typ "atom list \<Rightarrow> atom list \<Rightarrow> atom list"}) $ t1 $ t2;
-  fun binds_fn args nos =
-    if alpha_const = @{const_name alpha_lst}
-    then foldr1 append (map (bind_lst args) nos)
-    else fold_union (map (bind_set args) nos);
-  val lhs_binds = binds_fn args binds;
-  val rhs_binds = binds_fn args2 binds;
-  val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys);
-  val rhs_bodys = foldr1 HOLogic.mk_prod (map (nth args2) bodys);
-  val lhs = HOLogic.mk_prod (lhs_binds, lhs_bodys);
-  val rhs = HOLogic.mk_prod (rhs_binds, rhs_bodys);
-  val body_dts = map (nth dts) bodys;
-  fun fv_for_dt dt =
-    if Datatype_Aux.is_rec_type dt
-    then nth fv_frees (Datatype_Aux.body_index dt)
-    else Const (@{const_name supp},
-      Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ "atom set"})
-  val fvs = map fv_for_dt body_dts;
-  val fv = mk_compound_fv' lthy fvs;
-  fun alpha_for_dt dt =
-    if Datatype_Aux.is_rec_type dt
-    then nth alpha_frees (Datatype_Aux.body_index dt)
-    else Const (@{const_name "op ="},
-      Datatype_Aux.typ_of_dtyp dt_descr sorts dt -->
-      Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ bool})
-  val alphas = map alpha_for_dt body_dts;
-  val alpha = mk_compound_alpha' lthy alphas;
-  val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs
-  val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre)
-  val t = Syntax.check_term lthy alpha_gen_ex
-  fun alpha_bn_bind (SOME bn, i) =
-      if member (op =) bodys i then NONE
-      else SOME ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)
-    | alpha_bn_bind (NONE, _) = NONE
+  val (alpha_name, binder_ty) = 
+    case bmode of
+      Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
+    | Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
+    | Res => (@{const_name "alpha_res"}, @{typ "atom set"})
+  val ty = fastype_of args
+  val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
+  val alpha_ty = [ty, ty] ---> @{typ "bool"}
+  val fv_ty = ty --> @{typ "atom set"}
 in
-  t :: (map_filter alpha_bn_bind binds)
+  HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},
+    Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) 
+      $ HOLogic.mk_prod (binders, args) $ alpha $ fv $ (Bound 0) $ HOLogic.mk_prod (binders', args'))
 end
 *}
 
 ML {*
-fun alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn args_in_bn bm =
-case bm of
-  BC (_, [], [i]) =>
-    let
-      val arg = nth args i;
-      val arg2 = nth args2 i;
-      val dt = nth dts i;
-    in
-      case AList.lookup (op=) args_in_bn i of
-        NONE => if Datatype_Aux.is_rec_type dt
-                then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2]
-                else [HOLogic.mk_eq (arg, arg2)]
-      | SOME (SOME (f : term)) => [(the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2]
-      | SOME NONE => []
-    end
-| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
-    fv_frees bn_alphabn @{const_name alpha_lst} x y
-| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
-    fv_frees bn_alphabn @{const_name alpha_gen} x y
-| BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
-    fv_frees bn_alphabn @{const_name alpha_res} x y
+fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = 
+  case binder of
+    (NONE, i) => []
+  | (SOME bn, i) =>
+     if member (op=) bodies i
+     then [] 
+     else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)]
 *}
 
-
 ML {*
-fun alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess
-  (alphabn, (_, ith_dtyp, args_in_bns)) =
+fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
 let
-  fun alpha_bn_constr (cname, dts) (args_in_bn, bclauses) =
-  let
-    val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
-    val names = Datatype_Prop.make_tnames Ts;
-    val names2 = Name.variant_list names (Datatype_Prop.make_tnames Ts);
-    val args = map Free (names ~~ Ts);
-    val args2 = map Free (names2 ~~ Ts);
-    val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
-    val alpha_bn_bm = alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees
-      fv_frees bn_alphabn args_in_bn;
-    val rhs = HOLogic.mk_Trueprop
-      (alphabn $ (list_comb (c, args)) $ (list_comb (c, args2)));
-    val lhss = map HOLogic.mk_Trueprop (flat (map alpha_bn_bm bclauses))
-  in
-    Library.foldr Logic.mk_implies (lhss, rhs)
-  end;
-  val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
+  fun mk_frees i =
+    let
+      val arg = nth args i
+      val arg' = nth args' i
+      val ty = fastype_of arg
+    in
+      if nth is_rec i
+      then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg'
+      else HOLogic.mk_eq (arg, arg')
+    end
+  fun mk_alpha_fv i = 
+    let
+      val ty = fastype_of (nth args i)
+    in
+      case AList.lookup (op=) alpha_map ty of
+        NONE => (HOLogic.eq_const ty, supp_const ty) 
+      | SOME (alpha, fv) => (alpha, fv) 
+    end
+  
 in
-  map2 alpha_bn_constr constrs (args_in_bns ~~ bclausess)
+  case bclause of
+    BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies 
+  | BC (bmode, binders, bodies) => 
+    let
+      val (alphas, fvs) = split_list (map mk_alpha_fv bodies)
+      val comp_fv = foldl1 mk_prod_fv fvs
+      val comp_alpha = foldl1 mk_prod_alpha alphas
+      val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
+      val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
+      val comp_binders = mk_binders lthy bmode args binders
+      val comp_binders' = mk_binders lthy bmode args' binders
+      val alpha_prem = 
+        mk_alpha_prem bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
+      val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)
+    in
+      map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)
+    end
 end
 *}
 
 ML {*
-fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss =
+fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = 
 let
-  fun mk_alphabn_free (bn, ith, _) =
-    let
-      val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
-      val ty = nth_dtyp dt_descr sorts ith;
-      val alphabn_type = ty --> ty --> @{typ bool};
-      val alphabn_free = Free(alphabn_name, alphabn_type);
-    in
-      (alphabn_name, alphabn_free)
-    end;
-  val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free bn_funs);
-  val bn_alphabn = (map (fn (bn, _, _) => bn) bn_funs) ~~ alphabn_frees
-  val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;
-  val eqs = map2 (alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausessl
-    (alphabn_frees ~~ bn_funs);
+  val arg_names = Datatype_Prop.make_tnames arg_tys
+  val arg_names' = Name.variant_list arg_names arg_names
+  val args = map Free (arg_names ~~ arg_tys)
+  val args' = map Free (arg_names' ~~ arg_tys)
+  val alpha = fst (the (AList.lookup (op=) alpha_map ty))
+  val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
+  val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses
 in
-  (bn_alphabn, alphabn_names, eqs)
+  Library.foldr Logic.mk_implies (flat prems, concl)
 end
 *}
 
 ML {*
-fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm =
-case bm of
-  BC (_, [], [i]) =>
-    let
-      val arg = nth args i;
-      val arg2 = nth args2 i;
-      val dt = nth dts i;
-    in
-      if Datatype_Aux.is_rec_type dt
-      then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2]
-      else [HOLogic.mk_eq (arg, arg2)]
-    end
-| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
-    fv_frees bn_alphabn @{const_name alpha_lst} x y
-| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
-    fv_frees bn_alphabn @{const_name alpha_gen} x y
-| BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
-    fv_frees bn_alphabn @{const_name alpha_res} x y
+fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =
+let
+  fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i = 
+  let
+    val arg = nth args i
+    val arg' = nth args' i
+    val ty = fastype_of arg
+  in
+    case AList.lookup (op=) bn_args i of
+      NONE => (case (AList.lookup (op=) alpha_map ty) of
+                 NONE =>  [HOLogic.mk_eq (arg, arg')]
+               | SOME (alpha, _) => [alpha $ arg $ arg'])
+    | SOME (NONE) => []
+    | SOME (SOME bn) => [the (AList.lookup (op=) alpha_bn_map bn) $ arg $ arg']
+  end  
+in
+  case bclause of
+    BC (_, [], bodies) => 
+      map HOLogic.mk_Trueprop 
+        (flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies))
+  | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
+end
 *}
 
 ML {*
-fun alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess (alpha_free, ith_dtyp) =
+fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
 let
-  fun alpha_constr (cname, dts) bclauses =
-  let
-    val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
-    val names = Datatype_Prop.make_tnames Ts;
-    val names2 = Name.variant_list names (Datatype_Prop.make_tnames Ts);
-    val args = map Free (names ~~ Ts);
-    val args2 = map Free (names2 ~~ Ts);
-    val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
-    val alpha_bm = alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn
-    val rhs = HOLogic.mk_Trueprop
-      (alpha_free $ (list_comb (c, args)) $ (list_comb (c, args2)));
-    val lhss = map HOLogic.mk_Trueprop (flat (map alpha_bm bclauses))
-  in
-    Library.foldr Logic.mk_implies (lhss, rhs)
-  end;
-  val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
+  val arg_names = Datatype_Prop.make_tnames arg_tys
+  val arg_names' = Name.variant_list arg_names arg_names
+  val args = map Free (arg_names ~~ arg_tys)
+  val args' = map Free (arg_names' ~~ arg_tys)
+  val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm)
+  val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
+  val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses
 in
-  map2 alpha_constr constrs bclausess
+  Library.foldr Logic.mk_implies (flat prems, concl)
 end
 *}
 
 ML {*
-fun define_raw_alpha dt_descr sorts bn_funs bclausesss fv_frees lthy =
+fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
 let
-  val alpha_names = prefix_dt_names dt_descr sorts "alpha_";
-  val alpha_types = map (fn (i, _) =>
-    nth_dtyp dt_descr sorts i --> nth_dtyp dt_descr sorts i --> @{typ bool}) dt_descr;
-  val alpha_frees = map Free (alpha_names ~~ alpha_types);
+  val nth_constrs_info = nth constrs_info bn_n
+  val nth_bclausess = nth bclausesss bn_n
+in
+  map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
+end
+*}
 
-  val (bn_alphabn, alpha_bn_names, alpha_bn_eqs) =
-    alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss
+ML {*
+fun define_raw_alpha descr sorts bn_info bclausesss fvs fv_bns lthy =
+let
+  val alpha_names = prefix_dt_names descr sorts "alpha_"
+  val alpha_arg_tys = all_dtyps descr sorts
+  val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys
+  val alpha_frees = map Free (alpha_names ~~ alpha_tys)
+  val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs)
 
-  val alpha_bns = map snd bn_alphabn;
-  val alpha_bn_types = map fastype_of alpha_bns;
+  val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
+  val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
+  val alpha_bn_names = map (prefix "alpha_") bn_names
+  val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
+  val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys
+  val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
+  val alpha_bn_map = bns ~~ alpha_bn_frees
 
-  val alpha_nums = 0 upto (length alpha_frees - 1)
+  val constrs_info = all_dtyp_constrs_types descr sorts
 
-  val alpha_eqs = map2 (alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausesss
-    (alpha_frees ~~ alpha_nums);
+  val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss 
+  val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info
 
   val all_alpha_names = map2 (fn s => fn ty => ((Binding.name s, ty), NoSyn))
-    (alpha_names @ alpha_bn_names) (alpha_types @ alpha_bn_types)
-  val all_alpha_eqs = map (pair Attrib.empty_binding) (flat alpha_eqs @ flat alpha_bn_eqs)
-
+    (alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys)
+  val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
+  
   val (alphas, lthy') = Inductive.add_inductive_i
      {quiet_mode = true, verbose = false, alt_name = Binding.empty,
       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
-     all_alpha_names [] all_alpha_eqs [] lthy
+     all_alpha_names [] all_alpha_intros [] lthy
 
-  val alpha_ts_loc = #preds alphas;
+  val alpha_trms_loc = #preds alphas;
   val alpha_induct_loc = #raw_induct alphas;
   val alpha_intros_loc = #intrs alphas;
   val alpha_cases_loc = #elims alphas;
-  val morphism = ProofContext.export_morphism lthy' lthy;
+  val phi = ProofContext.export_morphism lthy' lthy;
 
-  val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
-  val alpha_induct = Morphism.thm morphism alpha_induct_loc;
-  val alpha_intros = Morphism.fact morphism alpha_intros_loc
-  val alpha_cases = Morphism.fact morphism alpha_cases_loc
+  val alpha_trms = map (Morphism.term phi) alpha_trms_loc;
+  val alpha_induct = Morphism.thm phi alpha_induct_loc;
+  val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
+  val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
 in
-  (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy')
+  (alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
 end
-handle UnequalLengths => error "Main"
 *}
 
+ML {* ProofContext.export_morphism *}
+
 end
diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/NewParser.thy	Mon May 24 20:02:37 2010 +0100
@@ -343,19 +343,18 @@
   (* definition of raw fv_functions *)
   val lthy3 = Theory_Target.init NONE thy;
 
-  val (fv, fv_bn, fv_def, lthy3a) = 
+  val (raw_fvs, raw_fv_bns, raw_fv_defs, lthy3a) = 
     if get_STEPS lthy2 > 3 
     then define_raw_fvs descr sorts raw_bn_info raw_bclauses lthy3
     else raise TEST lthy3
-  
 
   (* definition of raw alphas *)
   val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) =
     if get_STEPS lthy > 4 
-    then define_raw_alpha descr sorts raw_bn_info raw_bclauses fv lthy3a
+    then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs raw_fv_bns lthy3a
     else raise TEST lthy3a
   
-  val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
+  val (alpha_ts_nobn, alpha_ts_bn) = chop (length raw_fvs) alpha_ts
   
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr;
   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
@@ -377,12 +376,12 @@
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm ((*raw_bn_eqs @*) raw_perm_defs) (map fst bns) lthy4
-  val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fv_bn) lthy5
+  val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5
   val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
 
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
-  val fv_alpha_all = combine_fv_alpha_bns (fv, fv_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
+  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts
@@ -407,11 +406,11 @@
   val bns_rsp = flat (map snd bns_rsp_pre);
 
   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
-    else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
+    else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1;
   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
   val (fv_rsp_pre, lthy10) = fold_map
     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
-    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fv_bn) lthy9;
+    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9;
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
@@ -425,8 +424,8 @@
       in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11a
-    val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fv_bn)
-  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fv_bn)) lthy12;
+    val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
+  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ [] (*raw_bn_funs*)) lthy12a;
@@ -450,11 +449,11 @@
   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
     [Attrib.internal (K (Rule_Cases.case_names constr_names))]), 
     [Rule_Cases.name constr_names q_induct]) lthy13;
-  val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct
+  val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct
   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
   val q_perm = map (lift_thm qtys lthy14) raw_perm_defs;
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
-  val q_fv = map (lift_thm qtys lthy15) fv_def;
+  val q_fv = map (lift_thm qtys lthy15) raw_fv_defs;
   val lthy16 = note_simp_suffix "fv" q_fv lthy15;
   val q_bn = map (lift_thm qtys lthy16) [] (*raw_bn_eqs;*)
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal/Perm.thy
--- a/Nominal/Perm.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/Perm.thy	Mon May 24 20:02:37 2010 +0100
@@ -1,10 +1,55 @@
 theory Perm
 imports 
   "../Nominal-General/Nominal2_Base"
-  "../Nominal-General/Nominal2_Atoms"
+  "../Nominal-General/Nominal2_Atoms" 
+  "Nominal2_FSet"
+uses ("nominal_dt_rawperm.ML")
+     ("nominal_dt_rawfuns.ML")
 begin
 
+use "nominal_dt_rawperm.ML"
+use "nominal_dt_rawfuns.ML"
 
+ML {*
+open Nominal_Dt_RawPerm
+open Nominal_Dt_RawFuns
+*}
+
+ML {*
+fun is_atom ctxt ty =
+  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
+
+fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
+  | is_atom_set _ _ = false;
+
+fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
+  | is_atom_fset _ _ = false;
+
+fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
+  | is_atom_list _ _ = false
+
+
+(* functions for producing sets, fsets and lists of general atom type
+   out from concrete atom types *)
+fun mk_atom_set t =
+let
+  val ty = fastype_of t;
+  val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
+  val img_ty = atom_ty --> ty --> @{typ "atom set"};
+in
+  Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
+end
+
+fun mk_atom_fset t =
+let
+  val ty = fastype_of t;
+  val atom_ty = dest_fsetT ty --> @{typ "atom"};
+  val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
+  val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
+in
+  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+end
+*}
 (* permutations for quotient types *)
 
 ML {* Class_Target.prove_instantiation_exit_result *}
diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Mon May 24 20:02:37 2010 +0100
@@ -15,6 +15,14 @@
   datatype bmode = Lst | Res | Set
   datatype bclause = BC of bmode * (term option * int) list * int list
 
+  val is_atom: Proof.context -> typ -> bool
+  val is_atom_set: Proof.context -> typ -> bool
+  val is_atom_fset: Proof.context -> typ -> bool
+  val is_atom_list: Proof.context -> typ -> bool
+  val mk_atom_set: term -> term
+  val mk_atom_fset: term -> term
+
+
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
@@ -151,7 +159,7 @@
     case AList.lookup (op=) bn_args i of
       NONE => (case (AList.lookup (op=) fv_map ty) of
                  NONE => mk_supp arg
-              | SOME fv => fv $ arg)
+               | SOME fv => fv $ arg)
     | SOME (NONE) => @{term "{}::atom set"}
     | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
   end  
@@ -161,7 +169,7 @@
   | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
 end
 
-fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
+fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = 
 let
   val arg_names = Datatype_Prop.make_tnames arg_tys
   val args = map Free (arg_names ~~ arg_tys)
@@ -173,7 +181,7 @@
   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 end
 
-fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys)) bclauses =
+fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
 let
   val arg_names = Datatype_Prop.make_tnames arg_tys
   val args = map Free (arg_names ~~ arg_tys)
@@ -196,7 +204,7 @@
 fun define_raw_fvs descr sorts bn_info bclausesss lthy =
 let
   val fv_names = prefix_dt_names descr sorts "fv_"
-  val fv_arg_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
+  val fv_arg_tys = all_dtyps descr sorts
   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
   val fv_frees = map Free (fv_names ~~ fv_tys);
   val fv_map = fv_arg_tys ~~ fv_frees