# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1339505776 -3600
# Node ID 264253617b5eda6a2861ccb715208e596d9391ed
# Parent  b3d97424b13096272233ca96df584b743b239088
improved the finfun parts

diff -r b3d97424b130 -r 264253617b5e Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Jun 12 01:23:52 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jun 12 13:56:16 2012 +0100
@@ -8,7 +8,7 @@
 imports Main 
         "~~/src/HOL/Library/Infinite_Set"
         "~~/src/HOL/Quotient_Examples/FSet"
-        "~~/src/HOL/Library/FinFun_Syntax"
+        "~~/src/HOL/Library/FinFun"
 keywords
   "atom_decl" "equivariance" :: thy_decl 
 uses ("nominal_basics.ML")
@@ -655,25 +655,28 @@
   by (lifting set_eqvt)
 
 
-subsection {* Permutations for @{typ "'a \<Rightarrow>f 'b"} (FinFuns) *}
+subsection {* Permutations for @{typ "('a, 'b) finfun"} *}
 
 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
+lift_definition
+  permute_finfun :: "perm \<Rightarrow> ('a, 'b) finfun \<Rightarrow> ('a, 'b) finfun"
+is
+  "permute :: perm \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
+  apply(simp add: permute_fun_comp)
+  apply(rule finfun_right_compose)
+  apply(rule finfun_left_compose)
+  apply(assumption)
+  apply(simp)
+  done
 
 instance
 apply(default)
-apply(simp_all add: permute_finfun_def finfun_apply_inverse Rep_finfun_permute Abs_finfun_inverse)
+apply(transfer)
+apply(simp)
+apply(transfer)
+apply(simp)
 done
 
 end
@@ -1125,6 +1128,11 @@
 unfolding finite_def
 by simp
 
+lemma fun_upd_eqvt[eqvt]:
+  shows "p \<bullet> (f(x := y)) = (p \<bullet> f)((p \<bullet> x) := (p \<bullet> y))"
+unfolding fun_upd_def
+by (simp)
+
 
 subsubsection {* Equivariance for product operations *}
 
@@ -1215,24 +1223,15 @@
   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)
-
+subsubsection {* Equivariance for @{typ "('a, 'b) finfun"} *}
+
+lemma permute_finfun_update[eqvt]:
+  shows "(p \<bullet> (finfun_update f a b)) = finfun_update (p \<bullet> f) (p \<bullet> a) (p \<bullet> b)"
+by (transfer) (simp)
+
+lemma permute_finfun_const[eqvt]:
+  shows "(p \<bullet> (finfun_const b)) = (finfun_const (p \<bullet> b))"
+by (transfer) (simp)
 
 
 section {* Supp, Freshness and Supports *}
@@ -2231,24 +2230,24 @@
   done
 
 
-subsection {* Type @{typ "'a \<Rightarrow>f 'b"} is finitely supported *}
+subsection {* Type @{typ "('a, 'b) finfun"} is finitely supported *}
 
 lemma fresh_finfun_const:
-  shows "a \<sharp> (K$ b) \<longleftrightarrow> a \<sharp> b"
+  shows "a \<sharp> (finfun_const 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)"
+  shows "\<lbrakk>a \<sharp> f; a \<sharp> x; a \<sharp> y\<rbrakk> \<Longrightarrow> a \<sharp> finfun_update f x y"
   unfolding fresh_conv_MOST
   unfolding permute_finfun_update
   by (elim MOST_rev_mp) (simp)
 
 lemma supp_finfun_const:
-  "supp (K$ b) = supp(b)"
+  shows "supp (finfun_const b) = supp(b)"
   by (simp add: supp_def)
 
 lemma supp_finfun_update:
-  "supp (f(a $:= b)) \<subseteq> supp(f, a, b)"
+  shows "supp (finfun_update f x y) \<subseteq> supp(f, x, y)"
 using fresh_finfun_update
 by (auto simp add: fresh_def supp_Pair)