theory LFex

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

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"

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>ty _" [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 alpha_rkind_alpha_rty_alpha_rtrm_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 alpha_rkind_alpha_rty_alpha_rtrm_inj

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

  "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: alpha_rkind_alpha_rty_alpha_rtrm.inducts)

apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)

apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_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

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

  (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 alpha_rkind_alpha_rty_alpha_rtrm_inj}

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

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

     @{thms alpha_eqvt} ctxt)) ctxt)) *}

thm alpha_equivps

local_setup  {* define_quotient_type

  [(([], @{binding kind}, NoSyn), (@{typ rkind}, @{term alpha_rkind})),

   (([], @{binding ty},   NoSyn), (@{typ rty},   @{term alpha_rty}  )),

   (([], @{binding trm},  NoSyn), (@{typ rtrm},  @{term alpha_rtrm} ))]

  (ALLGOALS (resolve_tac @{thms alpha_equivps}))

*}

local_setup {*

(fn ctxt => ctxt

 |> snd o (Quotient_Def.quotient_lift_const ("TYP", @{term Type}))

 |> snd o (Quotient_Def.quotient_lift_const ("KPI", @{term KPi}))

 |> snd o (Quotient_Def.quotient_lift_const ("TCONST", @{term TConst}))

 |> snd o (Quotient_Def.quotient_lift_const ("TAPP", @{term TApp}))

 |> snd o (Quotient_Def.quotient_lift_const ("TPI", @{term TPi}))

 |> snd o (Quotient_Def.quotient_lift_const ("CONS", @{term Const}))

 |> snd o (Quotient_Def.quotient_lift_const ("VAR", @{term Var}))

 |> snd o (Quotient_Def.quotient_lift_const ("APP", @{term App}))

 |> snd o (Quotient_Def.quotient_lift_const ("LAM", @{term Lam}))

 |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind}))

 |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty}))

 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}

print_theorems

local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]

  (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *}

local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}]

  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}

local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}]

  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}

local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}]

  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}

ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}

  @{thms rfv_rsp} @{thms alpha_equivps} 1 *}

local_setup {* prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}

local_setup {* prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}

local_setup {* prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *}

local_setup {* prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *}

local_setup {* prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *}

local_setup {* prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *}

local_setup {* prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *}

local_setup {* prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *}

lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted]

thm rkind_rty_rtrm.inducts

lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted]

instantiation kind and ty and trm :: pt

begin

quotient_definition

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

is

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

quotient_definition

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

is

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

quotient_definition

  "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm"

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

lemmas ALPHA_kind_ALPHA_ty_ALPHA_trm_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]

lemmas kind_ty_trm_INJECT = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

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)

apply (simp_all only: 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_fv:

 "supp t1 = fv_kind t1"

 "supp t2 = fv_ty t2"

 "supp t3 = fv_trm t3"

apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts)

apply (simp_all add: supp_rkind_rty_rtrm_easy)

apply (simp_all add: fv_kind_ty_trm)

apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)")

apply(simp (no_asm) add: supp_def)

apply(simp add: kind_ty_trm_INJECT)

apply(simp add: Abs_eq_iff)

apply(simp add: alpha_gen)

apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)

apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])

apply(subgoal_tac "supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)")

apply(simp (no_asm) add: supp_def)

apply(simp add: kind_ty_trm_INJECT)

apply(simp add: Abs_eq_iff)

apply(simp add: alpha_gen)

apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)

apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)

apply(subgoal_tac "supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)")

apply(simp (no_asm) add: supp_def)

apply(simp add: kind_ty_trm_INJECT)

apply(simp add: Abs_eq_iff)

apply(simp add: alpha_gen)

apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)

apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)

done

(* Not needed anymore *)

apply (simp add: permute_set_eq supp_def Abs_eq_iff kind_ty_trm_INJECT)

apply (simp add: alpha_gen supp_fv)

apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute)

done

lemma supp_rkind_rty_rtrm:

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

apply (simp_all only: supp_fv fv_kind_ty_trm)

done

end