Theory OpSemGenericBis

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : Common work for operational semantics based on refinements bis
 *
 * Copyright (c) 2023 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‹ Generic Operational Semantics as a Locale, bis›

theory  OpSemGenericBis
  imports AfterTraceBis "HOL-CSPM.DeadlockResults"
begin

section ‹Definition›

locale OpSemGeneric = 
    fixes τ_trans ::  process   process  bool (infixl τ 50)
  assumes τ_trans_NdetL: P  Q τ P
      and τ_trans_transitivity: P τ Q  Q τ R  P τ R
      and τ_trans_anti_mono_ready_set: P τ Q  ready_set Q  ready_set P
      and τ_trans_mono_AfterExt:
          e  ready_set Q  P τ Q  P afterExt e τ Q afterExt e
begin

text ‹This locale needs to be instantiated with a binary
      relation @{term [show_types] (↝τ)} which:
       is compatible with constNdet
       is transitive
       makes constready_set anti-monotonic
       makes @{const [source] AfterExt} monotonic.›

text ‹From the τ› transition termP τ Q we derive the event transition as follows:›

abbreviation event_trans ::  process   event   process  bool (‹_/ _/ _› [50, 3, 51] 50)
  where P e Q  e  ready_set P  P afterExt e τ Q


text ‹From idempotence, commutativity and term absorbance of term(⊓), 
      we get the following for free.›

lemma τ_trans_eq: P τ P
  and τ_trans_NdetR: P  Q τ Q
  and BOT_τ_trans_anything:  τ P
  and BOT_ev_trans_anything:  (ev e) P
  by (metis Ndet_id τ_trans_NdetL,
      metis Ndet_commute τ_trans_NdetL,
      metis Ndet_BOT τ_trans_NdetL,
      metis AfterExt_BOT Ndet_BOT UNIV_I τ_trans_NdetL event.simps(3) ready_set_BOT) 


text ‹As immediate consequences of the axioms, we prove that event transitions 
      absorb τ› transitions on right and on left.›

lemma event_trans_τ_trans: P  e P'  P' τ P''   P  e P''
  by (meson τ_trans_transitivity)

lemma τ_trans_event_trans: P τ P'   P'  e P''  P  e P''
  using τ_trans_mono_AfterExt τ_trans_transitivity τ_trans_anti_mono_ready_set by blast



text ‹We can now define the concept of transition with a trace 
      and demonstrate the first properties.›

inductive trace_trans ::  process   trace   process  bool (‹_/ *_/ _› [50, 3, 51] 50)
  where    trace_τ_trans : P τ P'  P * [] P'
  |     trace_tick_trans : P   P'  P * [] P'
  |  trace_Cons_ev_trans :
     P (ev e) P'  P' * s P''  P * (ev e) # s P''


lemma trace_trans_τ_trans: P *s P'  P' τ P''  P *s P''
  apply (induct rule: trace_trans.induct)
  subgoal using τ_trans_transitivity trace_τ_trans by blast
  subgoal using event_trans_τ_trans trace_tick_trans by blast
  using trace_Cons_ev_trans by blast
  

lemma τ_trans_trace_trans:  P τ P'  P' *s P''  P *s P''
  apply (rotate_tac, induct rule: trace_trans.induct)
  subgoal using τ_trans_transitivity trace_τ_trans by blast
  subgoal using τ_trans_event_trans trace_tick_trans by blast
  using τ_trans_event_trans trace_Cons_ev_trans by blast


lemma tickFree_if_trans_trans_not_STOP : 
  P *s Q  Q  STOP  tickFree s
  by (induct rule: trace_trans.induct, simp_all)
     (metis τ_trans_anti_mono_ready_set bot.extremum_uniqueI 
            ready_set_AfterExt ready_set_empty_iff_STOP)


lemma BOT_trace_trans_tickFree_anything : tickFree s   *s P
proof (induct s arbitrary: P)
  show P. tickFree []   *[] P
    by (simp add: BOT_τ_trans_anything trace_τ_trans)
