--- 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)