Theory DIV

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

theory DIV = CSP_semantics:

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

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

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

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

(*** DIV_memT ***)

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

(*** DIV_memF ***)

lemma DIV_memF : "(f ~:f [[DIV]]F ev)"
apply (simp add: memF_def evalF_def)
by (simp add: Abs_domF_inverse empF_def)

lemmas DIV_mem = DIV_memT DIV_memF

(*******************************
       DIVsf in domSF
 *******************************)

(* T2 *)

lemma DIV_T2 : "HC_T2 ([[DIV]]T ev, [[DIV]]F ev)"
by (simp add: HC_T2_def DIV_mem)

(* F3 *)

lemma DIV_F3 : "HC_F3 ([[DIV]]T ev, [[DIV]]F ev)"
by (simp add: HC_F3_def DIV_mem)

(* T3_F4 *)

lemma DIV_T3_F4 : "HC_T3_F4 ([[DIV]]T ev, [[DIV]]F ev)"
by (simp add: HC_T3_F4_def DIV_mem)

(*** DIV_domSF ***)

lemma DIV_domSF : "([[DIV]]T ev, [[DIV]]F ev) : domSF"
apply (simp add: domSF_iff)
apply (simp add: DIV_T2)
apply (simp add: DIV_F3)
apply (simp add: DIV_T3_F4)
done

end