Theory Almost_Compactification

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


chapter‹ Other Results similar to Compactification ›

(*<*)
theory Almost_Compactification
  imports Process_Normalization
begin
  (*>*)

text ‹Unlike const‹Sync› and const‹Seq›, some operators like @{const [source] Det} do not enjoy
      a compactification result. Nevertheless, we still can prove some useful lemmas.›


section ‹Some preliminary Results›

lemma Mprefix_Det_Mprefix_bis :
  ‹(□a ∈ A → P a) □ (□b ∈ B → Q b) = 
   (□x ∈ (A ∩ B) → P x ⊓ Q x) □ (□a ∈ (A - B) → P a) □ (□b ∈ (B - A) → Q b)›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
    by (cases t) (auto simp add: F_Det F_Mprefix F_Ndet)
next
  show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
    by (cases t, simp_all add: F_Mprefix F_Ndet F_Det D_Det T_Det disjoint_iff) blast+
next
  show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    by (auto simp add: D_Det D_Mprefix image_iff D_Ndet)
next
  show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    by (auto simp add: D_Mprefix D_Ndet D_Det split: if_split_asm)
qed


lemma GlobalNdet_Ndet_GlobalNdet:
  ‹A ≠ {} ⟹ B ≠ {} ⟹ (⊓a ∈ A. P a) ⊓ (⊓b ∈ B. Q b) =
   ⊓x ∈ (A ∪ B). (if x ∈ A ∩ B then P x ⊓ Q x else if x ∈ A then P x else Q x)›
  by (simp add: Process_eq_spec F_Ndet D_Ndet F_GlobalNdet D_GlobalNdet, safe)
    (auto simp add: F_Ndet D_Ndet split: if_splits)

lemma GlobalNdet_Ndet_GlobalNdet_bis:
  ‹A ∩ B ≠ {} ⟹ A - B ≠ {} ⟹ B - A ≠ {} ⟹
   (⊓a ∈ A. P a) ⊓ (⊓b ∈ B. Q b) = 
   (⊓x ∈ (A ∩ B). P x ⊓ Q x) ⊓ (⊓a ∈ (A - B). P a) ⊓ (⊓b ∈ (B - A). Q b)›
  by (auto simp add: Process_eq_spec F_Ndet D_Ndet F_GlobalNdet D_GlobalNdet)


lemma GlobalNdet_GlobalNdet:
  ‹(⊓a ∈ A. ⊓b ∈ B a. P b) =
   (if ∀a ∈ A. B a ≠ {} then ⊓b ∈ (⋃a ∈ A. B a). P b else (⊓b ∈ (⋃a ∈ A. B a). P b) ⊓ STOP)›
  by (auto simp add: Process_eq_spec F_GlobalNdet D_GlobalNdet F_Ndet D_Ndet F_STOP D_STOP)




section ‹Results for @{const [source] Det}›

(* TODO: write results for SKIP, if possible *)

lemma P_nd_set_almost_compactification_Det :
  ‹(□ (s, A) ∈ s_A_set. P⟪A⟫nd s) =
   □e ∈ (⋃(s, A) ∈ s_A_set. ε A s) →
   ⊓(s, A) ∈ {(s, A) ∈ s_A_set. e ∈ ε A s}.
   ⊓s' ∈ τ A s e. P⟪A⟫nd s'› (is ‹?lhs = ?rhs›)
