Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T
theory CSP_T_tracesfun (*-------------------------------------------*
| CSP-Prover on Isabelle2004 |
| December 2004 |
| July 2005 (modified) |
| August 2005 (modified) |
| |
| CSP-Prover on Isabelle2005 |
| October 2005 (modified) |
| April 2006 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_T_tracesfun = CSP_T_surj:
(*****************************************************************
1. semantics for process functions
2.
3.
4.
*****************************************************************)
(*********************************************************
semantics
*********************************************************)
consts
tracesfun :: "('p,'a) procfun => (('p => 'a domT) => 'a domT)"
tracesFun :: "('p,'a) procFun => (('p => 'a domT) => ('p => 'a domT))"
semTfun :: "('p,'a) procfun => (('p => 'a domT) => 'a domT)" ("[[_]]Tfun")
semTFun :: "('p,'a) procFun =>
(('p => 'a domT) => ('p => 'a domT))" ("[[_]]TFun")
defs
tracesfun_def : "tracesfun Pf == (%f. traces (Pf (%p. Proc_T (f p))))"
tracesFun_def : "tracesFun PF == (%f. (%p. tracesfun (%f. (PF f) p) f))"
semTfun_def : "[[Pf]]Tfun == (%f. [[Pf (%p. Proc_T (f p))]]T)"
semTFun_def : "[[PF]]TFun == (%f. (%p. [[(%f. (PF f) p)]]Tfun f))"
(*********************************************************
semantics for each operators
*********************************************************)
lemma tracesfun_p:
"tracesfun (%f. f p) = (%Tf. (Tf p))"
apply (simp add: tracesfun_def)
apply (simp add: traces_Proc_T)
done
lemma tracesfun_STOP:
"tracesfun (%f. STOP) = (%Tf. {<>}t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_SKIP:
"tracesfun (%f. SKIP) = (%Tf. {<>, <Tick>}t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_DIV:
"tracesfun (%f. DIV) = (%Tf. {<>}t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Act_prefix:
"tracesfun (%f. a -> (Pf f)) =
(%Tf. {t. t = <> | (EX s. t = <Ev a> ^^ s & s :t tracesfun Pf Tf) }t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Ext_pre_choice:
"tracesfun (%f. ? a:X -> (Pff a f)) =
(%Tf. {t. t = <> |
(EX a s. t = <Ev a> ^^ s & s :t tracesfun (Pff a) Tf & a : X) }t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Ext_choice:
"tracesfun (%f. (Pf f) [+] (Qf f))
= (%Tf. tracesfun Pf Tf UnT tracesfun Qf Tf)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Int_choice:
"tracesfun (%f. (Pf f) |~| (Qf f))
= (%Tf. tracesfun Pf Tf UnT tracesfun Qf Tf)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Rep_int_choice_var:
"tracesfun (%f. !! c:C .. (Pff c f)) =
(%Tf. {t. t = <> | (EX c:C. t :t tracesfun (Pff c) Tf) }t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Rep_int_choice_fun:
"inj g ==> tracesfun (%f. !!<g> a:X .. (Pff a f)) =
(%Tf. {t. t = <> | (EX a:X. t :t tracesfun (Pff a) Tf) }t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Rep_int_choice_com:
"tracesfun (%f. ! a:X .. (Pff a f)) =
(%Tf. {t. t = <> | (EX a:X. t :t tracesfun (Pff a) Tf) }t)"
by (simp add: tracesfun_def traces_def)
lemmas tracesfun_Rep_int_choice = tracesfun_Rep_int_choice_var
tracesfun_Rep_int_choice_fun
tracesfun_Rep_int_choice_com
lemma tracesfun_IF:
"tracesfun (%f. IF b THEN (Pf f) ELSE (Qf f))
= (%Tf. if b then tracesfun Pf Tf else tracesfun Qf Tf)"
apply (case_tac "b")
by (simp_all add: tracesfun_def traces_def)
lemma tracesfun_Parallel:
"tracesfun (%f. (Pf f) |[X]| (Qf f))
= (%Tf. {u. EX s t. u : s |[X]|tr t &
s :t tracesfun Pf Tf & t :t tracesfun Qf Tf }t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Hiding:
"tracesfun (%f. (Pf f) -- X)
= (%Tf. {t. EX s. t = s --tr X & s :t tracesfun Pf Tf}t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Renaming:
"tracesfun (%f. (Pf f) [[r]])
= (%Tf. {t. EX s. s [[r]]* t & s :t tracesfun Pf Tf}t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Seq_compo:
"tracesfun (%f. (Pf f) ;; (Qf f))
= (%Tf. {u. (EX s. u = rmTick s & s :t tracesfun Pf Tf ) |
(EX s t. u = s ^^ t & s ^^ <Tick> :t tracesfun Pf Tf &
t :t tracesfun Qf Tf & noTick s) }t)"
by (simp add: tracesfun_def traces_def)
lemma tracesfun_Depth_rest:
"tracesfun (%f. (Pf f) |. n)
= (%Tf. {t. t :t tracesfun Pf Tf & (lengtht t) <= n}t)"
apply (simp add: tracesfun_def traces_def)
apply (simp add: rest_domT_iff)
done
lemmas tracesfun_simp =
tracesfun_p tracesfun_STOP tracesfun_SKIP tracesfun_DIV
tracesfun_Act_prefix tracesfun_Ext_pre_choice
tracesfun_Ext_choice tracesfun_Int_choice
tracesfun_Rep_int_choice tracesfun_IF
tracesfun_Parallel tracesfun_Hiding
tracesfun_Renaming tracesfun_Seq_compo
tracesfun_Depth_rest
lemma tracesfun_Int_choice_Ext_choice:
"tracesfun (%f. (Pf f) |~| (Qf f)) = tracesfun (%Tf. (Pf Tf) [+] (Qf Tf))"
by (simp add: tracesfun_simp)
(*********************************************************
in tracesfun
*********************************************************)
lemma in_tracesfun_p:
"(t :t tracesfun (%f. f p) Tf) = (t :t (Tf p))"
apply (simp add: tracesfun_def)
apply (simp add: traces_Proc_T)
done
lemma in_tracesfun_STOP:
"(t :t tracesfun (%f. STOP) Tf) = (t = <>)"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_SKIP:
"(t :t tracesfun (%f. SKIP) Tf) = (t = <> | t = <Tick>)"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_DIV:
"(t :t tracesfun (%f. DIV) Tf) = (t = <>)"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Act_prefix:
"(t :t tracesfun (%f. a -> (Pf f)) Tf) =
(t = <> | (EX s. t = <Ev a> ^^ s & s :t tracesfun Pf Tf))"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Ext_pre_choice:
"(t :t tracesfun (%f. ? a:X -> (Pff a f)) Tf) =
(t = <> |
(EX a s. t = <Ev a> ^^ s & s :t tracesfun (Pff a) Tf & a : X))"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Ext_choice:
"(t :t tracesfun (%f. (Pf f) [+] (Qf f)) Tf) =
(t :t tracesfun Pf Tf | t:t tracesfun Qf Tf)"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Int_choice:
"(t :t tracesfun (%f. (Pf f) |~| (Qf f)) Tf) =
(t :t tracesfun Pf Tf | t:t tracesfun Qf Tf)"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Rep_int_choice_var:
"(t :t tracesfun (%f. !! c:C .. (Pff c f)) Tf) =
(t = <> | (EX c:C. t :t tracesfun (Pff c) Tf))"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Rep_int_choice_fun:
"inj g ==> (t :t tracesfun (%f. !!<g> a:X .. (Pff a f)) Tf) =
(t = <> | (EX a:X. t :t tracesfun (Pff a) Tf))"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Rep_int_choice_com:
"(t :t tracesfun (%f. ! a:X .. (Pff a f)) Tf) =
(t = <> | (EX a:X. t :t tracesfun (Pff a) Tf))"
by (simp add: tracesfun_def in_traces)
lemmas in_tracesfun_Rep_int_choice = in_tracesfun_Rep_int_choice_var
in_tracesfun_Rep_int_choice_fun
in_tracesfun_Rep_int_choice_com
lemma in_tracesfun_IF:
"(t :t tracesfun (%f. IF b THEN (Pf f) ELSE (Qf f)) Tf) =
(if b then t :t tracesfun Pf Tf else t :t tracesfun Qf Tf)"
apply (case_tac "b")
by (simp_all add: tracesfun_def traces_def)
lemma in_tracesfun_Parallel:
"(u :t tracesfun (%f. (Pf f) |[X]| (Qf f)) Tf) =
(EX s t. u : s |[X]|tr t & s :t tracesfun Pf Tf & t :t tracesfun Qf Tf)"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Hiding:
"(t :t tracesfun (%f. (Pf f) -- X) Tf) =
(EX s. t = s --tr X & s :t tracesfun Pf Tf)"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Renaming:
"(t :t tracesfun (%f. (Pf f) [[r]]) Tf) =
(EX s. s [[r]]* t & s :t tracesfun Pf Tf)"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Seq_compo:
"(u :t tracesfun (%f. (Pf f) ;; (Qf f)) Tf) =
((EX s. u = rmTick s & s :t tracesfun Pf Tf ) |
(EX s t. u = s ^^ t & s ^^ <Tick> :t tracesfun Pf Tf &
t :t tracesfun Qf Tf & noTick s))"
by (simp add: tracesfun_def in_traces)
lemma in_tracesfun_Depth_rest:
"(t :t tracesfun (%f. (Pf f) |. n) Tf) =
(t :t tracesfun Pf Tf & (lengtht t) <= n)"
by (simp add: tracesfun_def in_traces)
lemmas in_tracesfun =
in_tracesfun_p in_tracesfun_STOP in_tracesfun_SKIP in_tracesfun_DIV
in_tracesfun_Act_prefix in_tracesfun_Ext_pre_choice
in_tracesfun_Ext_choice in_tracesfun_Int_choice
in_tracesfun_Rep_int_choice in_tracesfun_IF
in_tracesfun_Parallel in_tracesfun_Hiding
in_tracesfun_Renaming in_tracesfun_Seq_compo
in_tracesfun_Depth_rest
(**************************************************
tracesfun, tracesFun, [[P]]Tfun, [[P]]TFun
**************************************************)
lemma semTfun_tracesfun: "Pf : Procfun ==> [[Pf]]Tfun = tracesfun Pf"
apply (simp add: tracesfun_def semTfun_def)
apply (rule Procfun.induct[of Pf])
apply (simp_all add: traces_def semT_def)
done
lemma semTFun_tracesFun: "PF : ProcFun ==> [[PF]]TFun = tracesFun PF"
apply (simp add: tracesFun_def semTFun_def)
apply (simp add: ProcFun_def)
apply (simp add: semTfun_tracesfun)
done
lemmas semT_to_traces = semT_def semTfun_tracesfun semTFun_tracesFun
lemma proj_semTFun_semTfun:
"(proj_fun p o [[PF]]TFun) = [[(%f. PF f p)]]Tfun"
apply (simp add: semTFun_def)
apply (simp add: proj_fun_def)
apply (simp add: expand_fun_eq)
done
lemma proj_tracesFun_tracesfun:
"(proj_fun p o tracesFun PF) = tracesfun (%f. PF f p)"
apply (simp add: tracesFun_def)
apply (simp add: proj_fun_def)
apply (simp add: expand_fun_eq)
done
(**************************************************
traces tracesfun tracesFun
**************************************************)
lemma tracesfun_f:
"Pf : Procfun ==> traces (Pf f) = tracesfun (Pf) (%p. traces(f p))"
apply (simp add: tracesfun_def)
apply (rule Procfun.induct[of Pf])
apply (simp_all add: traces_def)
apply (simp add: traces_Proc_T)
done
lemma tracesFun_f_p:
"PF : ProcFun ==> traces(PF f p) = tracesFun(PF) (%p. traces(f p)) p"
apply (simp add: tracesFun_def)
apply (simp add: ProcFun_def)
apply (simp add: tracesfun_f[THEN sym])
done
lemma tracesfun_compo_tracesFun_Tf:
"[| Pf : Procfun ; QF : ProcFun |] ==>
tracesfun(Pf o QF) Tf = tracesfun(Pf) (tracesFun(QF) Tf)"
apply (simp add: tracesfun_def)
apply (simp add: tracesfun_f)
apply (simp add: tracesFun_f_p)
apply (simp add: traces_Proc_T)
done
lemma tracesfun_compo_tracesFun_fun:
"[| Pf : Procfun ; QF : ProcFun |] ==>
tracesfun(Pf o QF) = tracesfun(Pf) o tracesFun(QF)"
apply (simp add: expand_fun_eq)
apply (simp add: tracesfun_compo_tracesFun_Tf)
done
lemmas tracesfun_compo_tracesFun = tracesfun_compo_tracesFun_Tf
tracesfun_compo_tracesFun_fun
tracesfun_compo_tracesFun_Tf[simplified comp_def]
tracesfun_compo_tracesFun_fun[simplified comp_def]
lemma tracesFun_compo_tracesFun_Tf:
"[| PF : ProcFun ; QF : ProcFun |] ==>
tracesFun(PF o QF) Tf = tracesFun(PF) (tracesFun(QF) Tf)"
apply (simp add: tracesFun_def)
apply (simp add: tracesfun_def)
apply (simp add: tracesFun_f_p)
apply (simp add: traces_Proc_T)
done
(*** composition of process functions ***)
lemma tracesFun_compo_tracesFun_fun:
"[| PF : ProcFun ; QF : ProcFun |] ==>
tracesFun(PF o QF) = tracesFun(PF) o tracesFun(QF)"
apply (simp add: expand_fun_eq)
apply (simp add: tracesFun_compo_tracesFun_Tf)
done
lemmas tracesFun_compo_tracesFun = tracesFun_compo_tracesFun_Tf
tracesFun_compo_tracesFun_fun
tracesFun_compo_tracesFun_Tf[simplified comp_def]
tracesFun_compo_tracesFun_fun[simplified comp_def]
lemma tracesFun_compo_n_Tf:
"PF : ProcFun ==> tracesFun(PF ^ n) Tf = (tracesFun(PF) ^ n) Tf"
apply (induct_tac n)
apply (simp add: tracesFun_def)
apply (simp add: tracesfun_def)
apply (simp add: traces_Proc_T)
apply (simp add: iteration_in_ProcFun tracesFun_compo_tracesFun)
done
(**************************************************
[[P]]T, [[P]]Tfun, [[P]]TFun
**************************************************)
lemma semTfun_f:
"Pf : Procfun ==> [[Pf f]]T = [[Pf]]Tfun (%p. [[f p]]T)"
by (simp add: semT_to_traces tracesfun_f)
lemma semTFun_f_p:
"PF : ProcFun ==> [[PF f p]]T = [[PF]]TFun (%p. [[f p]]T) p"
by (simp add: semT_to_traces tracesFun_f_p)
lemma semTfun_compo_semTFun_Tf:
"[| Pf : Procfun ; QF : ProcFun |] ==>
[[Pf o QF]]Tfun Tf = [[Pf]]Tfun ([[QF]]TFun Tf)"
by (simp add: semT_to_traces tracesfun_compo_tracesFun compo_in_Procfun)
lemma semTfun_compo_semTFun_fun:
"[| Pf : Procfun ; QF : ProcFun |] ==>
[[Pf o QF]]Tfun = [[Pf]]Tfun o [[QF]]TFun"
apply (simp add: expand_fun_eq)
apply (simp add: semTfun_compo_semTFun_Tf)
done
lemmas semTfun_compo_ProcFun = semTfun_compo_semTFun_Tf semTfun_compo_semTFun_fun
semTfun_compo_semTFun_Tf[simplified comp_def]
semTfun_compo_semTFun_fun[simplified comp_def]
lemma semTFun_compo_semTFun_Tf:
"[| PF : ProcFun ; QF : ProcFun |] ==>
[[PF o QF]]TFun Tf = [[PF]]TFun ([[QF]]TFun Tf)"
by (simp add: semT_to_traces tracesFun_compo_tracesFun compo_in_ProcFun)
(*** composition of process functions ***)
lemma semTFun_compo_semTFun_fun:
"[| PF : ProcFun ; QF : ProcFun |] ==>
[[PF o QF]]TFun = [[PF]]TFun o [[QF]]TFun"
apply (simp add: expand_fun_eq)
apply (simp add: semTFun_compo_semTFun_Tf)
done
lemmas semTFun_compo_ProcFun = semTFun_compo_semTFun_Tf semTFun_compo_semTFun_fun
semTFun_compo_semTFun_Tf[simplified comp_def]
semTFun_compo_semTFun_fun[simplified comp_def]
lemma semTFun_compo_n_Tf:
"PF : ProcFun ==> [[PF ^ n]]TFun Tf = ([[PF]]TFun ^ n) Tf"
by (simp add: semT_to_traces tracesFun_compo_n_Tf iteration_in_ProcFun)
(************************************************ cong *)
(**************************************************
ProcFun_congruence
**************************************************)
lemma cspT_ProcFun_cong:
"[| PF : ProcFun ; f =T' g |] ==> PF f =T' PF g"
apply (simp add: eqT_prod_def)
apply (rule allI)
apply (simp add: cspT_semantics)
apply (simp add: tracesFun_f_p)
done
lemma cspT_Procfun_cong:
"[| Pf : Procfun ; f =T' g |] ==> Pf f =T Pf g"
apply (insert cspT_ProcFun_cong[of "(%f p. Pf f)" f g])
apply (simp add: ProcFun_def)
apply (simp add: eqT_prod_def)
done
lemma cspT_ProcX_cong:
"[| PX : ProcX ; X1 =T X2 |] ==> PX X1 =T PX X2"
apply (insert cspT_Procfun_cong[of "(%f. PX (f MUp))" "(%p. X1)" "(%p. X2)"])
apply (simp add: ProcX_def)
apply (simp add: eqT_prod_def)
done
end
lemma tracesfun_p:
tracesfun (%f. f p) = (%Tf. Tf p)
lemma tracesfun_STOP:
tracesfun (%f. STOP) = (%Tf. {<>}t)
lemma tracesfun_SKIP:
tracesfun (%f. SKIP) = (%Tf. {<>, <Tick>}t)
lemma tracesfun_DIV:
tracesfun (%f. DIV) = (%Tf. {<>}t)
lemma tracesfun_Act_prefix:
tracesfun (%f. a -> Pf f) = (%Tf. {t. t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t tracesfun Pf Tf)}t)
lemma tracesfun_Ext_pre_choice:
tracesfun (%f. ? a:X -> Pff a f) = (%Tf. {t. t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t tracesfun (Pff a) Tf ∧ a ∈ X)}t)
lemma tracesfun_Ext_choice:
tracesfun (%f. Pf f [+] Qf f) = (%Tf. tracesfun Pf Tf UnT tracesfun Qf Tf)
lemma tracesfun_Int_choice:
tracesfun (%f. Pf f |~| Qf f) = (%Tf. tracesfun Pf Tf UnT tracesfun Qf Tf)
lemma tracesfun_Rep_int_choice_var:
tracesfun (%f. !! c:C .. Pff c f) = (%Tf. {t. t = <> ∨ (∃c∈C. t :t tracesfun (Pff c) Tf)}t)
lemma tracesfun_Rep_int_choice_fun:
inj g ==> tracesfun (%f. !!<g> a:X .. Pff a f) = (%Tf. {t. t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf)}t)
lemma tracesfun_Rep_int_choice_com:
tracesfun (%f. ! a:X .. Pff a f) = (%Tf. {t. t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf)}t)
lemmas tracesfun_Rep_int_choice:
tracesfun (%f. !! c:C .. Pff c f) = (%Tf. {t. t = <> ∨ (∃c∈C. t :t tracesfun (Pff c) Tf)}t)
inj g ==> tracesfun (%f. !!<g> a:X .. Pff a f) = (%Tf. {t. t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf)}t)
tracesfun (%f. ! a:X .. Pff a f) = (%Tf. {t. t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf)}t)
lemmas tracesfun_Rep_int_choice:
tracesfun (%f. !! c:C .. Pff c f) = (%Tf. {t. t = <> ∨ (∃c∈C. t :t tracesfun (Pff c) Tf)}t)
inj g ==> tracesfun (%f. !!<g> a:X .. Pff a f) = (%Tf. {t. t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf)}t)
tracesfun (%f. ! a:X .. Pff a f) = (%Tf. {t. t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf)}t)
lemma tracesfun_IF:
tracesfun (%f. IF b THEN Pf f ELSE Qf f) = (%Tf. if b then tracesfun Pf Tf else tracesfun Qf Tf)
lemma tracesfun_Parallel:
tracesfun (%f. Pf f |[X]| Qf f) = (%Tf. {u. ∃s t. u ∈ s |[X]|tr t ∧ s :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf}t)
lemma tracesfun_Hiding:
tracesfun (%f. Pf f -- X) = (%Tf. Abs_domT {s --tr X |s. s :t tracesfun Pf Tf})
lemma tracesfun_Renaming:
tracesfun (%f. Pf f [[r]]) = (%Tf. {t. ∃s. s [[r]]* t ∧ s :t tracesfun Pf Tf}t)
lemma tracesfun_Seq_compo:
tracesfun (%f. Pf f ;; Qf f) = (%Tf. {u. (∃s. u = rmTick s ∧ s :t tracesfun Pf Tf) ∨ (∃s t. u = s ^^ t ∧ s ^^ <Tick> :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf ∧ noTick s)}t)
lemma tracesfun_Depth_rest:
tracesfun (%f. Pf f |. n) = (%Tf. {t. t :t tracesfun Pf Tf ∧ lengtht t ≤ n}t)
lemmas tracesfun_simp:
tracesfun (%f. f p) = (%Tf. Tf p)
tracesfun (%f. STOP) = (%Tf. {<>}t)
tracesfun (%f. SKIP) = (%Tf. {<>, <Tick>}t)
tracesfun (%f. DIV) = (%Tf. {<>}t)
tracesfun (%f. a -> Pf f) = (%Tf. {t. t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t tracesfun Pf Tf)}t)
tracesfun (%f. ? a:X -> Pff a f) = (%Tf. {t. t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t tracesfun (Pff a) Tf ∧ a ∈ X)}t)
tracesfun (%f. Pf f [+] Qf f) = (%Tf. tracesfun Pf Tf UnT tracesfun Qf Tf)
tracesfun (%f. Pf f |~| Qf f) = (%Tf. tracesfun Pf Tf UnT tracesfun Qf Tf)
tracesfun (%f. !! c:C .. Pff c f) = (%Tf. {t. t = <> ∨ (∃c∈C. t :t tracesfun (Pff c) Tf)}t)
inj g ==> tracesfun (%f. !!<g> a:X .. Pff a f) = (%Tf. {t. t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf)}t)
tracesfun (%f. ! a:X .. Pff a f) = (%Tf. {t. t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf)}t)
tracesfun (%f. IF b THEN Pf f ELSE Qf f) = (%Tf. if b then tracesfun Pf Tf else tracesfun Qf Tf)
tracesfun (%f. Pf f |[X]| Qf f) = (%Tf. {u. ∃s t. u ∈ s |[X]|tr t ∧ s :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf}t)
tracesfun (%f. Pf f -- X) = (%Tf. Abs_domT {s --tr X |s. s :t tracesfun Pf Tf})
tracesfun (%f. Pf f [[r]]) = (%Tf. {t. ∃s. s [[r]]* t ∧ s :t tracesfun Pf Tf}t)
tracesfun (%f. Pf f ;; Qf f) = (%Tf. {u. (∃s. u = rmTick s ∧ s :t tracesfun Pf Tf) ∨ (∃s t. u = s ^^ t ∧ s ^^ <Tick> :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf ∧ noTick s)}t)
tracesfun (%f. Pf f |. n) = (%Tf. {t. t :t tracesfun Pf Tf ∧ lengtht t ≤ n}t)
lemmas tracesfun_simp:
tracesfun (%f. f p) = (%Tf. Tf p)
tracesfun (%f. STOP) = (%Tf. {<>}t)
tracesfun (%f. SKIP) = (%Tf. {<>, <Tick>}t)
tracesfun (%f. DIV) = (%Tf. {<>}t)
tracesfun (%f. a -> Pf f) = (%Tf. {t. t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t tracesfun Pf Tf)}t)
tracesfun (%f. ? a:X -> Pff a f) = (%Tf. {t. t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t tracesfun (Pff a) Tf ∧ a ∈ X)}t)
tracesfun (%f. Pf f [+] Qf f) = (%Tf. tracesfun Pf Tf UnT tracesfun Qf Tf)
tracesfun (%f. Pf f |~| Qf f) = (%Tf. tracesfun Pf Tf UnT tracesfun Qf Tf)
tracesfun (%f. !! c:C .. Pff c f) = (%Tf. {t. t = <> ∨ (∃c∈C. t :t tracesfun (Pff c) Tf)}t)
inj g ==> tracesfun (%f. !!<g> a:X .. Pff a f) = (%Tf. {t. t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf)}t)
tracesfun (%f. ! a:X .. Pff a f) = (%Tf. {t. t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf)}t)
tracesfun (%f. IF b THEN Pf f ELSE Qf f) = (%Tf. if b then tracesfun Pf Tf else tracesfun Qf Tf)
tracesfun (%f. Pf f |[X]| Qf f) = (%Tf. {u. ∃s t. u ∈ s |[X]|tr t ∧ s :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf}t)
tracesfun (%f. Pf f -- X) = (%Tf. Abs_domT {s --tr X |s. s :t tracesfun Pf Tf})
tracesfun (%f. Pf f [[r]]) = (%Tf. {t. ∃s. s [[r]]* t ∧ s :t tracesfun Pf Tf}t)
tracesfun (%f. Pf f ;; Qf f) = (%Tf. {u. (∃s. u = rmTick s ∧ s :t tracesfun Pf Tf) ∨ (∃s t. u = s ^^ t ∧ s ^^ <Tick> :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf ∧ noTick s)}t)
tracesfun (%f. Pf f |. n) = (%Tf. {t. t :t tracesfun Pf Tf ∧ lengtht t ≤ n}t)
lemma tracesfun_Int_choice_Ext_choice:
tracesfun (%f. Pf f |~| Qf f) = tracesfun (%Tf. Pf Tf [+] Qf Tf)
lemma in_tracesfun_p:
(t :t tracesfun (%f. f p) Tf) = (t :t Tf p)
lemma in_tracesfun_STOP:
(t :t tracesfun (%f. STOP) Tf) = (t = <>)
lemma in_tracesfun_SKIP:
(t :t tracesfun (%f. SKIP) Tf) = (t = <> ∨ t = <Tick>)
lemma in_tracesfun_DIV:
(t :t tracesfun (%f. DIV) Tf) = (t = <>)
lemma in_tracesfun_Act_prefix:
(t :t tracesfun (%f. a -> Pf f) Tf) = (t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t tracesfun Pf Tf))
lemma in_tracesfun_Ext_pre_choice:
(t :t tracesfun (%f. ? a:X -> Pff a f) Tf) = (t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t tracesfun (Pff a) Tf ∧ a ∈ X))
lemma in_tracesfun_Ext_choice:
(t :t tracesfun (%f. Pf f [+] Qf f) Tf) = (t :t tracesfun Pf Tf ∨ t :t tracesfun Qf Tf)
lemma in_tracesfun_Int_choice:
(t :t tracesfun (%f. Pf f |~| Qf f) Tf) = (t :t tracesfun Pf Tf ∨ t :t tracesfun Qf Tf)
lemma in_tracesfun_Rep_int_choice_var:
(t :t tracesfun (%f. !! c:C .. Pff c f) Tf) = (t = <> ∨ (∃c∈C. t :t tracesfun (Pff c) Tf))
lemma in_tracesfun_Rep_int_choice_fun:
inj g ==> (t :t tracesfun (%f. !!<g> a:X .. Pff a f) Tf) = (t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf))
lemma in_tracesfun_Rep_int_choice_com:
(t :t tracesfun (%f. ! a:X .. Pff a f) Tf) = (t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf))
lemmas in_tracesfun_Rep_int_choice:
(t :t tracesfun (%f. !! c:C .. Pff c f) Tf) = (t = <> ∨ (∃c∈C. t :t tracesfun (Pff c) Tf))
inj g ==> (t :t tracesfun (%f. !!<g> a:X .. Pff a f) Tf) = (t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf))
(t :t tracesfun (%f. ! a:X .. Pff a f) Tf) = (t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf))
lemmas in_tracesfun_Rep_int_choice:
(t :t tracesfun (%f. !! c:C .. Pff c f) Tf) = (t = <> ∨ (∃c∈C. t :t tracesfun (Pff c) Tf))
inj g ==> (t :t tracesfun (%f. !!<g> a:X .. Pff a f) Tf) = (t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf))
(t :t tracesfun (%f. ! a:X .. Pff a f) Tf) = (t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf))
lemma in_tracesfun_IF:
(t :t tracesfun (%f. IF b THEN Pf f ELSE Qf f) Tf) = (if b then t :t tracesfun Pf Tf else t :t tracesfun Qf Tf)
lemma in_tracesfun_Parallel:
(u :t tracesfun (%f. Pf f |[X]| Qf f) Tf) = (∃s t. u ∈ s |[X]|tr t ∧ s :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf)
lemma in_tracesfun_Hiding:
(t :t tracesfun (%f. Pf f -- X) Tf) = (∃s. t = s --tr X ∧ s :t tracesfun Pf Tf)
lemma in_tracesfun_Renaming:
(t :t tracesfun (%f. Pf f [[r]]) Tf) = (∃s. s [[r]]* t ∧ s :t tracesfun Pf Tf)
lemma in_tracesfun_Seq_compo:
(u :t tracesfun (%f. Pf f ;; Qf f) Tf) = ((∃s. u = rmTick s ∧ s :t tracesfun Pf Tf) ∨ (∃s t. u = s ^^ t ∧ s ^^ <Tick> :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf ∧ noTick s))
lemma in_tracesfun_Depth_rest:
(t :t tracesfun (%f. Pf f |. n) Tf) = (t :t tracesfun Pf Tf ∧ lengtht t ≤ n)
lemmas in_tracesfun:
(t :t tracesfun (%f. f p) Tf) = (t :t Tf p)
(t :t tracesfun (%f. STOP) Tf) = (t = <>)
(t :t tracesfun (%f. SKIP) Tf) = (t = <> ∨ t = <Tick>)
(t :t tracesfun (%f. DIV) Tf) = (t = <>)
(t :t tracesfun (%f. a -> Pf f) Tf) = (t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t tracesfun Pf Tf))
(t :t tracesfun (%f. ? a:X -> Pff a f) Tf) = (t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t tracesfun (Pff a) Tf ∧ a ∈ X))
(t :t tracesfun (%f. Pf f [+] Qf f) Tf) = (t :t tracesfun Pf Tf ∨ t :t tracesfun Qf Tf)
(t :t tracesfun (%f. Pf f |~| Qf f) Tf) = (t :t tracesfun Pf Tf ∨ t :t tracesfun Qf Tf)
(t :t tracesfun (%f. !! c:C .. Pff c f) Tf) = (t = <> ∨ (∃c∈C. t :t tracesfun (Pff c) Tf))
inj g ==> (t :t tracesfun (%f. !!<g> a:X .. Pff a f) Tf) = (t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf))
(t :t tracesfun (%f. ! a:X .. Pff a f) Tf) = (t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf))
(t :t tracesfun (%f. IF b THEN Pf f ELSE Qf f) Tf) = (if b then t :t tracesfun Pf Tf else t :t tracesfun Qf Tf)
(u :t tracesfun (%f. Pf f |[X]| Qf f) Tf) = (∃s t. u ∈ s |[X]|tr t ∧ s :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf)
(t :t tracesfun (%f. Pf f -- X) Tf) = (∃s. t = s --tr X ∧ s :t tracesfun Pf Tf)
(t :t tracesfun (%f. Pf f [[r]]) Tf) = (∃s. s [[r]]* t ∧ s :t tracesfun Pf Tf)
(u :t tracesfun (%f. Pf f ;; Qf f) Tf) = ((∃s. u = rmTick s ∧ s :t tracesfun Pf Tf) ∨ (∃s t. u = s ^^ t ∧ s ^^ <Tick> :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf ∧ noTick s))
(t :t tracesfun (%f. Pf f |. n) Tf) = (t :t tracesfun Pf Tf ∧ lengtht t ≤ n)
lemmas in_tracesfun:
(t :t tracesfun (%f. f p) Tf) = (t :t Tf p)
(t :t tracesfun (%f. STOP) Tf) = (t = <>)
(t :t tracesfun (%f. SKIP) Tf) = (t = <> ∨ t = <Tick>)
(t :t tracesfun (%f. DIV) Tf) = (t = <>)
(t :t tracesfun (%f. a -> Pf f) Tf) = (t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t tracesfun Pf Tf))
(t :t tracesfun (%f. ? a:X -> Pff a f) Tf) = (t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t tracesfun (Pff a) Tf ∧ a ∈ X))
(t :t tracesfun (%f. Pf f [+] Qf f) Tf) = (t :t tracesfun Pf Tf ∨ t :t tracesfun Qf Tf)
(t :t tracesfun (%f. Pf f |~| Qf f) Tf) = (t :t tracesfun Pf Tf ∨ t :t tracesfun Qf Tf)
(t :t tracesfun (%f. !! c:C .. Pff c f) Tf) = (t = <> ∨ (∃c∈C. t :t tracesfun (Pff c) Tf))
inj g ==> (t :t tracesfun (%f. !!<g> a:X .. Pff a f) Tf) = (t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf))
(t :t tracesfun (%f. ! a:X .. Pff a f) Tf) = (t = <> ∨ (∃a∈X. t :t tracesfun (Pff a) Tf))
(t :t tracesfun (%f. IF b THEN Pf f ELSE Qf f) Tf) = (if b then t :t tracesfun Pf Tf else t :t tracesfun Qf Tf)
(u :t tracesfun (%f. Pf f |[X]| Qf f) Tf) = (∃s t. u ∈ s |[X]|tr t ∧ s :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf)
(t :t tracesfun (%f. Pf f -- X) Tf) = (∃s. t = s --tr X ∧ s :t tracesfun Pf Tf)
(t :t tracesfun (%f. Pf f [[r]]) Tf) = (∃s. s [[r]]* t ∧ s :t tracesfun Pf Tf)
(u :t tracesfun (%f. Pf f ;; Qf f) Tf) = ((∃s. u = rmTick s ∧ s :t tracesfun Pf Tf) ∨ (∃s t. u = s ^^ t ∧ s ^^ <Tick> :t tracesfun Pf Tf ∧ t :t tracesfun Qf Tf ∧ noTick s))
(t :t tracesfun (%f. Pf f |. n) Tf) = (t :t tracesfun Pf Tf ∧ lengtht t ≤ n)
lemma semTfun_tracesfun:
Pf ∈ Procfun ==> [[Pf]]Tfun = tracesfun Pf
lemma semTFun_tracesFun:
PF ∈ ProcFun ==> [[PF]]TFun = tracesFun PF
lemmas semT_to_traces:
[[P]]T == traces P
Pf ∈ Procfun ==> [[Pf]]Tfun = tracesfun Pf
PF ∈ ProcFun ==> [[PF]]TFun = tracesFun PF
lemmas semT_to_traces:
[[P]]T == traces P
Pf ∈ Procfun ==> [[Pf]]Tfun = tracesfun Pf
PF ∈ ProcFun ==> [[PF]]TFun = tracesFun PF
lemma proj_semTFun_semTfun:
proj_fun p o [[PF]]TFun = [[%f. PF f p]]Tfun
lemma proj_tracesFun_tracesfun:
proj_fun p o tracesFun PF = tracesfun (%f. PF f p)
lemma tracesfun_f:
Pf ∈ Procfun ==> traces (Pf f) = tracesfun Pf (%p. traces (f p))
lemma tracesFun_f_p:
PF ∈ ProcFun ==> traces (PF f p) = tracesFun PF (%p. traces (f p)) p
lemma tracesfun_compo_tracesFun_Tf:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> tracesfun (Pf o QF) Tf = tracesfun Pf (tracesFun QF Tf)
lemma tracesfun_compo_tracesFun_fun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> tracesfun (Pf o QF) = tracesfun Pf o tracesFun QF
lemmas tracesfun_compo_tracesFun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> tracesfun (Pf o QF) Tf = tracesfun Pf (tracesFun QF Tf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> tracesfun (Pf o QF) = tracesfun Pf o tracesFun QF
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> tracesfun (%x. Pf (QF x)) Tf = tracesfun Pf (tracesFun QF Tf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> tracesfun (%x. Pf (QF x)) = (%x. tracesfun Pf (tracesFun QF x))
lemmas tracesfun_compo_tracesFun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> tracesfun (Pf o QF) Tf = tracesfun Pf (tracesFun QF Tf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> tracesfun (Pf o QF) = tracesfun Pf o tracesFun QF
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> tracesfun (%x. Pf (QF x)) Tf = tracesfun Pf (tracesFun QF Tf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> tracesfun (%x. Pf (QF x)) = (%x. tracesfun Pf (tracesFun QF x))
lemma tracesFun_compo_tracesFun_Tf:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> tracesFun (PF o QF) Tf = tracesFun PF (tracesFun QF Tf)
lemma tracesFun_compo_tracesFun_fun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> tracesFun (PF o QF) = tracesFun PF o tracesFun QF
lemmas tracesFun_compo_tracesFun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> tracesFun (PF o QF) Tf = tracesFun PF (tracesFun QF Tf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> tracesFun (PF o QF) = tracesFun PF o tracesFun QF
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> tracesFun (%x. PF (QF x)) Tf = tracesFun PF (tracesFun QF Tf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> tracesFun (%x. PF (QF x)) = (%x. tracesFun PF (tracesFun QF x))
lemmas tracesFun_compo_tracesFun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> tracesFun (PF o QF) Tf = tracesFun PF (tracesFun QF Tf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> tracesFun (PF o QF) = tracesFun PF o tracesFun QF
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> tracesFun (%x. PF (QF x)) Tf = tracesFun PF (tracesFun QF Tf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> tracesFun (%x. PF (QF x)) = (%x. tracesFun PF (tracesFun QF x))
lemma tracesFun_compo_n_Tf:
PF ∈ ProcFun ==> tracesFun (PF ^ n) Tf = (tracesFun PF ^ n) Tf
lemma semTfun_f:
Pf ∈ Procfun ==> [[Pf f]]T = [[Pf]]Tfun (%p. [[f p]]T)
lemma semTFun_f_p:
PF ∈ ProcFun ==> [[PF f p]]T = [[PF]]TFun (%p. [[f p]]T) p
lemma semTfun_compo_semTFun_Tf:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Tfun Tf = [[Pf]]Tfun ([[QF]]TFun Tf)
lemma semTfun_compo_semTFun_fun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Tfun = [[Pf]]Tfun o [[QF]]TFun
lemmas semTfun_compo_ProcFun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Tfun Tf = [[Pf]]Tfun ([[QF]]TFun Tf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Tfun = [[Pf]]Tfun o [[QF]]TFun
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[%x. Pf (QF x)]]Tfun Tf = [[Pf]]Tfun ([[QF]]TFun Tf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[%x. Pf (QF x)]]Tfun = (%x. [[Pf]]Tfun ([[QF]]TFun x))
lemmas semTfun_compo_ProcFun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Tfun Tf = [[Pf]]Tfun ([[QF]]TFun Tf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Tfun = [[Pf]]Tfun o [[QF]]TFun
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[%x. Pf (QF x)]]Tfun Tf = [[Pf]]Tfun ([[QF]]TFun Tf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[%x. Pf (QF x)]]Tfun = (%x. [[Pf]]Tfun ([[QF]]TFun x))
lemma semTFun_compo_semTFun_Tf:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]TFun Tf = [[PF]]TFun ([[QF]]TFun Tf)
lemma semTFun_compo_semTFun_fun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]TFun = [[PF]]TFun o [[QF]]TFun
lemmas semTFun_compo_ProcFun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]TFun Tf = [[PF]]TFun ([[QF]]TFun Tf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]TFun = [[PF]]TFun o [[QF]]TFun
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[%x. PF (QF x)]]TFun Tf = [[PF]]TFun ([[QF]]TFun Tf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[%x. PF (QF x)]]TFun = (%x. [[PF]]TFun ([[QF]]TFun x))
lemmas semTFun_compo_ProcFun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]TFun Tf = [[PF]]TFun ([[QF]]TFun Tf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]TFun = [[PF]]TFun o [[QF]]TFun
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[%x. PF (QF x)]]TFun Tf = [[PF]]TFun ([[QF]]TFun Tf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[%x. PF (QF x)]]TFun = (%x. [[PF]]TFun ([[QF]]TFun x))
lemma semTFun_compo_n_Tf:
PF ∈ ProcFun ==> [[PF ^ n]]TFun Tf = ([[PF]]TFun ^ n) Tf
lemma cspT_ProcFun_cong:
[| PF ∈ ProcFun; f =T' g |] ==> PF f =T' PF g
lemma cspT_Procfun_cong:
[| Pf ∈ Procfun; f =T' g |] ==> Pf f =T Pf g
lemma cspT_ProcX_cong:
[| PX ∈ ProcX; X1.0 =T X2.0 |] ==> PX X1.0 =T PX X2.0