theory LFex

imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"

begin

atom_decl name

atom_decl ident

datatype rkind =

    Type

  | KPi "rty" "name" "rkind"

and rty =

    TConst "ident"

  | TApp "rty" "rtrm"

  | TPi "rty" "name" "rty"

and rtrm =

    Const "ident"

  | Var "name"

  | App "rtrm" "rtrm"

  | Lam "rty" "name" "rtrm"

instantiation rkind and rty and rtrm :: pt

begin

primrec

    permute_rkind

and permute_rty

and permute_rtrm

where

  "permute_rkind pi Type = Type"

| "permute_rkind pi (KPi t n k) = KPi (permute_rty pi t) (pi \<bullet> n) (permute_rkind pi k)"

| "permute_rty pi (TConst i) = TConst (pi \<bullet> i)"

| "permute_rty pi (TApp A M) = TApp (permute_rty pi A) (permute_rtrm pi M)"

| "permute_rty pi (TPi A x B) = TPi (permute_rty pi A) (pi \<bullet> x) (permute_rty pi B)"

| "permute_rtrm pi (Const i) = Const (pi \<bullet> i)"

| "permute_rtrm pi (Var x) = Var (pi \<bullet> x)"

| "permute_rtrm pi (App M N) = App (permute_rtrm pi M) (permute_rtrm pi N)"

| "permute_rtrm pi (Lam A x M) = Lam (permute_rty pi A) (pi \<bullet> x) (permute_rtrm pi M)"

lemma rperm_zero_ok:

  "0 \<bullet> (x :: rkind) = x"

  "0 \<bullet> (y :: rty) = y"

  "0 \<bullet> (z :: rtrm) = z"

apply(induct x and y and z rule: rkind_rty_rtrm.inducts)

apply(simp_all)

done

lemma rperm_plus_ok:

 "(p + q) \<bullet> (x :: rkind) = p \<bullet> q \<bullet> x"

 "(p + q) \<bullet> (y :: rty) = p \<bullet> q \<bullet> y"

 "(p + q) \<bullet> (z :: rtrm) = p \<bullet> q \<bullet> z"

apply(induct x and y and z rule: rkind_rty_rtrm.inducts)

apply(simp_all)

done

instance

apply default

apply (simp_all only:rperm_zero_ok rperm_plus_ok)

done

end

(*

setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}

local_setup {*

  snd o define_fv_alpha "LFex.rkind"

  [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],

   [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],

   [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}

notation

    alpha_rkind  ("_ \<approx>ki _" [100, 100] 100)

and alpha_rty    ("_ \<approx>rty _" [100, 100] 100)

and alpha_rtrm   ("_ \<approx>tr _" [100, 100] 100)

thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *}

thm alphas_inj

lemma alphas_eqvt:

  "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"

  "t2 \<approx>rty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>rty (pi \<bullet> s2)"

  "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"

sorry

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []),

  (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}]

     @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} 

     @{thms rkind.inject rty.inject rtrm.inject} @{thms alphas_inj}

     @{thms rkind.distinct rty.distinct rtrm.distinct}

     @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases}

     @{thms alphas_eqvt} ctxt)) ctxt)) *}

thm alphas_equivp

*)

primrec

where

inductive

    arkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)

and arty   :: "rty \<Rightarrow> rty \<Rightarrow> bool"     ("_ \<approx>rty _" [100, 100] 100)

and artrm  :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)

where

  a1: "(Type) \<approx>ki (Type)"

| a3: "i = j \<Longrightarrow> (TConst i) \<approx>rty (TConst j)"

| a4: "\<lbrakk>A \<approx>rty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>rty (TApp A' M')"

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

lemma arkind_arty_artrm_inj:

  "(Type) \<approx>ki (Type) = True"

  "(TConst i) \<approx>rty (TConst j) = (i = j)"

  "(TApp A M) \<approx>rty (TApp A' M') = (A \<approx>rty A' \<and> M \<approx>tr M')"

  "(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')"

apply -

apply (simp add: arkind_arty_artrm.intros)

apply rule apply (erule arkind.cases) apply simp apply blast

apply (simp only: arkind_arty_artrm.intros)

