--- a/Quot/Nominal/Abs.thy	Thu Jan 28 23:47:02 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Fri Jan 29 00:22:00 2010 +0100
@@ -1,4 +1,4 @@
-theory LamEx
+theory Abs
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" 
 begin
 
@@ -322,5 +322,5 @@
 apply(lifting alpha_abs.simps(1))
 done
 
-done
+end
 

--- a/Quot/Nominal/LamEx.thy	Thu Jan 28 23:47:02 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Fri Jan 29 00:22:00 2010 +0100
@@ -1,5 +1,5 @@
 theory LamEx
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" 
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
 begin
 
 
@@ -153,9 +153,17 @@
 where
   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
-| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b)
+| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)
        \<Longrightarrow> rLam a t \<approx> rLam b s"
 
+lemma a3_inverse:
+  assumes "rLam a t \<approx> rLam b s"
+  shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)"
+using assms
+apply(erule_tac alpha.cases)
+apply(auto)
+done
+
 text {* should be automatic with new version of eqvt-machinery *}
 lemma alpha_eqvt:
   shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
@@ -174,9 +182,6 @@
 apply(rule conjI)
 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
 apply(simp add: eqvts atom_eqvt)
-apply(rule conjI)
-apply(subst permute_eqvt[symmetric])
-apply(simp)
 apply(subst permute_eqvt[symmetric])
 apply(simp)
 done
@@ -201,13 +206,10 @@
 apply(rule_tac x="- pi" in exI)
 apply(simp)
 apply(simp add: fresh_star_def fresh_minus_perm)
-apply(rule conjI)
 apply(erule conjE)+
 apply(rotate_tac 3)
 apply(drule_tac pi="- pi" in alpha_eqvt)
 apply(simp)
-apply(clarify)
-apply(simp)
 done
 
 lemma alpha_trans:
@@ -231,10 +233,10 @@
 apply(simp add: fresh_star_plus)
 apply(drule_tac x="- pia \<bullet> sa" in spec)
 apply(drule mp)
-apply(rotate_tac 8)
+apply(rotate_tac 7)
 apply(drule_tac pi="- pia" in alpha_eqvt)
 apply(simp)
-apply(rotate_tac 11)
+apply(rotate_tac 9)
 apply(drule_tac pi="pia" in alpha_eqvt)
 apply(simp)
 done
@@ -330,12 +332,7 @@
 apply(simp)
 apply(drule sym)
 apply(simp)
-apply(case_tac "a = pi \<bullet> a")
-apply(simp)
-defer
-apply(simp)
-apply(simp add: fresh_star_def)
-sorry
+oops
 
 quotient_type lam = rlam / alpha
   by (rule alpha_equivp)
@@ -440,16 +437,23 @@
   by  (lifting a2)
 
 lemma a3: 
-  "\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s \<and> (pi \<bullet> a) = b)\<rbrakk> 
+  "\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)\<rbrakk> 
    \<Longrightarrow> Lam a t = Lam b s"
   apply  (lifting a3)
   done
 
+lemma a3_inv:
+  assumes "Lam a t = Lam b s"
+  shows "\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)"
+using assms
+apply(lifting a3_inverse)
+done
+
 lemma alpha_cases: 
   "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
     \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
     \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s; 
-         \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk> 
+         \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s\<rbrakk> 
    \<Longrightarrow> P\<rbrakk>
     \<Longrightarrow> P"
   by (lifting alpha.cases)
@@ -460,7 +464,7 @@
     \<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);
      \<And>t a s b.
         \<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and>
-         (fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s) \<and> pi \<bullet> a = b\<rbrakk> 
+         (fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s)\<rbrakk> 
      \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
     \<Longrightarrow> qxb qx qxa"
   by (lifting alpha.induct)
@@ -486,6 +490,16 @@
 apply(simp_all)
 done
 
+lemma Lam_pseudo_inject:
+  shows "(Lam a t = Lam b s) = 
+      (\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s))"
+apply(rule iffI)
+apply(rule a3_inv)
+apply(assumption)
+apply(rule a3)
+apply(assumption)
+done
+
 lemma rlam_distinct:
   shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')"
   and   "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)"
@@ -560,42 +574,18 @@
 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"
+lemma lam_supp2:
+  shows "supp (Lam x t) = supp (Abs {atom x} t)"
+apply(simp add: supp_def permute_set_eq atom_eqvt)
+apply(simp add: Lam_pseudo_inject)
+apply(simp add: abs_eq)
 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
+apply(simp add: lam_supp2)
+apply(simp add: supp_Abs)
+done
 
 lemma fresh_lam:
   "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)"