Theory Det

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Burkhart Wolff, Safouan Taha.
 *                   (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‹ Deterministic Choice Operator Definition ›

theory  Det 
imports Process
begin

subsection‹The Det Operator Definition›
lift_definition
        Det      :: "[ process, process]   process"   (infixl "[+]" 79)
        is   "λP Q. (  {(s,X). s = []  (s,X)   P   Q}
                      {(s,X). s  []  (s,X)   P   Q}
                      {(s,X). s = []  s  𝒟 P  𝒟 Q}
                      {(s,X). s = []  tick  X  [tick]  𝒯 P  𝒯 Q},
                     𝒟 P  𝒟 Q)"
proof -
  show is_process (   {(s,X). s = []  (s,X)   (P :: process)   Q}
                      {(s,X). s  []  (s,X)   P   Q}
                      {(s,X). s = []  s  𝒟 P  𝒟 Q}
                      {(s,X). s = []  tick  X  [tick]  𝒯 P  𝒯 Q},
                     𝒟 P  𝒟 Q) (is is_process (?f, ?d)) for P Q
  proof (simp only: fst_conv snd_conv Rep_process is_process_def 
                    DIVERGENCES_def FAILURES_def, intro conjI)
    show "([], {})  ?f"
      by(simp add: is_processT1)
  next
    show "s X. (s, X)  ?f  front_tickFree s"
      by(auto simp: is_processT2)
  next
    show "s t.   (s @ t, {})  ?f  (s, {})  ?f"
      by(auto simp: is_processT1 dest!: is_processT3[rule_format])
  next
    show "s X Y. (s, Y)  ?f  X  Y    (s, X)  ?f"
      by(auto dest: is_processT4[rule_format,OF conj_commute[THEN iffD1],OF conjI])
  next
    show "sa X Y. (sa, X)  ?f  (c. c  Y  (sa @ [c], {})  ?f)  (sa, X  Y)  ?f"
      by(auto simp: is_processT5 T_F)
  next
    show " s X. (s @ [tick], {})  ?f  (s, X - {tick})  ?f"
      apply((rule allI)+, rule impI, rename_tac s X)
      apply(case_tac "s=[]", simp_all add: is_processT6[rule_format] T_F_spec)
      by(auto simp: is_processT6[rule_format] T_F_spec)
  next
    show "s t. s  ?d  tickFree s  front_tickFree t  s @ t  ?d"
      by(auto simp: is_processT7)
  next
    show "s X. s  ?d  (s, X)  ?f"
      by(auto simp: is_processT8[rule_format]) 
  next
    show "s. s @ [tick]  ?d  s  ?d"
      by(auto intro!:is_processT9[rule_format])  
  qed
qed

notation
  Det (infixl "" 79)

term (A  B)  D' = C


subsection‹The Projections›

lemma F_Det    :
   " (P  Q) =    {(s,X). s = []  (s,X)   P   Q}
                  {(s,X). s  []  (s,X)   P   Q}
                  {(s,X). s = []  s  𝒟 P  𝒟 Q}
                  {(s,X). s = []  tick  X  [tick]  𝒯 P  𝒯 Q}"
  by (subst Failures.rep_eq, simp add: Det.rep_eq FAILURES_def)

lemma D_Det: "𝒟 (P  Q) = 𝒟 P  𝒟 Q"
   by (subst Divergences.rep_eq, simp add: Det.rep_eq DIVERGENCES_def)

lemma T_Det: "𝒯 (P  Q) = 𝒯 P  𝒯 Q"
  apply (subst Traces.rep_eq, simp add: TRACES_def Failures.rep_eq[symmetric] F_Det)
  apply(auto simp: T_F F_T is_processT1 Nil_elem_T)
  by(rule_tac x="{}" in exI, simp add: T_F F_T is_processT1 Nil_elem_T)+
  

subsection‹Basic Laws›
text‹The following theorem of Commutativity helps to simplify the subsequent
continuity proof by symmetry breaking. It is therefore already developed here:›

