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‹Synchroptick_comm›.
Then, the laws of associativity will be derived
manually (instead of globally interpreting the locale locale‹Synchroptick_assoc›).
›

text ‹Starting with Isabelle-26, the arguments on which the interpretation
is based are sometimes ``hidden'' behind a definition a definition to prevent a call to
the simplifier from breaking everything.›



subsection ‹Classical Version›

text (in Synchroptick) ‹
The following interpretation is initially the reason we wanted the parameter
term‹tj› 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).
›

definition SyncClassic_tj :: ‹'r ⇒ 'r ⇒ 'r option›
  where ‹SyncClassic_tj r s ≡ if r = s then ⌊r⌋ else ◇›

interpretation SyncClassic : Synchroptick_comm
  SyncClassic_tj SyncClassic_tj id id
  by unfold_locales (auto simp add: SyncClassic_tj_def 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 ‹Right Unit›

definition SyncRunit_tj :: ‹'r ⇒ unit ⇒ 'r option›
  where ‹SyncRunit_tj r s ≡ ⌊r⌋›

definition SyncRunit_tj_dual :: ‹unit ⇒ 's ⇒ 's option›
  where ‹SyncRunit_tj_dual r s ≡ ⌊s⌋›

interpretation SyncRunit : Synchroptick_comm
  SyncRunit_tj SyncRunit_tj_dual id id
  by unfold_locales
    (auto simp add: SyncRunit_tj_def SyncRunit_tj_dual_def split: if_split_asm)

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


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


subsection ‹Product Type›

definition SyncPair_tj :: ‹'r ⇒ 's ⇒ ('r × 's) option›
  where ‹SyncPair_tj r s ≡ ⌊(r, s)⌋›

interpretation SyncPair : Synchroptick_comm
  SyncPair_tj SyncPair_tj prod.swap prod.swap
  by unfold_locales (auto simp add: SyncPair_tj_def 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›

definition SyncPairlist_tj :: ‹'r ⇒ 'r ⇒ 'r list option›
  where ‹SyncPairlist_tj r s ≡ ⌊[r, s]⌋›

definition SyncPairlist_tj_conv :: ‹'r list ⇒ 'r list›
  where ‹SyncPairlist_tj_conv rs ≡ [rs ! Suc 0, rs ! 0]›

interpretation SyncPairlist : Synchroptick_comm
  SyncPairlist_tj SyncPairlist_tj SyncPairlist_tj_conv SyncPairlist_tj_conv
  by unfold_locales (auto simp add: SyncPairlist_tj_def SyncPairlist_tj_conv_def split: if_split_asm)

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.
›

definition SyncRlist_tj :: ‹'r ⇒ 'r list ⇒ 'r list option›
  where ‹SyncRlist_tj r s ≡ ⌊r # s⌋›

definition SyncRlist_tj_dual :: ‹'r list ⇒ 'r ⇒ 'r list option›
  where ‹SyncRlist_tj_dual s r ≡ ⌊s @ [r]⌋›
(* 
definition SyncRlist_tj_conv :: ‹'r list ⇒ 'r list›
  where ‹SyncRlist_tj_conv ≡ rotate1›
 *)
definition SyncRlist_tj_dual_conv :: ‹'r list ⇒ 'r list›
  where ‹SyncRlist_tj_dual_conv rs ≡ if rs = [] then [] else last rs # butlast rs›
  ― ‹because term‹λrs. last rs # butlast rs› is not injective.›


interpretation SyncRlist : Synchroptick_comm
  SyncRlist_tj SyncRlist_tj_dual rotate1 SyncRlist_tj_dual_conv
  by unfold_locales
    (auto simp add: SyncRlist_tj_def SyncRlist_tj_dual_def SyncRlist_tj_dual_conv_def 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.Synchroptick_comm_dual.Syncptick  (‹(_ ⟦_⟧✓Llist _)› [70, 0, 71] 70)
notation SyncRlist.Synchroptick_comm_dual.Interptick (‹(_ |||✓Llist _)› [72, 73] 72)
notation SyncRlist.Synchroptick_comm_dual.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‹Synchroptick›.
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

definition SyncListslenL_tj :: ‹'r list ⇒ 'r list ⇒ 'r list option›
  where ‹SyncListslenL_tj r s ≡ if length r = lenL then ⌊r @ s⌋ else ◇›

definition SyncListslenL_tj_dual :: ‹'r list ⇒ 'r list ⇒ 'r list option›
  where ‹SyncListslenL_tj_dual s r ≡ if length r = lenL then ⌊s @ r⌋ else ◇›

definition SyncListslenL_tj_conv :: ‹'r list ⇒ 'r list›
  where ‹SyncListslenL_tj_conv rs ≡ drop lenL rs @ take lenL rs›

definition SyncListslenL_tj_dual_conv :: ‹'r list ⇒ 'r list›
  where ‹SyncListslenL_tj_dual_conv rs ≡ rev (take lenL (rev rs)) @ rev (drop lenL (rev rs))›

global_interpretation SyncListslenL : Synchroptick_comm 
  SyncListslenL_tj SyncListslenL_tj_dual SyncListslenL_tj_conv SyncListslenL_tj_dual_conv
  by unfold_locales
    (auto simp add: SyncListslenL_tj_def SyncListslenL_tj_dual_def
      SyncListslenL_tj_conv_def SyncListslenL_tj_dual_conv_def 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.Synchroptick_comm_dual.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.Synchroptick_comm_dual.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.Synchroptick_dual.Parptick lenL P Q›



paragraph ‹Control on both sides›

definition SyncLists_tj :: ‹[nat, nat, 'r list, 'r list] ⇒ 'r list option›
  where ‹SyncLists_tj lenL lenR r s ≡ if length r = lenL ∧ length s = lenR then ⌊r @ s⌋ else ◇›

definition SyncLists_tj_conv :: ‹nat ⇒ 'r list ⇒ 'r list›
  where ‹SyncLists_tj_conv lenL rs ≡ drop lenL rs @ take lenL rs›

interpretation SyncLists : Synchroptick_comm 
  ‹SyncLists_tj lenL lenR› ‹SyncLists_tj lenR lenL›
  ‹SyncLists_tj_conv lenL› ‹SyncLists_tj_conv lenR› for lenL lenR
  by unfold_locales
    (auto simp add: SyncLists_tj_def SyncLists_tj_conv_def split: if_split_asm)


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 -
  interpret * : Synchroptick_assoc SyncClassic_tj SyncClassic_tj SyncClassic_tj SyncClassic_tj id id
    by (unfold_locales) (auto simp add: SyncClassic_tj_def split: if_split_asm)
  show ?thesis by (fact "*.Syncptick_assoc"[simplified])
qed



subsection ‹Unit›

lemma (in Synchroptick) Syncptick_SyncRunit_assoc :
  ‹P ⟦S⟧✓ (Q ⟦S⟧✓Runit R) = P ⟦S⟧✓ Q ⟦S⟧✓Runit R›
proof -
  interpret * : Synchroptick_assoc ‹(⊗✓)› SyncRunit_tj ‹(⊗✓)› SyncRunit_tj id id
    by unfold_locales (auto simp add: SyncRunit_tj_def)
  show ?thesis by (fact "*.Syncptick_assoc"[unfolded Renaming_id])
qed

lemma (in Synchroptick) SyncLunit_Syncptick_assoc :
  ‹P ⟦S⟧✓Lunit (Q ⟦S⟧✓ R) = P ⟦S⟧✓Lunit Q ⟦S⟧✓ R›
proof -
  interpret * : Synchroptick_assoc SyncRunit_tj_dual ‹(⊗✓)› SyncRunit_tj_dual ‹(⊗✓)› id id
    by unfold_locales (auto simp add: SyncRunit_tj_dual_def)
  show ?thesis by (fact "*.Syncptick_assoc"[unfolded 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 * : Synchroptick_assoc SyncPair_tj SyncPair_tj SyncPair_tj
    SyncPair_tj ‹λ((r, s), t). (r, s, t)› ‹λ(r, s, t). ((r, s), t)›
    by unfold_locales (auto simp add: SyncPair_tj_def)
  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 * : Synchroptick_assoc SyncPairlist_tj SyncRlist_tj_dual SyncRlist_tj SyncPairlist_tj id id
    by unfold_locales (auto simp add: SyncPairlist_tj_def SyncRlist_tj_def SyncRlist_tj_dual_def)
  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 * : Synchroptick_assoc SyncRlist_tj SyncRlist_tj_dual SyncRlist_tj SyncRlist_tj_dual id id
    by unfold_locales (auto simp add: SyncRlist_tj_def SyncRlist_tj_dual_def)
  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 * : Synchroptick_assoc
    SyncRlist_tj ‹SyncListslenL_tj (Suc lenQ)› SyncRlist_tj ‹SyncListslenL_tj lenQ› id id
    by unfold_locales (auto simp add: SyncRlist_tj_def SyncListslenL_tj_def 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 * : Synchroptick_assoc
    ‹SyncListslenL_tj_dual lenQ› SyncRlist_tj_dual
    ‹SyncListslenL_tj_dual (Suc lenQ)› SyncRlist_tj_dual id id
    by unfold_locales (auto simp add: SyncRlist_tj_dual_def SyncListslenL_tj_dual_def 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 * : Synchroptick_assoc
    ‹SyncLists_tj lenP lenQ› ‹SyncLists_tj (lenP + lenQ) lenR›
    ‹SyncLists_tj lenP (lenQ + lenR)› ‹SyncLists_tj lenQ lenR› id id
    by unfold_locales (auto simp add: SyncLists_tj_def 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 * : Synchroptick_assoc
    SyncPairlist_tj ‹SyncListslenL_tj (Suc (Suc 0))› SyncRlist_tj SyncRlist_tj id id
    by unfold_locales
      (auto simp add: SyncPairlist_tj_def SyncListslenL_tj_def SyncRlist_tj_def 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 * : Synchroptick_assoc
    SyncRlist_tj_dual SyncRlist_tj_dual ‹SyncListslenL_tj_dual (Suc (Suc 0))› SyncPairlist_tj id id
    by unfold_locales
      (auto simp add: SyncPairlist_tj_def SyncRlist_tj_dual_def SyncListslenL_tj_dual_def 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.
›

lemma setinterleaves_is_setinterleavesClassic :
  ‹t setinterleaves ((u, v), range tick ∪ ev ` A) ⟷
   t setinterleaves✓⇘SyncClassic_tj⇙ ((u, v), A)›
  for t :: ‹('a, 'r) traceptick›
  by (induct ‹(SyncClassic_tj :: 'r ⇒ 'r ⇒ 'r option, u, A, v)›
      arbitrary: t u v) (simp_all add: SyncClassic_tj_def image_iff)

corollary setinterleaves_is_setinterleavesRunit :
  ‹t setinterleaves ((u, v), insert ✓ (ev ` A)) ⟷
   t setinterleaves✓⇘SyncRunit_tj⇙ ((u, v), A)› (is ‹?lhs ⟷ ?rhs›)
proof -
  have ‹?lhs ⟷ t setinterleaves ((u, v), range tick ∪ ev ` A)›
    by (simp add: UNIV_unit)
  also have ‹… ⟷ t setinterleaves✓⇘SyncClassic_tj⇙ ((u, v), A)›
    by (fact setinterleaves_is_setinterleavesClassic)
  also have ‹… ⟷ ?rhs›
    by (intro arg_cong[where f = ‹λtj. t setinterleaves✓⇘tj⇙ ((u, v), A)›] ext)
      (simp add: SyncClassic_tj_def SyncRunit_tj_def)
  finally show ‹?lhs ⟷ ?rhs› .
qed


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_setinterleavesClassic)
      (metis setinterleaving_dual)
next
  show ‹t ∈ 𝒟 (P ⟦A⟧✓Classic Q) ⟹ t ∈ 𝒟 (P ⟦A⟧ Q)› for t
    by (simp add: D_Sync SyncClassic.D_Syncptick
        flip: setinterleaves_is_setinterleavesClassic)
      (metis setinterleaving_dual)
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 SyncClassic_tj X_P A X_Q›
    by (auto simp add: super_ref_Syncptick_def subset_iff SyncClassic_tj_def)
      (metis eventptick.exhaust)
  with "*"(1-3) show ‹(t, X) ∈ ℱ (P ⟦A⟧✓Classic Q)›
    by (auto simp add: SyncClassic.F_Syncptick setinterleaves_is_setinterleavesClassic)
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✓⇘SyncClassic_tj⇙ ((t_P, t_Q), A)›
      ‹X ⊆ super_ref_Syncptick SyncClassic_tj 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_setinterleavesClassic) 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 SyncClassic_tj_def split: if_split_asm)
  ultimately show ‹(t, X) ∈ ℱ (P ⟦A⟧ Q)› by (meson is_processT4)
qed



subsection ‹Other Properties›

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


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) (SyncLists_tj_conv lenL) = 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 Inter_STOP inf_bot_right is_ticks_length_unique non_terminating_Seq
        strict_ticks_of_STOP strict_ticks_of_Sync_subset subset_empty)
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_ftF] obtain u' where ‹u = u' @ [✓(rs)]›
    by (cases u rule: rev_cases, auto simp add: ‹t = t' @ [✓(rs)]› split: if_split_asm)
      (metis Hiding_tF append1_eq_conv eventptick.disc(2)
        eventptick.simps(4) not_tF_and_ftF tF_Cons_iff tF_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_tF
        ftF_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_tF 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) ftF_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 (no_types) tF_Nil eventptick.disc(2) tF_map_ev_comp[of of_ev]
      tF_append_iff tF_Cons_iff last_append
      butlast_append[of "map (ev ∘ of_ev) _"] last_snoc
      butlast_snoc[of _ "✓(_)"] not_tF_and_ftF ftF_dw_closed
      is_processT2_TR is_processT9
      strict_ticks_of_memI[of _ _ P] strict_ticks_of_memI[of _ _ ‹Q _›],
      metis butlast_append butlast_snoc eventptick.disc(2) ftF_charn
      tF_Cons_iff tF_append_iff tF_imp_ftF tF_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 non_terminating_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) tF_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'› tF_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⇙(Synchroptick.Syncptick tj 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 ‹Synchroptick tj›
    and ‹⋀r s. r ∈ ✓s(P) ⟹ s ∈ ✓s(Q) ⟹
       case tj r s of ◇ ⇒ True | ⌊r_s⌋ ⇒ length r_s = n›
proof -
  interpret Synchroptick tj
    by (fact ‹Synchroptick tj›)
  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✓⇘tj⇙ ((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 ftF_Nil in blast)+
    from "*" obtain r s t_P' t_Q'
      where ‹tj 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 ‹tj 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 (auto intro!: is_ticks_length_Syncptick SyncPairlist.Synchroptick_axioms
      simp add: SyncPairlist_tj_def)

lemma is_ticks_length_Suc_SyncRlist [is_ticks_length_intro] :
  ‹length✓⇘n⇙(Q) ⟹ length✓⇘Suc n⇙(P ⟦S⟧✓Rlist Q)›
   by (auto intro!: is_ticks_length_Syncptick SyncRlist.Synchroptick_axioms
      simp add: SyncRlist_tj_def dest: 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 (auto intro!: is_ticks_length_Syncptick SyncRlist.Synchroptick_comm_dual.Synchroptick_axioms
      simp add: SyncRlist_tj_dual_def dest: 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 (auto intro!: is_ticks_length_Syncptick SyncListslenL.Synchroptick_axioms
      simp add: SyncListslenL_tj_def dest: 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 (auto intro!: is_ticks_length_Syncptick SyncListslenL.Synchroptick_comm_dual.Synchroptick_axioms
      simp add: SyncListslenL_tj_dual_def dest: is_ticks_lengthD)

lemma is_ticks_length_sum_SyncLists [is_ticks_length_intro] :
  ‹length✓⇘n + m⇙(P ⇘n⇙⟦S⟧✓⇘m⇙ Q)›
  by (auto intro: is_ticks_length_Syncptick SyncLists.Synchroptick_axioms
      simp add: SyncLists_tj_def)

lemma is_ticks_length_SyncRunit [is_ticks_length_intro] :
  ‹length✓⇘n⇙(P) ⟹ length✓⇘n⇙(P ⟦A⟧✓Runit Q)›
  by (auto intro!: is_ticks_length_Syncptick SyncRunit.Synchroptick_axioms
      simp add: SyncRunit_tj_def dest: is_ticks_lengthD)

corollary is_ticks_length_SyncLunit [is_ticks_length_intro] :
  ‹length✓⇘n⇙(Q) ⟹ length✓⇘n⇙(P ⟦A⟧✓Lunit Q)›
  by (simp flip: SyncRunit.Syncptick_commute add: is_ticks_length_SyncRunit)



subsection ‹Conversions›

lemma SyncPairlist_to_SyncRlist :
  ‹P ⟦S⟧✓Pairlist Q = P ⟦S⟧✓Rlist RenamingTick Q (λs. [s])›
proof -
  have * : ‹(λr s. SyncRlist_tj (id r) [s]) = SyncPairlist_tj›
    by (intro ext) (simp add: SyncRlist_tj_def SyncPairlist_tj_def)
  show ?thesis
    by (auto intro:  SyncRlist.inj_RenamingTick_Syncptick_inj_RenamingTick
        [of id ‹λs. [s]›, unfolded "*", simplified, symmetric] inj_onI)
qed

lemma SyncPairlist_to_SyncLlist :
  ‹P ⟦S⟧✓Pairlist Q = RenamingTick P (λr. [r]) ⟦S⟧✓Llist Q›
proof -
  have * : ‹(λr s. SyncRlist_tj_dual [r] (id s)) = SyncPairlist_tj›
    by (intro ext) (simp add: SyncRlist_tj_dual_def SyncPairlist_tj_def)
  show ?thesis
    by (auto intro:  SyncRlist.Synchroptick_comm_dual.inj_RenamingTick_Syncptick_inj_RenamingTick
        [of ‹λr. [r]› id, unfolded "*", simplified, symmetric] inj_onI)
qed

lemma SyncRlist_to_SyncListslenL :
  ‹P ⟦S⟧✓Rlist Q = RenamingTick P (λr. [r]) ⇘Suc 0⇙⟦S⟧✓ListslenL Q›
proof -
  have * : ‹(λr s. SyncListslenL_tj (Suc 0) [r] (id s)) = SyncRlist_tj›
    by (intro ext) (simp add: SyncListslenL_tj_def SyncRlist_tj_def)
  show ?thesis
    by (auto intro:  SyncListslenL.inj_RenamingTick_Syncptick_inj_RenamingTick
        [of ‹λr. [r]› id ‹Suc 0›, unfolded "*", simplified, symmetric] inj_onI)
qed

lemma SyncLlist_to_SyncListslenR :
  ‹P ⟦S⟧✓Llist Q = P ⇘Suc 0⇙⟦S⟧✓ListslenR RenamingTick Q (λs. [s])›
proof -
  have * : ‹(λr s. SyncListslenL_tj_dual (Suc 0) (id r) [s]) = SyncRlist_tj_dual›
    by (intro ext) (simp add: SyncListslenL_tj_dual_def SyncRlist_tj_dual_def)
  show ?thesis
    by (auto intro: SyncListslenL.Synchroptick_comm_dual.inj_RenamingTick_Syncptick_inj_RenamingTick
        [of id ‹λs. [s]› ‹Suc 0›, unfolded "*", simplified, symmetric] inj_onI)
qed


lemma SyncListslenL_to_SyncLists :
  ‹length✓⇘m⇙(Q) ⟹ P ⇘n⇙⟦S⟧✓ListslenL Q = P ⇘n⇙⟦S⟧✓⇘m⇙ Q›
  by (auto intro!: SyncLists.Syncptick_same_tj_on_strict_ticks_of SyncListslenL.Synchroptick_axioms
      simp add: SyncListslenL_tj_def SyncLists_tj_def 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_tj_on_strict_ticks_of
      SyncListslenL.Synchroptick_comm_dual.Synchroptick_axioms
      simp add: SyncListslenL_tj_dual_def SyncLists_tj_def 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›
proof -
  have * : ‹(λr s. case SyncPair_tj r s of ◇ ⇒ ◇ |
                   ⌊r_s⌋ ⇒ ⌊case r_s of (r, s) ⇒ [r, s]⌋) = SyncPairlist_tj›
    by (intro ext) (simp add: SyncPair_tj_def SyncPairlist_tj_def)
  show ?thesis  
    by (auto intro: SyncPair.inj_on_RenamingTick_Syncptick
        [of ‹λ(r, s). [r, s]›, unfolded "*"] inj_onI)
qed

lemma SyncPairlist_to_SyncPair :
  ‹RenamingTick (P ⟦S⟧✓Pairlist Q) (λrs. (rs ! 0, rs ! Suc 0)) = P ⟦S⟧✓Pair Q›
proof -
  have * : ‹(λr s. case SyncPairlist_tj r s of ◇ ⇒ ◇ |
                   ⌊r_s⌋ ⇒ ⌊(r_s ! 0, r_s ! Suc 0)⌋) = SyncPair_tj›
    by (intro ext) (simp add: SyncPair_tj_def SyncPairlist_tj_def)
  thm SyncPairlist.inj_on_RenamingTick_Syncptick
        [of ‹λrs. (rs ! 0, rs ! Suc 0)›, unfolded "*"]
  show ?thesis
    by (auto intro!: SyncPairlist.inj_on_RenamingTick_Syncptick
        [of ‹λrs. (rs ! 0, rs ! Suc 0)›, unfolded "*"] inj_onI
        simp add: SyncPairlist_tj_def)
qed

lemma SyncPair_to_SyncRlist :
  ‹RenamingTick (P ⟦S⟧✓Pair Q) (λ(r, s). r # s) = P ⟦S⟧✓Rlist Q›
proof -
  have * : ‹(λr s. case SyncPair_tj r s of ◇ ⇒ ◇ |
                   ⌊r_s⌋ ⇒ ⌊case r_s of (r, s) ⇒ r # s⌋) = SyncRlist_tj›
    by (intro ext) (simp add: SyncPair_tj_def SyncRlist_tj_def)
  show ?thesis
    by (auto intro!: SyncPair.inj_on_RenamingTick_Syncptick
        [of ‹λ(r, s). r # s›, unfolded "*"] inj_onI)
qed

lemma SyncPair_to_SyncLlist :
  ‹RenamingTick (P ⟦S⟧✓Pair Q) (λ(r, s). r @ [s]) = P ⟦S⟧✓Llist Q›
proof -
  have * : ‹(λr s. case SyncPair_tj r s of ◇ ⇒ ◇ |
                   ⌊r_s⌋ ⇒ ⌊case r_s of (r, s) ⇒ r @ [s]⌋) = SyncRlist_tj_dual›
    by (intro ext) (simp add: SyncPair_tj_def SyncRlist_tj_dual_def)
  show ?thesis
    by (auto intro!: SyncPair.inj_on_RenamingTick_Syncptick
        [of ‹λ(r, s). r @ [s]›, unfolded "*"] inj_onI)
qed

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_tj n)›
      by (rule inj_onI) (auto simp add: SyncListslenL_tj_def 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
              simp add: SyncPair_tj_def)
      qed
    qed
    also have ‹P ⟦S⟧✓Pair Q =
               Synchroptick.Syncptick
               (λr s. case if length r = n then ⌊r @ s⌋ else ◇
                      of ◇ ⇒ ◇ | ⌊rs⌋ ⇒ ⌊?g rs⌋) P S Q›
      by (rule SyncPair.Syncptick_same_tj_on_strict_ticks_of[symmetric], unfold_locales)
        (use ‹length✓⇘n⇙(P)› in ‹auto split: if_split_asm dest: is_ticks_lengthD simp add: SyncPair_tj_def›)
    also have ‹(λr s. case if length r = n then ⌊r @ s⌋ else ◇ of ◇ ⇒ ◇ | ⌊rs⌋ ⇒ ⌊?g rs⌋) =
      (λr s. case SyncListslenL_tj n r s of ◇ ⇒ ◇ | ⌊r_s⌋ ⇒ ⌊?g r_s⌋)› (is ‹_ = ?rhs'›)
      by (intro ext) (simp add: SyncListslenL_tj_def)
    finally show ‹?RT ?lhs ?g = Synchroptick.Syncptick
      (λr s. case SyncListslenL_tj n r s of ◇ ⇒ ◇ | ⌊r_s⌋ ⇒ ⌊?g r_s⌋) P S Q› .
  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
        simp add: SyncPair_tj_def)
  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
        simp add: SyncPair_tj_def)
  also have ‹… = ?RT (Q ⇘n⇙⟦S⟧✓ListslenL P) (SyncListslenL_tj_conv n)›
    by (simp add: RenamingTick_comp SyncPair_to_SyncListslenL[OF ‹length✓⇘n⇙(Q)›])
      (metis SyncListslenL_tj_conv_def)
  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] SyncClassic_tj_def)

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

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

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

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

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 SyncListslenL_tj_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.Synchroptick_comm_dual.Interptick_STOP[of n P g]
      option.the_def SyncListslenL_tj_dual_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 SyncLists_tj_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] SyncClassic_tj_def)

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

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

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

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

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 SyncListslenL_tj_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.Synchroptick_comm_dual.STOP_Interptick[of n Q g]
      option.the_def SyncListslenL_tj_dual_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 SyncLists_tj_def intro!: arg_cong[where f = ‹RenamingTick (Q ; STOP)›])


corollary SKIP_SyncClassic_SKIP [simp] :
  ‹SKIP r ⟦A⟧✓Classic SKIP s = (if r = s then SKIP r else STOP)›
  by (simp add: SyncClassic.SKIP_Syncptick_SKIP SyncClassic_tj_def)

corollary SKIP_SyncRunit_SKIP [simp] :
  ‹SKIP r ⟦A⟧✓Runit SKIP s = SKIP r›
  by (simp add: SyncRunit.SKIP_Syncptick_SKIP SyncRunit_tj_def)

corollary SKIP_SyncLunit_SKIP [simp] :
  ‹SKIP r ⟦A⟧✓Lunit SKIP s = SKIP s›
  by (simp add: SyncRunit.Synchroptick_comm_dual.SKIP_Syncptick_SKIP SyncRunit_tj_dual_def)

corollary SKIP_SyncPair_SKIP [simp] :
  ‹SKIP r ⟦A⟧✓Pair SKIP s = SKIP (r, s)›
  by (simp add: SyncPair.SKIP_Syncptick_SKIP SyncPair_tj_def)

corollary SKIP_SyncPairlist_SKIP [simp] :
  ‹SKIP r ⟦A⟧✓Pairlist SKIP s = SKIP [r, s]›
  by (simp add: SyncPairlist.SKIP_Syncptick_SKIP SyncPairlist_tj_def)

corollary SKIP_SyncRlist_SKIP [simp] :
  ‹SKIP r ⟦A⟧✓Rlist SKIP s = SKIP (r # s)›
  by (simp add: SyncRlist.SKIP_Syncptick_SKIP SyncRlist_tj_def)

corollary SKIP_SyncLlist_SKIP [simp] :
  ‹SKIP r ⟦A⟧✓Llist SKIP s = SKIP (r @ [s])›
  by (simp add: SyncRlist.Synchroptick_comm_dual.SKIP_Syncptick_SKIP SyncRlist_tj_dual_def)

corollary SKIP_SyncListslenL_SKIP [simp] :
  ‹SKIP r ⇘n⇙⟦A⟧✓ListslenL SKIP s =
   (if length r = n then SKIP (r @ s) else STOP)›
  by (simp add: SyncListslenL.SKIP_Syncptick_SKIP SyncListslenL_tj_def)

corollary SKIP_SyncListslenR_SKIP [simp] :
  ‹SKIP r ⇘n⇙⟦A⟧✓ListslenR SKIP s =
   (if length s = n then SKIP (r @ s) else STOP)›
  by (simp add: SyncListslenL.Synchroptick_comm_dual.SKIP_Syncptick_SKIP SyncListslenL_tj_dual_def)

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


corollary SKIPS_SyncRunit_SKIPS [simp] :
  ‹SKIPS R ⟦A⟧✓Runit SKIPS S = (if S = {} then STOP else SKIPS R)›
  by (simp add: SyncRunit.SKIPS_Syncptick_SKIPS SyncRunit_tj_def)
    (simp add: GlobalNdet_cartprod SKIPS_def)

corollary SKIPS_SyncLunit_SKIPS [simp] :
  ‹SKIPS R ⟦A⟧✓Lunit SKIPS S = (if R = {} then STOP else SKIPS S)›
  by (simp add: SyncRunit.Synchroptick_comm_dual.SKIPS_Syncptick_SKIPS SyncRunit_tj_dual_def)
    (simp add: GlobalNdet_cartprod SKIPS_def)

corollary SKIPS_SyncPair_SKIPS [simp] :
  ‹SKIPS R ⟦A⟧✓Pair SKIPS S = SKIPS (R × S)›
  by (simp add: SyncPair.SKIPS_Syncptick_SKIPS SyncPair_tj_def) (simp add: SKIPS_def)

corollary SKIPS_SyncPairlist_SKIPS [simp] :
  ‹SKIPS R ⟦A⟧✓Pairlist SKIPS S = SKIPS {[r, s] |r s. r ∈ R ∧ s ∈ S}›
  by (simp add: SyncPairlist.SKIPS_Syncptick_SKIPS SyncPairlist_tj_def)
    (auto intro!: Process_eqI_Dmin_version dest!: Dmin_GlobalNdet_subset[THEN set_mp]
      simp add: SKIPS_projs SKIP_projs GlobalNdet_projs split: if_split_asm)+

corollary SKIPS_SyncRlist_SKIPS [simp] :
  ‹SKIPS R ⟦A⟧✓Rlist SKIPS S = SKIPS {r # s |r s. r ∈ R ∧ s ∈ S}›
  by (simp add: SyncRlist.SKIPS_Syncptick_SKIPS SyncRlist_tj_def)
    (auto intro!: Process_eqI_Dmin_version dest!: Dmin_GlobalNdet_subset[THEN set_mp]
      simp add: SKIPS_projs SKIP_projs GlobalNdet_projs split: if_split_asm)+

corollary SKIPS_SyncLlist_SKIPS [simp] :
  ‹SKIPS R ⟦A⟧✓Llist SKIPS S = SKIPS {r @ [s] |r s. r ∈ R ∧ s ∈ S}›
  by (simp add: SyncRlist.Synchroptick_comm_dual.SKIPS_Syncptick_SKIPS SyncRlist_tj_dual_def)
    (auto intro!: Process_eqI_Dmin_version dest!: Dmin_GlobalNdet_subset[THEN set_mp]
      simp add: SKIPS_projs SKIP_projs GlobalNdet_projs split: if_split_asm)+




section ‹Operational Laws›

(* Do we need this ? *)

subsection ‹Classical Version›

locale After_SyncClassic = After_Synchroptick SyncClassic_tj
begin

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

end

locale AfterExt_SyncClassic =
  AfterExt_Synchroptick SyncClassic_tj

sublocale AfterExt_SyncClassic ⊆ After_SyncClassic
  by unfold_locales

locale OpSemTransitions_SyncClassic =
  OpSemTransitions_Synchroptick SyncClassic_tj

sublocale OpSemTransitions_SyncClassic ⊆ AfterExt_SyncClassic
  by unfold_locales


subsection ‹Product Type›

locale After_SyncPair = After_Synchroptick SyncPair_tj
begin

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

end

locale AfterExt_SyncPair =
  AfterExt_Synchroptick SyncPair_tj

sublocale AfterExt_SyncPair ⊆ After_SyncPair
  by unfold_locales

locale OpSemTransitions_SyncPair =
  OpSemTransitions_Synchroptick SyncPair_tj

sublocale OpSemTransitions_SyncPair ⊆ AfterExt_SyncPair
  by unfold_locales



subsection ‹List Type›

subsubsection ‹Pair›

locale After_SyncPairlist = After_Synchroptick SyncPairlist_tj
begin

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

end

locale AfterExt_SyncPairlist =
  AfterExt_Synchroptick SyncPairlist_tj

sublocale AfterExt_SyncPairlist ⊆ After_SyncPairlist
  by unfold_locales

locale OpSemTransitions_SyncPairlist =
  OpSemTransitions_Synchroptick SyncPairlist_tj

sublocale OpSemTransitions_SyncPairlist ⊆ AfterExt_SyncPairlist
  by unfold_locales



subsubsection ‹Right List›

locale After_SyncRlist = After_Synchroptick SyncRlist_tj
begin

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

end

locale AfterExt_SyncRlist =
  AfterExt_Synchroptick SyncRlist_tj

sublocale AfterExt_SyncRlist ⊆ After_SyncRlist
  by unfold_locales

locale OpSemTransitions_SyncRlist =
  OpSemTransitions_Synchroptick SyncRlist_tj

sublocale OpSemTransitions_SyncRlist ⊆ AfterExt_SyncRlist
  by unfold_locales



subsubsection ‹Left List›

locale After_SyncLlist = After_Synchroptick SyncRlist_tj_dual
begin

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

end

locale AfterExt_SyncLlist =
  AfterExt_Synchroptick SyncRlist_tj_dual

sublocale AfterExt_SyncLlist ⊆ After_SyncLlist
  by unfold_locales

locale OpSemTransitions_SyncLlist =
  OpSemTransitions_Synchroptick SyncRlist_tj_dual

sublocale OpSemTransitions_SyncLlist ⊆ AfterExt_SyncLlist
  by unfold_locales



subsubsection ‹Arbitrary Lists›

paragraph ‹Control on left side›

locale After_SyncListslenL =
  After_Synchroptick ‹SyncListslenL_tj lenL›
  for lenL :: nat
begin

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

end

locale AfterExt_SyncListslenL =
  AfterExt_Synchroptick ‹SyncListslenL_tj lenL›
  for lenL :: nat

sublocale AfterExt_SyncListslenL ⊆ After_SyncListslenL
  by unfold_locales

locale OpSemTransitions_SyncListslenL =
  OpSemTransitions_Synchroptick ‹SyncListslenL_tj lenL›
  for lenL :: nat

sublocale OpSemTransitions_SyncListslenL ⊆ AfterExt_SyncListslenL
  by unfold_locales



paragraph ‹Control on right side›

locale After_SyncListslenR =
  After_Synchroptick ‹SyncListslenL_tj_dual lenR›
  for lenR :: nat
begin

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

end

locale AfterExt_SyncListslenR =
  AfterExt_Synchroptick ‹SyncListslenL_tj_dual lenR›
  for lenR :: nat

sublocale AfterExt_SyncListslenR ⊆ After_SyncListslenR
  by unfold_locales

locale OpSemTransitions_SyncListslenR =
  OpSemTransitions_Synchroptick ‹SyncListslenL_tj_dual lenR›
  for lenR :: nat

sublocale OpSemTransitions_SyncListslenR ⊆ AfterExt_SyncListslenR
  by unfold_locales



paragraph ‹Control on both sides›

locale After_SyncLists =
  After_Synchroptick ‹SyncLists_tj lenL lenR› for lenL lenR :: nat
begin

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

end

locale AfterExt_SyncLists =
  AfterExt_Synchroptick ‹SyncLists_tj lenL lenR› for lenL lenR :: nat

sublocale AfterExt_SyncLists ⊆ After_SyncLists
  by unfold_locales

locale OpSemTransitions_SyncLists =
  OpSemTransitions_Synchroptick ‹SyncLists_tj lenL lenR› for lenL lenR :: nat

sublocale OpSemTransitions_SyncLists ⊆ AfterExt_SyncLists
  by unfold_locales


(*<*)
end
  (*>*)