Theory ParRed

(*  Title:      Sigma/ParRed.thy
    Author:     Ludovic Henrio and Florian Kammuller
    Copyright   2006

Confluence of beta for ASP, based on the equally named file in HOL/Proofs/Lambda.
*)

section ‹Parallel reduction›

theory ParRed imports "HOL-Proofs-Lambda.Commutation" Sigma begin

subsection ‹Parallel reduction›
inductive par_beta :: "[sterm,sterm]  bool"  (infixl "β" 50)
  where
  pbeta_Fvar[simp,intro!]: "Fvar x β Fvar x"
| pbeta_Obj[simp,intro!] : 
  " dom f' = dom f; finite L;
     ldom f. s p. s  L  p  L  s  p 
                  (t. (the(f l)⇗[Fvar s, Fvar p]⇖) β t 
                         the(f' l) = σ[s,p] t);
     ldom f. body (the(f l))   Obj f T β Obj f' T"
| pbeta_Upd[simp,intro!] : 
  " t β t'; lc t; finite L; 
     s p. s  L  p  L  s  p
       (t''. (u⇗[Fvar s, Fvar p]⇖) β t''  u' = σ[s,p] t'');
     body u   Upd t l u β Upd t' l u'"
| pbeta_Upd'[simp,intro!]: 
  " Obj f T β Obj f' T; finite L;
     s p. s  L  p  L  s  p
        (t''. (t⇗[Fvar s, Fvar p]⇖) β t''  t' = σ[s,p] t''); l  dom f;
     lc (Obj f T); body t   (Upd (Obj f T) l t)  β (Obj (f'(l  t')) T)"
| pbeta_Call[simp,intro!]: 
  " t β t'; u β u'; lc t; lc u 
   Call t l u β Call t' l u'"
| pbeta_beta[simp,intro!]: 
  " Obj f T β Obj f' T; l  dom f; p β p'; lc (Obj f T); lc p 
   Call (Obj f T) l p β (the(f' l)⇗[(Obj f' T), p']⇖)"

(* These are rule formats for inversions rules *)

inductive_cases par_beta_cases [elim!]:
  "Fvar x β t"
  "Obj f T β t"
  "Call f l p β t"
  "Upd f l t β u"

abbreviation
  par_beta_ascii :: "[sterm, sterm] => bool"  (infixl "=>" 50) where
  "t => u == par_beta t u"

lemma Obj_par_red[consumes 1, case_names obj]: 
  " Obj f T β z; 
     lz.  dom lz = dom f; z = Obj lz T  Q   Q"
  by (rule par_beta_cases(2), assumption, auto)

lemma Upd_par_red[consumes 1, case_names upd obj]: 
  fixes t l u z
  assumes 
  "Upd t l u β z" and
  "t' u' L.  t β t'; finite L;
                s p. s  L  p  L  s  p 
                  (t''. (u⇗[Fvar s, Fvar p]⇖) β t'' 
                           u' = σ[s,p]t'');
                z = Upd t' l u'   Q" and
  "f f' T u' L.  l  dom f; Obj f T = t; Obj f T β Obj f' T;
                    finite L;
                    s p. s  L  p  L  s  p 
                      (t''. (u⇗[Fvar s, Fvar p]⇖) β t'' 
                               u' = σ[s,p]t'');
                z = Obj (f'(l  u')) T   Q"
  shows Q
  using assms
proof (cases rule: par_beta.cases)
  case pbeta_Upd thus ?thesis using assms(2) by force
next
  case pbeta_Upd'
  from this(1-2) this(5-6) assms(3)[OF _ _ this(3-4)]
  show ?thesis by force
qed

lemma Call_par_red[consumes 1, case_names call beta]: 
  fixes s l u z
  assumes 
  "Call s l u β z" and
  "t u'.  s β t; u β u'; z = Call t l u' 
   Q"
  "f f' T u'.  Obj f T = s; Obj f T β Obj f' T;
                  l  dom f'; u β u';
                  z = (the (f' l)⇗[Obj f' T, u']⇖)   Q"
  shows Q
  using assms
proof (cases rule: par_beta.cases)
  case pbeta_Call thus ?thesis using assms(2) by force
next
  case pbeta_beta
  from this(1-5) assms(3)[OF _ this(3)]
  show ?thesis by force
qed

lemma pbeta_induct[consumes 1, case_names Fvar Call Upd Upd' Obj beta Bnd]:
  fixes 
  t :: sterm and t' :: sterm and 
  P1 :: "sterm  sterm  bool" and P2 :: "sterm  sterm  bool"
  assumes
  "t β t'" and
  "x. P1 (Fvar x) (Fvar x)" and
  "t t' l u u'.  t β t'; P1 t t'; lc t; u β u'; P1 u u'; lc u  
       P1 (Call t l u) (Call t' l u')" and
  "t t' l u u'.  t β t'; P1 t t'; lc t; P2 u u'; body u 
       P1 (Upd t l u) (Upd t' l u')" and
  "f f' T t t' l.  Obj f T β Obj f' T; P1 (Obj f T) (Obj f' T);
                      P2 t t'; l  dom f; lc (Obj f T); body t 
       P1 (Upd (Obj f T) l t) (Obj (f'(l  t')) T)" and
  "f f' T.  dom f' = dom f; ldom f. body (the(f l)); 
               ldom f. P2 (the(f l)) (the(f' l)) 
       P1 (Obj f T) (Obj f' T)" and
  "f f' T l p p'.  Obj f T β Obj f' T; P1 (Obj f T) (Obj f' T); lc (Obj f T);
                      l  dom f; p β p'; P1 p p'; lc p 
       P1 (Call (Obj f T) l p) (the(f' l)⇗[Obj f' T, p']⇖)" and
  "L t t'. 
       finite L; 
        s p. s  L  p  L  s  p 
         (t''. t⇗[Fvar s,Fvar p]⇖ β t'' 
                  P1 (t⇗[Fvar s,Fvar p]⇖) t''  t' = σ[s,p] t'') 
       P2 t t'"
  shows "P1 t t'"
  by (induct rule: par_beta.induct[OF assms(1)], auto simp: assms)

subsection ‹Preservation›
lemma par_beta_lc[simp]:
  fixes t t'
  assumes "t β t'"
  shows "lc t  lc t'"
using assms
proof 
  (induct
    taking: "λt t'. body t'"
    rule: pbeta_induct)
  case Fvar thus ?case by simp
next
  case Call thus ?case by simp
next
  case Upd thus ?case by (simp add: lc_upd)
next
  case Upd' thus ?case by (simp add: lc_upd lc_obj)
next
  case Obj thus ?case by (simp add: lc_obj)
next
  case (beta f f' T l p p') thus ?case 
    by (clarify, simp add: lc_obj body_lc[of "the(f' l)" "Obj f' T" p'])
next
  case (Bnd L t t') note cof = this(2)
  from exFresh_s_p_cof[OF finite L]
  obtain s p where sp: "s  L  p  L  s  p" by auto
  with cof obtain t'' where "lc t''" and "t' = σ[s,p] t''" by blast
  with lc_body[of t'' s p] sp show "body t'" by force
qed

lemma par_beta_preserves_FV[simp, rule_format]: 
  fixes t t' x
  assumes "t β t'"
  shows "x  FV t  x  FV t'"
using assms
proof 
  (induct
    taking: "λt t'. x  FV t  x  FV t'"
    rule: pbeta_induct)
  case Fvar thus ?case by simp
next
  case Call thus ?case by simp
next
  case Upd thus ?case by simp
next
  case Upd' thus ?case by simp
next
  case Obj thus ?case by (simp add: FV_option_lem)
next
  case (beta f f' T l p p') thus ?case
  proof (intro strip)
    assume "x  FV (Call (Obj f T) l p)"
    with
      x  FV (Obj f T)  x  FV (Obj f' T)
      x  FV p  x  FV p'
    have obj': "x  FV (Obj f' T)" and p': "x  FV p'"
      by auto
    from l  dom f Obj f T β Obj f' T have "l  dom f'"
      by auto
    with 
      obj' p' FV_option_lem[of f']
      contra_subsetD[OF sopen_FV[of 0 "Obj f' T" p' "the(f' l)"]]
    show "x  FV (the (f' l)⇗[Obj f' T,p']⇖)" by (auto simp: openz_def)
  qed
next
  case (Bnd L t t') note cof = this(2)
  from finite L exFresh_s_p_cof[of "L  {x}"]
  obtain s p where 
    "s  L"and "p  L" and "s  p" and 
    "x  FV (Fvar s)" and "x  FV (Fvar p)"
    by auto
  with cof obtain t'' where
    tt'': "x  FV (t⇗[Fvar s, Fvar p]⇖)  x  FV t''" and
    "t' = σ[s,p] t''"
    by auto
  show ?case
  proof (intro strip)
    assume "x  FV t"
    with 
      tt'' x  FV (Fvar s) x  FV (Fvar p)
      contra_subsetD[OF sopen_FV[of 0 "Fvar s" "Fvar p" t]]
      sclose_subset_FV[of 0 s p t''] t' = σ[s,p] t''
    show "x  FV t'" by (auto simp: openz_def closez_def)
  qed
qed

lemma par_beta_body[simp]:
  " finite L; 
     s p. s  L  p  L  s  p 
       (t''. t⇗[Fvar s,Fvar p]⇖ β t''  t' = σ[s,p] t'') 
   body t  body t'"
proof (intro conjI)
  fix L :: "fVariable set" and t :: sterm and t' :: sterm
  assume "finite L" hence "finite (L  FV t)" by simp
  from exFresh_s_p_cof[OF this] 
  obtain s p where sp: "s  L  FV t  p  L  FV t  s  p" by auto
  hence "s  FV t" and "p  FV t" and "s  p" by auto

  assume 
    "s p. s  L  p  L  s  p
       (t''. t⇗[Fvar s,Fvar p]⇖ => t''  t' = σ[s,p] t'')"
  with sp obtain t'' where "t⇗[Fvar s,Fvar p]⇖ β t''" and "t' = σ[s,p] t''"
    by blast

  from par_beta_lc[OF this(1)] have "lc (t⇗[Fvar s,Fvar p]⇖)" and "lc t''" 
    by auto

  from 
    lc_body[OF this(1) s  p] 
    sclose_sopen_eq_t[OF s  FV t p  FV t s  p] 
  show "body t"
    by (simp add: closez_def openz_def)

  from lc_body[OF lc t'' s  p] t' = σ[s,p] t'' show "body t'" by simp
qed

subsection ‹Miscellaneous properties of par\_beta›
lemma Fvar_pbeta [simp]: "(Fvar x β t) = (t = Fvar x)" by auto
lemma Obj_pbeta: "Obj f T β Obj f' T
   dom f' = dom f 
       (L. finite L 
            (ldom f. s p. s  L  p  L  s  p
                (t. (the(f l)⇗[Fvar s, Fvar p]⇖) β t 
                       the(f' l) = σ[s,p]t)))
       (ldom f. body (the(f l)))"
  by (rule par_beta_cases(2), assumption, auto)

lemma Obj_pbeta_subst: 
  " finite L; 
     s p. s  L  p  L  s  p 
       (t''. (t⇗[Fvar s, Fvar p]⇖) β t''  t' = σ[s,p] t''); 
     Obj f T β Obj f' T; lc (Obj f T); body t 
   Obj (f(l  t)) T β Obj (f'(l  t')) T"
proof -
  fix L f f' T l t t' 
  assume "Obj f T β Obj f' T" from Obj_pbeta[OF this]
  have 
    dom: "dom (f'(l  t')) = dom (f(l  t))" and 
    exL: "L. finite L 
             (ldom f. s p. s  L  p  L  s  p 
                            (t. the (f l)⇗[Fvar s,Fvar p]⇖ β t 
                                   the (f' l) = σ[s,p] t))" and
    bodyf: "ldom f. body (the (f l))"
    by auto

  assume "body t" with bodyf 
  have body: "l'dom (f(l  t)). body (the ((f(l  t)) l'))"
    by auto

  assume 
    "finite L" and
    "s p. s  L  p  L  s  p 
       (t''. t⇗[Fvar s,Fvar p]⇖ β t''  t' = σ[s,p] t'')"
  with exL
  obtain L' where 
    "finite (L'  L)" and
    "l'dom (f(l  t)). s p. s  L'  L  p  L'  L  s  p 
                             (t''. the ((f(l  t)) l')⇗[Fvar s,Fvar p]⇖ β t'' 
                                      the ((f'(l  t')) l') = σ[s,p] t'')"
    by auto
  from par_beta.pbeta_Obj[OF dom this body]
  show "Obj (f(l  t)) T β Obj (f'(l  t')) T"
    by assumption
qed

lemma Upd_pbeta: "Upd t l u β Upd t' l u'
   t β t' 
       (L. finite L 
            (s p. s  L  p  L  s  p 
                (t''. (u⇗[Fvar s, Fvar p]⇖) β t''  u' = σ[s,p]t'')))
       lc t  body u"
  by (rule par_beta_cases(4), assumption, auto)

lemma par_beta_refl: 
  fixes t
  assumes "lc t"
  shows "t β t"
  using assms
proof -
  define pred_cof
    where "pred_cof L t 
      (s p. s  L  p  L  s  p  (t'. (t⇗[Fvar s, Fvar p]⇖) β t'  t = σ[s,p] t'))"
    for L t
  from assms show ?thesis
  proof 
    (induct
      taking: "λt. body t  (L. finite L  pred_cof L t)"
      rule: lc_induct)
    case Fvar thus ?case by simp
  next
    case Call thus ?case by simp
  next
    case Upd thus ?case
      unfolding pred_cof_def
      by auto
  next
    case (Obj f T) note pred = this
    define pred_fl where "pred_fl s p b l  (t'. (the b⇗[Fvar s, Fvar p]⇖) β t'  the b = σ[s,p]t')"
      for s p b and l :: Label

    from fmap_ex_cof[of f pred_fl] pred
    obtain L where
      "finite L" and "ldom f. body (the(f l)) 
                               (s p. s  L  p  L  s  p  pred_fl s p (f l) l)"
      unfolding pred_cof_def pred_fl_def
      by auto
    thus "Obj f T β Obj f T"
      unfolding pred_fl_def
      by auto
  next
    case (Bnd L t) note pred = this(2)
    with finite L show ?case
    proof 
      (auto simp: body_def, unfold pred_cof_def,
        rule_tac x = "L  FV t" in exI, simp, clarify)
      fix s p assume 
        "s  L" and "p  L" and "s  p" and
        "s  FV t" and "p  FV t"
      from 
        this(1-3) pred 
        sclose_sopen_eq_t[OF this(4-5) this(3)]
      show "t'. t⇗[Fvar s,Fvar p]⇖ β t'  t = σ[s,p] t'"
        by (rule_tac x = "t⇗[Fvar s,Fvar p]⇖" in exI, simp add: openz_def closez_def)
    qed
  qed
qed

lemma par_beta_body_refl:
  fixes u
  assumes "body u"
  shows "L. finite L  (s p. s  L  p  L  s  p 
                           (t'. (u⇗[Fvar s, Fvar p]⇖) β t'  u = σ[s,p] t'))"
proof (rule_tac x = "FV u" in exI, simp, clarify)
  fix s p assume "s  FV u" and "p  FV u" and "s  p"
  from 
    par_beta_refl[OF body_lc[OF assms lc_Fvar[of s] lc_Fvar[of p]]]
    sclose_sopen_eq_t[OF this]
  show "t'. (u⇗[Fvar s, Fvar p]⇖) β t'  u = σ[s,p] t'"
    by (rule_tac x = "u⇗[Fvar s, Fvar p]⇖" in exI, simp add: openz_def closez_def)
qed

lemma par_beta_ssubst[rule_format]:
  fixes t t'
  assumes "t β t'"
  shows "x v v'. v β v'  [x  v] t β [x  v'] t'"
proof -
  define pred_cof
    where "pred_cof L t t' 
      (s p. s  L  p  L  s  p  (t''. t⇗[Fvar s, Fvar p]⇖ β t''  t' = σ[s,p] t''))"
    for L t t'
  {
    fix x v v' t t'
    assume 
      "v β v'" and
      "x v v'. v β v'  (L. finite L  pred_cof L ([x  v] t) ([x  v'] t'))"
    hence
      "L. finite L  pred_cof L ([x  v] t) ([x  v'] t')"
        by auto
  }note Lex = this

  {
    fix x v l and f :: "Label  sterm option"
    assume "l  dom f" hence "l  dom (λl. ssubst_option x v (f l))"
      by simp
  }note domssubst = this
  {
    fix x v l T and f :: "Label  sterm option"
    assume "lc (Obj f T)" and "lc v" from ssubst_preserves_lc[OF this] 
    have obj: "lc (Obj (λl. ssubst_option x v (f l)) T)" by simp
  }note lcobj = this

  from assms show ?thesis
  proof 
    (induct
      taking: "λt t'. x v v'. v β v'
                        (L. finite L 
                               pred_cof L ([x  v] t) ([x  v'] t'))"
      rule: pbeta_induct)
    case Fvar thus ?case by simp
  next
    case Call thus ?case by simp
  next
    case (Upd t t' l u u') note pred_t = this(2) and pred_u = this(4)
    show ?case
    proof (intro strip)
      fix x v v' assume "v β v'"
      from Lex[OF this pred_u]
      obtain L where
        "finite L" and "pred_cof L ([x  v] u) ([x  v'] u')"
        by auto
      with
        ssubst_preserves_lc[of t v x]
        ssubst_preserves_body[of u v x]
        lc t par_beta_lc[OF v β v'] body u
        v β v' pred_t
      show "[x  v] Upd t l u β [x  v'] Upd t' l u'"
        unfolding pred_cof_def
        by auto
    qed
  next
    case (Upd' f f' T t t' l) 
    note pred_obj = this(2) and pred_t = this(3)
    show ?case
    proof (intro strip)
      from Obj f T β Obj f' T l  dom f have "l  dom f'" by auto
      fix x v v' assume "v β v'"
      with
        domssubst[OF l  dom f]
        ssubst_preserves_lc[of "Obj f T" v x]
        ssubst_preserves_body[of t v x]
        lc (Obj f T) par_beta_lc[OF v β v'] body t
        pred_obj
      have 
        "[x  v] Obj f T β [x  v'] Obj f' T" and
        "lc ([x  v] Obj f T)" and "body ([x  v] t)"
        by auto
      note lem = 
        pbeta_Upd'[OF this(1)[simplified] _ _ 
                      domssubst[OF l  dom f] 
                      this(2)[simplified] this(3)]

      from Lex[OF v β v' pred_t]
      obtain L where
        "finite L" and "pred_cof L ([x  v] t) ([x  v'] t')"
        by auto
      with lem[of L "[x  v'] t'"] ssubstoption_insert[OF l  dom f']
      show "[x  v] Upd (Obj f T) l t β [x  v'] Obj (f'(l  t')) T"
        unfolding pred_cof_def
        by auto
    qed
  next
    case (beta f f' T l p p') 
    note pred_obj = this(2) and pred_p = this(6)
    show ?case
    proof (intro strip)
      fix x v v' assume "v β v'"
      from 
        par_beta_lc[OF this]
        ssubst_preserves_lc[OF lc p]
      have "lc v" and "lc v'" and "lc ([x  v] p)" by auto
      note lem = 
        pbeta_beta[OF _ domssubst[OF l  dom f] _ 
                      lcobj[OF lc (Obj f T) this(1)] this(3)]
      from Obj f T β Obj f' T have "dom f = dom f'" by auto
      with l  dom f have "the (ssubst_option x v' (f' l)) = [x  v'] the (f' l)"
        by auto
      with
        lem[of x "λl. ssubst_option x v' (f' l)" "[x  v'] p'"]
        v β v' pred_obj pred_p
        ssubst_openz_distrib[OF lc v']
      show
        "[x  v] Call (Obj f T) l p β [x  v'] (the (f' l)⇗[Obj f' T, p']⇖)"
        by simp
    qed
  next
    case (Obj f f' T) note pred = fmap_ball_all3[OF this(1) this(3)]
    show ?case
    proof (intro strip)
      fix x v v'
      define pred_bnd
        where "pred_bnd s p b b' l 
          (t''. [x  v] the b⇗[Fvar s,Fvar p]⇖ β t''  [x  v'] the b' = σ[s,p] t'')"
        for s p b b' and l::Label
      assume "v β v'"
      with pred dom f' = dom f fmap_ex_cof2[of f' f pred_bnd] 
      obtain L where
        "finite L" and 
        predf: "ldom f. pred_cof L ([x  v] the (f l)) ([x  v'] the (f' l))"
        unfolding pred_cof_def pred_bnd_def 
        by auto

      have "ldom (λl. ssubst_option x v (f l)). body (the (ssubst_option x v (f l)))"
      proof (intro strip, simp)
        fix l' :: Label assume "l'  dom f"
        with ldom f. body (the(f l)) have "body (the (f l'))" by blast
        note ssubst_preserves_body[OF this]
        from 
          this[of v x] par_beta_lc[OF v β v']
          l'  dom f ssubst_option_lem[of f x v]
        show "body (the (ssubst_option x v (f l')))" by auto
      qed
      note intro = pbeta_Obj[OF _ finite L _ this]
      from
        predf
        ssubst_option_lem[of f x v]
        ssubst_option_lem[of f' x v'] dom f' = dom f
        dom_ssubstoption_lem[of x v f]
        dom_ssubstoption_lem[of x v' f']
      show "[x  v] Obj f T β [x  v'] Obj f' T"
        unfolding pred_cof_def
        by (simp, intro intro[of "(λl. ssubst_option x v' (f' l))" T], auto)
    qed
  next
    case (Bnd L t t') note pred = this(2)
    show ?case
    proof (intro strip)
      fix x v v' assume "v β v'"
      from finite L
      show "L. finite L  pred_cof L ([x  v] t) ([x  v'] t')"
      proof (rule_tac x = "L  {x}  FV v'" in exI, 
          unfold pred_cof_def, auto)
        fix s p assume "s  L" and "p  L" and "s  p"
        with pred 
        obtain t'' where
          "t⇗[Fvar s,Fvar p]⇖ β t''" and
          "x v v'. v β v'  [x  v] (t⇗[Fvar s,Fvar p]⇖) β [x  v'] t''" and
          "t' = σ[s,p] t''"
          by blast
        from this(2) v β v' 
        have ssubst_pbeta: "[x  v] (t⇗[Fvar s,Fvar p]⇖) β [x  v'] t''" by blast
        
        assume "s  x" and "p  x"
        hence "x  FV (Fvar s)" and "x  FV (Fvar p)" by auto
        from 
          ssubst_pbeta
          par_beta_lc[OF v β v'] ssubst_sopen_commute[OF _ this]
        have "[x  v] t⇗[Fvar s,Fvar p]⇖ β [x  v'] t''" by (simp add: openz_def)
        moreover
        assume "s  FV v'" and "p  FV v'"
        from 
          ssubst_sclose_commute[OF this not_sym[OF s  x] 
                                        not_sym[OF p  x]] 
          t' = σ[s,p] t''
        have "[x  v'] t' = σ[s,p] [x  v'] t''" by (simp add: closez_def)
        ultimately
        show "t''. [x  v] t⇗[Fvar s,Fvar p]⇖ β t''  [x  v'] t' = σ[s,p] t''" 
          by (rule_tac x = "[x  v'] t''" in exI, simp)
      qed
    qed
  qed
qed

lemma renaming_par_beta: "t β t'  [s  Fvar sa] t β [s  Fvar sa] t'"
  by (erule par_beta_ssubst, simp+)

lemma par_beta_beta:
  fixes l f f' u u'
  assumes 
  "l  dom f" and "Obj f T β Obj f' T" and "u β u'" and "lc (Obj f T)" and "lc u"
  shows "(the(f l)⇗[Obj f T, u]⇖) β (the(f' l)⇗[Obj f' T, u']⇖)"
proof -
  from Obj_pbeta[OF Obj f T β Obj f' T] 
  obtain L where 
    "dom f = dom f'" and
    "finite L" and
    pred_sp: "ldom f.s p. s  L  p  L  s  p
                          (t''. the (f l)⇗[Fvar s,Fvar p]⇖ β t'' 
                                   the (f' l) = σ[s,p] t'')" and
    "ldom f. body (the (f l))"
    by auto

  from this(2) finite_FV[of "Obj f T"] have fin: "finite (L  FV (Obj f T)  FV u)" by simp
  from exFresh_s_p_cof[OF this]
  obtain s p where 
    sp: "s  L  FV (Obj f T)  FV u  p  L  FV (Obj f T)  FV u  s  p"
    by auto
  with l  dom f obtain t'' where 
    "the (f l)⇗[Fvar s, Fvar p]⇖ β t''" and "the (f' l) = σ[s,p] t''"
    using pred_sp by blast
  from par_beta_lc[OF this(1)] have "lc t''" by simp
  from 
    sopen_sclose_eq_t[OF this] 
    the (f l)⇗[Fvar s, Fvar p]⇖ β t'' the(f' l) = σ[s,p] t''
  have "the (f l)⇗[Fvar s, Fvar p]⇖ β (the (f' l)⇗[Fvar s, Fvar p]⇖)" 
    by (simp add: openz_def closez_def)
  from par_beta_ssubst[OF this] u β u'
  have "[p  u] (the (f l)⇗[Fvar s, Fvar p]⇖) β [p  u'] (the (f' l)⇗[Fvar s, Fvar p]⇖)"
    by simp
  note par_beta_ssubst[OF this Obj f T β Obj f' T]
  moreover
  from l  dom f sp
  have "s  FV (the(f l))" and "p  FV (the(f l))" and "s  p" and "s  FV u"
    by force+
  note ssubst_intro[OF this]
  moreover
  from l  dom f dom f = dom f' have "l  dom f'" by force
  with 
    par_beta_preserves_FV[OF Obj f T β Obj f' T]
    par_beta_preserves_FV[OF u β u'] sp FV_option_lem[of f']
  have "s  FV (the (f' l))" and "p  FV (the (f' l))" and "s  p" and "s  FV u'"
    by auto
  note ssubst_intro[OF this]
  ultimately
  show "the (f l)⇗[Obj f T, u]⇖ β (the (f' l)⇗[Obj f' T, u']⇖)" 
    by (simp add: openz_def closez_def)
qed

subsection ‹Inclusions›
text beta ⊆ par_beta ⊆ beta^*› \medskip›
lemma beta_subset_par_beta: "beta  par_beta"
proof (clarify)
  define pred_cof
    where "pred_cof L t t' 
      (s p. s  L  p  L  s  p  (t''. (t⇗[Fvar s, Fvar p]⇖) β t''  t' = σ[s,p] t''))"
    for L t t'

  fix t t' assume "t β t'" thus "t β t'"
  proof 
    (induct
      taking: "λt t'. body t  body t'  (L. finite L  pred_cof L t t')"
      rule: beta_induct)
    case CallL thus ?case by (simp add: par_beta_refl)
  next
    case CallR thus ?case by (simp add: par_beta_refl)
  next
    case beta thus ?case by (simp add: par_beta_refl)
  next
    case UpdL
    from 
      par_beta_lc[OF this(2)] this(2) 
      par_beta_body_refl[OF this(3)] this(3)
    show ?case by auto
  next
    case (UpdR t t' u l)
    from this(1) obtain L where
      "finite L" and "pred_cof L t t'" and "body t"
      by auto
    from 
      this(2) pbeta_Upd[OF par_beta_refl[OF lc u] lc u this(1) _ this(3)]
    show ?case
      unfolding pred_cof_def
      by auto
  next
    case (Upd l f T t)
    from par_beta_body_refl[OF body t]
    obtain L where
      "finite L" and 
      "s p. s  L  p  L  s  p 
         (t'. t⇗[Fvar s, Fvar p]⇖ β t'  t = σ[s,p] t')"
      by auto
    from 
      pbeta_Upd'[OF par_beta_refl[OF lc (Obj f T)] this
                    l  dom f lc (Obj f T) body t]
    show ?case by assumption
  next
    case (Obj l f t t' T) note cof = this(2) and body = this(3)
    from cof obtain L where 
      "body t" and "finite L" and "pred_cof L t t'"
      by auto
    from body have "lc (Obj f T)" by (simp add: lc_obj)
    from 
      Obj_pbeta_subst[OF finite L _ par_beta_refl[OF this] this body t]
      pred_cof L t t'
    show ?case
      unfolding pred_cof_def
      by auto
  next
    case (Bnd L t t') note pred = this(2)
    from finite L exFresh_s_p_cof[of "L  FV t"]
    obtain s p where 
      "s  L" and "p  L" and "s  p" and
      "s  FV t" and "p  FV t"
      by auto
    with pred obtain t'' where 
      "t⇗[Fvar s, Fvar p]⇖ β t''" and "t' = σ[s,p] t''"
      by blast
    from 
      par_beta_lc[OF this(1)] this(2) lc_body[OF _ s  p]
    have "body σ[s,p](t⇗[Fvar s, Fvar p]⇖)" and "body t'" by auto
    from this(1) sclose_sopen_eq_t[OF s  FV t p  FV t s  p]
    have "body t" by (simp add: openz_def closez_def)
    with body t' finite L pred show ?case
      unfolding pred_cof_def
      by (simp, rule_tac x = L in exI, auto)
  qed
qed

lemma par_beta_subset_beta: "par_beta  beta^**"
proof (rule predicate2I)
  define pred_cof
    where "pred_cof L t t' 
      (s p. s  L  p  L  s  p  (t''. (t⇗[Fvar s, Fvar p]⇖) β* t''  t' = σ[s,p] t''))"
    for L t t'

  fix x y assume "x β y" thus "x β* y"
  proof (induct 
      taking: "λt t'. body t'  (L. finite L  pred_cof L t t')"
      rule: pbeta_induct)
    case Fvar thus ?case by simp
  next
    case Call thus ?case by auto
  next
    case (Upd t t' l u u')
    from this(4) obtain L where
      "finite L" and "pred_cof L u u'" by auto
    from 
      this(2) 
      rtrancl_beta_Upd[OF t β* t' this(1) _ lc t body u]
    show ?case
      unfolding pred_cof_def
      by simp
  next
    case (Upd' f f' T t t' l)
    from this(3) obtain L where
      "body t'" and "finite L" and "pred_cof L t t'" by auto
    from 
      this(3)
      rtrancl_beta_Upd[OF Obj f T β* Obj f' T finite L _
                          lc (Obj f T) body t]
    have rtranclp: "Upd (Obj f T) l t β* Upd (Obj f' T) l t'"
      unfolding pred_cof_def
      by simp

    from 
      Obj_pbeta[OF Obj f T β Obj f' T] l  dom f 
      par_beta_lc[OF Obj f T β Obj f' T]
    have "l  dom f'" and "lc (Obj f' T)" by auto
    from beta_Upd[OF this body t'] rtranclp
    show ?case by simp
  next
    case (Obj f f' T) note body = this(2) and pred = this(3)
    define pred_bnd
      where "pred_bnd s p b b' l  (t''. the b⇗[Fvar s,Fvar p]⇖ β* t''  the b' = σ[s,p] t'')"
      for s p b b' and l::Label
    from 
      pred dom f' = dom f fmap_ex_cof2[of f' f pred_bnd]
    obtain L where
      "finite L" and 
      "ldom f. s p. s  L  p  L  s  p  pred_bnd s p (f l) (f' l) l"
      unfolding pred_cof_def pred_bnd_def
      by auto
    from 
      this(2)
      rtrancl_beta_obj_n[OF finite L _ sym[OF dom f' = dom f] body]
    show ?case
      unfolding pred_bnd_def
      by simp
  next
    case (beta f f' T l p p')
    note 
      rtrancl_beta_Call[OF Obj f T β* Obj f' T lc (Obj f T) 
                           p β* p' lc p]
    moreover
    from 
      Obj_pbeta[OF Obj f T β Obj f' T] l  dom f 
      par_beta_lc[OF Obj f T β Obj f' T]
      par_beta_lc[OF p β p']
    have "l  dom f'" and "lc (Obj f' T)" and "lc p'" by auto
    note beta.beta[OF this]
    ultimately
    show ?case 
      by (auto simp: rtranclp.rtrancl_into_rtrancl[of _ _ "Call (Obj f' T) l p'"])
  next
    case (Bnd L t t') note pred = this(2)
    hence "pred_cof L t t'"
      unfolding pred_cof_def
      by blast
    moreover
    from pred finite L par_beta_body[of L t t']
    have "body t'" by blast
    ultimately
    show ?case
      using finite L
      by auto
  qed
qed

subsection ‹Confluence (directly)›

(***Main result: Confluence of beta relation for Sigma calculus              ***)
(*** by diamond property of parallel reduction and beta <= par_beta <= beta^* ***)
lemma diamond_binder:
  fixes L1 L2 t ta tb
  assumes 
  "finite L1"  and
  pred_L1: "s p. s  L1  p  L1  s  p
               (t'. (t⇗[Fvar s, Fvar p]⇖ β t' 
                      (z. (t⇗[Fvar s, Fvar  p]⇖ β z)  (u. t' β u  z β u))) 
                      ta = σ[s,p]t')" and
  "finite L2" and
  pred_L2: "s p. s  L2  p  L2  s  p 
               (t'. t⇗[Fvar s, Fvar p]⇖ β t'  tb = σ[s,p]t')"
  shows
  "L'. finite L' 
       (t''. (s p. s  L'  p  L'  s  p 
                   (u. ta⇗[Fvar s, Fvar p]⇖ β u  t'' = σ[s,p]u))
              (s p. s  L'  p  L'  s  p 
                   (u. tb⇗[Fvar s, Fvar p]⇖ β u  t'' = σ[s,p]u)))"
proof -
  from finite L1 finite L2 have "finite (L1  L2)" by simp
  from exFresh_s_p_cof[OF this]
  obtain s p where sp: "s  L1  L2  p  L1  L2  s  p" by auto
  with pred_L1
  obtain t' where 
    "t⇗[Fvar s,Fvar p]⇖ β t'" and 
    "z. t⇗[Fvar s,Fvar p]⇖ β z  (u. t' β u  z β u)" and
    "ta = σ[s,p] t'"
    by blast

  from sp pred_L2 obtain t'' where "t⇗[Fvar s,Fvar p]⇖ β t''" and "tb = σ[s,p] t''" 
    by blast
  from z. t⇗[Fvar s,Fvar p]⇖ β z  (u. t' β u  z β u) this(1) 
  obtain u where "t' β u" and "t'' β u" by blast

  from finite L1 finite L2 have "finite (L1  L2  FV t  {s}  {p})" by simp
  moreover
  {
    fix x :: sterm and y :: sterm
    assume "t⇗[Fvar s, Fvar p]⇖ β y" and "x = σ[s,p] y" and "y β u"
    hence 
      "sa pa. sa  L1  L2  FV t  {s}  {p} 
              pa  L1  L2  FV t  {s}  {p}  sa  pa 
         (t. x⇗[Fvar sa,Fvar pa]⇖ β t   σ[s,p] u = σ[sa,pa] t)"
    proof (intro strip)
      fix sa :: fVariable and pa :: fVariable
      assume 
        sapa: "sa  L1  L2  FV t  {s}  {p} 
                pa  L1  L2  FV t  {s}  {p}  sa  pa"
      with sp par_beta_lc[OF y β u]
      have "s  p" and "s  FV (Fvar pa)" and "lc y" and "lc u" by auto
      from 
        sopen_sclose_eq_ssubst[OF this(1-3)] 
        sopen_sclose_eq_ssubst[OF this(1-2) this(4)]
        renaming_par_beta x = σ[s,p] y y β u
      have "x⇗[Fvar sa, Fvar pa]⇖ β (σ[s,p] u⇗[Fvar sa, Fvar pa]⇖)"
        by (auto simp: openz_def closez_def)
      
      moreover
      from 
        sapa par_beta_preserves_FV[OF t ⇗[Fvar s,Fvar p]⇖ β y]
        sopen_FV[of 0 "Fvar s" "Fvar p" t]
        par_beta_preserves_FV[OF y β u]
        sclose_subset_FV[of 0 s p u]
      have "sa  FV (σ[s,p] u)" and "pa  FV (σ[s,p] u)" and "sa  pa"
        by (auto simp: openz_def closez_def)
      from sym[OF sclose_sopen_eq_t[OF this]] 
      have "σ[s,p] u = σ[sa,pa] (σ[s,p] u⇗[Fvar sa, Fvar pa]⇖)"
        by (simp add: openz_def closez_def)

      ultimately show "t. x⇗[Fvar sa,Fvar pa]⇖ β t  σ[s,p] u = σ[sa,pa] t" 
        by blast
    qed
  }note 
      this[OF t ⇗[Fvar s,Fvar p]⇖ β t' ta = σ[s,p] t' t' β u]
      this[OF t ⇗[Fvar s,Fvar p]⇖ β t'' tb = σ[s,p] t'' t'' β u]
  ultimately
  show 
    "L'. finite L' 
         (t''. (s p. s  L'  p  L'  s  p 
                    (t'. ta⇗[Fvar s,Fvar p]⇖ β t'  t'' = σ[s,p] t'))
                (s p. s  L'  p  L'  s  p 
                    (t'. tb⇗[Fvar s,Fvar p]⇖ β t'  t'' = σ[s,p] t')))"
    by (rule_tac x = "L1  L2  FV t  {s}  {p}" in exI, simp, blast)
qed

lemma exL_exMap_lem:
  fixes 
  f :: "Label -~> sterm" and 
  lz :: "Label -~> sterm" and f' :: "Label -~> sterm"
  assumes "dom f = dom lz" and "dom f' = dom f"
  shows 
  "L1 L2. finite L1 
     (ldom f. s p. s  L1  p  L1  s  p 
                      (t. (the(f l)⇗[Fvar s, Fvar p]⇖ β t 
                             (z. (the(f l)⇗[Fvar s, Fvar  p]⇖ β z) 
                                 (u. t β u  z β u)))
                             the(f' l) = σ[s,p]t))
     finite L2
     (ldom f. s p. s  L2  p  L2  s  p 
           (t. the(f l)⇗[Fvar s, Fvar p]⇖ β t  the(lz l) = σ[s,p]t))
     (L'. finite L' 
             (lu. dom lu = dom f 
             (ldom f. s p. s  L'  p  L'  s  p 
                            (t. (the(f' l)⇗[Fvar s, Fvar p]⇖) β t 
                                   the(lu l) = σ[s,p]t))
             (ldom f. body (the (f' l)))
             (ldom f. s p. s  L'  p  L'  s  p 
                            (t. (the(lz l)⇗[Fvar s, Fvar p]⇖) β t 
                                   the(lu l) = σ[s,p]t))
             (ldom f. body (the (lz l)))))"
  using assms
proof (induct rule: fmap_induct3)
  case empty thus ?case by force
next 
  case (insert x a b c F1 F2 F3) thus ?case
  proof (intro strip)
    fix L1 :: "fVariable set" and L2 :: "fVariable set"
    {
      fix 
        L :: "fVariable set" and
        t :: sterm and F :: "Label -~> sterm" and
        P :: "sterm  sterm  fVariable  fVariable  bool"
      assume 
        "dom F1 = dom F" and
        *: "ldom (F1(x  a)). 
           s p. s  L  p  L  s  p
             P (the ((F1(x  a)) l)) (the ((F(x  t)) l)) s p"
      hence 
        F: "ldom F1. s p. s  L  p  L  s  p
              P (the(F1 l)) (the(F l)) s p"
      proof (intro strip)
        fix l :: Label and s :: fVariable and p :: fVariable
        assume "l  dom F1" hence "l  dom (F1(x  a))" by simp
        moreover assume "s  L  p  L  s  p"
        ultimately
        have "P (the((F1(x  a)) l)) (the((F(x  t)) l)) s p"
          using * by blast
        moreover from x  dom F1 l  dom F1 have "l  x" by auto
        ultimately show "P (the(F1 l)) (the(F l)) s p" by force
      qed

      from * have "s p. s  L  p  L  s  p  P a t s p" by auto
      note this F
    }
    note pred = this
    note 
      tmp =
      pred[of _  L1 "(λt t' s p. 
                        t''. (t⇗[Fvar s,Fvar p]⇖ β t''
                             (z. t⇗[Fvar s,Fvar p]⇖ β z  (u. t'' β u  z β u)))
                             t' = σ[s,p] t'')"]
    note predc = tmp(1) note predF3 = tmp(2)
    note tmp = pred[of _ L2 
                       "(λt t' s p. t''. t⇗[Fvar s,Fvar p]⇖ β t''  t' = σ[s,p] t'')"]
    note predb = tmp(1) note predF2 = tmp(2)

    assume 
      a: "ldom (F1(x  a)). s p. s  L1  p  L1  s  p 
         (t. (the ((F1(x  a)) l)⇗[Fvar s,Fvar p]⇖ β t 
                (z. the ((F1(x  a)) l)⇗[Fvar s,Fvar p]⇖ β z 
                    (u. t β u  z β u))) 
                the ((F3(x  c)) l) = σ[s,p] t)" and
      b: "ldom (F1(x  a)). s p. s  L2  p  L2  s  p 
         (t. the ((F1(x  a)) l)⇗[Fvar s,Fvar p]⇖ β t 
                the ((F2(x  b)) l) = σ[s,p] t)" and
      "finite L1" and "finite L2"
    from 
      diamond_binder[OF this(3) predc[OF sym[OF dom F3 = dom F1] this(1)]
                        this(4) predb[OF dom F1 = dom F2 this(2)]]
    obtain La t where 
      "finite La" and
      pred_c: "s p. s  La  p  La  s  p 
                 (u. c⇗[Fvar s,Fvar p]⇖ β u  t = σ[s,p] u)" and
      pred_b: "s p. s  La  p  La  s  p 
                 (u. b⇗[Fvar s,Fvar p]⇖ β u  t = σ[s,p] u)"
      by blast
    {
      from this(1) have "finite (La  FV c  FV b)" by simp
      from exFresh_s_p_cof[OF this]
      obtain s p where 
        sp: "s  La  FV c  FV b  p  La  FV c  FV b  s  p" 
        by auto
      with pred_c obtain u where "c⇗[Fvar s,Fvar p]⇖ β u" by blast
      from par_beta_lc[OF this] have "lc (c⇗[Fvar s,Fvar p]⇖)" by simp
      with lc_body[of "c⇗[Fvar s,Fvar p]⇖" s p] sp sclose_sopen_eq_t[of s c p 0]
      have c: "body c" by (auto simp: closez_def openz_def)
          
      from sp pred_b obtain u where "b⇗[Fvar s,Fvar p]⇖ β u" by blast      
      from par_beta_lc[OF this] have "lc (b⇗[Fvar s,Fvar p]⇖)" by simp
      with lc_body[of "b⇗[Fvar s,Fvar p]⇖" s p] sp sclose_sopen_eq_t[of s b p 0]
      have "body b" by (auto simp: closez_def openz_def)
      note c this
    }note bodycb = this
    from 
      predF3[OF sym[OF dom F3 = dom F1] a]
      predF2[OF dom F1 = dom F2 b]
      finite L1 finite L2
    have 
      "L'. finite L' 
           (lu. dom lu = dom F1 
           (ldom F1. s p. s  L'  p  L'  s  p 
                           (t. the (F3 l)⇗[Fvar s,Fvar p]⇖ β t 
                                  the (lu l) = σ[s,p] t)) 
           (ldom F1. body (the (F3 l))) 
           (ldom F1. s p. s  L'  p  L'  s  p 
                           (t. the (F2 l)⇗[Fvar s,Fvar p]⇖ β t 
                                  the (lu l) = σ[s,p] t)) 
           (ldom F1. body (the (F2 l))))"
      by (rule_tac x = L1 in allE[OF insert(1)], simp)
    then obtain Lb f where 
      "finite Lb" and "dom f = dom F1" and
      pred_F3: "ldom F1. s p. s  La  Lb  p  La  Lb  s  p 
                              (t. the (F3 l)⇗[Fvar s,Fvar p]⇖ β t 
                                     the (f l) = σ[s,p] t)" and
      body_F3: "ldom F1. body (the (F3 l))" and
      pred_F2: "ldom F1. s p. s  La  Lb  p  La  Lb  s  p 
                              (t. the (F2 l)⇗[Fvar s,Fvar p]⇖ β t 
                                     the (f l) = σ[s,p] t)" and
      body_F2: "ldom F1. body (the (F2 l))"
      by auto 
    from finite La finite Lb have "finite (La  Lb)" by simp
    moreover
    from dom f = dom F1 have "dom (f(x  t)) = dom (F1(x  a))" by simp
    moreover
    from pred_c pred_F3
    have 
      "ldom (F1(x  a)). s p. s  La  Lb  p  La  Lb  s  p 
                               (t'. the ((F3(x  c)) l)⇗[Fvar s,Fvar p]⇖ β t' 
                                       the ((f(x  t)) l) = σ[s,p] t')"
      by auto
    moreover
    from bodycb(1) body_F3 
    have "ldom (F1(x  a)). body (the ((F3(x  c)) l))"
      by simp
    moreover
    from pred_b pred_F2
    have 
      "ldom (F1(x  a)). s p. s  La  Lb  p  La  Lb  s  p 
                               (t'. the ((F2(x  b)) l)⇗[Fvar s,Fvar p]⇖ β t' 
                                       the ((f(x  t)) l) = σ[s,p] t')"
      by auto
    moreover
    from bodycb(2) body_F2 
    have "ldom (F1(x  a)). body (the ((F2(x  b)) l))"
      by simp
    ultimately
    show 
      "L'. finite L'
           (lu. dom lu = dom (F1(x  a)) 
                 (ldom (F1(x  a)). 
                    s p. s  L'  p  L'  s  p 
                      (t'. the ((F3(x  c)) l)⇗[Fvar s,Fvar p]⇖ β t'
                              the (lu l) = σ[s,p] t'))
                 (ldom (F1(x  a)). body (the ((F3(x  c)) l))) 
                 (ldom (F1(x  a)). 
                    s p. s  L'  p  L'  s  p 
                      (t'. the ((F2(x  b)) l)⇗[Fvar s,Fvar p]⇖ β t'
                 the (lu l) = σ[s,p] t'))
                 (ldom (F1(x  a)). body (the ((F2(x  b)) l))))"
      by (rule_tac x = "La  Lb" in exI, 
        simp (no_asm_simp) only: conjI simp_thms(22),
        rule_tac x = "(f(x  t))" in exI, simp)
  qed
qed

lemma exL_exMap:
  " dom (f::Label -~> sterm) = dom (lz::Label -~> sterm); 
     dom (f'::Label -~> sterm) = dom f; 
     finite L1;
     ldom f. s p. s  L1  p  L1  s  p 
       (t. (the(f l)⇗[Fvar s, Fvar p]⇖ β t 
              (z. (the(f l)⇗[Fvar s, Fvar  p]⇖ β z)  (u. t β u  z β u)))
              the(f' l) = σ[s,p]t);
     finite L2;
     ldom lz. s p. s  L2  p  L2  s  p 
       (t. the(f l)⇗[Fvar s, Fvar p]⇖ β t  the(lz l) = σ[s,p]t) 
   L'. finite L' 
          (lu. dom lu = dom f 
                (ldom f. s p. s  L'  p  L'  s  p 
                               (t. (the(f' l)⇗[Fvar s, Fvar p]⇖) β t 
                                      the(lu l) = σ[s,p]t))
                (ldom f. body (the (f' l)))
                (ldom f. s p. s  L'  p  L'  s  p 
                               (t. (the(lz l)⇗[Fvar s, Fvar p]⇖) β t 
                                      the(lu l) = σ[s,p]t))
                (ldom f. body (the (lz l))))"
  using exL_exMap_lem[of f lz f'] by simp

lemma diamond_par_beta: "diamond par_beta"
  unfolding diamond_def commute_def square_def
proof (rule impI [THEN allI [THEN allI]])
  fix x y assume "x β y" 
  thus "z. x β z  (u. y β u  z β u)"
  proof (induct rule: par_beta.induct)
    case pbeta_Fvar thus ?case by simp
  next
    case (pbeta_Upd t t' L u u' l) 
    note pred_t = this(2) and pred_u = this(5)
    show ?case
    proof (intro strip)
      fix z assume "Upd t l u β z"
      thus "u. Upd t' l u' β u  z β u"
      proof (induct rule: Upd_par_red)
          (* Upd: case Upd
             Upd t' l u' ⇒β Upd tb l ub ∧ Upd ta l ua ⇒β Upd tb l ub *)
        case (upd ta ua La)
        from 
          diamond_binder[OF finite L pred_u this(2-3)]
          this(1) pred_t
          par_beta_lc[OF this(1)] par_beta_lc[OF t β t']
        obtain L' ub tb where 
          "t' β tb" and "lc t'" and "ta β tb" and 
          "lc ta" and "finite L'" and
          "s p. s  L'  p  L'  s  p 
             (u. u'⇗[Fvar s,Fvar p]⇖ β u  ub = σ[s,p] u)" and
          "s p. s  L'  p  L'  s  p 
             (u. ua⇗[Fvar s,Fvar p]⇖ β u  ub = σ[s,p] u)"
          by auto
        from 
          par_beta.pbeta_Upd[OF this(1-2) this(5-6)]
          par_beta.pbeta_Upd[OF this(3-5) this(7)]
          par_beta_body[OF this(5-6)]
          par_beta_body[OF this(5) this(7)] z = Upd ta l ua
        show ?case by (force simp: exI[of _ "Upd tb l ub"])
      next
        case (obj f fa T ua La)
          (* Upd: case Obj
             Upd (Obj f' T) l u' ⇒β Obj (fb(l ↦ ub)) T 
           ∧ Obj (fa(l ↦ ua)) T ⇒β Obj (fb(l ↦ ub)) T *)
        from diamond_binder[OF finite L pred_u this(4-5)]
        obtain Lb ub where
          "finite Lb" and
          ub1: "s p. s  Lb  p  Lb  s  p 
                  (u. ua⇗[Fvar s,Fvar p]⇖ β u  ub = σ[s,p] u)" and
          ub2: "s p. s  Lb  p  Lb  s  p 
                  (u. u'⇗[Fvar s,Fvar p]⇖ β u  ub = σ[s,p] u)"
          by auto
        from Obj f T = t Obj f T β Obj fa T
        have "t β Obj fa T" by simp
        with pred_t obtain a where "t' β a" "Obj fa T β a"
          by auto
        with 
          par_beta_lc[OF this(2)] 
          par_beta_body[OF finite Lb ub1]
        obtain fb where
          "t' β Obj fb T" and "Obj fa T β Obj fb T" and
          "lc (Obj fa T)" and "body ua"
          by auto
        from Obj_pbeta_subst[OF finite Lb ub1 this(2-4)] 
        have "Obj (fa(l  ua)) T β Obj (fb(l  ub)) T" by assumption
        moreover
        from 
          t β t' Obj f T = t
          par_beta_lc[OF t β t'] t' β Obj fb T
          par_beta_body[OF finite Lb ub2]
        obtain f' where 
          "t' = Obj f' T" and "Obj f' T β Obj fb T" and 
          "lc (Obj f' T)" and "body u'"
          by auto
        note par_beta.pbeta_Upd'[OF this(2) finite Lb ub2 _ this(3-4)]
        moreover
        from 
          t β t' Obj f T = t t' = Obj f' T
          l  dom f Obj_pbeta[of f T f']
        have "l  dom f'" by simp
        ultimately
        show ?case
          using z = Obj (fa(l  ua)) T t' = Obj f' T
          by (rule_tac x = "Obj (fb(l  ub)) T" in exI, simp)
      qed
    qed
  next
    case (pbeta_Obj f' f L T) note pred = this(3)
    show ?case
    proof (clarify)
        (* Obj f' T ⇒β Obj fb T ∧ Obj fa T ⇒β Obj fb T *)
      fix fa La
      assume 
        "dom fa = dom f" and "finite La" and
        "ldom f. s p. s  La  p  La  s  p
                      (t. the (f l)⇗[Fvar s,Fvar p]⇖ β t 
                             the (fa l) = σ[s,p] t)"
      from 
        exL_exMap[OF sym[OF this(1)] dom f' = dom f 
                     finite L pred this(2)]
        this(1) this(3) dom f' = dom f
      obtain Lb fb where 
        "dom fb = dom f'" and "dom fb = dom fa" and "finite Lb" and
        "ldom f'. s p. s  Lb  p  Lb  s  p 
                       (t. the (f' l)⇗[Fvar s,Fvar p]⇖ β t 
                              the (fb l) = σ[s,p] t)" and
        "ldom f'. body (the (f' l))" and
        "ldom fa. s p. s  Lb  p  Lb  s  p 
                       (t. the (fa l)⇗[Fvar s,Fvar p]⇖ β t 
                              the (fb l) = σ[s,p] t)" and
        "ldom fa. body (the (fa l))"
        by auto
      from 
        par_beta.pbeta_Obj[OF this(1) this(3-5)]
        par_beta.pbeta_Obj[OF this(2) this(3) this(6-7)]
      show "u. Obj f' T β u  Obj fa T β u"
        by (rule_tac x = "Obj fb T" in exI, simp)
    qed
  next
    case (pbeta_Upd' f T f' L t t' l) 
    note pred_obj = this(2) and pred_bnd = this(4)
    show ?case
    proof (clarify)
      fix z assume "Upd (Obj f T) l t β z"
      thus "u. Obj (f'(l  t')) T β u  z β u"
      proof (induct rule: Upd_par_red)
          (* Upd': case Upd 
             Obj (f'(l ↦ t')) T ⇒β Obj (fb(l ↦ tb)) T 
           ∧ Upd (Obj fa T) l ta ⇒β Obj (fb(l ↦ tb)) T *)
        case (upd a ta La) note pred_ta = this(3)
        from Obj f T β a z = Upd a l ta
        obtain fa where 
          "Obj f T β Obj fa T" and "z = Upd (Obj fa T) l ta"
          by auto
        from this(1) pred_obj
        obtain b where "Obj f' T β b" and "Obj fa T β b"
          by (elim allE impE exE conjE, simp)
        with 
          par_beta_lc[OF this(1)] par_beta_lc[OF this(2)]
        obtain fb where 
          "Obj f' T β Obj fb T" and "lc (Obj f' T)" and
          "Obj fa T β Obj fb T" and "lc (Obj fa T)"
          by auto
        from diamond_binder[OF finite L pbeta_Upd'(4) finite La pred_ta]
        obtain Lb tb where 
          "finite Lb" and
          cb1: "s p. s  Lb  p  Lb  s  p 
                  (u. t'⇗[Fvar s,Fvar p]⇖ β u  tb = σ[s,p] u)" and
          cb2: "s p. s  Lb  p  Lb  s  p 
                  (u. ta⇗[Fvar s,Fvar p]⇖ β u  tb = σ[s,p] u)"
          by auto
        from 
          par_beta_body[OF this(1-2)] 
          Obj_pbeta_subst[OF finite Lb cb1 Obj f' T β Obj fb T
                             lc (Obj f' T)]
        have "Obj (f'(l  t')) T β Obj (fb(l  tb)) T" 
          by simp
        moreover
        from Obj_pbeta[OF Obj f T β Obj fa T] l  dom f
        have "l  dom fa" by simp
        from 
          par_beta_body[OF finite Lb cb2]
          par_beta.pbeta_Upd'[OF Obj fa T β Obj fb T finite Lb 
                                 cb2 this lc (Obj fa T)]
        have "Upd (Obj fa T) l ta β Obj (fb(l  tb)) T" by simp
        ultimately
        show ?case
          using z = Upd (Obj fa T) l ta
          by (rule_tac x = "Obj (fb(l  tb)) T" in exI, simp)
      next
          (* Upd': case Obj 
             Obj (f'(l ↦ t')) T ⇒β Obj (fb(l ↦ tb)) T 
           ∧ Obj (fa(l ↦ ta)) T ⇒β Obj (fb(l ↦ tb)) T *)
        case (obj f'' fa T' ta La) 
        note pred_ta = this(5) and this
        hence 
          "l  dom f" and "Obj f T β Obj fa T" and
          "z = Obj (fa(l  ta)) T"
          by auto
        from diamond_binder[OF finite L pred_bnd finite La pred_ta]
        obtain Lb tb where
          "finite Lb" and
          tb1: "s p. s  Lb  p  Lb  s  p 
                  (u. t'⇗[Fvar s,Fvar p]⇖ β u  tb = σ[s,p] u)" and
          tb2: "s p. s  Lb  p  Lb  s  p 
                  (u. ta⇗[Fvar s,Fvar p]⇖ β u  tb = σ[s,p] u)"
          by auto
        from Obj f T β Obj fa T pred_obj
        obtain b where "Obj f' T β b" and "Obj fa T β b"
          by (elim allE impE exE conjE, simp)
        with par_beta_lc[OF this(1)] par_beta_lc[OF this(2)]
        obtain fb where 
          "Obj f' T β Obj fb T" "lc (Obj f' T)" and
          "Obj fa T β Obj fb T" "lc (Obj fa T)"
          by auto
        from 
          par_beta_body[OF finite Lb tb1] 
          Obj_pbeta_subst[OF finite Lb tb1 this(1-2)]
          par_beta_body[OF finite Lb tb2] 
          Obj_pbeta_subst[OF finite Lb tb2 this(3-4)]
        have 
          "Obj (f'(l  t')) T β Obj (fb(l  tb)) T" and
          "Obj (fa(l  ta)) T β Obj (fb(l  tb)) T" 
          by simp+
        with z = Obj (fa(l  ta)) T show ?case
          by (rule_tac x = "Obj (fb(l  tb)) T" in exI, simp)
      qed
    qed
  next
    case (pbeta_Call t t' u u' l) 
    note pred_t = this(2) and pred_u = this(4)
    show ?case
    proof (intro strip)
      fix z assume "Call t l u β z"
      thus "u. Call t' l u' β u  z β u"
      proof (induct rule: Call_par_red)
          (* Call: case Call 
             Call t' l u' ⇒β Call tb l ub ∧ Call t' l u' ⇒β Call tb l ub *)
        case (call ta ua)
        from 
          this(1-2) pred_t pred_u
        obtain tb ub where "t' β tb" "u' β ub" "ta β tb" "ua β ub"
          by (elim allE impE exE conjE, simp)
        from 
          par_beta_lc[OF this(1)] par_beta_lc[OF this(2)]
          par_beta.pbeta_Call[OF this(1-2)]
          par_beta_lc[OF this(3)] par_beta_lc[OF this(4)] 
          par_beta.pbeta_Call[OF this(3-4)]
          z = Call ta l ua
        show ?case
          by (rule_tac x = "Call tb l ub" in exI, simp)
      next
          (* Call: case beta 
             Call (Obj f' T) l u' ⇒β (the (fb l)[Obj fb T,ub])
           ∧ the (fa l)[Obj fa T,ua]β (the (fb l)[Obj fb T,ub]) *)
        case (beta f fa T ua) 
        from this(1-2) have "t β Obj fa T" by simp
        with u β ua pred_t pred_u
        obtain b ub where 
          "t' β b" and "Obj fa T β b" and "u' β ub" and "ua β ub"
          by (elim allE impE exE conjE, simp)
        from this(1-2) par_beta_lc[OF this(2)]
        obtain fb where 
          "t' β Obj fb T" and 
          "Obj fa T β Obj fb T" and "lc (Obj fa T)"
          by auto
        from 
          par_beta_beta[OF l  dom fa this(2) ua β ub this(3)]
          par_beta_lc[OF ua β ub]
        have "the (fa l)⇗[Obj fa T,ua]⇖ β (the (fb l)⇗[Obj fb T,ub]⇖)" by simp
        moreover
        from l  dom fa Obj_pbeta[OF Obj fa T β Obj fb T]
        have "l  dom fb" by simp
        from 
          t β t' sym[OF Obj f T = t]
          par_beta_lc[OF t β t'] t' β Obj fb T
        obtain f' where 
          "t' = Obj f' T" and "Obj f' T β Obj fb T" and
          "lc (Obj f' T)"
          by auto
        from 
          Obj_pbeta[OF this(2)] l  dom fb
          par_beta.pbeta_beta[OF this(2) _ u' β ub this(3)]
          par_beta_lc[OF u' β ub]
        have "Call (Obj f' T) l u' β (the (fb l)⇗[Obj fb T,ub]⇖)" by auto
        ultimately
        show ?case
          using t' = Obj f' T z = (the (fa l)⇗[Obj fa T,ua]⇖)
          by (rule_tac x = "(the (fb l)⇗[Obj fb T,ub]⇖)" in exI, simp)
      qed
    qed
  next
    case (pbeta_beta f T f' l p p') 
    note pred_obj = this(2) and pred_p = this(5)
    show ?case
    proof (intro strip)
      fix z assume "Call (Obj f T) l p β z"
      thus "u. the (f' l)⇗[Obj f' T,p']⇖ β u  z β u"
      proof (induct rule: Call_par_red)
          (* beta: case Call 
             Call (Obj fa T) l pa ⇒β (the (fb l)[Obj fb T,pb]) 
           ∧ the (f' l)[Obj f' T,p']β (the (fb l)[Obj fb T,pb]) *)
        case (call a pa)
        then obtain fa where 
          "Obj f T β Obj fa T" and "z = Call (Obj fa T) l pa"
          by auto
        from 
          this(1) p β pa pred_obj pred_p
        obtain b pb where 
          "Obj f' T β b" and "Obj fa T β b" and 
          "p' β pb" and "pa β pb"
          by (elim allE impE exE conjE, simp)
        with par_beta_lc[OF this(1)] par_beta_lc[OF this(2)]
        obtain fb where 
          "Obj f' T β Obj fb T" and "lc (Obj f' T)" and
          "Obj fa T β Obj fb T" and "lc (Obj fa T)"
          by auto
        from this(1) l  dom f Obj f T β Obj f' T Obj f T β Obj fa T
        have "l  dom f'" and "l  dom fa" by auto
        from p' β pb pa β pb par_beta_lc
        have "p' β pb" and "lc p'" and "pa β pb" and "lc pa" by auto
        from 
          par_beta.pbeta_beta[OF Obj fa T β Obj fb T l  dom fa
                                  this(3) lc (Obj fa T) this(4)] 
          par_beta_beta[OF l  dom f' Obj f' T β Obj fb T
                            this(1) lc (Obj f' T) this(2)]
          z = Call (Obj fa T) l pa
        show ?case
          by (rule_tac x = "(the (fb l)⇗[Obj fb T,pb]⇖)" in exI, simp)
      next
          (* beta: case beta 
             the (f' l)[Obj f' T,p']β (the (fb l)[Obj fb T,pb])
          ∧  the (fa l)[Obj fa T,pa]β (the (fb l)[Obj fb T,pb]) *)
        case (beta f'' fa Ta pa)
        hence "Obj f T β Obj fa T" and "z = (the (fa l)⇗[Obj fa T,pa]⇖)"
          by auto
        with p β pa pred_obj pred_p
        obtain b pb where 
          "Obj f' T β b" and "Obj fa T β b" and
          "p' β pb" and "pa β pb"
          by (elim allE impE exE conjE, simp)
        with par_beta_lc
        obtain fb where 
          "Obj f' T β Obj fb T" and "lc (Obj f' T)" and "lc p'" and
          "Obj fa T β Obj fb T" and "lc (Obj fa T)" and "lc pa"
          by auto
        from l  dom f Obj f T β Obj f' T Obj f T β Obj fa T
        have "l  dom f'" and "l  dom fa" by auto
        from
          par_beta_beta[OF l  dom f' Obj f' T β Obj fb T 
                           p' β pb lc (Obj f' T) lc p']
          par_beta_beta[OF l  dom fa Obj fa T β Obj fb T 
                           pa β pb lc (Obj fa T) lc pa]
          z = (the (fa l)⇗[Obj fa T,pa]⇖)
        show ?case
          by (rule_tac x = "(the (fb l)⇗[Obj fb T,pb]⇖)" in exI, simp)
      qed
    qed
  qed
qed

subsection ‹Confluence (classical not via complete developments)›

theorem beta_confluent: "confluent beta"
  by (rule diamond_par_beta diamond_to_confluence
      par_beta_subset_beta beta_subset_par_beta)+

end