Theory Beta_Eta
subsection ‹Combined beta and eta reduction of lambda terms›
theory Beta_Eta
imports "HOL-Proofs-Lambda.Eta" Joinable
begin
subsubsection ‹Auxiliary lemmas›
lemma liftn_lift_swap: "liftn n (lift t k) k = lift (liftn n t k) k"
by (induction n) simp_all
lemma subst_liftn:
"i ≤ n + k ∧ k ≤ i ⟹ (liftn (Suc n) s k)[t/i] = liftn n s k"
by (induction s arbitrary: i k t) auto
lemma subst_lift2[simp]: "(lift (lift t 0) 0)[x/Suc 0] = lift t 0"
proof -
have "lift (lift t 0) 0 = lift (lift t 0) (Suc 0)" using lift_lift by simp
thus ?thesis by simp
qed
lemma free_liftn:
"free (liftn n t k) i = (i < k ∧ free t i ∨ k + n ≤ i ∧ free t (i - n))"
by (induction t arbitrary: k i) (auto simp add: Suc_diff_le)
subsubsection ‹Reduction›
abbreviation beta_eta :: "dB ⇒ dB ⇒ bool" (infixl "→⇩β⇩η" 50)
where "beta_eta ≡ sup beta eta"
abbreviation beta_eta_reds :: "dB ⇒ dB ⇒ bool" (infixl "→⇩β⇩η⇧*" 50)
where "s →⇩β⇩η⇧* t ≡ (beta_eta)⇧*⇧* s t"
lemma beta_into_beta_eta_reds: "s →⇩β t ⟹ s →⇩β⇩η⇧* t"
by auto
lemma eta_into_beta_eta_reds: "s →⇩η t ⟹ s →⇩β⇩η⇧* t"
by auto
lemma beta_reds_into_beta_eta_reds: "s →⇩β⇧* t ⟹ s →⇩β⇩η⇧* t"
by (auto intro: rtranclp_mono[THEN predicate2D])
lemma eta_reds_into_beta_eta_reds: "s →⇩η⇧* t ⟹ s →⇩β⇩η⇧* t"
by (auto intro: rtranclp_mono[THEN predicate2D])
lemma beta_eta_appL[intro]: "s →⇩β⇩η⇧* s' ⟹ s ° t →⇩β⇩η⇧* s' ° t"
by (induction set: rtranclp) (auto intro: rtranclp.rtrancl_into_rtrancl)
lemma beta_eta_appR[intro]: "t →⇩β⇩η⇧* t' ⟹ s ° t →⇩β⇩η⇧* s ° t'"
by (induction set: rtranclp) (auto intro: rtranclp.rtrancl_into_rtrancl)
lemma beta_eta_abs[intro]: "t →⇩β⇩η⇧* t' ⟹ Abs t →⇩β⇩η⇧* Abs t'"
by (induction set: rtranclp) (auto intro: rtranclp.rtrancl_into_rtrancl)
lemma beta_eta_lift: "s →⇩β⇩η⇧* t ⟹ lift s k →⇩β⇩η⇧* lift t k"
proof (induction pred: rtranclp)
case base show ?case ..
next
case (step y z)
hence "lift y k →⇩β⇩η lift z k" using lift_preserves_beta eta_lift by blast
with step.IH show "lift s k →⇩β⇩η⇧* lift z k" by iprover
qed
lemma confluent_beta_eta_reds: "Joinable.confluent {(s, t). s →⇩β⇩η⇧* t}"
using confluent_beta_eta
unfolding diamond_def commute_def square_def
by (blast intro!: confluentI)
subsubsection ‹Equivalence›
text ‹Terms are equivalent iff they can be reduced to a common term.›
definition term_equiv :: "dB ⇒ dB ⇒ bool" (infixl "↔" 50)
where "term_equiv = joinablep beta_eta_reds"
lemma term_equivI:
assumes "s →⇩β⇩η⇧* u" and "t →⇩β⇩η⇧* u"
shows "s ↔ t"
using assms unfolding term_equiv_def by (rule joinableI[to_pred])
lemma term_equivE:
assumes "s ↔ t"
obtains u where "s →⇩β⇩η⇧* u" and "t →⇩β⇩η⇧* u"
using assms unfolding term_equiv_def by (rule joinableE[to_pred])
lemma reds_into_equiv[elim]: "s →⇩β⇩η⇧* t ⟹ s ↔ t"
by (blast intro: term_equivI)
lemma beta_into_equiv[elim]: "s →⇩β t ⟹ s ↔ t"
by (rule reds_into_equiv) (rule beta_into_beta_eta_reds)
lemma eta_into_equiv[elim]: "s →⇩η t ⟹ s ↔ t"
by (rule reds_into_equiv) (rule eta_into_beta_eta_reds)
lemma beta_reds_into_equiv[elim]: "s →⇩β⇧* t ⟹ s ↔ t"
by (rule reds_into_equiv) (rule beta_reds_into_beta_eta_reds)
lemma eta_reds_into_equiv[elim]: "s →⇩η⇧* t ⟹ s ↔ t"
by (rule reds_into_equiv) (rule eta_reds_into_beta_eta_reds)
lemma term_refl[iff]: "t ↔ t"
unfolding term_equiv_def by (blast intro: joinablep_refl reflpI)
lemma term_sym[sym]: "(s ↔ t) ⟹ (t ↔ s)"
unfolding term_equiv_def by (rule joinable_sym[to_pred])
lemma conversep_term [simp]: "conversep (↔) = (↔)"
by (auto simp add: fun_eq_iff intro: term_sym)
lemma term_trans[trans]: "s ↔ t ⟹ t ↔ u ⟹ s ↔ u"
unfolding term_equiv_def
using trans_joinable[to_pred] trans_rtrancl[to_pred] confluent_beta_eta_reds
by (blast elim: transpE)
lemma term_beta_trans[trans]: "s ↔ t ⟹ t →⇩β u ⟹ s ↔ u"
by (fast dest!: beta_into_beta_eta_reds intro: term_trans)
lemma term_eta_trans[trans]: "s ↔ t ⟹ t →⇩η u ⟹ s ↔ u"
by (fast dest!: eta_into_beta_eta_reds intro: term_trans)
lemma equiv_appL[intro]: "s ↔ s' ⟹ s ° t ↔ s' ° t"
unfolding term_equiv_def using beta_eta_appL
by (iprover intro: joinable_subst[to_pred])
lemma equiv_appR[intro]: "t ↔ t' ⟹ s ° t ↔ s ° t'"
unfolding term_equiv_def using beta_eta_appR
by (iprover intro: joinable_subst[to_pred])
lemma equiv_app: "s ↔ s' ⟹ t ↔ t' ⟹ s ° t ↔ s' ° t'"
by (blast intro: term_trans)
lemma equiv_abs[intro]: "t ↔ t' ⟹ Abs t ↔ Abs t'"
unfolding term_equiv_def using beta_eta_abs
by (iprover intro: joinable_subst[to_pred])
lemma equiv_lift: "s ↔ t ⟹ lift s k ↔ lift t k"
by (auto intro: term_equivI beta_eta_lift elim: term_equivE)
lemma equiv_liftn: "s ↔ t ⟹ liftn n s k ↔ liftn n t k"
by (induction n) (auto intro: equiv_lift)
text ‹Our definition is equivalent to the the symmetric and transitive closure of
the reduction relation.›
lemma equiv_eq_rtscl_reds: "term_equiv = (sup beta_eta beta_eta¯¯)⇧*⇧*"
unfolding term_equiv_def
using confluent_beta_eta_reds
by (rule joinable_eq_rtscl[to_pred])
end