Theory Ndet

(*<*)
―‹ ********************************************************************
 * 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‹ Nondeterministic Choice Operator Definition ›

theory  Ndet 
imports Process
begin


subsection‹The Ndet Operator Definition›
lift_definition
        Ndet     :: "[ process, process]   process"   (infixl "|-|" 80)
is   "λP Q. ( 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. ([], {})  ( P   Q)"
         by(simp add: is_processT1)
next
    show "P Q. s X. (s, X)  ( P   Q)  front_tickFree s"
         by(auto simp: is_processT2)
next
    show "P Q. s t.   (s @ t, {}) ( P   Q)  (s, {})  ( P   Q)"
         by (auto simp: is_processT1 dest!: is_processT3[rule_format])
next
    show "P Q. 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 "P Q. 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 "P Q. 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 "P Q. s t. s  𝒟 P  𝒟 Q  tickFree s  front_tickFree t  s @ t  𝒟 P  𝒟 Q"
         by(auto simp: is_processT7)
next
    show "P Q. s X. s  𝒟 P  𝒟 Q  (s, X)  ( P   Q)"
         by(auto simp: is_processT8[rule_format])
next
    show "P Q. s. s @ [tick]  𝒟 P  𝒟 Q  s  𝒟 P  𝒟 Q"
         by(auto intro!:is_processT9[rule_format])
     qed

notation
  Ndet (infixl "" 80)


subsection ‹The Projections›

lemma F_Ndet : " (P  Q) =  P   Q"
  by (simp add: FAILURES_def Failures.rep_eq Ndet.rep_eq)
 
lemma D_Ndet : "𝒟 (P  Q) = 𝒟 P  𝒟 Q"
  by (simp add: DIVERGENCES_def Divergences.rep_eq Ndet.rep_eq)

lemma T_Ndet : "𝒯 (P  Q) = 𝒯 P  𝒯 Q"
  apply (subst Traces.rep_eq, simp add: TRACES_def Failures.rep_eq[symmetric] F_Ndet)
  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 commutativity of the operator helps to simplify the subsequent
      continuity proof and is therefore developed here: ›

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