Theory Proc_name

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Proc_name = CSP_semantics:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

(*********************************************************
                        DomSF
 *********************************************************)

(*** Proc_name_memSF ***)

lemma Proc_name_evalSF: "[[<C>]]SF ev = (ev C)"
apply (simp add: evalSF_def)
apply (simp add: pairSF_def)
apply (simp add: evalT_def evalF_def)
apply (simp add: fstSF_def sndSF_def)
apply (simp add: Rep_domSF_inverse)
done

(*********************************************************
                      mono
 *********************************************************)

(*** T ***)

lemma Proc_name_evalT_mono:
  "ev1 <= ev2 ==> [[<C>]]T ev1 <= [[<C>]]T ev2"
apply (simp add: subsetSF_prod_decompo)
apply (simp add: evalT_def)
apply (simp add: order_prod_def)
done

(*** F ***)

lemma Proc_name_evalF_mono:
  "ev1 <= ev2 ==> [[<C>]]F ev1 <= [[<C>]]F ev2"
apply (simp add: subsetSF_prod_decompo)
apply (simp add: evalF_def)
apply (simp add: order_prod_def)
done

(****************** to add them again ******************)

declare disj_not1   [simp]
declare not_None_eq [simp]

end