Theory Proc_name_cms

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

theory Proc_name_cms = Proc_name + Domain_SF_prod_cms:

(*  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]

(*****************************************************************

         1. [[<C>]]SF : non expanding
         2.
         3. 
         4. 

 *****************************************************************)

(*********************************************************
                   map Proc_name T
 *********************************************************)

(*** restSF (sub) ***)

lemma Proc_name_restSF_sub:
   "ev1 rest n <= ev2 rest n
    ==> [[<C>]]SF ev1 rest n <= [[<C>]]SF ev2 rest n"
apply (simp add: Proc_name_evalSF)
apply (simp add: prod_restriction_def)
apply (simp add: order_prod_def)
done

(*** restSF (equal) ***)

lemma Proc_name_restSF:
   "ev1 rest n = ev2 rest n
    ==> [[<C>]]SF ev1 rest n = [[<C>]]SF ev2 rest n"
apply (rule order_antisym)
by (simp_all add: Proc_name_restSF_sub)

(*** Proc_name_evalSF_non_expanding ***)

lemma Proc_name_evalSF_non_expanding:
 "non_expanding [[<C>]]SF"
apply (simp add: non_expanding_def map_alpha_def)
apply (intro allI)
apply (rule rest_distance_subset)
apply (intro allI impI)
apply (rule Proc_name_restSF, simp)
done

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end