# Theory CR_Takahashi

```(* Authors: Christian Urban and Mathilde Arnaud                   *)
(*                                                                *)
(* A formalisation of the Church-Rosser proof by Masako Takahashi.*)
(* This formalisation follows with some very slight exceptions    *)
(* the version of this proof given by Randy Pollack in the paper: *)
(*                                                                *)
(*  Polishing Up the Tait-Martin Löf Proof of the                 *)
(*  Church-Rosser Theorem (1995).                                 *)

theory CR_Takahashi
imports "HOL-Nominal.Nominal"
begin

atom_decl name

nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam "«name»lam" ("Lam [_]._" [100,100] 100)

nominal_primrec
subst :: "lam ⇒ name ⇒ lam ⇒ lam"  ("_[_::=_]" [100,100,100] 100)
where
"(Var x)[y::=s] = (if x=y then s else (Var x))"
| "(App t⇩1 t⇩2)[y::=s] = App (t⇩1[y::=s]) (t⇩2[y::=s])"
| "x♯(y,s) ⟹ (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(fresh_guess)+
done

lemma  subst_eqvt[eqvt]:
fixes pi::"name prm"
shows "pi∙(t1[x::=t2]) = (pi∙t1)[(pi∙x)::=(pi∙t2)]"
by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)
(auto simp add: perm_bij fresh_atm fresh_bij)

lemma forget:
shows "x♯t ⟹ t[x::=s] = t"
by (nominal_induct t avoiding: x s rule: lam.strong_induct)

lemma fresh_fact:
fixes z::"name"
shows "⟦z♯s; (z=y ∨ z♯t)⟧ ⟹ z♯t[y::=s]"
by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
(auto simp add: abs_fresh fresh_prod fresh_atm)

lemma substitution_lemma:
assumes a: "x≠y" "x♯u"
shows "t[x::=s][y::=u] = t[y::=u][x::=s[y::=u]]"
using a
by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)

lemma subst_rename:
assumes a: "y♯t"
shows "t[x::=s] = ([(y,x)]∙t)[y::=s]"
using a
by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
(auto simp add: swap_simps fresh_atm abs_fresh)

section ‹Beta-Reduction›

inductive
"Beta" :: "lam⇒lam⇒bool" (" _ ⟶⇩β _" [80,80] 80)
where
b1[intro]: "t1 ⟶⇩β t2 ⟹ App t1 s ⟶⇩β App t2 s"
| b2[intro]: "s1 ⟶⇩β s2 ⟹ App t s1 ⟶⇩β App t s2"
| b3[intro]: "t1 ⟶⇩β t2 ⟹ Lam [x].t1 ⟶⇩β Lam [x].t2"
| b4[intro]: "App (Lam [x].t) s ⟶⇩β t[x::=s]"

section ‹Transitive Closure of Beta›

inductive
"Beta_star" :: "lam⇒lam⇒bool" (" _ ⟶⇩β⇧* _" [80,80] 80)
where
bs1[intro]: "t ⟶⇩β⇧* t"
| bs2[intro]: "t ⟶⇩β s ⟹ t ⟶⇩β⇧* s"
| bs3[intro,trans]: "⟦t1⟶⇩β⇧* t2; t2 ⟶⇩β⇧* t3⟧ ⟹ t1 ⟶⇩β⇧* t3"

section ‹One-Reduction›

inductive
One :: "lam⇒lam⇒bool" (" _ ⟶⇩1 _" [80,80] 80)
where
o1[intro]: "Var x⟶⇩1 Var x"
| o2[intro]: "⟦t1⟶⇩1t2; s1⟶⇩1s2⟧ ⟹ App t1 s1 ⟶⇩1 App t2 s2"
| o3[intro]: "t1⟶⇩1t2 ⟹ Lam [x].t1 ⟶⇩1 Lam [x].t2"
| o4[intro]: "⟦x♯(s1,s2); t1⟶⇩1t2; s1⟶⇩1s2⟧ ⟹ App (Lam [x].t1) s1 ⟶⇩1 t2[x::=s2]"

equivariance One
nominal_inductive One

lemma One_refl:
shows "t ⟶⇩1 t"
by (nominal_induct t rule: lam.strong_induct) (auto)

lemma One_subst:
assumes a: "t1 ⟶⇩1 t2" "s1 ⟶⇩1 s2"
shows "t1[x::=s1] ⟶⇩1 t2[x::=s2]"
using a
by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
(auto simp add: substitution_lemma fresh_atm fresh_fact)

lemma better_o4_intro:
assumes a: "t1 ⟶⇩1 t2" "s1 ⟶⇩1 s2"
shows "App (Lam [x].t1) s1 ⟶⇩1 t2[x::=s2]"
proof -
obtain y::"name" where fs: "y♯(x,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp, blast)
have "App (Lam [x].t1) s1 = App (Lam [y].([(y,x)]∙t1)) s1" using fs
by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
also have "… ⟶⇩1  ([(y,x)]∙t2)[y::=s2]" using fs a by (auto simp add: One.eqvt)
also have "… = t2[x::=s2]" using fs by (simp add: subst_rename[symmetric])
finally show "App (Lam [x].t1) s1 ⟶⇩1 t2[x::=s2]" by simp
qed

lemma One_Var:
assumes a: "Var x ⟶⇩1 M"
shows "M = Var x"
using a by (cases rule: One.cases) (simp_all)

lemma One_Lam:
assumes a: "Lam [x].t ⟶⇩1 s" "x♯s"
shows "∃t'. s = Lam [x].t' ∧ t ⟶⇩1 t'"
using a
by (cases rule: One.strong_cases)
(auto simp add: lam.inject abs_fresh alpha)

lemma One_App:
assumes a: "App t s ⟶⇩1 r"
shows "(∃t' s'. r = App t' s' ∧ t ⟶⇩1 t' ∧ s ⟶⇩1 s') ∨
(∃x p p' s'. r = p'[x::=s'] ∧ t = Lam [x].p ∧ p ⟶⇩1 p' ∧ s ⟶⇩1 s' ∧ x♯(s,s'))"
using a by (cases rule: One.cases) (auto simp add: lam.inject)

lemma One_Redex:
assumes a: "App (Lam [x].t) s ⟶⇩1 r" "x♯(s,r)"
shows "(∃t' s'. r = App (Lam [x].t') s' ∧ t ⟶⇩1 t' ∧ s ⟶⇩1 s') ∨
(∃t' s'. r = t'[x::=s'] ∧ t ⟶⇩1 t' ∧ s ⟶⇩1 s')"
using a
by (cases rule: One.strong_cases)
(auto dest: One_Lam simp add: lam.inject abs_fresh alpha fresh_prod)

section ‹Transitive Closure of One›

inductive
"One_star" :: "lam⇒lam⇒bool" (" _ ⟶⇩1⇧* _" [80,80] 80)
where
os1[intro]: "t ⟶⇩1⇧* t"
| os2[intro]: "t ⟶⇩1 s ⟹ t ⟶⇩1⇧* s"
| os3[intro]: "⟦t1⟶⇩1⇧* t2; t2 ⟶⇩1⇧* t3⟧ ⟹ t1 ⟶⇩1⇧* t3"

section ‹Complete Development Reduction›

inductive
Dev :: "lam ⇒ lam ⇒ bool" (" _ ⟶⇩d _" [80,80]80)
where
d1[intro]: "Var x ⟶⇩d Var x"
| d2[intro]: "t ⟶⇩d s ⟹ Lam [x].t ⟶⇩d Lam[x].s"
| d3[intro]: "⟦¬(∃y t'. t1 = Lam [y].t'); t1 ⟶⇩d t2; s1 ⟶⇩d s2⟧ ⟹ App t1 s1 ⟶⇩d App t2 s2"
| d4[intro]: "⟦x♯(s1,s2); t1 ⟶⇩d t2; s1 ⟶⇩d s2⟧ ⟹ App (Lam [x].t1) s1 ⟶⇩d t2[x::=s2]"

equivariance Dev
nominal_inductive Dev

lemma better_d4_intro:
assumes a: "t1 ⟶⇩d t2" "s1 ⟶⇩d s2"
shows "App (Lam [x].t1) s1 ⟶⇩d t2[x::=s2]"
proof -
obtain y::"name" where fs: "y♯(x,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp,blast)
have "App (Lam [x].t1) s1 = App (Lam [y].([(y,x)]∙t1)) s1" using fs
by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
also have "… ⟶⇩d  ([(y,x)]∙t2)[y::=s2]" using fs a by (auto simp add: Dev.eqvt)
also have "… = t2[x::=s2]" using fs by (simp add: subst_rename[symmetric])
finally show "App (Lam [x].t1) s1 ⟶⇩d t2[x::=s2]" by simp
qed

lemma Dev_preserves_fresh:
fixes x::"name"
assumes a: "M⟶⇩d N"
shows "x♯M ⟹ x♯N"
using a
by (induct) (auto simp add: abs_fresh fresh_fact)

lemma Dev_Lam:
assumes a: "Lam [x].M ⟶⇩d N"
shows "∃N'. N = Lam [x].N' ∧ M ⟶⇩d N'"
proof -
from a have "x♯Lam [x].M" by (simp add: abs_fresh)
with a have "x♯N" by (simp add: Dev_preserves_fresh)
with a show "∃N'. N = Lam [x].N' ∧ M ⟶⇩d N'"
by (cases rule: Dev.strong_cases)
(auto simp add: lam.inject abs_fresh alpha)
qed

lemma Development_existence:
shows "∃M'. M ⟶⇩d M'"
by (nominal_induct M rule: lam.strong_induct)
(auto dest!: Dev_Lam intro: better_d4_intro)

lemma Triangle:
assumes a: "t ⟶⇩d t1" "t ⟶⇩1 t2"
shows "t2 ⟶⇩1 t1"
using a
proof(nominal_induct avoiding: t2 rule: Dev.strong_induct)
case (d4 x s1 s2 t1 t1' t2)
have  fc: "x♯t2" "x♯s1" by fact+
have "App (Lam [x].t1) s1 ⟶⇩1 t2" by fact
then obtain t' s' where reds:
"(t2 = App (Lam [x].t') s' ∧ t1 ⟶⇩1 t' ∧ s1 ⟶⇩1 s') ∨
(t2 = t'[x::=s'] ∧ t1 ⟶⇩1 t' ∧ s1 ⟶⇩1 s')"
using fc by (auto dest!: One_Redex)
have ih1: "t1 ⟶⇩1 t' ⟹  t' ⟶⇩1 t1'" by fact
have ih2: "s1 ⟶⇩1 s' ⟹  s' ⟶⇩1 s2" by fact
{ assume "t1 ⟶⇩1 t'" "s1 ⟶⇩1 s'"
then have "App (Lam [x].t') s' ⟶⇩1 t1'[x::=s2]"
using ih1 ih2 by (auto intro: better_o4_intro)
}
moreover
{ assume "t1 ⟶⇩1 t'" "s1 ⟶⇩1 s'"
then have "t'[x::=s'] ⟶⇩1 t1'[x::=s2]"
using ih1 ih2 by (auto intro: One_subst)
}
ultimately show "t2 ⟶⇩1 t1'[x::=s2]" using reds by auto
qed (auto dest!: One_Lam One_Var One_App)

lemma Diamond_for_One:
assumes a: "t ⟶⇩1 t1" "t ⟶⇩1 t2"
shows "∃t3. t2 ⟶⇩1 t3 ∧ t1 ⟶⇩1 t3"
proof -
obtain tc where "t ⟶⇩d tc" using Development_existence by blast
with a have "t2 ⟶⇩1 tc" and "t1 ⟶⇩1 tc" by (simp_all add: Triangle)
then show "∃t3. t2 ⟶⇩1 t3 ∧ t1 ⟶⇩1 t3" by blast
qed

lemma Rectangle_for_One:
assumes a:  "t ⟶⇩1⇧* t1" "t ⟶⇩1 t2"
shows "∃t3. t1 ⟶⇩1 t3 ∧ t2 ⟶⇩1⇧* t3"
using a Diamond_for_One by (induct arbitrary: t2) (blast)+

lemma CR_for_One_star:
assumes a: "t ⟶⇩1⇧* t1" "t ⟶⇩1⇧* t2"
shows "∃t3. t2 ⟶⇩1⇧* t3 ∧ t1 ⟶⇩1⇧* t3"
using a Rectangle_for_One by (induct arbitrary: t2) (blast)+

section ‹Establishing the Equivalence of Beta-star and One-star›

lemma Beta_Lam_cong:
assumes a: "t1 ⟶⇩β⇧* t2"
shows "Lam [x].t1 ⟶⇩β⇧* Lam [x].t2"
using a by (induct) (blast)+

lemma Beta_App_cong_aux:
assumes a: "t1 ⟶⇩β⇧* t2"
shows "App t1 s⟶⇩β⇧* App t2 s"
and "App s t1 ⟶⇩β⇧* App s t2"
using a by (induct) (blast)+

lemma Beta_App_cong:
assumes a: "t1 ⟶⇩β⇧* t2" "s1 ⟶⇩β⇧* s2"
shows "App t1 s1 ⟶⇩β⇧* App t2 s2"
using a by (blast intro: Beta_App_cong_aux)

lemmas Beta_congs = Beta_Lam_cong Beta_App_cong

lemma One_implies_Beta_star:
assumes a: "t ⟶⇩1 s"
shows "t ⟶⇩β⇧* s"
using a by (induct) (auto intro!: Beta_congs)

lemma One_congs:
assumes a: "t1 ⟶⇩1⇧* t2"
shows "Lam [x].t1 ⟶⇩1⇧* Lam [x].t2"
and   "App t1 s ⟶⇩1⇧* App t2 s"
and   "App s t1 ⟶⇩1⇧* App s t2"
using a by (induct) (auto intro: One_refl)

lemma Beta_implies_One_star:
assumes a: "t1 ⟶⇩β t2"
shows "t1 ⟶⇩1⇧* t2"
using a by (induct) (auto intro: One_refl One_congs better_o4_intro)

lemma Beta_star_equals_One_star:
shows "t1 ⟶⇩1⇧* t2 = t1 ⟶⇩β⇧* t2"
proof
assume "t1 ⟶⇩1⇧* t2"
then show "t1 ⟶⇩β⇧* t2" by (induct) (auto intro: One_implies_Beta_star)
next
assume "t1 ⟶⇩β⇧* t2"
then show "t1 ⟶⇩1⇧* t2" by (induct) (auto intro: Beta_implies_One_star)
qed

section ‹The Church-Rosser Theorem›

theorem CR_for_Beta_star:
assumes a: "t ⟶⇩β⇧* t1" "t⟶⇩β⇧* t2"
shows "∃t3. t1 ⟶⇩β⇧* t3 ∧ t2 ⟶⇩β⇧* t3"
proof -
from a have "t ⟶⇩1⇧* t1" and "t⟶⇩1⇧* t2" by (simp_all add: Beta_star_equals_One_star)
then have "∃t3. t1 ⟶⇩1⇧* t3 ∧ t2 ⟶⇩1⇧* t3" by (simp add: CR_for_One_star)
then show "∃t3. t1 ⟶⇩β⇧* t3 ∧ t2 ⟶⇩β⇧* t3" by (simp add: Beta_star_equals_One_star)
qed

end
```