Theory After_Operator_Non_Too_Destructive

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

section ‹Non too Destructiveness of After›

(*<*)
theory After_Operator_Non_Too_Destructive
  imports Process_Restriction_Space
    "HOL-CSP_OpSem.After_Trace_Operator" 
begin
  (*>*)


subsection ‹Equality›

lemma initials_restriction_processptick: ‹(P ↓ n)0 = (if n = 0 then UNIV else P0)›
  by (cases n, solves simp)
    (auto simp add: initials_def T_restriction_processptick,
      metis append.right_neutral append_eq_conv_conj drop_Nil drop_Suc_Cons)


lemma (in After) restriction_processptick_After:
  ‹P after e ↓ n = (if ev e ∈ P0 then (P ↓ Suc n) after e else Ψ P e ↓ n)›
proof (split if_split, intro conjI impI)
  show ‹ev e ∉ P0 ⟹ P after e ↓ n = Ψ P e ↓ n› by (simp add: not_initial_After)
next
  assume ‹ev e ∈ P0›
  show ‹P after e ↓ n = (P ↓ Suc n) after e› (is ‹?lhs = ?rhs›)
  proof (subst Process_eq_spec, safe)
    show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
      by (elim D_restriction_processptickE)
        (simp_all add: ‹ev e ∈ P0› After_projs
          initials_restriction_processptick D_restriction_processptick,
          meson Cons_eq_appendI eventptick.disc(1) length_Cons tickFree_Cons_iff)
  next
    show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
      by (auto simp add: D_After initials_restriction_processptick ‹ev e ∈ P0›
          D_restriction_processptick T_After Cons_eq_append_conv)
  next
    show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
      by (elim F_restriction_processptickE)
        (simp_all add: ‹ev e ∈ P0› After_projs
          initials_restriction_processptick F_restriction_processptick,
          meson Cons_eq_appendI eventptick.disc(1) length_Cons tickFree_Cons_iff)
  next
    show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
      by (auto simp add: F_After initials_restriction_processptick ‹ev e ∈ P0›
          F_restriction_processptick T_After Cons_eq_append_conv)
  qed
qed

lemma (in AfterExt) restriction_processptick_Aftertick:
  ‹P after✓ e ↓ n =
   (case e of ✓(r) ⇒ Ω P r ↓ n | ev x ⇒ if e ∈ P0 then (P ↓ Suc n) after✓ e else Ψ P x ↓ n)›
  by (simp add: Aftertick_def restriction_processptick_After split: eventptick.split )

lemma (in AfterExt) restriction_processptick_Aftertrace:
  ‹t ∈ 𝒯 P ⟹ tF t ⟹ P after𝒯 t ↓ n = (P ↓ (n + length t)) after𝒯 t›
proof (induct t arbitrary: n rule: rev_induct)
  show ‹P after𝒯 [] ↓ n = (P ↓ (n + length [])) after𝒯 []› for n by simp
next
  fix e t n
  assume   hyp : ‹t ∈ 𝒯 P ⟹ tF t ⟹ P after𝒯 t ↓ n = (P ↓ (n + length t)) after𝒯 t› for n
  assume prems : ‹t @ [e] ∈ 𝒯 P› ‹tickFree (t @ [e])›
  from prems(2) obtain a where ‹e = ev a› by (cases e) simp_all
  with initials_Aftertrace[OF prems(1)] have ‹ev a ∈ (P after𝒯 t)0› by simp
  from prems is_processT3_TR_append have ‹t ∈ 𝒯 P› ‹tF t› by auto
  from hyp[OF this] have ‹P after𝒯 t ↓ Suc n = (P ↓ (Suc n + length t)) after𝒯 t› .
  thus ‹P after𝒯 (t @ [e]) ↓ n = (P ↓ (n + length (t @ [e]))) after𝒯 (t @ [e])›
    by (simp add: Aftertrace_snoc restriction_processptick_Aftertick
        ‹e = ev a› ‹ev a ∈ (P after𝒯 t)0›)
qed



subsection ‹Non too Destructiveness›

lemma (in After) non_too_destructive_on_After :
  ‹non_too_destructive_on (λP. P after e) {P. ev e ∈ P0}›
  by (auto intro!: non_too_destructive_onI simp add: restriction_processptick_After)

lemma (in AfterExt) non_too_destructive_on_Aftertick :
  ‹non_too_destructive_on (λP. P after✓ e) {P. e ∈ P0}›
  if ‹⋀r. e = ✓(r) ⟹ non_too_destructive_on Ω {P. ✓(r) ∈ P0}›
