--- a/Quot/Nominal/LamEx.thy	Thu Jan 28 14:20:26 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Thu Jan 28 15:47:35 2010 +0100
@@ -47,7 +47,18 @@
 unfolding fresh_star_def
 by (simp add: fresh_plus)
 
-
+lemma supp_finite_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "supp S = S"
+  apply(rule finite_supp_unique)
+  apply(simp add: supports_def)
+  apply(auto simp add: permute_set_eq swap_atom)[1]
+  apply(metis)
+  apply(rule assms)
+  apply(auto simp add: permute_set_eq swap_atom)[1]
+done
+  
 
 atom_decl name
 
@@ -244,9 +255,30 @@
 inductive
     alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
 where
-  a1: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)"
-| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2"
-| a3: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s"
+  a21: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)"
+| a22: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2"
+| a23: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s"
+
+lemma fv_vars:
+  fixes a::name
+  assumes a1: "\<forall>x \<in> rfv t - {atom a}. pi \<bullet> x = x"
+  shows "(pi \<bullet> t) \<approx>2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)"
+using a1
+apply(induct t)
+apply(auto)
+apply(rule a21)
+apply(case_tac "name = a")
+apply(simp)
+apply(simp)
+defer
+apply(rule a22)
+apply(simp)
+apply(simp)
+apply(rule a23)
+apply(case_tac "a = name")
+apply(simp)
+oops
+
 
 lemma 
   assumes a1: "t \<approx>2 s"
@@ -272,9 +304,11 @@
 apply(drule alpha_rfv)
 apply(drule sym)
 apply(simp)
+apply(simp add: rfv_eqvt[symmetric])
 defer
 apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})")
 apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})")
+
 defer
 sorry
 
@@ -300,6 +334,7 @@
 apply(simp)
 defer
 apply(simp)
+apply(simp add: fresh_star_def)
 sorry
 
 quotient_type lam = rlam / alpha