Theory STOP

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

theory STOP = CSP_semantics:

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

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

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

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

(*** STOP_memT ***)

lemma STOP_memT: "(t :t [[STOP]]T ev) = (t = []t)"
by (simp add: evalT_def memT_def Abs_domT_inverse)

(*** STOP_domF ***)

lemma STOP_domF: "{f. EX X. f = ([]t, X)} : domF"
by (simp add: domF_def HC_F2_def)

(*** STOP_memF ***)

lemma STOP_memF : "(f :f [[STOP]]F ev) = (EX X. f = ([]t, X))"
apply (simp add: memF_def evalF_def)
by (simp add: STOP_domF Abs_domF_inverse)

lemmas STOP_mem = STOP_memT STOP_memF

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

(* T2 *)

lemma STOP_T2 : "HC_T2 ([[STOP]]T ev, [[STOP]]F ev)"
by (simp add: HC_T2_def STOP_mem)

(* F3 *)

lemma STOP_F3 : "HC_F3 ([[STOP]]T ev, [[STOP]]F ev)"
by (simp add: HC_F3_def STOP_mem)

(* T3_F4 *)

lemma STOP_T3_F4 : "HC_T3_F4 ([[STOP]]T ev, [[STOP]]F ev)"
by (simp add: HC_T3_F4_def STOP_mem)

(*** STOP_domSF ***)

lemma STOP_domSF : "([[STOP]]T ev, [[STOP]]F ev) : domSF"
apply (simp add: domSF_iff)
apply (simp add: STOP_T2)
apply (simp add: STOP_F3)
apply (simp add: STOP_T3_F4)
done

end