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