Theory CSP_T_continuous

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

theory CSP_T_continuous
imports CSP_T_traces Domain_T_cpo CPO_prod
begin

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

         1. continuous traces
         2. continuous [[ ]]Tfun

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

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

(*** Constant_continuous ***)

lemma continuous_Constant: "continuous (%p. C)"
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (insert complete_cpo_lm)
apply (drule_tac x="X" in spec, simp)
apply (simp add: hasLUB_def)
apply (elim exE)
apply (simp add: image_def isLUB_def isUB_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (drule mp)
apply (simp add: directed_def)
apply (auto)
done

lemma continuous_traces_STOP: "continuous (traces (STOP))"
by (simp add: traces_def continuous_Constant)

lemma continuous_traces_SKIP: "continuous (traces (SKIP))"
by (simp add: traces_def continuous_Constant)

lemma continuous_traces_DIV: "continuous (traces (DIV))"
by (simp add: traces_def continuous_Constant)

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

lemma continuous_traces_Act_prefix:
 "continuous (traces P) ==> continuous (traces (a -> P))"
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_UnionT)
apply (rule order_antisym)

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

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

by (simp add: directed_def)

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

lemma continuous_traces_Ext_pre_choice:
 "ALL a. continuous (traces (Pf a))
  ==> continuous (traces (? a:X -> (Pf a)))"
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_UnionT)

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

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 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_traces)
 apply (erule disjE, simp)
 apply (elim conjE exE)
 apply (rule disjI2)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="s" 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_traces_Ext_choice:
 "[| continuous (traces P) ; continuous (traces Q) |]
  ==> continuous (traces (P [+] Q))"
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_UnionT)
apply (rule order_antisym)
 apply (rule, simp add: in_traces, fast)
 apply (rule, simp add: in_traces, fast)
apply (simp add: directed_def)
by (rule LUB_unique, simp_all)

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

lemma continuous_traces_Int_choice:
 "[| continuous (traces P) ; continuous (traces Q) |]
  ==> continuous (traces (P |~| Q))"
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_UnionT)
apply (rule order_antisym)
 apply (rule, simp add: in_traces, fast)
 apply (rule, simp add: in_traces, fast)
apply (simp add: directed_def)
by (rule LUB_unique, simp_all)

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

lemma continuous_traces_Rep_int_choice:
 "ALL c. continuous (traces(Pf c))
  ==> continuous (traces (!! :C .. Pf))"
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_UnionT)

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

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (erule disjE, fast)
 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_traces)
 apply (erule disjE, simp)
 apply (elim conjE bexE)
 apply (rule disjI2)
 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_traces_IF:
 "[| continuous (traces P) ; continuous (traces Q) |]
  ==> continuous (traces (IF b THEN P ELSE Q))"
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: traces_def)
 apply (rule_tac x="xa" in exI, simp)
 apply (simp add: traces_def)
done

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

lemma continuous_traces_Parallel:
 "[| continuous (traces P) ; continuous (traces Q) |]
  ==> continuous (traces (P |[X]| Q))"
apply (subgoal_tac "mono (traces P) & mono (traces Q)")

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_UnionT)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 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="s" in exI)
 apply (rule_tac x="ta" in exI)
 apply (simp)
 apply (rule conjI)
 apply (rule memT_subdomT, simp)
 apply (simp add: mono_def)
 apply (rotate_tac -4)
 apply (rule memT_subdomT, simp)
 apply (simp add: mono_def)
 apply (simp)

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

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

by (simp add: continuous_mono)

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

lemma continuous_traces_Hiding:
 "continuous (traces P)
  ==> continuous (traces (P -- 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_UnionT)
apply (rule order_antisym)

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

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

by (simp add: directed_def)

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

lemma continuous_traces_Renaming:
 "continuous (traces P)
  ==> continuous (traces (P [[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_UnionT)
apply (rule order_antisym)
 apply (rule, simp add: in_traces, fast)
 apply (rule, simp add: in_traces, fast)
by (simp add: directed_def)

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

lemma continuous_traces_Seq_compo:
 "[| continuous (traces P) ; continuous (traces Q) |]
  ==> continuous (traces (P ;; Q))"
apply (subgoal_tac "mono (traces P) & mono (traces Q)")
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_UnionT)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim bexE exE conjE disjE)
 apply (rule_tac x="xb" in bexI)
 apply (fast)
 apply (simp)

 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 disjI2)
 apply (rule_tac x="s" in exI)
 apply (rule_tac x="ta" in exI)
 apply (simp)
 apply (rule conjI)
 apply (rule memT_subdomT, simp)
 apply (simp add: mono_def)
 apply (rotate_tac -4)
 apply (rule memT_subdomT, simp)
 apply (simp add: mono_def)
 apply (simp)

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

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

by (simp add: continuous_mono)

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

lemma continuous_traces_Depth_rest:
 "continuous (traces P)
  ==> continuous (traces (P |. 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_UnionT)
apply (rule order_antisym)
 apply (rule, simp add: in_traces)
 apply (rule, simp add: in_traces)
by (simp add: directed_def)

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

lemma continuous_traces_variable: 
   "continuous (traces ($p))"
apply (simp add: traces_def)
apply (simp add: continuous_prod_variable)
done

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

lemma continuous_traces: 
  "continuous (traces P)"
apply (induct_tac P)
apply (simp add: continuous_traces_STOP)
apply (simp add: continuous_traces_SKIP)
apply (simp add: continuous_traces_DIV)
apply (simp add: continuous_traces_Act_prefix)
apply (simp add: continuous_traces_Ext_pre_choice)
apply (simp add: continuous_traces_Ext_choice)
apply (simp add: continuous_traces_Int_choice)
apply (simp add: continuous_traces_Rep_int_choice)
apply (simp add: continuous_traces_IF)
apply (simp add: continuous_traces_Parallel)
apply (simp add: continuous_traces_Hiding)
apply (simp add: continuous_traces_Renaming)
apply (simp add: continuous_traces_Seq_compo)
apply (simp add: continuous_traces_Depth_rest)
apply (simp add: continuous_traces_variable)
done

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

lemma continuous_semTf: 
  "continuous [[P]]Tf"
apply (simp add: semTf_def)
apply (simp add: continuous_traces)
done

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

lemma continuous_semTfun: "continuous [[Pf]]Tfun"
apply (simp add: prod_continuous)
apply (simp add: semTfun_def)
apply (simp add: proj_fun_def)
apply (simp add: comp_def)
apply (simp add: continuous_semTf)
done

end