Theory CSP_F_continuous

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   July 2005 (modified)    |
            |              September 2005 (modified)    |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_continuous = CSP_F_failuresfun + Domain_F_cpo + CSP_T_mono:

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

         1. continuous failuresfun
         2. continuous failuresFun
         3. continuous [[ ]]Ffun
         4. continuous [[ ]]FFun

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

(*=============================================================*
 |                    tracesfun fstF                           |
 *=============================================================*)

lemma continuous_tracesfun_fstF:
   "Pf : Procfun ==> continuous (%SFf. tracesfun Pf (fstF o SFf))"
apply (subgoal_tac "(%SFf. tracesfun Pf (fstF o SFf)) = (tracesfun Pf) o (op o fstF)")
apply (simp add: continuous_tracesfun continuous_op_fstF compo_continuous)
apply (simp add: expand_fun_eq)
done

(*--------------------------------*
 |        STOP,SKIP,DIV           |
 *--------------------------------*)

lemma continuous_failuresfun_STOP: "continuous (failuresfun (%f. STOP))"
by (simp add: failuresfun_simp continuous_Constant)

lemma continuous_failuresfun_SKIP: "continuous (failuresfun (%f. SKIP))"
by (simp add: failuresfun_simp continuous_Constant)

lemma continuous_failuresfun_DIV: "continuous (failuresfun (%f. DIV))"
by (simp add: failuresfun_simp continuous_Constant)

(*--------------------------------*
 |          Act_prefix            |
 *--------------------------------*)

lemma continuous_failuresfun_Act_prefix:
 "continuous (failuresfun Pf) ==> continuous (failuresfun (%f. a -> (Pf f)))"
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (drule_tac x="X" in spec, simp)
apply (elim conjE exE)
apply (rule_tac x="x" in exI, simp)

apply (subgoal_tac "X ~= {}")
apply (simp add: isLUB_UnionF)
apply (rule order_antisym)

(* <= *)
apply (rule)
apply (simp add: in_failuresfun)
apply (erule disjE, fast)
apply (elim conjE exE)
apply (simp)

(* => *)
apply (rule)
apply (simp)
apply (erule bexE)
apply (simp add: in_failuresfun)
apply (erule disjE, simp)
apply (elim conjE exE)
apply (rule disjI2)
apply (rule_tac x="sa" in exI, simp)
apply (rule_tac x="xa" in bexI)
apply (simp_all)

by (simp add: directed_def)

(*--------------------------------*
 |        Ext_pre_choice          |
 *--------------------------------*)

lemma continuous_failuresfun_Ext_pre_choice:
 "ALL a. continuous (failuresfun (Pff a))
     ==> continuous (failuresfun (%f. ? a:X -> (Pff a f)))"
apply (simp add: continuous_iff)
apply (intro allI impI)

apply (subgoal_tac "Xa ~= {}")
apply (erule exchange_forall_orderE)
apply (drule_tac x="Xa" in spec)
apply (simp add: isLUB_UnionF)

apply (rule_tac x="LUB Xa" in exI)
apply (rule conjI)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failuresfun)
 apply (erule disjE, fast)
 apply (elim conjE exE)
 apply (simp)
 apply (drule_tac x="a" in spec)
 apply (elim conjE exE)
 apply (subgoal_tac "LUB Xa = x", simp)
 apply (simp add: isLUB_LUB)

(* => *)
 apply (rule)
 apply (simp)
 apply (erule bexE)
 apply (simp add: in_failuresfun)
 apply (erule disjE, simp)
 apply (elim conjE exE)
 apply (rule disjI2)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sa" in exI, simp)

 apply (drule_tac x="a" in spec)
 apply (elim conjE exE)
 apply (subgoal_tac "LUB Xa = xa", simp)
 apply (rule_tac x="x" in bexI)
 apply (simp)
 apply (simp)
 apply (simp add: isLUB_LUB)

 apply (drule_tac x="a" in spec)
 apply (elim conjE exE)
 apply (simp add: isLUB_LUB)

by (simp add: directed_def)

(*--------------------------------*
 |          Ext_choice            |
 *--------------------------------*)

lemma continuous_failuresfun_Ext_choice:
 "[| Pf : Procfun ; Qf : Procfun ;
     continuous (failuresfun Pf) ; continuous (failuresfun Qf) |]
  ==> continuous (failuresfun (%f. (Pf f [+] Qf f)))"
