Theory Comparison_He_Hoare

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : Comparison with the work of He and Hoare:
 *                   From algebra to operational semantics
 *
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * 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 list of conditions and the following disclaimer.
 *
 *     * 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.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * 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
 * OWNER 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.
 ******************************************************************************›
(*>*)

chapter ‹ Comparison with He and Hoare ›

(*<*)
theory  Comparison_He_Hoare
  imports Operational_Semantics_Laws "HOL-Library.LaTeXsugar"
begin
  (*>*)


lemma (in After) initial_ev_imp_eq_prefix_After_Sliding :
  ‹P = (e → (P after e)) ⊳ P› if ‹ev e ∈ P0›
proof (subst Process_eq_spec, safe)
  show ‹(s, X) ∈ ℱ P ⟹ (s, X) ∈ ℱ ((e → (P after e)) ⊳ P)› for s X
    by (simp add: F_Sliding)
next
  show ‹(s, X) ∈ ℱ ((e → (P after e)) ⊳ P) ⟹ (s, X) ∈ ℱ P› for s X
    by (cases s) (auto simp add: F_Sliding write0_def F_Mprefix F_After ‹ev e ∈ P0›)
next
  show ‹s ∈ 𝒟 P ⟹ s ∈ 𝒟 ((e → (P after e)) ⊳ P)› for s
    by (simp add: D_Sliding)
next
  show ‹s ∈ 𝒟 ((e → (P after e)) ⊳ P) ⟹ s ∈ 𝒟 P› for s
    by (cases s) (auto simp add: D_Sliding write0_def D_Mprefix D_After ‹ev e ∈ P0›)
qed



context OpSemTransitions
begin

(* not really useful since we need an additional assumption
   to establish something like FD @{thm FD_iff_eq_Ndet} *)

(* lemma ‹P ⊑FD Q ⟷ P = P ⊓ Q› by (fact FD_iff_eq_Ndet) *)

abbreviation τ_eq :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infix ‹=τ› 50)
  where ‹P =τ Q ≡ P ↝τ Q ∧ Q ↝τ P›

lemma τ_eqI  : ‹P ↝τ Q ⟹ Q ↝τ P ⟹ P =τ Q›
  and τ_eqD1 : ‹P =τ  Q ⟹ P ↝τ Q›
  and τ_eqD2 : ‹P =τ  Q ⟹ Q ↝τ P›
  by simp_all

lemma τ_trans_iff_τ_eq_Ndet:
  ‹∀P Q P' Q'. P ↝τ P' ⟶ Q ↝τ Q' ⟶ P ⊓ Q ↝τ P' ⊓ Q' ⟹ P ↝τ Q ⟷ P =τ P ⊓ Q›
  by (metis Ndet_id τ_trans_NdetL τ_trans_NdetR τ_trans_transitivity)

lemma eq_imp_τ_eq: ‹P = Q ⟹ P =τ Q› by (simp add: τ_trans_eq)



definition ev_transHOARE :: ‹('a, 'r) processptick ⇒ 'a ⇒ ('a, 'r) processptick ⇒ bool› (‹_ ⇘HOARE⇙↝⇘_⇙ _› [50, 3, 51] 50)
  where ‹P ⇘HOARE⇙↝⇘e⇙ Q ≡ P ↝τ (e → Q) □ P›


lemma ev_transHOARE_imp_in_initials:
  ‹P ⇘HOARE⇙↝⇘e⇙ Q ⟹ ev e ∈ P0›
  using τ_trans_ev_trans ev_trans_DetL ev_trans_prefix unfolding ev_transHOARE_def by blast


lemma ev_transHOARE_imp_ev_trans: ‹P ↝⇘e⇙ Q› if ‹P ⇘HOARE⇙↝⇘e⇙ Q›
proof (rule conjI)
  from ‹P ⇘HOARE⇙↝⇘e⇙ Q› show ‹ev e ∈ P0› by (fact ev_transHOARE_imp_in_initials)

  from ‹P ⇘HOARE⇙↝⇘e⇙ Q›[unfolded ev_transHOARE_def]
  have ‹P after✓ ev e ↝τ ((e → Q) □ P) after✓ ev e›
    by (rule τ_trans_mono_Aftertick[rotated]) (simp add: initials_Det initials_write0)
  moreover have ‹… = Q ⊓ (P after✓ ev e)›
    by (simp add: Aftertick_Det ‹ev e ∈ P0› initials_write0 Aftertick_write0)
  moreover have ‹… ↝τ Q› by (fact τ_trans_NdetL)
  ultimately show ‹P after✓ ev e ↝τ Q›
    using ‹ev e ∈ P0› ev_trans_τ_trans by presburger
