Theory CL_Z

(*
 * Title:      Z  
 * Author:     Bertram Felgenhauer (2016)
 * Author:     Julian Nagele (2016)
 * Author:     Vincent van Oostrom (2016)
 * Author:     Christian Sternagel (2016)
 * Maintainer: Bertram Felgenhauer <bertram.felgenhauer@uibk.ac.at>
 * Maintainer: Juilan Nagele <julian.nagele@uibk.ac.at>
 * Maintainer: Christian Sternagel <c.sternagel@gmail.com>
 * License:    BSD
 *)

section ‹Combinatory Logic has the Church-Rosser property›

theory CL_Z imports Z
begin

datatype CL = S | K | I | App CL CL ("` _ _" [999, 999] 999)

inductive_set red :: "CL rel" where
  L: "(t, t') ∈ red ⟹ (` t u, ` t' u) ∈ red"
| R: "(u, u') ∈ red ⟹ (` t u, ` t u') ∈ red"
| S: "(` ` ` S x y z, ` ` x z ` y z) ∈ red"
| K: "(` ` K x y, x) ∈ red"
| I: "(` I x, x) ∈ red"

lemma App_mono:
  "(t, t') ∈ red⇧* ⟹ (u, u') ∈ red⇧* ⟹ (` t u, ` t' u') ∈ red⇧*"
proof -
  assume "(t, t') ∈ red⇧*" hence "(` t u, ` t' u) ∈ red⇧*"
    by (induct t' rule: rtrancl_induct) (auto intro: rtrancl_into_rtrancl red.intros)
  moreover assume "(u, u') ∈ red⇧*" hence "(` t' u, ` t' u') ∈ red⇧*"
    by (induct u' rule: rtrancl_induct) (auto intro: rtrancl_into_rtrancl red.intros)
  ultimately show ?thesis by auto
qed

fun bullet_app :: "CL ⇒ CL ⇒ CL" where
  "bullet_app (` ` S x y) z = ` ` x z ` y z"
| "bullet_app (` K x) y = x"
| "bullet_app I x = x"
| "bullet_app t u = ` t u"

lemma bullet_app_red:
  "(` t u, bullet_app t u) ∈ red⇧="
by (induct t u rule: bullet_app.induct) (auto intro: red.intros)

lemma bullet_app_redsI:
  "(s, ` t u) ∈ red⇧* ⟹ (s, bullet_app t u) ∈ red⇧*"
using bullet_app_red[of t u] by auto

lemma bullet_app_redL:
  "(t, t') ∈ red ⟹ (bullet_app t u, bullet_app t' u) ∈ red⇧*"
by (induct t u rule: bullet_app.induct)
   (auto 0 6 intro: App_mono bullet_app_redsI elim: red.cases simp only: bullet_app.simps)

lemma bullet_app_redR:
  "(u, u') ∈ red ⟹ (bullet_app t u, bullet_app t u') ∈ red⇧*"
by (induct t u rule: bullet_app.induct) (auto intro: App_mono)

lemma bullet_app_mono:
  assumes "(t, t') ∈ red⇧*" "(u, u') ∈ red⇧*" shows "(bullet_app t u, bullet_app t' u') ∈ red⇧*"
proof -
  have "(bullet_app t u, bullet_app t' u) ∈ red⇧*" using assms(1)
    by (induct t' rule: rtrancl_induct) (auto intro: rtrancl_trans bullet_app_redL)
  moreover have "(bullet_app t' u, bullet_app t' u') ∈ red⇧*" using assms(2)
    by (induct u' rule: rtrancl_induct) (auto intro: rtrancl_trans bullet_app_redR)
  ultimately show ?thesis by auto
qed

fun bullet :: "CL ⇒ CL" where
  "bullet (` t u) = bullet_app (bullet t) (bullet u)"
| "bullet t = t"

lemma bullet_incremental:
  "(t, bullet t) ∈ red⇧*"
by (induct t rule: bullet.induct) (auto intro: App_mono bullet_app_redsI)

interpretation CL:z_property bullet red
proof (unfold_locales, intro conjI)
  fix t u assume "(t, u) ∈ red" thus "(u, bullet t) ∈ red⇧*"
  proof (induct t arbitrary: u rule: bullet.induct)
    case (1 t1 t2) show ?case using 1(3)
      by (cases) (auto intro: 1 App_mono bullet_app_redsI bullet_incremental)
  qed (auto elim: red.cases)
next
  fix t u assume "(t, u) ∈ red" thus "(bullet t, bullet u) ∈ red⇧*"
    by (induct t u rule: red.induct) (auto intro: App_mono bullet_app_mono bullet_app_redsI)
qed

lemmas CR_red = CL.CR

end