--- a/Nominal/ExCoreHaskell.thy	Tue Mar 23 11:43:09 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Tue Mar 23 16:28:29 2010 +0100
@@ -82,6 +82,9 @@
 | "bv_tvck TVCKNil = {}"
 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"*)
 
+thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_tvtk_lst_tvck_lst_vt_lst.fv
+
+
 end
 
 

--- a/Nominal/Fv.thy	Tue Mar 23 11:43:09 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 23 16:28:29 2010 +0100
@@ -278,15 +278,15 @@
 end
 *}
 
+ML AList.lookup
+
 (* We assume no bindings in the type on which bn is defined *)
 (* TODO: currently works only with current fv_bn function *)
 ML {*
-fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) =
+fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) =
 let
   val {descr, sorts, ...} = dt_info;
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
-  val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
-  val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp));
   fun fv_bn_constr (cname, dts) args_in_bn =
   let
     val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -296,16 +296,18 @@
     fun fv_arg ((dt, x), arg_no) =
       let
         val ty = fastype_of x
+        val _ = tracing (PolyML.makestring args_in_bn);
+        val _ = tracing (PolyML.makestring bn_fvbn);
       in
-        if arg_no mem args_in_bn then 
-          (if is_rec_type dt then
-            (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.")
-          else @{term "{} :: atom set"}) else
-        if is_atom thy ty then mk_single_atom x else
-        if is_atom_set thy ty then mk_atom_set x else
-        if is_atom_fset thy ty then mk_atom_fset x else
-        if is_rec_type dt then nth fv_frees (body_index dt) $ x else
-        @{term "{} :: atom set"}
+        case AList.lookup (op=) args_in_bn arg_no of
+          SOME NONE => @{term "{} :: atom set"}
+        | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
+        | NONE =>
+            if is_atom thy ty then mk_single_atom x else
+            if is_atom_set thy ty then mk_atom_set x else
+            if is_atom_fset thy ty then mk_atom_fset x else
+            if is_rec_type dt then nth fv_frees (body_index dt) $ x else
+            @{term "{} :: atom set"}
       end;
     val arg_nos = 0 upto (length dts - 1)
   in
@@ -315,20 +317,33 @@
   val (_, (_, _, constrs)) = nth descr ith_dtyp;
   val eqs = map2i fv_bn_constr constrs args_in_bns
 in
-  ((bn, fvbn), (fvbn_name, eqs))
+  ((bn, fvbn), eqs)
 end
 *}
 
 ML {*
-fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) =
+fun fv_bns thy dt_info fv_frees rel_bns =
+let
+  fun mk_fvbn_free (bn, ith, _) =
+    let
+      val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
+    in
+      (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
+    end;
+  val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free rel_bns);
+  val bn_fvbn = (map (fn (bn, _, _) => bn) rel_bns) ~~ fvbn_frees
+  val (l1, l2) = split_list (map (fv_bn thy dt_info fv_frees bn_fvbn) (fvbn_frees ~~ rel_bns));
+in
+  (l1, (fvbn_names ~~ l2))
+end
+*}
+
+
+ML {*
+fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees bn_alphabn ((bn, ith_dtyp, args_in_bns), (alpha_bn_free, is_rec)) =
 let
   val {descr, sorts, ...} = dt_info;
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
-  val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
-  val alpha_bn_type = 
-    (*if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} else*)
-    nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool};
-  val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type);
   val pi = Free("pi", @{typ perm})
   fun alpha_bn_constr (cname, dts) args_in_bn =
   let
@@ -345,12 +360,12 @@
         val argty = fastype_of arg;
         val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty);
       in
-      if is_rec_type dt then
-        if arg_no mem args_in_bn then alpha_bn_free $ arg $ arg2
-        else (nth alpha_frees (body_index dt)) $ arg $ arg2
-      else
-        if arg_no mem args_in_bn then @{term True}
-        else HOLogic.mk_eq (arg, arg2)
+        case AList.lookup (op=) args_in_bn arg_no of
+          SOME NONE => @{term True}
+        | SOME (SOME f) => (the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2
+        | NONE =>
+            if is_rec_type dt then (nth alpha_frees (body_index dt)) $ arg $ arg2
+            else HOLogic.mk_eq (arg, arg2)
       end
     val arg_nos = 0 upto (length dts - 1)
     val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
@@ -361,10 +376,33 @@
   val (_, (_, _, constrs)) = nth descr ith_dtyp;
   val eqs = map2i alpha_bn_constr constrs args_in_bns
 in
-  ((bn, alpha_bn_free), (alpha_bn_name, eqs))
+  ((bn, alpha_bn_free), eqs)
 end
 *}
 