proof -
  have ‹?lhs = (□ (s, A) ∈ s_A_set. P_nd_step (ε A) (τ A) P⟪A⟫nd s)›
    by (auto intro: mono_GlobalDet_eq arg_cong[OF P_nd_rec])
  also have ‹… = □s_A ∈ s_A_set. P_nd_step (ε (snd s_A)) (τ (snd s_A)) P⟪snd s_A⟫nd (fst s_A)›
    by (simp only: case_prod_beta')
  also have ‹… = □e ∈ (⋃s_A ∈ s_A_set. ε (snd s_A) (fst s_A)) →
                  ⊓s_A ∈ {s_A ∈ s_A_set. e ∈ ε (snd s_A) (fst s_A)}. 
                  GlobalNdet (τ (snd s_A) (fst s_A) e) P⟪snd s_A⟫nd›
    by (simp add: GlobalDet_Mprefix)
  also have ‹… = ?rhs› by (simp add: case_prod_beta')
  finally show ‹?lhs = ?rhs› .
qed



lemma P_nd_set_almost_compactification_Det_bis :
  ‹(□ (s, A) ∈ s_A_set. P⟪A⟫nd s) =
   □e ∈ (⋃(s, A) ∈ s_A_set. ε A s) →
   ⊓(s', A) ∈ {(s', A)| s' s A. (s, A) ∈ s_A_set ∧ e ∈ ε A s ∧ s' ∈ τ A s e}. P⟪A⟫nd s'›
  (is ‹_ = ?rhs›)
  by (subst P_nd_set_almost_compactification_Det, intro mono_Mprefix_eq)
    (auto simp add: Process_eq_spec GlobalNdet_projs ε_simps split: if_split_asm, blast+)




lemma P_d_set_almost_compactification_Det:
  shows ‹(□ (s, A) ∈ s_A_set. P⟪A⟫d s) =
         □e ∈ (⋃(s, A) ∈ s_A_set. ε A s) →
         ⊓(s, A) ∈ {(s, A) ∈ s_A_set. e ∈ ε A s}. P⟪A⟫d ⌈τ A s e⌉› (is ‹?lhs = ?rhs›)
proof -
  have ‹?lhs = (□ (s, A) ∈ s_A_set. P_d_step (ε A) (τ A) P⟪A⟫d s)›
    by (auto intro: mono_GlobalDet_eq arg_cong[OF P_d_rec])
  also have ‹… = □s_A ∈ s_A_set. P_d_step (ε (snd s_A)) (τ (snd s_A)) P⟪snd s_A⟫d (fst s_A)›
    by (simp only: case_prod_beta')
  also have ‹… = □e ∈ (⋃s_A ∈ s_A_set. ε (snd s_A) (fst s_A)) →
                  ⊓s_A ∈ {s_A ∈ s_A_set. e ∈ ε (snd s_A) (fst s_A)}.
                  P⟪snd s_A⟫d ⌈τ (snd s_A) (fst s_A) e⌉›
    by (simp add: GlobalDet_Mprefix)
  also have ‹… = ?rhs› by (simp add: case_prod_beta')
  finally show ‹?lhs = ?rhs› .
qed




lemma P_d_set_almost_compactification_Det_bis:
  shows ‹(□ (s, A) ∈ s_A_set. P⟪A⟫d s) =
         □e ∈ (⋃(s, A) ∈ s_A_set. ε A s) →
         ⊓(s', A) ∈ {(⌈τ A s e⌉, A)| s A. (s, A) ∈ s_A_set ∧ e ∈ ε A s}. P⟪A⟫d s'›
  by (subst P_d_set_almost_compactification_Det, intro mono_Mprefix_eq)
    (auto simp add: Process_eq_spec GlobalNdet_projs ε_simps, (metis option.sel)+)





section ‹Results for @{const [source] Ndet}›

― ‹Possible ???›



section ‹Other Operators›

subsection ‹const‹initials››

lemma initials_PSKIPS_nd :
  ‹(PSKIPS⟪A⟫nd σ)0 = (if σ ∈ ρ A then tick ` ω A σ else ev ` ε A σ)›
  by (subst PSKIPS_nd_rec) (simp add: initials_Mprefix ρ_simps)

lemma initials_PSKIPS_d :
  ‹(PSKIPS⟪A⟫d σ)0 = (if σ ∈ ρ A then {✓(⌈ω A σ⌉)} else ev ` ε A σ)›
  by (subst PSKIPS_d_rec) (auto simp add: initials_Mprefix ρ_simps)

lemma initials_P_nd : ‹(P⟪A⟫nd s)0 = ev ` ε A s›
  by (subst P_nd_rec) (simp_all add: initials_Mprefix)

lemma initials_P_d : ‹(P⟪A⟫d s)0 = ev ` ε A s›
  by (subst P_d_rec) (simp add: initials_Mprefix)



subsection ‹const‹Throw››

lemma Throw_PSKIPS_nd :
  ‹PSKIPS⟪A⟫nd σ Θ b ∈ B. Q b =
   (if σ ∈ ρ A then SKIPS (ω A σ) else
    □a∈ε A σ → (if a ∈ B then Q a else ⊓σ' ∈ τ A σ a. (PSKIPS⟪A⟫nd σ' Θ b ∈ B. Q b)))›
  by (auto simp add: PSKIPS_nd_rec_in_ρ Throw_disjoint_events_of
      events_of_SKIPS PSKIPS_nd_rec_notin_ρ Throw_Mprefix
      Throw_distrib_GlobalNdet_right
      intro: mono_Mprefix_eq)

lemma Throw_PSKIPS_d :
  ‹PSKIPS⟪A⟫d σ Θ b ∈ B. Q b =
   (if σ ∈ ρ A then SKIP ⌈ω A σ⌉ else
    □a∈ε A σ → (if a ∈ B then Q a else PSKIPS⟪A⟫d ⌈τ A σ a⌉ Θ b ∈ B. Q b))›
  by (simp add: PSKIPS_d_rec_in_ρ PSKIPS_d_rec_notin_ρ Throw_Mprefix)

lemma Throw_P_nd :
  ‹P⟪A⟫nd σ Θ b ∈ B. Q b =
   □a∈ε A σ → (if a ∈ B then Q a else ⊓σ' ∈ τ A σ a. (P⟪A⟫nd σ' Θ b ∈ B. Q b))›
  by (subst P_nd_rec)
    (auto simp add: Throw_Mprefix Throw_distrib_GlobalNdet_right intro: mono_Mprefix_eq)

lemma Throw_P_d :
  ‹P⟪A⟫d σ Θ b ∈ B. Q b =
   □a∈ε A σ → (if a ∈ B then Q a else P⟪A⟫d ⌈τ A σ a⌉ Θ b ∈ B. Q b)›
  by (subst P_d_rec) (simp add: Throw_Mprefix)



subsection ‹const‹Interrupt››

lemma SKIPS_Interrupt_is_SKIPS_Det :
  ‹SKIPS R △ P = SKIPS R □ P›
  by (auto simp add: SKIPS_def Interrupt_distrib_GlobalNdet_right
      Det_distrib_GlobalNdet_right SKIP_Interrupt_is_SKIP_Det intro: mono_GlobalNdet_eq)

lemma Interrupt_PSKIPS_nd :
  ‹PSKIPS⟪A⟫nd σ △ Q =
   Q □ (if σ ∈ ρ A then SKIPS (ω A σ) else □a ∈ ε A σ → ⊓σ' ∈ τ A σ a. PSKIPS⟪A⟫nd σ' △ Q)›
  by (subst PSKIPS_nd_rec)
    (auto simp add: Interrupt_Mprefix SKIPS_Interrupt_is_SKIPS_Det Det_commute
      ρ_simps ε_simps Interrupt_distrib_GlobalNdet_right
      intro!: arg_cong2[where f = ‹(□)›] mono_Mprefix_eq split: if_split_asm)

lemma Interrupt_PSKIPS_d :
  ‹PSKIPS⟪A⟫d σ △ Q =
   Q □ (if σ ∈ ρ A then SKIP ⌈ω A σ⌉ else □a ∈ ε A σ → PSKIPS⟪A⟫d ⌈τ A σ a⌉ △ Q)›
  by (simp add: Det_commute Interrupt_Mprefix PSKIPS_d_rec_in_ρ
      PSKIPS_d_rec_notin_ρ SKIP_Interrupt_is_SKIP_Det)

lemma Interrupt_P_nd :
  ‹P⟪A⟫nd σ △ Q = Q □ (□a ∈ ε A σ → ⊓σ' ∈ τ A σ a. P⟪A⟫nd σ' △ Q)›
  by (subst P_nd_rec)
    (auto simp add: Interrupt_Mprefix Interrupt_distrib_GlobalNdet_right ε_simps
      intro!: arg_cong2[where f = ‹(□)›] mono_Mprefix_eq split: if_split_asm)

lemma Interrupt_P_d :
  ‹P⟪A⟫d σ △ Q = Q □ (□a ∈ ε A σ → P⟪A⟫d ⌈τ A σ a⌉ △ Q)›
  by (metis Interrupt_Mprefix P_d_rec)


(* TODO: see if we also write lemmas when Q is a procOmata *)


subsection ‹After›

context After
begin

lemma After_SKIPS : ‹SKIPS R after a = Ψ (SKIPS R) a›
  by (simp add: Process_eq_spec After_projs image_iff)

lemma After_PSKIPS_nd :
  ‹PSKIPS⟪A⟫nd σ after a =
   (if σ ∈ ρ A then Ψ (SKIPS (ω A σ)) a else 
    if a ∈ ε A σ then ⊓σ' ∈ τ A σ a. PSKIPS⟪A⟫nd σ' else Ψ (PSKIPS⟪A⟫nd σ) a)›
  by (subst (1 4) PSKIPS_nd_rec)
    (simp add: ε_simps ρ_simps After_SKIPS After_Mprefix)

lemma After_PSKIPS_d :
  ‹PSKIPS⟪A⟫d σ after a =
   (if σ ∈ ρ A then Ψ (SKIP ⌈ω A σ⌉) a else 
    if a ∈ ε A σ then PSKIPS⟪A⟫d ⌈τ A σ a⌉ else Ψ (PSKIPS⟪A⟫d σ) a)›
  by (subst (1 2) PSKIPS_d_rec)
    (auto simp add: ε_simps ρ_simps After_SKIP After_Mprefix)

lemma After_P_nd :
  ‹P⟪A⟫nd σ after a = (if a ∈ ε A σ then ⊓σ' ∈ τ A σ a. P⟪A⟫nd σ' else Ψ (P⟪A⟫nd σ) a)›
  by (subst (1 4) P_nd_rec) (simp add: ε_simps After_Mprefix)

lemma After_P_d :
  ‹P⟪A⟫d σ after a = (if a ∈ ε A σ then P⟪A⟫d ⌈τ A σ a⌉ else Ψ (P⟪A⟫d σ) a)›
  by (subst (1 2) P_d_rec)
    (simp add: ε_simps After_SKIP After_Mprefix)

end


context AfterExt
begin

lemma Aftertick_SKIPS :
  ‹SKIPS R after✓ e = (case e of ev a ⇒ Ψ (SKIPS R) a | ✓(r) ⇒ Ω (SKIPS R) r)›
  by (cases e) (simp_all add: Aftertick_def After_SKIPS)

lemma Aftertick_PSKIPS_nd :
  ‹PSKIPS⟪A⟫nd σ after✓ e =
   (case e of ev a ⇒ if σ ∈ ρ A then Ψ (SKIPS (ω A σ)) a else 
                      if a ∈ ε A σ then ⊓σ' ∈ τ A σ a. PSKIPS⟪A⟫nd σ' else Ψ (PSKIPS⟪A⟫nd σ) a
            | ✓(r) ⇒ if σ ∈ ρ A then Ω (SKIPS (ω A σ)) r else Ω (PSKIPS⟪A⟫nd σ) r)›
proof (cases e)
  show ‹e = ev a ⟹ ?thesis› for a
    by (simp add: After_PSKIPS_nd Aftertick_def)
next
  show ‹e = ✓(r) ⟹ ?thesis› for r
    by (subst (1 5) PSKIPS_nd_rec) (simp add: Aftertick_def ρ_simps)
qed

lemma Aftertick_PSKIPS_d :
  ‹PSKIPS⟪A⟫d σ after✓ e =
   (case e of ev a ⇒ if σ ∈ ρ A then Ψ (SKIP ⌈ω A σ⌉) a else 
                      if a ∈ ε A σ then PSKIPS⟪A⟫d ⌈τ A σ a⌉ else Ψ (PSKIPS⟪A⟫d σ) a
            | ✓(r) ⇒ if σ ∈ ρ A then Ω (SKIP ⌈ω A σ⌉) r else Ω (PSKIPS⟪A⟫d σ) r)›
proof (cases e)
  show ‹e = ev a ⟹ ?thesis› for a
    by (simp add: After_PSKIPS_d Aftertick_def)
next
  show ‹e = ✓(r) ⟹ ?thesis› for r
    by (subst (1 2) PSKIPS_d_rec) (auto simp add: Aftertick_def ρ_simps)
qed

lemma Aftertick_P_nd :
  ‹P⟪A⟫nd σ after✓ e =
   (case e of ev a ⇒ if a ∈ ε A σ then ⊓σ' ∈ τ A σ a. P⟪A⟫nd σ' else Ψ (P⟪A⟫nd σ) a
            | ✓(r) ⇒ Ω (P⟪A⟫nd σ) r)›
proof (cases e)
  show ‹e = ev a ⟹ ?thesis› for a
    by (simp add: After_P_nd Aftertick_def)
next
  show ‹e = ✓(r) ⟹ ?thesis› for r
    by (subst (1 2) P_nd_rec) (auto simp add: Aftertick_def)
qed


lemma Aftertick_P_d :
  ‹P⟪A⟫d σ after✓ e =
   (case e of ev a ⇒ if a ∈ ε A σ then P⟪A⟫d ⌈τ A σ a⌉ else Ψ (P⟪A⟫d σ) a
            | ✓(r) ⇒ Ω (P⟪A⟫d σ) r)›
proof (cases e)
  show ‹e = ev a ⟹ ?thesis› for a
    by (simp add: After_P_d Aftertick_def)
next
  show ‹e = ✓(r) ⟹ ?thesis› for r
    by (subst (1 2) P_d_rec) (auto simp add: Aftertick_def)
qed


end


section ‹OpSem›

context OpSemTransitions
begin

lemma SKIPS_τ_trans_SKIP : ‹r ∈ R ⟹ SKIPS R ↝τ SKIP r›
  by (simp add: SKIPS_def τ_trans_GlobalNdet)



text ‹
In the ProcOmata, we will absorb the ‹τ› transitions
that appear when we unfold the fixed-point operator.
›

lemma τ_trans_PSKIPS_nd :
  ‹r ∈ ω A σ ⟹ PSKIPS⟪A⟫nd σ ↝τ SKIP r›
  by (subst PSKIPS_nd_rec) (auto simp add: SKIPS_τ_trans_SKIP)

lemma τ_trans_PSKIPS_d :
  ‹σ ∈ ρ A ⟹ PSKIPS⟪A⟫d σ ↝✓⇘⌈ω A σ⌉⇙ Ω (SKIP ⌈ω A σ⌉) ⌈ω A σ⌉›
  by (auto simp add: PSKIPS_d_rec SKIP_trans_tick_Ω_SKIP ρ_simps)


lemma ev_trans_PSKIPS_nd :
  ‹σ ∉ ρ A ⟹ σ' ∈ τ A σ a ⟹ PSKIPS⟪A⟫nd σ ↝⇘a⇙ PSKIPS⟪A⟫nd σ'›
  by (subst PSKIPS_nd_rec)
    (auto simp add: ρ_simps ε_simps
             intro: ev_trans_τ_trans[OF ev_trans_Mprefix τ_trans_GlobalNdet])

lemma ev_trans_PSKIPS_d :
  ‹σ ∉ ρ A ⟹ a ∈ ε A σ ⟹ PSKIPS⟪A⟫d σ ↝⇘a⇙ PSKIPS⟪A⟫d ⌈τ A σ a⌉›
  by (subst PSKIPS_d_rec)
    (auto simp add: ρ_simps intro: ev_trans_Mprefix)

lemma ev_trans_P_nd :
  ‹σ' ∈ τ A σ a ⟹ P⟪A⟫nd σ ↝⇘a⇙ P⟪A⟫nd σ'›
  by (subst P_nd_rec)
    (auto simp add: ε_simps
             intro: ev_trans_τ_trans[OF ev_trans_Mprefix τ_trans_GlobalNdet])

lemma ev_trans_P_d :
  ‹a ∈ ε A σ ⟹ P⟪A⟫d σ ↝⇘a⇙ P⟪A⟫d ⌈τ A σ a⌉›
  by (subst P_d_rec) (auto intro: ev_trans_Mprefix)



end

(*<*)
end
  (*>*)