Theory LamYNom (Isabelle2016: February 2016)

section {* Nominal implementation in Isabelle *}
(*Disclaimer: Some of the definitions were copied over and adapted from 
Nominal2-Isabelle2015/Nominal/Nominal2/Ex/Lambda.thy *)

theory LamYNom
imports "Nominal2-Isabelle/Nominal/Nominal2" begin

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

atom_decl name

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

nominal_datatype trm =
  Var name
| App trm trm
| Lam x::name l::trm  binds x in l ("Lam [_]. _" [100, 100] 100)
| Y type

subsection {* Definition of substitution *}

nominal_function
  subst :: "trm ⇒ name ⇒ trm ⇒ trm"  ("_ [_ ::= _]" [90, 90, 90] 90)
where
  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
| "atom x ♯ (y, s) ⟹ (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
| "(Y t)[y ::= s] = Y t"
apply(simp add: eqvt_def subst_graph_aux_def)
apply(rule TrueI)
using [[simproc del: alpha_lst]]
apply(auto)
apply(rule_tac y="a" and c="(aa, b)" in trm.strong_exhaust)
apply(blast)+
apply(simp_all add: fresh_star_def fresh_Pair_elim)
apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
apply(simp_all add: Abs_fresh_iff)
apply(simp add: fresh_star_def fresh_Pair)
apply(simp only: eqvt_at_def)
apply(simp)
apply(simp add: fresh_star_Pair perm_supp_eq)
apply(simp only: eqvt_at_def)
apply(perm_simp)
apply(simp)
apply(simp add: fresh_star_Pair perm_supp_eq)
done
nominal_termination (eqvt)
by lexicographic_order

lemma forget:
  shows "atom x ♯ t ⟹ t[x ::= s] = t"
by (nominal_induct t avoiding: x s rule: trm.strong_induct)
   (auto simp add: fresh_at_base)

lemma fresh_type:
  fixes n :: name and t :: type
  shows "atom n ♯ t"
by (nominal_induct t rule:type.strong_induct, auto)

lemma fresh_fact:
  fixes z::"name"
  assumes a: "atom z ♯ s"
      and b: "z = y ∨ atom z ♯ t"
  shows "atom z ♯ t[y ::= s]"
using a b
apply (nominal_induct t avoiding: z y s rule: trm.strong_induct)
by (auto simp add:fresh_type)

lemma substitution_lemma:  
  assumes a: "x ≠ y" "atom 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: trm.strong_induct)
   (auto simp add: fresh_fact forget)

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

inductive 
  beta_Y :: "trm ⇒ trm ⇒ bool" (" _ ⇒ _" [80,80] 80)
where
  red_L[intro]: "⟦ M ⇒ M' ⟧ ⟹ App M N ⇒ App M' N"
| red_R[intro]: "⟦ N ⇒ N' ⟧ ⟹ App M N ⇒ App M N'"
| abs[intro]: "⟦ M ⇒ M' ⟧ ⟹ Lam [x]. M ⇒ Lam [x]. M'"
| beta[intro]: "⟦ atom x ♯ N ⟧ ⟹ App (Lam [x]. M) N ⇒ M[x ::= N]"
(*| eta[intro]: "⟦ atom x ♯ M ⟧ ⟹ App (Lam [x]. M) (Var x) ⇒Y M"*)
| Y[intro]: "App (Y σ) M ⇒ App M (App (Y σ) M)"

equivariance beta_Y
nominal_inductive beta_Y
  avoids beta: "x" | abs: "x"
by (simp_all add: fresh_star_def fresh_Pair fresh_fact fresh_type)

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

inductive 
  pbeta :: "trm ⇒ trm ⇒ bool" ("_ ≫ _" [80,80] 80)
where
  refl[intro]: "(Var x) ≫ (Var x)"
| reflY[intro]: "Y σ ≫ Y σ"
| app[intro]: "⟦ M ≫ M' ; N ≫ N' ⟧ ⟹ App M N ≫ App M' N'"
| abs[intro]: "⟦ M ≫ M' ⟧ ⟹ Lam [x]. M ≫ Lam [x]. M'"
| beta[intro]: "⟦ atom x ♯ N ; atom x ♯ N' ; M ≫ M' ; N ≫ N' ⟧ ⟹ App (Lam [x]. M) N ≫ M'[x ::= N']"
| Y[intro]: "⟦ M ≫ M' ⟧ ⟹ App (Y σ) M ≫ App M' (App (Y σ) M')"
equivariance pbeta

