--- a/Nominal/Fv.thy	Tue Mar 09 11:36:40 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 09 16:24:39 2010 +0100
@@ -77,7 +77,8 @@
 *}
 
 (* Finds bindings with the same function and binding, and gathers all
-   bodys for such pairs *)
+   bodys for such pairs
+ *)
 ML {*
 fun gather_binds binds =
 let
@@ -143,9 +144,58 @@
 
 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
 
+ML {*
+fun non_rec_binds l =
+let
+  fun is_non_rec (SOME (f, false), _, _) = SOME f
+    | is_non_rec _ = NONE
+in
+  distinct (op =) (map_filter is_non_rec (flat (flat l)))
+end
+*}
+
+(* We assume no bindings in the type on which bn is defined *)
+ML {*
+fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bn) =
+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) =
+  let
+    val Ts = map (typ_of_dtyp descr sorts) dts;
+    val names = Datatype_Prop.make_tnames Ts;
+    val args = map Free (names ~~ Ts);
+    val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
+    fun fv_arg ((dt, x), arg_no) =
+      let
+        val ty = fastype_of x
+      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: not good")
+          else @{term "{} :: atom set"}) else
+        if is_atom thy ty then mk_single_atom x else
+        if is_atom_set thy ty then mk_atoms 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
+    HOLogic.mk_Trueprop (HOLogic.mk_eq
+      (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos))))
+  end;
+  val (_, (_, _, constrs)) = nth descr ith_dtyp;
+  val eqs = map fv_bn_constr constrs
+in
+  ((bn, fvbn), (fvbn_name, eqs))
+end
+*}
+
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
-fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy =
+fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
 let
   val thy = ProofContext.theory_of lthy;
   val {descr, sorts, ...} = dt_info;
@@ -154,6 +204,11 @@
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
   val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
   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 fv_bns = 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, _) =>
     "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
   val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
@@ -182,22 +237,30 @@
             if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else
             (* TODO we do not know what to do with non-atomizable things *)
             @{term "{} :: atom set"}
-        | fv_bind args (SOME f, i, _) = f $ (nth args i);
+        | fv_bind args (SOME (f, _), i, _) = f $ (nth args i);
       fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
+      fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE
+        | find_nonrec_binder _ _ = NONE
       fun fv_arg ((dt, x), arg_no) =
-        let
-          val arg =
-            if is_rec_type dt then nth fv_frees (body_index dt) $ x else
-            if ((is_atom thy) o fastype_of) x then mk_single_atom x else
-            if ((is_atom_set thy) o fastype_of) x then mk_atoms x else
-            (* TODO we do not know what to do with non-atomizable things *)
-            @{term "{} :: atom set"}
-          (* If i = j then we generate it only once *)
-          val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
-          val sub = fv_binds args relevant
-        in
-          mk_diff arg sub
-        end;
+        case get_first (find_nonrec_binder arg_no) bindcs of
+          SOME f =>
+            (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of
+                SOME fv_bn => fv_bn $ x
+              | NONE => error "bn specified in a non-rec binding but not in bn list")
+        | NONE =>
+            let
+              val arg =
+                if is_rec_type dt then nth fv_frees (body_index dt) $ x else
+                if ((is_atom thy) o fastype_of) x then mk_single_atom x else
+                if ((is_atom_set thy) o fastype_of) x then mk_atoms x else
+                (* TODO we do not know what to do with non-atomizable things *)
+                @{term "{} :: atom set"}
+              (* If i = j then we generate it only once *)
+              val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
+              val sub = fv_binds args relevant
+            in
+              mk_diff arg sub
+            end;
       val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
         (fv_c $ list_comb (c, args), mk_union (map fv_arg  (dts ~~ args ~~ arg_nos))))
       val alpha_rhs =
@@ -240,9 +303,12 @@
     end;
   fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds;
   val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr (gather_binds bindsall)))
+  val fv_eqs_all = fv_eqs @ (flat fv_bn_eqs);
+  val fv_names_all = fv_names @ fv_bn_names;
   val add_binds = map (fn x => (Attrib.empty_binding, x))
+(* Function_Fun.add_fun Function_Common.default_config ... true *)
   val (fvs, lthy') = (Primrec.add_primrec
-    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)
+    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
   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}
@@ -253,18 +319,31 @@
 end
 *}
 
-(* tests
+(*
 atom_decl name
 
-datatype ty =
-  Var "name set"
+datatype lam =
+  VAR "name"
+| APP "lam" "lam"
+| LET "bp" "lam"
+and bp =
+  BP "name" "lam"
 
-ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *}
+primrec
+  bi::"bp \<Rightarrow> atom set"
+where
+  "bi (BP x t) = {atom x}"
 
-local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *}
-print_theorems
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *}
 
 
+local_setup {*
+  snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam")
+  [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [0])] *}
+print_theorems
+*)
+
+(*
 datatype rtrm1 =
   rVr1 "name"
 | rAp1 "rtrm1" "rtrm1"

--- a/Nominal/Parser.thy	Tue Mar 09 11:36:40 2010 +0100
+++ b/Nominal/Parser.thy	Tue Mar 09 16:24:39 2010 +0100
@@ -146,7 +146,7 @@
 ML {* 
 fun rawify_binds dts_env cnstrs_env bn_fun_env binds =
   map (map (map (map (fn (opt_trm, i, j) => 
-    (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env) opt_trm, i, j))))) binds
+    (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds
 *}
 
 ML {* 
@@ -232,6 +232,8 @@
   val thy_name = Context.theory_name thy
   val (((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), lthy2) =
     raw_nominal_decls dts bn_funs bn_eqs binds lthy
+  val bn_funs_decls = [];
+
   val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
   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
@@ -250,7 +252,12 @@
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
   val raw_binds_flat = map (map flat) raw_binds;
-  val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3;
+  val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3;
+in
+if !restricted_nominal = 0 then
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
+else
+let
   val alpha_ts_loc = #preds alpha
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
@@ -268,11 +275,6 @@
   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
-in
-if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
-else
-let
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
     ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
@@ -436,7 +438,7 @@
   fun prep_bn env bn_str =
     case (Syntax.read_term lthy bn_str) of
        Free (x, _) => (NONE, env_lookup env x)
-     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), env_lookup env x)
+     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x)
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
   fun prep_typ env (i, opt_name) =