diff -r 5f5e99a11f66 -r 984ea1299cd7 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Fri Mar 19 06:55:17 2010 +0100
+++ b/Nominal/Fv.thy	Fri Mar 19 08:31:43 2010 +0100
@@ -1,5 +1,5 @@
 theory Fv
-imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
+imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" "Nominal2_FSet"
 begin
 
 (* The bindings data structure:
@@ -141,10 +141,16 @@
 
 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
   | is_atom_set thy _ = false;
+
+fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
+  | is_atom_fset thy _ = false;
+
+val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
 *}
 
 
 
+
 (* Like map2, only if the second list is empty passes empty lists insted of error *)
 ML {*
 fun map2i _ [] [] = []
@@ -201,7 +207,7 @@
     if b = noatoms then a else
     if b = a then noatoms else
     HOLogic.mk_binop @{const_name minus} (a, b);
-  fun mk_atoms t =
+  fun mk_atom_set t =
     let
       val ty = fastype_of t;
       val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
@@ -209,6 +215,14 @@
     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"};
+    in
+      fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t))
+    end;
   (* Similar to one in USyntax *)
   fun mk_pair (fst, snd) =
     let val ty1 = fastype_of fst
@@ -288,7 +302,8 @@
             (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_atoms 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;
@@ -402,7 +417,8 @@
       fun fv_bind args (NONE, i, _) =
             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
             if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else
-            if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else
+            if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else
+            if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (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);
@@ -420,7 +436,8 @@
               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
+                if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else
+                if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset 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 *)
@@ -836,7 +853,8 @@
   simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
     REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN'
     asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
-      swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh}))
+      swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
+      supp_fset_to_set supp_fmap_atom}))
 *}
 
 ML {*
@@ -854,7 +872,8 @@
 
   fun mk_supp_arg (x, ty) =
     if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else
-    if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atoms x)
+    if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else
+    if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x)
     else mk_supp ty x
   val lhss = map mk_supp_arg (frees ~~ tys)
   val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
@@ -888,7 +907,8 @@
 ML {*
 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW (
   rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image finite_insert finite.emptyI finite_Un})
+  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
+    supp_fmap_atom finite_insert finite.emptyI finite_Un})
 *}
 
 ML {*