proof (intro non_too_destructive_onI, clarify)
  fix P Q n assume * : ‹P ↓ Suc n = Q ↓ Suc n› ‹e ∈ P0› ‹e ∈ Q0›
  show ‹P after✓ e ↓ n = Q after✓ e ↓ n›
  proof (cases e)
    from "*" show ‹e = ev a ⟹ P after✓ e ↓ n = Q after✓ e ↓ n› for a
      by (simp add: restriction_processptick_Aftertick)
  next
    fix r assume ‹e = ✓(r)›
    with "*"(2, 3) have ‹P ∈ {P. ✓(r) ∈ P0}› ‹Q ∈ {P. ✓(r) ∈ P0}› by auto
    from non_too_destructive_onD[OF that[simplified ‹e = ✓(r)›, OF refl] this "*"(1)]
    have ‹Ω P ↓ n = Ω Q ↓ n› .
    with ‹e = ✓(r)› show ‹P after✓ e ↓ n = Q after✓ e ↓ n›
      by (simp add: restriction_processptick_Aftertick) (metis restriction_fun_def)
  qed
qed



lemma (in After) non_too_destructive_After :
  ‹non_too_destructive (λP. P after e)› if * : ‹non_too_destructive_on Ψ {P. ev e ∉ P0}›
proof (rule non_too_destructiveI)
  fix P Q :: ‹('a, 'r) processptick› and n
  assume ‹P ↓ Suc n = Q ↓ Suc n›
  hence ‹ev e ∈ P0 ∧ ev e ∈ Q0 ∨ ev e ∉ P0 ∧ ev e ∉ Q0›
    by (metis initials_restriction_processptick nat.distinct(1))
  thus ‹P after e ↓ n = Q after e ↓ n›
  proof (elim disjE conjE)
    show ‹ev e ∈ P0 ⟹ ev e ∈ Q0 ⟹ P after e ↓ n = Q after e ↓ n›
      by (simp add: restriction_processptick_After ‹P ↓ Suc n = Q ↓ Suc n›)
  next
    assume ‹ev e ∉ P0› ‹ev e ∉ Q0›
    hence ‹P after e = Ψ P e› ‹Q after e = Ψ Q e›
      by (simp_all add: not_initial_After)
    from ‹P ↓ Suc n = Q ↓ Suc n› have ‹Ψ P ↓ n = Ψ Q ↓ n›
      by (intro "*"[THEN non_too_destructive_onD, of P Q])
        (simp_all add: ‹ev e ∉ P0› ‹ev e ∉ Q0›)
    with ‹P after e = Ψ P e› ‹Q after e = Ψ Q e›
    show ‹P after e ↓ n = Q after e ↓ n› 
      by (metis restriction_fun_def)
  qed
qed


lemma (in AfterExt) non_too_destructive_Aftertick :
  ‹non_too_destructive (λP. P after✓ e)›
  if * : ‹⋀a. e = ev a ⟹ non_too_destructive_on Ψ {P. ev a ∉ P0}›
    ‹⋀r. e = ✓(r) ⟹ non_too_destructive (λP. Ω P r)›
proof (rule non_too_destructiveI)
  show ‹P after✓ e ↓ n = Q after✓ e ↓ n› if ‹P ↓ Suc n = Q ↓ Suc n› for P Q n
  proof (cases e)
    show ‹P after✓ e ↓ n = Q after✓ e ↓ n› if ‹e = ev a› for a
      by (simp add: Aftertick_def ‹e = ev a›)
        (fact non_too_destructive_After[OF "*"(1)[simplified ‹e = ev a›, OF refl],
            THEN non_too_destructiveD, OF ‹P ↓ Suc n = Q ↓ Suc n›])
  next
    fix r assume ‹e = ✓(r)›
    from "*"(2)[unfolded ‹e = ✓(r)›, OF refl,
        THEN non_too_destructiveD, OF ‹P ↓ Suc n = Q ↓ Suc n›]
    have ‹Ω P r ↓ n = Ω Q r ↓ n› .
    thus ‹P after✓ e ↓ n = Q after✓ e ↓ n›
      by (simp add: Aftertick_def ‹e = ✓(r)›)
  qed
qed


lemma (in AfterExt) restriction_shift_Aftertrace :
  ‹restriction_shift (λP. P after𝒯 t) (- int (length t))›
  if ‹non_too_destructive Ψ› ‹non_too_destructive Ω›
    ― ‹We could imagine more precise assumptions, but is it useful?›
proof (induct t)
  case Nil show ?case by (simp add: restriction_shiftI)
next
  case (Cons e t)
  have ‹non_too_destructive (λP. P after✓ e)›
    by (rule non_too_destructive_Aftertick)
      (simp add: ‹non_too_destructive Ψ›,
        metis non_too_destructive_fun_iff ‹non_too_destructive Ω›)
  hence * : ‹restriction_shift (λP. P after✓ e) (- 1)›
    unfolding non_too_destructive_def
      non_too_destructive_on_def restriction_shift_def .
  from restriction_shift_comp_restriction_shift[OF Cons.hyps "*"]
  show ?case by simp
qed


(*<*)
end
  (*>*)