--- a/Nominal/Ex/LamTest.thy	Fri Jan 07 05:06:25 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Fri Jan 07 05:40:31 2011 +0000
@@ -17,10 +17,11 @@
 apply(auto simp add: eqvt_def)
 done
 
+term THE_default
 
 lemma the_default_eqvt:
   assumes unique: "\<exists>!x. P x"
-  shows "(p \<bullet> (THE_default d P)) = (THE_default (p \<bullet> d) (p \<bullet> P))"
+  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(perm_simp add: permute_minus_cancel)
@@ -30,6 +31,21 @@
   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 ex1: "\<exists>!y. G x y"
+  assumes eqvt: "eqvt G"
+  shows "(p \<bullet> (f x)) = f (p \<bullet> x)"
+  apply (simp only: f_def)
+  apply(subst the_default_eqvt)
+  apply (rule ex1)
+  apply(perm_simp)
+  using eqvt
+  apply(simp add: eqvt_def)
+  done
+
+
 
 ML {*