--- a/Nominal/Nominal2_Base.thy	Mon Jan 17 12:33:37 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Jan 17 12:34:11 2011 +0000
@@ -415,6 +415,7 @@
   shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)"
   unfolding permute_fun_def by simp
 
+
 subsection {* Permutations for booleans *}
 
 instantiation bool :: pt
@@ -451,6 +452,16 @@
   unfolding permute_fun_def permute_bool_def
   by (auto, drule_tac x="p \<bullet> x" in spec, simp)
 
+lemma ex1_eqvt:
+  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+  unfolding Ex1_def
+  apply(simp add: ex_eqvt)
+  unfolding permute_fun_def 
+  apply(simp add: conj_eqvt all_eqvt)
+  unfolding permute_fun_def
+  apply(simp add: imp_eqvt permute_bool_def)
+  done
+
 lemma permute_boolE:
   fixes P::"bool"
   shows "p \<bullet> P \<Longrightarrow> P"
@@ -718,7 +729,6 @@
 instance int :: pure
 proof qed (rule permute_int_def)
 
-
 subsection {* Supp, Freshness and Supports *}
 
 context pt
@@ -1233,16 +1243,26 @@
   unfolding fresh_def
   by auto
 
-text {* Support of Equivariant Functions *}
+text {* Equivariant Functions *}
+
+definition
+  "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
+
+lemma eqvtI:
+  shows "(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f"
+unfolding eqvt_def
+by simp
 
 lemma supp_fun_eqvt:
-  assumes a: "\<And>p. p \<bullet> f = f"
+  assumes a: "eqvt f"
   shows "supp f = {}"
+  using a
+  unfolding eqvt_def
   unfolding supp_def 
-  using a by simp
+  by simp
 
 lemma fresh_fun_eqvt_app:
-  assumes a: "\<And>p. p \<bullet> f = f"
+  assumes a: "eqvt f"
   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
 proof -
   from a have "supp f = {}" by (simp add: supp_fun_eqvt)
@@ -1251,6 +1271,81 @@
     using supp_fun_app by auto
 qed
 
+text {* equivariance of a function at a given argument *}
+definition
+ "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
+
+lemma supp_eqvt_at:
+  assumes asm: "eqvt_at f x"
+  and     fin: "finite (supp x)"
+  shows "supp (f x) \<subseteq> supp x"
+apply(rule supp_is_subset)
+unfolding supports_def
+unfolding fresh_def[symmetric]
+using asm
+apply(simp add: eqvt_at_def)
+apply(simp add: swap_fresh_fresh)
+apply(rule fin)
+done
+
+lemma finite_supp_eqvt_at:
+  assumes asm: "eqvt_at f x"
+  and     fin: "finite (supp x)"
+  shows "finite (supp (f x))"
+apply(rule finite_subset)
+apply(rule supp_eqvt_at[OF asm fin])
+apply(rule fin)
+done
+
+lemma fresh_eqvt_at:
+  assumes asm: "eqvt_at f x"
+  and     fin: "finite (supp x)"
+  and     fresh: "a \<sharp> x"
+  shows "a \<sharp> f x"
+using fresh
+unfolding fresh_def
+using supp_eqvt_at[OF asm fin]
+by auto
+
+text {* helper functions for nominal_functions *}
+
+lemma the_default_eqvt:
+  assumes unique: "\<exists>!x. P x"
+  shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))"
+  apply(rule THE_default1_equality [symmetric])
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(simp add: ex1_eqvt)
+  apply(rule unique)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(rule subst[OF permute_fun_app_eq])
+  apply(simp)
+  apply(rule THE_defaultI'[OF unique])
+  done
+
+lemma fundef_ex1_eqvt:
+  fixes x::"'a::pt"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes eqvt: "eqvt G"
+  assumes ex1: "\<exists>!y. G x y"
+  shows "(p \<bullet> (f x)) = f (p \<bullet> x)"
+  apply(simp only: f_def)
+  apply(subst the_default_eqvt)
+  apply(rule ex1)
+  using eqvt
+  unfolding eqvt_def
+  apply(simp add: permute_fun_app_eq)
+  done
+
+lemma fundef_ex1_eqvt_at:
+  fixes x::"'a::pt"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes eqvt: "eqvt G"
+  assumes ex1: "\<exists>!y. G x y"
+  shows "eqvt_at f x"
+  unfolding eqvt_at_def
+  using assms
+  by (auto intro: fundef_ex1_eqvt)
+
 
 section {* Support of Finite Sets of Finitely Supported Elements *}
 
@@ -1274,15 +1369,23 @@
   unfolding fresh_def
   by (simp add: supp_finite_atom_set[OF assms])
 
-
 lemma Union_fresh:
   shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
   unfolding Union_image_eq[symmetric]
   apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
-  apply(simp add: permute_fun_def UNION_def Collect_def Bex_def ex_eqvt mem_def conj_eqvt)
-  apply(subst permute_fun_app_eq)
-  back
-  apply(simp add: supp_eqvt)
+  unfolding eqvt_def
+  unfolding permute_fun_def
+  apply(simp)
+  unfolding UNION_def 
+  unfolding Collect_def 
+  unfolding Bex_def 
+  apply(simp add: ex_eqvt)
+  unfolding permute_fun_def
+  apply(simp add: conj_eqvt)
+  apply(simp add: mem_eqvt)
+  apply(simp add: supp_eqvt) 
+  unfolding permute_fun_def
+  apply(simp)
   apply(assumption)
   done
 
@@ -1547,7 +1650,7 @@
   by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
 
 lemma fresh_star_eqvt:
-  shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
+  shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)"
 unfolding fresh_star_def
 unfolding Ball_def
 apply(simp add: all_eqvt)