theory LFex
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"  "Abs"
begin

atom_decl name
atom_decl ident

datatype kind =
    Type
  | KPi "ty" "name" "kind"
and ty =
    TConst "ident"
  | TApp "ty" "trm"
  | TPi "ty" "name" "ty"
and trm =
    Const "ident"
  | Var "name"
  | App "trm" "trm"
  | Lam "ty" "name" "trm"

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) = {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) = {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})"

instantiation kind and ty and trm :: pt
begin

primrec
    permute_kind
and permute_ty
and permute_trm
where
  "permute_kind pi Type = Type"
| "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \<bullet> n) (permute_kind pi k)"
| "permute_ty pi (TConst i) = TConst (pi \<bullet> i)"
| "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)"
| "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \<bullet> x) (permute_ty pi B)"
| "permute_trm pi (Const i) = Const (pi \<bullet> i)"
| "permute_trm pi (Var x) = Var (pi \<bullet> x)"
| "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)"
| "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)"

lemma rperm_zero_ok:
  "0 \<bullet> (x :: kind) = x"
  "0 \<bullet> (y :: ty) = y"
  "0 \<bullet> (z :: trm) = z"
apply(induct x and y and z rule: kind_ty_trm.inducts)
apply(simp_all)
done

lemma rperm_plus_ok:
 "(p + q) \<bullet> (x :: kind) = p \<bullet> q \<bullet> x"
 "(p + q) \<bullet> (y :: ty) = p \<bullet> q \<bullet> y"
 "(p + q) \<bullet> (z :: trm) = p \<bullet> q \<bullet> z"
apply(induct x and y and z rule: kind_ty_trm.inducts)
apply(simp_all)
done

instance
apply default
apply (simp_all only:rperm_zero_ok rperm_plus_ok)
done

end

inductive
    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)"
| 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')"
| 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')"
| 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)
*)

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

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"
  and   M::"trm"
  shows "K \<approx>ki K"
  and   "A \<approx>ty A"
  and   "M \<approx>tr M"
  apply(induct K and A and M rule: kind_ty_trm.inducts)
  apply(auto intro: akind_aty_atrm.intros)
  apply (rule a2)
  apply auto
  apply(rule_tac x="0" in exI)
  apply(simp_all add: fresh_star_def fresh_zero_perm)
  apply (rule a5)
  apply auto
  apply(rule_tac x="0" in exI)
  apply(simp_all add: fresh_star_def fresh_zero_perm)
  apply (rule a9)
  apply auto
  apply(rule_tac x="0" in exI)
  apply(simp_all add: fresh_star_def fresh_zero_perm)
  done

lemma alpha_equivps:
  shows "equivp akind"
  and   "equivp aty"
  and   "equivp atrm"
sorry

quotient_type KIND = kind / akind
  by (rule alpha_equivps)

quotient_type
    TY = ty / aty and
    TRM = trm / atrm
  by (auto intro: alpha_equivps)

quotient_definition
   "TYP :: KIND"
as
  "Type"

quotient_definition
   "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
as
  "KPi"

quotient_definition
   "TCONST :: ident \<Rightarrow> TY"
as
  "TConst"

quotient_definition
   "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
as
  "TApp"

quotient_definition
   "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
as
  "TPi"

(* FIXME: does not work with CONST *)
quotient_definition
   "CONS :: ident \<Rightarrow> TRM"
as
  "Const"

quotient_definition
   "VAR :: name \<Rightarrow> TRM"
as
  "Var"

quotient_definition
   "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
as
  "App"

quotient_definition
   "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
as
  "Lam"

(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
quotient_definition
   "fv_kind :: KIND \<Rightarrow> atom set"
as
  "rfv_kind"

quotient_definition
   "fv_ty :: TY \<Rightarrow> atom set"
as
  "rfv_ty"

quotient_definition
   "fv_trm :: TRM \<Rightarrow> atom set"
as
  "rfv_trm"

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>
     (t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
  apply(rule akind_aty_atrm.induct)
  apply(simp_all)
  done

lemma perm_rsp[quot_respect]:
  "(op = ===> akind ===> akind) permute permute"
  "(op = ===> aty ===> aty) permute permute"
  "(op = ===> atrm ===> atrm) permute permute"
  by (simp_all add:alpha_eqvt)

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 var_rsp[quot_respect]: 
  "(op = ===> atrm) Var Var"
  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
lemma app_rsp[quot_respect]: 
  "(atrm ===> atrm ===> atrm) App App"
  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
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)
  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)
