--- a/Nominal/Ex/Lambda.thy	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/Ex/Lambda.thy	Thu Jul 09 02:32:46 2015 +0100
@@ -12,6 +12,16 @@
 
 atom_decl name
 
+thm obtain_atom
+
+lemma 
+ "(\<forall>thesis. (finite X \<longrightarrow> (\<forall>a. ((a \<notin> X \<and> sort_of a = s) \<longrightarrow> thesis)) \<longrightarrow> thesis)) \<longleftrightarrow>
+  (finite X \<longrightarrow> (\<exists> a. (a \<notin> X \<and> sort_of a = s)))"
+apply(auto) 
+done
+
+
+
 ML {* trace := true *}
 
 nominal_datatype lam =
@@ -19,6 +29,24 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
+nominal_datatype environment = 
+   Ni
+ | En name closure environment
+and closure = 
+   Clos "lam" "environment"
+
+thm environment_closure.exhaust(1)
+
+nominal_function 
+  env_lookup :: "environment => name => closure"
+where
+  "env_lookup Ni x = Clos (Var x) Ni"
+| "env_lookup (En v clos rest) x = (if (v = x) then clos else env_lookup rest x)"
+   apply (auto)
+   apply (simp add: env_lookup_graph_aux_def eqvt_def)
+   by (metis environment_closure.strong_exhaust(1))
+
+
 lemma 
   "Lam [x]. Var x = Lam [y]. Var y"
 proof -
@@ -232,6 +260,16 @@
 
 section {* free name function *}
 
+
+lemma fresh_removeAll_name:
+  fixes x::"name"
+    and xs:: "name list"
+  shows "atom x \<sharp> (removeAll y xs) \<longleftrightarrow> (atom x \<sharp> xs \<or> x = y)"
+  apply (induct xs)
+  apply(auto simp add: fresh_def supp_Nil supp_Cons supp_at_base)
+  done
+
+
 text {* first returns an atom list *}
 
 nominal_function