Theory EtaNorm
section "Eta Normalization"
theory EtaNorm
imports Term BetaNorm
begin
inductive
eta :: "term ⇒ term ⇒ bool" (infixl "→⇩η" 50)
where
eta [simp, intro]: "¬ is_dependent s ⟹ Abs T (s $ Bv 0) →⇩η decr 0 s"
| appL [simp, intro]: "s →⇩η t ⟹ s $ u →⇩η t $ u"
| appR [simp, intro]: "s →⇩η t ⟹ u $ s →⇩η u $ t"
| abs [simp, intro]: "s →⇩η t ⟹ Abs T s →⇩η Abs T t"
abbreviation
eta_reds :: "term ⇒ term ⇒ bool" (infixl "→⇩η⇧*" 50) where
"s →⇩η⇧* t ≡ eta⇧*⇧* s t"
abbreviation
eta_red0 :: "term ⇒ term ⇒ bool" (infixl "→⇩η⇧=" 50) where
"s →⇩η⇧= t ≡ eta⇧=⇧= s t"
inductive_cases eta_cases [elim!]:
"Abs T s →⇩η z"
"s $ t →⇩η u"
"Bv i →⇩η t"
lemma subst_bv2_not_free [simp]: "¬ loose_bvar1 s i ⟹ subst_bv2 s i t = subst_bv2 s i u"
by (induction s arbitrary: i t u) (simp_all add:)
lemma free_lift [simp]:
"loose_bvar1 (lift t k) i = (i < k ∧ loose_bvar1 t i ∨ k < i ∧ loose_bvar1 t (i - 1))"
by (induct t arbitrary: i k) (auto cong: conj_cong)
lemma free_subst_bv2 [simp]:
"loose_bvar1 (subst_bv2 s k t) i =
(loose_bvar1 s k ∧ loose_bvar1 t i ∨ loose_bvar1 s (if i < k then i else i + 1))"
apply (induct s arbitrary: i k t)
using free_lift apply (simp_all add: diff_Suc split: nat.split)
by blast
lemma free_eta: "s →⇩η t ⟹ loose_bvar1 t i = loose_bvar1 s i"
apply (induct arbitrary: i set: eta)
apply (simp_all cong: conj_cong)
using is_dependent_def loose_bvar1_decr''' loose_bvar1_decr'''' by blast
lemma not_free_eta:
"s →⇩η t ⟹ ¬ loose_bvar1 s i ⟹ ¬ loose_bvar1 t i"
by (simp add: free_eta)
lemma no_loose_bvar1_subst_bv2_decr: "¬ loose_bvar1 t i ⟹ subst_bv2 t i x = decr i t"
by (induction t i x rule: subst_bv2.induct) auto
lemma eta_subst_bv2 [simp]:
"s →⇩η t ⟹ subst_bv2 s i u →⇩η subst_bv2 t i u"
proof (induction s t arbitrary: u i rule: eta.induct)
case (eta s T)
hence 1: "¬ loose_bvar1 s 0"
using is_dependent_def by simp
have "decr 0 s = subst_bv2 s 0 dummy" for dummy
using no_loose_bvar1_subst_bv2_decr[symmetric, OF 1, of dummy] .
from this obtain dummy where dummy: "decr 0 s = subst_bv2 s 0 dummy"
by simp
show ?case
using 1 apply (simp add: dummy subst_bv2_subst_bv2 [symmetric])
using free_lift is_dependent_def no_loose_bvar1_subst_bv2_decr by auto
qed auto
theorem lift_subst_bv2_dummy: "¬ loose_bvar s i ⟹ lift (decr i s) i = s"
by (induct s arbitrary: i) simp_all
lemma decr_is_closed[simp]: "is_closed t ⟹ decr lev t = t"
by (metis is_open_def lift_subst_bv2_dummy lift_def loose_bvar_Suc loose_bvar_incr_bvar no_loose_bvar_no_incr zero_induct)
lemma eta_reducible_imp_eta_step: "eta_reducible t ⟹ ∃t'. t →⇩η t'"
by (induction t rule: eta_reducible.induct) auto
lemma eta_step_imp_eta_reducible: "t →⇩η t' ⟹ eta_reducible t"
proof (induction t t' rule: eta.induct)
case (abs s t T)
show ?case
proof(cases s)
case (App u v)
then show ?thesis by (cases v; use abs eta_reducible_Abs in metis)
qed (use abs in auto)
qed auto
lemma eta_reds_appR: "s →⇩η⇧* t ⟹ u $ s →⇩η⇧* u $ t"
by (induction s t rule: rtranclp.induct) (auto simp add: rtranclp.rtrancl_into_rtrancl)
lemma eta_reds_appL: "s →⇩η⇧* t ⟹ s $ u →⇩η⇧* t $ u"
by (induction s t rule: rtranclp.induct) (auto simp add: rtranclp.rtrancl_into_rtrancl)
lemma eta_reds_abs: "s →⇩η⇧* t ⟹ Abs T s →⇩η⇧* Abs T t"
by (induction s t rule: rtranclp.induct) (auto simp add: rtranclp.rtrancl_into_rtrancl)
lemma eta_norm_imp_eta_reds: assumes "eta_norm t = t'" shows "t →⇩η⇧* t'"
using assms proof (induction t arbitrary: t' rule: eta_norm.induct)
case (1 T body)
then show ?case
proof (cases "eta_norm body")
case (App f u)
then show ?thesis
using 1 apply (clarsimp simp add: is_dependent_def eta_reds_abs split: term.splits nat.splits if_splits)
by (metis eta.eta eta_reds_abs eta_reducible.simps(11) is_dependent_def
not_eta_reducible_eta_norm not_eta_reducible_imp_eta_norm_no_change rtranclp.simps)
qed (auto simp add: is_dependent_def eta_reds_abs split: term.splits nat.splits if_splits)
next
case (2 f u)
hence "f →⇩η⇧* eta_norm f" "u →⇩η⇧* eta_norm u"
by simp_all
then show ?case using 2
by (metis eta_norm.simps(2) eta_reds_appL eta_reds_appR rtranclp_trans)
qed auto
lemma rtrancl_eta_App:
"s →⇩η⇧* s' ⟹ t →⇩η⇧* t' ⟹ s $ t →⇩η⇧* s' $ t'"
by (blast intro!: eta_reds_appR eta_reds_appL intro: rtranclp_trans)
lemma eta_preserves_typ_of1: "t →⇩η t' ⟹ typ_of1 Ts t = Some τ ⟹ typ_of1 Ts t' = Some τ"
proof (induction Ts t arbitrary: τ t' rule: typ_of1.induct)
case (1 uu uv T)
then show ?case
using eta_step_imp_eta_reducible by fastforce
next
case (2 Ts i)
then show ?case
using eta_step_imp_eta_reducible by fastforce
next
case (3 uw ux T)
then show ?case
using eta_step_imp_eta_reducible by fastforce
next
case (4 Ts T body)
then show ?case
proof(cases body)
case (Abs B b)
then show ?thesis using 4
by (metis eta_cases(1) term.distinct(19) typ_of1.simps(4) typ_of_Abs_body_typ')
next
case (App u v)
note oApp = App
then show ?thesis
proof(cases "is_dependent u")
case True
then show ?thesis
by (metis "4.IH" "4.prems"(1) "4.prems"(2) App eta_cases(1) term.inject(5)
typ_of1.simps(4) typ_of_Abs_body_typ')
next
case False
then show ?thesis
proof(cases v)
case (Ct n T)
then show ?thesis
using 4 oApp False typ_of_Abs_body_typ'
by (metis eta_cases(1) term.distinct(3) term.inject(5) typ_of1.simps(4))
next
case (Fv n T)
then show ?thesis
using 4 oApp False typ_of_Abs_body_typ'
by (metis eta_cases(1) term.distinct(9) term.inject(5) typ_of1.simps(4))
next
case (Bv n)
then show ?thesis
proof(cases n)
case 0 thm 4
show ?thesis
proof(cases rule: eta_cases(1)[OF "4.prems"(1)])
case (1 s)
thm "4"(3)
obtain rty where "typ_of1 (T#Ts) (s $ Bv 0) = Some (rty)"
using typ_of_Abs_body_typ'[OF "4"(3)] "1"(3) "1"(1) by blast
moreover have "τ = T → rty"
by (metis "1"(1) "4.prems"(2) calculation option.inject typ_of_Abs_body_typ')
ultimately have "typ_of1 (T#Ts) s = Some τ"
using typ_of1_arg_typ
by (metis length_Cons nth_Cons_0 typ_of1.simps(2) zero_less_Suc)
hence "typ_of1 Ts (decr 0 s) = Some τ"
by (metis "1"(3) append_Cons append_Nil is_dependent_def list.size(3) typ_of1_decr)
then show ?thesis
using 1 oApp False typ_of_Abs_body_typ' Bv 0 by auto
next
case (2 t)
then show ?thesis
using oApp False typ_of_Abs_body_typ' Bv 0
by (metis "4.IH" "4.prems"(2) typ_of1.simps(4))
qed
next
case (Suc nat)
then show ?thesis
using 4 oApp False typ_of_Abs_body_typ' Bv
apply -
apply (rule eta_cases(1)[of T body t'])
apply blast
apply blast
apply (metis "4.IH" "4.prems"(2) typ_of1.simps(4))
done
qed
next
case (Abs T t)
then show ?thesis
using 4 oApp False typ_of_Abs_body_typ'
apply -
apply (erule eta.cases(1))
by (metis term.distinct(15) term.distinct(19) term.inject(4) term.inject(5)
typ_of1.simps(4))+
next
case (App f u)
then show ?thesis
using 4 oApp False typ_of_Abs_body_typ'
by (metis eta_cases(1) term.distinct(17) term.inject(5) typ_of1.simps(4))
qed
qed
qed (use 4 in auto)
next
case (5 Ts f u)
then show ?case
by (smt bind.bind_lunit eta_cases(2) typ_of1.simps(5) typ_of1_split_App_obtains)
qed
lemma eta_preserves_typ_of: "t →⇩η t' ⟹ typ_of t = Some τ ⟹ typ_of t' = Some τ"
using eta_preserves_typ_of1 typ_of_def by simp
lemma eta_star_preserves_typ_of1: "r →⇩η⇧* s ⟹ typ_of1 Ts r = Some T ⟹ typ_of1 Ts s = Some T"
proof (induction rule: rtranclp.induct)
case (rtrancl_refl a)
then show ?case
by simp
next
case (rtrancl_into_rtrancl a b c)
then show ?case
using eta_preserves_typ_of1 by blast
qed
lemma eta_star_preserves_typ_of: "r →⇩η⇧* s ⟹ typ_of r = Some T ⟹ typ_of s = Some T"
using eta_star_preserves_typ_of1 typ_of_def by simp
lemma subst_bvs1'_decr: "∀x∈set us. is_closed x ⟹ ¬ loose_bvar1 t k
⟹ subst_bvs1' (decr k t) k us = decr k (subst_bvs1' t (Suc k) us)"
by (induction k t arbitrary: us rule: decr.induct) (auto simp add: is_open_def)
lemma subst_bvs_decr: "∀x∈set us. is_closed x ⟹ ¬ is_dependent t
⟹ subst_bvs us (decr 0 t) = decr 0 (subst_bvs1' t 1 us)"
by (simp add: is_dependent_def subst_bvs1'_decr subst_bvs_subst_bvs1')
end