# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295462510 -3600
# Node ID 1df873b63cb2bec64e99340a972d1cc2b266679b
# Parent  d72a7168f1cb714d3c525dae0026e64352d56ad4
added obtain_fresh lemma; tuned Lambda.thy

diff -r d72a7168f1cb -r 1df873b63cb2 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jan 19 19:06:52 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jan 19 19:41:50 2011 +0100
@@ -213,7 +213,7 @@
   assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"
   shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]"
 proof -
-  obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" sorry
+  obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" by (rule obtain_fresh)
   have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs
     by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
   also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt)
@@ -223,8 +223,6 @@
 
 
 
-
-
 section {* Locally Nameless Terms *}
 
 nominal_datatype ln = 
@@ -250,7 +248,7 @@
 where
   "trans (Var x) xs = lookup xs 0 x"
 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
-| "atom x \<sharp> xs \<Longrightarrow> trans (Lam x t) xs = LNLam (trans t (x # xs))"
+| "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
diff -r d72a7168f1cb -r 1df873b63cb2 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Wed Jan 19 19:06:52 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Jan 19 19:41:50 2011 +0100
@@ -2228,6 +2228,17 @@
   thus ?thesis ..
 qed
 
+lemma obtain_fresh':
+  assumes fin: "finite (supp x)"
+  obtains a::"'a::at_base" where "atom a \<sharp> x"
+using obtain_at_base[where X="supp x"]
+by (auto simp add: fresh_def fin)
+
+lemma obtain_fresh:
+  fixes x::"'b::fs"
+  obtains a::"'a::at_base" where "atom a \<sharp> x"
+  by (rule obtain_fresh') (auto simp add: finite_supp)
+
 lemma supp_finite_set_at_base:
   assumes a: "finite S"
   shows "supp S = atom ` S"
@@ -2539,10 +2550,7 @@
   assumes P: "finite (supp P)"
   shows "(FRESH x. f (P x)) = f (FRESH x. P x)"
 proof -
-  obtain a::'a where "atom a \<notin> supp P"
-    using P by (rule obtain_at_base)
-  hence "atom a \<sharp> P"
-    by (simp add: fresh_def)
+  obtain a::'a where "atom a \<sharp> P" using P by (rule obtain_fresh')
   show "(FRESH x. f (P x)) = f (FRESH x. P x)"
     apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh])
     apply (cut_tac `atom a \<sharp> P`)
@@ -2562,11 +2570,9 @@
   and     Q: "finite (supp Q)"
   shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"
 proof -
-  from assms have "finite (supp P \<union> supp Q)" by simp
-  then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"
-    by (rule obtain_at_base)
-  hence "atom a \<sharp> P" and "atom a \<sharp> Q"
-    by (simp_all add: fresh_def)
+  from assms have "finite (supp (P, Q))" by (simp add: supp_Pair)
+  then obtain a::'a where "atom a \<sharp> (P, Q)" by (rule obtain_fresh') 
+  then have "atom a \<sharp> P" and "atom a \<sharp> Q" by (simp_all add: fresh_Pair)
   show ?thesis
     apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh])
     apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)