959 end

   957 

   958 section {* support and freshness for applications *}

   959 

   960 lemma supp_fun_app:

   961   shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"

   962 proof (rule subsetCI)

   963   fix a::"atom"

   964   assume a: "a \<in> supp (f x)"

   965   assume b: "a \<notin> supp f \<union> supp x"

   966   then have "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}" "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" 

   967     unfolding supp_def by auto

   968   then have "finite ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})" by simp

   969   moreover 

   970   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})"

   971     by auto

   972   ultimately have "finite {b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x}"

   973     using finite_subset by auto

   974   then have "a \<notin> supp (f x)" unfolding supp_def

   975     by (simp add: permute_fun_app_eq)

   976   with a show "False" by simp

   977 qed

   978     

   979 lemma fresh_fun_app:

   980   shows "a \<sharp> (f, x) \<Longrightarrow> a \<sharp> f x"

   981 unfolding fresh_def

   982 using supp_fun_app

   983 by (auto simp add: supp_Pair)

   984 

   985 lemma fresh_fun_eqvt_app:

   986   assumes a: "\<forall>p. p \<bullet> f = f"

   987   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"

   988 proof -

   989   from a have b: "supp f = {}"

   990     unfolding supp_def by simp

   991   show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"

   992     unfolding fresh_def

   993     using supp_fun_app b

   994     by auto

   995 qed

   996 

   997 end