apply (subgoal_tac "mono (failuresfun Pf) & mono (failuresfun Qf)")
apply (subgoal_tac "continuous (%SFf. tracesfun Pf (fstF o SFf)) &
                    continuous (%SFf. tracesfun Qf (fstF o SFf))")
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (elim conjE)
apply (drule_tac x="X" in spec, simp)
apply (drule_tac x="X" in spec, simp)
apply (drule_tac x="X" in spec, simp)
apply (drule_tac x="X" in spec, simp)
apply (elim conjE exE)

apply (subgoal_tac "xa = x")
apply (subgoal_tac "xb = x")
apply (subgoal_tac "xc = x")
apply (rule_tac x="x" in exI, simp)

apply (subgoal_tac "X ~= {}")
apply (simp add: isLUB_UnionF)
apply (simp add: isLUB_UnionT)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failuresfun)
 apply (elim conjE bexE disjE)

 (* 1 *)
  apply (simp add: directed_def)
  apply (drule_tac x="xd" in spec)
  apply (drule_tac x="xe" in spec)
  apply (simp, elim conjE exE)
  apply (rule_tac x="z" in bexI)
  apply (rule disjI1)
  apply (rule conjI)
  apply (rule memF_subsetF, simp)
  apply (simp add: mono_def)
  apply (rotate_tac -4)
  apply (rule memF_subsetF, simp)
  apply (simp add: mono_def)

 (* 2-5 *)
  apply (fast)+

(* => *)
 apply (rule)
 apply (simp add: in_failuresfun)
 apply (fast)

apply (simp add: directed_def)
apply (rule LUB_unique, simp_all)+

apply (simp add: continuous_tracesfun_fstF)
apply (simp add: continuous_mono)
done

(*--------------------------------*
 |          Int_choice            |
 *--------------------------------*)

lemma continuous_failuresfun_Int_choice:
 "[| continuous (failuresfun Pf) ; continuous (failuresfun Qf) |]
  ==> continuous (failuresfun (%f. (Pf f |~| Qf f)))"
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (drule_tac x="X" in spec, simp)
apply (drule_tac x="X" in spec, simp)
apply (elim conjE exE)

apply (subgoal_tac "xa = x")
apply (rule_tac x="x" in exI, simp)

apply (subgoal_tac "X ~= {}")
apply (simp add: isLUB_UnionF)
apply (rule order_antisym)
 apply (rule, simp add: in_failuresfun, fast)
 apply (rule, simp add: in_failuresfun, fast)
apply (simp add: directed_def)
by (rule LUB_unique, simp_all)

(*--------------------------------*
 |        Rep_int_choice          |
 *--------------------------------*)

lemma continuous_failuresfun_Rep_int_choice:
 "ALL c. continuous (failuresfun (Pff c))
  ==> continuous (failuresfun (%f. !! c:C .. (Pff c f)))"
apply (simp add: continuous_iff)
apply (intro allI impI)

apply (subgoal_tac "X ~= {}")
apply (erule exchange_forall_orderE)
apply (drule_tac x="X" in spec)
apply (simp add: isLUB_UnionF)

apply (rule_tac x="LUB X" in exI)
apply (rule conjI)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failuresfun)
 apply (elim conjE bexE)
 apply (drule_tac x="c" in spec)
 apply (elim conjE exE)
 apply (subgoal_tac "LUB X = x", simp)
 apply (elim bexE)
 apply (rule_tac x="xa" in bexI)
 apply (fast)
 apply (simp)
 apply (simp add: isLUB_LUB)

(* => *)
 apply (rule)
 apply (simp)
 apply (erule bexE)
 apply (simp add: in_failuresfun)
 apply (elim conjE bexE)
 apply (rule_tac x="c" in bexI)

 apply (drule_tac x="c" in spec)
 apply (elim conjE exE)
 apply (subgoal_tac "LUB X = xa", simp)
 apply (rule_tac x="x" in bexI)
 apply (simp)
 apply (simp)
 apply (simp add: isLUB_LUB)
 apply (simp)

 apply (drule_tac x="c" in spec)
 apply (elim conjE exE)
 apply (simp add: isLUB_LUB)

by (simp add: directed_def)

(*--------------------------------*
 |              IF                |
 *--------------------------------*)

lemma continuous_failuresfun_IF:
 "[| continuous (failuresfun Pf) ; continuous (failuresfun Qf) |]
  ==> continuous (failuresfun (%f. IF b THEN (Pf f) ELSE (Qf f)))"
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (drule_tac x="X" in spec, simp)
apply (drule_tac x="X" in spec, simp)
apply (elim conjE exE)
apply (case_tac "b")
 apply (rule_tac x="x" in exI, simp)
 apply (simp add: failuresfun_def)
 apply (simp add: failures_def)
 apply (rule_tac x="x" in exI, simp)
 apply (simp add: failuresfun_def)
 apply (simp add: failures_def)