nominal_inductive pbeta
 avoids beta: "x" | abs: "x"
by (simp_all add: fresh_star_def fresh_Pair fresh_fact fresh_type)

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

nominal_function 
  not_abst :: "trm ⇒ bool"
where
  "not_abst (Var x) = True"
| "not_abst (App t1 t2) = True"
| "not_abst (Lam [x]. t) = False"
| "not_abst (Y t) = True"
apply (simp add: eqvt_def not_abst_graph_aux_def)
apply (rule TrueI)
apply (rule_tac y="x" in trm.exhaust)
using [[simproc del: alpha_lst]]
by auto
nominal_termination (eqvt) by lexicographic_order

nominal_function 
  not_Y :: "trm ⇒ bool"
where
  "not_Y (Var x) = True"
| "not_Y (App t1 t2) = True"
| "not_Y (Lam [x]. t) = True"
| "not_Y (Y t) = False"
apply (simp add: eqvt_def not_Y_graph_aux_def)
apply (rule TrueI)
apply (rule_tac y="x" in trm.exhaust)
using [[simproc del: alpha_lst]]
by auto
nominal_termination (eqvt) by lexicographic_order

inductive 
  pbeta_max :: "trm ⇒ trm ⇒ bool" ("_ >>> _" [80,80] 80)
where
  refl[intro]: "(Var x) >>> (Var 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]: "⟦ M >>> M' ⟧ ⟹ Lam [x]. M >>> Lam [x]. M'"
| beta[intro]: "⟦ atom x ♯ N ; atom x ♯ N' ; M >>> M' ; N >>> N' ⟧ ⟹ App (Lam [x]. M) N >>> M'[x ::= N']"
| Y[intro]: "⟦ M >>> M' ⟧ ⟹ App (Y σ) M >>> App M' (App (Y σ) M')"
equivariance pbeta_max

nominal_inductive pbeta_max
  avoids beta: "x" | abs: "x" (*don't understand what this does exactly or why we need it in the abs case ...*)
by (simp_all add: fresh_star_def fresh_Pair fresh_fact fresh_type)

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

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

lemma pbeta_max_ex:
  fixes M
  shows "∃M'. M >>> M'"
apply (induct M rule:trm.induct)
apply auto
apply (case_tac "not_abst trm1")
apply (case_tac "not_Y trm1")
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(2))
  thus ?case unfolding 2 by auto
next
case (2 P Q P' Q')
  thus ?case
  apply (nominal_induct P P' avoiding: Q Q' rule:pbeta_max.strong_induct)
  by auto
qed

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

lemma subst_rename: 
  assumes a: "atom y ♯ t"
  shows "t[x ::= s] = ((y ↔ x) ∙ t)[y ::= s]"
using a 
apply (nominal_induct t avoiding: x y s rule: trm.strong_induct)
apply (auto simp add: fresh_at_base)
by (simp add: flip_fresh_fresh fresh_type)

lemma fresh_in_pbeta: "s ≫ s' ⟹ atom (x::name) ♯ s ⟹  atom x ♯ s'"
apply (nominal_induct s s' rule:pbeta.strong_induct)
apply simp
apply simp
apply auto[1]
proof goal_cases
case 1 thus ?case by auto
next
case (2 xx N N' M M')
  then have "atom x ♯ N'" by simp
  { assume "x = xx" with 2 have ?case by (simp add: fresh_fact) }
  { assume "x ≠ xx" with 2 have ?case by (simp add: fresh_fact) }
  thus ?case using ‹x = xx ⟹ atom x ♯ M' [xx ::= N']› by blast
next
case 3 thus ?case by simp
qed

