# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1296098657 -3600
# Node ID 5964c84ece5d7a6bfcc0ce35532af2444b512671
# Parent  747ebf2f066dd4aa7efde0e452f6c97b7d6b8004
the proofs with eqvt_at

diff -r 747ebf2f066d -r 5964c84ece5d Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Jan 25 18:58:26 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Thu Jan 27 04:24:17 2011 +0100
@@ -1361,6 +1361,20 @@
   apply(rule THE_defaultI'[OF unique])
   done
 
+lemma fundef_ex1_eqvt2:
+  fixes x::"'a::pt"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes eqvt: "eqvt_at G x"
+  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_at_def
+  apply(simp)
+  done
+
 lemma fundef_ex1_eqvt:
   fixes x::"'a::pt"
   assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
@@ -1375,6 +1389,16 @@
   apply(simp add: permute_fun_app_eq)
   done
 
+lemma fundef_ex1_eqvt_at2:
+  fixes x::"'a::pt"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes eqvt: "eqvt_at G x"
+  assumes ex1: "\<exists>!y. G x y"
+  shows "eqvt_at f x"
+  unfolding eqvt_at_def
+  using assms
+  by (auto intro: fundef_ex1_eqvt2)
+
 lemma fundef_ex1_eqvt_at:
   fixes x::"'a::pt"
   assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
@@ -1385,7 +1409,6 @@
   using assms
   by (auto intro: fundef_ex1_eqvt)
 
-
 section {* Support of Finite Sets of Finitely Supported Elements *}
 
 text {* support and freshness for atom sets *}