Theory Ndet

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

theory  Ndet 
imports Process
begin


subsection‹ Definition and Consequences ›
definition
        Ndet     :: "['α process,'α process] ⇒ 'α process"   (infixl "|-|" 80)
where   "P |-| Q ≡ Abs_process(ℱ P ∪ ℱ Q , 𝒟 P ∪ 𝒟 Q)"

notation
  Ndet (infixl "⊓" 80)


lemma is_process_REP_Ndet:
"is_process (ℱ P ∪ ℱ Q , 𝒟 P ∪ 𝒟 Q)"
proof(simp only: fst_conv snd_conv Rep_process is_process_def DIVERGENCES_def FAILURES_def,
      intro conjI)
    show "([], {}) ∈ (ℱ P ∪ ℱ Q)"
         by(simp add: is_processT1)
next
    show "∀s X. (s, X) ∈ (ℱ P ∪ ℱ Q) ⟶ front_tickFree s"
         by(auto simp: is_processT2)
next
    show "∀s t.   (s @ t, {}) ∈(ℱ P ∪ ℱ Q) ⟶ (s, {}) ∈ (ℱ P ∪ ℱ Q)"
         by (auto simp: is_processT1 dest!: is_processT3[rule_format])
next
    show "∀s X Y. (s, Y) ∈ (ℱ P ∪ ℱ Q) ∧ X ⊆ Y ⟶ (s, X) ∈ (ℱ P ∪ ℱ Q)"
         by(auto dest: is_processT4[rule_format,OF conj_commute[THEN iffD1], OF conjI])
next
    show "∀sa X Y. (sa, X) ∈ (ℱ P ∪ ℱ Q) ∧ (∀c. c ∈ Y ⟶ (sa @ [c], {}) ∉ (ℱ P ∪ ℱ Q))
          ⟶ (sa, X ∪ Y) ∈ (ℱ P ∪ ℱ Q)"
         by(auto simp: is_processT5 T_F)
next
    show "∀s X. (s @ [tick], {}) ∈ (ℱ P ∪ ℱ Q) ⟶ (s, X - {tick}) ∈ (ℱ P ∪ ℱ Q)"
         apply((rule allI)+, rule impI)
         apply(rename_tac s X, case_tac "s=[]", simp_all add: is_processT6[rule_format] T_F_spec)
         apply(erule disjE,simp_all add: is_processT6[rule_format] T_F_spec)
         apply(erule disjE,simp_all add: is_processT6[rule_format] T_F_spec)
         done
next
    show "∀s t. s ∈ 𝒟 P ∪ 𝒟 Q ∧ tickFree s ∧ front_tickFree t ⟶ s @ t ∈ 𝒟 P ∪ 𝒟 Q"
         by(auto simp: is_processT7)
next
    show "∀s X. s ∈ 𝒟 P ∪ 𝒟 Q ⟶ (s, X) ∈ (ℱ P ∪ ℱ Q)"
         by(auto simp: is_processT8[rule_format])
next
    show "∀s. s @ [tick] ∈ 𝒟 P ∪ 𝒟 Q ⟶ s ∈ 𝒟 P ∪ 𝒟 Q"
         by(auto intro!:is_processT9[rule_format])
qed


lemma Rep_Abs_Ndet:
"Rep_process(Abs_process(ℱ P ∪ ℱ Q , 𝒟 P ∪ 𝒟 Q)) = (ℱ P ∪ ℱ Q , 𝒟 P ∪ 𝒟 Q)"
  by(simp only:CollectI Rep_process Abs_process_inverse is_process_REP_Ndet)


subsection‹Some Laws›
text ‹The commutativity of the operator helps to simplify the subsequent
      continuity proof and is therefore developed here: ›
lemma F_Ndet : "ℱ (P ⊓ Q) = ℱ P ∪ ℱ Q"
  apply (subst Failures_def)
  apply (simp only: Ndet_def)
  by (simp add: FAILURES_def Rep_Abs_Ndet)


