--- a/Nominal/Nominal2_FSet.thy	Mon Mar 22 09:02:30 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Mon Mar 22 10:15:46 2010 +0100
@@ -147,10 +147,22 @@
   apply (simp add: supp_fset_to_set)
   done
 
+lemma supp_fempty:
+  "supp {||} = {}"
+  by (simp add: supp_def eqvts)
+
 instance fset :: (at) fs
   apply (default)
   apply (induct_tac x rule: fset_induct)
-  apply (simp add: supp_def eqvts)
+  apply (simp add: supp_fempty)
+  apply (simp add: supp_at_finsert)
+  apply (simp add: supp_at_base)
+  done
+
+lemma supp_at_fset:
+  "supp (fset :: 'a :: at fset) = fset_to_set (fmap atom fset)"
+  apply (induct fset)
+  apply (simp add: supp_fempty)
   apply (simp add: supp_at_finsert)
   apply (simp add: supp_at_base)
   done

--- a/Nominal/TySch.thy	Mon Mar 22 09:02:30 2010 +0100
+++ b/Nominal/TySch.thy	Mon Mar 22 10:15:46 2010 +0100
@@ -14,8 +14,12 @@
 and tyS =
   All xs::"name fset" ty::"t" bind xs in ty
 
-lemma size_eqvt: "size (pi \<bullet> x) = size x"
-sorry (* Can this be shown? *)
+lemma size_eqvt_raw:
+  "size (pi \<bullet> t :: t_raw) = size t"
+  "size (pi \<bullet> ts :: tyS_raw) = size ts"
+  apply (induct rule: t_raw_tyS_raw.inducts)
+  apply simp_all
+  done
 
 instantiation t and tyS :: size begin
 
@@ -36,7 +40,7 @@
   apply (simp_all only: t_raw_tyS_raw.size)
   apply (simp_all only: alpha_gen)
   apply clarify
-  apply (simp_all only: size_eqvt)
+  apply (simp_all only: size_eqvt_raw)
   done
 
 lemma [quot_respect]:
@@ -73,7 +77,7 @@
   assumes a1: "\<And>name b. P b (Var name)"
   and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
   and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
-  shows "P (a :: 'a :: pt) t \<and> P' d ts "
+  shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
 proof -
   have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
     apply (rule t_tyS.induct)
@@ -85,14 +89,30 @@
     apply simp
     apply (rule allI)
     apply (rule allI)
-    apply(subgoal_tac "\<exists>new::name fset. fset_to_set (fmap atom new) \<sharp>* (d, All (p \<bullet> fset) (p \<bullet> t))
-                                      \<and> fcard new = fcard fset")
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> TySch.All fset t) \<sharp>* pa)")
     apply clarify
-    (*apply(rule_tac t="p \<bullet> All fset t" and 
-                   s="(((p \<bullet> fset) \<leftrightarrow> new) + p) \<bullet> All fset t" in subst)
+    apply(rule_tac t="p \<bullet> TySch.All fset t" and 
+                   s="pa \<bullet> (p \<bullet> TySch.All fset t)" in subst)
+    apply (rule supp_perm_eq)
+    apply assumption
+    apply (simp only: t_tyS.perm)
     apply (rule a3)
-    apply simp_all*)
-    sorry
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    apply (rule at_set_avoiding2)
+    apply (simp add: fin_fset_to_set)
+    apply (simp add: finite_supp)
+    apply (simp add: eqvts finite_supp)
+    apply (subst atom_eqvt_raw[symmetric])
+    apply (subst fmap_eqvt[symmetric])
+    apply (subst fset_to_set_eqvt[symmetric])
+    apply (simp only: fresh_star_permute_iff)
+    apply (simp add: fresh_star_def)
+    apply clarify
+    apply (simp add: fresh_def)
+    apply (simp add: t_tyS_supp)
+    done
   then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
   then show ?thesis by simp
 qed