--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/NewFv.thy	Tue Apr 27 19:01:22 2010 +0200
@@ -0,0 +1,243 @@
+theory NewFv
+imports "../Nominal-General/Nominal2_Atoms" 
+        "Abs" "Perm" "Rsp" "Nominal2_FSet"
+begin
+
+ML {*
+datatype bmodes =
+   BEmy of int
+|  BLst of ((term option * int) list) * (int list)
+|  BSet of ((term option * int) list) * (int list)
+|  BRes of ((term option * int) list) * (int list)
+*}
+
+ML {*
+  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
+  (* TODO: It is the same as one in 'nominal_atoms' *)
+  fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
+  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];
+  val noatoms = @{term "{} :: atom set"};
+  fun mk_union sets =
+    fold (fn a => fn b =>
+      if a = noatoms then b else
+      if b = noatoms then a else
+      if a = b then a else
+      HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
+*}
+
+ML {*
+fun is_atom thy typ =
+  Sign.of_sort thy (typ, @{sort at})
+
+fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
+  | is_atom_set _ _ = false;
+
+fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
+  | is_atom_fset _ _ = false;
+
+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) $ Const (@{const_name atom}, 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 \<Rightarrow> atom set"}
+in
+  fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t))
+end;
+
+fun mk_diff a b =
+  if b = noatoms then a else
+  if b = a then noatoms else
+  HOLogic.mk_binop @{const_name minus} (a, b);
+*}
+
+ML {*
+fun atoms thy x =
+let
+  val ty = fastype_of x;
+in
+  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
+  @{term "{} :: atom set"}
+end
+*}
+
+ML {*
+fun setify x =
+  if fastype_of x = @{typ "atom list"} then
+  Const (@{const_name set}, @{typ "atom list \<Rightarrow> atom set"}) $ x else x
+*}
+
+ML {*
+fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
+let
+  fun fv_body i =
+    let
+      val x = nth args i;
+      val dt = nth dts i;
+    in
+      if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x
+    end
+  val fv_bodys = mk_union (map fv_body bodys)
+  val bound_vars =
+    case binds of
+      [(SOME bn, i)] => setify (bn $ nth args i)
+    | _ => mk_union (map fv_body (map snd binds));
+  val non_rec_vars =
+    case binds of
+      [(SOME bn, i)] =>
+        if i mem bodys
+        then ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
+        else noatoms
+    | _ => noatoms
+in
+  mk_union [mk_diff fv_bodys bound_vars, non_rec_vars]
+end
+*}
+
+ML {*
+fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm =
+case bm of
+  BEmy i =>
+    let
+      val x = nth args i;
+      val dt = nth dts i;
+    in
+      case AList.lookup (op=) args_in_bn i of
+        NONE => if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x
+      | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
+      | SOME NONE => noatoms
+    end
+| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
+| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
+| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
+*}
+
+ML {*
+fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees
+  bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =
+let
+  val {descr, sorts, ...} = dt_info;
+  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  fun fv_bn_constr (cname, dts) (args_in_bn, bml) =
+  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));
+    val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
+  in
+    HOLogic.mk_Trueprop (HOLogic.mk_eq
+      (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
+  end;
+  val (_, (_, _, constrs)) = nth descr ith_dtyp;
+in
+  map2 fv_bn_constr constrs (args_in_bns ~~ bmll)
+end
+*}
+
+ML {*
+fun fv_bns thy dt_info fv_frees bns bmlll =
+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 bns);
+  val bn_fvbn = (map (fn (bn, _, _) => bn) bns) ~~ fvbn_frees
+  val bmlls = map (fn (_, i, _) => nth bmlll i) bns;
+  val eqs = map2 (fv_bn thy dt_info fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bns);
+in
+  (bn_fvbn, (fvbn_names, eqs))
+end
+*}
+
+ML {*
+fun fv_bm thy dts args fv_frees bn_fvbn bm =
+case bm of
+  BEmy i =>
+    let
+      val x = nth args i;
+      val dt = nth dts i;
+    in
+      if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x
+    end
+| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
+| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
+| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
+*}
+
+ML {*
+fun fv thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn bmll (fv_free, ith_dtyp) =
+let
+  val {descr, sorts, ...} = dt_info;
+  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  fun fv_constr (cname, dts) bml =
+  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));
+    val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
+  in
+    HOLogic.mk_Trueprop (HOLogic.mk_eq
+      (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
+  end;
+  val (_, (_, _, constrs)) = nth descr ith_dtyp;
+in
+  map2 fv_constr constrs bmll
+end
+*}
+ML {*
+val by_pat_completeness_auto =
+  Proof.global_terminal_proof
+    (Method.Basic Pat_Completeness.pat_completeness,
+     SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
+
+fun termination_by method =
+  Function.termination_proof NONE
+  #> Proof.global_terminal_proof (Method.Basic method, NONE)
+*}
+
+
+
+ML {*
+fun define_fv dt_info bns bmlll lthy =
+let
+  val thy = ProofContext.theory_of lthy;
+  val {descr, sorts, ...} = dt_info;
+  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
+    "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 (bn_fvbn, (fv_bn_names, fv_bn_eqs)) = fv_bns thy dt_info fv_frees bns bmlll;
+  val fvbns = map snd bn_fvbn;
+  val fv_nums = 0 upto (length fv_frees - 1)
+  val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bmlll (fv_frees ~~ fv_nums);
+  val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
+  val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs)
+  val lthy' =
+    lthy
+    |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config
+    |> by_pat_completeness_auto
+    |> Local_Theory.restore
+    |> termination_by (Lexicographic_Order.lexicographic_order)
+in
+  (fv_frees @ fvbns, lthy')
+end
+*}
+
+end

--- a/Nominal/NewParser.thy	Tue Apr 27 14:30:44 2010 +0200
+++ b/Nominal/NewParser.thy	Tue Apr 27 19:01:22 2010 +0200
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "Equivp" "Rsp" "Lift"
+        "Perm" "NewFv"
 begin
 
 section{* Interface for nominal_datatype *}
@@ -51,14 +51,6 @@
 *}
 
 ML {*
-datatype bmodes =
-   BEmy of int
-|  BLst of ((term option * int) list) * (int list)
-|  BSet of ((term option * int) list) * (int list)
-|  BRes of ((term option * int) list) * (int list)
-*}
-
-ML {*
 fun get_cnstrs dts =
   map (fn (_, _, _, constrs) => constrs) dts
 
@@ -277,8 +269,17 @@
 
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
+
+  val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
+  fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
+  val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
+  val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
+  val thy = Local_Theory.exit_global lthy2;
+  val lthy3 = Theory_Target.init NONE thy;
+
+  val (_, lthy4) = define_fv dtinfo bn_funs_decls raw_bclauses lthy3;
 in
-  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy2)
+  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
 end
 *}
 
@@ -500,6 +501,7 @@
 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars]
 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
+thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps