Theory LamYNmless

section {* Locally Nameless implementation in Isabelle *}

theory LamYNmless
imports Main begin

subsection {* Definition of $\lamy$ pre-terms *}

typedecl atom

axiomatization where
  atom_inf: "infinite (UNIV :: atom set)"

datatype type = O | Arr type type ("_ → _")

datatype ptrm = FVar atom | BVar nat | App ptrm ptrm | Lam ptrm | Y type

subsection {* Definition of the open operation *}

fun opn :: "nat ⇒ ptrm ⇒ ptrm ⇒ ptrm" ("{_ → _} _")  where
"{k → u} (FVar x) = FVar x" |
"{k → u} (BVar i) = (if i = k then u else BVar i)" |
"{k → u} (App t1 t2) = App ({k → u} t1)({k → u} t2)" |
"{k → u} (Lam t) = Lam ({(k+1) → u} t)" |
"{k → u} (Y σ) = Y σ"

definition opn':: "ptrm ⇒ ptrm ⇒ ptrm" ("_^_") where
"opn' t u ≡ {0 → u} t"

lemma bvar_0_open_any:"BVar 0^M = M"
by (simp add: opn'_def)

lemma bvar_Suc_n_open_any:"(BVar (Suc n))^M = BVar (Suc n)"
by (simp add: opn'_def)

subsection {* Definition of well formed terms *}

inductive trm :: "ptrm ⇒ bool" where
var: "trm (FVar x)" |
app: "⟦ trm t1 ; trm t2 ⟧ ⟹ trm (App t1 t2)" |
lam: "⟦ finite L ; (⋀x. x ∉ L ⟹ trm (t^(FVar x))) ⟧ ⟹ trm (Lam t)" |
Y: "trm (Y σ)"
thm trm.simps

lemma bvar_not_trm: "trm (BVar n) ⟹ False"
using trm.cases by auto

lemma x_Ex: "⋀L:: atom set. finite L ⟹ ∃x. x ∉ L" 
by (simp add: ex_new_if_finite atom_inf)

subsection {* Definition of substitution *}

fun FV :: "ptrm ⇒ atom set"  where
"FV (FVar x) = {x}" |
"FV (BVar i) = {}" |
"FV (App t1 t2) = (FV t1) ∪ (FV t2)" |
"FV (Lam t) = FV t" |
"FV (Y σ) = {}"

lemma FV_finite: "finite (FV u)"
by (induct u, auto)

primrec subst :: "ptrm ⇒ atom ⇒ ptrm ⇒ ptrm" ("_ [_ ::= _]" [90, 90, 90] 90) where
"(FVar x)[z ::= u] = (if x = z then u else FVar x)" |
"(BVar x)[z ::= u] = BVar x" |
"(App t1 t2)[z ::= u] = App (t1[z ::= u]) (t2[z ::= u])" |
"(Lam t)[z ::= u] = Lam (t[z ::= u])" |
"(Y σ)[z ::= u] = (Y σ)"

lemma subst_fresh: "x ∉ FV t ⟹ t[x ::= u] = t"
apply (induct t)
apply (subst subst.simps(1))
using [[simp_trace]]
apply (drule subst[OF FV.simps(1)])
apply (drule subst[OF Set.insert_iff])
apply (drule subst[OF Set.empty_iff])
apply (drule subst[OF HOL.simp_thms(31)])
by auto

lemma subst_fresh2: "x ∉ FV t ⟹ t = t[x ::= u]"
by (induct t, auto)

lemma opn_trm_core: "i ≠ j ⟹ {j → v} e = {i → u}({j → v} e) ⟹ e = {i → u} e"
apply (induct e arbitrary: i j)
apply auto
by blast

lemma opn_trm: "trm e ⟹ e = {k → t}e"
apply (induct arbitrary: k t rule:trm.induct)
apply simp+
defer
apply simp
proof goal_cases
case (1 L e k t)
  then obtain y where 2: "y ∉ (L ∪ FV e)" using FV_finite x_Ex by (meson finite_UnI)
  show ?case
  apply (rule_tac j = 0 and v= "FVar y" in opn_trm_core)
  using "1"(3) "2" opn'_def by auto
qed

lemma opn_trm2: "trm e ⟹ {k → t}e = e" 
using opn_trm by simp

lemma subst_open: "trm u ⟹ ({n → w}t)[x ::= u] = {n → w [x ::= u]} (t [x ::= u])"
apply (induct t arbitrary:n)
by (auto simp add:opn_trm)

lemma subst_open2: "trm u ⟹ {n → w [x ::= u]} (t [x ::= u]) = ({n → w}t)[x ::= u]"
by (simp add:subst_open)

lemma fvar_subst_simp: "x ≠ y ⟹ FVar y = FVar y[x ::= u]" 
by simp

lemma fvar_subst_simp2: "u = FVar x[x ::= u]" 
by simp

lemma subst_open_var: "trm u ⟹ x ≠ y ⟹ (t^FVar y)[x ::= u] = (t [x ::= u])^FVar y"
unfolding opn'_def
apply (subst(2) fvar_subst_simp)
apply simp
apply (rule_tac subst_open)
by simp

lemma subst_open_var2: "trm u ⟹ x ≠ y ⟹ (t [x ::= u])^FVar y = (t^FVar y)[x ::= u]" 
using subst_open_var by simp

lemma subst_intro: "trm u ⟹ x ∉ FV t ⟹ (t^FVar x)[x::=u] = t^u"
unfolding opn'_def
apply (subst(6) fvar_subst_simp2[where x=x])
apply (subst(10) subst_fresh2[where x=x and u=u])
defer
apply (rule subst_open)
by auto

lemma subst_intro2: "trm u ⟹ x ∉ FV t ⟹ t^u = (t^FVar x)[x::=u]" 
using subst_intro by simp

lemma subst_trm: "trm e ⟹ trm u ⟹ trm(e[x::=u])"
proof (induct rule:trm.induct)
case var thus ?case by (simp add:trm.var)
next
case app thus ?case by (simp add:trm.app)
next
case Y thus ?case by (simp add:trm.Y)
next
case (lam L t) 
  show ?case
  unfolding subst.simps
  apply (rule trm.lam[where L="L ∪ {x}"])
  using lam apply auto[1]
  apply (subst subst_open_var2)
  using lam by auto
qed

lemma trm_opn: "trm (Lam M) ∧ trm N ⟹ trm M^N"
apply (frule conjE[where R="trm (Lam M)"])
apply simp
apply (drule conjE[where R="trm N"])
apply simp
apply (cases rule:trm.cases)
apply auto
proof goal_cases
case (1 L) 
  then obtain x where 2: "x ∉ L ∪ FV M" by (meson FV_finite finite_UnI x_Ex)
  with 1 have 3: "trm M^FVar x" by simp
  
  show ?case
  apply(subst subst_intro2)
  using 1 apply simp
  using 2 apply auto[1]
  apply (subst subst_trm)
  using 1 3 by auto
qed

subsection {* Definition of the close operation *}

fun cls :: "nat ⇒ atom ⇒ ptrm ⇒ ptrm" ("{_ <- _} _")  where
"{k <- x} (FVar y) = (if x = y then BVar k else FVar y)" |
"{k <- x} (BVar i) = BVar i" |
"{k <- x} (App t1 t2) = App ({k <- x} t1)({k <- x} t2)" |
"{k <- x} (Lam t) = Lam ({(k+1) <- x} t)" |
"{k <- x} (Y σ) = Y σ"

definition cls':: "atom ⇒ ptrm ⇒ ptrm" ("\\_^_") where
"cls' x t ≡ {0 <- x} t"

lemma FV_simp: "⟦ x ∉ FV M ; x ≠ y ⟧ ⟹ x ∉ FV {k → FVar y} M"
apply (induct M arbitrary:k)
by auto

lemma FV_simp2: "x ∉ FV M ∪ FV N ⟹ x ∉ FV {k → N}M"
apply (induct M arbitrary:k)
by auto

lemma FV_simp3: "x ∉ FV {k → N}M ⟹ x ∉ FV M"
apply (induct M arbitrary:k)
by auto

lemma FV_simp4: "x ∉ FV M ⟹ x ∉ FV {k <- y} M"
apply (induct M arbitrary:k)
by auto

lemma FV_simp5: "x ∉ FV M ∪ FV N ⟹ x ∉ FV (M[y ::= N])"
apply (induct M)
by auto

lemma fv_opn_cls_id: "x ∉ FV t ⟹ {k <- x}{k → FVar x}t = t"
apply (induct t arbitrary:k)
by auto

lemma fv_opn_cls_id2: "x ∉ FV t ⟹ t = {k <- x}{k → FVar x}t" 
using fv_opn_cls_id by simp

lemma opn_cls_swap: "k ≠ m ⟹ x ≠ y ⟹ {k <- x}{m → FVar y}M = {m → FVar y}{k <- x}M"
apply (induct M arbitrary:k m)
by auto

lemma opn_cls_swap2: "k ≠ m ⟹ x ≠ y ⟹ {m → FVar y}{k <- x}M = {k <- x}{m → FVar y}M"
using opn_cls_swap by simp

lemma opn_opn_swap: "k ≠ m ⟹ x ≠ y ⟹ {k → FVar x}{m → FVar y}M = {m → FVar y}{k → FVar x}M"
apply (induct M arbitrary:k m)
by auto

lemma cls_opn_eq_subst: "trm M ⟹ ({k → FVar y} {k <- x} M) = (M[x ::= FVar y])"
proof (induct M arbitrary: k rule:trm.induct)
case var thus ?case by auto
next
case app thus ?case by auto
next
case Y thus ?case by auto
next
case (lam L t k) 
  then obtain x' where 2: "x' ∉ L ∪ {x,y} ∪ FV t" by (meson FV_finite finite.emptyI finite.insertI finite_UnI x_Ex)
  with lam have "{Suc k → FVar y} {Suc k <- x} {0 → FVar x'} t = ({0 → FVar x'} t) [x ::= FVar y]" unfolding opn'_def using "lam"(3) FV_simp UnI1 UnI2 insertCI opn'_def by auto
  then have "{0 → FVar x'} {Suc k → FVar y} {Suc k <- x} t = {0 → FVar x'}(t [x ::= FVar y])"
  apply (subst opn_opn_swap)
  apply simp
  using 2 apply simp
  apply (subst opn_cls_swap2)
  apply simp
  using 2 apply auto[1]
  using subst_open_var 2 by (simp add: UnI2 insertI1 subst_open trm.var)
  then have 3: "{0 <- x'}{0 → FVar x'}{Suc k → FVar y} {Suc k <- x} t = {0 <- x'}{0 → FVar x'}(t [x ::= FVar y])" by simp

  show ?case unfolding cls.simps opn.simps subst.simps
  apply rule
  apply (subst fv_opn_cls_id2[where x=x' and k = 0 and t="{k + 1 → FVar y} {k + 1 <- x} t"])
  apply (rule FV_simp)
  apply (rule FV_simp4)
  using 2 apply simp
  using 2 apply simp
  apply (subst fv_opn_cls_id2[where x=x' and k = 0 and t="t [x ::= FVar y]"])
  apply (rule FV_simp5)
  using 2 3 by auto
qed

lemma cls_opn_eq_subst2: "trm M ⟹ (M[x ::= FVar y]) =({k → FVar y} {k <- x} M)"
using cls_opn_eq_subst by simp

subsection {*$\beta Y$-reduction*}

inductive beta_Y :: "ptrm ⇒ ptrm ⇒ bool" (infix "⇒" 300)
where
  red_L[intro]: "⟦ trm N ; M ⇒ M' ⟧ ⟹ App M N ⇒ App M' N"
| red_R[intro]: "⟦ trm M ; N ⇒ N' ⟧ ⟹ App M N ⇒ App M N'"
| abs[intro]: "⟦ finite L ; (⋀x. x ∉ L ⟹ M^(FVar x) ⇒ M'^(FVar x)) ⟧ ⟹ Lam M ⇒ Lam M'"
| beta[intro]: "⟦ trm (Lam M) ; trm N ⟧ ⟹ App (Lam M) N ⇒ M^N"
| Y[intro]: "trm M ⟹ App (Y σ) M ⇒ App M (App (Y σ) M)"

lemma trm_beta_Y_simp1: "M ⇒ M' ⟹ trm M ∧ trm M'"
apply rule
apply (induct M' rule:beta_Y.induct)
apply (subst trm.simps, simp)+
apply auto[1]
apply (simp add: lam trm.app)
apply (simp add: trm.Y trm.app)
apply (induct M M' rule:beta_Y.induct)
apply (subst trm.simps, simp)+
apply auto[1]
apply (rule trm_opn)
apply (simp add: lam)
apply (simp add: trm.Y trm.app)
done

subsection {* Parallel $\beta Y$-reduction *}

inductive 
  pbeta :: "ptrm ⇒ ptrm ⇒ bool" ("_ ≫ _" [80,80] 80)
where
  refl[intro]: "(FVar x) ≫ (FVar x)"
| reflY[intro]: "Y σ ≫ Y σ"
| app[intro]: "⟦ M ≫ M' ; N ≫ N' ⟧ ⟹ App M N ≫ App M' N'"
| abs[intro]: "⟦ finite L ; (⋀x. x ∉ L ⟹ M^(FVar x) ≫ M'^(FVar x)) ⟧ ⟹ Lam M ≫ Lam M'"
| beta[intro]: "⟦ finite L ; (⋀x. x ∉ L ⟹ M^(FVar x) ≫ M'^(FVar x)) ; N ≫ N' ⟧ ⟹ App (Lam M) N ≫ M'^N'"
| Y[intro]: "⟦ M ≫ M' ⟧ ⟹ App (Y σ) M ≫ App M' (App (Y σ) M')"

lemma trm_pbeta_simp1: "M ≫ M' ⟹ trm M ∧ trm M'"
apply rule
apply (induct M M' rule:pbeta.induct)
apply (subst trm.simps, simp)+
apply auto[1]
apply (simp add: lam trm.app)
apply (simp add: trm.Y trm.app)
apply (induct M M' rule:pbeta.induct)
apply (subst trm.simps, simp)+
apply auto[1]
apply (rule trm_opn)
apply (simp add: lam)
apply (simp add: trm.Y trm.app)
done

subsection {* Maximal parallel $\beta Y$-reduction *}

fun not_abst :: "ptrm ⇒ bool"
where
  "not_abst (FVar x) = True"
| "not_abst (BVar x) = True"
| "not_abst (App t1 t2) = True"
| "not_abst (Lam t) = False"
| "not_abst (Y t) = True"

fun not_Y :: "ptrm ⇒ bool"
where
  "not_Y (FVar x) = True"
| "not_Y (BVar x) = True"
| "not_Y (App t1 t2) = True"
| "not_Y (Lam t) = True"
| "not_Y (Y t) = False"

inductive 
  pbeta_max :: "ptrm ⇒ ptrm ⇒ bool" ("_ >>> _" [80,80] 80)
where
  refl[intro]: "(FVar x) >>> (FVar x)"
| reflY[intro]: "Y σ >>> Y σ"
| app[intro]: "⟦ not_abst M ; not_Y M ;  M >>> M' ; N >>> N' ⟧ ⟹ App M N >>> App M' N'"
| abs[intro]: "⟦ finite L ; (⋀x. x ∉ L ⟹ M^(FVar x) >>> M'^(FVar x)) ⟧ ⟹ Lam M >>>  Lam M'"
| beta[intro]: "⟦ finite L ; (⋀x. x ∉ L ⟹ M^(FVar x) >>> M'^(FVar x)) ; N >>> N' ⟧ ⟹ App (Lam M) N >>> M'^N'"
| Y[intro]: "⟦ M >>> M' ⟧ ⟹ App (Y σ) M >>> App M' (App (Y σ) M')"

lemma trm_pbeta_max_simp1: "M >>> M' ⟹ trm M ∧ trm M'"
apply rule
apply (induct M M' rule:pbeta_max.induct)
apply (subst trm.simps, simp)+
apply auto[1]
apply (simp add: lam trm.app)
apply (simp add: trm.Y trm.app)
apply (induct M M' rule:pbeta_max.induct)
apply (subst trm.simps, simp)+
apply auto[1]
apply (rule trm_opn)
apply (simp add: lam)
apply (simp add: trm.Y trm.app)
done

lemma pbeta_beta': "finite L ⟹ (⋀x. x ∉ L ⟹ M^(FVar x) ≫ M'^(FVar x)) ⟹ N ≫ N' ⟹ App (Lam M) N ≫ {0 → N'} M'" 
using pbeta.beta opn'_def by simp

lemma not_Y_ex: "¬(not_Y M) ⟹ ∃σ. M = Y σ"
apply (cases M rule:not_Y.cases)
by auto

lemma not_abst_simp: "not_abst M ⟹ not_abst {k → FVar y} {k <- x} M"
apply (cases M)
unfolding opn'_def opn.simps
by auto

lemma not_Y_simp: "not_Y M ⟹ not_Y {k → FVar y} {k <- x} M"
apply (cases M)
unfolding opn'_def opn.simps
by auto

subsection {* \cref{Lemma:maxEx} *}

lemma pbeta_max_beta': "finite L ⟹ (⋀x. x ∉ L ⟹ M^(FVar x) >>> M'^(FVar x)) ⟹ N >>> N' ⟹ App (Lam M) N >>> {0 → N'} M'" using pbeta_max.beta opn'_def by simp

lemma Lem2_5_1_beta_max:
  assumes "s >>> s'"
      shows "(s[x ::= FVar y]) >>> (s'[x ::= FVar y])"
using assms proof (induct s s' rule:pbeta_max.induct)
case (refl s)
  then show ?case by auto
next
case (reflY s)
  then show ?case by auto
next
case (app M)
  show ?case 
  unfolding subst.simps
  apply (rule pbeta_max.app)
  apply (cases M)
  using app apply simp_all
  apply (cases M)
  using app by simp_all
next
case (abs L M M') 
  show ?case
  unfolding subst.simps
  apply (rule_tac L="L ∪ {x}" in pbeta_max.abs)
  using abs apply simp 
  unfolding opn'_def
  apply (subst subst_fresh2[where x=x and u="FVar y"])
  apply auto[1]
  apply (subst(8) subst_fresh2[where x=x and u="FVar y"])
  apply auto[1]
  apply (subst subst_open2)
  defer
  apply (subst subst_open2)
  defer
  defer
  apply (rule trm.var)
  using abs unfolding opn'_def
  by simp
 next
case (beta L M M' N N')
  show ?case unfolding subst.simps opn'_def
  apply (subst subst_open)
  defer
  apply (rule_tac L="L ∪ {x}" in pbeta_max_beta')
  using beta apply simp
  apply (subst subst_open_var2)
  apply (rule trm.var)
  apply auto[1]
  apply (subst subst_open_var2)
  apply (rule trm.var)
  apply auto[1]
  using beta trm_pbeta_max_simp1 apply simp
  using beta trm_pbeta_max_simp1 apply simp
  by (rule trm.var)
next
case Y thus ?case by auto
qed

lemma pbeta_max_cls: "t >>> d ⟹ y ∉ FV t ∪ FV d ∪ {x} ⟹ {k → FVar y}{k <- x}t >>> {k → FVar y}{k <- x}d"
apply (subst cls_opn_eq_subst)
defer
apply (subst cls_opn_eq_subst)
defer
apply (rule Lem2_5_1_beta_max)
using trm_pbeta_max_simp1 by auto

lemma pbeta_max_ex:
  fixes M assumes "trm M"
  shows "∃M'. M >>> M'"
using assms apply (induct M rule:trm.induct)
apply auto
apply (case_tac "not_abst t1")
apply (case_tac "not_Y t1")
apply auto[1]
proof goal_cases
case (1 P Q P' Q')
  then obtain σ where 2: "P = Y σ" using not_Y_ex by auto
  have "App (Y σ) Q >>> App Q' (App (Y σ) Q')"
  apply (rule_tac pbeta_max.Y)
  by (rule 1(4))
  thus ?case unfolding 2 by auto
next
case (2 P Q P' Q')
  from 2(3,4,5,1,2) show ?case
  apply (induct P P' rule:pbeta_max.induct)
  by auto
next
case (3 L M)
  then obtain x where 4:"x ∉ L ∪ FV M" by (meson FV_finite finite_UnI x_Ex)
  with 3 obtain M' where 5: "M^FVar x >>> M'" by auto

  have 6: "⋀y. y ∉ FV M' ∪ FV M ∪ {x} ⟹ M^FVar y >>> (\\x^M')^FVar y"
  unfolding opn'_def cls'_def 
  apply (subst(3) fv_opn_cls_id2[where x=x])
  using 4 apply simp
  apply (rule_tac pbeta_max_cls)
  using 5 opn'_def by (auto simp add: FV_simp)

  show ?case
  apply rule
  apply (rule_tac L="FV M' ∪ FV M ∪ {x}" in pbeta_max.abs)
  using 6 by (auto simp add: FV_finite)
qed

subsection {* \cref{Lemma:maxClose} *}

lemma Lem2_5_1:
  assumes "s ≫ s'"
      and "t ≫ t'"
      shows "(s[x ::= t]) ≫ (s'[x ::= t'])"
using assms proof (induct s s' rule:pbeta.induct)
case (refl s)
  then show ?case by auto
next
case (reflY s)
  then show ?case by auto
next
case app
  show ?case 
  unfolding subst.simps
  apply (rule pbeta.app)
  using app
  by simp+
next
case (abs L M M') 
  show ?case
  unfolding subst.simps
  apply (rule_tac L="L ∪ {x}" in pbeta.abs)
  using abs apply simp 
  unfolding opn'_def
  apply (subst subst_fresh2[where x=x and u=t])
  apply auto[1]
  apply (subst(8) subst_fresh2[where x=x and u=t'])
  apply auto[1]
  apply (subst subst_open2)
  defer
  apply (subst subst_open2)
  defer
  using abs(2,3) apply (simp add: UnI1 abs.prems opn'_def)
  using trm_pbeta_simp1 abs.prems by auto
 next
case (beta L M M' N N')
  show ?case unfolding subst.simps opn'_def
  apply (subst subst_open)
  defer
  apply (rule_tac L="L ∪ {x}" in pbeta_beta')
  using beta apply simp
  apply (subst subst_open_var2)
  using beta trm_pbeta_simp1 apply simp
  apply auto[1]
  apply (subst subst_open_var2)
  using beta trm_pbeta_simp1 apply simp
  apply auto[1]
  using beta trm_pbeta_simp1 by auto
next
case Y thus ?case by auto
qed

lemma Lem2_5_1opn:
  assumes "⋀x. x ∉ L ⟹ s^FVar x ≫ s'^FVar x" and "finite L"
      and "t ≫ t'"
      shows "s^t ≫ s'^t'"
proof -
  from assms(2) obtain x where 1: "x ∉ L ∪ FV s ∪ FV s'" by (meson FV_finite infinite_Un x_Ex)
  show ?thesis
  apply (subst subst_intro2[where x=x])
  using assms(3) apply (simp add: trm_pbeta_simp1)
  using 1 apply simp
  apply (subst (2) subst_intro2[where x=x])
  using assms(3) apply (simp add: trm_pbeta_simp1)
  using 1 apply simp
  apply(rule Lem2_5_1)
  using assms 1 by auto
qed

lemma pbeta_max_closes_pbeta:
  fixes a b d
  assumes "a >>> d"
  and "a ≫ b"
  shows "b ≫ d"
using assms proof (induct arbitrary: b rule:pbeta_max.induct)
case (refl a)  
  show ?case using refl pbeta.cases by fastforce
next
case (reflY a) then have 1: "b = Y a" apply (cases rule: pbeta.cases) by simp
  show ?case unfolding 1 by auto
next
case (beta L al ald ar ard)
  from beta(6) show ?case
  apply (cases rule: pbeta.cases)
  proof goal_cases
  case (2 L' alb arb)
    with beta have ih: "arb ≫ ard" "⋀x. x ∉ L ∪ L' ⟹ alb^FVar x ≫ ald^FVar x"  by simp+
    show ?case unfolding 2 apply (rule_tac L="L ∪ L'" in Lem2_5_1opn)
    defer using beta(1) 2(2) apply simp
    using ih by auto
  next
  case (1 alb arb)
    with beta have ih:  "arb ≫ ard" by simp
    show ?case unfolding 1 
    using 1(2) apply (cases rule:pbeta.cases)
    apply simp
    proof goal_cases
    case (1 L' alb')
      with beta have ih2: "⋀x. x ∉ L ∪ L' ⟹ alb'^FVar x ≫ ald^FVar x" by simp
      show ?case
      apply (rule_tac L="L ∪ L'" in pbeta.beta)
      using 1 beta ih ih2 by auto
    qed
  qed
next
case (app al ald ar ard) 
  from app(7,1,2) show ?case
  apply (cases "App al ar" b rule:pbeta.cases)
  using app apply auto[1]
  apply simp
  by simp
next
case (abs L al ald) 
  from abs(4) show ?case 
  apply (cases rule:pbeta.cases) 
  apply simp
  proof goal_cases
  case (1 L' alb)
    with abs have ih: "⋀x. x ∉ L ∪ L' ⟹ alb^FVar x ≫ ald^FVar x" by simp
    show ?case
    apply (rule_tac L="L ∪ L'" in pbeta.abs)
    using 1 abs ih by auto
  qed
next
case (Y M M' σ) 
  from Y(3) show ?case
  apply (cases rule:pbeta.cases)
  proof goal_cases
  case (1 M'' N'')
    from 1(2) have 2: "M'' = Y σ" by (cases rule:pbeta.cases, simp)
    show ?case unfolding 1 2
    apply (rule pbeta.Y)
    using 1 Y by simp
  next
  case (2 M'') show ?case unfolding 2
    apply (rule pbeta.app)
    using Y 2 apply simp
    apply (rule pbeta.app)
    apply (rule pbeta.reflY)
    using Y 2 by simp
  qed
qed

subsection {* Proof of $\dip(\gg)$ *}

lemma Lem2_5_2: 
  assumes "a ≫ b"
      and "a ≫ c"
    shows "∃d. b ≫ d ∧ c ≫ d"
proof -
  obtain d where 1: "a >>> d" using pbeta_max_ex assms(2) trm_pbeta_simp1 by blast
  have "b ≫ d ∧ c ≫ d" 
  apply rule 
  apply (rule_tac pbeta_max_closes_pbeta)
  using 1 assms apply simp+
  apply (rule_tac pbeta_max_closes_pbeta)
  using 1 assms apply simp+
  done
  thus ?thesis by auto
qed

subsection {* Reflexive-transitive closure of $\beta Y$ *}

inductive close :: "(ptrm ⇒ ptrm ⇒ bool) ⇒ ptrm ⇒ ptrm ⇒ bool" ("_* _  _" [80,80] 80) for R::"ptrm ⇒ ptrm ⇒ bool"
where
  base[intro]: "R a b ⟹ R* a b"
| refl[intro]: "R* a a"
| trans[intro]: "⟦ R* a b ; R* b c ⟧ ⟹ R* a c"

definition DP :: "(ptrm ⇒ ptrm ⇒ bool) ⇒ (ptrm ⇒ ptrm ⇒ bool) ⇒ bool" where
"DP R T = (∀a b c. R a b ∧ T a c ⟶ (∃d. T b d ∧ R c d))"

lemma DP_R_R_imp_DP_R_Rc_pbeta:
  assumes "DP pbeta pbeta"
    shows "DP pbeta (close pbeta)"
using assms unfolding DP_def
apply auto
proof -
case goal1 
  from goal1(3,2) show ?case
  apply (induct arbitrary: b rule:close.induct)
  using goal1(1) by blast+
qed

lemma DP_R_R_imp_DP_Rc_Rc_pbeta:
  assumes "DP pbeta pbeta"
    shows "DP (close pbeta) (close pbeta)"
using assms unfolding DP_def
apply auto
proof -
case goal1 
  from goal1(2,3) show ?case
  apply (induct arbitrary: c rule:close.induct)
  using DP_R_R_imp_DP_R_Rc_pbeta using DP_def assms apply fastforce
  apply auto
  by blast
qed

lemma pbeta_refl[intro]: "trm s ⟹ s ≫ s"
apply (induct s rule:trm.induct)
by auto

lemma M1': "M ⇒ M' ⟹ M ≫ M'"
proof (induct M M' rule:beta_Y.induct)
case red_L 
  show ?case
  apply (rule pbeta.app)
  using trm_beta_Y_simp1 red_L apply simp
  apply (rule pbeta_refl)
  using red_L by simp
next
case red_R 
  show ?case
  apply (rule pbeta.app)
  apply (rule pbeta_refl)
  using trm_beta_Y_simp1 red_R by auto
next
case (abs L) 
  show ?case
  apply (rule_tac L=L in pbeta.abs)
  using abs by auto
next
case (beta M N)
  from beta(1) obtain L where 1: "finite L" "∀x. x ∉ L ⟶ trm (M^FVar x)" using trm.simps by (metis finite.intros(1) trm_opn)
  show ?case 
  apply (rule_tac L=L in pbeta.beta)
  using 1 apply simp
  apply (rule pbeta_refl)
  using 1 apply simp
  apply (rule pbeta_refl)
  using beta by simp
next
case Y thus ?case by auto
qed

lemma M1: "beta_Y* M M' ⟹ pbeta* M M'"
apply (induct M M' rule:close.induct)
apply auto
apply (rule base)
by (simp add: M1')

lemma red_r_close: "beta_Y* N N' ⟹ trm M ⟹ beta_Y* (App M N) (App M N')"
apply (induct rule:close.induct)
by auto

lemma red_l_close: "beta_Y* M M' ⟹ trm N ⟹ beta_Y* (App M N) (App M' N)"
apply (induct rule:close.induct)
by auto

lemma beta_Y_beta': "trm (Lam M) ⟹ trm N ⟹ App (Lam M) N ⇒ {0 → N} M" using beta_Y.beta opn'_def by simp

lemma Lem2_5_1'_beta_Y:
  assumes "s ⇒ s'"
      shows "(s[x ::= FVar y]) ⇒ (s'[x ::= FVar y])"
using assms proof (induct s s' rule:beta_Y.induct)
case (red_L N M M')
  show ?case 
  unfolding subst.simps
  apply (rule beta_Y.red_L)
  using red_L trm.var subst_trm by blast+
next
case (red_R M N N')
  show ?case 
  unfolding subst.simps
  apply (rule beta_Y.red_R)
  using red_R trm.var subst_trm by blast+
next
case (abs L M M') 
  show ?case
  unfolding subst.simps
  apply (rule_tac L="L ∪ {x}" in beta_Y.abs)
  using abs apply simp 
  unfolding opn'_def
  apply (subst subst_fresh2[where x=x and u="FVar y"])
  apply auto[1]
  apply (subst(8) subst_fresh2[where x=x and u="FVar y"])
  apply auto[1]
  apply (subst subst_open2)
  defer
  apply (subst subst_open2)
  defer
  defer
  apply (rule trm.var)
  using abs unfolding opn'_def
  by simp
 next
case (beta M N)
  show ?case unfolding subst.simps opn'_def
  apply (subst subst_open)
  apply (rule trm.var)
  apply (rule beta_Y_beta')
  defer
  using beta trm.var subst_trm apply simp
  using beta(1) trm.var subst_trm subst.simps(4) by metis
next
case Y 
  show ?case unfolding subst.simps 
  apply rule
  using Y trm.var subst_trm by simp
qed

lemma beta_Y_lam_cls: "a ⇒ b ⟹ Lam {0 <- x} a ⇒ Lam {0 <- x} b"
apply (rule_tac L="{}" in beta_Y.abs)
apply simp
unfolding opn'_def
defer
apply (subst(2) cls_opn_eq_subst)
using trm_beta_Y_simp1 apply simp
apply (subst cls_opn_eq_subst)
using trm_beta_Y_simp1 apply simp
apply (rule Lem2_5_1'_beta_Y)
by simp

lemma abs_close: "⟦ ⋀x. x ∉ L ⟹ beta_Y* (M^FVar x) (M'^FVar x) ; finite L ⟧ ⟹ beta_Y* (Lam M) (Lam M')"
proof goal_cases
case 1
  note 11 = 1
  then obtain x where 2: "x ∉ L ∪ FV M ∪ FV M'" by (meson FV_finite finite_UnI x_Ex)
  with 1 have "op ⇒* M^FVar x  M'^FVar x" by simp
  then show ?case
  apply (subst (4)fv_opn_cls_id2[where k=0 and x=x])
  using 2 apply simp
  apply (subst (2)fv_opn_cls_id2[where k=0 and x=x])
  using 2 apply simp
  unfolding opn'_def
  apply (induct rule:close.induct)
  apply auto
  apply (rule base)
  apply (rule beta_Y_lam_cls)
  by simp
qed

lemma M2: "pbeta* M M' ⟹ beta_Y* M M'"
proof (induct M M' rule:close.induct)
case refl show ?case by (rule close.refl)
next
case trans 
  show ?case apply (rule close.trans)
  using trans by simp+
next
case base thus ?case
  proof (induct rule:pbeta.induct)
  case refl show ?case by (rule close.refl)
  next
  case reflY show ?case by (rule close.refl)
  case (app M M' N N') 
    show ?case
    apply (rule_tac b="App M N'" in close.trans)
    using red_r_close app.hyps(1,4) trm_pbeta_simp1 apply auto[1]
    using red_l_close app.hyps(2,3) trm_pbeta_simp1 by blast
  next
  case (abs L M M')
    show ?case
    apply (rule_tac L=L in  abs_close)
    using abs by simp+
  next
  case (beta L M M' N N')
    show ?case
    apply (rule_tac b="App (Lam M') N" in close.trans)
    apply (rule red_l_close)
    apply (rule_tac L=L in  abs_close)
    using beta apply simp
    using beta trm_pbeta_simp1 apply simp+
    apply (rule_tac b="App (Lam M') N'" in close.trans)
    apply (rule red_r_close)
    using beta apply simp
    apply (rule_tac L=L in trm.lam)
    using beta apply simp
    using beta(2) trm_pbeta_simp1 apply auto[1]
    apply (rule close.base)
    apply (rule beta_Y.beta)
    apply (rule_tac L=L in trm.lam)
    using beta apply simp
    using beta(2) trm_pbeta_simp1 apply auto[1]
    using beta trm_pbeta_simp1 by simp
  next
  case (Y M M' σ) 
    show ?case
    apply (rule_tac b="App M (App (Y σ) M)" in close.trans)
    apply (rule close.base)
    apply (rule beta_Y.Y)
    using Y trm_pbeta_simp1 apply simp
    apply (rule_tac b="App M' (App (Y σ) M)" in close.trans)
    apply (rule red_l_close)
    using Y apply simp
    using Y trm_pbeta_simp1 apply auto[1]
    apply (rule red_r_close)
    apply (rule red_r_close)
    using Y trm_pbeta_simp1 by auto
  qed
qed

subsection {* Simple-typing relation $\vdash$ *}

type_synonym ctxt = "(atom × type) list"

inductive wf_ctxt :: "ctxt ⇒ bool" where
nil: "wf_ctxt []" |
cons: "⟦ x ∉ fst`set C ; wf_ctxt C ⟧ ⟹ wf_ctxt ((x, σ)#C)"

inductive wt_trm :: "ctxt ⇒ ptrm ⇒ type ⇒ bool" ("_ ⊢ _ : _") where
var: "⟦ wf_ctxt Γ ; (x,σ) ∈ set Γ ⟧ ⟹ Γ ⊢ FVar x : σ" |
app: "⟦ Γ ⊢ t1 : τ → σ ; Γ ⊢ t2 : τ ⟧ ⟹ Γ ⊢ App t1 t2 : σ" |
abs: "⟦ finite L ; (⋀x. x ∉ L ⟹ ((x,σ)#Γ) ⊢ (t^(FVar x)) : τ) ⟧ ⟹ Γ ⊢ Lam t : σ → τ" |
Y: "⟦ wf_ctxt Γ ⟧ ⟹  Γ ⊢ Y σ : (σ → σ) → σ"

lemma wf_ctxt_cons: "wf_ctxt ((x, σ)#Γ) ⟹ wf_ctxt Γ ∧ x ∉ fst`set Γ"
apply (cases rule:wf_ctxt.cases)
by auto

lemma wt_terms_impl_wf_ctxt: "Γ ⊢ M : σ ⟹ wf_ctxt Γ"
apply (induct rule:wt_trm.induct)
apply auto
using wf_ctxt_cons by (meson x_Ex)

lemma opn_typ_aux: "(x, τ) # Γ ⊢ FVar y : σ ⟹ x = y ⟹ τ = σ"
proof (rule ccontr, goal_cases)
case 1 
  then have "wf_ctxt ((y, τ) # Γ)" by (simp add: wt_terms_impl_wf_ctxt)
  then have "y ∉ fst`set Γ" by (simp add: wf_ctxt_cons)
  then have "(y, σ) ∉ set Γ" by force
  with 1(3) have 2: "(y, σ) ∉ set ((y, τ) # Γ)" by simp
  from 1(1) have "(y, σ) ∈ set ((y, τ) # Γ)" apply (cases rule:wt_trm.cases) by auto
  with 2 show ?case by simp
qed

lemma weakening:
  fixes Γ Γ' M σ
  assumes "Γ ⊢ M : σ" and "set Γ ⊆ set Γ'"
  and "wf_ctxt Γ'"
  shows "Γ' ⊢ M : σ"
using assms proof (induct Γ M σ arbitrary:Γ' rule:wt_trm.induct)
case var 
  show ?case 
  apply (rule wt_trm.var) 
  using var by auto
next
case app
  show ?case
  apply (rule wt_trm.app)
  using app by auto
next
case (abs L σ Γ t τ)
  have 1: "⋀x. x ∉ (L ∪ fst ` set Γ') ⟹ wf_ctxt ((x, σ) # Γ')"
  apply (rule cons)
  using abs by simp+

  show ?case
  apply (rule_tac L="L ∪ fst ` set Γ'" in wt_trm.abs)
  using abs apply simp
  apply (rule abs(3))
  apply simp
  using abs.prems(1) 1 by auto
next
case Y thus ?case using wt_trm.Y by simp
qed

lemma wf_ctxt_exchange: "wf_ctxt ((x,σ) # (y,π) # Γ) ⟹ wf_ctxt ((y,π) # (x,σ) # Γ)"
proof goal_cases
case 1 
  then have "wf_ctxt ((y,π) # Γ) ∧ x ∉ fst`set ((y,π) # Γ)" by (rule wf_ctxt_cons)
  then have 1: "wf_ctxt ((y,π) # Γ)" "x ∉ fst`set ((y,π) # Γ)"  by simp+
  from 1(1) have 2: "wf_ctxt Γ ∧ y ∉ fst`set Γ" by (rule wf_ctxt_cons)
  from 1(2) have 3: "x ∉ fst`set Γ" by simp
  from 1(2) 2 have 4: "y ∉ fst`set((x,σ) # Γ)" by auto

  show ?case
  apply (rule cons)
  using 4 apply simp  
  apply (rule cons)
  using 3 apply simp
  using 2 by simp
qed

lemma exchange: "(x,σ) # (y,π) # Γ ⊢ M : δ ⟹ (y,π) # (x,σ) # Γ ⊢ M : δ"
proof goal_cases
case 1
  have "set ((x,σ) # (y,π) # Γ) ⊆ set ((y,π) # (x,σ) # Γ)" by auto
  thus ?case using 1 weakening wt_terms_impl_wf_ctxt wf_ctxt_exchange by blast
qed

lemma trm_wt_trm: "Γ ⊢ M : σ ⟹ trm M"
apply (induct Γ M σ rule:wt_trm.induct)
apply (subst trm.simps, simp)+
apply auto[1]
by (subst trm.simps, simp)

lemma subst_typ:
  assumes "trm M" and "((x,τ)#Γ) ⊢ M : σ" and "Γ ⊢ N : τ"
  shows "Γ ⊢ M[x ::= N] : σ"
using assms proof (induct M arbitrary: Γ x N σ rule: trm.induct)
case (var y)
  show ?case
  proof (cases "x = y")
  case True 
    show ?thesis 
    apply (simp add: True)
    using var opn_typ_aux True by blast
  next
  case False
    from var have 1: "wf_ctxt Γ" using wt_terms_impl_wf_ctxt wf_ctxt_cons by auto
    from var have "(y,σ) ∈ set ((x, τ) # Γ)" apply (cases rule:wt_trm.cases) by auto
    with False have 2: "(y,σ) ∈ set Γ" by simp

    show ?thesis
    using False apply simp
    apply (rule_tac wt_trm.var)
    using 1 2 by simp+
  qed
next
case (app M' N')
  from app(5) obtain π where  "(x, τ) # Γ ⊢ M' : π → σ" "(x, τ) # Γ ⊢ N' : π" 
    by (cases rule:wt_trm.cases, simp)
  with app(2,4,6) have ih: "Γ ⊢ M'[x ::= N] : π → σ" "Γ ⊢ N'[x ::= N] : π" by simp+
  show ?case
  unfolding subst.simps
  apply (rule wt_trm.app)
  using ih by simp+
next
case (lam L M)
  from lam(4) obtain π δ where 1: "σ = π → δ" "(x, τ) # Γ ⊢ Lam M : π → δ" by (cases rule:wt_trm.cases, simp)
  
  from 1(2) have "∃L. finite L ∧ (∀x'. x' ∉ L ⟶ (x', π) # (x, τ) # Γ ⊢ M^FVar x' : δ)"
  apply (drule_tac subst[OF wt_trm.simps])
  by simp
  then obtain L' where 2: "finite L'" "⋀x'. x' ∉ L' ⟹ (x', π) # (x, τ) # Γ ⊢ M^FVar x' : δ" by auto                                                         
  from 2(2) have 3: "⋀x'. x' ∉ L' ⟹ (x, τ) # (x', π) # Γ ⊢ M^FVar x' : δ" by (rule exchange)

  show ?case apply (subst subst.simps)
  unfolding 1(1)
  apply (rule_tac L="L ∪ L' ∪ {x} ∪ fst ` set Γ" in wt_trm.abs)
  using lam 2 apply simp
  apply (subst subst_open_var2)
  using trm_wt_trm lam apply simp
  apply auto[1]
  apply (rule lam(3))
  apply simp
  apply (rule 3)
  apply simp
  apply (rule weakening)
  using lam apply simp
  apply auto[1]
  apply (rule wf_ctxt.cons)
  apply simp
  using lam wt_terms_impl_wf_ctxt by simp
next
case (Y γ)
  from Y(1) have 1: "σ = (γ → γ) → γ" by (cases rule:wt_trm.cases, simp)
  show ?case unfolding subst.simps 1
  apply (rule wt_trm.Y)
  using Y wt_terms_impl_wf_ctxt wf_ctxt_cons by simp
qed

lemma opn_typ:
  fixes L
  assumes "finite L" "⋀x. x ∉ L ⟹ ((x,τ)#Γ) ⊢ M^FVar x : σ" and "Γ ⊢ N : τ"
  shows "Γ ⊢ M^N : σ"
proof -
  obtain x where 1: "x ∉ L ∪ FV M" using assms by (meson FV_finite finite_UnI x_Ex)
  with assms have 2: "((x,τ)#Γ) ⊢ M^FVar x : σ" by simp

  show ?thesis
  apply (subst subst_intro2[where x=x])
  apply (rule trm_wt_trm)
  using assms apply simp
  using 1 apply simp
  apply (rule subst_typ)
  apply (rule trm_wt_trm)
  using 2 apply simp
  apply (rule assms(2))
  using 1 apply simp
  using assms by simp
qed

lemma beta_Y_typ:
  assumes "Γ ⊢ M : σ"
  and "M ⇒ M'"
  shows "Γ ⊢ M' : σ"
using assms(2,1)
proof (induct  M M' arbitrary: Γ σ rule: beta_Y.induct)
case (red_L N M M')
  from red_L(4) obtain τ where 1: "Γ ⊢ M : τ → σ" "Γ ⊢ N : τ"
    apply (cases rule:wt_trm.cases) by simp
  with red_L(3) have "Γ ⊢ M' : τ → σ" by simp
  thus ?case 
    apply (rule wt_trm.app)
    using 1 by simp
next
case (red_R M N N')
  from red_R(4) obtain τ where 1: "Γ ⊢ M : τ → σ" "Γ ⊢ N : τ"
    apply (cases rule:wt_trm.cases) by simp
  with red_R(3) have 2: "Γ ⊢ N' : τ" by simp
  show ?case 
    apply (rule wt_trm.app)
    using 1 2 by simp+
next
case (abs L M M')
  from abs(4) obtain π τ where 1: "σ = π → τ" "Γ ⊢ Lam M : π → τ"
    apply (cases rule:wt_trm.cases) using abs.prems by blast
  from 1(2) have "∃L. finite L ∧ (∀x. x ∉ L ⟶ (x, π) # Γ ⊢ M^FVar x : τ)"
  apply (drule_tac subst[OF wt_trm.simps])
  by simp
  then obtain L' where 2: "finite L'" "⋀x. x ∉ L' ⟹ (x, π) # Γ ⊢ M^FVar x : τ" by auto

  have 3: "⋀x. x ∉ L ∪ L' ⟹ ((x,π)#Γ) ⊢ M'^FVar x : τ"
  apply (rule abs(3))
  using 2 by auto

  show ?case
    apply (subst 1(1))
    apply (rule_tac L="L ∪ L'" in wt_trm.abs)
    using abs 2 3 by simp+
next
case (beta M N) 
  from beta(3) obtain τ where 1: "Γ ⊢ (Lam M) : τ → σ" "Γ ⊢ N : τ" 
    apply (cases rule:wt_trm.cases) by simp
  from 1(1) have 2: "∃L. finite L ∧ (∀x. x ∉ L ⟶ (x, τ) # Γ ⊢ M^FVar x : σ)"
  apply (drule_tac subst[OF wt_trm.simps])
  by simp
  then obtain L where 3: "finite L" "⋀x. x ∉ L ⟹ (x, τ) # Γ ⊢ M^FVar x : σ" by auto

  show ?case
  apply (rule_tac L=L in opn_typ)
  using 3 1(2) by auto
next
case (Y M τ)
  from Y(2) obtain π where 1: "Γ ⊢ (Y τ) : π → σ" "Γ ⊢ M : π" 
    apply (cases rule:wt_trm.cases) by simp
  have "Γ ⊢ (Y τ) : (τ → τ) → τ" apply (rule wt_trm.Y)
    using wt_terms_impl_wf_ctxt Y by simp
  with 1(1) have "π → σ = (τ → τ) → τ" apply (cases rule:wt_trm.cases) by simp
  then have 2: "π = τ → τ" "σ = τ" by simp+
  show ?case
    apply (subst 2)
    apply (rule wt_trm.app)
    defer
    apply (rule wt_trm.app)
    apply (rule wt_trm.Y)
    using wt_terms_impl_wf_ctxt Y apply simp
    using 1(2) 2(1) by simp+
qed

lemma beta_Y_c_typ:
  assumes "Γ ⊢ M : σ"
  and "beta_Y* M M'"
  shows "Γ ⊢ M' : σ"
using assms(2,1)
apply (induct M M' arbitrary: σ rule: close.induct)
using beta_Y_typ by auto

subsection {* Church Rosser Theorem *}

lemma church_rosser_typ:
  assumes "Γ ⊢ a : σ"
      and "beta_Y* a b"
      and "beta_Y* a c"
    shows "∃d. beta_Y* b d ∧ beta_Y* c d ∧ Γ ⊢ d : σ"
proof -
  from assms have "pbeta* a b" "pbeta* a c" using M1 base by simp+
  then obtain d where "pbeta* b d" "pbeta* c d" by (metis DP_R_R_imp_DP_Rc_Rc_pbeta DP_def Lem2_5_2) 
  thus ?thesis using M2 beta_Y_c_typ assms by blast
qed
end