Theory Mprefix

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Burkhart Wolff.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : A Combined CSP Theory
 *
 * Copyright (c) 2009 Université Paris-Sud, 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.
 ******************************************************************************›
(*>*)


section‹ The Multi-Prefix Operator Definition ›

theory  Mprefix 
imports Process 
begin 

subsection‹ The Definition and some Consequences ›

lift_definition   Mprefix     :: "['a set,'a => 'a process] => 'a process"
  is "λA P. ({(tr,ref). tr = [] ∧ ref Int (ev ` A) = {}} ∪
             {(tr,ref). tr ≠ [] ∧ hd tr ∈ (ev ` A) ∧ 
                        (∃ a. ev a = (hd tr)∧(tl tr,ref)∈ℱ(P a))},
             {d. d ≠ [] ∧  hd d  ∈ (ev ` A) ∧ (∃ a. ev a = hd d ∧ tl d ∈ 𝒟 (P a))})"
proof -
  show ‹is_process ({(tr, ref). tr = [] ∧ ref ∩ ev ` (A :: 'a set) = {}} ∪
                    {(tr, ref). tr ≠ [] ∧ hd tr ∈ ev ` A ∧ 
                                (∃a. ev a = hd tr ∧ (tl tr, ref) ∈ ℱ (P a))},
                    {d. d ≠ [] ∧ hd d ∈ ev ` A ∧ (∃a. ev a = hd d ∧ tl d ∈ 𝒟 (P a))}) › 
    (is ‹is_process(?f, ?d)›) for A P
proof  (simp only: is_process_def FAILURES_def DIVERGENCES_def
                   Product_Type.fst_conv Product_Type.snd_conv,
        intro conjI allI impI)
    show "([],{}) ∈ ?f" by(simp)
next  
    fix    s:: "'a event list" fix X::"'a event set"
    assume H : "(s, X) ∈ ?f"
    show       "front_tickFree s"
               apply(insert H, auto simp:  front_tickFree_def tickFree_def
                                    dest!:list_nonMt_append)
               apply(rename_tac aa ta x, case_tac "ta", auto simp: front_tickFree_charn
                                    dest! : is_processT2[rule_format])
               apply(simp add: tickFree_def)
               done 
next
    fix s t :: "'a event list" 
    assume     "(s @ t, {}) ∈ ?f"
    then show  "(s, {}) ∈ ?f"
               by(auto elim: is_processT3[rule_format])
next
    fix    s:: "'a event list" fix X Y::"'a event set"
    assume     "(s, Y) ∈ ?f ∧ X ⊆ Y"
    then show  "(s, X) ∈ ?f"
               by(auto intro: is_processT4[rule_format])
next
    fix    s:: "'a event list" fix X Y::"'a event set"
    assume     "(s, X) ∈ ?f ∧ (∀ c. c∈Y ⟶ (s @ [c], {}) ∉ ?f)"
    then show  "(s, X ∪ Y) ∈ ?f "
               by(auto intro!: is_processT1 is_processT5[rule_format]) 
next
    fix s::    "'a event list" fix X::"'a event set"
    assume     "(s @ [tick], {}) ∈ ?f"
    then show  "(s, X - {tick}) ∈ ?f"
               by(cases s, auto dest!: is_processT6[rule_format])
next
    fix s t::  "'a event list" fix X::"'a event set"
    assume     "s ∈  ?d ∧ tickFree s ∧ front_tickFree t"
    then show  "s @ t ∈ ?d"
               by(auto intro!: is_processT7_S, cases s, simp_all)
next
    fix s::    "'a event list" fix X::"'a event set"
    assume     "s ∈ ?d"
    then show  "(s, X) ∈ ?f"
               by(auto simp: is_processT8_S)
next
    fix s::    "'a event list" 
    assume     "s @ [tick] ∈ ?d"
    then show  "s ∈ ?d"
               apply(auto)
               apply(cases s, simp_all)
               apply(cases s, auto intro: is_processT9[rule_format])
               done

           qed
         qed


syntax
  "_Mprefix" :: "[pttrn,'a set,'a process] ⇒ 'a process"	(‹(3□(_/∈_)/ → (_))›[0,0,64]64)

term "Ball A (λx. P)"

syntax_consts
  "_Mprefix" ⇌ Mprefix

translations
  "□x∈A → P" ⇌ "CONST Mprefix A (λx. P)"

text‹Syntax Check:›
term ‹□x∈A → □y∈A → □z∈A → P z x y = Q›


(* bizarre exercise in style proposed by Makarius... *)
lemma is_process_REP_Mprefix'  :
     "is_process ({(tr,ref). tr=[] ∧  ref ∩ (ev ` A) = {}} ∪
                  {(tr,ref). tr ≠ [] ∧ hd tr ∈ (ev ` A) ∧
                        (∃ a. ev a = (hd tr) ∧ (tl tr,ref) ∈ ℱ(P a))},
                  {d. d ≠  [] ∧  hd d ∈ (ev ` A) ∧
                        (∃ a. ev a = hd d  ∧ tl d ∈ 𝒟(P a))})"
 (is "is_process(?f, ?d)")
proof  (simp only:is_process_def FAILURES_def DIVERGENCES_def
                  Product_Type.fst_conv Product_Type.snd_conv,
        intro conjI allI impI,goal_cases)
  case 1
    show "([],{}) ∈ ?f" by(simp)
next  
  case (2 s X) 
    assume H : "(s, X) ∈ ?f"
    have       "front_tickFree s"
      apply(insert H, auto simp:  front_tickFree_def tickFree_def
                           dest!:list_nonMt_append)
      apply(rename_tac aa ta x, case_tac "ta", auto simp: front_tickFree_charn
                           dest! : is_processT2[rule_format])
      apply(simp add: tickFree_def)
      done    
    then show "front_tickFree s"  by(auto) 
next
  case (3 s t) 
    assume H : "(s @ t, {}) ∈ ?f"
    show "(s, {}) ∈ ?f" using H  by(auto elim: is_processT3[rule_format])
next
  case (4 s X Y) 
    assume H1: "(s, Y) ∈ ?f ∧ X ⊆ Y"
    then show "(s, X) ∈ ?f"  by(auto intro: is_processT4[rule_format])
next
  case (5 s X Y)   
    assume  "(s, X) ∈ ?f ∧ (∀ c. c∈Y ⟶ (s @ [c], {}) ∉ ?f)"
    then show "(s, X ∪ Y) ∈ ?f"  by(auto intro!: is_processT1 is_processT5[rule_format]) 
next
  case (6 s X)   
    assume  "(s @ [tick], {}) ∈ ?f"   
    then show "(s, X - {tick}) ∈ ?f"  by(cases s, auto dest!: is_processT6[rule_format])
next
  case (7 s t) 
    assume H1 : "s ∈  ?d ∧ tickFree s ∧ front_tickFree t"
    have 7:     "s @ t ∈ ?d"
      using H1  by(auto intro!: is_processT7_S, cases s, simp_all)
    then show "s @ t ∈ ?d" using H1  by(auto)
next
  case (8 s X)   
    assume H : "s ∈ ?d"
    then show "(s, X) ∈ ?f" using H by(auto simp: is_processT8_S)
next
  case (9 s)  
    assume H: "s @ [tick] ∈ ?d"
    then have 9:   "s ∈ ?d"
       apply(auto)
       apply(cases s, simp_all)
       apply(cases s, auto intro: is_processT9[rule_format])
       done
    then show "s ∈ ?d" by(auto)
qed

   
lemma Rep_Abs_Mprefix'' : 
assumes H1 : "f = {(tr, ref). tr = [] ∧ ref ∩ ev ` A = {}} ∪
                  {(tr, ref). tr ≠ [] ∧ hd tr ∈ ev ` A 
                             ∧ (∃a. ev a = hd tr ∧ (tl tr, ref) ∈ ℱ (P a))}"
    and H2 : "d = {d. d ≠  [] ∧  hd d ∈ (ev ` A) ∧ 
                     (∃ a. ev a = hd d  ∧ tl d ∈ 𝒟(P a))}"
  shows "Rep_process (Abs_process (f,d)) = (f,d)"
  using Abs_process_inverse H1 H2 is_process_REP_Mprefix' by blast