lemma D_Ndet : "𝒟(P ⊓ Q) = 𝒟 P ∪ 𝒟 Q"
  by(subst D_def, simp only: Ndet_def Rep_Abs_Ndet DIVERGENCES_def snd_conv)


lemma T_Ndet : "𝒯 (P ⊓ Q) = 𝒯 P ∪ 𝒯 Q"
apply(subst Traces_def, simp only: Ndet_def Rep_Abs_Ndet TRACES_def FAILURES_def
                             fst_def snd_conv)
apply(auto simp: T_F F_T is_processT1 Nil_elem_T)
apply(rule_tac x="{}" in exI, simp add: T_F F_T is_processT1 Nil_elem_T)+
done

lemma Ndet_commute: "(P ⊓ Q) = (Q ⊓ P)"
by(auto simp: Process_eq_spec F_Ndet D_Ndet)

subsection‹The Continuity Rule›
lemma  mono_Ndet1: "P ⊑ Q ⟹ 𝒟 (Q ⊓ S) ⊆ 𝒟 (P ⊓ S)"
apply(drule le_approx1)
by (auto simp: Process_eq_spec F_Ndet D_Ndet)

lemma mono_Ndet2: "P ⊑ Q ⟹ (∀ s. s ∉ 𝒟 (P ⊓ S) ⟶ Ra (P ⊓ S) s = Ra (Q ⊓ S) s)"
apply(subst (asm) le_approx_def)
by (auto simp: Process_eq_spec F_Ndet D_Ndet Ra_def)

lemma mono_Ndet3: "P ⊑ Q ⟹ min_elems (𝒟 (P ⊓ S)) ⊆ 𝒯 (Q ⊓ S)"
apply(auto dest!:le_approx3 simp: min_elems_def subset_iff F_Ndet D_Ndet T_Ndet)
apply(erule_tac x="t" in allE, auto)
by (erule_tac x="[]" in allE, auto simp: less_list_def Nil_elem_T D_T)

lemma mono_Ndet[simp] : "P ⊑ Q ⟹ (P ⊓ S) ⊑ (Q ⊓ S)"
by(auto simp:le_approx_def mono_Ndet1 mono_Ndet2 mono_Ndet3)

lemma mono_Ndet_sym[simp] : "P ⊑ Q ⟹ (S ⊓ P) ⊑ (S ⊓ Q)"
by (auto simp: Ndet_commute)


lemma cont_Ndet1: 
assumes chain:"chain Y"
shows  "((⨆ i. Y i) ⊓ S) = (⨆ i. (Y i ⊓ S))"
proof -
   have A : "chain (λi. Y i ⊓ S)"
        apply(insert chain,rule chainI)
        apply(frule_tac i="i" in chainE)
        by(simp)
   show ?thesis using chain
        by(auto simp add: limproc_is_thelub Process_eq_spec D_Ndet F_Ndet F_LUB D_LUB A)
qed


lemma Ndet_cont[simp]: 
assumes f: "cont f"
and     g: "cont g"
shows      "cont (λx. f x ⊓ g x)"
proof -
   have A:"⋀x. cont f ⟹ cont g ⟹ cont (λX. (f x)⊓ X)"
          apply(rule contI2, rule monofunI)
          apply(auto)
          apply(subst Ndet_commute, subst cont_Ndet1)
          by   (auto simp:Ndet_commute)
   have B:"⋀y. cont f ⟹ cont g ⟹ cont (λx. f x ⊓ y)"
          apply(rule_tac c="(λ g. g ⊓ y)" in cont_compose)
          apply(rule contI2,rule monofunI)
          by   (simp_all add: cont_Ndet1)
   show ?thesis using f g
   by (rule_tac f="(λ x. (λ g. f x ⊓ g))" in cont_apply, auto simp: A B)
qed


end