Theory SKIP

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

theory SKIP = CSP_semantics:

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

         1. ([[SKIP]]T ev, [[SKIP]]F ev) : domSF
         2. 
         3. 
         4. 

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

(*********************************************************
                     domT and domF
 *********************************************************)

(*** SKIP_memT ***)

lemma SKIP_memT: "(t :t [[SKIP]]T ev) = (t = []t | t = [Tick]t)"
by (simp add: evalT_def memT_def Abs_domT_inverse)

(*** SKIP_domF ***)

lemma SKIP_domF: "{f. (EX X. f = ([]t, X) & X <= Evset) |
                      (EX X. f = ([Tick]t, X)) } : domF"
by (auto simp add: domF_def HC_F2_def)

(*** SKIP_memF ***)

lemma SKIP_memF :
  "(f :f [[SKIP]]F ev) = ((EX X. f = ([]t, X) & X <= Evset) |
                          (EX X. f = ([Tick]t, X)))"
apply (simp add: memF_def evalF_def)
by (simp add: SKIP_domF Abs_domF_inverse)

lemmas SKIP_mem = SKIP_memT SKIP_memF

(*******************************
             domSF
 *******************************)

(* T2 *)

lemma SKIP_T2 : "HC_T2 ([[SKIP]]T ev, [[SKIP]]F ev)"
by (simp add: HC_T2_def SKIP_mem)

(* F3 *)

lemma SKIP_F3 : "HC_F3 ([[SKIP]]T ev, [[SKIP]]F ev)"
apply (simp add: HC_F3_def SKIP_mem)
by (auto simp add: Evset_def)

(* T3_F4 *)

lemma SKIP_T3_F4 : "HC_T3_F4 ([[SKIP]]T ev, [[SKIP]]F ev)"
by (simp add: HC_T3_F4_def SKIP_mem)

(*** SKIP_domSF ***)

lemma SKIP_domSF : "([[SKIP]]T ev, [[SKIP]]F ev) : domSF"
apply (simp add: domSF_iff)
apply (simp add: SKIP_T2)
apply (simp add: SKIP_F3)
apply (simp add: SKIP_T3_F4)
done

end