# Theory ParRed

Up to index of Isabelle/HOL/Locally-Nameless-Sigma

theory ParRed
imports Commutation Sigma
`(*  Title:      Sigma/ParRed.thy    Author:     Ludovic Henrio and Florian Kammuller    Copyright   2006Confluence of beta for ASP, based on the equally named file in HOL/Proofs/Lambda.*)header {* Parallel reduction *}theory ParRed imports "~~/src/HOL/Proofs/Lambda/Commutation" Sigma beginsubsection {* 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;     ∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p                  --> (∃t. (the(f l)⇗[Fvar s, Fvar p]⇖) =>⇩β t                         ∧ the(f' l) = σ[s,p] t);     ∀l∈dom 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 \<mapsto> 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 \<mapsto> u')) T |] ==> Q"  shows Q  using assmsproof (cases rule: par_beta.cases)  case pbeta_Upd thus ?thesis using assms(2) by forcenext  case pbeta_Upd'  from this(1-2) this(5-6) assms(3)[OF _ _ this(3-4)]  show ?thesis by forceqedlemma 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 assmsproof (cases rule: par_beta.cases)  case pbeta_Call thus ?thesis using assms(2) by forcenext  case pbeta_beta  from this(1-5) assms(3)[OF _ this(3)]  show ?thesis by forceqedlemma 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 \<mapsto> t')) T)" and  "!!f f' T. [| dom f' = dom f; ∀l∈dom f. body (the(f l));                ∀l∈dom 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 assmsproof   (induct    taking: "λt t'. body t'"    rule: pbeta_induct)  case Fvar thus ?case by simpnext  case Call thus ?case by simpnext  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 forceqedlemma par_beta_preserves_FV[simp, rule_format]:   fixes t t' x  assumes "t =>⇩β t'"  shows "x ∉ FV t --> x ∉ FV t'"using assmsproof   (induct    taking: "λt t'. x ∉ FV t --> x ∉ FV t'"    rule: pbeta_induct)  case Fvar thus ?case by simpnext  case Call thus ?case by simpnext  case Upd thus ?case by simpnext  case Upd' thus ?case by simpnext  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)  qednext  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)  qedqedlemma 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 simpqedsubsection {* Miscellaneous properties of par\_beta *}lemma Fvar_pbeta [simp]: "(Fvar x =>⇩β t) = (t = Fvar x)" by autolemma Obj_pbeta: "Obj f T =>⇩β Obj f' T  ==> dom f' = dom f       ∧ (∃L. finite L            ∧ (∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p               --> (∃t. (the(f l)⇗[Fvar s, Fvar p]⇖) =>⇩β t                       ∧ the(f' l) = σ[s,p]t)))      ∧ (∀l∈dom 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 \<mapsto> t)) T =>⇩β Obj (f'(l \<mapsto> 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 \<mapsto> t')) = dom (f(l \<mapsto> t))" and     exL: "∃L. finite L             ∧ (∀l∈dom 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: "∀l∈dom f. body (the (f l))"    by auto  assume "body t" with bodyf   have body: "∀l'∈dom (f(l \<mapsto> t)). body (the ((f(l \<mapsto> 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 \<mapsto> t)). ∀s p. s ∉ L' ∪ L ∧ p ∉ L' ∪ L ∧ s ≠ p                             --> (∃t''. the ((f(l \<mapsto> t)) l')⇗[Fvar s,Fvar p]⇖ =>⇩β t''                                      ∧ the ((f'(l \<mapsto> t')) l') = σ[s,p] t'')"    by auto  from par_beta.pbeta_Obj[OF dom this body]  show "Obj (f(l \<mapsto> t)) T =>⇩β Obj (f'(l \<mapsto> t')) T"    by assumptionqedlemma 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 assmsproof -  def pred_cof ≡ "λL t. (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p                           --> (∃t'. (t⇗[Fvar s, Fvar p]⇖) =>⇩β t' ∧ t = σ[s,p] 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    def pred_fl ≡ "λs p b l::Label. (∃t'. (the b⇗[Fvar s, Fvar p]⇖) =>⇩β t' ∧ the b = σ[s,p]t')"    from fmap_ex_cof[of f pred_fl] pred    obtain L where      "finite L" and "∀l∈dom 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  qedqedlemma 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)qedlemma par_beta_ssubst[rule_format]:  fixes t t'  assumes "t =>⇩β t'"  shows "∀x v v'. v =>⇩β v' --> [x -> v] t =>⇩β [x -> v'] t'"proof -  def pred_cof ≡ "λL t t'. (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p                              --> (∃t''. t⇗[Fvar s, Fvar p]⇖ =>⇩β t'' ∧ t' = σ[s,p] 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 \<mapsto> 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'      def pred_bnd ≡ "λs p b b' l::Label. ∃t''. [x -> v] the b⇗[Fvar s,Fvar p]⇖ =>⇩β t''                                               ∧ [x -> v'] the b' = σ[s,p] t''"      assume "v =>⇩β v'"      with pred `dom f' = dom f` fmap_ex_cof2[of f' f pred_bnd]       obtain L where        "finite L" and         predf: "∀l∈dom f. pred_cof L ([x -> v] the (f l)) ([x -> v'] the (f' l))"        unfolding pred_cof_def pred_bnd_def         by auto      have "∀l∈dom (λ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 `∀l∈dom 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  qedqedlemma 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: "∀l∈dom 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    "∀l∈dom 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)qedsubsection {* Inclusions *}text {* @{text "beta ⊆ par_beta ⊆ beta^*"} \medskip *}lemma beta_subset_par_beta: "beta ≤ par_beta"proof (clarify)  def pred_cof ≡ "λL t t'. (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p                           --> (∃t''. (t⇗[Fvar s, Fvar p]⇖) =>⇩β t'' ∧ t' = σ[s,p] 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)  qedqedlemma par_beta_subset_beta: "par_beta ≤ beta^**"proof (rule predicate2I)  def pred_cof ≡ "λL t t'. (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p                              --> (∃t''. (t⇗[Fvar s, Fvar p]⇖) ->⇩β⇧* t'' ∧ t' = σ[s,p] 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)    def pred_bnd ≡ "λs p b b' l::Label. ∃t''. the b⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t''                                             ∧ the b' = σ[s,p] t''"    from       pred `dom f' = dom f` fmap_ex_cof2[of f' f pred_bnd]    obtain L where      "finite L" and       "∀l∈dom 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  qedqedsubsection {* 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)qedlemma 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     --> (∀l∈dom 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    --> (∀l∈dom 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             ∧ (∀l∈dom f. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p                            --> (∃t. (the(f' l)⇗[Fvar s, Fvar p]⇖) =>⇩β t                                   ∧ the(lu l) = σ[s,p]t))            ∧ (∀l∈dom f. body (the (f' l)))            ∧ (∀l∈dom f. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p                            --> (∃t. (the(lz l)⇗[Fvar s, Fvar p]⇖) =>⇩β t                                   ∧ the(lu l) = σ[s,p]t))            ∧ (∀l∈dom f. body (the (lz l)))))"  using assmsproof (induct rule: fmap_induct3)  case empty thus ?case by forcenext   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        *: "∀l∈dom (F1(x \<mapsto> a)).            ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p            --> P (the ((F1(x \<mapsto> a)) l)) (the ((F(x \<mapsto> t)) l)) s p"      hence         F: "∀l∈dom 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 \<mapsto> a))" by simp        moreover assume "s ∉ L ∧ p ∉ L ∧ s ≠ p"        ultimately        have "P (the((F1(x \<mapsto> a)) l)) (the((F(x \<mapsto> 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: "∀l∈dom (F1(x \<mapsto> a)). ∀s p. s ∉ L1 ∧ p ∉ L1 ∧ s ≠ p         --> (∃t. (the ((F1(x \<mapsto> a)) l)⇗[Fvar s,Fvar p]⇖ =>⇩β t                ∧ (∀z. the ((F1(x \<mapsto> a)) l)⇗[Fvar s,Fvar p]⇖ =>⇩β z                    --> (∃u. t =>⇩β u ∧ z =>⇩β u)))                ∧ the ((F3(x \<mapsto> c)) l) = σ[s,p] t)" and      b: "∀l∈dom (F1(x \<mapsto> a)). ∀s p. s ∉ L2 ∧ p ∉ L2 ∧ s ≠ p         --> (∃t. the ((F1(x \<mapsto> a)) l)⇗[Fvar s,Fvar p]⇖ =>⇩β t                ∧ the ((F2(x \<mapsto> 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           ∧ (∀l∈dom F1. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p                           --> (∃t. the (F3 l)⇗[Fvar s,Fvar p]⇖ =>⇩β t                                  ∧ the (lu l) = σ[s,p] t))           ∧ (∀l∈dom F1. body (the (F3 l)))           ∧ (∀l∈dom F1. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p                           --> (∃t. the (F2 l)⇗[Fvar s,Fvar p]⇖ =>⇩β t                                  ∧ the (lu l) = σ[s,p] t))           ∧ (∀l∈dom 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: "∀l∈dom 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: "∀l∈dom F1. body (the (F3 l))" and      pred_F2: "∀l∈dom 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: "∀l∈dom 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 \<mapsto> t)) = dom (F1(x \<mapsto> a))" by simp    moreover    from pred_c pred_F3    have       "∀l∈dom (F1(x \<mapsto> a)). ∀s p. s ∉ La ∪ Lb ∧ p ∉ La ∪ Lb ∧ s ≠ p                               --> (∃t'. the ((F3(x \<mapsto> c)) l)⇗[Fvar s,Fvar p]⇖ =>⇩β t'                                       ∧ the ((f(x \<mapsto> t)) l) = σ[s,p] t')"      by auto    moreover    from bodycb(1) body_F3     have "∀l∈dom (F1(x \<mapsto> a)). body (the ((F3(x \<mapsto> c)) l))"      by simp    moreover    from pred_b pred_F2    have       "∀l∈dom (F1(x \<mapsto> a)). ∀s p. s ∉ La ∪ Lb ∧ p ∉ La ∪ Lb ∧ s ≠ p                               --> (∃t'. the ((F2(x \<mapsto> b)) l)⇗[Fvar s,Fvar p]⇖ =>⇩β t'                                       ∧ the ((f(x \<mapsto> t)) l) = σ[s,p] t')"      by auto    moreover    from bodycb(2) body_F2     have "∀l∈dom (F1(x \<mapsto> a)). body (the ((F2(x \<mapsto> b)) l))"      by simp    ultimately    show       "∃L'. finite L'          ∧ (∃lu. dom lu = dom (F1(x \<mapsto> a))                 ∧ (∀l∈dom (F1(x \<mapsto> a)).                     ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p                      --> (∃t'. the ((F3(x \<mapsto> c)) l)⇗[Fvar s,Fvar p]⇖ =>⇩β t'                             ∧ the (lu l) = σ[s,p] t'))                ∧ (∀l∈dom (F1(x \<mapsto> a)). body (the ((F3(x \<mapsto> c)) l)))                 ∧ (∀l∈dom (F1(x \<mapsto> a)).                     ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p                      --> (∃t'. the ((F2(x \<mapsto> b)) l)⇗[Fvar s,Fvar p]⇖ =>⇩β t'                ∧ the (lu l) = σ[s,p] t'))                ∧ (∀l∈dom (F1(x \<mapsto> a)). body (the ((F2(x \<mapsto> b)) l))))"      by (rule_tac x = "La ∪ Lb" in exI,         simp (no_asm_simp) only: conjI simp_thms(22),        rule_tac x = "(f(x \<mapsto> t))" in exI, simp)  qedqedlemma exL_exMap:  "[| dom (f::Label -~> sterm) = dom (lz::Label -~> sterm);      dom (f'::Label -~> sterm) = dom f;      finite L1;     ∀l∈dom 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;     ∀l∈dom 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                ∧ (∀l∈dom f. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p                               --> (∃t. (the(f' l)⇗[Fvar s, Fvar p]⇖) =>⇩β t                                      ∧ the(lu l) = σ[s,p]t))               ∧ (∀l∈dom f. body (the (f' l)))               ∧ (∀l∈dom f. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p                               --> (∃t. (the(lz l)⇗[Fvar s, Fvar p]⇖) =>⇩β t                                      ∧ the(lu l) = σ[s,p]t))               ∧ (∀l∈dom f. body (the (lz l))))"  using exL_exMap_lem[of f lz f'] by simplemma diamond_par_beta: "diamond par_beta"  unfolding diamond_def commute_def square_defproof (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 \<mapsto> ub)) T            ∧ Obj (fa(l \<mapsto> ua)) T =>⇩β Obj (fb(l \<mapsto> 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 \<mapsto> ua)) T =>⇩β Obj (fb(l \<mapsto> 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 \<mapsto> ua)) T` `t' = Obj f' T`          by (rule_tac x = "Obj (fb(l \<mapsto> 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        "∀l∈dom 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        "∀l∈dom 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        "∀l∈dom f'. body (the (f' l))" and        "∀l∈dom 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        "∀l∈dom 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 \<mapsto> t')) T =>⇩β u ∧ z =>⇩β u"      proof (induct rule: Upd_par_red)          (* Upd': case Upd              Obj (f'(l \<mapsto> t')) T =>⇩β Obj (fb(l \<mapsto> tb)) T            ∧ Upd (Obj fa T) l ta =>⇩β Obj (fb(l \<mapsto> 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 \<mapsto> t')) T =>⇩β Obj (fb(l \<mapsto> 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 \<mapsto> tb)) T" by simp        ultimately        show ?case          using `z = Upd (Obj fa T) l ta`          by (rule_tac x = "Obj (fb(l \<mapsto> tb)) T" in exI, simp)      next          (* Upd': case Obj              Obj (f'(l \<mapsto> t')) T =>⇩β Obj (fb(l \<mapsto> tb)) T            ∧ Obj (fa(l \<mapsto> ta)) T =>⇩β Obj (fb(l \<mapsto> 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 \<mapsto> 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 \<mapsto> t')) T =>⇩β Obj (fb(l \<mapsto> tb)) T" and          "Obj (fa(l \<mapsto> ta)) T =>⇩β Obj (fb(l \<mapsto> tb)) T"           by simp+        with `z = Obj (fa(l \<mapsto> ta)) T` show ?case          by (rule_tac x = "Obj (fb(l \<mapsto> 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  qedqedsubsection {* 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`