subsection ‹ Projections in Prefix ›

lemma F_Mprefix : 
  "ℱ (□ x ∈ A → P x) = {(tr,ref). tr=[] ∧  ref ∩ (ev ` A) = {}} ∪
                         {(tr,ref). tr ≠ [] ∧ hd tr ∈ (ev ` A) ∧ 
                                   (∃ a. ev a = (hd tr) ∧ (tl tr,ref) ∈ ℱ(P a))}"
  by (subst Failures.rep_eq, simp add: Mprefix.rep_eq FAILURES_def)

lemma D_Mprefix:
  "𝒟 (□ x ∈ A → P x) = {d. d ≠  [] ∧  hd d ∈ (ev ` A) ∧ 
                             (∃ a. ev a = hd d  ∧ tl d ∈ 𝒟(P a))}"
  by (subst Divergences.rep_eq, simp add: Mprefix.rep_eq DIVERGENCES_def)


lemma T_Mprefix:
  "𝒯 (□ x ∈ A → P x)={s. s=[] ∨ (∃ a. a∈A ∧ s≠[] ∧ hd s = ev a ∧ tl s ∈ 𝒯(P a))}"
  by (subst Traces.rep_eq, auto simp add: TRACES_def Failures.rep_eq[symmetric] F_Mprefix)
     (use F_T T_F in ‹blast+›)
  

subsection ‹ Basic Properties ›

lemma tick_T_Mprefix [simp]: "[tick] ∉ 𝒯 (□ x ∈ A → P x)"
  by(simp add:T_Mprefix)


lemma Nil_Nin_D_Mprefix [simp]: "[] ∉ 𝒟 (□ x ∈ A → P x)"
  by(simp add: D_Mprefix)

subsection‹ Proof of Continuity Rule ›

subsubsection‹ Backpatch Isabelle 2009-1›

―‹re-introduced from Isabelle/HOLCF 2009-1; clearly
   a derived concept, but still a useful shortcut›

definition
  contlub :: "('a::cpo ⇒ 'b::cpo) ⇒ bool" 
  where
  "contlub f = (∀Y. chain Y ⟶ f (⨆ i. Y i) = (⨆ i. f (Y i)))"

lemma contlubE:
  "⟦contlub f; chain Y⟧ ⟹ f (⨆ i. Y i) = (⨆ i. f (Y i))"
  by (simp add: contlub_def)


lemma monocontlub2cont: "⟦monofun f; contlub f⟧ ⟹ cont f"
apply (rule contI)
apply (rule thelubE)
apply (erule (1) ch2ch_monofun)
apply (erule (1) contlubE [symmetric])
done

lemma contlubI:
  "(⋀Y. chain Y ⟹ f (⨆ i. Y i) = (⨆ i. f (Y i))) ⟹ contlub f"
by (simp add: contlub_def)


lemma cont2contlub: "cont f ⟹ contlub f"
apply (rule contlubI)
apply (rule po_class.lub_eqI [symmetric])
apply (erule (1) contE)
done


subsubsection‹ Core of Proof  ›

lemma mono_Mprefix1:
"∀a∈A. P a ⊑ Q a ⟹ 𝒟 (Mprefix A Q) ⊆ 𝒟 (Mprefix A P)"
  apply(auto simp: D_Mprefix) using le_approx1 by blast

lemma mono_Mprefix2:
"∀x∈A. P x ⊑ Q x ⟹
 ∀s. s ∉ 𝒟 (Mprefix A P) ⟶ Ra (Mprefix A P) s = Ra (Mprefix A Q) s"          
  apply (auto simp: Ra_def D_Mprefix F_Mprefix) using proc_ord2a by blast+

