Theory CSP_T_continuous

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T

theory CSP_T_continuous
imports CSP_T_tracesfun Domain_T_cpo CPO_prod
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   July 2005  (modified)   |
            |                 August 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_T_continuous = CSP_T_tracesfun + Domain_T_cpo + CPO_prod:

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

         1. continuous tracesfun
         2. continuous tracesFun
         3. continuous [[ ]]Tfun
         4. continuous [[ ]]TFun

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

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

(*** Constant_continuous ***)

lemma continuous_Constant: "continuous (%f. P)"
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_tracesfun_STOP: "continuous (tracesfun (%f. STOP))"
by (simp add: tracesfun_simp continuous_Constant)

lemma continuous_tracesfun_SKIP: "continuous (tracesfun (%f. SKIP))"
by (simp add: tracesfun_simp continuous_Constant)

lemma continuous_tracesfun_DIV: "continuous (tracesfun (%f. DIV))"
by (simp add: tracesfun_simp continuous_Constant)

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

lemma continuous_tracesfun_Act_prefix:
 "continuous (tracesfun Pf) ==> continuous (tracesfun (%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_UnionT)
apply (rule order_antisym)

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

(* => *)
apply (rule)
apply (simp)
apply (erule bexE)
apply (simp add: in_tracesfun)
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_tracesfun_Ext_pre_choice:
 "ALL a. continuous (tracesfun (Pff a))
  ==> continuous (tracesfun (%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_UnionT)

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

(* <= *)
 apply (rule)
 apply (simp add: in_tracesfun)
 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_tracesfun)
 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_tracesfun_Ext_choice:
 "[| continuous (tracesfun Pf) ; continuous (tracesfun Qf) |]
  ==> continuous (tracesfun (%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_UnionT)
apply (rule order_antisym)
 apply (rule, simp add: in_tracesfun, fast)
 apply (rule, simp add: in_tracesfun, fast)
apply (simp add: directed_def)
by (rule LUB_unique, simp_all)

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

lemma continuous_tracesfun_Int_choice:
 "[| continuous (tracesfun Pf) ; continuous (tracesfun Qf) |]
  ==> continuous (tracesfun (%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_UnionT)
apply (rule order_antisym)
 apply (rule, simp add: in_tracesfun, fast)
 apply (rule, simp add: in_tracesfun, fast)
apply (simp add: directed_def)
by (rule LUB_unique, simp_all)

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

lemma continuous_tracesfun_Rep_int_choice:
 "ALL c. continuous (tracesfun (Pff c))
  ==> continuous (tracesfun (%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_UnionT)

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

(* <= *)
 apply (rule)
 apply (simp add: in_tracesfun)
 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_tracesfun)
 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_tracesfun_IF:
 "[| continuous (tracesfun Pf) ; continuous (tracesfun Qf) |]
  ==> continuous (tracesfun (%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: tracesfun_def)
 apply (simp add: traces_def)
 apply (rule_tac x="x" in exI, simp)
 apply (simp add: tracesfun_def)
 apply (simp add: traces_def)
apply (subgoal_tac "xa = x", simp)
by (rule LUB_unique, simp_all)

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

lemma continuous_tracesfun_Parallel:
 "[| continuous (tracesfun Pf) ; continuous (tracesfun Qf) |]
  ==> continuous (tracesfun (%f. (Pf f) |[X]| (Qf f)))"
apply (subgoal_tac "mono (tracesfun Pf) & mono (tracesfun 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_UnionT)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_tracesfun)
 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_tracesfun)
 apply (fast)

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

by (simp add: continuous_mono)

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

lemma continuous_tracesfun_Hiding:
 "continuous (tracesfun Pf)
  ==> continuous (tracesfun (%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_UnionT)
apply (rule order_antisym)

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

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

by (simp add: directed_def)

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

lemma continuous_tracesfun_Renaming:
 "continuous (tracesfun Pf)
  ==> continuous (tracesfun (%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_UnionT)
apply (rule order_antisym)
 apply (rule, simp add: in_tracesfun, fast)
 apply (rule, simp add: in_tracesfun, fast)
by (simp add: directed_def)

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

lemma continuous_tracesfun_Seq_compo:
 "[| continuous (tracesfun Pf) ; continuous (tracesfun Qf) |]
  ==> continuous (tracesfun (%f. (Pf f ;; Qf f)))"
apply (subgoal_tac "mono (tracesfun Pf) & mono (tracesfun Qf)")
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_tracesfun)
 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_tracesfun)
 apply (fast)

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

by (simp add: continuous_mono)

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

lemma continuous_tracesfun_Depth_rest:
 "continuous (tracesfun Pf)
  ==> continuous (tracesfun (%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_UnionT)
apply (rule order_antisym)
 apply (rule, simp add: in_tracesfun)
 apply (rule, simp add: in_tracesfun)
by (simp add: directed_def)

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

lemma continuous_tracesfun_variable: 
   "continuous (tracesfun (%f. f pn))"
apply (simp add: tracesfun_simp)
apply (simp add: continuous_prod_variable)
done

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

lemma continuous_tracesfun: 
  "Pf : Procfun ==> continuous (tracesfun Pf)"
apply (rule Procfun.induct[of Pf])
apply (simp)
apply (simp add: continuous_tracesfun_variable)
apply (simp add: continuous_tracesfun_STOP)
apply (simp add: continuous_tracesfun_SKIP)
apply (simp add: continuous_tracesfun_DIV)
apply (simp add: continuous_tracesfun_Act_prefix)
apply (simp add: continuous_tracesfun_Ext_pre_choice)
apply (simp add: continuous_tracesfun_Ext_choice)
apply (simp add: continuous_tracesfun_Int_choice)
apply (simp add: continuous_tracesfun_Rep_int_choice)
apply (simp add: continuous_tracesfun_IF)
apply (simp add: continuous_tracesfun_Parallel)
apply (simp add: continuous_tracesfun_Hiding)
apply (simp add: continuous_tracesfun_Renaming)
apply (simp add: continuous_tracesfun_Seq_compo)
apply (simp add: continuous_tracesfun_Depth_rest)
done

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

lemma continuous_semTfun: 
  "Pf : Procfun ==> continuous [[Pf]]Tfun"
by (simp add: semT_to_traces continuous_tracesfun)

(*=============================================================*
 |                         tracesFun                           |
 *=============================================================*)

lemma continuous_tracesFun: 
  "PF : ProcFun ==> continuous (tracesFun PF)"
apply (simp add: prod_continuous)
apply (simp add: proj_tracesFun_tracesfun)
apply (simp add: ProcFun_def)
apply (simp add: continuous_tracesfun)
done

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

lemma continuous_semTFun: 
  "PF : ProcFun ==> continuous [[PF]]TFun"
by (simp add: semT_to_traces continuous_tracesFun)

end

lemma continuous_Constant: 

  continuous (%f. P)

lemma continuous_tracesfun_STOP: 

  continuous (tracesfun (%f. STOP))

lemma continuous_tracesfun_SKIP: 

  continuous (tracesfun (%f. SKIP))

lemma continuous_tracesfun_DIV: 

  continuous (tracesfun (%f. DIV))

lemma continuous_tracesfun_Act_prefix: 

  continuous (tracesfun Pf) ==> continuous (tracesfun (%f. a -> Pf f))

lemma continuous_tracesfun_Ext_pre_choice: 

  ∀a. continuous (tracesfun (Pff a))
  ==> continuous (tracesfun (%f. ? a:X -> Pff a f))

lemma continuous_tracesfun_Ext_choice: 

  [| continuous (tracesfun Pf); continuous (tracesfun Qf) |]
  ==> continuous (tracesfun (%f. Pf f [+] Qf f))

lemma continuous_tracesfun_Int_choice: 

  [| continuous (tracesfun Pf); continuous (tracesfun Qf) |]
  ==> continuous (tracesfun (%f. Pf f |~| Qf f))

lemma continuous_tracesfun_Rep_int_choice: 

  ∀c. continuous (tracesfun (Pff c))
  ==> continuous (tracesfun (%f. !! c:C .. Pff c f))

lemma continuous_tracesfun_IF: 

  [| continuous (tracesfun Pf); continuous (tracesfun Qf) |]
  ==> continuous (tracesfun (%f. IF b THEN Pf f ELSE Qf f))

lemma continuous_tracesfun_Parallel: 

  [| continuous (tracesfun Pf); continuous (tracesfun Qf) |]
  ==> continuous (tracesfun (%f. Pf f |[X]| Qf f))

lemma continuous_tracesfun_Hiding: 

  continuous (tracesfun Pf) ==> continuous (tracesfun (%f. Pf f -- X))

lemma continuous_tracesfun_Renaming: 

  continuous (tracesfun Pf) ==> continuous (tracesfun (%f. Pf f [[r]]))

lemma continuous_tracesfun_Seq_compo: 

  [| continuous (tracesfun Pf); continuous (tracesfun Qf) |]
  ==> continuous (tracesfun (%f. Pf f ;; Qf f))

lemma continuous_tracesfun_Depth_rest: 

  continuous (tracesfun Pf) ==> continuous (tracesfun (%f. Pf f |. n))

lemma continuous_tracesfun_variable: 

  continuous (tracesfun (%f. f pn))

lemma continuous_tracesfun: 

  Pf ∈ Procfun ==> continuous (tracesfun Pf)

lemma continuous_semTfun: 

  Pf ∈ Procfun ==> continuous [[Pf]]Tfun

lemma continuous_tracesFun: 

  PF ∈ ProcFun ==> continuous (tracesFun PF)

lemma continuous_semTFun: 

  PF ∈ ProcFun ==> continuous [[PF]]TFun