lemma Det_commute:"(P  Q) = (Q  P)"
  by(auto simp: Process_eq_spec F_Det D_Det)


subsection‹The Continuity-Rule›

lemma mono_Det1: "P  Q  𝒟 (Q  S)  𝒟 (P  S)"
  apply (drule le_approx1)
  by (auto simp: Process_eq_spec F_Det D_Det)

lemma mono_Det2: 
assumes ordered: "P  Q"
shows   "( s. s  𝒟 (P  S)  Ra (P  S) s = Ra (Q  S) s)"
proof -
   have A:"s t. []  𝒟 P  []  𝒟 S  s = []  
           ([], t)   P  ([], t)   S  ([], t)   Q"
        by (insert ordered,frule_tac X="t" and s="[]" in proc_ord2a, simp_all)
   have B:"s t. s  𝒟 P  s  𝒟 S 
          (s  []  ((s, t)   P  (s, t)   S)  (s, t)   Q  (s, t)   S) 
          (s = []  tick  t  ([tick]  𝒯 P  [tick]  𝒯 S) 
           ([], t)   Q  ([], t)   S  []  𝒟 Q   [tick]  𝒯 Q   [tick]  𝒯 S)"
        apply(intro conjI impI, elim conjE disjE, rule disjI1)
        apply(simp_all add: proc_ord2a[OF ordered,symmetric])
        apply(elim conjE disjE,subst le_approx2T[OF ordered])
        apply(frule is_processT9_S_swap, simp_all)
        done
   have C: "s. s  𝒟 P  s  𝒟 S 
                {X. s = []  (s, X)   Q  (s, X)   S 
                    s  []  ((s, X)   Q  (s, X)   S) 
                    s = []  s  𝒟 Q  s = []  tick  X  
                    ([tick]  𝒯 Q  [tick]  𝒯 S)}
               {X. s = []  (s, X)   P  (s, X)   S 
                     s  []  ((s, X)   P  (s, X)   S) 
                     s = []  tick  X  ([tick]  𝒯 P  [tick]  𝒯 S)}"
        apply(intro subsetI, frule is_processT9_S_swap, simp)
        apply(elim conjE disjE, simp_all add: proc_ord2a[OF ordered,symmetric] is_processT8_S)
        apply(insert le_approx1[OF ordered] le_approx_lemma_T[OF ordered]) 
        by   (auto simp: proc_ord2a[OF ordered,symmetric])    
    show ?thesis
    apply(simp add: Process_eq_spec F_Det D_Det Ra_def min_elems_def)
    apply(intro allI impI equalityI C, simp_all)
    apply(intro allI impI subsetI, simp)
    apply(metis A B)    
    done
qed


lemma mono_Det3: "P  Q  min_elems (𝒟 (P  S))  𝒯 (Q  S)"
apply (frule le_approx3)
apply (simp add: Process_eq_spec F_Det T_Det D_Det Ra_def min_elems_def subset_iff)
apply (auto intro:D_T)
done

lemma mono_Det[simp]  : "P  Q  (P  S)  (Q  S)"
by (auto simp: le_approx_def mono_Det1 mono_Det2 mono_Det3)


lemma mono_Det_sym[simp] : "P  Q  (S  P)  (S  Q)"
by (simp add: Det_commute)



