Bindings adapted to multiple defined datatypes.
theory LFex
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
begin
atom_decl name
atom_decl ident
datatype kind =
Type
| KPi "ty" "name" "kind"
and ty =
TConst "ident"
| TApp "ty" "trm"
| TPi "ty" "name" "ty"
and trm =
Const "ident"
| Var "name"
| App "trm" "trm"
| Lam "ty" "name" "trm"
primrec
rfv_kind :: "kind \<Rightarrow> atom set"
and rfv_ty :: "ty \<Rightarrow> atom set"
and rfv_trm :: "trm \<Rightarrow> atom set"
where
"rfv_kind (Type) = {}"
| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
| "rfv_ty (TConst i) = {atom i}"
| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
| "rfv_trm (Const i) = {atom i}"
| "rfv_trm (Var x) = {atom x}"
| "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
instantiation kind and ty and trm :: pt
begin
primrec
permute_kind
and permute_ty
and permute_trm
where
"permute_kind pi Type = Type"
| "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \<bullet> n) (permute_kind pi k)"
| "permute_ty pi (TConst i) = TConst (pi \<bullet> i)"
| "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)"
| "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \<bullet> x) (permute_ty pi B)"
| "permute_trm pi (Const i) = Const (pi \<bullet> i)"
| "permute_trm pi (Var x) = Var (pi \<bullet> x)"
| "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)"
| "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)"
lemma rperm_zero_ok:
"0 \<bullet> (x :: kind) = x"
"0 \<bullet> (y :: ty) = y"
"0 \<bullet> (z :: trm) = z"
apply(induct x and y and z rule: kind_ty_trm.inducts)
apply(simp_all)
done
lemma rperm_plus_ok:
"(p + q) \<bullet> (x :: kind) = p \<bullet> q \<bullet> x"
"(p + q) \<bullet> (y :: ty) = p \<bullet> q \<bullet> y"
"(p + q) \<bullet> (z :: trm) = p \<bullet> q \<bullet> z"
apply(induct x and y and z rule: kind_ty_trm.inducts)
apply(simp_all)
done
instance
apply default
apply (simp_all only:rperm_zero_ok rperm_plus_ok)
done
end
inductive
akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)
and atrm :: "trm \<Rightarrow> trm \<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 akind rfv_kind 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 aty rfv_ty 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 atrm rfv_trm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
lemma akind_aty_atrm_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 akind rfv_kind 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 aty rfv_ty 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 atrm rfv_trm pi ({atom b}, M'))))"
apply -
apply (simp add: akind_aty_atrm.intros)
apply rule apply (erule akind.cases) apply simp apply blast
apply (simp only: akind_aty_atrm.intros)
apply rule apply (erule aty.cases) apply simp apply simp apply simp
apply (simp only: akind_aty_atrm.intros)
apply rule apply (erule aty.cases) apply simp apply simp apply simp
apply (simp only: akind_aty_atrm.intros)
apply rule apply (erule aty.cases) apply simp apply simp apply blast
apply (simp only: akind_aty_atrm.intros)
apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: akind_aty_atrm.intros)
apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: akind_aty_atrm.intros)
apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: akind_aty_atrm.intros)
apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: akind_aty_atrm.intros)
done
lemma rfv_eqvt[eqvt]:
"((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
"((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
"((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
apply(induct t1 and t2 and t3 rule: kind_ty_trm.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: akind_aty_atrm.inducts)
apply (simp_all add: akind_aty_atrm.intros)
apply (simp_all add: akind_aty_atrm_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::"kind"
and A::"ty"
and M::"trm"
shows "K \<approx>ki K"
and "A \<approx>ty A"
and "M \<approx>tr M"
apply(induct K and A and M rule: kind_ty_trm.inducts)
apply(auto intro: akind_aty_atrm.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'::"kind" and A A'::"ty" and M M'::"trm"
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: akind_aty_atrm.inducts)
apply(simp_all add: akind_aty_atrm.intros)
apply (simp_all add: akind_aty_atrm_inj)
apply(rule alpha_gen_atom_sym)
apply(rule alpha_eqvt)
apply(assumption)+
apply(rule alpha_gen_atom_sym)
apply(rule alpha_eqvt)
apply(assumption)+
apply(rule alpha_gen_atom_sym)
apply(rule alpha_eqvt)
apply(assumption)+
done
lemma al_trans:
fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm"
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: akind_aty_atrm.inducts)
apply(simp_all add: akind_aty_atrm.intros)
apply(erule akind.cases)
apply(simp_all add: akind_aty_atrm.intros)
apply(simp add: akind_aty_atrm_inj)
apply(rule alpha_gen_atom_trans)
apply(rule alpha_eqvt)
apply(assumption)+
apply(rotate_tac 4)
apply(erule aty.cases)
apply(simp_all add: akind_aty_atrm.intros)
apply(rotate_tac 3)
apply(erule aty.cases)
apply(simp_all add: akind_aty_atrm.intros)
apply(simp add: akind_aty_atrm_inj)
apply(rule alpha_gen_atom_trans)
apply(rule alpha_eqvt)
apply(assumption)+
apply(rotate_tac 4)
apply(erule atrm.cases)
apply(simp_all add: akind_aty_atrm.intros)
apply(rotate_tac 3)
apply(erule atrm.cases)
apply(simp_all add: akind_aty_atrm.intros)
apply(simp add: akind_aty_atrm_inj)
apply(rule alpha_gen_atom_trans)
apply(rule alpha_eqvt)
apply(assumption)+
done
lemma alpha_equivps:
shows "equivp akind"
and "equivp aty"
and "equivp atrm"
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 KIND = kind / akind
by (rule alpha_equivps)
quotient_type
TY = ty / aty and
TRM = trm / atrm
by (auto intro: alpha_equivps)
quotient_definition
"TYP :: KIND"
is
"Type"
quotient_definition
"KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
is
"KPi"
quotient_definition
"TCONST :: ident \<Rightarrow> TY"
is
"TConst"
quotient_definition
"TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
is
"TApp"
quotient_definition
"TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
is
"TPi"
(* FIXME: does not work with CONST *)
quotient_definition
"CONS :: ident \<Rightarrow> TRM"
is
"Const"
quotient_definition
"VAR :: name \<Rightarrow> TRM"
is
"Var"
quotient_definition
"APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
is
"App"
quotient_definition
"LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
is
"Lam"
(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
quotient_definition
"fv_kind :: KIND \<Rightarrow> atom set"
is
"rfv_kind"
quotient_definition
"fv_ty :: TY \<Rightarrow> atom set"
is
"rfv_ty"
quotient_definition
"fv_trm :: TRM \<Rightarrow> atom set"
is
"rfv_trm"
lemma alpha_rfv:
shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
(t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
(t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
apply(rule akind_aty_atrm.induct)
apply(simp_all add: alpha_gen)
done
lemma perm_rsp[quot_respect]:
"(op = ===> akind ===> akind) permute permute"
"(op = ===> aty ===> aty) permute permute"
"(op = ===> atrm ===> atrm) permute permute"
by (simp_all add:alpha_eqvt)
lemma tconst_rsp[quot_respect]:
"(op = ===> aty) TConst TConst"
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
lemma tapp_rsp[quot_respect]:
"(aty ===> atrm ===> aty) TApp TApp"
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
lemma var_rsp[quot_respect]:
"(op = ===> atrm) Var Var"
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
lemma app_rsp[quot_respect]:
"(atrm ===> atrm ===> atrm) App App"
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
lemma const_rsp[quot_respect]:
"(op = ===> atrm) Const Const"
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
lemma kpi_rsp[quot_respect]:
"(aty ===> op = ===> akind ===> akind) 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]:
"(aty ===> op = ===> aty ===> aty) 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]:
"(aty ===> op = ===> atrm ===> atrm) 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
lemma rfv_ty_rsp[quot_respect]:
"(aty ===> op =) rfv_ty rfv_ty"
by (simp add: alpha_rfv)
lemma rfv_kind_rsp[quot_respect]:
"(akind ===> op =) rfv_kind rfv_kind"
by (simp add: alpha_rfv)
lemma rfv_trm_rsp[quot_respect]:
"(atrm ===> op =) rfv_trm rfv_trm"
by (simp add: alpha_rfv)
thm kind_ty_trm.induct
lemmas KIND_TY_TRM_induct = kind_ty_trm.induct[quot_lifted]
thm kind_ty_trm.inducts
lemmas KIND_TY_TRM_inducts = kind_ty_trm.inducts[quot_lifted]
instantiation KIND and TY and TRM :: pt
begin
quotient_definition
"permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"
is
"permute :: perm \<Rightarrow> kind \<Rightarrow> kind"
quotient_definition
"permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
is
"permute :: perm \<Rightarrow> ty \<Rightarrow> ty"
quotient_definition
"permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
is
"permute :: perm \<Rightarrow> trm \<Rightarrow> trm"
lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.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 AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
lemmas KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
lemmas fv_kind_ty_trm = rfv_kind_rfv_ty_rfv_trm.simps[quot_lifted]
lemmas fv_eqvt = rfv_eqvt[quot_lifted]
lemma supp_kind_ty_trm_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 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_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, trm))) supports (LAM ty na trm)"
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 KIND_TY_TRM_fs:
"finite (supp (x\<Colon>KIND))"
"finite (supp (y\<Colon>TY))"
"finite (supp (z\<Colon>TRM))"
apply(induct x and y and z rule: KIND_TY_TRM_inducts)
apply(simp_all add: supp_kind_ty_trm_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 KIND and TY and TRM :: fs
apply(default)
apply(simp_all only: KIND_TY_TRM_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: KIND_TY_TRM_inducts)
apply (simp_all add: supp_kind_ty_trm_easy)
apply (simp_all add: fv_kind_ty_trm)
apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abs {atom name} kind)")
apply(simp add: supp_Abs Set.Un_commute)
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 ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)")
apply(simp add: supp_Abs Set.Un_commute)
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 ty name trm) = supp ty \<union> supp (Abs {atom name} trm)")
apply(simp add: supp_Abs Set.Un_commute)
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 *)
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 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_kind_ty_trm:
"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_kind_ty_trm_easy)
apply (simp_all only: supp_fv fv_kind_ty_trm)
done
end