diff -r d29a8a6f3138 -r 75a95431cd8b Nominal/Nominal2_Base.thy
--- 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 *}