apply (subgoal_tac "xa = x", simp)
by (rule LUB_unique, simp_all)

(*--------------------------------*
 |           Parallel             |
 *--------------------------------*)

lemma continuous_failuresfun_Parallel:
 "[| continuous (failuresfun Pf) ; continuous (failuresfun Qf) |]
  ==> continuous (failuresfun (%f. (Pf f) |[X]| (Qf f)))"
apply (subgoal_tac "mono (failuresfun Pf) & mono (failuresfun Qf)")

apply (simp add: continuous_iff)
apply (intro allI impI)
apply (drule_tac x="Xa" in spec, simp)
apply (drule_tac x="Xa" in spec, simp)
apply (elim conjE exE)

apply (subgoal_tac "xa = x")
apply (rule_tac x="x" in exI, simp)

apply (subgoal_tac "Xa ~= {}")
apply (simp add: isLUB_UnionF)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failuresfun)
 apply (elim exE bexE conjE)

 apply (simp add: directed_def)
 apply (drule_tac x="xb" in spec)
 apply (drule_tac x="xc" in spec)
 apply (simp, elim conjE exE)
 apply (rule_tac x="z" in bexI)
 apply (rule_tac x="Y" in exI)
 apply (rule_tac x="Z" in exI)
 apply (simp)
 apply (rule_tac x="sa" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp)

 apply (rule conjI)
 apply (rule memF_subsetF, simp)
 apply (simp add: mono_def)
 apply (rotate_tac -4)
 apply (rule memF_subsetF, simp)
 apply (simp add: mono_def)
 apply (simp)

(* => *)
 apply (rule)
 apply (simp add: in_failuresfun)
 apply (fast)

apply (simp add: directed_def)
apply (simp add: LUB_unique)

by (simp add: continuous_mono)

(*--------------------------------*
 |            Hiding              |
 *--------------------------------*)

lemma continuous_failuresfun_Hiding:
 "continuous (failuresfun Pf)
  ==> continuous (failuresfun (%f. (Pf f) -- X))"
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (drule_tac x="Xa" in spec, simp)
apply (elim conjE exE)

apply (rule_tac x="x" in exI, simp)
apply (subgoal_tac "Xa ~= {}")
apply (simp add: isLUB_UnionF)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failuresfun)
 apply (fast)

(* => *)
 apply (rule)
 apply (simp add: in_failuresfun)
 apply (fast)

by (simp add: directed_def)

(*--------------------------------*
 |           Renaming             |
 *--------------------------------*)

lemma continuous_failuresfun_Renaming:
 "continuous (failuresfun Pf)
  ==> continuous (failuresfun (%f. (Pf f) [[r]]))"
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (drule_tac x="X" in spec, simp)
apply (elim conjE exE)

apply (rule_tac x="x" in exI, simp)
apply (subgoal_tac "X ~= {}")
apply (simp add: isLUB_UnionF)
apply (rule order_antisym)
 apply (rule, simp add: in_failuresfun, fast)
 apply (rule, simp add: in_failuresfun, fast)
by (simp add: directed_def)

(*--------------------------------*
 |           Seq_compo            |
 *--------------------------------*)

lemma continuous_failuresfun_Seq_compo:
 "[| Pf : Procfun ;
     continuous (failuresfun Pf) ; continuous (failuresfun Qf) |]
  ==> continuous (failuresfun (%f. (Pf f ;; Qf f)))"
apply (subgoal_tac "mono (tracesfun Pf) & mono (failuresfun Qf)")
apply (subgoal_tac "continuous (%SFf. tracesfun Pf (fstF o SFf))")
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (drule_tac x="X" in spec, simp)
apply (drule_tac x="X" in spec, simp)
apply (drule_tac x="X" in spec, simp)
apply (elim conjE exE)

apply (subgoal_tac "xa = x")
apply (subgoal_tac "xb = x")
apply (rule_tac x="x" in exI, simp)

