# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268150271 -3600
# Node ID 56efa1e854bfdd2666b9cf81cbd7344ecdb07de5
# Parent  aa787c9b6955ae54e224b344e324ea0e07d450f2
Separate primrecs in Fv.

diff -r aa787c9b6955 -r 56efa1e854bf Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 09 16:24:39 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 09 16:57:51 2010 +0100
@@ -193,6 +193,8 @@
 end
 *}
 
+ML {* fn x => split_list(flat x) *}
+ML {* fn x => apsnd flat (split_list (map split_list x)) *}
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
@@ -302,18 +304,29 @@
       (fv_eq, alpha_eq)
     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 fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall)
+  val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs))
+  val rel_bns_nos = map (fn (_, i, _) => i) rel_bns;
+  fun filter_fun (a, b) = b mem rel_bns_nos;
+  val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1))
+  val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs)))
+  val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs)))
+  val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs);
+  val fv_names_all = fv_names_fst @ fv_bn_names;
   val add_binds = map (fn x => (Attrib.empty_binding, x))
 (* Function_Fun.add_fun Function_Common.default_config ... true *)
+  val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)
   val (fvs, lthy') = (Primrec.add_primrec
     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
-  val (alphas, lthy'') = (Inductive.add_inductive_i
+  val (fvs2, lthy'') =
+    if fv_eqs_snd = [] then (([], []), lthy') else
+   (Primrec.add_primrec
+    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) 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}
      (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
-     (add_binds alpha_eqs) [] lthy')
+     (add_binds alpha_eqs) [] lthy'')
 in
   ((fvs, alphas), lthy'')
 end
@@ -339,7 +352,7 @@
 
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam")
-  [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [0])] *}
+  [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [0])] *}
 print_theorems
 *)