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>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 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
alpha_rkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
and alpha_rty :: "rty \<Rightarrow> rty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)
and alpha_rtrm :: "rtrm \<Rightarrow> rtrm \<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 alpha_rkind fv_rkind 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 alpha_rty fv_rty 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 alpha_rtrm fv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
lemma alpha_rkind_alpha_rty_alpha_rtrm_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 alpha_rkind fv_rkind 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 alpha_rty fv_rty 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 alpha_rtrm fv_rtrm pi ({atom b}, M'))))"
apply -
apply (simp add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply rule apply (erule alpha_rkind.cases) apply simp apply blast
apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply rule apply (erule alpha_rty.cases) apply simp apply simp apply simp
apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply rule apply (erule alpha_rty.cases) apply simp apply simp apply simp
apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply rule apply (erule alpha_rty.cases) apply simp apply simp apply blast
apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
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)"
"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
lemma al_refl:
fixes K::"rkind"
and A::"rty"
and M::"rtrm"
shows "K \<approx>ki K"
and "A \<approx>ty A"
and "M \<approx>tr M"
apply(induct K and A and M rule: rkind_rty_rtrm.inducts)
apply(auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2))
apply auto
apply(rule_tac x="0" in exI)
apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5))
apply auto
apply(rule_tac x="0" in exI)
apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9))
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>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: 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(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>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: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply(erule alpha_rkind.cases)
apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
apply(erule alpha_gen_compose_trans)
apply(assumption)
apply(erule alpha_eqvt)
apply(rotate_tac 4)
apply(erule alpha_rty.cases)
apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply(rotate_tac 3)
apply(erule alpha_rty.cases)
apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
apply(erule alpha_gen_compose_trans)
apply(assumption)
apply(erule alpha_eqvt)
apply(rotate_tac 4)
apply(erule alpha_rtrm.cases)
apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply(rotate_tac 3)
apply(erule alpha_rtrm.cases)
apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
apply(erule alpha_gen_compose_trans)
apply(assumption)
apply(erule alpha_eqvt)
done
lemma alpha_equivps:
shows "equivp alpha_rkind"
and "equivp alpha_rty"
and "equivp alpha_rtrm"
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 / alpha_rkind
by (rule alpha_equivps)
quotient_type
RTY = rty / alpha_rty and
RTRM = rtrm / alpha_rtrm
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>
(t1 \<approx>ty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and>
(t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)"
apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct)
apply(simp_all add: alpha_gen)
done
lemma perm_rsp[quot_respect]:
"(op = ===> alpha_rkind ===> alpha_rkind) permute permute"
"(op = ===> alpha_rty ===> alpha_rty) permute permute"
"(op = ===> alpha_rtrm ===> alpha_rtrm) permute permute"
by (simp_all add:alpha_eqvt)
lemma tconst_rsp[quot_respect]:
"(op = ===> alpha_rty) TConst TConst"
apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
lemma tapp_rsp[quot_respect]:
"(alpha_rty ===> alpha_rtrm ===> alpha_rty) TApp TApp"
apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
lemma var_rsp[quot_respect]:
"(op = ===> alpha_rtrm) Var Var"
apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
lemma app_rsp[quot_respect]:
"(alpha_rtrm ===> alpha_rtrm ===> alpha_rtrm) App App"
apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
lemma const_rsp[quot_respect]:
"(op = ===> alpha_rtrm) Const Const"
apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
lemma kpi_rsp[quot_respect]:
"(alpha_rty ===> op = ===> alpha_rkind ===> alpha_rkind) KPi KPi"
apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2)) apply simp_all
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]:
"(alpha_rty ===> op = ===> alpha_rty ===> alpha_rty) TPi TPi"
apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5)) apply simp_all
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]:
"(alpha_rty ===> op = ===> alpha_rtrm ===> alpha_rtrm) Lam Lam"
apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9)) apply simp_all
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]:
"(alpha_rty ===> op =) fv_rty fv_rty"
by (simp add: alpha_rfv)
lemma fv_rkind_rsp[quot_respect]:
"(alpha_rkind ===> op =) fv_rkind fv_rkind"
by (simp add: alpha_rfv)
lemma fv_rtrm_rsp[quot_respect]:
"(alpha_rtrm ===> op =) fv_rtrm fv_rtrm"
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 ALPHA_RKIND_ALPHA_RTY_ALPHA_RTRM_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
lemmas RKIND_RTY_RTRM_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 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)
apply(subst swap_at_base_simps(3))
apply(simp_all add: fresh_atom)
apply(clarify)
apply(subst swap_at_base_simps(3))
apply(simp_all add: fresh_atom)
done
lemma RKIND_RTY_RTRM_fs:
"finite (supp (x\<Colon>RKIND))"
"finite (supp (y\<Colon>RTY))"
"finite (supp (z\<Colon>RTRM))"
apply(induct x and y and z rule: RKIND_RTY_RTRM_inducts)
apply(simp_all add: supp_rkind_rty_rtrm_easy)
apply(rule supports_finite)
apply(rule supp_bind(1))
apply(simp add: supp_Pair supp_atom)
apply(rule supports_finite)
apply(rule supp_bind(2))
apply(simp add: supp_Pair supp_atom)
apply(rule supports_finite)
apply(rule supp_bind(3))
apply(simp add: supp_Pair supp_atom)
done
instance RKIND and RTY and RTRM :: fs
apply(default)
apply(simp_all only: RKIND_RTY_RTRM_fs)
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: RKIND_RTY_RTRM_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 add: supp_Abs Set.Un_commute)
apply(simp (no_asm) add: supp_def)
apply(simp add: RKIND_RTY_RTRM_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 add: supp_Abs Set.Un_commute)
apply(simp (no_asm) add: supp_def)
apply(simp add: RKIND_RTY_RTRM_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 add: supp_Abs Set.Un_commute)
apply(simp (no_asm) add: supp_def)
apply(simp add: RKIND_RTY_RTRM_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 *)
lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
apply (simp add: permute_set_eq supp_def Abs_eq_iff RKIND_RTY_RTRM_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