Theory CSP_proc_cpo

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |              December 2004                |
            |              February 2005  (modified)    |
            |        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       + Hiding_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   !!!
 *****************************************************************)

lemma evalSF_continuous: "continuous [[P]]SF"
apply (simp add: continuous_evalSF_decompo)
apply (induct_tac P)
apply (simp add: STOP_evalT_continuous
                 STOP_evalF_continuous)
apply (simp add: SKIP_evalT_continuous
                 SKIP_evalF_continuous)
apply (simp add: DIV_evalT_continuous
                 DIV_evalF_continuous)
apply (simp add: Act_prefix_evalT_continuous
                 Act_prefix_evalF_continuous)
apply (simp add: Ext_pre_choice_evalT_continuous
                 Ext_pre_choice_evalF_continuous)
apply (simp add: Ext_choice_evalT_continuous
                 Ext_choice_evalF_continuous)
apply (simp add: Int_choice_evalT_continuous
                 Int_choice_evalF_continuous)
apply (simp add: Rep_int_choice_evalT_continuous
                 Rep_int_choice_evalF_continuous)
apply (simp add: Conditional_evalT_continuous
                 Conditional_evalF_continuous)
apply (simp add: Parallel_evalT_continuous
                 Parallel_evalF_continuous)
apply (simp add: Hiding_evalT_continuous
                 Hiding_evalF_continuous)
apply (simp add: Renaming_evalT_continuous
                 Renaming_evalF_continuous)
apply (simp add: Seq_compo_evalT_continuous
                 Seq_compo_evalF_continuous)
apply (simp add: continuous_evalSF_decompo[THEN sym])
apply (simp add: Proc_name_evalSF_continuous)
done

(*****************************************************************
               !!!   [[df]]DF continuous   !!!
 *****************************************************************)

lemma evalDF_continuous: "continuous [[df]]DF"
apply (simp add: prod_continuous)
apply (simp add: proj_fun_evalDF)
apply (simp add: evalSF_continuous)
done

(*****************************************************************
                      Tarski on evalDF
 *****************************************************************)

lemma evalDF_Tarski_thm:
   "[[df]]DF hasLFP & LFP [[df]]DF isLUB {x. EX n. x = ([[df]]DF^n) Bot}"
apply (rule Tarski_thm)
apply (simp add: evalDF_continuous)
done

end