Theory Prefixes_Constructive

(***********************************************************************************
 * 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 ‹Constructiveness of Prefixes›

(*<*)
theory Prefixes_Constructive
  imports Process_Restriction_Space
begin
  (*>*)

subsection ‹Equality›

lemma restriction_processptick_Mprefix :
  ‹□a ∈ A → P a ↓ n = (case n of 0 ⇒ ⊥ | Suc m ⇒ □a∈A → (P a ↓ m))› (is ‹?lhs = ?rhs›)
proof (cases n)
  show ‹n = 0 ⟹ ?lhs = ?rhs› by simp
next
  fix m assume ‹n = Suc m›
  show ‹?lhs = ?rhs›
  proof (rule Process_eq_optimizedI)
    show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
      by (auto simp add: ‹n = Suc m› Mprefix_projs D_restriction_processptick) blast
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    with D_imp_front_tickFree obtain a t'
      where ‹a ∈ A› ‹t = ev a # t'› ‹ftF t'› ‹t' ∈ 𝒟 (P a ↓ m)›
      by (auto simp add: ‹n = Suc m› D_Mprefix)
    thus ‹t ∈ 𝒟 ?lhs›
      by (simp add: ‹n = Suc m› D_restriction_processptick Mprefix_projs)
        (metis append_Cons eventptick.disc(1) length_Cons tickFree_Cons_iff)
  next
    show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
      by (auto simp add: ‹n = Suc m› restriction_processptick_projs Mprefix_projs)
  next
    show ‹(t, X) ∈ ℱ ?rhs ⟹ t ∉ 𝒟 ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
      by (auto simp add: ‹n = Suc m› restriction_processptick_projs Mprefix_projs)
  qed
qed


lemma restriction_processptick_Mndetprefix :
  ‹⊓a ∈ A → P a ↓ n = (case n of 0 ⇒ ⊥ | Suc m ⇒ ⊓a∈A → (P a ↓ m))› (is ‹?lhs = ?rhs›)
proof (cases n)
  show ‹n = 0 ⟹ ?lhs = ?rhs› by simp
next
  fix m assume ‹n = Suc m›
  show ‹?lhs = ?rhs›
  proof (rule Process_eq_optimizedI)
    show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
      by (auto simp add: ‹n = Suc m› Mndetprefix_projs D_restriction_processptick) blast
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    with D_imp_front_tickFree obtain a t'
      where ‹a ∈ A› ‹t = ev a # t'› ‹ftF t'› ‹t' ∈ 𝒟 (P a ↓ m)›
      by (auto simp add: ‹n = Suc m› D_Mndetprefix')
    thus ‹t ∈ 𝒟 ?lhs›
      by (simp add: ‹n = Suc m› D_restriction_processptick Mndetprefix_projs)
        (metis append_Cons eventptick.disc(1) length_Cons tickFree_Cons_iff)
  next
    show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
      by (auto simp add: ‹n = Suc m› restriction_processptick_projs
          Mndetprefix_projs split: if_split_asm)
  next
    show ‹(t, X) ∈ ℱ ?rhs ⟹ t ∉ 𝒟 ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
      by (auto simp add: ‹n = Suc m› restriction_processptick_projs
          Mndetprefix_projs split: if_split_asm)
  qed
qed


corollary restriction_processptick_write0 :
  ‹a → P ↓ n = (case n of 0 ⇒ ⊥ | Suc m ⇒ a → (P ↓ m))›
  unfolding write0_def by (simp add: restriction_processptick_Mprefix)


corollary restriction_processptick_write :
  ‹c!a → P ↓ n = (case n of 0 ⇒ ⊥ | Suc m ⇒ c!a → (P ↓ m))›
  unfolding write_def by (simp add: restriction_processptick_Mprefix)


corollary restriction_processptick_read :
  ‹c?a∈A → P a ↓ n = (case n of 0 ⇒ ⊥ | Suc m ⇒ c?a∈A → (P a ↓ m))›
  unfolding read_def comp_def by (simp add: restriction_processptick_Mprefix)


corollary restriction_processptick_ndet_write :
  ‹c!!a∈A → P a ↓ n = (case n of 0 ⇒ ⊥ | Suc m ⇒ c!!a∈A → (P a ↓ m))›
  unfolding ndet_write_def comp_def by (simp add: restriction_processptick_Mndetprefix)



subsection ‹Constructiveness›

lemma Mprefix_constructive : ‹constructive (λP. □a ∈ A → P a)›
  by (auto intro: constructiveI
      simp add: restriction_processptick_Mprefix restriction_fun_def)

lemma Mndetprefix_constructive : ‹constructive (λP. ⊓a ∈ A → P a)›
  by (auto intro: constructiveI
      simp add: restriction_processptick_Mndetprefix restriction_fun_def)

lemma write0_constructive : ‹constructive (λP. a → P)›
  by (auto intro: constructiveI simp add: restriction_processptick_write0)

lemma write_constructive : ‹constructive (λP. c!a → P)›
  by (auto intro: constructiveI simp add: restriction_processptick_write)

lemma read_constructive : ‹constructive (λP. c?a ∈ A → P a)›
  by (auto intro: constructiveI
      simp add: restriction_processptick_read restriction_fun_def)

lemma ndet_write_constructive : ‹constructive (λP. c!!a ∈ A → P a)›
  by (auto intro: constructiveI
      simp add: restriction_processptick_ndet_write restriction_fun_def)


(*<*)
end
  (*>*)