Theory Beta_Eta

(* Author: Joshua Schneider, ETH Zurich *)

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