Theory Throw_Non_Destructive

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


section ‹Non Destructiveness of Throw›


(*<*)
theory Throw_Non_Destructive
  imports Process_Restriction_Space "HOL-CSP_OpSem.Initials"
begin
  (*>*)


subsection ‹Equality›

lemma Depth_Throw_1_is_constant: ‹P Θ a ∈ A. Q1 a ↓ 1 = P Θ a ∈ A. Q2 a ↓ 1›
proof (rule FD_antisym)
  show ‹P Θ a ∈ A. Q2 a ↓ 1 ⊑⇩F⇩D P Θ a ∈ A. Q1 a ↓ 1› for Q1 Q2
  proof (unfold refine_defs, safe)
    show div :  ‹t ∈ 𝒟 (Throw P A Q1 ↓ 1) ⟹ t ∈ 𝒟 (Throw P A Q2 ↓ 1)› for t
    proof (elim D_restriction_process⇩p⇩t⇩i⇩c⇩kE) 
      assume ‹t ∈ 𝒟 (P Θ a ∈ A. Q1 a)› and ‹length t ≤ 1›
      from ‹length t ≤ 1› consider ‹t = []› | e where ‹t = [e]› by (cases t) simp_all
      thus ‹t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)›
      proof cases
        from ‹t ∈ 𝒟 (P Θ a ∈ A. Q1 a)› show ‹t = [] ⟹ t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)›
          by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩k D_Throw)
      next
        fix e assume ‹t = [e]›
        with ‹t ∈ 𝒟 (P Θ a ∈ A. Q1 a)›
        consider ‹[] ∈ 𝒟 P› | a where ‹t = [ev a]› ‹[ev a] ∈ 𝒟 P› ‹a ∉ A›
          | a where ‹t = [ev a]› ‹[ev a] ∈ 𝒯 P› ‹a ∈ A›
          by (auto simp add: D_Throw disjoint_iff image_iff)
            (metis D_T append_Nil event⇩p⇩t⇩i⇩c⇩k.exhaust process_charn,
              metis append_Nil empty_iff empty_set hd_append2 hd_in_set in_set_conv_decomp set_ConsD)
        thus ‹t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)›
        proof cases
          show ‹t = [ev a] ⟹ [ev a] ∈ 𝒯 P ⟹ a ∈ A ⟹ t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)› for a
            by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩k T_Throw)
              (metis append_Nil append_self_conv front_tickFree_charn inf_bot_left
                is_ev_def is_processT1_TR length_0_conv length_Cons list.set(1)
                tickFree_Cons_iff tickFree_Nil)
        next
          show ‹[] ∈ 𝒟 P ⟹ t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)›
            by (simp flip: BOT_iff_Nil_D add: D_BOT)
              (use ‹t = [e]› front_tickFree_single in blast)
        next
          show ‹t = [ev a] ⟹ [ev a] ∈ 𝒟 P ⟹ a ∉ A ⟹ t ∈ 𝒟 (P Θ a ∈ A. Q2 a ↓ 1)› for a  
            by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩k D_Throw disjoint_iff image_iff)
              (metis append.right_neutral empty_set event⇩p⇩t⇩i⇩c⇩k.disc(1) event⇩p⇩t⇩i⇩c⇩k.sel(1)
                front_tickFree_Nil list.simps(15) singletonD tickFree_Cons_iff tickFree_Nil)
        qed
      qed
    next
      fix u v assume * : ‹t = u @ v› ‹u ∈ 𝒯 (Throw P A Q1)› ‹length u = 1› ‹tF u› ‹ftF v›
      from ‹length u = 1› ‹tF u› obtain a where ‹u = [ev a]›
        by (cases u) (auto simp add: is_ev_def)
      with "*"(2) show ‹t ∈ 𝒟 (Throw P A Q2 ↓ 1)›
        by (simp add: ‹t = u @ v› D_restriction_process⇩p⇩t⇩i⇩c⇩k Throw_projs Cons_eq_append_conv)
          (metis (no_types) "*"(3-5) One_nat_def append_Nil empty_set inf_bot_left
            insert_disjoint(2) is_processT1_TR list.simps(15))
    qed

    show ‹(t, X) ∈ ℱ (Throw P A Q1 ↓ 1) ⟹ (t, X) ∈ ℱ (Throw P A Q2 ↓ 1)› for t X
    proof (elim F_restriction_process⇩p⇩t⇩i⇩c⇩kE)
      assume ‹(t, X) ∈ ℱ (P Θ a ∈ A. Q1 a)› ‹length t ≤ 1›
      then consider ‹t ∈ 𝒟 (P Θ a ∈ A. Q1 a)› | ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` A = {}›
        | a where ‹t = [ev a]› ‹[ev a] ∈ 𝒯 P› ‹a ∈ A›
        by (auto simp add: F_Throw D_Throw)
      thus ‹(t, X) ∈ ℱ (P Θ a ∈ A. Q2 a ↓ 1)›
      proof cases
        from D_F div ‹length t ≤ 1›
        show ‹t ∈ 𝒟 (P Θ a ∈ A. Q1 a) ⟹ (t, X) ∈ ℱ (P Θ a ∈ A. Q2 a ↓ 1)›
          using D_restriction_process⇩p⇩t⇩i⇩c⇩kI by blast
      next
        show ‹(t, X) ∈ ℱ P ⟹ set t ∩ ev ` A = {} ⟹ (t, X) ∈ ℱ (Throw P A Q2 ↓ 1)›
          by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩k F_Throw)
      next
        show ‹⟦t = [ev a]; [ev a] ∈ 𝒯 P; a ∈ A⟧ ⟹ (t, X) ∈ ℱ (Throw P A Q2 ↓ 1)› for a
          by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩k T_Throw)
            (metis append.right_neutral append_Nil empty_set event⇩p⇩t⇩i⇩c⇩k.disc(1)
              front_tickFree_Nil inf_bot_left is_processT1_TR length_Cons
              list.size(3) tickFree_Cons_iff tickFree_Nil)
      qed
    next
      fix u v assume * : ‹t = u @ v› ‹u ∈ 𝒯 (Throw P A Q1)› ‹length u = 1› ‹tF u› ‹ftF v›
      from ‹length u = 1› ‹tF u› obtain a where ‹u = [ev a]›
        by (cases u) (auto simp add: is_ev_def)
      with "*"(2) show ‹(t, X) ∈ ℱ (Throw P A Q2 ↓ 1)›
        by (simp add: ‹t = u @ v› F_restriction_process⇩p⇩t⇩i⇩c⇩k Throw_projs Cons_eq_append_conv)
          (metis (no_types) "*"(3-5) One_nat_def append_Nil empty_set inf_bot_left
            insert_disjoint(2) is_processT1_TR list.simps(15))
    qed
  qed

  thus ‹P Θ a ∈ A. Q2 a ↓ 1 ⊑⇩F⇩D P Θ a ∈ A. Q1 a ↓ 1› by simp
