Theory Combinators

(* Author: Joshua Schneider, ETH Zurich *)

subsection ‹Combinators defined as closed lambda terms›

theory Combinators
imports Beta_Eta
begin

definition I_def: "ℐ = Abs (Var 0)"
definition B_def: "ℬ = Abs (Abs (Abs (Var 2 ° (Var 1 ° Var 0))))"
definition T_def: "𝒯 = Abs (Abs (Var 0 ° Var 1))" ― ‹reverse application›

lemma I_eval: "ℐ ° x →⇩β x"
proof -
  have "ℐ ° x →⇩β Var 0[x/0]" unfolding I_def ..
  then show ?thesis by simp
qed

lemma I_equiv[iff]: "ℐ ° x ↔ x"
using I_eval ..

lemma I_closed[simp]: "liftn n ℐ k = ℐ"
unfolding I_def by simp

lemma B_eval1: "ℬ ° g →⇩β Abs (Abs (lift (lift g 0) 0 ° (Var 1 ° Var 0)))"
proof -
  have "ℬ ° g →⇩β Abs (Abs (Var 2 ° (Var 1 ° Var 0))) [g/0]" unfolding B_def ..
  then show ?thesis by (simp add: numerals)
qed

lemma B_eval2: "ℬ ° g ° f →⇩β⇧* Abs (lift g 0 ° (lift f 0 ° Var 0))"
proof -
  have "ℬ ° g ° f →⇩β⇧* Abs (Abs (lift (lift g 0) 0 ° (Var 1 ° Var 0))) ° f"
    using B_eval1 by blast
  also have "... →⇩β Abs (lift (lift g 0) 0 ° (Var 1 ° Var 0)) [f/0]" ..
  also have "... = Abs (lift g 0 ° (lift f 0 ° Var 0))" by simp
  finally show ?thesis .
qed

lemma B_eval: "ℬ ° g ° f ° x →⇩β⇧* g ° (f ° x)"
proof -
  have "ℬ ° g ° f ° x →⇩β⇧* Abs (lift g 0 ° (lift f 0 ° Var 0)) ° x"
    using B_eval2 by blast
  also have "... →⇩β (lift g 0 ° (lift f 0 ° Var 0)) [x/0]" ..
  also have "... = g ° (f ° x)" by simp
  finally show ?thesis .
qed

lemma B_equiv[iff]: "ℬ ° g ° f ° x ↔ g ° (f ° x)"
using B_eval ..

lemma B_closed[simp]: "liftn n ℬ k = ℬ"
unfolding B_def by simp

lemma T_eval1: "𝒯 ° x →⇩β Abs (Var 0 ° lift x 0)"
proof -
  have "𝒯 ° x →⇩β Abs (Var 0 ° Var 1) [x/0]" unfolding T_def ..
  then show ?thesis by simp
qed

lemma T_eval: "𝒯 ° x ° f →⇩β⇧* f ° x"
proof -
  have "𝒯 ° x ° f →⇩β⇧* Abs (Var 0 ° lift x 0) ° f"
    using T_eval1 by blast
  also have "... →⇩β (Var 0 ° lift x 0) [f/0]" ..
  also have "... = f ° x" by simp
  finally show ?thesis .
qed

lemma T_equiv[iff]: "𝒯 ° x ° f ↔ f ° x"
using T_eval ..

lemma T_closed[simp]: "liftn n 𝒯 k = 𝒯"
unfolding T_def by simp

end