--- 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 {*

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Nominal2_FSet.thy	Fri Mar 19 08:31:43 2010 +0100
@@ -0,0 +1,107 @@
+theory Nominal2_FSet
+imports FSet Nominal2_Supp
+begin
+
+lemma permute_rsp_fset[quot_respect]:
+  "(op = ===> op \<approx> ===> op \<approx>) permute permute"
+  apply (simp add: eqvts[symmetric])
+  apply clarify
+  apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
+  apply (subst mem_eqvt[symmetric])
+  apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
+  apply (subst mem_eqvt[symmetric])
+  apply (erule_tac x="- x \<bullet> xb" in allE)
+  apply simp
+  done
+
+instantiation FSet.fset :: (pt) pt
+begin
+
+term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+quotient_definition
+  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x"
+  by (rule permute_zero)
+
+lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x"
+  by (lifting permute_list_zero)
+
+lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x"
+  by (rule permute_plus)
+
+lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x"
+  by (lifting permute_list_plus)
+
+instance
+  apply default
+  apply (rule permute_fset_zero)
+  apply (rule permute_fset_plus)
+  done
+
+end
+
+lemma permute_fset[simp,eqvt]:
+  "p \<bullet> ({||} :: 'a :: pt fset) = {||}"
+  "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
+  by (lifting permute_list.simps)
+
+lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)"
+  apply (induct l)
+  apply (simp_all)
+  apply (simp only: eqvt_apply)
+  done
+
+lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
+  by (lifting map_eqvt)
+
+lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"
+  by (lifting set_eqvt)
+
+lemma supp_fset_to_set:
+  "supp (fset_to_set x) = supp x"
+  apply (simp add: supp_def)
+  apply (simp add: eqvts)
+  apply (simp add: fset_cong)
+  done
+
+lemma atom_fmap_cong:
+  shows "(fmap atom x = fmap atom y) = (x = y)"
+  apply(rule inj_fmap_eq_iff)
+  apply(simp add: inj_on_def)
+  done
+
+lemma supp_fmap_atom:
+  "supp (fmap atom x) = supp x"
+  apply (simp add: supp_def)
+  apply (simp add: eqvts eqvts_raw atom_fmap_cong)
+  done
+
+(*lemma "\<not> (memb x S) \<Longrightarrow> \<not> (memb y T) \<Longrightarrow> ((x # S) \<approx> (y # T)) = (x = y \<and> S \<approx> T)"*)
+
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
+
+lemma supp_insert: "supp (insert (x :: 'a :: fs) xs) = supp x \<union> supp xs"
+  oops
+
+lemma supp_finsert:
+  "supp (finsert (x :: 'a :: fs) S) = supp x \<union> supp S"
+  apply (subst supp_fset_to_set[symmetric])
+  apply simp
+  (* apply (simp add: supp_insert supp_fset_to_set) *)
+  oops
+
+instance fset :: (fs) fs
+  apply (default)
+  apply (induct_tac x rule: fset_induct)
+  apply (simp add: supp_def eqvts)
+  (* apply (simp add: supp_finsert) *)
+  (* apply default ? *)
+  oops
+
+end

--- a/Nominal/TySch.thy	Fri Mar 19 06:55:17 2010 +0100
+++ b/Nominal/TySch.thy	Fri Mar 19 08:31:43 2010 +0100
@@ -10,109 +10,6 @@
 ML {* val _ = cheat_fv_eqvt := false *}
 ML {* val _ = cheat_alpha_eqvt := false *}
 