apply (subgoal_tac "X ~= {}")
apply (simp add: isLUB_UnionF)
apply (simp add: isLUB_UnionT)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failuresfun)
 apply (elim bexE exE conjE disjE)

 (* 1 *)
  apply (fast)

 (* 2 *)
  apply (simp add: directed_def)
  apply (drule_tac x="xc" in spec)
  apply (drule_tac x="xd" in spec)
  apply (simp, elim conjE exE)
  apply (rule_tac x="z" in bexI)
  apply (rule disjI2)
  apply (rule_tac x="sa" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp)

  apply (rule conjI)
  apply (rule memT_subdomT, simp)
  apply (simp add: mono_def)
  apply (subgoal_tac "fstF o xc <= fstF o z")
  apply (simp add: comp_def)

  apply (simp add: comp_def)
  apply (simp add: order_prod_def)
  apply (simp add: mono_fstF[simplified mono_def])

  apply (rotate_tac -4)
  apply (rule memF_subsetF, simp)
  apply (simp add: mono_def)
  apply (simp)

(* => *)
 apply (rule)
 apply (simp add: in_failuresfun)
 apply (fast)

apply (simp add: directed_def)
apply (simp add: LUB_unique)+
apply (simp add: continuous_tracesfun_fstF)
apply (simp add: continuous_mono)
apply (simp add: mono_tracesfun)
done

(*--------------------------------*
 |          Depth_rest            |
 *--------------------------------*)

lemma continuous_failuresfun_Depth_rest:
 "continuous (failuresfun Pf)
  ==> continuous (failuresfun (%f. (Pf f) |. n))"
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (drule_tac x="X" in spec, simp)
apply (elim conjE exE)

apply (rule_tac x="x" in exI, simp)
apply (subgoal_tac "X ~= {}")
apply (simp add: isLUB_UnionF)
apply (rule order_antisym)
 apply (rule, simp add: in_failuresfun)
 apply (rule, simp add: in_failuresfun)
by (simp add: directed_def)

(*--------------------------------*
 |            variable            |
 *--------------------------------*)

lemma continuous_failuresfun_variable: 
   "continuous (failuresfun (%f. f pn))"
apply (subgoal_tac "continuous [[%f. f pn]]Ffun")
apply (simp add: semF_decompo_fun)
apply (simp add: continuous_domF_decompo
                 tracesfun_failuresfun_in_domF)
apply (erule conjE)
apply (simp)

apply (simp add: semFfun_variable)
apply (simp add: continuous_prod_variable)
done

(*--------------------------------*
 |            Procfun             |
 *--------------------------------*)

lemma continuous_failuresfun: 
  "Pf : Procfun ==> continuous (failuresfun Pf)"
apply (rule Procfun.induct[of Pf])
apply (simp)
apply (simp add: continuous_failuresfun_variable)
apply (simp add: continuous_failuresfun_STOP)
apply (simp add: continuous_failuresfun_SKIP)
apply (simp add: continuous_failuresfun_DIV)
apply (simp add: continuous_failuresfun_Act_prefix)
apply (simp add: continuous_failuresfun_Ext_pre_choice)
apply (simp add: continuous_failuresfun_Ext_choice)
apply (simp add: continuous_failuresfun_Int_choice)
apply (simp add: continuous_failuresfun_Rep_int_choice)
apply (simp add: continuous_failuresfun_IF)
apply (simp add: continuous_failuresfun_Parallel)
apply (simp add: continuous_failuresfun_Hiding)
apply (simp add: continuous_failuresfun_Renaming)
apply (simp add: continuous_failuresfun_Seq_compo)
apply (simp add: continuous_failuresfun_Depth_rest)
done

(*=============================================================*
 |                         [[P]]Ffun                           |
 *=============================================================*)

lemma continuous_semFfun: 
  "Pf : Procfun ==> continuous [[Pf]]Ffun"
apply (simp add: semF_decompo_fun)
apply (simp add: continuous_domF_decompo tracesfun_failuresfun_in_domF)
apply (simp add: continuous_tracesfun_fstF)
apply (simp add: continuous_failuresfun)
done

(*=============================================================*
 |                         failuresFun                           |
 *=============================================================*)

lemma continuous_failuresFun: 
  "PF : ProcFun ==> continuous (failuresFun PF)"
apply (simp add: prod_continuous)
apply (simp add: proj_failuresFun_failuresfun)
apply (simp add: ProcFun_def)
apply (simp add: continuous_failuresfun)
done

(*=============================================================*
 |                         [[P]]FFun                           |
 *=============================================================*)

lemma continuous_semFFun: 
  "PF : ProcFun ==> continuous [[PF]]FFun"
apply (simp add: prod_continuous)
apply (simp add: proj_semFFun_semFfun)
apply (simp add: ProcFun_def)
apply (simp add: continuous_semFfun)
done

end