qed



subsection ‹Refinement›

lemma restriction_process⇩p⇩t⇩i⇩c⇩k_Throw_FD :
  ‹(P Θ a ∈ A. Q a) ↓ n ⊑⇩F⇩D (P ↓ n) Θ a ∈ A. (Q a ↓ n)› (is ‹?lhs ⊑⇩F⇩D ?rhs›)
proof (unfold refine_defs, safe)
  show ‹t ∈ 𝒟 ?lhs› if ‹t ∈ 𝒟 ?rhs› for t
  proof -
    from ‹t ∈ 𝒟 ?rhs›
    consider t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒟 (P ↓ n)› ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
      | t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 (P ↓ n)›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟 (Q a ↓ n)›
      unfolding D_Throw by blast
    thus ‹t ∈ 𝒟 ?lhs›
    proof cases
      show ‹⟦t = t1 @ t2; t1 ∈ 𝒟 (P ↓ n); tF t1; set t1 ∩ ev ` A = {}; ftF t2⟧ ⟹ t ∈ 𝒟 ?lhs› for t1 t2
        by (elim D_restriction_process⇩p⇩t⇩i⇩c⇩kE, simp_all add: Throw_projs D_restriction_process⇩p⇩t⇩i⇩c⇩k)
          (blast, metis (no_types, lifting) front_tickFree_append inf_sup_aci(8) inf_sup_distrib2 sup_bot_right)
    next
      fix t1 a t2
      assume ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 (P ↓ n)›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟 (Q a ↓ n)›
      from ‹t2 ∈ 𝒟 (Q a ↓ n)› show ‹t ∈ 𝒟 ?lhs›
      proof (elim D_restriction_process⇩p⇩t⇩i⇩c⇩kE)
        from ‹t1 @ [ev a] ∈ 𝒯 (P ↓ n)› show ‹t2 ∈ 𝒟 (Q a) ⟹ length t2 ≤ n ⟹ t ∈ 𝒟 ?lhs›
        proof (elim T_restriction_process⇩p⇩t⇩i⇩c⇩kE)
          from ‹a ∈ A› ‹set t1 ∩ ev ` A = {}› ‹t = t1 @ ev a # t2›
          show ‹t2 ∈ 𝒟 (Q a) ⟹ t1 @ [ev a] ∈ 𝒯 P ⟹ t ∈ 𝒟 ?lhs›
            by (auto simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩k D_Throw)
        next
          fix u v assume ‹t2 ∈ 𝒟 (Q a)› ‹length t2 ≤ n› ‹t1 @ [ev a] = u @ v›
            ‹u ∈ 𝒯 P› ‹length u = n› ‹tF u› ‹ftF v›
          from ‹t1 @ [ev a] = u @ v› ‹ftF v› consider ‹t1 @ [ev a] = u›
            | v' where ‹t1 = u @ v'› ‹v = v' @ [ev a]› ‹ftF v'›
            by (cases v rule: rev_cases) (simp_all add: front_tickFree_append_iff)
          thus ‹t ∈ 𝒟 ?lhs›
          proof cases
            from ‹a ∈ A› ‹length u = n› ‹set t1 ∩ ev ` A = {}› ‹t2 ∈ 𝒟 (Q a)› ‹tF u› ‹u ∈ 𝒯 P›
            show ‹t1 @ [ev a] = u ⟹ t ∈ 𝒟 ?lhs›
              by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩k T_Throw ‹t = t1 @ ev a # t2›)
                (metis Cons_eq_appendI D_imp_front_tickFree append_Nil append_assoc is_processT1_TR)
          next
            from ‹ftF v› ‹length u = n› ‹set t1 ∩ ev ` A = {}› ‹t = t1 @ ev a # t2› ‹u ∈ 𝒯 P›
            show ‹t1 = u @ v' ⟹ v = v' @ [ev a] ⟹ ftF v' ⟹ t ∈ 𝒟 ?lhs› for v'
              by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩k T_Throw)
                (metis D_imp_front_tickFree Int_assoc Un_Int_eq(3) append_assoc
                  front_tickFree_append front_tickFree_nonempty_append_imp
                  inf_bot_right list.distinct(1) same_append_eq set_append ‹t ∈ 𝒟 ?rhs›)
          qed
        qed
      next
        from ‹t1 @ [ev a] ∈ 𝒯 (P ↓ n)›
        show ‹⟦t2 = u @ v; u ∈ 𝒯 (Q a); length u = n; tF u; ftF v⟧ ⟹ t ∈ 𝒟 ?lhs› for u v
        proof (elim T_restriction_process⇩p⇩t⇩i⇩c⇩kE)
          assume ‹t2 = u @ v› ‹u ∈ 𝒯 (Q a)› ‹length u = n› ‹tF u›
            ‹ftF v› ‹t1 @ [ev a] ∈ 𝒯 P› ‹length (t1 @ [ev a]) ≤ n›
          from ‹a ∈ A› ‹set t1 ∩ ev ` A = {}› ‹t1 @ [ev a] ∈ 𝒯 P› ‹u ∈ 𝒯 (Q a)›
          have ‹t1 @ ev a # u ∈ 𝒯 (P Θ a∈A. Q a)› by (auto simp add: T_Throw)
          moreover have ‹n < length (t1 @ ev a # u)› by (simp add: ‹length u = n›)
          ultimately have ‹t1 @ ev a # u ∈ 𝒟 ?lhs› by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
          moreover have ‹t = (t1 @ ev a # u) @ v› by (simp add: ‹t = t1 @ ev a # t2› ‹t2 = u @ v›)
          moreover from ‹t1 @ [ev a] ∈ 𝒯 P› ‹tF u› append_T_imp_tickFree
          have ‹tF (t1 @ ev a # u)› by auto
          ultimately show ‹t ∈ 𝒟 ?lhs› using ‹ftF v› is_processT7 by blast
        next
          fix w x assume ‹t2 = u @ v› ‹u ∈ 𝒯 (Q a)› ‹length u = n› ‹tF u› ‹ftF v›
            ‹t1 @ [ev a] = w @ x› ‹w ∈ 𝒯 P› ‹length w = n› ‹tF w› ‹ftF x›
          from ‹t1 @ [ev a] = w @ x› consider ‹t1 @ [ev a] = w›
            | x' where ‹t1 = w @ x'› ‹x = x' @ [ev a]›
            by (cases x rule: rev_cases) simp_all
          thus ‹t ∈ 𝒟 ?lhs›
          proof cases
            assume ‹t1 @ [ev a] = w›
            with ‹a ∈ A› ‹set t1 ∩ ev ` A = {}› ‹u ∈ 𝒯 (Q a)› ‹w ∈ 𝒯 P›
            have ‹t1 @ ev a # u ∈ 𝒯 (P Θ a∈A. Q a)› by (auto simp add: T_Throw)
            moreover have ‹n < length (t1 @ ev a # u)› by (simp add: ‹length u = n›)
            ultimately have ‹t1 @ ev a # u ∈ 𝒟 ?lhs› by (blast intro: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
            moreover have ‹t = (t1 @ ev a # u) @ v›
              by (simp add: ‹t = t1 @ ev a # t2› ‹t2 = u @ v›)
            moreover from ‹t1 @ [ev a] = w› ‹tF u› ‹tF w› have ‹tF (t1 @ ev a # u)› by auto
            ultimately show ‹t ∈ 𝒟 ?lhs› using ‹ftF v› is_processT7 by blast
          next
            fix x' assume ‹t1 = w @ x'› ‹x = x' @ [ev a]›
            from ‹set t1 ∩ ev ` A = {}› ‹t1 = w @ x'› ‹w ∈ 𝒯 P›
            have ‹w ∈ 𝒯 P ∧ set w ∩ ev ` A = {}› by auto
            hence ‹w ∈ 𝒯 (P Θ a∈A. Q a)› by (simp add: T_Throw)
            with ‹length w = n› ‹tF w› have ‹w ∈ 𝒟 ?lhs›
              by (blast intro: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
            moreover have ‹t = w @ x @ t2›
              by (simp add: ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] = w @ x›)
            moreover from D_imp_front_tickFree[OF ‹t ∈ 𝒟 ?rhs›] ‹t = t1 @ ev a # t2› ‹t1 = w @ x'›
              front_tickFree_nonempty_append_imp that tickFree_append_iff
            have ‹ftF (x @ t2)› by (simp add: ‹t = w @ x @ t2› front_tickFree_append_iff)
            ultimately show ‹t ∈ 𝒟 ?lhs› by (simp add: ‹tF w› is_processT7)
          qed
        qed
      qed
    qed
  qed

  thus ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
    by (meson is_processT8 le_approx2 mono_Throw restriction_process⇩p⇩t⇩i⇩c⇩k_approx_self)
qed



subsection ‹Non Destructiveness›

lemma Throw_non_destructive :
  ‹non_destructive (λ(P :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k, Q). P Θ a ∈ A. Q a)›
proof (rule order_non_destructiveI, clarify)
  fix P P' :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k› and Q Q' :: ‹'a ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› and n
  assume ‹(P, Q) ↓ n = (P', Q') ↓ n› ‹0 < n›
  hence ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›
    by (simp_all add: restriction_prod_def)

  { let ?lhs = ‹P Θ a ∈ A. Q a ↓ n›
    fix t u v assume ‹t = u @ v› ‹u ∈ 𝒯 (Throw P' A Q')› ‹length u = n› ‹tF u› ‹ftF v›
    from this(2) consider ‹u ∈ 𝒯 P'› ‹set u ∩ ev ` A = {}›
      | (divL) t1 t2 where ‹u = t1 @ t2› ‹t1 ∈ 𝒟 P'› ‹tF t1›
        ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
      | (traces) t1 a t2 where ‹u = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P'›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q' a)›
      unfolding T_Throw by blast
    hence ‹t ∈ 𝒟 ?lhs›
    proof cases
      assume ‹u ∈ 𝒯 P'› ‹set u ∩ ev ` A = {}›
      from ‹u ∈ 𝒯 P'› ‹length u = n› ‹P ↓ n = P' ↓ n› have ‹u ∈ 𝒯 P›
        by (metis T_restriction_process⇩p⇩t⇩i⇩c⇩kI dual_order.refl
            length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
      with ‹set u ∩ ev ` A = {}› have ‹u ∈ 𝒯 (Throw P A Q)›
        by (simp add: T_Throw)
      with ‹ftF v› ‹t = u @ v› ‹tF u› ‹length u = n› show ‹t ∈ 𝒟 ?lhs›
        by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI is_processT7)
    next
      case divL
      show ‹t ∈ 𝒟 ?lhs›
      proof (cases ‹length t1 = n›)
        assume ‹length t1 = n›
        with ‹P ↓ n = P' ↓ n› divL(2,4) have ‹t1 ∈ 𝒯 (Throw P A Q)›
          by (simp add: T_Throw)
            (metis D_T T_restriction_process⇩p⇩t⇩i⇩c⇩kI dual_order.refl
              length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
        with ‹ftF v› ‹length t1 = n› ‹t = u @ v› ‹tF u›
          divL(1,3,5) ‹length u = n› show ‹t ∈ 𝒟 ?lhs›
          by (auto simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩k is_processT7)
      next
        assume ‹length t1 ≠ n›
        with ‹length u = n› divL(1) have ‹length t1 < n› by simp
        with ‹P ↓ n = P' ↓ n› divL(2,3,4) have ‹t1 ∈ 𝒟 P›
          by (simp add: D_Throw)
            (metis D_restriction_process⇩p⇩t⇩i⇩c⇩kI length_less_in_D_restriction_process⇩p⇩t⇩i⇩c⇩k)
        with ‹ftF v› ‹t = u @ v› divL(1,3,4) show ‹t ∈ 𝒟 ?lhs›
          by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩k T_Throw)
            (metis ‹length u = n› ‹tF u› append.assoc divL(5))
      qed
    next
      case traces
      from ‹length u = n› traces(1)
      have ‹length (t1 @ [ev a]) ≤ n› ‹length t2 ≤ n› by simp_all
      from ‹P ↓ n = P' ↓ n› ‹t1 @ [ev a] ∈ 𝒯 P'› ‹length (t1 @ [ev a]) ≤ n›
      have ‹t1 @ [ev a] ∈ 𝒯 P›
        by (metis T_restriction_process⇩p⇩t⇩i⇩c⇩kI length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
      moreover from ‹length t2 ≤ n› ‹t2 ∈ 𝒯 (Q' a)› ‹Q ↓ n = Q' ↓ n›
      have ‹t2 ∈ 𝒯 (Q a)›
        by (metis T_restriction_process⇩p⇩t⇩i⇩c⇩kI restriction_fun_def
            length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
      ultimately have ‹u ∈ 𝒯 (P Θ a ∈ A. Q a)›
        using traces(1,3,4) unfolding T_Throw by blast
      with ‹ftF v› ‹length u = n› ‹t = u @ v› ‹tF u›
      show ‹t ∈ 𝒟 ?lhs› by (auto simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩k)
    qed
  } note * = this

  show ‹P Θ a ∈ A. Q a ↓ n ⊑⇩F⇩D P' Θ a ∈ A. Q' a ↓ n› (is ‹?lhs ⊑⇩F⇩D ?rhs›)
  proof (unfold refine_defs, safe)
    show div : ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    proof (elim D_restriction_process⇩p⇩t⇩i⇩c⇩kE)
      assume ‹t ∈ 𝒟 (P' Θ a ∈ A. Q' a)› ‹length t ≤ n›
      from this(1) consider (divL) t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒟 P'›
        ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
      | (divR) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P'›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟 (Q' a)›
        unfolding D_Throw by blast
      thus ‹t ∈ 𝒟 ?lhs›
      proof cases
        case divL
        show ‹t ∈ 𝒟 ?lhs›
        proof (cases ‹length t1 = n›)
          assume ‹length t1 = n›
          have ‹t1 ∈ 𝒯 P'› by (simp add: D_T divL(2))
          with ‹P ↓ n = P' ↓ n› ‹length t1 = n› have ‹t1 ∈ 𝒯 P›
            by (metis T_restriction_process⇩p⇩t⇩i⇩c⇩kI dual_order.eq_iff
                length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
          with divL(4) have ‹t1 ∈ 𝒯 (Throw P A Q)› by (simp add: T_Throw)
          with ‹length t1 = n› divL(1,3,5) show ‹t ∈ 𝒟 ?lhs›
            by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI is_processT7)
        next
          assume ‹length t1 ≠ n›
          with ‹length t ≤ n› divL(1) have ‹length t1 < n› by simp
          with ‹t1 ∈ 𝒟 P'› ‹P ↓ n = P' ↓ n› have ‹t1 ∈ 𝒟 P›
            by (metis D_restriction_process⇩p⇩t⇩i⇩c⇩kI length_less_in_D_restriction_process⇩p⇩t⇩i⇩c⇩k)
          with divL(3, 4) front_tickFree_Nil have ‹t1 ∈ 𝒟 (Throw P A Q)›
            by (simp (no_asm) add: D_Throw) blast
          with divL(1,3,5) show ‹t ∈ 𝒟 ?lhs›
            by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI is_processT7)
        qed
      next
        case divR
        from ‹length t ≤ n› divR(1)
        have ‹length (t1 @ [ev a]) ≤ n› ‹length t2 < n› by simp_all
        from ‹P ↓ n = P' ↓ n› ‹t1 @ [ev a] ∈ 𝒯 P'› ‹length (t1 @ [ev a]) ≤ n›
        have ‹t1 @ [ev a] ∈ 𝒯 P›
          by (metis T_restriction_process⇩p⇩t⇩i⇩c⇩kI length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
        moreover from ‹length t2 < n› ‹t2 ∈ 𝒟 (Q' a)› ‹Q ↓ n = Q' ↓ n›
        have ‹t2 ∈ 𝒟 (Q a)›
          by (metis D_restriction_process⇩p⇩t⇩i⇩c⇩kI restriction_fun_def
              length_less_in_D_restriction_process⇩p⇩t⇩i⇩c⇩k)
        ultimately have ‹t ∈ 𝒟 (P Θ a ∈ A. Q a)›
          using divR(1,3,4) unfolding D_Throw by blast
        thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
      qed
    next
      show ‹t = u @ v ⟹ u ∈ 𝒯 (Throw P' A Q') ⟹ length u = n ⟹
            tF u ⟹ ftF v ⟹ t ∈ 𝒟 ?lhs› for u v by (fact "*")
    qed

    show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
    proof (elim F_restriction_process⇩p⇩t⇩i⇩c⇩kE)
      assume ‹(t, X) ∈ ℱ (Throw P' A Q')› ‹length t ≤ n›
      from this(1) consider ‹t ∈ 𝒟 (Throw P' A Q')› | ‹(t, X) ∈ ℱ P'› ‹set t ∩ ev ` A = {}›
        | (failR) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P'›
          ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ ℱ (Q' a)›
        unfolding Throw_projs by auto
      thus ‹(t, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹t ∈ 𝒟 (Throw P' A Q')›
        hence ‹t ∈ 𝒟 ?rhs› by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
        with D_F div show ‹(t, X) ∈ ℱ ?lhs› by blast
      next
        assume ‹(t, X) ∈ ℱ P'› ‹set t ∩ ev ` A = {}›
        from ‹(t, X) ∈ ℱ P'› ‹P ↓ n = P' ↓ n› ‹length t ≤ n› have ‹t ∈ 𝒯 P›
          by (metis F_T T_restriction_process⇩p⇩t⇩i⇩c⇩kI length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
        with ‹set t ∩ ev ` A = {}› have ‹t ∈ 𝒯 (Throw P A Q)› by (simp add: T_Throw)
        from F_imp_front_tickFree ‹(t, X) ∈ ℱ P'› have ‹ftF t› by blast
        thus ‹(t, X) ∈ ℱ ?lhs›
        proof (elim front_tickFreeE)
          show ‹(t, X) ∈ ℱ ?lhs› if ‹tF t›
          proof (cases ‹length t = n›)
            assume ‹length t = n›
            with ‹t ∈ 𝒯 (Throw P A Q)› ‹tF t› front_tickFree_charn show ‹(t, X) ∈ ℱ ?lhs›
              by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩k) blast
          next
            assume ‹length t ≠ n›
            with ‹length t ≤ n› have ‹length t < n› by simp
            with ‹(t, X) ∈ ℱ P'› ‹P ↓ n = P' ↓ n› have ‹(t, X) ∈ ℱ P›
              by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩k length_less_in_F_restriction_process⇩p⇩t⇩i⇩c⇩k)
            with ‹set t ∩ ev ` A = {}› have ‹(t, X) ∈ ℱ (Throw P A Q)› by (simp add: F_Throw)
            thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩kI)
          qed
        next
          fix t' r assume ‹t = t' @ [✓(r)]›
          with ‹t ∈ 𝒯 (Throw P A Q)› have ‹(t, X) ∈ ℱ (Throw P A Q)›
            by (simp add: tick_T_F)
          thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩kI)
        qed
      next
        case failR
        from ‹length t ≤ n› failR(1)
        have ‹length (t1 @ [ev a]) ≤ n› ‹length t2 < n› by simp_all
        from ‹P ↓ n = P' ↓ n› ‹t1 @ [ev a] ∈ 𝒯 P'› ‹length (t1 @ [ev a]) ≤ n›
        have ‹t1 @ [ev a] ∈ 𝒯 P›
          by (metis T_restriction_process⇩p⇩t⇩i⇩c⇩kI length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
        moreover from ‹length t2 < n› ‹(t2, X) ∈ ℱ (Q' a)› ‹Q ↓ n = Q' ↓ n›
        have ‹(t2, X) ∈ ℱ (Q a)›
          by (metis F_restriction_process⇩p⇩t⇩i⇩c⇩kI restriction_fun_def
              length_less_in_F_restriction_process⇩p⇩t⇩i⇩c⇩k)
        ultimately have ‹(t, X) ∈ ℱ (P Θ a ∈ A. Q a)›
          using failR(1,3,4) unfolding F_Throw by blast
        thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩kI)
      qed
    next
      show ‹t = u @ v ⟹ u ∈ 𝒯 (Throw P' A Q') ⟹ length u = n ⟹
            tF u ⟹ ftF v ⟹ (t, X) ∈ ℱ ?lhs› for u v
        by (simp add: "*" is_processT8)
    qed
  qed
qed



lemma ThrowR_constructive_if_disjoint_initials :
  ‹constructive (λQ :: 'a ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k. P Θ a ∈ A. Q a)›
  if ‹A ∩ {e. ev e ∈ P⇧0} = {}›
proof (rule order_constructiveI)
  fix Q Q' :: ‹'a ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› and n assume ‹Q ↓ n = Q' ↓ n›

  { let ?lhs = ‹Throw P A Q ↓ Suc n›
    fix t u v
    assume ‹t = u @ v› ‹u ∈ 𝒯 (Throw P A Q')› ‹length u = Suc n› ‹tF u› ‹ftF v›
    from ‹u ∈ 𝒯 (Throw P A Q')› consider ‹u ∈ 𝒯 P› ‹set u ∩ ev ` A = {}›
      | (divL) t1 t2 where ‹u = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1›
        ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
      | (traces) t1 a t2 where ‹u = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q' a)›
      unfolding T_Throw by blast
    hence ‹u ∈ 𝒟 ?lhs›
    proof cases
      assume ‹u ∈ 𝒯 P› ‹set u ∩ ev ` A = {}›
      hence ‹u ∈ 𝒯 (Throw P A Q)› by (simp add: T_Throw)
      with ‹length u = Suc n› ‹tF u› show ‹u ∈ 𝒟 ?lhs›
        by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
    next
      case divL
      hence ‹u ∈ 𝒟 (Throw P A Q)› by (auto simp add: D_Throw)
      thus ‹u ∈ 𝒟 ?lhs› by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
    next
      case traces
      from ‹length u = Suc n› traces(1) have ‹length t2 ≤ n› by simp
      with ‹t2 ∈ 𝒯 (Q' a)› ‹Q ↓ n = Q' ↓ n› have ‹t2 ∈ 𝒯 (Q a)›
        by (metis T_restriction_process⇩p⇩t⇩i⇩c⇩kI restriction_fun_def
            length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
      with traces(1-4) have ‹u ∈ 𝒯 (Throw P A Q)› by (auto simp add: T_Throw)
      thus ‹u ∈ 𝒟 ?lhs›
        by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI ‹length u = Suc n› ‹tF u›)
    qed
    hence ‹t ∈ 𝒟 ?lhs› by (simp add: ‹ftF v› ‹t = u @ v› ‹tF u› is_processT7)
  } note * = this

  show ‹(P Θ a ∈ A. Q a) ↓ Suc n ⊑⇩F⇩D P Θ a ∈ A. Q' a ↓ Suc n› (is ‹?lhs ⊑⇩F⇩D ?rhs›)
  proof (unfold refine_defs, safe)
    show div : ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    proof (elim D_restriction_process⇩p⇩t⇩i⇩c⇩kE)
      assume ‹t ∈ 𝒟 (P Θ a ∈ A. Q' a)› ‹length t ≤ Suc n›
      from this(1) consider (divL) t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒟 P›
        ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
      | (divR) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟 (Q' a)›
        unfolding D_Throw by blast
      thus ‹t ∈ 𝒟 ?lhs›
      proof cases
        case divL
        hence ‹t ∈ 𝒟 (P Θ a ∈ A. Q a)› by (auto simp add: D_Throw)
        thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
      next
        case divR
        from divR(2,4) that have ‹t1 ≠ []›
          by (cases t1) (auto intro: initials_memI)
        with divR(1) ‹length t ≤ Suc n› nat_less_le have ‹length t2 < n› by force
        with ‹t2 ∈ 𝒟 (Q' a)› ‹Q ↓ n = Q' ↓ n› have ‹t2 ∈ 𝒟 (Q a)›
          by (metis D_restriction_process⇩p⇩t⇩i⇩c⇩kI restriction_fun_def
              length_less_in_D_restriction_process⇩p⇩t⇩i⇩c⇩k)
        with divR(1-4) have ‹t ∈ 𝒟 (Throw P A Q)› by (auto simp add: D_Throw)
        thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
      qed
    next
      show ‹t = u @ v ⟹ u ∈ 𝒯 (Throw P A Q') ⟹ length u = Suc n ⟹
            tF u ⟹ ftF v ⟹ t ∈ 𝒟 ?lhs› for u v by (fact "*")
    qed

    show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
    proof (elim F_restriction_process⇩p⇩t⇩i⇩c⇩kE)
      assume ‹(t, X) ∈ ℱ (Throw P A Q')› ‹length t ≤ Suc n›
      from this(1) consider ‹t ∈ 𝒟 (Throw P A Q')› | ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` A = {}›
        | (failR) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
          ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ ℱ (Q' a)›
        unfolding Throw_projs by auto
      thus ‹(t, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹t ∈ 𝒟 (Throw P A Q')›
        hence ‹t ∈ 𝒟 ?rhs› by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
        with D_F div show ‹(t, X) ∈ ℱ ?lhs› by blast
      next
        assume ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` A = {}›
        hence ‹(t, X) ∈ ℱ (Throw P A Q)› by (simp add: F_Throw)
        thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩kI)
      next
        case failR
        from failR(2, 4) that have ‹t1 ≠ []›
          by (cases t1) (auto intro: initials_memI)
        with failR(1) ‹length t ≤ Suc n› nat_less_le have ‹length t2 < n› by force
        with ‹(t2, X) ∈ ℱ (Q' a)› ‹Q ↓ n = Q' ↓ n› have ‹(t2, X) ∈ ℱ (Q a)›
          by (metis F_restriction_process⇩p⇩t⇩i⇩c⇩kI restriction_fun_def
              length_less_in_F_restriction_process⇩p⇩t⇩i⇩c⇩k)
        with failR(1-4) have ‹(t, X) ∈ ℱ (Throw P A Q)› by (auto simp add: F_Throw)
        thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩kI)
      qed
    next
      show ‹t = u @ v ⟹ u ∈ 𝒯 (Throw P A Q') ⟹ length u = Suc n ⟹
            tF u ⟹ ftF v ⟹ (t, X) ∈ ℱ ?lhs› for u v
        by (simp add: "*" is_processT8)
    qed
  qed
qed


(*<*)
end
  (*>*)