-lemma permute_rsp_fset[quot_respect]:
-  "(op = ===> op \<approx> ===> op \<approx>) permute permute"
-  apply (simp add: eqvts[symmetric])
-  apply clarify
-  apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
-  apply (subst mem_eqvt[symmetric])
-  apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
-  apply (subst mem_eqvt[symmetric])
-  apply (erule_tac x="- x \<bullet> xb" in allE)
-  apply simp
-  done
-
-instantiation FSet.fset :: (pt) pt
-begin
-
-term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-quotient_definition
-  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x"
-by (rule permute_zero)
-
-lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x"
-by (lifting permute_list_zero)
-
-lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x"
-by (rule permute_plus)
-
-lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x"
-by (lifting permute_list_plus)
-
-instance
-apply default
-apply (rule permute_fset_zero)
-apply (rule permute_fset_plus)
-done
-
-end
-
-lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"
-by (lifting set_eqvt)
-
-thm list_induct2'[no_vars]
-
-lemma fset_induct2:
-    "Pa {||} {||} \<Longrightarrow>
-    (\<forall>x xs. Pa (finsert x xs) {||}) \<Longrightarrow>
-    (\<forall>y ys. Pa {||} (finsert y ys)) \<Longrightarrow>
-    (\<forall>x xs y ys. Pa xs ys \<longrightarrow> Pa (finsert x xs) (finsert y ys)) \<Longrightarrow>
-    Pa xsa ysa"
-by (lifting list_induct2')
-
-lemma set_cong: "(set x = set y) = (x \<approx> y)"
-  apply rule
-  apply simp_all
-  apply (induct x y rule: list_induct2')
-  apply simp_all
-  apply auto
-  done
-
-lemma fset_cong:
-  "(fset_to_set x = fset_to_set y) = (x = y)"
-  by (lifting set_cong)
-
-lemma supp_fset_to_set:
-  "supp (fset_to_set x) = supp x"
-  apply (simp add: supp_def)
-  apply (simp add: eqvts)
-  apply (simp add: fset_cong)
-  done
-
-lemma inj_map_eq_iff:
-  "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
-  by (simp add: Set.expand_set_eq[symmetric] inj_image_eq_iff)
-
-lemma inj_fmap_eq_iff:
-  "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"
-  by (lifting inj_map_eq_iff)
-
-lemma atom_fmap_cong:
-  shows "(fmap atom x = fmap atom y) = (x = y)"
-  apply(rule inj_fmap_eq_iff)
-  apply(simp add: inj_on_def)
-  done
-
-lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)"
-apply (induct l)
-apply (simp_all)
-apply (simp only: eqvt_apply)
-done
-
-lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
-by (lifting map_eqvt)
-
-lemma supp_fmap_atom:
-  "supp (fmap atom x) = supp x"
-  apply (simp add: supp_def)
-  apply (simp add: eqvts eqvts_raw atom_fmap_cong)
-  done
-
 nominal_datatype t =
   Var "name"
 | Fun "t" "t"
@@ -125,42 +22,39 @@
 thm t_tyS.perm
 thm t_tyS.inducts
 thm t_tyS.distinct
+ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 
 lemma finite_fv_t_tyS:
   shows "finite (fv_t t)" "finite (fv_tyS ts)"
   by (induct rule: t_tyS.inducts) (simp_all)
 
-lemma infinite_Un:
-  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
 lemma supp_fv_t_tyS:
   shows "fv_t t = supp t" "fv_tyS ts = supp ts"
-apply(induct rule: t_tyS.inducts)
-apply(simp_all only: t_tyS.fv)
-prefer 3
-apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
-prefer 2
-apply(subst finite_supp_Abs)
-apply(drule sym)
-apply(simp add: finite_fv_t_tyS(1))
-apply(simp)
-apply(simp_all (no_asm) only: supp_def)
-apply(simp_all only: t_tyS.perm)
-apply(simp_all only: permute_ABS)
-apply(simp_all only: t_tyS.eq_iff Abs_eq_iff)
-apply(simp_all only: alpha_gen)
-apply(simp_all only: eqvts[symmetric])
-apply(simp_all only: eqvts eqvts_raw)
-apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
-apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
-apply(simp_all only: de_Morgan_conj[symmetric])
-done
+  apply(induct rule: t_tyS.inducts)
+  apply(simp_all only: t_tyS.fv)
+  prefer 3
+  apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
+  prefer 2
+  apply(subst finite_supp_Abs)
+  apply(drule sym)
+  apply(simp add: finite_fv_t_tyS(1))
+  apply(simp)
+  apply(simp_all (no_asm) only: supp_def)
+  apply(simp_all only: t_tyS.perm)
+  apply(simp_all only: permute_ABS)
+  apply(simp_all only: t_tyS.eq_iff Abs_eq_iff)
+  apply(simp_all only: alpha_gen)
+  apply(simp_all only: eqvts[symmetric])
+  apply(simp_all only: eqvts eqvts_raw)
+  apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
+  apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
+  apply(simp_all only: de_Morgan_conj[symmetric])
+  done
 
 instance t and tyS :: fs
-apply default
-apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS)
-done
+  apply default
+  apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS)
+  done
 
 lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS]
 
@@ -169,7 +63,7 @@
   \<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2);
   \<And>fset t. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)
  \<rbrakk> \<Longrightarrow> P a t"
-
+  oops
 
 
 lemma