lemma mono_Mprefix3 :
assumes H:"∀x∈A. P x ⊑ Q x"
shows " min_elems (𝒟 (Mprefix A P)) ⊆ 𝒯 (Mprefix A Q)"
proof(auto simp: min_elems_def D_Mprefix T_Mprefix image_def, goal_cases)
  case (1 x a)
  with H[rule_format, of a, OF 1(2)] show ?case 
    apply(auto dest!: le_approx3 simp: min_elems_def)
    apply(subgoal_tac "∀t. t ∈ 𝒟 (P a) ⟶ ¬ t < tl x", auto)
    apply(rename_tac t, erule_tac x="(ev a)#t" in allE, auto)
    using less_cons hd_Cons_tl by metis
qed

lemma mono_Mprefix0:
"∀x∈A. P x ⊑ Q x ⟹ Mprefix A P ⊑ Mprefix A Q" 
apply(simp add: le_approx_def mono_Mprefix1 mono_Mprefix3)
apply(rule mono_Mprefix2)
apply(auto simp: le_approx_def)
done


lemma mono_Mprefix[simp]: "monofun(Mprefix A)"
by(auto simp: below_fun_def monofun_def mono_Mprefix0)


lemma proc_ord2_set: 
"P ⊑ Q ⟹ {(s, X). s ∉ 𝒟 P ∧ (s, X) ∈ ℱ P} = {(s, X). s ∉ 𝒟 P ∧ (s, X) ∈ ℱ Q}"
by(auto simp: le_approx2)


lemma proc_ord_proc_eq_spec: "P ⊑ Q ⟹ 𝒟 P ⊆ 𝒟 Q ⟹ P = Q"
by (metis (mono_tags, lifting) below_antisym below_refl le_approx_def subset_antisym)


lemma Mprefix_chainpreserving: "chain Y ⟹ chain (λi. Mprefix A (Y i))"
apply(rule chainI, rename_tac i)
apply(frule_tac i="i" in chainE)
by(simp add: mono_Mprefix0 fun_belowD)


lemma limproc_is_thelub_fun: 
assumes     "chain S" 
shows       "(Lub S c) = lim_proc (range (λx. (S x c)))"
proof -
  have    "⋀xa. chain (λx. S x xa)"
                  using `chain S` by(auto intro!: chainI  simp: chain_def fun_belowD )
  then     show ?thesis  by (metis contlub_lambda limproc_is_thelub)
qed


lemma contlub_Mprefix : "contlub(%P. Mprefix A P)"
proof(rule contlubI, rule proc_ord_proc_eq_spec)
   fix Y   :: "nat ⇒ 'a ⇒ 'a process" 
   assume C : "chain Y" 
   have   C': "⋀xa. chain (λx. Y x xa)"
                 apply(insert C,rule chainI)
                 by(auto simp: chain_def fun_belowD)
   show       "Mprefix A (⨆ i. Y i) ⊑ (⨆ i. Mprefix A (Y i))"
                 by(auto simp: Process.le_approx_def F_Mprefix D_Mprefix T_Mprefix C C'
                               Mprefix_chainpreserving limproc_is_thelub limproc_is_thelub_fun
                               D_T D_LUB D_LUB_2 F_LUB T_LUB_2 Ra_def min_elems_def)
next
   fix Y   :: "nat ⇒ 'a ⇒ 'a process" 
   assume C : "chain Y" 
   show       "𝒟 (Mprefix A (⨆ i. Y i)) ⊆ 𝒟 (⨆ i. Mprefix A (Y i))"
                 apply(auto simp: Process.le_approx_def F_Mprefix D_Mprefix T_Mprefix 
                                  C Mprefix_chainpreserving limproc_is_thelub D_LUB_2)
                 by (meson C fun_below_iff in_mono is_ub_thelub le_approx1)
qed



lemma Mprefix_cont [simp]: 
"(⋀x. cont (f x)) ⟹ cont (λy. □ z ∈  A → f z y)"
apply(rule_tac f = "λz y. (f y z)" in cont_compose)
apply(rule monocontlub2cont)
apply(auto intro: mono_Mprefix contlub_Mprefix cont2cont_lambda)
done


