# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265112646 -3600
# Node ID 163d6917af629721c640fcac4a7295eb71e2549c
# Parent  278253330b6ad3b55a7ac3cc9ef8fa14f26fb0a7
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.

diff -r 278253330b6a -r 163d6917af62 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Tue Feb 02 12:48:12 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Tue Feb 02 13:10:46 2010 +0100
@@ -80,50 +80,25 @@
 and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 where
   a1: "(Type) \<approx>ki (Type)"
-| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"
+| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
 | a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
-| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"
+| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>ty (TPi A' b B')"
 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
-| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"
-
-(*
-function(sequential)
-    akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
-and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
-and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
-where
-  a1: "(Type) \<approx>ki (Type) = True"
-| a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
-| "_ \<approx>ki _ = False"
-| a3: "(TConst i) \<approx>ty (TConst j) = (i = j)"
-| a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
-| a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
-| "_ \<approx>ty _ = False"
-| a6: "(Const i) \<approx>tr (Const j) = (i = j)"
-| a7: "(Var x) \<approx>tr (Var y) = (x = y)"
-| a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
-| a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
-| "_ \<approx>tr _ = False"
-apply (pat_completeness)
-apply simp_all
-done
-termination
-by (size_change)
-*)
+| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
 
 lemma akind_aty_atrm_inj:
   "(Type) \<approx>ki (Type) = True"
-  "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
+  "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K')))"
   "(TConst i) \<approx>ty (TConst j) = (i = j)"
   "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
-  "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
+  "((TPi A a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))))"
   "(Const i) \<approx>tr (Const j) = (i = j)"
   "(Var x) \<approx>tr (Var y) = (x = y)"
   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
-  "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
+  "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))))"
 apply -
 apply (simp add: akind_aty_atrm.intros)
 
@@ -167,45 +142,16 @@
   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
 apply(induct rule: akind_aty_atrm.inducts)
 apply (simp_all add: akind_aty_atrm.intros)
-apply(rule a2)
-apply simp
-apply(erule conjE)
-apply(erule exE)
-apply(erule conjE)
-apply(rule_tac x="pi \<bullet> pia" in exI)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(simp add: permute_eqvt[symmetric])
-apply(rule a5)
-apply simp
-apply(erule conjE)
-apply(erule exE)
-apply(erule conjE)
-apply(rule_tac x="pi \<bullet> pia" in exI)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(simp add: permute_eqvt[symmetric])
-apply(rule a9)
-apply simp
-apply(erule conjE)
-apply(erule exE)
-apply(erule conjE)
-apply(rule_tac x="pi \<bullet> pia" in exI)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
-apply(simp add: permute_eqvt[symmetric])
+apply (simp_all add: akind_aty_atrm_inj)
+apply (rule alpha_gen_atom_eqvt)
+apply (simp add: rfv_eqvt)
+apply assumption
+apply (rule alpha_gen_atom_eqvt)
+apply (simp add: rfv_eqvt)
+apply assumption
+apply (rule alpha_gen_atom_eqvt)
+apply (simp add: rfv_eqvt)
+apply assumption
 done
 
 lemma al_refl:
@@ -220,22 +166,85 @@
   apply (rule a2)
   apply auto
   apply(rule_tac x="0" in exI)
-  apply(simp_all add: fresh_star_def fresh_zero_perm)
+  apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
   apply (rule a5)
   apply auto
   apply(rule_tac x="0" in exI)
-  apply(simp_all add: fresh_star_def fresh_zero_perm)
+  apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
   apply (rule a9)
   apply auto
   apply(rule_tac x="0" in exI)