+ML {*
+fun alpha_bns thy dt_info alpha_frees rel_bns bns_rec =
+let
+  val {descr, sorts, ...} = dt_info;
+  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  fun mk_alphabn_free (bn, ith, _) =
+    let
+      val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
+      val alphabn_type = nth_dtyp ith --> nth_dtyp ith --> @{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 rel_bns);
+  val bn_alphabn = (map (fn (bn, _, _) => bn) rel_bns) ~~ alphabn_frees;
+  val pair = split_list (map (alpha_bn thy dt_info alpha_frees bn_alphabn)
+    (rel_bns ~~ (alphabn_frees ~~ bns_rec)))
+in
+  (alphabn_names, pair)
+end
+*}
+
+
 (* Checks that a list of bindings contains only compatible ones *)
 ML {*
 fun bns_same l =
@@ -384,7 +422,7 @@
   val fv_frees = map Free (fv_names ~~ fv_types);
   val nr_bns = non_rec_binds bindsall;
   val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
-  val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);
+  val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns;
   val fvbns = map snd bn_fv_bns;
   val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
@@ -393,8 +431,8 @@
   val alpha_frees = map Free (alpha_names ~~ alpha_types);
   (* We assume that a bn is either recursive or not *)
   val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
-  val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec))
-  val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs;
+  val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) =
+    alpha_bns thy dt_info alpha_frees bns bns_rec
   val alpha_bn_frees = map snd bn_alpha_bns;
   val alpha_bn_types = map fastype_of alpha_bn_frees;
   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =

--- a/Nominal/Parser.thy	Tue Mar 23 11:43:09 2010 +0100
+++ b/Nominal/Parser.thy	Tue Mar 23 16:28:29 2010 +0100
@@ -152,6 +152,27 @@
   | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
 *}
 
+ML {* @{term "{x, y}"} *}
+ML range_type
+ML {*
+fun strip_union t =
+  case t of
+    Const (@{const_name sup}, _) $ l $ r => strip_union l @ strip_union r
+  | (h as (Const (@{const_name insert}, T))) $ x $ y =>
+     (h $ x $ Const (@{const_name bot}, range_type (range_type T))) :: strip_union y
+  | Const (@{const_name bot}, _) => []
+  | _ => [t]
+*}
+
+ML {*
+fun bn_or_atom t =
+  case t of
+    Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ 
+      Const (@{const_name bot}, _) => (i, NONE)
+  | f $ Bound i => (i, SOME f)
+  | _ => error "Unsupported binding function"
+*}
+
 ML {*
 fun prep_bn dt_names dts eqs = 
 let
@@ -166,11 +187,11 @@
     val (ty_name, _) = dest_Type (domain_type ty)
     val dt_index = find_index (fn x => x = ty_name) dt_names
     val (cnstr_head, cnstr_args) = strip_comb cnstr
-    val included = map (fn i => length (cnstr_args) - i - 1) (loose_bnos rhs)
+    val rhs_elements = map bn_or_atom (strip_union rhs)
+    val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
   in
     (dt_index, (bn_fun, (cnstr_head, included)))
   end 
- 
   fun order dts i ts = 
   let
     val dt = nth dts i
@@ -274,6 +295,8 @@
 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
+ML {* fun map_option _ NONE = NONE
+        | map_option f (SOME x) = SOME (f x) *}
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
@@ -284,7 +307,8 @@
   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) =
     raw_nominal_decls dts bn_funs bn_eqs binds lthy
   val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
-  val raw_bns_exp = map (apsnd (map (apfst (Morphism.term morphism_2_1)))) raw_bns;
+  fun export_fun f (t, l) = (f t, map (map (apsnd (map_option f))) l);
+  val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_1)))) raw_bns;
   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
   val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc