--- a/Nominal/Nominal2_Base.thy	Mon Jun 11 14:02:57 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jun 12 01:23:52 2012 +0100
@@ -8,6 +8,7 @@
 imports Main 
         "~~/src/HOL/Library/Infinite_Set"
         "~~/src/HOL/Quotient_Examples/FSet"
+        "~~/src/HOL/Library/FinFun_Syntax"
 keywords
   "atom_decl" "equivariance" :: thy_decl 
 uses ("nominal_basics.ML")
@@ -654,6 +655,30 @@
   by (lifting set_eqvt)
 
 
+subsection {* Permutations for @{typ "'a \<Rightarrow>f 'b"} (FinFuns) *}
+
+instantiation finfun :: (pt, pt) pt
+begin
+
+definition "p \<bullet> f = Abs_finfun (p \<bullet> (finfun_apply f))"
+
+lemma Rep_finfun_permute:
+  shows "p \<bullet> finfun_apply f \<in> finfun"
+apply(simp add: permute_fun_comp)
+apply(rule finfun_right_compose)
+apply(rule finfun_left_compose)
+apply(rule finfun_apply)
+apply(simp)
+done
+
+instance
+apply(default)
+apply(simp_all add: permute_finfun_def finfun_apply_inverse Rep_finfun_permute Abs_finfun_inverse)
+done
+
+end
+
+
 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
 
 instantiation char :: pt
@@ -1190,6 +1215,25 @@
   shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
 
+subsubsection {* Equivariance for @{typ "'a \<Rightarrow>f 'b"} *}
+
+lemma permute_finfun_update[simp, eqvt]:
+  "(p \<bullet> (finfun_update f a b)) = finfun_update (p \<bullet> f) (p \<bullet> a) (p \<bullet> b)"
+unfolding finfun_update_def 
+unfolding permute_finfun_def
+apply(simp add: Abs_finfun_inverse fun_upd_finfun finfun_apply finfun_apply_inverse Rep_finfun_permute)
+apply(simp add: fun_upd_def)
+apply(perm_simp exclude: finfun_apply)
+apply(rule refl)
+done
+
+lemma permute_finfun_const[simp, eqvt]:
+  shows "(p \<bullet> (K$ b)) = (K$ (p \<bullet> b))"
+unfolding finfun_const_def 
+unfolding permute_finfun_def
+by (simp add: permute_finfun_def const_finfun finfun_apply_inverse Rep_finfun_permute Abs_finfun_inverse)
+
+
 
 section {* Supp, Freshness and Supports *}
 
@@ -2187,6 +2231,37 @@
   done
 
 
+subsection {* Type @{typ "'a \<Rightarrow>f 'b"} is finitely supported *}
+
+lemma fresh_finfun_const:
+  shows "a \<sharp> (K$ b) \<longleftrightarrow> a \<sharp> b"
+  by (simp add: fresh_def supp_def)
+
+lemma fresh_finfun_update:
+  shows "\<lbrakk>a \<sharp> f; a \<sharp> b; a \<sharp> x\<rbrakk> \<Longrightarrow> a \<sharp> f(b $:= x)"
+  unfolding fresh_conv_MOST
+  unfolding permute_finfun_update
+  by (elim MOST_rev_mp) (simp)
+
+lemma supp_finfun_const:
+  "supp (K$ b) = supp(b)"
+  by (simp add: supp_def)
+
+lemma supp_finfun_update:
+  "supp (f(a $:= b)) \<subseteq> supp(f, a, b)"
+using fresh_finfun_update
+by (auto simp add: fresh_def supp_Pair)
+    
+instance finfun :: (fs, fs) fs
+  apply(default)
+  apply(induct_tac x rule: finfun_weak_induct)
+  apply(simp add: supp_finfun_const finite_supp)
+  apply(rule finite_subset)
+  apply(rule supp_finfun_update)
+  apply(simp add: supp_Pair finite_supp)
+  done
+
+
 section {* Freshness and Fresh-Star *}
 
 lemma fresh_Unit_elim: