# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265035585 -3600
# Node ID 6f2bbe35987a7e82daf95251bacad19d4dfada50
# Parent  2ebfbd8618465d89e8d15f30c310defa79eeb7a1# Parent  7c633507a809b9fd9f60e59a47c74c2e6c9adbfb
merge

diff -r 2ebfbd861846 -r 6f2bbe35987a Quot/Nominal/Nominal2_Base.thy
--- a/Quot/Nominal/Nominal2_Base.thy	Mon Feb 01 15:45:40 2010 +0100
+++ b/Quot/Nominal/Nominal2_Base.thy	Mon Feb 01 15:46:25 2010 +0100
@@ -461,7 +461,6 @@
 
 end
 
-
 subsection {* Permutations for sums *}
 
 instantiation "+" :: (pt, pt) pt
@@ -883,7 +882,6 @@
 apply (simp add: supp_Pair finite_supp)
 done
 
-
 subsection {* Type @{typ "'a + 'b"} is finitely supported *}
 
 lemma supp_Inl: 
@@ -956,4 +954,44 @@
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
 
+
+section {* support and freshness for applications *}
+
+lemma supp_fun_app:
+  shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
+proof (rule subsetCI)
+  fix a::"atom"
+  assume a: "a \<in> supp (f x)"
+  assume b: "a \<notin> supp f \<union> supp x"
+  then have "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}" "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" 
+    unfolding supp_def by auto
+  then have "finite ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})" by simp
+  moreover 
+  have "{b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x} \<subseteq> ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})"
+    by auto
+  ultimately have "finite {b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x}"
+    using finite_subset by auto
+  then have "a \<notin> supp (f x)" unfolding supp_def
+    by (simp add: permute_fun_app_eq)
+  with a show "False" by simp
+qed
+    
+lemma fresh_fun_app:
+  shows "a \<sharp> (f, x) \<Longrightarrow> a \<sharp> f x"
+unfolding fresh_def
+using supp_fun_app
+by (auto simp add: supp_Pair)
+
+lemma fresh_fun_eqvt_app:
+  assumes a: "\<forall>p. p \<bullet> f = f"
+  shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
+proof -
+  from a have b: "supp f = {}"
+    unfolding supp_def by simp
+  show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
+    unfolding fresh_def
+    using supp_fun_app b
+    by auto
+qed
+
 end