theory LFex

imports "Parser"

begin

atom_decl name

atom_decl ident

ML {* restricted_nominal := 2 *}

nominal_datatype kind =

    Type

  | KPi "ty" n::"name" k::"kind" bind n in k

and ty =

    TConst "ident"

  | TApp "ty" "trm"

  | TPi "ty" n::"name" t::"ty" bind n in t

and trm =

    Const "ident"

  | Var "name"

  | App "trm" "trm"

  | Lam "ty" n::"name" t::"trm" bind n in t

lemma supports:

  "{} supports Type"

  "(supp (atom i)) supports (TConst i)"

  "(supp A \<union> supp M) supports (TApp A M)"

  "(supp (atom i)) supports (Const i)"

  "(supp (atom x)) supports (Var x)"

  "(supp M \<union> supp N) supports (App M N)"

  "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPi ty na ki)"

  "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPi ty na ty2)"

  "(supp ty \<union> supp (atom na) \<union> supp trm) supports (Lam ty na trm)"

apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh kind_ty_trm_perm)

apply(rule_tac [!] allI)+

apply(rule_tac [!] impI)

apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})

apply(simp_all add: fresh_atom)

done

lemma kind_ty_trm_fs:

  "finite (supp (x\<Colon>kind)) \<and> finite (supp (y\<Colon>ty)) \<and> finite (supp (z\<Colon>trm))"

apply(induct rule: kind_ty_trm_induct)

apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})

apply(simp_all add: supp_atom)

done

instance kind and ty and trm :: fs

apply(default)

apply(simp_all only: kind_ty_trm_fs)

done

lemma ex_out: 

  "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"

  "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"

  "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"

  "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"

apply (blast)+

done

lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"

by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])

lemma supp_eqs:

  "supp Type = {}"

  "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPi rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"

  "supp (TConst i) = {atom i}"

  "supp (TApp A M) = supp A \<union> supp M"

  "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPi rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"

  "supp (Const i) = {atom i}"

  "supp (Var x) = {atom x}"

  "supp (App M N) = supp M \<union> supp N"

  "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (Lam rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"

  apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm)

  apply(simp_all only: kind_ty_trm_inject Abs_eq_iff alpha_gen)

  apply(simp_all only: ex_out)

  apply(simp_all only: eqvts[symmetric])

  apply(simp_all only: Collect_neg_conj)

  apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc)

  apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc)

  apply(simp_all add: Un_left_commute)

  done

lemma supp_fv:

  "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3"

  apply(induct rule: kind_ty_trm_induct)

  apply(simp_all (no_asm) only: supp_eqs kind_ty_trm_fv)

  apply(simp_all)

  apply(simp_all add: supp_eqs)

  apply(simp_all add: supp_Abs)

  done

lemma supp_rkind_rty_rtrm:

  "supp Type = {}"

  "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 (Const 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 add: supp_fv kind_ty_trm_fv)

end