-  apply(simp_all add: fresh_star_def fresh_zero_perm)
+  apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
+  done
+
+lemma al_sym:
+  fixes K K'::"kind" and A A'::"ty" and M M'::"trm"
+  shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
+  and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A"
+  and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"
+  apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts)
+  apply(simp_all add: akind_aty_atrm.intros)
+  apply (simp_all add: akind_aty_atrm_inj)
+  apply(rule alpha_gen_atom_sym)
+  apply(rule alpha_eqvt)
+  apply(assumption)+
+  apply(rule alpha_gen_atom_sym)
+  apply(rule alpha_eqvt)
+  apply(assumption)+
+  apply(rule alpha_gen_atom_sym)
+  apply(rule alpha_eqvt)
+  apply(assumption)+
+  done
+
+lemma al_trans:
+  fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm"
+  shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
+  and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''"
+  and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"
+  apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: akind_aty_atrm.inducts)
+  apply(simp_all add: akind_aty_atrm.intros)
+  apply(erule akind.cases)
+  apply(simp_all add: akind_aty_atrm.intros)
+  apply(simp add: akind_aty_atrm_inj)
+  apply(rule alpha_gen_atom_trans)
+  apply(rule alpha_eqvt)
+  apply(assumption)+
+  apply(rotate_tac 4)
+  apply(erule aty.cases)
+  apply(simp_all add: akind_aty_atrm.intros)
+  apply(rotate_tac 3)
+  apply(erule aty.cases)
+  apply(simp_all add: akind_aty_atrm.intros)
+  apply(simp add: akind_aty_atrm_inj)
+  apply(rule alpha_gen_atom_trans)
+  apply(rule alpha_eqvt)
+  apply(assumption)+
+  apply(rotate_tac 4)
+  apply(erule atrm.cases)
+  apply(simp_all add: akind_aty_atrm.intros)
+  apply(rotate_tac 3)
+  apply(erule atrm.cases)
+  apply(simp_all add: akind_aty_atrm.intros)
+  apply(simp add: akind_aty_atrm_inj)
+  apply(rule alpha_gen_atom_trans)
+  apply(rule alpha_eqvt)
+  apply(assumption)+
   done
 
 lemma alpha_equivps:
   shows "equivp akind"
   and   "equivp aty"
   and   "equivp atrm"
-sorry
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto intro: al_refl al_sym al_trans)
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto intro: al_refl al_sym al_trans)
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto intro: al_refl al_sym al_trans)
+  done
 
 quotient_type KIND = kind / akind
   by (rule alpha_equivps)
