Theory CR

theory CR
imports Lam_Funs
begin

text ‹The Church-Rosser proof from Barendregt's book›

lemma forget: 
  assumes asm: "x♯L"
  shows "L[x::=P] = L"
using asm
proof (nominal_induct L avoiding: x P rule: lam.strong_induct)
  case (Var z)
  have "x♯Var z" by fact
  thus "(Var z)[x::=P] = (Var z)" by (simp add: fresh_atm)
next 
  case (App M1 M2)
  have "x♯App M1 M2" by fact
  moreover
  have ih1: "x♯M1 ⟹ M1[x::=P] = M1" by fact
  moreover
  have ih1: "x♯M2 ⟹ M2[x::=P] = M2" by fact
  ultimately show "(App M1 M2)[x::=P] = (App M1 M2)" by simp
next
  case (Lam z M)
  have vc: "z♯x" "z♯P" by fact+
  have ih: "x♯M ⟹  M[x::=P] = M" by fact
  have asm: "x♯Lam [z].M" by fact
  then have "x♯M" using vc by (simp add: fresh_atm abs_fresh)
  then have "M[x::=P] = M" using ih by simp
  then show "(Lam [z].M)[x::=P] = Lam [z].M" using vc by simp
qed

lemma forget_automatic: 
  assumes asm: "x♯L"
  shows "L[x::=P] = L"
  using asm 
by (nominal_induct L avoiding: x P rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_atm)

lemma fresh_fact: 
  fixes z::"name"
  assumes asms: "z♯N" "z♯L"
  shows "z♯(N[y::=L])"
using asms
proof (nominal_induct N avoiding: z y L rule: lam.strong_induct)
  case (Var u)
  have "z♯(Var u)" "z♯L" by fact+
  thus "z♯((Var u)[y::=L])" by simp
next
  case (App N1 N2)
  have ih1: "⟦z♯N1; z♯L⟧ ⟹ z♯N1[y::=L]" by fact
  moreover
  have ih2: "⟦z♯N2; z♯L⟧ ⟹ z♯N2[y::=L]" by fact
  moreover 
  have "z♯App N1 N2" "z♯L" by fact+
  ultimately show "z♯((App N1 N2)[y::=L])" by simp 
next
  case (Lam u N1)
  have vc: "u♯z" "u♯y" "u♯L" by fact+
  have "z♯Lam [u].N1" by fact
  hence "z♯N1" using vc by (simp add: abs_fresh fresh_atm)
  moreover
  have ih: "⟦z♯N1; z♯L⟧ ⟹ z♯(N1[y::=L])" by fact
  moreover
  have  "z♯L" by fact
  ultimately show "z♯(Lam [u].N1)[y::=L]" using vc by (simp add: abs_fresh)
qed

lemma fresh_fact_automatic: 
  fixes z::"name"
  assumes asms: "z♯N" "z♯L"
  shows "z♯(N[y::=L])"
  using asms 
by (nominal_induct N avoiding: z y L rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_atm)

lemma fresh_fact': 
  fixes a::"name"
  assumes a: "a♯t2"
  shows "a♯t1[a::=t2]"
using a 
by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_atm)

lemma substitution_lemma:  
  assumes a: "x≠y"
  and     b: "x♯L"
  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using a b
proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
  case (Var z) (* case 1: Variables*)
  have "x≠y" by fact
  have "x♯L" by fact
  show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")
  proof -
    { (*Case 1.1*)
      assume  "z=x"
      have "(1)": "?LHS = N[y::=L]" using ‹z=x› by simp
      have "(2)": "?RHS = N[y::=L]" using ‹z=x› ‹x≠y› by simp
      from "(1)" "(2)" have "?LHS = ?RHS"  by simp
    }
    moreover 
    { (*Case 1.2*)
      assume "z=y" and "z≠x" 
      have "(1)": "?LHS = L"               using ‹z≠x› ‹z=y› by simp
      have "(2)": "?RHS = L[x::=N[y::=L]]" using ‹z=y› by simp
      have "(3)": "L[x::=N[y::=L]] = L"    using ‹x♯L› by (simp add: forget)
      from "(1)" "(2)" "(3)" have "?LHS = ?RHS" by simp
    }
    moreover 
    { (*Case 1.3*)
      assume "z≠x" and "z≠y"
      have "(1)": "?LHS = Var z" using ‹z≠x› ‹z≠y› by simp
      have "(2)": "?RHS = Var z" using ‹z≠x› ‹z≠y› by simp
      from "(1)" "(2)" have "?LHS = ?RHS" by simp
    }
    ultimately show "?LHS = ?RHS" by blast
  qed
