Theory CSP_proc_cpo

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

theory CSP_proc_cpo =
       CSP_proc +
(*     STOP_cpo +
       SKIP_cpo +
       DIV_cpo +  *)
       Act_prefix_cpo +
(*     Ext_choice_cpo +
       Ext_pre_choice_cpo +
       Int_choice_cpo +
       Rep_int_choice_cpo +
       Conditional_cpo +
       Parallel_cpo +
       Renaming_cpo +
       Seq_compo_cpo + *)
       Proc_name_cpo :

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

         1. [[P]]SF : continuous
         2.
         3. 
         4. 

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

(*********************************************************
              continuous decomposition
 *********************************************************)

(* Abs_domSF *)

lemma continuous_Abs_domSF_only_if:
  "continuous [[P]]SF ==> continuous ([[P]]T ** [[P]]F)"
apply (simp add: evalSF_def)
apply (simp add: pairSF_def)
apply (simp add: pair_fun_def)
apply (insert compo_continuous
       [of "(%ev. Abs_domSF ([[P]]T ev, [[P]]F ev))" "Rep_domSF" ])
apply (simp add: comp_def)
apply (simp add: cont_Rep_domSF)
apply (simp add: Abs_domSF_inverse)
done

lemma continuous_Abs_domSF_if:
  "continuous ([[P]]T ** [[P]]F) ==> continuous [[P]]SF"
apply (simp add: evalSF_def)
apply (simp add: pairSF_def)
apply (simp add: pair_fun_def)
apply (insert continuous_Abs_domSF[of "(%x. ([[P]]T x, [[P]]F x))"])
by (simp add: comp_def)

(* iff *)

lemma continuous_Abs_domSF:
  "continuous [[P]]SF = continuous ([[P]]T ** [[P]]F)"
apply (rule iffI)
apply (simp add: continuous_Abs_domSF_only_if)
apply (simp add: continuous_Abs_domSF_if)
done

(* decompo *)

lemma continuous_evalSF_decompo:
  "continuous [[P]]SF = (continuous [[P]]T & continuous [[P]]F)"
apply (simp add: continuous_Abs_domSF)
by (simp add: pair_continuous)

(*****************************************************************
                !!!   proc continuous   !!!
             This proof will be completed soon.
 *****************************************************************)

lemma evalSF_continuous: "continuous [[P]]SF"
apply (simp add: continuous_evalSF_decompo)
apply (induct_tac P)
defer
defer
defer
apply (simp add: Act_prefix_evalT_continuous
                 Act_prefix_evalF_continuous)
defer
defer
defer
defer
defer
defer
defer
defer
defer
apply (simp add: continuous_evalSF_decompo[THEN sym])
apply (simp add: Proc_name_evalSF_continuous)
oops

end