# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265094994 -3600
# Node ID d7b8c4243cd64eefaff46a307d68adc4d2c66c4b
# Parent  2fe45593aaa9b8602e6379bb1c93c59ed318a45d
Lam2 finished apart from Rep_eqvt.

diff -r 2fe45593aaa9 -r d7b8c4243cd6 Quot/Nominal/LamEx2.thy
--- a/Quot/Nominal/LamEx2.thy	Mon Feb 01 20:02:44 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Tue Feb 02 08:16:34 2010 +0100
@@ -407,7 +407,8 @@
 apply auto
 done
 
-lemma pi_rep: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)"
+(* pi_abs would be also sufficient to prove the next lemma *)
+lemma replam_eqvt: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)"
 apply (unfold rep_lam_def)
 sorry
 
@@ -416,45 +417,42 @@
            alpha_gen = alpha_gen"
 apply (simp add: expand_fun_eq)
 apply (simp add: alpha_gen.simps)
-apply (simp add: pi_rep)
+apply (simp add: replam_eqvt)
 apply (simp only: Quotient_abs_rep[OF Quotient_lam])
 apply auto
 done
 
 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)"
 apply (simp add: expand_fun_eq)
-sorry
-
+apply (simp add: Quotient_rel_rep[OF Quotient_lam])
+done
 
 lemma a3:
   "\<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s) \<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
+  "Lam a t = Lam b s \<Longrightarrow> \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)"
 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\<rbrakk> 
+    \<And>a t b s. \<lbrakk>a1 = Lam a t; a2 = Lam b s; \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)\<rbrakk>
    \<Longrightarrow> P\<rbrakk>
     \<Longrightarrow> P"
   by (lifting alpha.cases)
 
+thm alpha.induct
+
 (* 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);
-     \<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)\<rbrakk> 
-     \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
+ \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2 fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
     \<Longrightarrow> qxb qx qxa"
   by (lifting alpha.induct)
 
@@ -479,9 +477,9 @@
 apply(simp_all)
 done
 
+thm a3_inv
 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))"
+  shows "(Lam a t = Lam b s) = (\<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s))"
 apply(rule iffI)
 apply(rule a3_inv)
 apply(assumption)
@@ -568,25 +566,27 @@
 apply(induct t rule: lam_induct)
 apply(simp add: var_supp)
 apply(simp add: app_supp)
-apply(subgoal_tac "supp (Lam name lam) = supp (Abst {atom name} lam)")
-apply(simp add: supp_Abst)
+apply(subgoal_tac "supp (Lam name lam) = supp (Abs {atom name} lam)")
+apply(simp add: supp_Abs)
 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
 apply(simp add: Lam_pseudo_inject)
-apply(simp add: abs_eq alpha_gen)
+apply(simp add: Abs_eq_iff)
+apply(simp add: alpha_gen.simps)
 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
 done
 
 lemma lam_supp2:
-  shows "supp (Lam x t) = supp (Abst {atom x} t)"
+  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 supp_fv alpha_gen)
+apply(simp add: Abs_eq_iff)
+apply(simp add: alpha_gen  supp_fv)
 done
 
 lemma lam_supp:
   shows "supp (Lam x t) = ((supp t) - {atom x})"
 apply(simp add: lam_supp2)
-apply(simp add: supp_Abst)
+apply(simp add: supp_Abs)
 done
 
 lemma fresh_lam: