theory lambda
imports Pure
begin

setup Pure_Thy.old_appl_syntax_setup

typedecl "term"

lemma [trans]: assumes st: "s == t"
  shows "PROP P(t) ==> PROP P(s)"
  by (unfold st)

lemma [trans]: 
  assumes ps: "PROP P(s)"
  assumes st: "s == t"
  shows "PROP P(t)"
  using ps by (unfold st)

locale RED =
fixes abs :: "[term \<Rightarrow> term] \<Rightarrow> term" (binder "lam " 10)
fixes "apply" :: "[term, term] \<Rightarrow> term" (infixl "^" 20)
fixes K   :: "term"
fixes I   :: "term"
fixes S   :: "term"
fixes B   :: "term"
fixes YC  :: "term"
fixes YT  :: "term"
fixes Red :: "[term, term] \<Rightarrow> prop" ("(_ >--> _)")
assumes K_def : "K \<equiv> lam x. (lam y. x)"
assumes I_def : "I \<equiv> lam x. x"
assumes S_def : "S \<equiv> lam x. (lam y. (lam z. x^z^(y^z)))"
assumes B_def : "B \<equiv> S^(K^S)^K"
assumes YC_def: "YC \<equiv> lam f. ((lam x. f^(x^x))^(lam x. f^(x^x)))"
assumes YT_def: "YT \<equiv> (lam z. lam x. x^(z^z^x))^(lam z. lam x. x^(z^z^x))"
assumes beta : "(lam x. f (x))^a >--> f(a)"
assumes refl : "M >--> M"
assumes trans[trans]: "\<lbrakk> M >--> N; N >--> L \<rbrakk> \<Longrightarrow> M >--> L"
assumes appr : "M >--> N \<Longrightarrow> M^Z >--> N^Z"
assumes appl : "M >--> N \<Longrightarrow> Z^M >--> Z^N"
assumes epsi : "\<lbrakk> !! x. P(x) >--> Q(x) \<rbrakk> \<Longrightarrow> (lam x. P(x)) >--> (lam x. Q(x))"
begin
notation (output)
  "abs" (binder "\<lambda> " 10)
end

locale CONV = RED +
fixes Conv :: "[term, term] \<Rightarrow> prop" ("(_ >=< _)")
assumes beta : "(lam x. f (x))^a >=< f(a)"
assumes refl : "M >=< M"
assumes symm[sym] : "M >=< N \<Longrightarrow> N >=< M"
assumes trans[trans]: "\<lbrakk> M >=< N; N >=< L \<rbrakk> \<Longrightarrow> M >=< L"
assumes appr : "M >=< N \<Longrightarrow> M^Z >=< N^Z"
assumes appl : "M >=< N \<Longrightarrow> Z^M >=< Z^N"
assumes epsi : "\<lbrakk> !! x. P(x) >=< Q(x) \<rbrakk> \<Longrightarrow> lam x. P(x) >=< lam x. Q(x)"
begin
lemmas beta_red = RED.beta[OF RED_axioms] and
       appr_red = RED.appr[OF RED_axioms] and
       appl_red = RED.appl[OF RED_axioms] and
       epsi_red = RED.epsi[OF RED_axioms] and
       trans_red = RED.trans[OF RED_axioms] and
       refl_red = RED.refl[OF RED_axioms]
end

end