--- a/Nominal/NewAlpha.thy	Mon May 24 20:02:37 2010 +0100
+++ b/Nominal/NewAlpha.thy	Mon May 24 20:50:15 2010 +0100
@@ -181,7 +181,7 @@
 *}
 
 ML {*
-fun define_raw_alpha descr sorts bn_info bclausesss fvs fv_bns lthy =
+fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy =
 let
   val alpha_names = prefix_dt_names descr sorts "alpha_"
   val alpha_arg_tys = all_dtyps descr sorts
@@ -226,6 +226,4 @@
 end
 *}
 
-ML {* ProofContext.export_morphism *}
-
 end

--- a/Nominal/NewParser.thy	Mon May 24 20:02:37 2010 +0100
+++ b/Nominal/NewParser.thy	Mon May 24 20:50:15 2010 +0100
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "NewAlpha" "Tacs" "Equivp" "Lift"
+        "Perm" "Tacs" "Equivp" "Lift"
 begin
 
 
@@ -351,7 +351,7 @@
   (* 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 raw_fvs raw_fv_bns lthy3a
+    then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a
     else raise TEST lthy3a
   
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length raw_fvs) alpha_ts

--- a/Nominal/Perm.thy	Mon May 24 20:02:37 2010 +0100
+++ b/Nominal/Perm.thy	Mon May 24 20:50:15 2010 +0100
@@ -2,58 +2,23 @@
 imports 
   "../Nominal-General/Nominal2_Base"
   "../Nominal-General/Nominal2_Atoms" 
-  "Nominal2_FSet"
+  "Nominal2_FSet" "Abs"
 uses ("nominal_dt_rawperm.ML")
      ("nominal_dt_rawfuns.ML")
+     ("nominal_dt_alpha.ML")
 begin
 
 use "nominal_dt_rawperm.ML"
-use "nominal_dt_rawfuns.ML"
-
-ML {*
-open Nominal_Dt_RawPerm
-open Nominal_Dt_RawFuns
-*}
+ML {* open Nominal_Dt_RawPerm *}
 
-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
-
+use "nominal_dt_rawfuns.ML"
+ML {* open Nominal_Dt_RawFuns *}
 
-(* 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
+use "nominal_dt_alpha.ML"
+ML {* open Nominal_Dt_Alpha *}
 
-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 *}
-
 ML {*
 fun quotient_lift_consts_export qtys spec ctxt =
 let
@@ -112,31 +77,4 @@
 end
 *}
 
-
-
-(* Test *)
-(*
-atom_decl name
-
-datatype trm =
-  Var "name"
-| App "trm" "(trm list) 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
 end
-*}
-
-print_theorems
-*)
-
-end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Mon May 24 20:50:15 2010 +0100
@@ -0,0 +1,237 @@
+(*  Title:      nominal_dt_alpha.ML
+    Author:     Cezary Kaliszyk
+    Author:     Christian Urban
+
+  Definitions of the alpha relations.
+*)
+
+signature NOMINAL_DT_ALPHA =
+sig
+  val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
+    bclause list list list -> term list -> Proof.context -> 
+    term list * thm list * thm list * thm * local_theory
+end
+
+structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
+struct
+
+(* construct the compound terms for prod_fv and prod_alpha *)
+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
+
+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
+
+(* generates the compound binder terms *)
+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 (combine_fn, bind_fn) =
+    case bmode of
+      Lst => (mk_append, bind_lst) 
+    | Set => (mk_union,  bind_set)
+    | Res => (mk_union,  bind_set)
+in
+  foldl1 combine_fn (map (bind_fn lthy args) bodies)
+end
+
+(* produces the term for an alpha with abstraction *)
+fun mk_alpha_term bmode fv alpha args args' binders binders' =
+let
+  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"}
+  val pair_lhs = HOLogic.mk_prod (binders, args)
+  val pair_rhs = HOLogic.mk_prod (binders', args')
+in
+  HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},
+    Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) 
+      $ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs)
+end
+
+(* for non-recursive binders we have to produce alpha_bn premises *)
+fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = 
+  case binder of
+    (NONE, _) => []
+  | (SOME bn, i) =>
+     if member (op=) bodies i then [] 
+     else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)]
+
+(* generat the premises for an alpha rule; mk_frees is used
+   if no binders are present *)
+fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
+let
+  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
+  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_term 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
+
+(* produces the introduction rule for an alpha rule *)
+fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = 
+let
+  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
+  Library.foldr Logic.mk_implies (flat prems, concl)
+end
+
+(* produces the premise of an alpha-bn rule; we only need to
+   treat the case special where the binding clause is empty;
+   
+   - if the body is not included in the bn_info, then we either
+     produce an equation or an alpha-premise
+
+   - if the body is included in the bn_info, then we create
+     either a recursive call to alpha-bn, or no premise  *)
+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
+
+fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
+let
+  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
+  Library.foldr Logic.mk_implies (flat prems, concl)
+end
+
+fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
+let
+  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
+
+fun define_raw_alpha descr sorts bn_info bclausesss fvs 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 (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 constrs_info = all_dtyp_constrs_types descr sorts
+
+  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_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_intros [] lthy
+
+  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 phi = ProofContext.export_morphism lthy' lthy;
+
+  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_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
+end
+
+end (* structure *)
+

--- a/Nominal/nominal_dt_rawfuns.ML	Mon May 24 20:02:37 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Mon May 24 20:50:15 2010 +0100
@@ -1,9 +1,8 @@
-(*  Title:      nominal_dt_rawperm.ML
+(*  Title:      nominal_dt_rawfuns.ML
     Author:     Cezary Kaliszyk
     Author:     Christian Urban
 
-  Definitions of the raw bn, fv and fv_bn
-  functions
+  Definitions of the raw fv and fv_bn functions
 *)
 
 signature NOMINAL_DT_RAWFUNS =