Theory SKIP_cms

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

theory SKIP_cms = SKIP + 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. [[SKIP]]T : map
         2. [[SKIP]]F : map
         3. 
         4. 

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

(*********************************************************
                   map SKIP T
 *********************************************************)

(*** restT (subset) ***)

lemma SKIP_evalT_map_alpha: "0 <= alpha ==> map_alpha [[SKIP]]T alpha"
apply (simp add: map_alpha_def)
apply (simp add: evalT_def)
apply (simp add: real_mult_order_eq)
done

(*** SKIP_evalT_non_expanding ***)

lemma SKIP_evalT_non_expanding: "non_expanding [[SKIP]]T"
by (simp add: non_expanding_def SKIP_evalT_map_alpha)

(*** SKIP_evalT_contraction_alpha ***)

lemma SKIP_evalT_contraction_alpha:
   "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha [[SKIP]]T alpha"
by (simp add: contraction_alpha_def SKIP_evalT_map_alpha)

(*********************************************************
                   map SKIP F
 *********************************************************)

(*** restF (subset) ***)

lemma SKIP_evalF_map_alpha: "0 <= alpha ==> map_alpha [[SKIP]]F alpha"
apply (simp add: map_alpha_def)
apply (simp add: evalF_def)
apply (simp add: real_mult_order_eq)
done

(*** SKIP_evalF_non_expanding ***)

lemma SKIP_evalF_non_expanding: "non_expanding [[SKIP]]F"
by (simp add: non_expanding_def SKIP_evalF_map_alpha)

(*** SKIP_evalF_contraction_alpha ***)

lemma SKIP_evalF_contraction_alpha:
   "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha [[SKIP]]F alpha"
by (simp add: contraction_alpha_def SKIP_evalF_map_alpha)

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end