lemma cont_Det0: 
assumes C : "chain Y"
shows       "(lim_proc (range Y)  S) = lim_proc (range (λi. Y i  S))"
proof -
  have C':"chain (λi. Y i  S)"
          by(auto intro!:chainI simp:chainE[OF C])
  show ?thesis
  apply (subst Process_eq_spec)
  apply (simp add: D_Det F_Det)
  apply(simp add: F_LUB[OF C]  D_LUB[OF C] T_LUB[OF C] F_LUB[OF C']  D_LUB[OF C'] T_LUB[OF C'])
  apply(safe)
  apply(auto simp: D_Det F_Det T_Det)
  using NF_ND apply blast
  using is_processT6_S2 is_processT8 apply blast
  apply (metis D_T append_Nil front_tickFree_single process_charn tickFree_Nil)
  using NF_ND is_processT6_S2 apply blast
  using NF_ND is_processT6_S2 by blast
qed

lemma cont_Det: 
assumes C: "chain Y"
shows   " (( i. Y i)  S) = ( i. (Y i  S))"
apply(insert C)
apply(subst limproc_is_thelub, simp)
apply(subst limproc_is_thelub)
apply(rule chainI)
apply(frule_tac i="i" in chainE)
apply(simp)
apply(erule cont_Det0)
done


lemma cont_Det': 
assumes chain:"chain Y"
shows "(( i. Y i)  S) = ( i. (Y i  S))"
proof -
   have chain':"chain (λi. Y i  S)"
          by(auto intro!:chainI simp: chainE[OF chain])
   have B:" (lim_proc (range Y)  S)    (lim_proc (range (λi. Y i  S)))"
          apply(simp add: D_Det F_Det F_LUB T_LUB D_LUB chain chain')
          apply(intro conjI subsetI, simp_all)
          by(auto split:prod.split prod.split_asm)
   have C:" (lim_proc (range (λi. Y i  S)))  (lim_proc (range Y)  S)"
      proof -
      have C1 : "ba ab ac. a. ([], ba)   (Y a)  ([], ba)   S  []  𝒟 (Y a) 
                   []  𝒟 (Y ab)  []  𝒟 S   tick  ba  ([], ba)   (Y ac) "
                using is_processT8 by auto
      have C2 : "ba ab ac ad D. a. ([], ba)   (Y a)  ([], ba)   S  []  𝒟 (Y a) 
                                tick  ba  [tick]  𝒯 (Y a) 
                   []D(Y ab)  []D S  ([],ba) (Y ac)  [tick]  𝒯 S  [tick]𝒯(Y ad)"
                using NF_ND is_processT6_S2 by blast
      have C3: "ba ab ac. a. []  𝒟 (Y a)  tick  ba  [tick]  𝒯 (Y a) 
                   []  𝒟 (Y ab)  []  𝒟 S  ([], ba)   S  
                   [tick]  𝒯 S  [tick]  𝒯 (Y ac)"
                by (metis D_T append_Nil front_tickFree_single process_charn tickFree_Nil)
      show ?thesis
          apply(simp add: D_Det F_Det F_LUB T_LUB D_LUB chain chain')
          apply(rule subsetI, simp)
          apply(simp split:prod.split prod.split_asm)
          apply(intro allI impI,simp)
          by (metis C3 is_processT6_S2 is_processT8_S)
      qed
   have D:"𝒟 (lim_proc (range Y)  S) = 𝒟 (lim_proc (range (λi. Y i  S)))"
          by(simp add: D_Det F_Det F_LUB T_LUB D_LUB chain chain')
   show ?thesis
   by(simp add: chain chain' limproc_is_thelub Process_eq_spec equalityI B C D)
qed

lemma Det_cont[simp]: 
assumes f:"cont f"
and     g:"cont g"
shows     "cont (λx. f x  g x)"
proof -
   have A : "x. cont f  cont (λy. y  f x)"
       apply (rule contI2,rule monofunI)
       apply (auto)
       apply (subst Det_commute,subst cont_Det)
       apply (auto simp: Det_commute)
       done
   have B : "y. cont f  cont (λx. y  f x)"
       apply (rule_tac c="(λ x. y  x)" in cont_compose)
       apply (rule contI2,rule monofunI)
       apply (auto)
       apply (subst Det_commute,subst cont_Det)
       by (simp_all add: Det_commute)
   show ?thesis using f g 
      apply(rule_tac f="(λx. (λ g. f x  g))" in cont_apply)
      apply(auto intro:contI2 monofunI simp:Det_commute A B)
      done
qed

end