# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264849972 -3600
# Node ID 2fcd18e7bb182dcbcf2cebb571d901d77450b2c1
# Parent  ee0619b5adff46cf4a353640256c44a6a04a2ed1# Parent  333c24bd595d25ff10dc905dab2a3e6d750cb3cd
merged

diff -r ee0619b5adff -r 2fcd18e7bb18 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Sat Jan 30 11:44:25 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Sat Jan 30 12:12:52 2010 +0100
@@ -1,37 +1,39 @@
 theory LFex
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"  "Abs"
 begin
 
 atom_decl name
 atom_decl ident
 
-datatype kind = 
+datatype kind =
     Type
   | KPi "ty" "name" "kind"
-and ty =  
+and ty =
     TConst "ident"
   | TApp "ty" "trm"
   | TPi "ty" "name" "ty"
-and trm = 
+and trm =
     Const "ident"
   | Var "name"
   | App "trm" "trm"
-  | Lam "ty" "name" "trm" 
+  | Lam "ty" "name" "trm"
+print_theorems
 
-fun
+primrec
     rfv_kind :: "kind \<Rightarrow> atom set"
 and rfv_ty   :: "ty \<Rightarrow> atom set"
 and rfv_trm  :: "trm \<Rightarrow> atom set"
 where
   "rfv_kind (Type) = {}"
 | "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
-| "rfv_ty (TConst i) = {}"
+| "rfv_ty (TConst i) = {atom i}"
 | "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
 | "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
-| "rfv_trm (Const i) = {}"
+| "rfv_trm (Const i) = {atom i}"
 | "rfv_trm (Var x) = {atom x}"
 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
+print_theorems
 
 instantiation kind and ty and trm :: pt
 begin
@@ -58,7 +60,7 @@
 instance
 apply default
 apply (simp_all only:rperm_zero_ok)
-apply(induct_tac [!] x)
+apply(induct_tac[!] x)
 apply(simp_all)
 apply(induct_tac ty)
 apply(simp_all)
@@ -85,6 +87,127 @@
 | 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)
+*)
+
+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')))"
+  "(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'))"
+  "(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'))"
+apply -
+apply (simp add: akind_aty_atrm.intros)
+
+apply rule apply (erule akind.cases) apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule aty.cases) apply simp apply simp apply simp
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule aty.cases) apply simp apply simp apply simp
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule aty.cases) apply simp apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+
+apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: akind_aty_atrm.intros)
+done
+
+(* TODO: ask Stefan why 'induct' goes wrong, commented out commands should work *)
+
+lemma rfv_eqvt[eqvt]:
+  "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
+  "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
+  "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
+apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts)
+apply(simp_all add:  union_eqvt Diff_eqvt)
+apply(simp_all add: permute_set_eq atom_eqvt)
+done
+
+lemma alpha_eqvt:
+  "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
+  "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
+  "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])
+done
+
 lemma al_refl:
   fixes K::"kind" 
   and   A::"ty"
@@ -184,7 +307,6 @@
 as
   "rfv_trm"
 
-thm akind_aty_atrm.induct
 lemma alpha_rfv:
   shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
      (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
@@ -197,21 +319,14 @@
   "(op = ===> akind ===> akind) permute permute"
   "(op = ===> aty ===> aty) permute permute"
   "(op = ===> atrm ===> atrm) permute permute"
-apply simp_all
-sorry (* by eqvt *)
+  by (simp_all add:alpha_eqvt)
 
-lemma kpi_rsp[quot_respect]: 
-  "(aty ===> op = ===> akind ===> akind) KPi KPi"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 lemma tconst_rsp[quot_respect]: 
   "(op = ===> aty) TConst TConst"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 lemma tapp_rsp[quot_respect]: 
   "(aty ===> atrm ===> aty) TApp TApp" 
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
-lemma tpi_rsp[quot_respect]: 
-  "(aty ===> op = ===> aty ===> aty) TPi TPi"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
 lemma var_rsp[quot_respect]: 
   "(op = ===> atrm) Var Var"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
@@ -221,9 +336,30 @@
 lemma const_rsp[quot_respect]: 
   "(op = ===> atrm) Const Const"
   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
+
+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_tac x="0" in exI)
+  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+  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_tac x="0" in exI)
+  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+  done
 lemma lam_rsp[quot_respect]: 
   "(aty ===> op = ===> atrm ===> atrm) Lam Lam"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
+  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
+  apply (rule a9) apply simp
+  apply (rule_tac x="0" in exI)
+  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+  done
+
 lemma rfv_ty_rsp[quot_respect]: 
   "(aty ===> op =) rfv_ty rfv_ty"
   by (simp add: alpha_rfv)
@@ -234,9 +370,6 @@
   "(atrm ===> op =) rfv_trm rfv_trm"
   by (simp add: alpha_rfv)
 
-thm akind_aty_atrm.induct
-thm kind_ty_trm.induct
-
 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);
  \<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);