subsection‹ High-level Syntax for Read and Write ›

text‹ The following syntax introduces the usual channel notation for CSP.
Slightly deviating from conventional wisdom, we view a channel not as a tag in
a pair, rather than as a function of type @{typ "'a⇒'b"}. This paves the way
for \emph{typed} channels over a common universe of events. ›

definition  read     :: "['a ⇒ 'b,'a set, 'a ⇒ 'b process] ⇒ 'b process"
where      "read c A P  ≡ Mprefix(c ` A) (P o (inv_into A c))"
definition "write"    :: "['a ⇒ 'b, 'a, 'b process] ⇒ 'b process"
where      "write c a P ≡ Mprefix {c a} (λ x. P)"
definition  write0   :: "['a, 'a process] ⇒ 'a process"
where      "write0 a P ≡ Mprefix {a} (λ x. P)"


syntax
  "_read"   :: "[id, pttrn, 'a process] => 'a process"
                                        (‹(3(_❙?_) /→ _)› [0,0,78] 78)
  "_readX"  :: "[id, pttrn, bool,'a process] => 'a process"
                                        (‹(3(_❙?_)❙|_ /→ _)› [0,0,78] 78)
  "_readS"  :: "[id, pttrn, 'b set,'a process] => 'a process"
                                        (‹(3(_❙?_)∈_ /→ _)› [0,0,78] 78)
  "_write"  :: "[id, 'b, 'a process] => 'a process"
                                        (‹(3(_❙!_) /→ _)› [0,0,78] 78)
  "_writeS" :: "['a, 'a process] => 'a process"
                                        (‹(3_ /→ _)› [0,78]78)

syntax_consts
  "_read" "_readX" "_readS" ⇌ read and
  "_write" ⇌ "write" and
  "_writeS" ⇌ write0

subsection‹CSP$_M$-Style Syntax for Communication Primitives›
translations
  "_read c p P"     ⇌ "CONST read c CONST UNIV (λp. P)"
  "_write c p P"    ⇌ "CONST write c p P"
  "_readX c p b P"  => "CONST read c {p. b} (λp. P)"
  "_writeS a P"     ⇌ "CONST write0 a P"
  "_readS c p A P"  => "CONST read c A (λp. P)"

text‹Syntax Check:›
term‹ d❙?y → c❙!x → P = Q›


lemma read_cont[simp]: "cont P ⟹ cont (λy. read c A (P y))"
  unfolding read_def o_def
  by (rule Mprefix_cont) (rule cont2cont_fun) 


lemma read_cont'[simp]: "(⋀x. cont (f x)) ⟹ cont (λy. c❙?x → f x y)" by simp


lemma write_cont[simp]: "cont (P::('b::cpo ⇒ 'a process))  ⟹ cont(λx. (c❙!a → P x))"
by(simp add:write_def)


corollary write0_cont_lub : "contlub(Mprefix {a})"
  using contlub_Mprefix by blast


lemma write0_contlub : "contlub(write0 a)"
  unfolding write0_def contlub_def
proof (auto)
  fix Y :: "nat ⇒ 'a process"
  assume   "chain Y"
  have * : "chain (λi. (λ_. Y i)::'b ⇒ 'a process)"
           by (meson ‹chain Y› fun_below_iff po_class.chain_def)
  have **: "(λx. Lub Y) = Lub (λi. (λ_. Y i))"
           by(rule ext,metis * ch2ch_fun limproc_is_thelub limproc_is_thelub_fun lub_eq)
  show "Mprefix {a} (λx. Lub Y) = (⨆i. Mprefix {a} (λx. Y i))"
    apply(subst **, subst contlubE[OF contlub_Mprefix])
    by (simp_all add: *)
qed
  
lemma write0_cont[simp]: "cont (P::('b::cpo ⇒ 'a process)) ⟹ cont(λx. (a → P x))"
by(simp add:write0_def)

end