theory LFex

imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "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. (({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. (({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. (({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 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 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 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)

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 (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:

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

  apply (rule a5)

  apply auto

  apply(rule_tac x="0" in exI)

  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 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"

  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)

quotient_type

    TY = ty / aty and

    TRM = trm / atrm

  by (auto intro: alpha_equivps)

quotient_definition

   "TYP :: KIND"

  "Type"

quotient_definition

   "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"

  "KPi"

quotient_definition

   "TCONST :: ident \<Rightarrow> TY"

  "TConst"

quotient_definition

   "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"

  "TApp"

quotient_definition

   "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"

  "TPi"

(* FIXME: does not work with CONST *)

quotient_definition

   "CONS :: ident \<Rightarrow> TRM"

  "Const"

quotient_definition

   "VAR :: name \<Rightarrow> TRM"

  "Var"

quotient_definition

   "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"

  "App"

quotient_definition

   "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"

  "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"

  "rfv_kind"

quotient_definition

   "fv_ty :: TY \<Rightarrow> atom set"

  "rfv_ty"

quotient_definition

   "fv_trm :: TRM \<Rightarrow> atom set"

  "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 add: alpha_gen)

  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 assumption

  apply (rule_tac x="0" in exI)

  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 assumption

  apply (rule_tac x="0" in exI)

  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 assumption

  apply (rule_tac x="0" in exI)

  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)

  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)

thm kind_ty_trm.induct

lemmas KIND_TY_TRM_induct = kind_ty_trm.induct[quot_lifted]

thm kind_ty_trm.inducts

lemmas KIND_TY_TRM_inducts = kind_ty_trm.inducts[quot_lifted]

instantiation KIND and TY and TRM :: pt

begin

quotient_definition

  "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"

  "permute :: perm \<Rightarrow> kind \<Rightarrow> kind"

quotient_definition

  "permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"

  "permute :: perm \<Rightarrow> ty \<Rightarrow> ty"

quotient_definition