@@ -245,6 +378,29 @@
 \<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm"
 by (lifting kind_ty_trm.induct)
 
+thm kind_ty_trm.inducts
+
+lemma KIND_TY_TRM_inducts: 
+"\<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);
+ \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
+\<Longrightarrow> P10 kind"
+"\<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);
+ \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
+\<Longrightarrow> P20 ty"
+"\<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);
+ \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
+\<Longrightarrow> P30 trm"
+by (lifting kind_ty_trm.inducts)
+
 instantiation KIND and TY and TRM :: pt
 begin
 
@@ -263,9 +419,7 @@
 as
   "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"
 
-term "permute_TRM"
-thm permute_kind_permute_ty_permute_trm.simps
-lemma [simp]:
+lemma permute_ktt[simp]:
 shows "pi \<bullet> TYP = TYP"
 and   "pi \<bullet> (KPI t n k) = KPI (pi \<bullet> t) (pi \<bullet> n) (pi \<bullet> k)"
 and   "pi \<bullet> (TCONST i) = TCONST (pi \<bullet> i)"
@@ -283,11 +437,13 @@
 apply simp_all
 done
 
-lemma perm_add_ok: "((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> (x1 :: KIND))) \<and> ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2) \<and> ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"
-apply(induct_tac [!] rule: KIND_TY_TRM_induct)
+lemma perm_add_ok: 
+  "((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))"
+  "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)"
+  "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)"
+apply(induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts)
 apply (simp_all)
-(* Sth went wrong... *)
-sorry
+done
 
 instance
 apply default
@@ -318,8 +474,156 @@
     \<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)"
-apply (lifting akind_aty_atrm.induct)
-done
+by (lifting akind_aty_atrm.induct)
+
+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)
+
+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')))"
+  "(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'))"
+  "(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)
+
+lemma fv_kind_ty_trm:
+ "fv_kind TYP = {}"
+ "fv_kind (KPI A x K) = fv_ty A \<union> (fv_kind K - {atom x})"
+ "fv_ty (TCONST i) = {atom i}"
+ "fv_ty (TAPP A M) = fv_ty A \<union> fv_trm M"
+ "fv_ty (TPI A x B) = fv_ty A \<union> (fv_ty B - {atom x})"
+ "fv_trm (CONS i) = {atom i}"
+ "fv_trm (VAR x) = {atom x}"
+ "fv_trm (APP M N) = fv_trm M \<union> fv_trm N"
+ "fv_trm (LAM A x M) = fv_ty A \<union> (fv_trm M - {atom x})"
+by(lifting rfv_kind_rfv_ty_rfv_trm.simps)
+
+lemma fv_eqvt:
+ "(p \<bullet> fv_kind t1) = fv_kind (p \<bullet> t1)"
+ "(p \<bullet> fv_ty t2) = fv_ty (p \<bullet> t2)"
+ "(p \<bullet> fv_trm t3) = fv_trm (p \<bullet> t3)"
+by(lifting rfv_eqvt)
+
+lemma supp_fv:
+ "fv_kind t1 = supp t1"
+ "fv_ty t2 = supp t2"
+ "fv_trm t3 = supp t3"
+apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
+apply (simp_all add: fv_kind_ty_trm)
+apply (simp_all add: supp_def)
+sorry
+
+lemma
+"(supp ((a \<rightleftharpoons> b) \<bullet> (K::KIND)) - {atom ((a \<rightleftharpoons> b) \<bullet> (x::name))} = supp K - {atom x} \<longrightarrow>
+(a \<rightleftharpoons> b) \<bullet> A = (A::TY) \<longrightarrow> (\<forall>pi\<Colon>perm. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K \<longrightarrow> (supp K - {atom x}) \<sharp>* pi \<longrightarrow> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> x)) =
+(supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x} \<and>
+(\<exists>pi\<Colon>perm. (supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)}) \<sharp>* pi \<and> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K) \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> A \<noteq> A)"
+apply (case_tac "(a \<rightleftharpoons> b) \<bullet> A = A")
+apply (case_tac "supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x}")
+apply simp_all
+sorry
+
+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 KIND_TY_TRM_INJECT)
+apply(simp only: supp_fv)
+apply simp
+apply (unfold supp_def)
+sorry
+
+lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
+apply(subst supp_kpi_pre)
+thm supp_Abs
+(*apply(simp add: supp_Abs)*)
+sorry
+
+lemma supp_kind_ty_trm:
+ "supp TYP = {}"
+ "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
+ "supp (TCONST i) = {atom i}"
+ "supp (TAPP A M) = supp A \<union> supp M"
+ "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
+ "supp (CONS i) = {atom i}"
+ "supp (VAR x) = {atom x}"
+ "supp (APP M N) = supp M \<union> supp N"
+ "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
+apply -
+apply (simp add: supp_def)
+apply (simp add: supp_kpi)
+apply (simp add: supp_def) (* need ty.distinct lifted *)
+sorry
+
 
 end