# HG changeset patch
# User urbanc
# Date 1176698722 -7200
# Node ID ca804eb70d3940ed5e3336edf309925d76ddc1e5
# Parent  3ea6c1cb3dab16e70cb463c7937516c2159ec75d
added a more usuable lemma for dealing with fresh_fun

diff -r 3ea6c1cb3dab -r ca804eb70d39 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Apr 16 04:02:15 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Apr 16 06:45:22 2007 +0200
@@ -2483,6 +2483,18 @@
   with b show "fr = h a" by force
 qed
 
+lemma fresh_fun_app':
+  fixes h :: "'x\<Rightarrow>'a"
+  and   a :: "'x"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)" 
+  and     f1: "finite ((supp h)::'x set)"
+  and     a: "a\<sharp>h" "a\<sharp>h a"
+  shows "(fresh_fun h) = (h a)"
+apply(rule fresh_fun_app[OF pt, OF at, OF f1])
+apply(auto simp add: fresh_prod intro: a)
+done
+
 lemma fresh_fun_equiv_ineq:
   fixes h :: "'y\<Rightarrow>'a"
   and   pi:: "'x prm"