lemma rfv_kind_rsp[quot_respect]:
  "(akind ===> op =) rfv_kind rfv_kind"
  by (simp add: alpha_rfv)
lemma rfv_trm_rsp[quot_respect]:
  "(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);
 \<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 \<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

quotient_definition
  "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"
as
  "permute :: perm \<Rightarrow> kind \<Rightarrow> kind"

quotient_definition
  "permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
as
  "permute :: perm \<Rightarrow> ty \<Rightarrow> ty"

quotient_definition
  "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
as
  "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"

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)"
and   "pi \<bullet> (TAPP A M) = TAPP (pi \<bullet> A) (pi \<bullet> M)"
and   "pi \<bullet> (TPI A x B) = TPI (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> B)"
and   "pi \<bullet> (CONS i) = CONS (pi \<bullet> i)"
and   "pi \<bullet> (VAR x) = VAR (pi \<bullet> x)"
and   "pi \<bullet> (APP M N) = APP (pi \<bullet> M) (pi \<bullet> N)"
and   "pi \<bullet> (LAM A x M) = LAM (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> M)"
apply (lifting permute_kind_permute_ty_permute_trm.simps)
done

lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
apply (induct rule: KIND_TY_TRM_induct)
apply simp_all
done

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)
done

instance
apply default
apply (simp_all add: perm_zero_ok perm_add_ok)
done

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>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_kind_ty_trm_easy:
 "supp TYP = {}"
 "supp (TCONST i) = {atom i}"
 "supp (TAPP A M) = supp A \<union> supp M"
 "supp (CONS i) = {atom i}"
 "supp (VAR x) = {atom x}"
 "supp (APP M N) = supp M \<union> supp N"
apply (simp_all add: supp_def permute_ktt KIND_TY_TRM_INJECT)
apply (simp_all only: supp_at_base[simplified supp_def])
apply (simp_all add: Collect_imp_eq Collect_neg_eq)
done

lemma supp_bind:
  "(supp (atom na, (ty, ki))) supports (KPI ty na ki)"
  "(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)"
  "(supp (atom na, (ty, trm))) supports (LAM ty na trm)"
apply(simp_all add: supports_def)
apply(fold fresh_def)
apply(simp_all add: fresh_Pair swap_fresh_fresh)
apply(clarify)
apply(subst swap_at_base_simps(3))
apply(simp_all add: fresh_atom)
apply(clarify)
apply(subst swap_at_base_simps(3))
apply(simp_all add: fresh_atom)
apply(clarify)
apply(subst swap_at_base_simps(3))
apply(simp_all add: fresh_atom)
done

lemma KIND_TY_TRM_fs:
  "finite (supp (x\<Colon>KIND))"
  "finite (supp (y\<Colon>TY))"
  "finite (supp (z\<Colon>TRM))"
apply(induct x and y and z rule: KIND_TY_TRM_inducts)
apply(simp_all add: supp_kind_ty_trm_easy)
apply(rule supports_finite)
apply(rule supp_bind(1))
apply(simp add: supp_Pair supp_atom)
apply(rule supports_finite)
apply(rule supp_bind(2))
apply(simp add: supp_Pair supp_atom)
apply(rule supports_finite)
apply(rule supp_bind(3))
apply(simp add: supp_Pair supp_atom)
done

instance KIND and TY and TRM :: fs
apply(default)
apply(simp_all only: KIND_TY_TRM_fs)
done

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: 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(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: 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"
(*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 (simp_all add: Collect_imp_eq Collect_neg_eq)
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 (rule refl)
sorry (* Stuck *)

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 (simp only: Set.Un_commute)
done

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 (simp_all only: supp_kind_ty_trm_easy)
apply (simp add: supp_kpi)
sorry (* Other ones will follow similarily *)


end