next
  fix e s P
  assume prem: tickFree (e # s) and hyp: tickFree s   *s P for P
  have * : tickFree s using prem by auto
  obtain e' where e = ev e' using event.exhaust prem by auto
  thus  *e # s P
    by simp (rule trace_Cons_ev_trans[OF _ hyp];
             simp add: * AfterExt_BOT BOT_τ_trans_anything ready_set_BOT)
qed


section‹Consequences of termP *s Q on term, term𝒯 and term𝒟
  
lemma trace_trans_imp_F_if_τ_trans_imp_leF: 
  P *s Q  X   Q  (s, X)   P
  if P Q. P τ Q  P F Q
proof (induct rule: trace_trans.induct)
  show P τ Q  X   Q  ([], X)   P for P Q
    by (meson failure_refine_def in_mono Refusals_iff that)
next
  show P  Q  X   Q  ([], X)   P for P Q
    by (metis append_Nil mem_Collect_eq ready_set_def tick_T_F)
next
  fix P e Q s Q'
  assume * : P (ev e) Q X   Q'  (s, X)   Q X   Q'
  have P afterExt ev e F Q using *(1) that by blast
  hence (s, X)   (P afterExt ev e) by (simp add: failure_refine_def subsetD *(2, 3))
  thus (ev e # s, X)   P by (simp add: F_AfterExt *(1)) (metis list.exhaust_sel)
qed


lemma trace_trans_imp_T_if_τ_trans_imp_leT: P *s Q  s  𝒯 P 
  if P Q. P τ Q  P T Q
proof (induct rule: trace_trans.induct)
  show P τ Q  []  𝒯 P for P Q
    by (simp add: Nil_elem_T)
next
  show P  Q  []  𝒯 P for P Q
    by (simp add: ready_set_def)
next
  fix P e Q s Q'
  assume * : P (ev e) Q s  𝒯 Q
  have P afterExt ev e T Q using *(1) that by blast
  hence s  𝒯 (P afterExt ev e) by (simp add: *(2) subsetD trace_refine_def)
  with *(1) list.collapse show ev e # s  𝒯 P 
    by (force simp add: T_AfterExt ready_set_def)
qed


lemma trace_trans_BOT_imp_D_if_τ_trans_imp_leD: P *s   s  𝒟 P 
  if P Q. P τ Q  P D Q
proof (induct s arbitrary: P)
  show P. P *[]   []  𝒟 P
    by (subst (asm) trace_trans.simps, auto) 
       (meson BOT_iff_D divergence_refine_def subsetD that)
next
  fix e s P
  assume prem : P *e # s  
  assume hyp: P *s   s  𝒟 P for P
  have P afterExt e *s 
    using prem by (cases rule: trace_trans.cases)
                  (auto simp add:  trace_τ_trans intro: τ_trans_trace_trans)
  from hyp[OF this] show e # s  𝒟 P
    by (auto simp add: D_AfterExt D_UU split: if_split_asm)
qed



section‹Characterizations for termP *s Q

text ‹The following results require a lot of work, but will be very useful.›

lemma trace_trans_iff :
  P * [] Q  P τ Q
  P * [] Q  P  Q
  P * (ev e) # s Q'  (Q. P (ev e) Q  Q * s Q')
  tickFree s  (P * s @ [f] Q')  (Q. P *s Q  Q f Q')
  front_tickFree (s @ t)  (P *s @ t Q')  (Q. P *s Q  Q *t Q')
proof -
  show f1 : P Q. P * [] Q  P τ Q
   and f2 : P Q. P * [] Q  P   Q
   and f3 : P Q' e. P * (ev e) # s Q'  (Q. P (ev e) Q  Q * s Q')
    by ((subst trace_trans.simps, auto)[1])+
   
  show f4 : tickFree s  (P * s @ [f] Q')  (Q. P *s Q  Q f Q') for s f P Q'
  proof safe
    show P * s @ [f] Q'  Q. P *s Q  Q f Q'
    proof (induct s arbitrary: P)
      case Nil
      thus ?case 
        apply (subst (asm) trace_trans.simps, simp)
        using τ_trans_eq τ_trans_transitivity f1 by blast
    next
      case (Cons e s)
      from Cons.prems have * : e  ready_set P  P afterExt e *s @ [f] Q'
        by (subst (asm) trace_trans.simps)
           (auto simp add:  intro: τ_trans_trace_trans)
      with Cons.hyps obtain Q where ** : P afterExt e *s Q Q f Q' by blast
      have P *e # s Q
      proof (cases e)
        fix e'
        assume e = ev e'
        thus P *e # s Q
          apply simp
          by (rule trace_Cons_ev_trans[OF _ **(1)]) (use * τ_trans_eq in blast)
      next
        from Cons.prems have e =   s = [] by (subst (asm) trace_trans.simps) auto
        thus e =   P *e # s Q using * **(1) f1 f2 by blast
      qed
      with "**"(2) show Q. P *e # s Q  Q f Q' by blast
    qed
  next
    show tickFree s  P *s Q  f  ready_set Q  Q afterExt f τ Q' 
          P *s @ [f] Q' for Q
    proof (induct s arbitrary: P Q)
      show tickFree []  P *[] Q  f  ready_set Q  Q afterExt f τ Q'  
            P *[] @ [f] Q' for P Q
        by (simp add: f1)
           (metis (full_types) τ_trans_eq τ_trans_event_trans event.exhaust 
                               trace_Cons_ev_trans trace_τ_trans trace_tick_trans)
    next
      case (Cons e s)
      from Cons.prems(2) have * : e  ready_set P  P afterExt e *s Q
        by (subst (asm) trace_trans.simps)
           (auto simp add: f1 intro: τ_trans_trace_trans)
      show ?case
      proof (cases e)
        fix e'
        assume e = ev e'
        thus P *(e # s) @ [f] Q' 
          apply simp
          by (rule trace_Cons_ev_trans
                   [OF _ Cons.hyps[OF tickFree_tl[OF Cons.prems(1), simplified] 
                                      *[THEN conjunct2] Cons.prems(3)]])
             (use * τ_trans_eq Cons.prems(4) in blast+)
      next
        show e =   P *(e # s) @ [f] Q' using Cons.prems(1) by auto
      qed
    qed
  qed

  show front_tickFree (s @ t)  P *s @ t Q'  (Q. P *s Q  Q *t Q')
  proof (induct t arbitrary: Q' rule: rev_induct)
    show P *s @ [] Q'  (Q. P *s Q  Q *[] Q') for Q'
      by (metis τ_trans_eq append.right_neutral trace_trans_τ_trans f1)
  next
    case (snoc e t)
    show P *s @ t @ [e] Q'  (Q. P *s Q  Q *t @ [e] Q')
    proof (intro iffI)
      assume assm : P *s @ t @ [e] Q'
      from assm obtain Q where P *s @ t Q Q e Q'
        by (metis append.assoc f4 front_tickFree_implies_tickFree snoc.prems)
      also obtain R where ** : P *s R R *t Q
        by (metis calculation(1) append.assoc front_tickFree_dw_closed snoc.hyps snoc.prems)
      ultimately show Q. P *s Q  Q *t @ [e] Q'
        by (metis append_is_Nil_conv f4 front_tickFree_mono list.distinct(1) snoc.prems)
    next
      assume Q. P *s Q  Q *t @ [e] Q'
      then obtain Q where P *s Q Q *t @ [e] Q' by blast
      also obtain R where Q *t R R e Q'
        by (metis append_is_Nil_conv calculation(2) f4
                  front_tickFree_mono list.distinct(1) snoc.prems)
      ultimately show P *s @ t @ [e] Q'
        by (metis append_assoc f4 front_tickFree_implies_tickFree snoc.hyps
                  snoc.prems tickFree_implies_front_tickFree)
    qed
  qed
qed



section‹Finally: termP *s Q is termP afterTrace s τ Q

theorem T_imp_trace_trans_iff_AfterTrace_τ_trans : 
  s  𝒯 P  (P *s Q)  P afterTrace s τ Q
proof (intro iffI)
  show P *s Q  s  𝒯 P  P afterTrace s τ Q
  proof (induct s arbitrary: P Q rule: rev_induct)
    show P Q. P *[] Q  []  𝒯 P  P afterTrace [] τ Q
      using trace_trans.cases by auto
  next
    fix s e P Q
    assume   hyp : P *s Q  s  𝒯 P  P afterTrace s τ Q for P Q
    assume prems : P *s @ [e] Q s @ [e]  𝒯 P
    have * : e  ready_set (P afterTrace s) 
      using prems(2) ready_set_AfterTrace by blast
    show P afterTrace (s @ [e]) τ Q
      by (metis AfterTrace_snoc τ_trans_event_trans append_single_T_imp_tickFree 
                hyp is_processT3_ST prems trace_trans_iff(4))
  qed
next
  show P afterTrace s τ Q  s  𝒯 P  P *s Q
  proof (induct arbitrary: P Q rule: AfterTrace.induct)
    show P Q. P afterTrace [] τ Q  []  𝒯 P  P *[] Q
      by (simp add: trace_τ_trans)
  next
    fix e and s ::  trace and Q P
    assume   hyp : P afterTrace s τ Q  s  𝒯 P  P *s Q for P Q
    assume prems : P afterTrace (e # s) τ Q e # s  𝒯 P
    have * : e  ready_set P  s  𝒯 (P afterExt e)
      by (metis AfterTrace.simps(1, 2) Cons_in_T_imp_elem_ready_set 
                T_AfterTrace append_Cons append_Nil prems(2))
    show P *e # s Q
    proof (cases e)
      fix e'
      assume ** : e = ev e'
      from * ** have P (ev e') P afterExt (ev e')
        by (simp add: τ_trans_eq)
      thus P *e # s Q
        by (subst **, rule trace_Cons_ev_trans[OF _ hyp[OF prems(1)[simplified] 
                                                        *[THEN conjunct2], simplified **]])
    next
      have e =   s = [] by (metis butlast.simps(2) front_tickFree_butlast 
                                        is_processT2_TR tickFree_Cons prems(2))
      thus e =   P *e # s Q 
        using * prems(1) trace_tick_trans by force
    qed
  qed
qed


text ‹As corollaries we obtain the reciprocal results of 

      @{thm trace_trans_imp_F_if_τ_trans_imp_leF
            trace_trans_imp_T_if_τ_trans_imp_leT
            trace_trans_BOT_imp_D_if_τ_trans_imp_leD}

lemma F_imp_exists_trace_trans: (s, X)   P  Q. (P *s Q)  X   Q
  by (meson F_T F_imp_refusal_AfterTrace Refusals_iff
            T_imp_trace_trans_iff_AfterTrace_τ_trans τ_trans_eq)

lemma T_imp_exists_trace_trans: s  𝒯 P  Q. P *s Q
  using F_imp_exists_trace_trans T_F by blast

lemma D_imp_trace_trans_BOT: tickFree s  s  𝒟 P  P *s 
  by (simp add: D_T D_imp_AfterTrace_is_BOT 
                T_imp_trace_trans_iff_AfterTrace_τ_trans τ_trans_eq)
 



text ‹When we have more information on termP τ Q, we obtain:›

lemma τ_trans_imp_leT_imp_STOP_trace_trans_iff: 
  P Q. P τ Q  P T Q  STOP *s P  s = []  P = STOP
  using STOP_T_iff by (subst trace_trans.simps)
                      (auto simp add: ready_set_STOP τ_trans_eq) 


lemma τ_trans_imp_leF_imp_SKIP_trace_trans_iff: 
  P Q. P τ Q  P F Q 
   SKIP *s P  s = []  P = SKIP  s = []  P = STOP
  using SKIP_F_iff STOP_F_iff by (subst trace_trans.simps)
                                 (auto simp add: AfterExt_SKIP ready_set_SKIP τ_trans_eq)
  
  
lemma τ_trans_imp_leT_imp_trace_trans_ready_set_subset_ready_set_AfterTrace:
  P Q. P τ Q  P T Q  P *s Q 
   ready_set Q  ready_set (P afterTrace s)
  using T_imp_trace_trans_iff_AfterTrace_τ_trans 
        anti_mono_ready_set_T trace_trans_imp_T_if_τ_trans_imp_leT by blast


lemma τ_trans_imp_leT_imp_trace_trans_imp_ready_set:
  P Q. P τ Q  P T Q  P *(s @ e # t) Q 
   e  ready_set (P afterTrace s)
  using ready_set_AfterTrace trace_trans_imp_T_if_τ_trans_imp_leT by blast


lemma trace_trans_iff_T_and_AfterTrace_τ_trans_if_τ_trans_imp_leT: 
  P Q. P τ Q  P T Q 
   (P *s Q)  s  𝒯 P  P afterTrace s τ Q
  using T_imp_trace_trans_iff_AfterTrace_τ_trans trace_trans_imp_T_if_τ_trans_imp_leT by blast
  


section‹General Rules of Operational Semantics›

text ‹Some rules of operational semantics are consequences of localeOpSemGeneric's
      axioms without needing to specify more what termP τ Q is.›

lemma SKIP_trans_tick: SKIP  STOP
  by (simp add: AfterExt_SKIP τ_trans_eq ready_set_SKIP)

lemma tick_trans_imp_BOT_L_or_STOP_R: P  Q  P =   Q = STOP
  by (metis τ_trans_anti_mono_ready_set ready_set_AfterExt ready_set_empty_iff_STOP subset_empty)

lemma STOP_trace_trans_iff : STOP *s P  s = []  P = STOP
  by (metis AfterExt_SKIP SKIP_neq_BOT SKIP_trans_tick empty_iff trace_trans.cases
            ready_set_STOP tick_trans_imp_BOT_L_or_STOP_R trace_trans_iff(1))



lemma ready_tick_imp_τ_trans_SKIP: P τ SKIP if   ready_set P
proof -
  from that have P FD SKIP
    unfolding failure_divergence_refine_def le_ref_def
    by (auto simp add: F_SKIP D_SKIP subset_iff ready_set_def is_processT6_S2)
       (metis append_Nil tick_T_F)
  then obtain Q where P = Q  SKIP
    by (metis mono_Ndet_FD mono_Ndet_FD_left FD_antisym Ndet_id idem_FD)
  thus P τ SKIP by (simp add: τ_trans_NdetR)
qed
 

lemma exists_tick_trans_is_ready_tick: (P'. P  P')    ready_set P
  using τ_trans_eq by blast



lemma tick_trans_iff : P  P'  P τ SKIP  P' = STOP
  by (metis AfterExt_BOT AfterExt_SKIP SKIP_neq_BOT SKIP_trans_tick 
            τ_trans_event_trans ready_tick_imp_τ_trans_SKIP tick_trans_imp_BOT_L_or_STOP_R)
 

lemma SKIP_cant_ev_trans: ¬ SKIP (ev e) STOP
  by (simp add: ready_set_SKIP)

lemma STOP_cant_event_trans: ¬ STOP e P
  by (simp add: ready_set_STOP)




lemma ev_trans_Mprefix: e  A  a  A  P a (ev e) (P e)
  by (simp add: AfterExt_def After_Mprefix τ_trans_eq ready_set_Mprefix)

lemma ev_trans_Mndetprefix: e  A  a  A  P a (ev e) (P e)
  by (simp add: AfterExt_def After_Mndetprefix τ_trans_eq ready_set_Mndetprefix)

lemma ev_trans_prefix: e  P  (ev e) P
  by (metis ev_trans_Mprefix insertI1 write0_def)



lemma τ_trans_MultiNdet: finite A  x  A  (a  A. P a) τ P x
  by (metis MultiNdet_insert' τ_trans_NdetL emptyE insert_absorb)

lemma τ_trans_GlobalNdet: (a  A. P a) τ P e if e  A
proof -
  have (a  A. P a) = P e  (a  A. P a)
    by (metis GlobalNdet_factorization_union GlobalNdet_unit
              empty_iff insertI1 insert_absorb insert_is_Un that)
  thus (a  A. P a) τ P e by (metis τ_trans_NdetL)
qed
  


lemma fix_point_τ_trans: cont f  P = (μ X. f X)  P τ f P
  by (metis τ_trans_eq cont_process_rec)


lemma event_trans_DetL: P e P'  P  Q e P'
  by (metis AfterExt_Det_is_AfterExt_Ndet Un_iff τ_trans_NdetL τ_trans_event_trans ready_set_Det)
 
lemma event_trans_DetR: Q e Q'  P  Q e Q'
  by (metis Det_commute event_trans_DetL)

lemma event_trans_MultiDet:
  finite A  a  A  P a e Q  (a  A. P a) e Q
  by (metis MultiDet_insert' event_trans_DetL insert_absorb)


 
lemma Sliding_event_transL: P e P'  P  Q e P'
  unfolding Sliding_def
  apply (drule event_trans_DetL[of e P P' Q])
  using τ_trans_NdetL τ_trans_event_trans by blast


lemma Sliding_τ_transR: P  Q τ Q
  unfolding Sliding_def by (simp add: τ_trans_NdetR)



lemma P P' Q. P  P'  ¬ P ; Q  P' ; Q
  by (metis SKIP_Seq SKIP_trans_tick STOP_cant_event_trans)



lemma ev_trans_SeqR:
    ready_set P  Q (ev e) Q'  P ; Q (ev e) Q'
  by (simp add: AfterExt_Seq ready_set_Seq AfterExt_BOT BOT_Seq)
     (metis Ndet_commute τ_trans_NdetL τ_trans_transitivity)
  
 


lemma SKIP S SKIP  STOP
  by (simp add: SKIP_trans_tick Sync_SKIP_SKIP)

lemma SKIP S SKIP τ SKIP
  by (simp add: Sync_SKIP_SKIP τ_trans_eq)


lemma tick_trans_Hiding: P \ B  STOP if P  P'
proof -
  have (P \ B) afterExt  = STOP  (P \ B) afterExt 
    by (simp add: AfterExt_def)
  thus P \ B  STOP 
    by (simp add: AfterExt_def τ_trans_eq ready_tick_imp_ready_tick_Hiding that)
qed



text ‹The following lemma is useless since the locale mechanism forces
      termf to be of type typ   while it could be typ  . 
      We will have to prove it again on each instantiation.›

lemma Renaming P f  STOP if P  P'
proof -
  have Renaming P f afterExt  = STOP  Renaming P f afterExt 
    by (metis τ_trans_eq not_ready_AfterExt tick_trans_iff)
  thus Renaming P f  STOP
    by (simp add: that tick_eq_EvExt AfterExt_def τ_trans_eq
                  ready_set_Renaming BOT_τ_trans_anything)
qed



end

end