diff -r 1d67ab20f358 -r 9174c7afd8b8 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Fri May 02 18:01:02 2008 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Fri May 02 18:42:17 2008 +0200
@@ -51,6 +51,20 @@
   by (nominal_induct t avoiding: x rule: lam.induct)
      (simp_all add: fresh_atm)
 
+lemma lookup_fresh:
+  fixes z::"name"
+  assumes "z\<sharp>\<theta>" "z\<sharp>x"
+  shows "z\<sharp> lookup \<theta> x"
+using assms 
+by (induct rule: lookup.induct) (auto simp add: fresh_list_cons)
+
+lemma lookup_fresh':
+  assumes "z\<sharp>\<theta>"
+  shows "lookup \<theta> z = Var z"
+using assms 
+by (induct rule: lookup.induct)
+   (auto simp add: fresh_list_cons fresh_prod fresh_atm)
+
 lemma psubst_subst:
   assumes h:"c\<sharp>\<theta>"
   shows "(\<theta><t>)[c::=s] = ((c,s)#\<theta>)<t>"