next
  case (Lam z M1) (* case 2: lambdas *)
  have ih: "⟦x≠y; x♯L⟧ ⟹ M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
  have "x≠y" by fact
  have "x♯L" by fact
  have fs: "z♯x" "z♯y" "z♯N" "z♯L" by fact+
  hence "z♯N[y::=L]" by (simp add: fresh_fact)
  show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
  proof - 
    have "?LHS = Lam [z].(M1[x::=N][y::=L])" using ‹z♯x› ‹z♯y› ‹z♯N› ‹z♯L› by simp
    also from ih have "… = Lam [z].(M1[y::=L][x::=N[y::=L]])" using ‹x≠y› ‹x♯L› by simp
    also have "… = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using ‹z♯x› ‹z♯N[y::=L]› by simp
    also have "… = ?RHS" using  ‹z♯y› ‹z♯L› by simp
    finally show "?LHS = ?RHS" .
  qed
next
  case (App M1 M2) (* case 3: applications *)
  thus "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp
qed

lemma substitution_lemma_automatic:  
  assumes asm: "x≠y" "x♯L"
  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
  using asm 
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
   (auto simp add: fresh_fact forget)

section ‹Beta Reduction›

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

equivariance Beta

nominal_inductive Beta
  by (simp_all add: abs_fresh fresh_fact')

inductive
  "Beta_star"  :: "lam⇒lam⇒bool" (‹ _ ⟶⇩β⇧* _› [80,80] 80)
where
    bs1[intro, simp]: "M ⟶⇩β⇧* M"
  | bs2[intro]: "⟦M1⟶⇩β⇧* M2; M2 ⟶⇩β M3⟧ ⟹ M1 ⟶⇩β⇧* M3"

equivariance Beta_star

lemma beta_star_trans:
  assumes a1: "M1⟶⇩β⇧* M2"
  and     a2: "M2⟶⇩β⇧* M3"
  shows "M1 ⟶⇩β⇧* M3"
using a2 a1
by (induct) (auto)

section ‹One-Reduction›

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

equivariance One

nominal_inductive One
  by (simp_all add: abs_fresh fresh_fact')

inductive
  "One_star"  :: "lam⇒lam⇒bool" (‹ _ ⟶⇩1⇧* _› [80,80] 80)
where
    os1[intro, simp]: "M ⟶⇩1⇧* M"
  | os2[intro]: "⟦M1⟶⇩1⇧* M2; M2 ⟶⇩1 M3⟧ ⟹ M1 ⟶⇩1⇧* M3"

equivariance One_star 

lemma one_star_trans:
  assumes a1: "M1⟶⇩1⇧* M2" 
  and     a2: "M2⟶⇩1⇧* M3"
  shows "M1⟶⇩1⇧* M3"
using a2 a1
by (induct) (auto)

lemma one_fresh_preserv:
  fixes a :: "name"
  assumes a: "t⟶⇩1s"
  and     b: "a♯t"
  shows "a♯s"
using a b
proof (induct)
  case o1 thus ?case by simp
next
  case o2 thus ?case by simp
next
  case (o3 s1 s2 c)
  have ih: "a♯s1 ⟹  a♯s2" by fact
  have c: "a♯Lam [c].s1" by fact
  show ?case
  proof (cases "a=c")
    assume "a=c" thus "a♯Lam [c].s2" by (simp add: abs_fresh)
  next
    assume d: "a≠c" 
    with c have "a♯s1" by (simp add: abs_fresh)
    hence "a♯s2" using ih by simp
    thus "a♯Lam [c].s2" using d by (simp add: abs_fresh) 
  qed
next 
  case (o4 c t1 t2 s1 s2)
  have i1: "a♯t1 ⟹ a♯t2" by fact
  have i2: "a♯s1 ⟹ a♯s2" by fact
  have as: "a♯App (Lam [c].s1) t1" by fact
  hence c1: "a♯Lam [c].s1" and c2: "a♯t1" by (simp add: fresh_prod)+
  from c2 i1 have c3: "a♯t2" by simp
  show "a♯s2[c::=t2]"
  proof (cases "a=c")
    assume "a=c"
    thus "a♯s2[c::=t2]" using c3 by (simp add: fresh_fact')
  next
    assume d1: "a≠c"
    from c1 d1 have "a♯s1" by (simp add: abs_fresh)
    hence "a♯s2" using i2 by simp
    thus "a♯s2[c::=t2]" using c3 by (simp add: fresh_fact)
  qed
qed

lemma one_fresh_preserv_automatic:
  fixes a :: "name"
  assumes a: "t⟶⇩1s"
  and     b: "a♯t"
  shows "a♯s"
using a b
apply(nominal_induct avoiding: a rule: One.strong_induct)
apply(auto simp add: abs_fresh fresh_atm fresh_fact)
done

lemma subst_rename: 
  assumes a: "c♯t1"
  shows "t1[a::=t2] = ([(c,a)]∙t1)[c::=t2]"
using a
by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct)
   (auto simp add: calc_atm fresh_atm abs_fresh)

lemma one_abs: 
  assumes a: "Lam [a].t⟶⇩1t'"
  shows "∃t''. t'=Lam [a].t'' ∧ t⟶⇩1t''"
proof -
  have "a♯Lam [a].t" by (simp add: abs_fresh)
  with a have "a♯t'" by (simp add: one_fresh_preserv)
  with a show ?thesis
    by (cases rule: One.strong_cases[where a="a" and aa="a"])
       (auto simp add: lam.inject abs_fresh alpha)
qed

lemma one_app: 
  assumes a: "App t1 t2 ⟶⇩1 t'"
  shows "(∃s1 s2. t' = App s1 s2 ∧ t1 ⟶⇩1 s1 ∧ t2 ⟶⇩1 s2) ∨ 
         (∃a s s1 s2. t1 = Lam [a].s ∧ t' = s1[a::=s2] ∧ s ⟶⇩1 s1 ∧ t2 ⟶⇩1 s2 ∧ a♯(t2,s2))"
using a by (erule_tac One.cases) (auto simp add: lam.inject)

lemma one_red: 
  assumes a: "App (Lam [a].t1) t2 ⟶⇩1 M" "a♯(t2,M)"
  shows "(∃s1 s2. M = App (Lam [a].s1) s2 ∧ t1 ⟶⇩1 s1 ∧ t2 ⟶⇩1 s2) ∨ 
         (∃s1 s2. M = s1[a::=s2] ∧ t1 ⟶⇩1 s1 ∧ t2 ⟶⇩1 s2)" 
using a
by (cases rule: One.strong_cases [where a="a" and aa="a"])
   (auto dest: one_abs simp add: lam.inject abs_fresh alpha fresh_prod)

text ‹first case in Lemma 3.2.4›

lemma one_subst_aux:
  assumes a: "N⟶⇩1N'"
  shows "M[x::=N] ⟶⇩1 M[x::=N']"
using a
proof (nominal_induct M avoiding: x N N' rule: lam.strong_induct)
  case (Var y) 
  thus "Var y[x::=N] ⟶⇩1 Var y[x::=N']" by (cases "x=y") auto
next
  case (App P Q) (* application case - third line *)
  thus "(App P Q)[x::=N] ⟶⇩1  (App P Q)[x::=N']" using o2 by simp
next 
  case (Lam y P) (* abstraction case - fourth line *)
  thus "(Lam [y].P)[x::=N] ⟶⇩1 (Lam [y].P)[x::=N']" using o3 by simp
qed

lemma one_subst_aux_automatic:
  assumes a: "N⟶⇩1N'"
  shows "M[x::=N] ⟶⇩1 M[x::=N']"
using a
by (nominal_induct M avoiding: x N N' rule: lam.strong_induct)
   (auto simp add: fresh_prod fresh_atm)

lemma one_subst: 
  assumes a: "M⟶⇩1M'"
  and     b: "N⟶⇩1N'"
  shows "M[x::=N]⟶⇩1M'[x::=N']" 
using a b
proof (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
  case (o1 M)
  thus ?case by (simp add: one_subst_aux)
next
  case (o2 M1 M2 N1 N2)
  thus ?case by simp
next
  case (o3 a M1 M2)
  thus ?case by simp
next
  case (o4 a N1 N2 M1 M2 N N' x)
  have vc: "a♯N" "a♯N'" "a♯x" "a♯N1" "a♯N2" by fact+
  have asm: "N⟶⇩1N'" by fact
  show ?case
  proof -
    have "(App (Lam [a].M1) N1)[x::=N] = App (Lam [a].(M1[x::=N])) (N1[x::=N])" using vc by simp
    moreover have "App (Lam [a].(M1[x::=N])) (N1[x::=N]) ⟶⇩1 M2[x::=N'][a::=N2[x::=N']]" 
      using o4 asm by (simp add: fresh_fact)
    moreover have "M2[x::=N'][a::=N2[x::=N']] = M2[a::=N2][x::=N']" 
      using vc by (simp add: substitution_lemma fresh_atm)
    ultimately show "(App (Lam [a].M1) N1)[x::=N] ⟶⇩1 M2[a::=N2][x::=N']" by simp
  qed
qed

lemma one_subst_automatic: 
  assumes a: "M⟶⇩1M'" 
  and     b: "N⟶⇩1N'"
  shows "M[x::=N]⟶⇩1M'[x::=N']" 
using a b
by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
   (auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)

lemma diamond[rule_format]:
  fixes    M :: "lam"
  and      M1:: "lam"
  assumes a: "M⟶⇩1M1" 
  and     b: "M⟶⇩1M2"
  shows "∃M3. M1⟶⇩1M3 ∧ M2⟶⇩1M3"
  using a b
proof (nominal_induct avoiding: M1 M2 rule: One.strong_induct)
  case (o1 M) (* case 1 --- M1 = M *)
  thus "∃M3. M⟶⇩1M3 ∧  M2⟶⇩1M3" by blast
next
  case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*)
  have vc: "x♯Q" "x♯Q'" "x♯M2" by fact+
  have i1: "⋀M2. Q ⟶⇩1M2 ⟹ (∃M3. Q'⟶⇩1M3 ∧ M2⟶⇩1M3)" by fact
  have i2: "⋀M2. P ⟶⇩1M2 ⟹ (∃M3. P'⟶⇩1M3 ∧ M2⟶⇩1M3)" by fact
  have "App (Lam [x].P) Q ⟶⇩1 M2" by fact
  hence "(∃P' Q'. M2 = App (Lam [x].P') Q' ∧ P⟶⇩1P' ∧ Q⟶⇩1Q') ∨ 
         (∃P' Q'. M2 = P'[x::=Q'] ∧ P⟶⇩1P' ∧ Q⟶⇩1Q')" using vc by (simp add: one_red)
  moreover (* subcase 2.1 *)
  { assume "∃P' Q'. M2 = App (Lam [x].P') Q' ∧ P⟶⇩1P' ∧ Q⟶⇩1Q'"
    then obtain P'' and Q'' where 
      b1: "M2=App (Lam [x].P'') Q''" and b2: "P⟶⇩1P''" and b3: "Q⟶⇩1Q''" by blast
    from b2 i2 have "(∃M3. P'⟶⇩1M3 ∧ P''⟶⇩1M3)" by simp
    then obtain P''' where
      c1: "P'⟶⇩1P'''" and c2: "P''⟶⇩1P'''" by force
    from b3 i1 have "(∃M3. Q'⟶⇩1M3 ∧ Q''⟶⇩1M3)" by simp
    then obtain Q''' where
      d1: "Q'⟶⇩1Q'''" and d2: "Q''⟶⇩1Q'''" by force
    from c1 c2 d1 d2 
    have "P'[x::=Q']⟶⇩1P'''[x::=Q'''] ∧ App (Lam [x].P'') Q'' ⟶⇩1 P'''[x::=Q''']" 
      using vc b3 by (auto simp add: one_subst one_fresh_preserv)
    hence "∃M3. P'[x::=Q']⟶⇩1M3 ∧ M2⟶⇩1M3" using b1 by blast
  }
  moreover (* subcase 2.2 *)
  { assume "∃P' Q'. M2 = P'[x::=Q'] ∧ P⟶⇩1P' ∧ Q⟶⇩1Q'"
    then obtain P'' Q'' where
      b1: "M2=P''[x::=Q'']" and b2: "P⟶⇩1P''" and  b3: "Q⟶⇩1Q''" by blast
    from b2 i2 have "(∃M3. P'⟶⇩1M3 ∧ P''⟶⇩1M3)" by simp
    then obtain P''' where
      c1: "P'⟶⇩1P'''" and c2: "P''⟶⇩1P'''" by blast
    from b3 i1 have "(∃M3. Q'⟶⇩1M3 ∧ Q''⟶⇩1M3)" by simp
    then obtain Q''' where
      d1: "Q'⟶⇩1Q'''" and d2: "Q''⟶⇩1Q'''" by blast
    from c1 c2 d1 d2 
    have "P'[x::=Q']⟶⇩1P'''[x::=Q'''] ∧ P''[x::=Q'']⟶⇩1P'''[x::=Q''']" 
      by (force simp add: one_subst)
    hence "∃M3. P'[x::=Q']⟶⇩1M3 ∧ M2⟶⇩1M3" using b1 by blast
  }
  ultimately show "∃M3. P'[x::=Q']⟶⇩1M3 ∧ M2⟶⇩1M3" by blast
next
  case (o2 P P' Q Q') (* case 3 *)
  have i0: "P⟶⇩1P'" by fact
  have i0': "Q⟶⇩1Q'" by fact
  have i1: "⋀M2. Q ⟶⇩1M2 ⟹ (∃M3. Q'⟶⇩1M3 ∧ M2⟶⇩1M3)" by fact
  have i2: "⋀M2. P ⟶⇩1M2 ⟹ (∃M3. P'⟶⇩1M3 ∧ M2⟶⇩1M3)" by fact
  assume "App P Q ⟶⇩1 M2"
  hence "(∃P'' Q''. M2 = App P'' Q'' ∧ P⟶⇩1P'' ∧ Q⟶⇩1Q'') ∨ 
         (∃x P' P'' Q'. P = Lam [x].P' ∧ M2 = P''[x::=Q'] ∧ P'⟶⇩1 P'' ∧ Q⟶⇩1Q' ∧ x♯(Q,Q'))" 
    by (simp add: one_app[simplified])
  moreover (* subcase 3.1 *)
  { assume "∃P'' Q''. M2 = App P'' Q'' ∧ P⟶⇩1P'' ∧ Q⟶⇩1Q''"
    then obtain P'' and Q'' where 
      b1: "M2=App P'' Q''" and b2: "P⟶⇩1P''" and b3: "Q⟶⇩1Q''" by blast
    from b2 i2 have "(∃M3. P'⟶⇩1M3 ∧ P''⟶⇩1M3)" by simp
    then obtain P''' where
      c1: "P'⟶⇩1P'''" and c2: "P''⟶⇩1P'''" by blast
    from b3 i1 have "∃M3. Q'⟶⇩1M3 ∧ Q''⟶⇩1M3" by simp
    then obtain Q''' where
      d1: "Q'⟶⇩1Q'''" and d2: "Q''⟶⇩1Q'''" by blast
    from c1 c2 d1 d2 
    have "App P' Q'⟶⇩1App P''' Q''' ∧ App P'' Q'' ⟶⇩1 App P''' Q'''" by blast
    hence "∃M3. App P' Q'⟶⇩1M3 ∧ M2⟶⇩1M3" using b1 by blast
  }
  moreover (* subcase 3.2 *)
  { assume "∃x P1 P'' Q''. P = Lam [x].P1 ∧ M2 = P''[x::=Q''] ∧ P1⟶⇩1 P'' ∧ Q⟶⇩1Q'' ∧ x♯(Q,Q'')"
    then obtain x P1 P1'' Q'' where
      b0: "P = Lam [x].P1" and b1: "M2 = P1''[x::=Q'']" and 
      b2: "P1⟶⇩1P1''" and  b3: "Q⟶⇩1Q''" and vc: "x♯(Q,Q'')" by blast
    from b0 i0 have "∃P1'. P'=Lam [x].P1' ∧ P1⟶⇩1P1'" by (simp add: one_abs)      
    then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1⟶⇩1P1'" by blast 
    from g1 b0 b2 i2 have "(∃M3. (Lam [x].P1')⟶⇩1M3 ∧ (Lam [x].P1'')⟶⇩1M3)" by simp
    then obtain P1''' where
      c1: "(Lam [x].P1')⟶⇩1P1'''" and c2: "(Lam [x].P1'')⟶⇩1P1'''" by blast
    from c1 have "∃R1. P1'''=Lam [x].R1 ∧ P1'⟶⇩1R1" by (simp add: one_abs)
    then obtain R1 where r1: "P1'''=Lam [x].R1" and r2: "P1'⟶⇩1R1" by blast
    from c2 have "∃R2. P1'''=Lam [x].R2 ∧ P1''⟶⇩1R2" by (simp add: one_abs)
    then obtain R2 where r3: "P1'''=Lam [x].R2" and r4: "P1''⟶⇩1R2" by blast
    from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha)
    from b3 i1 have "(∃M3. Q'⟶⇩1M3 ∧ Q''⟶⇩1M3)" by simp
    then obtain Q''' where
      d1: "Q'⟶⇩1Q'''" and d2: "Q''⟶⇩1Q'''" by blast
    from g1 r2 d1 r4 r5 d2 
    have "App P' Q'⟶⇩1R1[x::=Q'''] ∧ P1''[x::=Q'']⟶⇩1R1[x::=Q''']" 
      using vc i0' by (simp add: one_subst one_fresh_preserv)
    hence "∃M3. App P' Q'⟶⇩1M3 ∧ M2⟶⇩1M3" using b1 by blast
  }
  ultimately show "∃M3. App P' Q'⟶⇩1M3 ∧ M2⟶⇩1M3" by blast
next
  case (o3 P P' x) (* case 4 *)
  have i1: "P⟶⇩1P'" by fact
  have i2: "⋀M2. P ⟶⇩1M2 ⟹ (∃M3. P'⟶⇩1M3 ∧ M2⟶⇩1M3)" by fact
  have "(Lam [x].P)⟶⇩1 M2" by fact
  hence "∃P''. M2=Lam [x].P'' ∧ P⟶⇩1P''" by (simp add: one_abs)
  then obtain P'' where b1: "M2=Lam [x].P''" and b2: "P⟶⇩1P''" by blast
  from i2 b1 b2 have "∃M3. (Lam [x].P')⟶⇩1M3 ∧ (Lam [x].P'')⟶⇩1M3" by blast
  then obtain M3 where c1: "(Lam [x].P')⟶⇩1M3" and c2: "(Lam [x].P'')⟶⇩1M3" by blast
  from c1 have "∃R1. M3=Lam [x].R1 ∧ P'⟶⇩1R1" by (simp add: one_abs)
  then obtain R1 where r1: "M3=Lam [x].R1" and r2: "P'⟶⇩1R1" by blast
  from c2 have "∃R2. M3=Lam [x].R2 ∧ P''⟶⇩1R2" by (simp add: one_abs)
  then obtain R2 where r3: "M3=Lam [x].R2" and r4: "P''⟶⇩1R2" by blast
  from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha)
  from r2 r4 have "(Lam [x].P')⟶⇩1(Lam [x].R1) ∧ (Lam [x].P'')⟶⇩1(Lam [x].R2)" 
    by (simp add: one_subst)
  thus "∃M3. (Lam [x].P')⟶⇩1M3 ∧ M2⟶⇩1M3" using b1 r5 by blast
qed

lemma one_lam_cong: 
  assumes a: "t1⟶⇩β⇧*t2" 
  shows "(Lam [a].t1)⟶⇩β⇧*(Lam [a].t2)"
  using a
proof induct
  case bs1 thus ?case by simp
next
  case (bs2 y z) 
  thus ?case by (blast dest: b3)
qed

lemma one_app_congL: 
  assumes a: "t1⟶⇩β⇧*t2" 
  shows "App t1 s⟶⇩β⇧* App t2 s"
  using a
proof induct
  case bs1 thus ?case by simp
next
  case bs2 thus ?case by (blast dest: b1)
qed
  
lemma one_app_congR: 
  assumes a: "t1⟶⇩β⇧*t2" 
  shows "App s t1 ⟶⇩β⇧* App s t2"
using a
proof induct
  case bs1 thus ?case by simp
next 
  case bs2 thus ?case by (blast dest: b2)
qed

lemma one_app_cong: 
  assumes a1: "t1⟶⇩β⇧*t2" 
  and     a2: "s1⟶⇩β⇧*s2" 
  shows "App t1 s1⟶⇩β⇧* App t2 s2"
proof -
  have "App t1 s1 ⟶⇩β⇧* App t2 s1" using a1 by (rule one_app_congL)
  moreover
  have "App t2 s1 ⟶⇩β⇧* App t2 s2" using a2 by (rule one_app_congR)
  ultimately show ?thesis by (rule beta_star_trans)
qed

lemma one_beta_star: 
  assumes a: "(t1⟶⇩1t2)" 
  shows "(t1⟶⇩β⇧*t2)"
  using a
proof(nominal_induct rule: One.strong_induct)
  case o1 thus ?case by simp
next
  case o2 thus ?case by (blast intro!: one_app_cong)
next
  case o3 thus ?case by (blast intro!: one_lam_cong)
next 
  case (o4 a s1 s2 t1 t2)
  have vc: "a♯s1" "a♯s2" by fact+
  have a1: "t1⟶⇩β⇧*t2" and a2: "s1⟶⇩β⇧*s2" by fact+
  have c1: "(App (Lam [a].t2) s2) ⟶⇩β (t2 [a::= s2])" using vc by (simp add: b4)
  from a1 a2 have c2: "App (Lam [a].t1 ) s1 ⟶⇩β⇧* App (Lam [a].t2 ) s2" 
    by (blast intro!: one_app_cong one_lam_cong)
  show ?case using c2 c1 by (blast intro: beta_star_trans)
qed
 
lemma one_star_lam_cong: 
  assumes a: "t1⟶⇩1⇧*t2" 
  shows "(Lam  [a].t1)⟶⇩1⇧* (Lam [a].t2)"
  using a
proof induct
  case os1 thus ?case by simp
next
  case os2 thus ?case by (blast intro: one_star_trans)
qed

lemma one_star_app_congL: 
  assumes a: "t1⟶⇩1⇧*t2" 
  shows "App t1 s⟶⇩1⇧* App t2 s"
  using a
proof induct
  case os1 thus ?case by simp
next
  case os2 thus ?case by (blast intro: one_star_trans)
qed

lemma one_star_app_congR: 
  assumes a: "t1⟶⇩1⇧*t2" 
  shows "App s t1 ⟶⇩1⇧* App s t2"
  using a
proof induct
  case os1 thus ?case by simp
next
  case os2 thus ?case by (blast intro: one_star_trans)
qed

lemma beta_one_star: 
  assumes a: "t1⟶⇩βt2" 
  shows "t1⟶⇩1⇧*t2"
  using a
proof(induct)
  case b1 thus ?case by (blast intro!: one_star_app_congL)
next
  case b2 thus ?case by (blast intro!: one_star_app_congR)
next
  case b3 thus ?case by (blast intro!: one_star_lam_cong)
next
  case b4 thus ?case by auto 
qed

lemma trans_closure: 
  shows "(M1⟶⇩1⇧*M2) = (M1⟶⇩β⇧*M2)"
proof
  assume "M1 ⟶⇩1⇧* M2"
  then show "M1⟶⇩β⇧*M2"
  proof induct
    case (os1 M1) thus "M1⟶⇩β⇧*M1" by simp
  next
    case (os2 M1 M2 M3)
    have "M2⟶⇩1M3" by fact
    then have "M2⟶⇩β⇧*M3" by (rule one_beta_star)
    moreover have "M1⟶⇩β⇧*M2" by fact
    ultimately show "M1⟶⇩β⇧*M3" by (auto intro: beta_star_trans)
  qed
next
  assume "M1 ⟶⇩β⇧* M2" 
  then show "M1⟶⇩1⇧*M2"
  proof induct
    case (bs1 M1) thus  "M1⟶⇩1⇧*M1" by simp
  next
    case (bs2 M1 M2 M3) 
    have "M2⟶⇩βM3" by fact
    then have "M2⟶⇩1⇧*M3" by (rule beta_one_star)
    moreover have "M1⟶⇩1⇧*M2" by fact
    ultimately show "M1⟶⇩1⇧*M3" by (auto intro: one_star_trans)
  qed
qed

lemma cr_one:
  assumes a: "t⟶⇩1⇧*t1" 
  and     b: "t⟶⇩1t2"
  shows "∃t3. t1⟶⇩1t3 ∧ t2⟶⇩1⇧*t3"
  using a b
proof (induct arbitrary: t2)
  case os1 thus ?case by force
next
  case (os2 t s1 s2 t2)  
  have b: "s1 ⟶⇩1 s2" by fact
  have h: "⋀t2. t ⟶⇩1 t2 ⟹ (∃t3. s1 ⟶⇩1 t3 ∧ t2 ⟶⇩1⇧* t3)" by fact
  have c: "t ⟶⇩1 t2" by fact
  show "∃t3. s2 ⟶⇩1 t3 ∧  t2 ⟶⇩1⇧* t3" 
  proof -
    from c h have "∃t3. s1 ⟶⇩1 t3 ∧ t2 ⟶⇩1⇧* t3" by blast
    then obtain t3 where c1: "s1 ⟶⇩1 t3" and c2: "t2 ⟶⇩1⇧* t3" by blast
    have "∃t4. s2 ⟶⇩1 t4 ∧ t3 ⟶⇩1 t4" using b c1 by (blast intro: diamond)
    thus ?thesis using c2 by (blast intro: one_star_trans)
  qed
qed

lemma cr_one_star: 
  assumes a: "t⟶⇩1⇧*t2"
      and b: "t⟶⇩1⇧*t1"
    shows "∃t3. t1⟶⇩1⇧*t3∧t2⟶⇩1⇧*t3"
using a b
proof (induct arbitrary: t1)
  case (os1 t) then show ?case by force
next 
  case (os2 t s1 s2 t1)
  have c: "t ⟶⇩1⇧* s1" by fact
  have c': "t ⟶⇩1⇧* t1" by fact
  have d: "s1 ⟶⇩1 s2" by fact
  have "t ⟶⇩1⇧* t1 ⟹ (∃t3.  t1 ⟶⇩1⇧* t3 ∧ s1 ⟶⇩1⇧* t3)" by fact
  then obtain t3 where f1: "t1 ⟶⇩1⇧* t3"
                   and f2: "s1 ⟶⇩1⇧* t3" using c' by blast
  from cr_one d f2 have "∃t4. t3⟶⇩1t4 ∧ s2⟶⇩1⇧*t4" by blast
  then obtain t4 where g1: "t3⟶⇩1t4"
                   and g2: "s2⟶⇩1⇧*t4" by blast
  have "t1⟶⇩1⇧*t4" using f1 g1 by (blast intro: one_star_trans)
  thus ?case using g2 by blast
qed
  
lemma cr_beta_star: 
  assumes a1: "t⟶⇩β⇧*t1" 
  and     a2: "t⟶⇩β⇧*t2" 
  shows "∃t3. t1⟶⇩β⇧*t3∧t2⟶⇩β⇧*t3"
proof -
  from a1 have "t⟶⇩1⇧*t1" by (simp only: trans_closure)
  moreover
  from a2 have "t⟶⇩1⇧*t2" by (simp only: trans_closure)
  ultimately have "∃t3. t1⟶⇩1⇧*t3 ∧ t2⟶⇩1⇧*t3" by (blast intro: cr_one_star) 
  then obtain t3 where "t1⟶⇩1⇧*t3" and "t2⟶⇩1⇧*t3" by blast
  hence "t1⟶⇩β⇧*t3" and "t2⟶⇩β⇧*t3" by (simp_all only: trans_closure)
  then show "∃t3. t1⟶⇩β⇧*t3∧t2⟶⇩β⇧*t3" by blast
qed

end