Theory Synchronization_Product_Generalized_Interpretations

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, 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
 ***********************************************************************************)


chapter ‹Declensions of the Generalized Synchronization Product›

(*<*)
theory Synchronization_Product_Generalized_Interpretations
  imports Synchronization_Product_Generalized_Commutativity
    Synchronization_Product_Generalized_Associativity
    Read_Write_CSP_PTick_Laws
    Operational_Semantics_CSP_PTick_Laws
begin
  (*>*)

unbundle option_type_syntax


section ‹Interpretations›

text ‹
For practical reasons, we directly interpret locale‹Syncptick_comm_locale›.
Then, the laws of associativity will be derived
manually (instead of globally interpreting the locale locale‹Syncptick_assoc_locale›).
›

subsection ‹Classical Version›

text (in Syncptick_locale) ‹
The following interpretation is initially the reason we wanted the parameter
term‹tick_join› to be of type typ‹'r ⇒ 's ⇒ 't option› instead of
just typ‹'r ⇒ 's ⇒ 't› (we wanted the operator const‹Sync› already defined in
session‹HOL-CSP› to indeed be a particular case of the new one).
›

interpretation SyncClassic : Syncptick_comm_locale
  ‹λr s. if r = s then ⌊r⌋ else ◇›
  ‹λs r. if s = r then ⌊s⌋ else ◇› id id
  by unfold_locales (auto split: if_split_asm)

notation SyncClassic.Syncptick  (‹(_ ⟦_⟧✓Classic _)› [70, 0, 71] 70)
notation SyncClassic.Interptick (‹(_ |||✓Classic _)› [72, 73] 72)
notation SyncClassic.Parptick   (‹(_ ||✓Classic _)›  [74, 75] 74)



subsection ‹Product Type›

interpretation SyncPair : Syncptick_comm_locale
  ‹λr s. ⌊(r, s)⌋› ‹λs r. ⌊(s, r)⌋› prod.swap prod.swap
  by unfold_locales (auto split: if_split_asm)

notation SyncPair.Syncptick  (‹(_ ⟦_⟧✓Pair _)› [70, 0, 71] 70)
notation SyncPair.Interptick (‹(_ |||✓Pair _)› [72, 73] 72)
notation SyncPair.Parptick   (‹(_ ||✓Pair _)›  [74, 75] 74)



subsection ‹List Type›

subsubsection ‹Pair›

interpretation SyncPairlist : Syncptick_comm_locale
  ‹λr s. ⌊[r, s]⌋› ‹λs r. ⌊[s, r]⌋›
  ‹λrs. [rs ! Suc 0, rs ! 0]› ‹λrs. [rs ! Suc 0, rs ! 0]›
  by unfold_locales (auto intro: inj_onI) 

notation SyncPairlist.Syncptick  (‹(_ ⟦_⟧✓Pairlist _)› [70, 0, 71] 70)
notation SyncPairlist.Interptick (‹(_ |||✓Pairlist _)› [72, 73] 72)
notation SyncPairlist.Parptick   (‹(_ ||✓Pairlist _)›  [74, 75] 74)



subsubsection ‹Right List›

text ‹
Here, we want to have one process of type typ‹('a, 'r) processptick› on the left hand side,
and one of type typ‹('a, 'r list) processptick› on the right hand side.
›

interpretation SyncRlist : Syncptick_comm_locale
  ‹λr s. ⌊r # s⌋› ‹λs r. ⌊s @ [r]⌋›
  ‹rotate1› ‹λrs. if rs = [] then [] else last rs # butlast rs›
  ― ‹term‹λrs. last rs # butlast rs› is not injective.›
  by unfold_locales (auto intro: inj_onI) 

notation SyncRlist.Syncptick  (‹(_ ⟦_⟧✓Rlist _)› [70, 0, 71] 70)
notation SyncRlist.Interptick (‹(_ |||✓Rlist _)› [72, 73] 72)
notation SyncRlist.Parptick   (‹(_ ||✓Rlist _)›  [74, 75] 74)



subsubsection ‹Left List›

text ‹
Here, we want to have one process of type typ‹('a, 'r list) processptick›
on the left hand side, and one of type typ‹('a, 'r) processptick› on the right hand side.
There is no need to do a new interpretation, the operator we are looking for is actually
the symmetric of the one we defined just above.
›

notation SyncRlist.Syncptick_comm_locale_sym.Syncptick  (‹(_ ⟦_⟧✓Llist _)› [70, 0, 71] 70)
notation SyncRlist.Syncptick_comm_locale_sym.Interptick (‹(_ |||✓Llist _)› [72, 73] 72)
notation SyncRlist.Syncptick_comm_locale_sym.Parptick   (‹(_ ||✓Llist _)›  [74, 75] 74)



subsubsection ‹Arbitrary Lists›

text ‹
We believed for a long time that it was not possible to handle the case
where both processes have their ticks of type typ‹'r list›.
Indeed the concatenation on the lists is not injective, resulting in
the impossibility of interpreting locale‹Syncptick_locale›.
But it turns out that by adding some control on the length of the lists,
we actually can!
›

paragraph ‹Control on one side›

context fixes lenL :: nat begin

global_interpretation SyncListslenL : Syncptick_comm_locale 
  ‹λr s. if length r = lenL then ⌊r @ s⌋ else ◇›
  ‹λs r. if length r = lenL then ⌊s @ r⌋ else ◇›
  ‹λrs. drop lenL rs @ take lenL rs›
  ‹λrs. rev (take lenL (rev rs)) @ rev (drop lenL (rev rs))›
  by unfold_locales (auto split: if_split_asm)

end

