--- a/Quot/Nominal/LamEx.thy	Wed Jan 27 18:06:14 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Thu Jan 28 01:24:09 2010 +0100
@@ -243,13 +243,6 @@
 apply(simp)
 done
 
-(* PROBABLY NOT TRUE !!! needed for lifting 
-lemma alpha_fresh:
-  assumes a: "t \<approx> s"
-  shows "a\<sharp>t \<Longrightarrow> a\<sharp>s"
-using a
-apply(induct)
-*)
 
 quotient_type lam = rlam / alpha
   by (rule alpha_equivp)
@@ -305,13 +298,6 @@
 done
 
 
-
-(* NOT SURE see above
-lemma fresh_rsp:
-  "(op = ===> alpha ===> op =) fresh fresh"
-  apply(auto)
-*)
-
 section {* lifted theorems *}
 
 lemma lam_induct:
@@ -375,6 +361,7 @@
     \<Longrightarrow> P"
   by (lifting alpha.cases)
 
+(* not sure whether needed *)
 lemma alpha_induct: 
   "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
     \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
@@ -450,20 +437,69 @@
 done
 
 (* needs thinking *)
-lemma lam_supp:
-  shows "supp (Lam x t) = ((supp t) - {atom x})"
-apply(simp add: supp_def)
-sorry
+lemma lam_supp1:
+  shows "(supp (atom x, t)) supports (Lam x t) "
+apply(simp add: supports_def)
+apply(fold fresh_def)
+apply(simp add: fresh_Pair swap_fresh_fresh)
+apply(clarify)
+apply(subst swap_at_base_simps(3))
+apply(simp_all add: fresh_atom)
+done
 
+lemma lam_fsupp1:
+  assumes a: "finite (supp t)"
+  shows "finite (supp (Lam x t))"
+apply(rule supports_finite)
+apply(rule lam_supp1)
+apply(simp add: a supp_Pair supp_atom)
+done
 
 instance lam :: fs
 apply(default)
 apply(induct_tac x rule: lam_induct)
 apply(simp add: var_supp)
 apply(simp add: app_supp)
-apply(simp add: lam_supp)
+apply(simp add: lam_fsupp1)
 done
 
+lemma lam_fresh1:
+  assumes f: "finite (supp t)"
+  and a1: "b \<sharp> t" 
+  and a2: "atom a \<noteq> b"
+  shows "b \<sharp> Lam a t"
+  proof -
+    have "\<exists>c. c \<sharp> (b, a ,t, Lam a t)" sorry
+    then obtain c where fr1: "c \<noteq> b"
+                  and   fr2: "c \<noteq> atom a"
+                  and   fr3: "c \<sharp> t"
+                  and   fr4: "c \<sharp> Lam a t"
+                  and   fr5: "sort_of b = sort_of c"  
+                  apply(auto simp add: fresh_Pair fresh_atom)
+                  sorry
+    have e: "(c \<rightleftharpoons> b) \<bullet> (Lam a t) = Lam a ((c \<rightleftharpoons> b) \<bullet> t)" using a2 fr1 fr2
+      by simp
+    from fr4 have "((c \<rightleftharpoons> b) \<bullet>c) \<sharp> ((c \<rightleftharpoons> b) \<bullet>(Lam a t))"
+      by (simp only: fresh_permute_iff)
+    then have "b \<sharp> (Lam a ((c \<rightleftharpoons> b) \<bullet> t))" using fr1 fr2 fr5 e
+      by simp
+    then show ?thesis using a1 fr3 
+      by (simp only: swap_fresh_fresh)
+qed
+
+lemma lam_fresh2:
+  assumes f: "finite (supp t)"
+  shows "(atom a) \<sharp> Lam a t"
+sorry
+
+
+lemma lam_supp:
+  shows "supp (Lam x t) = ((supp t) - {atom x})"
+apply(default)
+apply(simp_all add: supp_conv_fresh)
+apply(auto)
+sorry
+
 lemma fresh_lam:
   "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)"
 apply(simp add: fresh_def)