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. cY  (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)"

translations
  "xA  P"  "CONST Mprefix A (λx. P)"

text‹Syntax Check:›
term xA  yA  zA  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. cY  (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. aA  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 Porder.po_class.lub_eqI [symmetric])
apply (erule (1) contE)
done


subsubsection‹ Core of Proof  ›

lemma mono_Mprefix1:
"aA. P a  Q a  𝒟 (Mprefix A Q)  𝒟 (Mprefix A P)"
  apply(auto simp: D_Mprefix) using le_approx1 by blast

lemma mono_Mprefix2:
"xA. 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:"xA. 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:
"xA. 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: Fun_Cpo.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.cont_compose)
apply(rule monocontlub2cont)
apply(auto intro: mono_Mprefix contlub_Mprefix Fun_Cpo.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)

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