@@ -312,7 +321,7 @@
      (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
      (t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
   apply(rule akind_aty_atrm.induct)
-  apply(simp_all)
+  apply(simp_all add: alpha_gen)
   done
 
 lemma perm_rsp[quot_respect]:
@@ -340,24 +349,24 @@
 lemma kpi_rsp[quot_respect]: 
   "(aty ===> op = ===> akind ===> akind) KPi KPi"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
-  apply (rule a2) apply simp
+  apply (rule a2) apply assumption
   apply (rule_tac x="0" in exI)
-  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
   done
 
 lemma tpi_rsp[quot_respect]: 
   "(aty ===> op = ===> aty ===> aty) TPi TPi"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
-  apply (rule a5) apply simp
+  apply (rule a5) apply assumption
   apply (rule_tac x="0" in exI)
-  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
   done
 lemma lam_rsp[quot_respect]: 
   "(aty ===> op = ===> atrm ===> atrm) Lam Lam"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
-  apply (rule a9) apply simp
+  apply (rule a9) apply assumption
   apply (rule_tac x="0" in exI)
-  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
   done
 
 lemma rfv_ty_rsp[quot_respect]: 
@@ -370,7 +379,12 @@
   "(atrm ===> op =) rfv_trm rfv_trm"
   by (simp add: alpha_rfv)
 
-lemma KIND_TY_TRM_induct: "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
+thm kind_ty_trm.induct
+
+lemma KIND_TY_TRM_induct: 
+  fixes P10 :: "KIND \<Rightarrow> bool" and P20 :: "TY \<Rightarrow> bool" and P30 :: "TRM \<Rightarrow> bool"
+  shows
+"\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
  \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
  \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
  \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
@@ -452,107 +466,108 @@
 
 end
 
-lemma "\<lbrakk>P10 TYP TYP;
- \<And>A A' K x K' x'.
-    \<lbrakk>(A :: TY) = A'; P20 A A';
-     \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
-          (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
- \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
- \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
- \<And>A A' B x B' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
-          (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
- \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
- \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
- \<And>A A' M x M' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
-          (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
-\<Longrightarrow> (x10 = x20 \<longrightarrow> P10 x10 x20) \<and>
-   (x30 = x40 \<longrightarrow> P20 x30 x40) \<and> (x50 = x60 \<longrightarrow> P30 x50 x60)"
-by (lifting akind_aty_atrm.induct)
+lemma AKIND_ATY_ATRM_inducts:
+"\<lbrakk>z1 = z2; P1 TYP TYP;
+ \<And>A A' a K b K'.
+    \<lbrakk>A = A'; P2 A A';
+     \<exists>pi. ({atom a},
+           K) \<approx>gen (\<lambda>x1 x2.
+                      x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
+    \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
+ \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
+ \<And>A A' M M'.
+    \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
+    \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
+ \<And>A A' a B b B'.
+    \<lbrakk>A = A'; P2 A A';
+     \<exists>pi. ({atom a},
+           B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
+    \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
+ \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
+ \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
+ \<And>M M' N N'.
+    \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
+    \<Longrightarrow> P3 (APP M N) (APP M' N');
+ \<And>A A' a M b M'.
+    \<lbrakk>A = A'; P2 A A';
+     \<exists>pi. ({atom a},
+           M) \<approx>gen (\<lambda>x1 x2.
+                      x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
+    \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
+\<Longrightarrow> P1 z1 z2"
+"\<lbrakk>z3 = z4; P1 TYP TYP;
+ \<And>A A' a K b K'.
+    \<lbrakk>A = A'; P2 A A';
+     \<exists>pi. ({atom a},
+           K) \<approx>gen (\<lambda>x1 x2.
+                      x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
+    \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
+ \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
+ \<And>A A' M M'.
+    \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
+    \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
+ \<And>A A' a B b B'.
+    \<lbrakk>A = A'; P2 A A';
+     \<exists>pi. ({atom a},
+           B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
+    \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
+ \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
+ \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
+ \<And>M M' N N'.
+    \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
+    \<Longrightarrow> P3 (APP M N) (APP M' N');
+ \<And>A A' a M b M'.
+    \<lbrakk>A = A'; P2 A A';
+     \<exists>pi. ({atom a},
+           M) \<approx>gen (\<lambda>x1 x2.
+                      x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
+    \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
+\<Longrightarrow> P2 z3 z4"
+"\<lbrakk>z5 = z6; P1 TYP TYP;
+ \<And>A A' a K b K'.
+    \<lbrakk>A = A'; P2 A A';
+     \<exists>pi. ({atom a},
+           K) \<approx>gen (\<lambda>x1 x2.
+                      x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
+    \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
+ \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
+ \<And>A A' M M'.
+    \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
+    \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
+ \<And>A A' a B b B'.
+    \<lbrakk>A = A'; P2 A A';
+     \<exists>pi. ({atom a},
+           B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
+    \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
+ \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
+ \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
+ \<And>M M' N N'.
+    \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
+    \<Longrightarrow> P3 (APP M N) (APP M' N');
+ \<And>A A' a M b M'.
+    \<lbrakk>A = A'; P2 A A';
+     \<exists>pi. ({atom a},
+           M) \<approx>gen (\<lambda>x1 x2.
+                      x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
+    \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
+\<Longrightarrow> P3 z5 z6"
+unfolding alpha_gen
+apply (lifting akind_aty_atrm.inducts[unfolded alpha_gen])
+done
 
-lemma AKIND_ATY_ATRM_inducts:
-"\<lbrakk>x10 = x20; P10 TYP TYP;
- \<And>A A' K x K' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
-          (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
- \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
- \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
- \<And>A A' B x B' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
-          (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
- \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
- \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
- \<And>A A' M x M' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
-          (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
-\<Longrightarrow> P10 x10 x20"
-"\<lbrakk>x30 = x40; P10 TYP TYP;
- \<And>A A' K x K' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
-          (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
- \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
- \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
- \<And>A A' B x B' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
-          (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
- \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
- \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
- \<And>A A' M x M' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
-          (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
- \<Longrightarrow> P20 x30 x40"
-"\<lbrakk>x50 = x60; P10 TYP TYP;
- \<And>A A' K x K' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
-          (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
- \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
- \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
- \<And>A A' B x B' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
-          (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
- \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
- \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
- \<And>A A' M x M' x'.
-    \<lbrakk>A = A'; P20 A A';
-     \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
-          (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
-    \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
-\<Longrightarrow> P30 x50 x60"
-by (lifting akind_aty_atrm.inducts)
-
+thm akind_aty_atrm_inj
 lemma KIND_TY_TRM_INJECT:
   "(TYP) = (TYP) = True"
-  "(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. (fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and> (fv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) = K' \<and> (pi \<bullet> x) = x')))"
+  "(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. ({atom x}, K) \<approx>gen (op =) fv_kind pi ({atom x'}, K')))"
   "(TCONST i) = (TCONST j) = (i = j)"
   "(TAPP A M) = (TAPP A' M') = (A = A' \<and> M = M')"
-  "(TPI A x B) = (TPI A' x' B') = ((A = A') \<and> (\<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and> (fv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) = B' \<and> (pi \<bullet> x) = x'))"
+  "(TPI A x B) = (TPI A' x' B') = (A = A' \<and> (\<exists>pi. ({atom x}, B) \<approx>gen (op =) fv_ty pi ({atom x'}, B')))"
   "(CONS i) = (CONS j) = (i = j)"
   "(VAR x) = (VAR y) = (x = y)"
   "(APP M N) = (APP M' N') = (M = M' \<and> N = N')"
-  "(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and> (fv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) = M' \<and> (pi \<bullet> x) = x'))"
-by (lifting akind_aty_atrm_inj)
+  "(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. ({atom x}, M) \<approx>gen (op =) fv_trm pi ({atom x'}, M')))"
+unfolding alpha_gen
+by (lifting akind_aty_atrm_inj[unfolded alpha_gen])
 
 lemma fv_kind_ty_trm:
  "fv_kind TYP = {}"
@@ -631,32 +646,24 @@
 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
 apply (simp_all add: supp_kind_ty_trm_easy)
 apply (simp_all add: fv_kind_ty_trm)
-apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abst {atom name} kind)")
-apply(simp add: supp_Abst Set.Un_commute)
+apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abs {atom name} kind)")
+apply(simp add: supp_Abs Set.Un_commute)
 apply(simp (no_asm) add: supp_def)
 apply(simp add: KIND_TY_TRM_INJECT)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
-apply(simp add: abs_eq alpha_gen)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] alpha_gen)
+apply(simp add: Abs_eq_iff alpha_gen)
 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
-apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric])
-apply (fold supp_def)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 apply (rule refl)
-apply(subst Set.Un_commute)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (rule refl)
-prefer 2
-apply(simp add: eqvts supp_eqvt atom_eqvt)
 sorry (* Stuck *)
 
-lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abst {atom x} K)) \<union> supp A"
+lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
 (*apply (subst supp_Pair[symmetric])*)
 unfolding supp_def
 apply (simp add: permute_set_eq)
-apply(subst abs_eq)
+apply(subst Abs_eq_iff)
 apply(subst KIND_TY_TRM_INJECT)
-apply(simp only: supp_fv)
+apply(simp only: alpha_gen supp_fv)
 apply simp
 apply (simp_all add: Collect_imp_eq Collect_neg_eq)
 apply(subst Set.Un_commute)
@@ -665,11 +672,16 @@
 apply (rule refl)
 prefer 2
 apply (rule refl)
-sorry (* Stuck *)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
+apply (rule refl)
+apply (simp_all)
+apply (simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric])
+sorry (* should be true... *)
 
 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
 apply(subst supp_kpi_pre)
-apply(subst supp_Abst)
+apply(subst supp_Abs)
 apply (simp only: Set.Un_commute)
 done