lemma pbeta_lam_case_ex: "(Lam [x]. s) ≫ s' ⟹ ∃t. s' = Lam [x]. t ∧ s ≫ t"
proof (cases "(Lam [x]. s)" s' rule:pbeta.cases, simp)
  case (goal1 _ _ x')
    then have 1: "s ≫ ((x' ↔ x) ∙ M')" using pbeta.eqvt by (metis Abs1_eq_iff(3) Nominal2_Base.swap_self add_flip_cancel flip_commute flip_def permute_flip_cancel2 permute_plus)
    from goal1 have 2: "(x' ↔ x) ∙ s' = Lam [x]. ((x' ↔ x) ∙ M')" by simp
    from goal1 have "atom x ♯ (Lam [x']. M')"  using fresh_in_pbeta by (meson trm.fresh(3) list.set_intros(1))
    with 2 have "s' = Lam [x]. ((x' ↔ x) ∙ M')" unfolding goal1 by (metis "2" flip_fresh_fresh goal1(3) trm.fresh(3) list.set_intros(1))
    with 1 show ?case by auto
qed

lemma pbeta_cases_2:
  shows "atom x ♯ t ⟹ App (Lam [x]. s) t ≫ a2 ⟹ 
    (⋀s' t'. a2 = App (Lam [x]. s') t' ⟹ atom x ♯ t' ⟹ s ≫ s' ⟹ t ≫ t' ⟹ P) ⟹
    (⋀t' s'. a2 = s' [x ::= t'] ⟹ atom x ♯ t ⟹ atom x ♯ t' ⟹ s ≫ s' ⟹ t ≫ t' ⟹ P) ⟹ P"
apply atomize_elim
proof (cases "App (Lam [x]. s) t" a2 rule:pbeta.cases, simp)
case goal1 
  then obtain s'' where 1: "M' = Lam [x]. s''" "s ≫ s''" using pbeta_lam_case_ex by blast
  thus ?case using goal1 fresh_in_pbeta  by auto
next
case (goal2 xx _ ss)
  have 1: "M' [xx ::= N'] = ((x ↔ xx) ∙ M') [x ::= N']"
    by (metis (no_types, lifting) Abs1_eq_iff(3) Nominal2_Base.swap_self add_flip_cancel flip_def fresh_in_pbeta goal2(3) goal2(7) permute_flip_cancel permute_plus subst_rename) 
  from goal2 have 2: "s ≫ ((x ↔ xx) ∙ M')"
    by (metis Abs1_eq_iff(3) Nominal2_Base.swap_self add_flip_cancel flip_def pbeta.eqvt permute_flip_cancel permute_plus)
  from goal2 have 3: "atom x ♯ N'" using fresh_in_pbeta by simp
  with goal2 1 2 show ?case by auto
qed

lemma Lem2_5_1:
  assumes "s ≫ s'"
      and "t ≫ t'"
      shows "(s[x ::= t]) ≫ (s'[x ::= t'])"
using assms proof (nominal_induct s s' avoiding: x t t' rule:pbeta.strong_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 p p' y) 
  show ?case 
  apply (subst subst.simps)
  using abs apply simp
  apply (subst subst.simps)
  using abs apply simp
  apply (rule_tac pbeta.abs)
  using abs by simp
next
case (beta y q q' p p')
  have "App ((Lam [y]. p) [x ::= t]) (q [x ::= t]) ≫ (p' [x ::= t'])[y ::= q'[x ::= t']]"
  apply (subst subst.simps(3))
  defer
  apply (rule_tac pbeta.beta)
  using beta by (simp add: fresh_fact)+

  then show ?case unfolding subst.simps
  apply (subst substitution_lemma) 
  using beta by (simp add: fresh_fact)+
next
case (Y M M' σ) 
  show ?case unfolding subst.simps
  apply (rule_tac pbeta.Y)
  using Y by simp
qed

lemma pbeta_max_closes_pbeta:
  fixes a b d
  assumes "a >>> d"
  and "a ≫ b"
  shows "b ≫ d"
using assms proof (nominal_induct arbitrary: b rule:pbeta_max.strong_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 x Q Qmax P Pmax)
  from beta(1,7) show ?case
  apply (rule_tac pbeta_cases_2)
  apply (simp, simp)
  proof -
  case (goal2 Q' P')
    with beta have "P' ≫ Pmax" "Q' ≫ Qmax" by simp+
    thus ?case unfolding goal2 apply (rule_tac Lem2_5_1) by simp+
  next
  case (goal1 P' Q')
    with beta have ih: "P' ≫ Pmax" "Q' ≫ Qmax" by simp+
    show ?case unfolding goal1 
    apply (rule_tac pbeta.beta) using goal1 beta ih
    by simp_all
  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 al ald x) thus ?case using pbeta_lam_case_ex by blast
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 by auto
  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 :: "(trm ⇒ trm ⇒ bool) ⇒ trm ⇒ trm ⇒ bool" ("_* _  _" [80,80] 80) for R::"trm ⇒ trm ⇒ 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"

subsection {* Proof of $\dip(\red^*)$ *}

definition DP :: "(trm ⇒ trm ⇒ bool) ⇒ (trm ⇒ trm ⇒ 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]: "s ≫ s"
apply (induct s rule:trm.induct)
by auto

lemma M1': "M ⇒ M' ⟹ M ≫ M'"
apply (induct M M' rule:beta_Y.induct)
by auto

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' ⟹ beta_Y* (App M N) (App M N')"
apply (induct rule:close.induct)
by auto

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

lemma abs_close: "beta_Y* M M' ⟹ beta_Y* (Lam [x]. M) (Lam [x]. M')"
apply (induct rule:close.induct)
by auto


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(4) apply auto[1]
    using red_l_close app.hyps(2) by auto[1]
  next
  case (abs M M' x)
    show ?case
    using abs abs_close by simp
  next
  case (beta x N N' M M')
    show ?case
    apply (rule_tac b="App (Lam [x]. M') N" in close.trans)
    apply (rule red_l_close)
    apply (rule abs_close)
    using beta apply simp
    apply (rule_tac b="App (Lam [x]. M') N'" in close.trans)
    apply (rule red_r_close)
    using beta apply simp
    apply (rule close.base)
    apply (rule beta_Y.beta)
    using beta 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)
    apply (rule_tac b="App M' (App (Y σ) M)" in close.trans)
    apply (rule red_l_close)
    using Y apply simp
    apply (rule red_r_close)
    apply (rule red_r_close)
    using Y by simp
  qed
qed

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

inductive wf_ctxt :: "(name × type) list ⇒ bool"
where
    nil:  "wf_ctxt []"
  | cons:  "⟦ wf_ctxt Γ ; atom x ♯ Γ ⟧ ⟹ wf_ctxt ((x,σ)#Γ)"
equivariance wf_ctxt

inductive
  wt_terms :: "(name × type) list ⇒ trm ⇒ type ⇒ bool" ("_ ⊢ _ : _")
where
  var: "⟦ (x,σ) ∈ set Γ ; wf_ctxt Γ ⟧ ⟹ Γ ⊢ Var x : σ"
| app: "⟦ Γ ⊢ M : σ → τ ; Γ ⊢ N : σ ⟧ ⟹ Γ ⊢ App M N : τ"
(* condition "atom x ♯ Γ" in abst should ensure that (x,σ) is consistent with Γ *)
| abs: "⟦ atom x ♯ Γ ; ((x,σ)#Γ) ⊢ M : τ ⟧ ⟹ Γ ⊢ Lam [x]. M : σ → τ"
| Y: "⟦ wf_ctxt Γ ⟧ ⟹  Γ ⊢ Y σ : (σ → σ) → σ"
equivariance wt_terms

nominal_inductive wt_terms
avoids abs: "x" 
by (simp_all add: fresh_star_def fresh_Pair fresh_fact fresh_type)

subsection {* Subject reduction theorem for $\red$ *}

lemma wf_ctxt_cons: "wf_ctxt ((x, σ)#Γ) ⟹ wf_ctxt Γ ∧ atom x ♯ Γ"
apply (cases rule:wf_ctxt.cases)
by auto

lemma wt_terms_impl_wf_ctxt: "Γ ⊢ M : σ ⟹ wf_ctxt Γ"
apply (induct rule:wt_terms.induct)
by (auto simp add: wf_ctxt_cons)

lemma weakening:
  fixes Γ Γ' M σ
  assumes "Γ ⊢ M : σ" and "set Γ ⊆ set Γ'"
  and "wf_ctxt Γ'"
  shows "Γ' ⊢ M : σ"
using assms proof (nominal_induct Γ M σ avoiding: Γ' rule:wt_terms.strong_induct)
case var 
  show ?case 
  apply (rule wt_terms.var) 
  using var by auto
next
case app
  show ?case
  apply (rule wt_terms.app)
  using app by auto
next
case (abs x Γ σ M τ)
  have 1: "wf_ctxt ((x, σ) # Γ')" 
  apply (rule cons)
  using abs by simp+

  show ?case
  apply (rule wt_terms.abs)
  using "1" wf_ctxt.cases apply auto[1]
  apply (rule abs(4))
  using abs apply auto[1]
  using 1 by simp
next
case Y thus ?case using wt_terms.Y by simp
qed

lemma wf_ctxt_exchange: "wf_ctxt ((x,σ) # (y,π) # Γ) ⟹ wf_ctxt ((y,π) # (x,σ) # Γ)"
proof goal_cases
case 1 
  then have 1: "wf_ctxt ((y,π) # Γ)" "atom x ♯ ((y,π) # Γ)" by (simp add: wf_ctxt_cons)+
  from 1(1) have 2: "wf_ctxt Γ" "atom y ♯ Γ" by (simp add: wf_ctxt_cons)+
  from 1(2) have 3: "atom x ♯ Γ" using fresh_Cons by blast
  from 1(2) 2(2) have 4: "atom y ♯ ((x,σ) # Γ)" by (metis fresh_Cons fresh_Pair fresh_at_base(2) fresh_type)

  show ?case
  apply (rule cons)
  apply (rule cons)
  by (simp add: 2 3 4)+
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  wt_terms_cases_2:
  shows "Γ ⊢ Lam [x]. M : a3 ⟹ atom x ♯ Γ⟹ (⋀σ τ. a3 = σ → τ ⟹ ((x, σ)#Γ) ⊢ M : τ ⟹ P) ⟹ P"
apply atomize_elim
apply (cases Γ "Lam [x]. M" a3 rule:wt_terms.cases, simp)
proof goal_cases
case (1 x' σ M' τ) 
  then have 2: "M = (x' ↔ x) ∙ M'"
  by (metis Abs1_eq_iff'(3) Nominal2_Base.swap_self flip_commute flip_def permute_zero)
  from 1 have "((x' ↔ x) ∙ ((x', σ) # Γ)) ⊢ (x' ↔ x) ∙ M' : (x' ↔ x) ∙ τ"
  by (rule_tac wt_terms.eqvt)
  with 2 fresh_type have 3: "((x' ↔ x) ∙ ((x', σ) # Γ)) ⊢ M : τ" by (simp add: flip_fresh_fresh)

  have "(x' ↔ x) ∙ (x', σ) = (x, σ)" using fresh_type by (simp add: flip_fresh_fresh)
  then have "(x' ↔ x) ∙ ((x', σ) # Γ) = (x, σ) # ((x' ↔ x) ∙ Γ)" by simp

  with 3 have 4: "(x, σ) # ((x' ↔ x) ∙ Γ) ⊢ M : τ" by simp
  with 4 1 have "(x, σ) # Γ ⊢ M : τ" by (simp add: flip_fresh_fresh)
  with 1  show ?case by simp
qed

lemma subst_typ_aux: "(x, τ) # Γ ⊢ Var 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 "atom y ♯ Γ" by (simp add: wf_ctxt_cons)
  then have "(y, σ) ∉ set Γ" by (metis (mono_tags, lifting) fresh_Cons fresh_PairD(1) fresh_append fresh_at_base(2) split_list)
  with 1(3) have 2: "(y, σ) ∉ set ((y, τ) # Γ)" by simp
  from 1(1) have "(y, σ) ∈ set ((y, τ) # Γ)" apply (cases rule:wt_terms.cases) by auto
  with 2 show ?case by simp
qed

lemma subst_typ:
  assumes "((x,τ)#Γ) ⊢ M : σ" and "Γ ⊢ N : τ"
  shows "Γ ⊢ M[x ::= N] : σ"
using assms proof (nominal_induct M avoiding: Γ x N arbitrary: σ rule: trm.strong_induct)
case (Var y)
  show ?case
  proof (cases "x = y")
  case True 
    show ?thesis 
    apply (simp add: True)
    using Var subst_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_terms.cases) by auto
    with False have 2: "(y,σ) ∈ set Γ" by simp

    show ?thesis
    apply (simp add: False)
    using Var
    apply (rule_tac wt_terms.var)
    using 1 2 by simp+
  qed
next
case (App M' N')
  from App(3) obtain π where  "(x, τ) # Γ ⊢ M' : π → σ" "(x, τ) # Γ ⊢ N' : π" 
    by (cases rule:wt_terms.cases, simp)
  with App(1,2,4) have ih: "Γ ⊢ M'[x ::= N] : π → σ" "Γ ⊢ N'[x ::= N] : π" by simp+
  show ?case
  unfolding subst.simps
  apply (rule wt_terms.app)
  using ih by simp+
next
case (Lam x' M)
  from Lam(5) obtain π δ where 1: "σ = π → δ" "(x, τ) # Γ ⊢ Lam [x']. M : π → δ" by (cases rule:wt_terms.cases, simp)
  from 1(2) have "(x', π) # (x, τ) # Γ ⊢ M : δ" apply (rule wt_terms_cases_2)
    using Lam(1,2) apply (simp add: fresh_Cons fresh_Pair fresh_type)
    by simp
  then have "(x, τ) # (x', π) # Γ ⊢ M : δ" by (rule exchange)

  with Lam(4,6) have ih: "(x', π) # Γ ⊢ M [x ::= N] : δ"
    by (meson Lam.hyps(1) cons set_subset_Cons weakening wt_terms_impl_wf_ctxt)

  show ?case apply (subst subst.simps)
  using Lam apply simp
  unfolding 1(1)
  apply (rule wt_terms.abs)
  using Lam apply simp
  using ih by simp
next
case (Y γ)
  from Y(1) have 1: "σ = (γ → γ) → γ" by (cases rule:wt_terms.cases, simp)
  show ?case unfolding subst.simps 1
  apply (rule wt_terms.Y)
  using Y wt_terms_impl_wf_ctxt wf_ctxt_cons by simp
qed

lemma beta_Y_typ:
  assumes "Γ ⊢ M : σ"
  and "M ⇒ M'"
  shows "Γ ⊢ M' : σ"
using assms(2,1)
proof (nominal_induct  M M' avoiding: Γ arbitrary: σ rule: beta_Y.strong_induct)
case (red_L M M' N)
  from red_L(3) obtain τ where 1: "Γ ⊢ M : τ → σ" "Γ ⊢ N : τ"
    apply (cases rule:wt_terms.cases) by simp
  with red_L(2) have "Γ ⊢ M' : τ → σ" by simp
  thus ?case 
    apply (rule wt_terms.app)
    using 1 by simp
next
case (red_R N N' M)
  from red_R(3) obtain τ where 1: "Γ ⊢ M : τ → σ" "Γ ⊢ N : τ"
    apply (cases rule:wt_terms.cases) by simp
  with red_R(2) have 2: "Γ ⊢ N' : τ" by simp
  show ?case 
    apply (rule wt_terms.app)
    using 1 2 by simp+
next
case (abs M M' x)
  from abs(4) obtain π τ where 1: "σ = π → τ" "Γ ⊢ Lam [x]. M : π → τ"
    apply (cases rule:wt_terms.cases) using abs.prems by blast
  from 1(2) abs(1) have 2: "((x,π)#Γ) ⊢ M : τ" by (rule wt_terms_cases_2, simp)
  with abs(3) have 3: "((x,π)#Γ) ⊢ M' : τ" by simp
  
  show ?case
    apply (subst 1(1))
    apply (rule wt_terms.abs)
    using abs 2 3 by simp+
next
case (beta x N M) 
  from beta(3) obtain τ where 1: "Γ ⊢ Lam [x]. M : τ → σ" "Γ ⊢ N : τ" 
    apply (cases rule:wt_terms.cases) by simp
  from 1(1) beta(1) have 2: "((x,τ)#Γ) ⊢ M : σ" by (rule wt_terms_cases_2, simp)
  show ?case
    apply (rule subst_typ)
    using 2 1(2) by simp+
next
case (Y τ M)
  from Y obtain π where 1: "Γ ⊢ (Y τ) : π → σ" "Γ ⊢ M : π" 
    apply (cases rule:wt_terms.cases) by simp
  have "Γ ⊢ (Y τ) : (τ → τ) → τ" apply (rule wt_terms.Y)
    using wt_terms_impl_wf_ctxt Y by simp
  with 1(1) have "π → σ = (τ → τ) → τ" apply (cases rule:wt_terms.cases) by simp
  then have 2: "π = τ → τ" "σ = τ" by simp+
  show ?case
    apply (subst 2)
    apply (rule wt_terms.app)
    defer
    apply (rule wt_terms.app)
    apply (rule wt_terms.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