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