--- a/Nominal/Ex/Datatypes.thy	Thu Apr 28 11:51:01 2011 +0800
+++ b/Nominal/Ex/Datatypes.thy	Tue May 03 13:09:08 2011 +0100
@@ -67,7 +67,29 @@
 thm baz.fv_bn_eqvt
 thm baz.size_eqvt
 thm baz.supp
+
+(*
+  a nominal datatype with a set argument of
+  pure type
+*)
   
+nominal_datatype set_ty = 
+  Set_ty "nat set"
+| Fun "nat \<Rightarrow> nat"
+| Var "name"
+| Lam x::"name" t::"set_ty" bind x in t
+
+thm set_ty.distinct
+thm set_ty.induct
+thm set_ty.exhaust
+thm set_ty.strong_exhaust
+thm set_ty.fv_defs
+thm set_ty.bn_defs
+thm set_ty.perm_simps
+thm set_ty.eq_iff
+thm set_ty.fv_bn_eqvt
+thm set_ty.size_eqvt
+thm set_ty.supp
 
 end
 

--- a/Nominal/Ex/Lambda.thy	Thu Apr 28 11:51:01 2011 +0800
+++ b/Nominal/Ex/Lambda.thy	Tue May 03 13:09:08 2011 +0100
@@ -15,6 +15,13 @@
 where
   Var: "triv (Var x) n"
 
+lemma 
+  "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)"
+unfolding triv_def
+apply(perm_simp)
+oops
+(*apply(perm_simp)*)
+
 equivariance triv
 nominal_inductive triv avoids Var: "{}::name set"
 apply(auto simp add: fresh_star_def) 

--- a/Nominal/Nominal2_Base.thy	Thu Apr 28 11:51:01 2011 +0800
+++ b/Nominal/Nominal2_Base.thy	Tue May 03 13:09:08 2011 +0100
@@ -789,7 +789,6 @@
   unfolding permute_perm_def
   by (simp add: diff_minus minus_add add_assoc)
 
-
 subsubsection {* Equivariance of Logical Operators *}
 
 lemma eq_eqvt [eqvt]:
@@ -951,6 +950,12 @@
   unfolding Union_eq 
   by (perm_simp) (rule refl)
 
+lemma Inter_eqvt [eqvt]:
+  shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)"
+  unfolding Inter_eq 
+  by (perm_simp) (rule refl)
+
+
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
@@ -958,9 +963,78 @@
 unfolding UNION_eq_Union_image
 by (perm_simp) (rule refl)
 
+text {* 
+  In order to prove that lfp is equivariant we need two
+  auxiliary classes which specify that (op <=) and
+  Inf are equivariant. Instances for bool and fun are 
+  given.
+*}
+
+class le_eqvt =  order + 
+  assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{pt, order}))))"
+
+class inf_eqvt = complete_lattice +
+  assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::('a::{pt, Inf}) set))"
+
+instantiation bool :: le_eqvt
+begin
+
+instance 
+apply(default)
+unfolding le_bool_def
+apply(perm_simp)
+apply(rule refl)
+done
+
+end
+
+instantiation "fun" :: (pt, le_eqvt) le_eqvt
+begin
+
+instance 
+apply(default)
+unfolding le_fun_def
+apply(perm_simp)
+apply(rule refl)
+done 
+
+end
+
+instantiation bool :: inf_eqvt
+begin
+
+instance 
+apply(default)
+unfolding Inf_bool_def
+apply(perm_simp)
+apply(rule refl)
+done
+
+end
+
+instantiation "fun" :: (pt, inf_eqvt) inf_eqvt
+begin
+
+instance 
+apply(default)
+unfolding Inf_fun_def
+apply(perm_simp)
+apply(rule refl)
+done 
+
+end
+
+lemma lfp_eqvt [eqvt]:
+  fixes F::"('a \<Rightarrow> 'b) \<Rightarrow> ('a::pt \<Rightarrow> 'b::{inf_eqvt, le_eqvt})"
+  shows "p \<bullet> (lfp F) = lfp (p \<bullet> F)"
+unfolding lfp_def
+by (perm_simp) (rule refl)
+
 lemma finite_eqvt [eqvt]:
   shows "p \<bullet> finite A = finite (p \<bullet> A)"
-  unfolding permute_finite permute_bool_def ..
+unfolding finite_def
+by (perm_simp) (rule refl)
+
 
 subsubsection {* Equivariance for product operations *}