abbreviation SyncListslenL_syntax ::
  ‹[('a, 'r list) processptick, nat, 'a set, ('a, 'r list) processptick]
   ⇒ ('a, 'r list) processptick› (‹(_ ⇘_⇙(⟦_⟧✓ListslenL) _)› [70, 0, 0, 71] 70)
  where ‹P ⇘lenL⇙⟦A⟧✓ListslenL Q ≡ SyncListslenL.Syncptick lenL P A Q›

abbreviation InterListslenL_syntax ::
  ‹[('a, 'r list) processptick, nat, ('a, 'r list) processptick]
   ⇒ ('a, 'r list) processptick› (‹(_ ⇘_⇙(|||✓ListslenL) _)› [72, 0, 73] 72)
  where ‹P ⇘lenL⇙|||✓ListslenL Q ≡ SyncListslenL.Interptick lenL P Q›

abbreviation ParListslenL_syntax ::
  ‹[('a, 'r list) processptick, nat, ('a, 'r list) processptick]
   ⇒ ('a, 'r list) processptick› (‹(_ ⇘_⇙(||✓ListslenL) _)› [74, 0, 75] 75)
  where ‹P ⇘lenL⇙||✓ListslenL Q ≡ SyncListslenL.Parptick lenL P Q›


text ‹
The control is done on the left process, so with the symmetric version
of this operator we control the ticks length of the right one.
›

abbreviation SyncListslenR_syntax ::
  ‹[('a, 'r list) processptick, nat, 'a set, ('a, 'r list) processptick]
   ⇒ ('a, 'r list) processptick› (‹(_ ⇘_⇙(⟦_⟧✓ListslenR) _)› [70, 0, 0, 71] 70)
  where ‹P ⇘lenL⇙⟦A⟧✓ListslenR Q ≡ SyncListslenL.Syncptick_comm_locale_sym.Syncptick lenL P A Q›

abbreviation InterListslenR_syntax ::
  ‹[('a, 'r list) processptick, nat, ('a, 'r list) processptick]
   ⇒ ('a, 'r list) processptick› (‹(_ ⇘_⇙(|||✓ListslenR) _)› [72, 0, 73] 72)
  where ‹P ⇘lenL⇙|||✓ListslenR Q ≡ SyncListslenL.Syncptick_comm_locale_sym.Interptick lenL P Q›

abbreviation ParListslenR_syntax ::
  ‹[('a, 'r list) processptick, nat, ('a, 'r list) processptick]
   ⇒ ('a, 'r list) processptick› (‹(_ ⇘_⇙(||✓ListslenR) _)› [74, 0, 75] 75)
  where ‹P ⇘lenL⇙||✓ListslenR Q ≡ SyncListslenL.Syncptick_locale_sym.Parptick lenL P Q›



paragraph ‹Control on both sides›

context fixes lenL :: nat and lenR :: nat begin

global_interpretation SyncLists : Syncptick_comm_locale 
  ‹λr s. if length r = lenL ∧ length s = lenR then ⌊r @ s⌋ else ◇›
  ‹λs r. if length s = lenR ∧ length r = lenL then ⌊s @ r⌋ else ◇›
  ‹λrs. drop lenL rs @ take lenL rs›
  ‹λrs. drop lenR rs @ take lenR rs›
  by unfold_locales (auto split: if_split_asm)

end


abbreviation SyncLists_syntax ::
  ‹[('a, 'r list) processptick, nat, 'a set, nat, ('a, 'r list) processptick]
   ⇒ ('a, 'r list) processptick› (‹(_ ⇘_⇙(⟦_⟧✓)⇘_⇙ _)› [70, 0, 0, 0, 71] 70)
  where ‹P ⇘lenL⇙⟦A⟧✓⇘lenR⇙ Q ≡ SyncLists.Syncptick lenL lenR P A Q›

abbreviation InterLists_syntax ::
  ‹[('a, 'r list) processptick, nat, nat, ('a, 'r list) processptick]
   ⇒ ('a, 'r list) processptick› (‹(_ ⇘_⇙(|||✓)⇘_⇙ _)› [72, 0, 0, 73] 72)
  where ‹P ⇘lenL⇙|||✓⇘lenR⇙ Q ≡ SyncLists.Interptick lenL lenR P Q›

abbreviation ParLists_syntax ::
  ‹[('a, 'r list) processptick, nat, nat, ('a, 'r list) processptick]
   ⇒ ('a, 'r list) processptick› (‹(_ ⇘_⇙(||✓)⇘_⇙ _)› [74, 0, 0, 75] 75)
  where ‹P ⇘lenL⇙||✓⇘lenR⇙ Q ≡ SyncLists.Parptick lenL lenR P Q›



section ‹Associativities›

subsection ‹Classical Version›

lemma SyncClassic_assoc :
  ‹P ⟦S⟧✓Classic (Q ⟦S⟧✓Classic R) = P ⟦S⟧✓Classic Q ⟦S⟧✓Classic R›
proof -
  let ?f = ‹λr s. if r = s then ⌊r⌋ else ◇›
  interpret * : Syncptick_assoc_locale ?f ?f ?f ?f id id
    by (unfold_locales) (auto split: if_split_asm)
  show ?thesis by (fact "*.Syncptick_assoc"[simplified Renaming_id])
qed



subsection ‹Product Type›

lemma SyncPair_assoc :
  ‹P ⟦S⟧✓Pair (Q ⟦S⟧✓Pair R) = RenamingTick (P ⟦S⟧✓Pair Q ⟦S⟧✓Pair R) (λ((r, s), t). (r, s, t))›
proof -
  interpret * : Syncptick_assoc_locale ‹λr s. ⌊(r, s)⌋› ‹λr s. ⌊(r, s)⌋› ‹λr s. ⌊(r, s)⌋›
    ‹λr s. ⌊(r, s)⌋› ‹λ((r, s), t). (r, s, t)› ‹λ(r, s, t). ((r, s), t)›
    by unfold_locales auto
  show ?thesis by (fact "*.Syncptick_assoc")
qed



subsection ‹List Type›

lemma SyncRlist_SyncPairlist_assoc :
  ‹P ⟦S⟧✓Rlist (Q ⟦S⟧✓Pairlist R) = (P ⟦S⟧✓Pairlist Q) ⟦S⟧✓Llist R›
proof -
  interpret * : Syncptick_assoc_locale ‹λr s. ⌊[r, s]⌋› ‹λr s. ⌊r @ [s]⌋›
    ‹λr s. ⌊r # s⌋› ‹λr s. ⌊[r, s]⌋› id id
    by unfold_locales auto
  show ?thesis by (fact "*.Syncptick_assoc"[unfolded Renaming_id])
qed


lemma SyncRlist_SyncLlist_assoc :
  ‹P ⟦S⟧✓Rlist (Q ⟦S⟧✓Llist R) = (P ⟦S⟧✓Rlist Q) ⟦S⟧✓Llist R›
proof -
  interpret * : Syncptick_assoc_locale ‹λr s. ⌊r # s⌋› ‹λr s. ⌊r @ [s]⌋›
    ‹λr s. ⌊r # s⌋› ‹λr s. ⌊r @ [s]⌋› id id
    by unfold_locales auto
  show ?thesis by (fact "*.Syncptick_assoc"[unfolded Renaming_id])
qed


lemma SyncRlist_SyncListslenL_assoc :
  ‹P ⟦S⟧✓Rlist (Q ⇘lenQ⇙⟦S⟧✓ListslenL R) = (P ⟦S⟧✓Rlist Q) ⇘Suc lenQ⇙⟦S⟧✓ListslenL R›
proof -
  interpret * : Syncptick_assoc_locale
    ‹λr s. ⌊r # s⌋›
    ‹λr s. if length r = Suc lenQ then ⌊r @ s⌋ else ◇›
    ‹λr s. ⌊r # s⌋›
    ‹λr s. if length r = lenQ then ⌊r @ s⌋ else ◇› id id
    by unfold_locales (auto split: if_split_asm)
  show ?thesis by (fact "*.Syncptick_assoc"[unfolded Renaming_id])
qed

lemma SyncListslenR_SyncLlist_assoc :
  ‹P ⇘Suc lenQ⇙⟦S⟧✓ListslenR (Q ⟦S⟧✓Llist R) = (P ⇘lenQ⇙⟦S⟧✓ListslenR Q) ⟦S⟧✓Llist R›
proof -
  interpret * : Syncptick_assoc_locale
    ‹λr s. if length s = lenQ then ⌊r @ s⌋ else ◇›
    ‹λr s. ⌊r @ [s]⌋›
    ‹λr s. if length s = Suc lenQ then ⌊r @ s⌋ else ◇›
    ‹λr s. ⌊r @ [s]⌋› id id
    by unfold_locales (auto split: if_split_asm)
  show ?thesis by (fact "*.Syncptick_assoc"[unfolded Renaming_id])
qed


lemma SyncLists_assoc :
  ‹P ⇘lenP⇙⟦S⟧✓⇘lenQ + lenR⇙ (Q ⇘lenQ⇙⟦S⟧✓⇘lenR⇙ R) =
   P ⇘lenP⇙⟦S⟧✓⇘lenQ⇙ Q ⇘lenP + lenQ⇙⟦S⟧✓⇘lenR⇙ R›
proof -
  interpret * : Syncptick_assoc_locale
    ‹λr s. if length r = lenP ∧ length s = lenQ then ⌊r @ s⌋ else ◇›
    ‹λr s. if length r = lenP + lenQ ∧ length s = lenR then ⌊r @ s⌋ else ◇›
    ‹λr s. if length r = lenP ∧ length s = lenQ + lenR then ⌊r @ s⌋ else ◇›
    ‹λr s. if length r = lenQ ∧ length s = lenR then ⌊r @ s⌋ else ◇› id id
    by unfold_locales (auto split: if_split_asm)
  show ?thesis by (fact "*.Syncptick_assoc"[unfolded Renaming_id])
qed


lemma SyncRlist_SyncRlist_assoc :
  ‹P ⟦S⟧✓Rlist (Q ⟦S⟧✓Rlist R) = (P ⟦S⟧✓Pairlist Q) ⇘Suc (Suc 0)⇙⟦S⟧✓ListslenL R›
proof -
  interpret * : Syncptick_assoc_locale
    ‹λr s. ⌊[r, s]⌋›
    ‹λr s. if length r = Suc (Suc 0) then ⌊r @ s⌋ else ◇›
    ‹λr s. ⌊r # s⌋›
    ‹λr s. ⌊r # s⌋› id id
    by unfold_locales (auto split: if_split_asm)
  show ?thesis by (fact "*.Syncptick_assoc"[unfolded Renaming_id])
qed

lemma SyncListslenR_SyncPairlist_assoc :
  ‹P ⇘Suc (Suc 0)⇙⟦S⟧✓ListslenR (Q ⟦S⟧✓Pairlist R) = (P ⟦S⟧✓Llist Q) ⟦S⟧✓Llist R›
proof -
  interpret * : Syncptick_assoc_locale
    ‹λr s. ⌊r @ [s]⌋›
    ‹λr s. ⌊r @ [s]⌋›
    ‹λr s. if length s = Suc (Suc 0) then ⌊r @ s⌋ else ◇›
    ‹λr s. ⌊[r, s]⌋› id id
    by unfold_locales (auto split: if_split_asm)
  show ?thesis by (fact "*.Syncptick_assoc"[unfolded Renaming_id])
qed



section ‹Properties›

subsection ‹Actual Generalization›

text ‹
We can actually recover the classical synchronization product defined in
session session‹HOL-CSP› as a particular case of our generalization.
›

theorem SyncClassic_is_Sync : ‹P ⟦A⟧✓Classic Q = P ⟦A⟧ Q›
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 (P ⟦A⟧ Q) ⟹ t ∈ 𝒟 (P ⟦A⟧✓Classic Q)› for t
    by (simp add: D_Sync SyncClassic.D_Syncptick'
        flip: setinterleaves_is_setinterleavesptick)
      (metis setinterleaving_sym)
next
  show ‹t ∈ 𝒟 (P ⟦A⟧✓Classic Q) ⟹ t ∈ 𝒟 (P ⟦A⟧ Q)› for t
    by (simp add: D_Sync SyncClassic.D_Syncptick
        flip: setinterleaves_is_setinterleavesptick)
      (metis setinterleaving_sym)
next
  fix t X assume ‹(t, X) ∈ ℱ (P ⟦A⟧ Q)› ‹t ∉ 𝒟 (P ⟦A⟧ Q)›
  then obtain t_P t_Q X_P X_Q
    where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
      ‹t setinterleaves ((t_P, t_Q), range tick ∪ ev ` A)›
      ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q›
    unfolding Sync_projs by blast
  from "*"(4) have ‹X ⊆ super_ref_Syncptick (λr s. if r = s then ⌊r⌋ else ◇) X_P A X_Q›
    by (auto simp add: super_ref_Syncptick_def subset_iff)
      (metis eventptick.exhaust)
  with "*"(1-3) show ‹(t, X) ∈ ℱ (P ⟦A⟧✓Classic Q)›
    by (auto simp add: SyncClassic.F_Syncptick setinterleaves_is_setinterleavesptick)
next
  fix t X assume ‹(t, X) ∈ ℱ (P ⟦A⟧✓Classic Q)› ‹t ∉ 𝒟 (P ⟦A⟧✓Classic Q)›
  then obtain t_P t_Q X_P X_Q
    where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
      ‹t setinterleaves✓⇘λr s. if r = s then ⌊r⌋ else ◇⇙ ((t_P, t_Q), A)›
      ‹X ⊆ super_ref_Syncptick (λr s. if r = s then ⌊r⌋ else ◇) X_P A X_Q›
    unfolding SyncClassic.Syncptick_projs by blast
  from "*"(1-3) have ‹(t, (X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q) ∈ ℱ (P ⟦A⟧ Q)›
    by (simp add: F_Sync setinterleaves_is_setinterleavesptick) blast
  moreover from "*"(4) have ‹X ⊆ (X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q›
    by (auto simp add: super_ref_Syncptick_def subset_iff split: if_split_asm)
  ultimately show ‹(t, X) ∈ ℱ (P ⟦A⟧ Q)› by (meson is_processT4)
qed



subsection ‹Other Properties›

lemma ‹SyncLists.Syncptick_locale_sym.Syncptick lenL lenR Q A P = P ⇘lenL⇙⟦A⟧✓⇘lenR⇙ Q›
  by (simp add: SyncLists.Syncptick_locale_sym.Syncptick_sym)


corollary TickSwap_SyncPair [simp] : ‹TickSwap (P ⟦S⟧✓Pair Q) = Q ⟦S⟧✓Pair P›
  by (simp add: SyncPair.Syncptick_commute TickSwap_is_Renaming)

lemma TickSwap_is_SyncPair_iff [simp] :
  ‹TickSwap P = Q ⟦S⟧✓Pair R ⟷ P = R ⟦S⟧✓Pair Q›
  by (simp add: TickSwap_eq_iff_eq_TickSwap)

corollary SyncClassic_commute : ‹P ⟦S⟧✓Classic Q = Q ⟦S⟧✓Classic P›
  by (fact SyncClassic.Syncptick_commute[simplified])


lemma ‹RenamingTick (P ⇘lenL⇙⟦S⟧✓⇘lenR⇙ Q) (λr_s. drop lenL r_s @ take lenL r_s) =
       Q ⇘lenR⇙⟦S⟧✓⇘lenL⇙ P›
  by (fact SyncLists.Syncptick_commute)



section ‹Ticks Length and Conversions›

text ‹
Through const‹RenamingTick›, conversions can be established between the interpretations.
For this, we sometimes need an assumption about the length of the ticks.
›

subsection ‹Ticks Length›

subsubsection ‹Definition and first Properties›

definition is_ticks_length ::
  ‹nat ⇒ ('a, 'r list) processptick ⇒ bool› (‹(length✓)⇘_⇙('(_'))›)
  where ‹length✓⇘n⇙(P) ≡ ∀rs ∈ ✓s(P). length rs = n›

text ‹
We might imagine term‹ ∀rs ∈ ✓s(P). length rs = n› instead.
But when the process term‹P› has divergences, the predicate would not hold.
Additionally, we only need the control about traces that are not divergences.
›

lemma is_ticks_lengthI : ‹(⋀rs. rs ∈ ✓s(P) ⟹ length rs = n) ⟹ length✓⇘n⇙(P)›
  by (simp add: is_ticks_length_def)

lemma is_ticks_lengthD : ‹length✓⇘n⇙(P) ⟹ rs ∈ ✓s(P) ⟹ length rs = n›
  by (simp add: is_ticks_length_def)


lemma is_ticks_length_unique :
  ―‹Not suitable for simplifier.›
  ‹length✓⇘n⇙(P) ⟷ ✓s(P) = {} ∨ (∀m. length✓⇘m⇙(P) ⟷ m = n)›
  by (auto simp add: is_ticks_length_def)

lemma empty_strict_ticks_of_imp_is_ticks_length :
  ‹✓s(P) = {} ⟹ length✓⇘n⇙(P)›
  using is_ticks_length_unique by blast

lemma nonempty_strict_ticks_of_imp_is_ticks_length_unique :
  ‹✓s(P) ≠ {} ⟹ length✓⇘n⇙(P) ⟹ length✓⇘m⇙(P) ⟹ m = n› 
  using is_ticks_length_unique by blast



subsubsection ‹Behaviour›

named_theorems is_ticks_length_simp
named_theorems is_ticks_length_intro

paragraph ‹Constant Processes›

lemma is_ticks_length_STOP [is_ticks_length_simp] :
  ‹length✓⇘n⇙(STOP)› by (simp add: empty_strict_ticks_of_imp_is_ticks_length)

lemma is_ticks_length_BOT [is_ticks_length_simp] :
  ‹length✓⇘n⇙(⊥)› by (simp add: empty_strict_ticks_of_imp_is_ticks_length)

lemma is_ticks_length_SKIP_iff [is_ticks_length_simp] :
  ‹length✓⇘n⇙(SKIP rs) ⟷ length rs = n›
  by (simp add: is_ticks_length_def)

lemma is_ticks_length_SKIPS_iff [is_ticks_length_simp] :
  ‹length✓⇘n⇙(SKIPS R) ⟷ (∀rs ∈ R. length rs = n)›
  by (simp add: is_ticks_length_def strict_ticks_of_def SKIPS_projs)



paragraph ‹Binary (or less) Operators›

lemma is_ticks_length_Ndet [is_ticks_length_intro] :
  ‹length✓⇘n⇙(P) ⟹ length✓⇘n⇙(Q) ⟹ length✓⇘n⇙(P ⊓ Q)›
  by (simp add: is_ticks_length_def)
    (meson Un_iff strict_ticks_of_Ndet_subset subset_iff)

lemma is_ticks_length_Det [is_ticks_length_intro] :
  ‹length✓⇘n⇙(P) ⟹ length✓⇘n⇙(Q) ⟹ length✓⇘n⇙(P □ Q)›
  by (simp add: is_ticks_length_def)
    (meson Un_iff strict_ticks_of_Det_subset subset_iff)

lemma is_ticks_length_Sliding [is_ticks_length_intro] :
  ‹length✓⇘n⇙(P) ⟹ length✓⇘n⇙(Q) ⟹ length✓⇘n⇙(P ⊳ Q)›
  by (simp add: is_ticks_length_def)                
    (meson Un_iff strict_ticks_of_Sliding_subset subset_iff)


lemma is_ticks_length_Sync [is_ticks_length_intro] :
  ‹length✓⇘n⇙(P) ⟹ length✓⇘n⇙(Q) ⟹ length✓⇘n⇙(P ⟦S⟧ Q)›
  by (simp add: is_ticks_length_def)
    (meson Int_iff strict_ticks_of_Sync_subset subset_iff)


lemma is_ticks_length_Seq [is_ticks_length_intro] :
  ‹non_terminating P ∨ length✓⇘n⇙(Q) ⟹ length✓⇘n⇙(P ; Q)›
proof (elim disjE)
  show ‹non_terminating P ⟹ length✓⇘n⇙(P ; Q)›
    by (metis is_ticks_length_def non_terminating_Seq non_terminating_is_right
        non_tickFree_tick strict_ticks_of_memE tickFree_append_iff)
next
  from strict_ticks_of_Seq_subset[of P Q]
  show ‹length✓⇘n⇙(Q) ⟹ length✓⇘n⇙(P ; Q)›
    by (auto simp add: is_ticks_length_def split: if_split_asm)
qed


lemma is_ticks_length_Hiding [is_ticks_length_intro] :
  ‹length✓⇘n⇙(P \ S)› if ‹length✓⇘n⇙(P)›
proof (rule is_ticks_lengthI)
  fix rs assume ‹rs ∈ ✓s(P \ S)›
  then obtain t t' where ‹t = t' @ [✓(rs)]› ‹t ∈ 𝒯 (P \ S)› ‹t ∉ 𝒟 (P \ S)›
    by (metis is_processT9 strict_ticks_of_memE)
  from this(2, 3) obtain u where ‹t = trace_hide u (ev ` S)› ‹u ∈ 𝒯 P›
    unfolding T_Hiding D_Hiding using F_T by fast
  from this(1) this(2)[THEN T_imp_front_tickFree] obtain u' where ‹u = u' @ [✓(rs)]›
    by (cases u rule: rev_cases, simp_all add: ‹t = t' @ [✓(rs)]› split: if_split_asm)
      (metis Hiding_tickFree front_tickFree_nonempty_append_imp list.distinct(1)
        non_tickFree_tick tickFree_append_iff)
  from ‹t ∉ 𝒟 (P \ S)› mem_D_imp_mem_D_Hiding[of u P S]
  have ‹u ∉ 𝒟 P› unfolding ‹t = trace_hide u (ev ` S)› by blast
  with ‹u ∈ 𝒯 P› ‹u = u' @ [✓(rs)]› have ‹rs ∈ ✓s(P)›
    by (simp add: strict_ticks_of_memI)
  with that show ‹length rs = n› by (simp add: is_ticks_lengthD)
qed


lemma is_ticks_length_Interrupt [is_ticks_length_intro] :
  ‹length✓⇘n⇙(P) ⟹ length✓⇘n⇙(Q) ⟹ length✓⇘n⇙(P △ Q)›
  by (simp add: is_ticks_length_def)
    (meson Un_iff strict_ticks_of_Interrupt_subset subsetD)


― ‹Missing lemma from session‹HOL-CSPM››
lemma strict_ticks_Throw_subset :
  ‹✓s(P Θ a∈A. Q a) ⊆ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))›
proof (rule subsetI)
  fix r assume ‹r ∈ ✓s(P Θ a∈A. Q a)›
  then obtain t where ‹t @ [✓(r)] ∈ 𝒯 (P Θ a∈A. Q a)› ‹t @ [✓(r)] ∉ 𝒟 (P Θ a∈A. Q a)›
    by (meson is_processT9 strict_ticks_of_memE)
  then consider ‹t @ [✓(r)] ∈ 𝒯 P› ‹t @ [✓(r)] ∉ 𝒟 P›
    | t1 a t2 where ‹t @ [✓(r)] = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
      ‹a ∈ A› ‹t2 ∈ 𝒯 (Q a)› ‹t2 ∉ 𝒟 (Q a)›
    by (simp add: Throw_projs)
      (metis (no_types, lifting) append_T_imp_tickFree
        front_tickFree_single is_processT9 not_Cons_self2)
  thus ‹r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))›
  proof cases
    show ‹t @ [✓(r)] ∈ 𝒯 P ⟹ t @ [✓(r)] ∉ 𝒟 P ⟹ r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))›
      by (simp add: strict_ticks_of_memI)
  next
    show ‹⟦t @ [✓(r)] = t1 @ ev a # t2; t1 @ [ev a] ∈ 𝒯 P; a ∈ A; t2 ∈ 𝒯 (Q a); t2 ∉ 𝒟 (Q a)⟧
           ⟹ r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))› for t1 a t2
      by (cases t2 rule: rev_cases, simp_all)
        (meson IntI events_of_memI in_set_conv_decomp strict_ticks_of_memI)
  qed
qed

lemma is_ticks_length_Throw [is_ticks_length_intro] :
  ‹length✓⇘n⇙(P Θ a ∈ A. Q a)›
  if ‹length✓⇘n⇙(P)› ‹⋀a. a ∈ α(P) ⟹ length✓⇘n⇙(Q a)›
proof -
  from that have ‹∀rs∈✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a)). length rs = n›
    by (auto simp add: is_ticks_length_def)
  with strict_ticks_Throw_subset show ‹length✓⇘n⇙(P Θ a ∈ A. Q a)›
    unfolding is_ticks_length_def by fast
qed

lemma is_ticks_length_Renaming [is_ticks_length_intro] :
  ‹length✓⇘n⇙(Renaming P f g) › if ‹⋀r. r ∈ ✓s(P) ⟹ length (g r) = n›
proof (rule is_ticks_lengthI)
  fix rs assume ‹rs ∈ ✓s(Renaming P f g)›
  then obtain t where ‹t @ [✓(rs)] ∈ 𝒯 (Renaming P f g)›
    ‹t @ [✓(rs)] ∉ 𝒟 (Renaming P f g)›
    by (meson is_processT9 strict_ticks_of_memE)
  then obtain u where * : ‹t @ [✓(rs)] = map (map_eventptick f g) u› and ‹u ∈ 𝒯 P›
    by (auto simp add: Renaming_projs)
  from this(1) ‹u ∈ 𝒯 P› append_T_imp_tickFree obtain u' r
    where ‹rs = g r› ‹u = u' @ [✓(r)]› ‹tF u'›
    by (cases u rule: rev_cases) (auto simp add: tick_eq_map_eventptick_iff)
  from "*" ‹t @ [✓(rs)] ∉ 𝒟 (Renaming P f g)› this(2, 3) front_tickFree_Cons_iff
  have ‹u' ∉ 𝒟 P› by (auto simp add: D_Renaming)
  moreover from ‹u ∈ 𝒯 P› have ‹u' @ [✓(r)] ∈ 𝒯 P›
    by (simp add: ‹u = u' @ [✓(r)]›)
  ultimately have ‹r ∈ ✓s(P)› by (meson is_processT9 strict_ticks_of_memI)
  with that have ‹length (g r) = n› by blast
  thus ‹length rs = n› by (simp add: ‹rs = g r›)
qed



paragraph ‹Architectural Operators›

lemma is_ticks_length_GlobalNdet [is_ticks_length_intro] :
  ‹(⋀a. a ∈ A ⟹ length✓⇘n⇙(P a)) ⟹ length✓⇘n⇙(⊓a ∈ A. P a)›
  by (simp add: is_ticks_length_def)
    (metis (no_types, lifting) UN_E strict_ticks_of_GlobalNdet_subset subsetD)

lemma is_ticks_length_GlobalDet [is_ticks_length_intro] :
  ‹(⋀a. a ∈ A ⟹ length✓⇘n⇙(P a)) ⟹ length✓⇘n⇙(□a ∈ A. P a)›
  by (simp add: is_ticks_length_def)
    (metis (no_types, lifting) UN_E strict_ticks_of_GlobalDet_subset subsetD)

lemma is_ticks_length_MultiSync [is_ticks_length_intro] :
  ‹(⋀m. m ∈ set_mset M ⟹ length✓⇘n⇙(P m)) ⟹ length✓⇘n⇙(⟦S⟧ m ∈# M. P m)›
  by (induct M rule: induct_subset_mset_empty_single)
    (simp_all add: is_ticks_length_STOP is_ticks_length_Sync)

lemma is_ticks_length_MultiSeq [is_ticks_length_intro] :
  ‹L ≠ [] ⟹ length✓⇘n⇙(P (last L)) ⟹ length✓⇘n⇙(SEQ l ∈@ L. P l)›
  by (induct L rule: rev_induct)
    (simp_all add: is_ticks_length_Seq)


paragraph ‹Communications›

lemma is_ticks_length_write0_iff [is_ticks_length_simp] :
  ‹length✓⇘n⇙(e → P) ⟷ length✓⇘n⇙(P)›
  by (simp add: is_ticks_length_def strict_ticks_of_write0)

lemma is_ticks_length_write_iff [is_ticks_length_simp] :
  ‹length✓⇘n⇙(c!e → P) ⟷ length✓⇘n⇙(P)›
  by (simp add: is_ticks_length_def strict_ticks_of_write)

lemma is_ticks_length_Mprefix_iff [is_ticks_length_simp] :
  ‹length✓⇘n⇙(□a ∈ A → P a) = (∀a ∈ A. length✓⇘n⇙(P a))› 
  by (auto simp add: is_ticks_length_def strict_ticks_of_Mprefix)

lemma is_ticks_length_read_iff [is_ticks_length_simp] :
  ‹length✓⇘n⇙(c?a∈A → P a) = (∀b ∈ c ` A. length✓⇘n⇙(P (inv_into A c b)))›
  by (simp add: read_def is_ticks_length_Mprefix_iff)

corollary ‹inj_on c A ⟹ length✓⇘n⇙(c?a∈A → P a) = (∀a ∈ A. length✓⇘n⇙(P a))›
  by (simp add: is_ticks_length_read_iff)

lemma is_ticks_length_Mndetprefix_iff [is_ticks_length_simp] :
  ‹length✓⇘n⇙(⊓a ∈ A → P a) = (∀a ∈ A. length✓⇘n⇙(P a))› 
  by (auto simp add: is_ticks_length_def strict_ticks_of_Mndetprefix)

lemma is_ticks_length_ndet_write_iff [is_ticks_length_simp] :
  ‹length✓⇘n⇙(c!!a∈A → P a) = (∀b ∈ c ` A. length✓⇘n⇙(P (inv_into A c b)))›
  by (simp add: ndet_write_def is_ticks_length_Mndetprefix_iff)

corollary ‹inj_on c A ⟹ length✓⇘n⇙(c!!a∈A → P a) = (∀a ∈ A. length✓⇘n⇙(P a))›
  by (simp add: is_ticks_length_ndet_write_iff)



paragraph ‹Generalizations›

lemma strict_ticks_of_Seqptick_subset : ‹✓s(P ;✓ Q) ⊆ ⋃ {✓s(Q r) |r. r ∈ ✓s(P)}›
  by (auto simp add: Seqptick_projs append_eq_map_conv elim!: strict_ticks_of_memE)
    (metis tickFree_Nil non_tickFree_tick tickFree_map_ev_comp
           front_tickFree_charn tickFree_append_iff tickFree_append_iff
           last_snoc[of ‹map (ev ∘ of_ev) _ @ _›] last_snoc[of _ ‹✓(_)›]
           butlast_snoc[of ‹map (ev ∘ of_ev) _ @ _›] butlast_snoc[of _ ‹✓(_)›]
           append.assoc[of ‹map (ev ∘ of_ev) _› _ ‹[_]›] tickFree_imp_front_tickFree
           T_imp_front_tickFree is_processT9 strict_ticks_of_memI,
      metis butlast_append butlast_snoc front_tickFree_iff_tickFree_butlast non_tickFree_tick
            tickFree_append_iff tickFree_imp_front_tickFree tickFree_map_ev_comp)


lemma non_terminating_Seqptick :
  ‹P ;✓ Q = RenamingTick P g› if ‹non_terminating P›
proof -
  from ‹non_terminating P› have £ : ‹𝒟 P = {}› ‹t @ [✓(r)] ∉ 𝒯 P› for t r
    by (force simp add: non_terminating_is_right nonterminating_implies_div_free)+
  show ‹P ;✓ Q = RenamingTick P g›
  proof (rule Process_eq_optimizedI)
    show ‹t ∈ 𝒟 (P ;✓ Q) ⟹ t ∈ 𝒟 (RenamingTick P g)›
      and ‹t ∈ 𝒟 (RenamingTick P g) ⟹ t ∈ 𝒟 (P ;✓ Q)› for t
      by (simp_all add: Seqptick_projs Renaming_projs "£")
  next
    fix t X assume ‹(t, X) ∈ ℱ (P ;✓ Q)›
    then obtain t' where * : ‹t = map (ev ∘ of_ev) t'›
      ‹(t', ref_Seqptick X) ∈ ℱ P› ‹tF t'›
      by (auto simp add: Seqptick_projs Renaming_projs "£")
    have $ : ‹t = map (map_eventptick id g) t'›
      by (simp add: "*"(1, 3) tickFree_map_map_eventptick_is)
    have $$ : ‹map_eventptick id g -` X ⊆ ref_Seqptick X›
      by (simp add: subset_iff ref_Seqptick_def image_iff)
        (metis Int_iff eventptick.exhaust eventptick.sel(1) eventptick.simps(9) id_apply rangeI)
    show ‹(t, X) ∈ ℱ (RenamingTick P g)›
      by (simp add: Renaming_projs) (metis "$" "$$" "*"(2) is_processT4)
  next
    fix t X assume ‹(t, X) ∈ ℱ (RenamingTick P g)›
    then obtain t' where * : ‹t = map (map_eventptick id g) t'›
      ‹(t', map_eventptick id g -` X) ∈ ℱ P›
      by (auto simp add: Renaming_projs "£")
    from "*"(2) F_T non_terminating_is_right ‹non_terminating P› have ‹tF t'› by blast
    have ‹(t', map_eventptick id g -` X ∪ range tick) ∈ ℱ P›
      by (rule is_processT5[OF "*"(2)]) (use "£"(2) F_T in blast)
    moreover have ‹ref_Seqptick X ⊆ map_eventptick id g -` X ∪ range tick›
      by (auto simp add: ref_Seqptick_def)
    ultimately have ‹(t', ref_Seqptick X) ∈ ℱ P›
      by (metis is_processT4)
    moreover have ‹t = map (ev ∘ of_ev) t'›
      by (simp add: "*"(1) ‹tF t'› tickFree_map_map_eventptick_is)
    ultimately show ‹(t, X) ∈ ℱ (P ;✓ Q)›
      by (auto simp add: Seqptick_projs ‹tF t'›)
  qed
qed



lemma is_ticks_length_Seqptick [is_ticks_length_intro] :
  ‹non_terminating P ∨ (∀r∈✓s(P). length✓⇘n⇙(Q r)) ⟹ length✓⇘n⇙(P ;✓ Q)›
proof (elim disjE)
  assume ‹non_terminating P›
  hence ‹✓s(P) = {}›
    by (metis (full_types) non_terminating_Seq strict_ticks_of_BOT
                           strict_ticks_of_Seq_subset subset_empty)
  show ‹non_terminating P ⟹ length✓⇘n⇙(P ;✓ Q)›
    by (subst non_terminating_Seqptick, assumption)
      (rule is_ticks_length_Renaming, simp add: is_ticks_length_Renaming ‹✓s(P) = {}›)
next
  from strict_ticks_of_Seqptick_subset[of P Q]
  show ‹∀r∈✓s(P). length✓⇘n⇙(Q r) ⟹ length✓⇘n⇙(P ;✓ Q)›
    by (auto simp add: is_ticks_length_def)
qed



lemma is_ticks_length_Syncptick :
  ‹length✓⇘n⇙(Syncptick_locale.Syncptick tick_join P A Q)›
  ― ‹We cannot work directly inside the locale since in this context
      the types of ticks typ‹'t› cannot be set to typ‹'r list›.›
  if ‹Syncptick_locale tick_join›
    and ‹⋀r s. r ∈ ✓s(P) ⟹ s ∈ ✓s(Q) ⟹
       case tick_join r s of ◇ ⇒ True | ⌊r_s⌋ ⇒ length r_s = n›
proof -
  interpret Syncptick_locale tick_join
    by (fact ‹Syncptick_locale tick_join›)
  show ‹length✓⇘n⇙(P ⟦A⟧✓ Q)›
  proof (rule is_ticks_lengthI)
    fix rs assume ‹rs ∈ ✓s(P ⟦A⟧✓ Q)›
    then obtain t where ‹t @ [✓(rs)] ∈ 𝒯 (P ⟦A⟧✓ Q)› ‹t @ [✓(rs)] ∉ 𝒟 (P ⟦A⟧✓ Q)›
      by (meson is_processT9 strict_ticks_of_memE)
    then obtain t_P t_Q where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
      and "*" : ‹t @ [✓(rs)] setinterleaves✓⇘tick_join⇙ ((t_P, t_Q), A)›
      unfolding Syncptick_projs by blast
    with ‹t @ [✓(rs)] ∉ 𝒟 (P ⟦A⟧✓ Q)› have ‹t_P ∉ 𝒟 P› ‹t_Q ∉ 𝒟 Q›
      by (simp add: D_Syncptick', use front_tickFree_Nil in blast)+
    from "*" obtain r s t_P' t_Q'
      where ‹tick_join r s = ⌊rs⌋› ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
      by (blast elim: snoc_tick_setinterleavesptickE)
    from this(2, 3) ‹t_P ∉ 𝒟 P› ‹t_Q ∉ 𝒟 Q› ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
    have ‹r ∈ ✓s(P)› ‹s ∈ ✓s(Q)› by (metis strict_ticks_of_memI)+
    from that(2)[OF this, unfolded ‹tick_join r s = ⌊rs⌋›] show ‹length rs = n› by simp 
  qed
qed



lemma is_ticks_length_One_RenamingTick_singl [is_ticks_length_simp] :
  ‹length✓⇘Suc 0⇙(RenamingTick P (λr. [r]))›
  by (simp add: is_ticks_length_Renaming)

lemma is_ticks_length_Two_SyncPairlist [is_ticks_length_simp] :
  ‹length✓⇘Suc (Suc 0)⇙(P ⟦S⟧✓Pairlist Q)›
  by (simp add: is_ticks_length_Syncptick[OF SyncPairlist.Syncptick_locale_axioms])


lemma is_ticks_length_Suc_SyncRlist [is_ticks_length_intro] :
  ‹length✓⇘n⇙(Q) ⟹ length✓⇘Suc n⇙(P ⟦S⟧✓Rlist Q)›
  by (rule is_ticks_length_Syncptick[OF SyncRlist.Syncptick_locale_axioms])
    (simp add: is_ticks_lengthD)

text ‹The equivalence is false.›

lemma False if ‹⋀P Q n. length✓⇘Suc n⇙(P ⟦S⟧✓Rlist Q) ⟹ length✓⇘n⇙(Q)›
  using that[of 0 STOP ‹SKIP [undefined]›]
  by (simp add: is_ticks_length_STOP is_ticks_length_SKIP_iff)


lemma is_ticks_length_Suc_SyncLlist [is_ticks_length_intro] :
  ‹length✓⇘n⇙(P) ⟹ length✓⇘Suc n⇙(P ⟦S⟧✓Llist Q)›
  by (rule is_ticks_length_Syncptick
      [OF SyncRlist.Syncptick_comm_locale_sym.Syncptick_locale_axioms])
    (simp add: is_ticks_lengthD)

lemma is_ticks_length_sum_SyncListslenL [is_ticks_length_intro] :
  ‹length✓⇘m⇙(Q) ⟹ length✓⇘n + m⇙(P ⇘n⇙⟦S⟧✓ListslenL Q)›
  by (rule is_ticks_length_Syncptick[OF SyncListslenL.Syncptick_locale_axioms])
    (simp add: is_ticks_lengthD)

lemma is_ticks_length_sum_SyncListslenR [is_ticks_length_intro] :
  ‹length✓⇘n⇙(P) ⟹ length✓⇘n + m⇙(P ⇘m⇙⟦S⟧✓ListslenR Q)›
  by (rule is_ticks_length_Syncptick
      [OF SyncListslenL.Syncptick_comm_locale_sym.Syncptick_locale_axioms])
    (simp add: is_ticks_lengthD)

lemma is_ticks_length_sum_SyncLists [is_ticks_length_intro] :
  ‹length✓⇘n + m⇙(P ⇘n⇙⟦S⟧✓⇘m⇙ Q)›
  by (rule is_ticks_length_Syncptick[OF SyncLists.Syncptick_locale_axioms]) simp



subsection ‹Conversions›

lemma SyncPairlist_to_SyncRlist :
  ‹P ⟦S⟧✓Pairlist Q = P ⟦S⟧✓Rlist RenamingTick Q (λs. [s])›
  by (rule SyncRlist.inj_RenamingTick_Syncptick_inj_RenamingTick
      [of id ‹λs. [s]›, simplified, symmetric])
    (auto intro: inj_onI)

lemma SyncPairlist_to_SyncLlist :
  ‹P ⟦S⟧✓Pairlist Q = RenamingTick P (λr. [r]) ⟦S⟧✓Llist Q›
  by (rule SyncRlist.Syncptick_comm_locale_sym.inj_RenamingTick_Syncptick_inj_RenamingTick
      [of ‹λr. [r]› id, simplified, symmetric])
    (auto intro: inj_onI)


lemma SyncRlist_to_SyncListslenL :
  ‹P ⟦S⟧✓Rlist Q = RenamingTick P (λr. [r]) ⇘Suc 0⇙⟦S⟧✓ListslenL Q›
  by (rule SyncListslenL.inj_RenamingTick_Syncptick_inj_RenamingTick
      [of ‹λr. [r]› id ‹Suc 0›, simplified, symmetric])
    (auto intro: inj_onI)

lemma SyncLlist_to_SyncListslenR :
  ‹P ⟦S⟧✓Llist Q = P ⇘Suc 0⇙⟦S⟧✓ListslenR RenamingTick Q (λs. [s])›
  by (rule SyncListslenL.Syncptick_comm_locale_sym.inj_RenamingTick_Syncptick_inj_RenamingTick
      [of id ‹λs. [s]› ‹Suc 0›, simplified, symmetric])
    (auto intro: inj_onI)


lemma SyncListslenL_to_SyncLists :
  ‹length✓⇘m⇙(Q) ⟹ P ⇘n⇙⟦S⟧✓ListslenL Q = P ⇘n⇙⟦S⟧✓⇘m⇙ Q›
  by (auto intro!: SyncLists.Syncptick_same_tick_join_on_strict_ticks_of
      SyncListslenL.Syncptick_locale_axioms
      dest: is_ticks_lengthD)

lemma SyncListslenR_to_SyncLists :
  ‹length✓⇘n⇙(P) ⟹ P ⇘m⇙⟦S⟧✓ListslenR Q = P ⇘n⇙⟦S⟧✓⇘m⇙ Q›
  by (auto intro!: SyncLists.Syncptick_same_tick_join_on_strict_ticks_of
      SyncListslenL.Syncptick_comm_locale_sym.Syncptick_locale_axioms
      dest: is_ticks_lengthD)

corollary SyncListslenL_is_SyncListslenR :
  ‹length✓⇘n⇙(P) ⟹ length✓⇘m⇙(Q) ⟹ P ⇘n⇙⟦S⟧✓ListslenL Q = P ⇘m⇙⟦S⟧✓ListslenR Q›
  by (simp add: SyncListslenL_to_SyncLists SyncListslenR_to_SyncLists)


corollary SyncPairlist_to_SyncListslenL :
  ‹P ⟦S⟧✓Pairlist Q = RenamingTick P (λr. [r]) ⇘Suc 0⇙⟦S⟧✓ListslenL RenamingTick Q (λs. [s])›
  by (simp add: SyncPairlist_to_SyncRlist SyncRlist_to_SyncListslenL)

corollary SyncPairlist_to_SyncListslenR :
  ‹P ⟦S⟧✓Pairlist Q = RenamingTick P (λr. [r]) ⇘Suc 0⇙⟦S⟧✓ListslenR RenamingTick Q (λs. [s])›
  by (simp add: SyncLlist_to_SyncListslenR SyncPairlist_to_SyncLlist)

corollary SyncRlist_to_SyncLists :
  ‹length✓⇘m⇙(Q) ⟹ P ⟦S⟧✓Rlist Q = RenamingTick P (λr. [r]) ⇘Suc 0⇙⟦S⟧✓⇘m⇙ Q›
  by (simp add: SyncListslenL_to_SyncLists SyncRlist_to_SyncListslenL)

corollary SyncLlist_to_SyncLists :
  ‹length✓⇘n⇙(P) ⟹ P ⟦S⟧✓Llist Q = P ⇘n⇙⟦S⟧✓⇘Suc 0⇙ RenamingTick Q (λs. [s])›
  by (simp add: SyncListslenR_to_SyncLists SyncLlist_to_SyncListslenR)

corollary SyncPairlist_to_SyncLists :
  ‹P ⟦S⟧✓Pairlist Q = RenamingTick P (λr. [r]) ⇘Suc 0⇙⟦S⟧✓⇘Suc 0⇙ RenamingTick Q (λs. [s])›
  by (simp add: SyncLlist_to_SyncLists SyncPairlist_to_SyncLlist
      is_ticks_length_One_RenamingTick_singl)




lemma SyncPair_to_SyncPairlist :
  ‹RenamingTick (P ⟦S⟧✓Pair Q) (λ(r, s). [r, s]) = P ⟦S⟧✓Pairlist Q›
  by (rule SyncPair.inj_on_RenamingTick_Syncptick
      [of ‹λ(r, s). [r, s]›, simplified])
    (auto intro: inj_onI)

lemma SyncPairlist_to_SyncPair :
  ‹RenamingTick (P ⟦S⟧✓Pairlist Q) (λrs. (rs ! 0, rs ! Suc 0)) = P ⟦S⟧✓Pair Q›
  by (rule SyncPairlist.inj_on_RenamingTick_Syncptick
      [of ‹λrs. (rs ! 0, rs ! Suc 0)›, simplified])
    (auto intro: inj_onI)

lemma SyncPair_to_SyncRlist :
  ‹RenamingTick (P ⟦S⟧✓Pair Q) (λ(r, s). r # s) = P ⟦S⟧✓Rlist Q›
  by (rule SyncPair.inj_on_RenamingTick_Syncptick
      [of ‹λ(r, s). r # s›, simplified])
    (auto intro: inj_onI)

lemma SyncPair_to_SyncLlist :
  ‹RenamingTick (P ⟦S⟧✓Pair Q) (λ(r, s). r @ [s]) = P ⟦S⟧✓Llist Q›
  by (rule SyncPair.inj_on_RenamingTick_Syncptick
      [of ‹λ(r, s). r @ [s]›, simplified])
    (auto intro: inj_onI)


lemma SyncPair_to_SyncListslenL :
  ‹RenamingTick (P ⟦S⟧✓Pair Q) (λ(r, s). r @ s) = P ⇘n⇙⟦S⟧✓ListslenL Q›
  (is ‹?lhs = ?rhs›) if ‹length✓⇘n⇙(P)›
proof -
  let ?g = ‹λrs. (take n rs, drop n rs)›
  let ?g' = ‹λ(r, s). r @ s›
  let ?RT = RenamingTick
  have ‹?RT ?lhs ?g = ?RT ?rhs ?g›
  proof (subst SyncListslenL.inj_on_RenamingTick_Syncptick)
    show ‹inj_on ?g (SyncListslenL.range_tick_join n)›
      by (rule inj_onI) (auto split: if_split_asm)
  next
    have ‹?RT (?RT (P ⟦S⟧✓Pair Q) ?g') ?g = P ⟦S⟧✓Pair Q›
    proof (fold RenamingTick_comp, subst (2) RenamingTick_id[of ‹P ⟦S⟧✓Pair Q›, symmetric])
      show ‹?RT (P ⟦S⟧✓Pair Q) (?g ∘ ?g') = ?RT (P ⟦S⟧✓Pair Q) id›
      proof (rule RenamingTick_is_restrictable_on_strict_ticks_of)
        from that show ‹rs ∈ ✓s(P ⟦S⟧✓Pair Q) ⟹ (?g ∘ (λ(x, y). x @ y)) rs = id rs› for rs
          by (auto dest!: set_mp[OF SyncPair.strict_ticks_of_Syncptick_subset] is_ticks_lengthD)
      qed
    qed
    also have ‹P ⟦S⟧✓Pair Q =
               Syncptick_locale.Syncptick
               (λr s. case if length r = n then ⌊r @ s⌋ else ◇
                      of ◇ ⇒ ◇ | ⌊rs⌋ ⇒ ⌊?g rs⌋) P S Q› (is ‹_ = ?rhs'›)
      by (rule SyncPair.Syncptick_same_tick_join_on_strict_ticks_of[symmetric], unfold_locales)
        (use ‹length✓⇘n⇙(P)› in ‹auto split: if_split_asm dest: is_ticks_lengthD›)
    finally show ‹?RT ?lhs ?g = ?rhs'› .
  qed
  hence ‹?RT (?RT ?lhs ?g) ?g' = ?RT (?RT ?rhs ?g) ?g'› by simp
  also from ‹length✓⇘n⇙(P)› have ‹?RT (?RT ?lhs ?g) ?g' = ?lhs›
    by (auto simp flip: RenamingTick_comp intro!: RenamingTick_is_restrictable_on_strict_ticks_of
                 dest!: set_mp[OF SyncPair.strict_ticks_of_Syncptick_subset] is_ticks_lengthD)
  also from ‹length✓⇘n⇙(P)› have ‹?RT (?RT ?rhs ?g) ?g' = ?rhs›
    by (fold RenamingTick_comp, subst (2) RenamingTick_id[of ?rhs, symmetric])
      (auto simp del: RenamingTick_id intro!: RenamingTick_is_restrictable_on_strict_ticks_of
               dest!: set_mp[OF SyncPair.strict_ticks_of_Syncptick_subset] is_ticks_lengthD)
  finally show ‹?lhs = ?rhs› .
qed


corollary SyncPair_to_SyncListslenR :
  ‹RenamingTick (P ⟦S⟧✓Pair Q) (λ(r, s). r @ s) = P ⇘n⇙⟦S⟧✓ListslenR Q›
  (is ‹?lhs = ?rhs›) if ‹length✓⇘n⇙(Q)›
proof -
  let ?RT = RenamingTick
  have ‹?RT (P ⟦S⟧✓Pair Q) (λ(x, y). x @ y) =
        ?RT (Q ⟦S⟧✓Pair P) ((λ(x, y). x @ y) ∘ prod.swap)›
    by (simp add: RenamingTick_comp subst SyncPair.Syncptick_commute)
  also from ‹length✓⇘n⇙(Q)›
  have ‹… = ?RT (Q ⟦S⟧✓Pair P) ((λrs. drop n rs @ take n rs) ∘ (λ(x, y). x @ y))›
    by (auto intro!: RenamingTick_is_restrictable_on_strict_ticks_of
              dest!: set_mp[OF SyncPair.strict_ticks_of_Syncptick_subset] is_ticks_lengthD)
  also have ‹… = ?RT (Q ⇘n⇙⟦S⟧✓ListslenL P) (λrs. drop n rs @ take n rs)›
    by (simp add: RenamingTick_comp SyncPair_to_SyncListslenL[OF ‹length✓⇘n⇙(Q)›])
  also have ‹… = P ⇘n⇙⟦S⟧✓ListslenR Q›
    by (fact SyncListslenL.Syncptick_commute)
  finally show ‹?lhs = ?rhs› .
qed

corollary SyncPair_to_SyncLists :
  ‹RenamingTick (P ⟦S⟧✓Pair Q) (λ(r, s). r @ s) = P ⇘n⇙⟦S⟧✓⇘m⇙ Q›
  (is ‹?lhs = ?rhs›) if ‹length✓⇘n⇙(P)› and ‹length✓⇘m⇙(Q)›
  by (subst SyncPair_to_SyncListslenL[OF ‹length✓⇘n⇙(P)›])
    (rule SyncListslenL_to_SyncLists[OF ‹length✓⇘m⇙(Q)›])



section ‹First Laws›

corollary InterClassic_STOP [simp] :
  ‹P |||✓Classic STOP = P ; STOP›
  by (simp add: SyncClassic.Interptick_STOP[of P id])

corollary InterPair_STOP :
  ‹P |||✓Pair STOP = RenamingTick (P ; STOP) (λr. (r, g r))›
  by (simp add: SyncPair.Interptick_STOP[of P g])

corollary InterPairlist_STOP :
  ‹P |||✓Pairlist STOP = RenamingTick (P ; STOP) (λr. [r, g r])›
  by (simp add: SyncPairlist.Interptick_STOP[of P g])

corollary InterRlist_STOP :
  ‹P |||✓Rlist STOP = RenamingTick (P ; STOP) (λr. r # g r)›
  by (simp add: SyncRlist.Interptick_STOP[of P g])

corollary InterLlist_STOP :
  ‹P |||✓Llist STOP = RenamingTick (P ; STOP) (λr. r @ [g r])›
  by (simp add: SyncRlist.Syncptick_comm_locale_sym.Interptick_STOP[of P g])

corollary InterListslenL_STOP :
  ‹P ⇘n⇙|||✓ListslenL STOP =
   RenamingTick (P ; STOP) (λr. if length r = n then r @ g r else undefined)›
  by (auto simp add: SyncListslenL.Interptick_STOP[of n P g] option.the_def
      intro!: arg_cong[where f = ‹RenamingTick (P ; STOP)›])

corollary InterListslenR_STOP :
  ‹P ⇘n⇙|||✓ListslenR STOP =
   RenamingTick (P ; STOP) (λr. if length (g r) = n then r @ g r else undefined)›
  by (auto simp add: SyncListslenL.Syncptick_comm_locale_sym.Interptick_STOP[of n P g] option.the_def
      intro!: arg_cong[where f = ‹RenamingTick (P ; STOP)›])

corollary InterLists_STOP :
  ‹P ⇘n⇙|||✓⇘m⇙ STOP =
   RenamingTick (P ; STOP) (λr. if length r = n ∧ length (g r) = m then r @ g r else undefined)›
  by (auto simp add: SyncLists.Interptick_STOP[of n m P g] option.the_def
      intro!: arg_cong[where f = ‹RenamingTick (P ; STOP)›])



corollary STOP_InterClassic [simp] :
  ‹STOP |||✓Classic Q = Q ; STOP›
  by (simp add: SyncClassic.STOP_Interptick[of Q id])

corollary STOP_InterPair :
  ‹STOP |||✓Pair Q = RenamingTick (Q ; STOP) (λs. (g s, s))›
  by (simp add: SyncPair.STOP_Interptick[of Q g])

corollary STOP_InterPairlist :
  ‹STOP |||✓Pairlist Q = RenamingTick (Q ; STOP) (λs. [g s, s])›
  by (simp add: SyncPairlist.STOP_Interptick[of Q g])

corollary STOP_InterRlist :
  ‹STOP |||✓Rlist Q = RenamingTick (Q ; STOP) (λs. g s # s)›
  by (simp add: SyncRlist.STOP_Interptick[of Q g])

corollary STOP_InterLlist :
  ‹STOP |||✓Llist Q = RenamingTick (Q ; STOP) (λs. g s @ [s])›
  by (simp add: SyncRlist.Syncptick_comm_locale_sym.STOP_Interptick[of Q g])

corollary STOP_InterListslenL :
  ‹STOP ⇘n⇙|||✓ListslenL Q =
   RenamingTick (Q ; STOP) (λr. if length (g r) = n then g r @ r else undefined)›
  by (auto simp add: SyncListslenL.STOP_Interptick[of n Q g] option.the_def
      intro!: arg_cong[where f = ‹RenamingTick (Q ; STOP)›])

corollary STOP_InterListslenR :
  ‹STOP ⇘n⇙|||✓ListslenR Q =
   RenamingTick (Q ; STOP) (λr. if length r = n then g r @ r else undefined)›
  by (auto simp add: SyncListslenL.Syncptick_comm_locale_sym.STOP_Interptick[of n Q g] option.the_def
      intro!: arg_cong[where f = ‹RenamingTick (Q ; STOP)›])

corollary STOP_InterLists :
  ‹STOP ⇘n⇙|||✓⇘m⇙ Q =
   RenamingTick (Q ; STOP) (λr. if length (g r) = n ∧ length r = m then g r @ r else undefined)›
  by (auto simp add: SyncLists.STOP_Interptick[of n m Q g] option.the_def
      intro!: arg_cong[where f = ‹RenamingTick (Q ; STOP)›])



corollary SKIP_SyncClassic_SKIP :
  ‹SKIP r ⟦A⟧✓Classic SKIP s =
   (if r = s then SKIP r else STOP)› by simp

corollary SKIP_SyncPair_SKIP :
  ‹SKIP r ⟦A⟧✓Pair SKIP s = SKIP (r, s)› by simp

corollary SKIP_SyncPairlist_SKIP :
  ‹SKIP r ⟦A⟧✓Pairlist SKIP s = SKIP [r, s]› by simp

corollary SKIP_SyncRlist_SKIP :
  ‹SKIP r ⟦A⟧✓Rlist SKIP s = SKIP (r # s)› by simp

corollary SKIP_SyncLlist_SKIP :
  ‹SKIP r ⟦A⟧✓Llist SKIP s = SKIP (r @ [s])› by simp

corollary SKIP_SyncListslenL_SKIP :
  ‹SKIP r ⇘n⇙⟦A⟧✓ListslenL SKIP s =
   (if length r = n then SKIP (r @ s) else STOP)› by simp

corollary SKIP_SyncListslenR_SKIP :
  ‹SKIP r ⇘n⇙⟦A⟧✓ListslenR SKIP s =
   (if length s = n then SKIP (r @ s) else STOP)› by simp

corollary SKIP_SyncLists_SKIP :
  ‹SKIP r ⇘n⇙⟦A⟧✓⇘m⇙ SKIP s =
   (if length r = n ∧ length s = m then SKIP (r @ s) else STOP)› by simp





section ‹Operational Laws›

subsection ‹Classical Version›

locale After_SyncClassic_locale = After_Syncptick_locale ‹λr s. if r = s then ⌊r⌋ else ◇›
begin

― ‹Just checking...›
lemma ‹Syncptick P S Q = P ⟦S⟧✓Classic Q› by (fact refl)

end

locale AfterExt_SyncClassic_locale =
  AfterExt_Syncptick_locale ‹λr s. if r = s then ⌊r⌋ else ◇›

sublocale AfterExt_SyncClassic_locale ⊆ After_SyncClassic_locale
  by unfold_locales

locale OpSemTransitions_SyncClassic_locale =
  OpSemTransitions_Syncptick_locale ‹λr s. if r = s then ⌊r⌋ else ◇›

sublocale OpSemTransitions_SyncClassic_locale ⊆ AfterExt_SyncClassic_locale
  by unfold_locales


subsection ‹Product Type›

locale After_SyncPair_locale = After_Syncptick_locale ‹λr s. ⌊(r, s)⌋›
begin

― ‹Just checking...›
lemma ‹Syncptick P S Q = P ⟦S⟧✓Pair Q› by (fact refl)

end

locale AfterExt_SyncPair_locale =
  AfterExt_Syncptick_locale ‹λr s. ⌊(r, s)⌋›

sublocale AfterExt_SyncPair_locale ⊆ After_SyncPair_locale
  by unfold_locales

locale OpSemTransitions_SyncPair_locale =
  OpSemTransitions_Syncptick_locale ‹λr s. ⌊(r, s)⌋›

sublocale OpSemTransitions_SyncPair_locale ⊆ AfterExt_SyncPair_locale
  by unfold_locales



subsection ‹List Type›

subsubsection ‹Pair›

locale After_SyncPairlist_locale = After_Syncptick_locale ‹λr s. ⌊[r, s]⌋›
begin

― ‹Just checking...›
lemma ‹Syncptick P S Q = P ⟦S⟧✓Pairlist Q› by (fact refl)

end

locale AfterExt_SyncPairlist_locale =
  AfterExt_Syncptick_locale ‹λr s. ⌊[r, s]⌋›

sublocale AfterExt_SyncPairlist_locale ⊆ After_SyncPairlist_locale
  by unfold_locales

locale OpSemTransitions_SyncPairlist_locale =
  OpSemTransitions_Syncptick_locale ‹λr s. ⌊[r, s]⌋›

sublocale OpSemTransitions_SyncPairlist_locale ⊆ AfterExt_SyncPairlist_locale
  by unfold_locales



subsubsection ‹Right List›

locale After_SyncRlist_locale = After_Syncptick_locale ‹λr s. ⌊r # s⌋›
begin

― ‹Just checking...›
lemma ‹Syncptick P S Q = P ⟦S⟧✓Rlist Q› by (fact refl)

end

locale AfterExt_SyncRlist_locale =
  AfterExt_Syncptick_locale ‹λr s. ⌊r # s⌋›

sublocale AfterExt_SyncRlist_locale ⊆ After_SyncRlist_locale
  by unfold_locales

locale OpSemTransitions_SyncRlist_locale =
  OpSemTransitions_Syncptick_locale ‹λr s. ⌊r # s⌋›

sublocale OpSemTransitions_SyncRlist_locale ⊆ AfterExt_SyncRlist_locale
  by unfold_locales



subsubsection ‹Left List›

locale After_SyncLlist_locale = After_Syncptick_locale ‹λr s. ⌊r @ [s]⌋›
begin

― ‹Just checking...›
lemma ‹Syncptick P S Q = P ⟦S⟧✓Llist Q› by (fact refl)

end

locale AfterExt_SyncLlist_locale =
  AfterExt_Syncptick_locale ‹λr s. ⌊r @ [s]⌋›

sublocale AfterExt_SyncLlist_locale ⊆ After_SyncLlist_locale
  by unfold_locales

locale OpSemTransitions_SyncLlist_locale =
  OpSemTransitions_Syncptick_locale ‹λr s. ⌊r @ [s]⌋›

sublocale OpSemTransitions_SyncLlist_locale ⊆ AfterExt_SyncLlist_locale
  by unfold_locales



subsubsection ‹Arbitrary Lists›

paragraph ‹Control on left side›

locale After_SyncListslenL_locale =
  After_Syncptick_locale ‹λr s. if length r = lenL then ⌊r @ s⌋ else ◇›
  for lenL :: nat
begin

― ‹Just checking...›
lemma ‹Syncptick P S Q = P ⇘lenL⇙⟦S⟧✓ListslenL Q› by (fact refl)

end

locale AfterExt_SyncListslenL_locale =
  AfterExt_Syncptick_locale ‹λr s. if length r = lenL then ⌊r @ s⌋ else ◇›
  for lenL :: nat

sublocale AfterExt_SyncListslenL_locale ⊆ After_SyncListslenL_locale
  by unfold_locales

locale OpSemTransitions_SyncListslenL_locale =
  OpSemTransitions_Syncptick_locale ‹λr s. if length r = lenL then ⌊r @ s⌋ else ◇›
  for lenL :: nat

sublocale OpSemTransitions_SyncListslenL_locale ⊆ AfterExt_SyncListslenL_locale
  by unfold_locales



paragraph ‹Control on right side›

locale After_SyncListslenR_locale =
  After_Syncptick_locale ‹λr s. if length s = lenR then ⌊r @ s⌋ else ◇›
  for lenR :: nat
begin

― ‹Just checking...›
lemma ‹Syncptick P S Q = P ⇘lenR⇙⟦S⟧✓ListslenR Q› by (fact refl)

end

locale AfterExt_SyncListslenR_locale =
  AfterExt_Syncptick_locale ‹λr s. if length s = lenR then ⌊r @ s⌋ else ◇›
  for lenR :: nat

sublocale AfterExt_SyncListslenR_locale ⊆ After_SyncListslenR_locale
  by unfold_locales

locale OpSemTransitions_SyncListslenR_locale =
  OpSemTransitions_Syncptick_locale ‹λr s. if length r = lenL then ⌊r @ s⌋ else ◇›
  for lenL :: nat

sublocale OpSemTransitions_SyncListslenR_locale ⊆ AfterExt_SyncListslenR_locale
  by unfold_locales



paragraph ‹Control on both sides›

locale After_SyncLists_locale =
  After_Syncptick_locale
  ‹λr s. if length r = lenL ∧ length s = lenR then ⌊r @ s⌋ else ◇›
  for lenL lenR :: nat
begin

― ‹Just checking...›
lemma ‹Syncptick P S Q = P ⇘lenL⇙⟦S⟧✓⇘lenR⇙ Q› by (fact refl)

end

locale AfterExt_SyncLists_locale =
  AfterExt_Syncptick_locale
  ‹λr s. if length r = lenL ∧ length s = lenR then ⌊r @ s⌋ else ◇›
  for lenL lenR :: nat

sublocale AfterExt_SyncLists_locale ⊆ After_SyncLists_locale
  by unfold_locales

locale OpSemTransitions_SyncLists_locale =
  OpSemTransitions_Syncptick_locale
  ‹λr s. if length r = lenL ∧ length s = lenR then ⌊r @ s⌋ else ◇›
  for lenL lenR :: nat

sublocale OpSemTransitions_SyncLists_locale ⊆ AfterExt_SyncLists_locale
  by unfold_locales


(*<*)
end
  (*>*)