apply rule apply (erule arty.cases) apply simp apply simp apply simp

apply (simp only: arkind_arty_artrm.intros)

apply rule apply (erule arty.cases) apply simp apply simp apply simp

apply (simp only: arkind_arty_artrm.intros)

apply rule apply (erule arty.cases) apply simp apply simp apply blast

apply (simp only: arkind_arty_artrm.intros)

apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast

apply (simp only: arkind_arty_artrm.intros)

apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast

apply (simp only: arkind_arty_artrm.intros)

apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast

apply (simp only: arkind_arty_artrm.intros)

apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast

apply (simp only: arkind_arty_artrm.intros)

done

lemma rfv_eqvt[eqvt]:

apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.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>rty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>rty (pi \<bullet> s2)"

  "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"

apply(induct rule: arkind_arty_artrm.inducts)

apply (simp_all add: arkind_arty_artrm.intros)

apply (simp_all add: arkind_arty_artrm_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::"rkind" 

  and   A::"rty"

  and   M::"rtrm"

  shows "K \<approx>ki K"

  and   "A \<approx>rty A"

  and   "M \<approx>tr M"

  apply(induct K and A and M rule: rkind_rty_rtrm.inducts)

  apply(auto intro: arkind_arty_artrm.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'::"rkind" and A A'::"rty" and M M'::"rtrm"

  shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"

  and   "A \<approx>rty A' \<Longrightarrow> A' \<approx>rty A"

  and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"

  apply(induct K K' and A A' and M M' rule: arkind_arty_artrm.inducts)

  apply(simp_all add: arkind_arty_artrm.intros)

  apply (simp_all add: arkind_arty_artrm_inj)

  apply(erule alpha_gen_compose_sym)

  apply(erule alpha_eqvt)

  apply(erule alpha_gen_compose_sym)

  apply(erule alpha_eqvt)

  apply(erule alpha_gen_compose_sym)

  apply(erule alpha_eqvt)

  done

lemma al_trans:

  fixes K K' K''::"rkind" and A A' A''::"rty" and M M' M''::"rtrm"

  shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"

  and   "A \<approx>rty A' \<Longrightarrow> A' \<approx>rty A'' \<Longrightarrow> A \<approx>rty 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: arkind_arty_artrm.inducts)

  apply(simp_all add: arkind_arty_artrm.intros)

  apply(erule arkind.cases)

  apply(simp_all add: arkind_arty_artrm.intros)

  apply(simp add: arkind_arty_artrm_inj)

  apply(erule alpha_gen_compose_trans)

  apply(assumption)

  apply(erule alpha_eqvt)

  apply(rotate_tac 4)

  apply(erule arty.cases)

  apply(simp_all add: arkind_arty_artrm.intros)

  apply(rotate_tac 3)

  apply(erule arty.cases)

  apply(simp_all add: arkind_arty_artrm.intros)

  apply(simp add: arkind_arty_artrm_inj)

  apply(erule alpha_gen_compose_trans)

  apply(assumption)

  apply(erule alpha_eqvt)

  apply(rotate_tac 4)

  apply(erule artrm.cases)

  apply(simp_all add: arkind_arty_artrm.intros)

  apply(rotate_tac 3)

  apply(erule artrm.cases)

  apply(simp_all add: arkind_arty_artrm.intros)

  apply(simp add: arkind_arty_artrm_inj)

  apply(erule alpha_gen_compose_trans)

  apply(assumption)

  apply(erule alpha_eqvt)

  done

lemma alpha_equivps:

  shows "equivp arkind"

  and   "equivp arty"

  and   "equivp artrm"

  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 RKIND = rkind / arkind

  by (rule alpha_equivps)

quotient_type

    RTY = rty / arty and

    RTRM = rtrm / artrm

  by (auto intro: alpha_equivps)

quotient_definition

   "TYP :: RKIND"

is

  "Type"

quotient_definition

   "KPI :: RTY \<Rightarrow> name \<Rightarrow> RKIND \<Rightarrow> RKIND"

is

  "KPi"

quotient_definition

   "TCONST :: ident \<Rightarrow> RTY"

is

  "TConst"

quotient_definition

   "TAPP :: RTY \<Rightarrow> RTRM \<Rightarrow> RTY"

is

  "TApp"

quotient_definition

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

is

  "TPi"

(* FIXME: does not work with CONST *)

quotient_definition

   "CONS :: ident \<Rightarrow> RTRM"

is

  "Const"

quotient_definition

   "VAR :: name \<Rightarrow> RTRM"

is

  "Var"

quotient_definition

   "APP :: RTRM \<Rightarrow> RTRM \<Rightarrow> RTRM"

is

  "App"

quotient_definition

   "LAM :: RTY \<Rightarrow> name \<Rightarrow> RTRM \<Rightarrow> RTRM"

is

  "Lam"

(* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *)

quotient_definition

is

quotient_definition

is

quotient_definition

is

lemma alpha_rfv:

  apply(rule arkind_arty_artrm.induct)

  apply(simp_all add: alpha_gen)

  done

lemma perm_rsp[quot_respect]:

  "(op = ===> arkind ===> arkind) permute permute"

  "(op = ===> arty ===> arty) permute permute"

  "(op = ===> artrm ===> artrm) permute permute"

  by (simp_all add:alpha_eqvt)

lemma tconst_rsp[quot_respect]: 

  "(op = ===> arty) TConst TConst"

  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

lemma tapp_rsp[quot_respect]: 

  "(arty ===> artrm ===> arty) TApp TApp" 

  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

lemma var_rsp[quot_respect]: 

  "(op = ===> artrm) Var Var"

  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

lemma app_rsp[quot_respect]: 

  "(artrm ===> artrm ===> artrm) App App"

  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

lemma const_rsp[quot_respect]: 

  "(op = ===> artrm) Const Const"

  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

lemma kpi_rsp[quot_respect]: 

  "(arty ===> op = ===> arkind ===> arkind) 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]: 

  "(arty ===> op = ===> arty ===> arty) 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]: 

  "(arty ===> op = ===> artrm ===> artrm) 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

  by (simp add: alpha_rfv)

  by (simp add: alpha_rfv)

  by (simp add: alpha_rfv)

thm rkind_rty_rtrm.induct

lemmas RKIND_RTY_RTRM_induct = rkind_rty_rtrm.induct[quot_lifted]

thm rkind_rty_rtrm.inducts

lemmas RKIND_RTY_RTRM_inducts = rkind_rty_rtrm.inducts[quot_lifted]

instantiation RKIND and RTY and RTRM :: pt

begin

quotient_definition

  "permute_RKIND :: perm \<Rightarrow> RKIND \<Rightarrow> RKIND"

is

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

quotient_definition

  "permute_RTY :: perm \<Rightarrow> RTY \<Rightarrow> RTY"

is

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

quotient_definition

  "permute_RTRM :: perm \<Rightarrow> RTRM \<Rightarrow> RTRM"

is

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

lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]

lemma perm_zero_ok: "0 \<bullet> (x :: RKIND) = x \<and> 0 \<bullet> (y :: RTY) = y \<and> 0 \<bullet> (z :: RTRM) = z"

apply (induct rule: RKIND_RTY_RTRM_induct)

apply (simp_all)

done

lemma perm_add_ok:

  "((p + q) \<bullet> (x1 :: RKIND) = (p \<bullet> q \<bullet> x1))"

  "((p + q) \<bullet> (x2 :: RTY) = p \<bullet> q \<bullet> x2)"

  "((p + q) \<bullet> (x3 :: RTRM) = p \<bullet> q \<bullet> x3)"

apply (induct x1 and x2 and x3 rule: RKIND_RTY_RTRM_inducts)

apply (simp_all)

done

instance

apply default

apply (simp_all add: perm_zero_ok perm_add_ok)

done

end

lemmas ARKIND_ARTY_ARTRM_inducts = arkind_arty_artrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]

lemmas RKIND_RTY_RTRM_INJECT = arkind_arty_artrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

lemmas fv_eqvt = rfv_eqvt[quot_lifted]

lemma supp_rkind_rty_rtrm_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 RKIND_RTY_RTRM_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, rtrm))) supports (LAM ty na rtrm)"

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)