qed



text ‹Two assumptions on ‹τ› transitions are necessary in the following proof, but are automatic
      when we instantiate term‹(↝τ)› with term‹(⊑FD)›, term‹(⊑DT)›, term‹(⊑F)› or term‹(⊑T)›.›

lemma hyps_on_τ_trans_imp_ev_trans_imp_ev_transHOARE: ‹P ⇘HOARE⇙↝⇘e⇙ Q›
  if non_BOT_τ_trans_DetL : ‹∀P P' Q. P = ⊥ ∨ P' ≠ ⊥ ⟶ P ↝τ P' ⟶ P □ Q ↝τ P' □ Q›
    and τ_trans_prefix      : ‹∀P P' e. P ↝τ P' ⟶ (e → P) ↝τ (e → P')›
    and ‹P ↝⇘e⇙ Q›
proof (unfold ev_transHOARE_def)
  show ‹P ↝τ (e → Q) □ P›
  proof (rule τ_trans_transitivity)
    have ‹P = (e → (P after e)) ⊳ P›
      by (simp add: initial_ev_imp_eq_prefix_After_Sliding ‹P ↝⇘e⇙ Q›)
    also have ‹(e → (P after e)) ⊳ P ↝τ (e → (P after e)) □ P›
      by (simp add: Sliding_def τ_trans_NdetL)
    finally show ‹P ↝τ (e → (P after e)) □ P› .
  next
    show ‹(e → (P after e)) □ P ↝τ (e → Q) □ P›
      by (rule non_BOT_τ_trans_DetL[rule_format],
          solves ‹simp add: write0_def›)
        (rule τ_trans_prefix[rule_format],
          fact ‹P ↝⇘e⇙ Q›[simplified ev_trans_is, THEN conjunct2])
  qed
qed


―‹Of course, we obtain an equivalence.›
lemma hyps_on_τ_trans_imp_ev_transHOARE_iff_ev_trans:
  ‹∀P P' Q. P = ⊥ ∨ P' ≠ ⊥ ⟶ P ↝τ P' ⟶ P □ Q ↝τ P' □ Q ⟹
   ∀P P' e. P ↝τ P' ⟶ (e → P) ↝τ (e → P') ⟹ P ⇘HOARE⇙↝⇘e⇙ Q ⟷ P ↝⇘e⇙ Q›
  by (rule iffI[OF ev_transHOARE_imp_ev_trans hyps_on_τ_trans_imp_ev_trans_imp_ev_transHOARE])


―‹When term‹P = ⊥›, we have the following result.›
lemma BOT_ev_transHOARE_anything: ‹⊥ ⇘HOARE⇙↝⇘e⇙ P›
proof -
  have ‹⊥ = (e → P) □ ⊥› by simp
  thus ‹⊥ ⇘HOARE⇙↝⇘e⇙ P› unfolding ev_transHOARE_def by (simp add: τ_trans_eq)
qed


―‹Finally, again under two (automatic during instantiation) assumption on term‹(↝τ)›,
   we have an equivalent definition with an ‹τ› equality instead of a ‹τ› transition.›
lemma hyps_on_τ_trans_imp_ev_transHOARE_def_bis: ‹P ⇘HOARE⇙↝⇘e⇙ Q ⟷ P =τ (e → Q) ⊳ P›
  if non_BOT_τ_trans_SlidingL : ‹∀P P' Q. P = ⊥ ∨ P' ≠ ⊥ ⟶ P ↝τ P' ⟶ P ⊳ Q ↝τ P' ⊳ Q›
    and τ_trans_prefix           : ‹∀P P' e. P ↝τ P' ⟶ (e → P) ↝τ (e → P')›
proof (rule iffI)
  show ‹P =τ (e → Q) ⊳ P ⟹ P ⇘HOARE⇙↝⇘e⇙ Q›
    by (metis Sliding_def τ_trans_NdetL τ_trans_transitivity ev_transHOARE_def)
next
  show ‹P =τ (e → Q) ⊳ P› if ‹P ⇘HOARE⇙↝⇘e⇙ Q›
  proof (rule τ_eqI)
    show ‹(e → Q) ⊳ P ↝τ P› by (simp add: τ_trans_SlidingR)
  next
    from ‹P ⇘HOARE⇙↝⇘e⇙ Q› have ‹P = (e → (P after e)) ⊳ P›
      by (simp add: ev_transHOARE_imp_in_initials initial_ev_imp_eq_prefix_After_Sliding)
    also have ‹… ↝τ (e → Q) ⊳ P›
      by (rule non_BOT_τ_trans_SlidingL[rule_format],
          solves ‹simp add: write0_def›)
        (rule τ_trans_prefix[rule_format],
          fact ‹P ⇘HOARE⇙↝⇘e⇙ Q›[THEN ev_transHOARE_imp_ev_trans,
            unfolded ev_trans_is, THEN conjunct2])
    finally show ‹P ↝τ (e → Q) ⊳ P› .
  qed
qed


end


context OpSemFD
begin

notation ev_transHOARE (‹_ ⇘FD-HOARE⇙↝⇘_⇙ _› [50, 3, 51] 50)
notation τ_eq (infix ‹FD=τ› 50)

theorem ev_transHOARE_iff_ev_trans : ‹P ⇘FD-HOARE⇙↝⇘e⇙ Q ⟷ P FD↝⇘e⇙ Q›
  by (simp add: τ_trans_DetL hyps_on_τ_trans_imp_ev_transHOARE_iff_ev_trans mono_write0_FD)

theorem ev_transHOARE_def_bis: ‹P ⇘FD-HOARE⇙↝⇘e⇙ Q ⟷ P FD=τ (e → Q) ⊳ P›
  by (simp add: τ_trans_SlidingL hyps_on_τ_trans_imp_ev_transHOARE_def_bis mono_write0_FD)

end


context OpSemDT
begin

notation ev_transHOARE (‹_ ⇘DT-HOARE⇙↝⇘_⇙ _› [50, 3, 51] 50)
notation τ_eq (infix ‹DT=τ› 50)

theorem ev_transHOARE_iff_ev_trans : ‹P ⇘DT-HOARE⇙↝⇘e⇙ Q ⟷ P DT↝⇘e⇙ Q›
  by (simp add: τ_trans_DetL hyps_on_τ_trans_imp_ev_transHOARE_iff_ev_trans mono_write0_DT)

theorem ev_transHOARE_def_bis: ‹P ⇘DT-HOARE⇙↝⇘e⇙ Q ⟷ P DT=τ (e → Q) ⊳ P›
  by (simp add: τ_trans_SlidingL hyps_on_τ_trans_imp_ev_transHOARE_def_bis mono_write0_DT)

end


context OpSemF
begin

notation ev_transHOARE (‹_ ⇘F-HOARE⇙↝⇘_⇙ _› [50, 3, 51] 50)
notation τ_eq (infix ‹F=τ› 50)

theorem ev_transHOARE_iff_ev_trans : ‹P ⇘F-HOARE⇙↝⇘e⇙ Q ⟷ P F↝⇘e⇙ Q›
  by (simp add: hyps_on_τ_trans_imp_ev_transHOARE_iff_ev_trans τ_trans_DetL mono_write0_F)

theorem ev_transHOARE_def_bis: ‹P ⇘F-HOARE⇙↝⇘e⇙ Q ⟷ P F=τ (e → Q) ⊳ P›
  by (simp add: hyps_on_τ_trans_imp_ev_transHOARE_def_bis τ_trans_SlidingL mono_write0_F)


end


context OpSemT
begin

notation ev_transHOARE (‹_ ⇘T-HOARE⇙↝⇘_⇙ _› [50, 3, 51] 50)
notation τ_eq (infix ‹T=τ› 50)

theorem ev_transHOARE_iff_ev_trans : ‹P ⇘T-HOARE⇙↝⇘e⇙ Q ⟷ P T↝⇘e⇙ Q›
  using τ_trans_DetL ev_transHOARE_imp_ev_trans hyps_on_τ_trans_imp_ev_trans_imp_ev_transHOARE
    mono_write0_T by blast

theorem ev_transHOARE_def_bis: ‹P ⇘T-HOARE⇙↝⇘e⇙ Q ⟷ P T=τ (e → Q) ⊳ P›
  by (simp add: τ_trans_SlidingL hyps_on_τ_trans_imp_ev_transHOARE_def_bis mono_write0_T)

end

(*<*)
end
  (*>*)