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

    fv_rkind :: "rkind \<Rightarrow> atom set"

and fv_rty   :: "rty \<Rightarrow> atom set"

and fv_rtrm  :: "rtrm \<Rightarrow> atom set"

where

  "fv_rkind (Type) = {}"

| "fv_rkind (KPi A x K) = (fv_rty A) \<union> ((fv_rkind K) - {atom x})"

| "fv_rty (TConst i) = {atom i}"

| "fv_rty (TApp A M) = (fv_rty A) \<union> (fv_rtrm M)"

| "fv_rty (TPi A x B) = (fv_rty A) \<union> ((fv_rty B) - {atom x})"

| "fv_rtrm (Const i) = {atom i}"

| "fv_rtrm (Var x) = {atom x}"

| "fv_rtrm (App M N) = (fv_rtrm M) \<union> (fv_rtrm N)"

| "fv_rtrm (Lam A x M) = (fv_rty A) \<union> ((fv_rtrm M) - {atom x})"

inductive

where

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

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

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

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

done

lemma rfv_eqvt[eqvt]:

  "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"

  "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"

  "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>t3))"

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

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

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   "M \<approx>tr M"

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

  apply auto

  apply(rule_tac x="0" in exI)

  apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)

  apply auto

  apply(rule_tac x="0" in exI)

  apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)

  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   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"

  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   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"

  apply(erule alpha_gen_compose_trans)

  apply(assumption)

  apply(erule alpha_eqvt)

  apply(rotate_tac 4)

  apply(rotate_tac 3)

  apply(erule alpha_gen_compose_trans)

  apply(assumption)

  apply(erule alpha_eqvt)

  apply(rotate_tac 4)

  apply(rotate_tac 3)

  apply(erule alpha_gen_compose_trans)

  apply(assumption)

  apply(erule alpha_eqvt)

  done

lemma alpha_equivps:

  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

  by (rule alpha_equivps)

quotient_type

  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

   "fv_kind :: RKIND \<Rightarrow> atom set"

is

  "fv_rkind"

quotient_definition

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

is

  "fv_rty"

quotient_definition

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

is

  "fv_rtrm"

lemma alpha_rfv:

  shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and>

     (t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)"

  apply(simp_all add: alpha_gen)

  done

lemma perm_rsp[quot_respect]:

  by (simp_all add:alpha_eqvt)

lemma tconst_rsp[quot_respect]: 

lemma tapp_rsp[quot_respect]: 

lemma var_rsp[quot_respect]: 

lemma app_rsp[quot_respect]: 

lemma const_rsp[quot_respect]: 

lemma kpi_rsp[quot_respect]: 

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

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

  apply (rule_tac x="0" in exI)

  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)

  done

lemma fv_rty_rsp[quot_respect]: 

  by (simp add: alpha_rfv)

lemma fv_rkind_rsp[quot_respect]:

  by (simp add: alpha_rfv)

lemma fv_rtrm_rsp[quot_respect]:

  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 fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]

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)