Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F
theory CSP_F_failuresfun (*-------------------------------------------*
| 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_F_failuresfun = CSP_T_tracesfun + CSP_F_surj:
(*****************************************************************
1. semantics for process functions
2.
3.
4.
*****************************************************************)
(*---------------------------------*
| |
| traces , invT, invF |
| |
*---------------------------------*)
lemma traces_Pf_Proc_T_F:
"Pf : Procfun ==>
traces (Pf (%p. Proc_T(fstF (F p)))) = traces (Pf (%p. Proc_F(F p)))"
apply (simp add: tracesfun_f)
apply (simp add: traces_Proc_T_F)
done
(*********************************************************
semantics
*********************************************************)
consts
failuresfun :: "('p,'a) procfun => (('p => 'a domF) => 'a setF)"
failuresFun :: "('p,'a) procFun => (('p => 'a domF) => ('p => 'a setF))"
semFfun :: "('p,'a) procfun => (('p => 'a domF) => 'a domF)" ("[[_]]Ffun")
semFFun :: "('p,'a) procFun =>
(('p => 'a domF) => ('p => 'a domF))" ("[[_]]FFun")
defs
failuresfun_def : "failuresfun Pf == (%SFf. failures (Pf (%p. Proc_F(SFf p))))"
failuresFun_def : "failuresFun PF == (%SFf. (%p. failuresfun (%SFf. (PF SFf) p) SFf))"
semFfun_def : "[[Pf]]Ffun == (%SFf. [[Pf (%p. Proc_F(SFf p))]]F)"
semFFun_def : "[[PF]]FFun == (%SFf. (%p. [[(%SFf. (PF SFf) p)]]Ffun SFf))"
(*********************************************************
semantics for each operators
*********************************************************)
lemma failuresfun_p:
"failuresfun (%f. f p) = (%SFf. sndF (SFf p))"
apply (simp add: failuresfun_def)
apply (simp add: failures_Proc_F)
done
lemma failuresfun_STOP:
"failuresfun (%f. STOP) = (%SFf. {f. EX X. f = (<>, X) }f)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_SKIP:
"failuresfun (%f. SKIP) = (%SFf. {f. (EX X. f = (<>, X) & X <= Evset) |
(EX X. f = (<Tick>, X)) }f)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_DIV:
"failuresfun (%f. DIV) = (%SFf. {}f)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_Act_prefix:
"failuresfun (%f. a -> (Pf f)) =
(%SFf. {f. (EX X. f = (<>,X) & Ev a ~: X) |
(EX s X. f = (<Ev a> ^^ s, X) & (s,X) :f failuresfun Pf SFf ) }f)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_Ext_pre_choice:
"failuresfun (%f. ? a:X -> (Pff a f)) =
(%SFf. {f. (EX Y. f = (<>,Y) & Ev`X Int Y = {}) |
(EX a s Y. f = (<Ev a> ^^ s, Y) &
(s,Y) :f failuresfun (Pff a) SFf & a : X) }f)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_Ext_choice:
"[| Pf : Procfun ; Qf : Procfun |] ==>
failuresfun (%f. (Pf f) [+] (Qf f)) =
(%SFf. {f. ((EX X. f = (<>, X)) & f :f failuresfun Pf SFf & f :f failuresfun Qf SFf |
(EX s. (EX X. f = (s, X)) &
(f :f failuresfun Pf SFf | f :f failuresfun Qf SFf) & s ~= <>) |
(EX X. f = (<>, X) &
(<Tick> :t tracesfun Pf (fstF o SFf) | <Tick> :t tracesfun Qf (fstF o SFf)) &
X <= Evset)) }f)"
apply (simp add: failuresfun_def)
apply (simp add: failures_def)
apply (simp add: tracesfun_def)
apply (simp add: tracesfun_f)
apply (simp add: traces_Proc_T)
apply (simp add: traces_Proc_F)
done
lemma failuresfun_Int_choice:
"failuresfun (%f. (Pf f) |~| (Qf f)) = (%SFf. failuresfun Pf SFf UnF failuresfun Qf SFf)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_Rep_int_choice_var:
"failuresfun (%f. !! c:C .. (Pff c f)) =
(%SFf. {f. EX c:C. f :f failuresfun (Pff c) SFf}f)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_Rep_int_choice_fun:
"inj f ==> failuresfun (%g. !!<f> a:X .. (Pff a g)) =
(%SFf. {f. EX a:X. f :f failuresfun (Pff a) SFf}f)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_Rep_int_choice_com:
"failuresfun (%f. ! a:X .. (Pff a f)) =
(%SFf. {f. EX a:X. f :f failuresfun (Pff a) SFf}f)"
by (simp add: failuresfun_def failures_def)
lemmas failuresfun_Rep_int_choice = failuresfun_Rep_int_choice_var
failuresfun_Rep_int_choice_fun
failuresfun_Rep_int_choice_com
lemma failuresfun_IF:
"failuresfun (%f. IF b THEN (Pf f) ELSE (Qf f))
= (%SFf. if b then failuresfun Pf SFf else failuresfun Qf SFf)"
apply (case_tac "b")
by (simp_all add: failuresfun_def failures_def)
lemma failuresfun_Parallel:
"failuresfun (%f. (Pf f) |[X]| (Qf f))
= (%SFf. {f. EX u Y Z. f = (u, Y Un Z) &
Y-((Ev`X) Un {Tick})= Z-((Ev`X) Un {Tick}) &
(EX s t. u : s |[X]|tr t & (s,Y) :f failuresfun Pf SFf &
(t,Z) :f failuresfun Qf SFf) }f)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_Hiding:
"failuresfun (%f. (Pf f) -- X)
= (%SFf. {f. EX s Y. f = (s --tr X, Y) &
(s,(Ev`X) Un Y) :f failuresfun Pf SFf }f)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_Renaming:
"failuresfun (%f. (Pf f) [[r]])
= (%SFf. {f. EX s t X. f = (t,X) & s [[r]]* t &
(s, [[r]]inv X) :f failuresfun Pf SFf }f)"
by (simp add: failuresfun_def failures_def)
lemma failuresfun_Seq_compo:
"Pf : Procfun ==>
failuresfun (%f. (Pf f) ;; (Qf f))
= (%SFf. {f. (EX t X. f = (t,X) & (t, X Un {Tick}) :f failuresfun Pf SFf &
noTick t) |
(EX s t X. f = (s ^^ t,X) & s ^^ <Tick> :t tracesfun Pf (fstF o SFf) &
(t, X) :f failuresfun Qf SFf & noTick s) }f)"
apply (simp add: failuresfun_def)
apply (simp add: failures_def)
apply (simp add: tracesfun_def)
apply (simp add: tracesfun_f)
apply (simp add: traces_Proc_T)
apply (simp add: traces_Proc_F)
done
lemma failuresfun_Depth_rest:
"failuresfun (%f. (Pf f) |. n)
= (%SFf. {(t, X).
(t, X) :f failuresfun Pf SFf &
(lengtht t < n |
lengtht t = n & (EX s. t = s ^^ <Tick> & noTick s))}f)"
apply (simp add: failuresfun_def failures_def)
apply (simp add: rest_setF_iff)
done
lemmas failuresfun_simp =
failuresfun_p failuresfun_STOP failuresfun_SKIP failuresfun_DIV
failuresfun_Act_prefix failuresfun_Ext_pre_choice
failuresfun_Ext_choice failuresfun_Int_choice
failuresfun_Rep_int_choice failuresfun_IF
failuresfun_Parallel failuresfun_Hiding
failuresfun_Renaming failuresfun_Seq_compo
failuresfun_Depth_rest
(*********************************************************
in failuresfun
*********************************************************)
lemma in_failuresfun_p:
"(f :f failuresfun (%f. f p) SFf) = (f :f sndF (SFf p))"
apply (simp add: failuresfun_def)
apply (simp add: failures_Proc_F)
done
lemma in_failuresfun_STOP:
"(f :f failuresfun (%f. STOP) SFf) = (EX X. f = (<>, X))"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_SKIP:
"(f :f failuresfun (%f. SKIP) SFf) =
((EX X. f = (<>, X) & X <= Evset) |
(EX X. f = (<Tick>, X)))"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_DIV:
"(f ~:f failuresfun (%f. DIV) SFf)"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_Act_prefix:
"(f :f failuresfun (%f. a -> (Pf f)) SFf) =
((EX X. f = (<>,X) & Ev a ~: X) |
(EX s X. f = (<Ev a> ^^ s, X) & (s,X) :f failuresfun Pf SFf ))"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_Ext_pre_choice:
"(f :f failuresfun (%f. ? a:X -> (Pff a f)) SFf) =
((EX Y. f = (<>,Y) & Ev`X Int Y = {}) |
(EX a s Y. f = (<Ev a> ^^ s, Y) &
(s,Y) :f failuresfun (Pff a) SFf & a : X))"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_Ext_choice:
"[| Pf : Procfun ; Qf : Procfun |] ==>
(f :f failuresfun (%f. (Pf f) [+] (Qf f)) SFf) =
(((EX X. f = (<>, X)) & f :f failuresfun Pf SFf & f :f failuresfun Qf SFf |
(EX s. (EX X. f = (s, X)) &
(f :f failuresfun Pf SFf | f :f failuresfun Qf SFf) & s ~= <>) |
(EX X. f = (<>, X) &
(<Tick> :t tracesfun Pf (fstF o SFf) | <Tick> :t tracesfun Qf (fstF o SFf)) &
X <= Evset)))"
apply (simp add: failuresfun_def in_failures)
apply (simp add: tracesfun_def)
apply (simp add: tracesfun_f)
apply (simp add: traces_Proc_T)
apply (simp add: traces_Proc_F)
done
lemma in_failuresfun_Int_choice:
"(f :f failuresfun (%f. (Pf f) |~| (Qf f)) SFf) =
(f :f failuresfun Pf SFf | f :f failuresfun Qf SFf)"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_Rep_int_choice_var:
"(f :f failuresfun (%f. !! c:C .. (Pff c f)) SFf) =
(EX c:C. f :f failuresfun (Pff c) SFf)"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_Rep_int_choice_fun:
"inj g ==> (f :f failuresfun (%f. !!<g> a:X .. (Pff a f)) SFf) =
(EX a:X. f :f failuresfun (Pff a) SFf)"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_Rep_int_choice_com:
"(f :f failuresfun (%f. ! a:X .. (Pff a f)) SFf) =
(EX a:X. f :f failuresfun (Pff a) SFf)"
by (simp add: failuresfun_def in_failures)
lemmas in_failuresfun_Rep_int_choice = in_failuresfun_Rep_int_choice_var
in_failuresfun_Rep_int_choice_fun
in_failuresfun_Rep_int_choice_com
lemma in_failuresfun_IF:
"(f :f failuresfun (%f. IF b THEN (Pf f) ELSE (Qf f)) SFf) =
(if b then f :f failuresfun Pf SFf else f :f failuresfun Qf SFf)"
apply (case_tac "b")
by (simp_all add: failuresfun_def failures_def)
lemma in_failuresfun_Parallel:
"(f :f failuresfun (%f. (Pf f) |[X]| (Qf f)) SFf) =
(EX u Y Z. f = (u, Y Un Z) &
Y-((Ev`X) Un {Tick})= Z-((Ev`X) Un {Tick}) &
(EX s t. u : s |[X]|tr t & (s,Y) :f failuresfun Pf SFf &
(t,Z) :f failuresfun Qf SFf))"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_Hiding:
"(f :f failuresfun (%f. (Pf f) -- X) SFf) =
(EX s Y. f = (s --tr X, Y) &
(s,(Ev`X) Un Y) :f failuresfun Pf SFf)"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_Renaming:
"(f :f failuresfun (%f. (Pf f) [[r]]) SFf) =
(EX s t X. f = (t,X) & s [[r]]* t &
(s, [[r]]inv X) :f failuresfun Pf SFf)"
by (simp add: failuresfun_def in_failures)
lemma in_failuresfun_Seq_compo:
"Pf : Procfun ==>
(f :f failuresfun (%f. Pf f ;; Qf f) SFf) =
((EX t X. f = (t, X) & (t, insert Tick X) :f failuresfun Pf SFf & noTick t) |
(EX s t X. f = (s ^^ t, X) & s ^^ <Tick> :t tracesfun Pf (fstF o SFf) &
(t, X) :f failuresfun Qf SFf & noTick s))"
apply (simp add: failuresfun_def in_failures)
apply (simp add: tracesfun_def)
apply (simp add: tracesfun_f)
apply (simp add: traces_Proc_T)
apply (simp add: traces_Proc_F)
done
lemma in_failuresfun_Depth_rest:
"(f :f failuresfun (%f. (Pf f) |. n) SFf) =
(EX t X. f = (t,X) &
(t, X) :f failuresfun Pf SFf &
(lengtht t < n |
lengtht t = n & (EX s. t = s ^^ <Tick> & noTick s)))"
by (simp add: failuresfun_def in_failures)
lemmas in_failuresfun =
in_failuresfun_p in_failuresfun_STOP in_failuresfun_SKIP in_failuresfun_DIV
in_failuresfun_Act_prefix in_failuresfun_Ext_pre_choice
in_failuresfun_Ext_choice in_failuresfun_Int_choice
in_failuresfun_Rep_int_choice in_failuresfun_IF
in_failuresfun_Parallel in_failuresfun_Hiding
in_failuresfun_Renaming in_failuresfun_Seq_compo
in_failuresfun_Depth_rest
(*************************************************
failuresfun, failuresFun
*************************************************)
lemma proj_failuresFun_failuresfun:
"(proj_fun p o failuresFun PF) = failuresfun (%f. PF f p)"
apply (simp add: failuresFun_def)
apply (simp add: proj_fun_def)
apply (simp add: expand_fun_eq)
done
lemma proj_semFFun_semFfun:
"(proj_fun p o [[PF]]FFun) = [[%f. PF f p]]Ffun"
apply (simp add: semFFun_def)
apply (simp add: proj_fun_def)
apply (simp add: expand_fun_eq)
done
(**************************************************
failures failuresfun failuresFun
**************************************************)
lemma failuresfun_f:
"Pf : Procfun ==>
failures (Pf f) =
failuresfun (Pf) (%p. (traces(f p),, failures(f p)))"
apply (simp add: failuresfun_def)
apply (rule Procfun.induct[of Pf])
apply (simp_all add: failures_def failures_Proc_F)
apply (simp_all add: tracesfun_f traces_Proc_F)
done
lemma failuresFun_f_p:
"PF : ProcFun ==>
failures(PF f p) =
failuresFun(PF) (%p. (traces(f p),, failures(f p))) p"
apply (simp add: failuresFun_def)
apply (simp add: ProcFun_def)
apply (simp add: failuresfun_f[THEN sym])
done
(**************************************************
[[ ]]Ffun [[ ]]FFun traces failures
**************************************************)
lemma semFfun_traces_failures:
"Pf : Procfun
==> [[Pf]]Ffun = (%SFf. (traces (Pf (%p. Proc_F(SFf p))) ,,
failures (Pf (%p. Proc_F(SFf p)))))"
apply (simp add: semFfun_def)
apply (simp add: semF_def)
done
lemma semFfun_tracesfun_failuresfun:
"Pf : Procfun ==> [[Pf]]Ffun = (%SFf. (tracesfun Pf (fstF o SFf) ,, failuresfun Pf SFf))"
apply (simp add: failuresfun_def tracesfun_def)
apply (simp add: semFfun_traces_failures)
apply (simp add: traces_Pf_Proc_T_F)
done
lemma semFFun_traces_failures:
"PF : ProcFun
==> [[PF]]FFun = (%SFf p. (traces (PF (%p. Proc_F(SFf p)) p) ,,
failures (PF (%p. Proc_F(SFf p)) p)))"
apply (simp add: semFFun_def)
apply (simp add: ProcFun_def)
apply (simp add: semFfun_traces_failures)
done
lemma semFFun_tracesFun_failuresFun:
"PF : ProcFun ==>
[[PF]]FFun =
(%SFf p. (tracesFun PF (fstF o SFf) p,, failuresFun PF SFf p))"
apply (simp add: tracesFun_def failuresFun_def semFFun_def)
apply (simp add: ProcFun_def)
apply (simp add: semFfun_tracesfun_failuresfun)
done
lemmas semF_decompo = semF_def
semFfun_traces_failures
semFFun_traces_failures
lemmas semF_decompo_fun = semF_def
semFfun_tracesfun_failuresfun
semFFun_tracesFun_failuresFun
(*** semFfun_variable ***)
lemma semFfun_variable: "[[%F. F p]]Ffun = (%SFf. SFf p)"
apply (simp add: semF_decompo_fun)
apply (simp add: tracesfun_simp)
apply (simp add: failuresfun_simp)
done
(**************************************************
failuresfun composition
**************************************************)
lemma failuresfun_compo_failuresFun_SFf:
"[| Pf : Procfun ; QF : ProcFun |] ==>
failuresfun(Pf o QF) SFf =
failuresfun(Pf) (%p. (tracesFun(QF) (fstF o SFf) p ,, failuresFun(QF) SFf p))"
apply (simp add: failuresfun_def)
apply (simp add: failuresfun_f)
apply (simp add: tracesFun_f_p failuresFun_f_p)
apply (simp add: failures_Proc_F traces_Proc_F)
apply (simp add: comp_def)
done
lemma failuresfun_compo_failuresFun_fun:
"[| Pf : Procfun ; QF : ProcFun |] ==>
failuresfun(Pf o QF) =
failuresfun(Pf) o (%SFf p. (tracesFun(QF) (fstF o SFf) p ,, failuresFun(QF) SFf p))"
apply (simp add: expand_fun_eq)
apply (simp add: failuresfun_compo_failuresFun_SFf)
done
lemmas failuresfun_compo_failuresFun = failuresfun_compo_failuresFun_SFf
failuresfun_compo_failuresFun_fun
failuresfun_compo_failuresFun_SFf[simplified comp_def]
failuresfun_compo_failuresFun_fun[simplified comp_def]
(*** ProcFun ***)
lemma failuresFun_compo_failuresFun_SFf_lm:
"[| PF : ProcFun ; QF : ProcFun |] ==>
failuresfun (%f. PF (QF f) p) SFf =
failuresfun (%SFf. PF SFf p)
(%p. (tracesFun(QF) (fstF o SFf) p ,, failuresFun(QF) SFf p))"
apply (insert failuresfun_compo_failuresFun_SFf[of "(%SFf. PF SFf p)" QF SFf])
apply (simp add: ProcFun_def comp_def)
done
lemma failuresFun_compo_failuresFun_SFf:
"[| PF : ProcFun ; QF : ProcFun |] ==>
failuresFun(PF o QF) SFf =
failuresFun(PF) (%p. (tracesFun(QF) (fstF o SFf) p ,, failuresFun(QF) SFf p))"
apply (simp add: failuresFun_def[of PF])
apply (simp add: failuresFun_def[of "(PF o QF)"])
apply (simp add: expand_fun_eq)
apply (simp add: failuresFun_compo_failuresFun_SFf_lm)
done
(*** composition of process functions ***)
lemma failuresFun_compo_failuresFun_fun:
"[| PF : ProcFun ; QF : ProcFun |] ==>
failuresFun(PF o QF) =
failuresFun(PF) o (%SFf p. (tracesFun(QF) (fstF o SFf) p ,, failuresFun(QF) SFf p))"
apply (simp add: expand_fun_eq)
apply (simp add: failuresFun_compo_failuresFun_SFf)
done
lemmas failuresFun_compo_failuresFun = failuresFun_compo_failuresFun_SFf
failuresFun_compo_failuresFun_fun
failuresFun_compo_failuresFun_SFf[simplified comp_def]
failuresFun_compo_failuresFun_fun[simplified comp_def]
(**************************************************
[[P]]F, [[P]]Ffun, [[P]]FFun
**************************************************)
lemma semFfun_f:
"Pf : Procfun ==> [[Pf f]]F = [[Pf]]Ffun (%p. [[f p]]F)"
apply (simp add: eqF_decompo)
apply (simp add: semFfun_def)
apply (simp add: tracesfun_f failuresfun_f)
apply (simp add: traces_Proc_F failures_Proc_F)
done
lemma semFFun_f_p:
"PF : ProcFun ==> [[PF f p]]F = [[PF]]FFun (%p. [[f p]]F) p"
apply (simp add: eqF_decompo)
apply (simp add: semFFun_def semFfun_def)
apply (simp add: tracesFun_f_p failuresFun_f_p)
apply (simp add: traces_Proc_F failures_Proc_F)
done
lemma semFfun_compo_semFFun_SFf:
"[| Pf : Procfun ; QF : ProcFun |] ==>
[[Pf o QF]]Ffun SFf = [[Pf]]Ffun ([[QF]]FFun SFf)"
apply (simp add: eqF_decompo)
apply (simp add: semFFun_def semFfun_def)
apply (simp add: tracesfun_f failuresfun_f)
apply (simp add: traces_Proc_F failures_Proc_F)
done
lemma semFfun_compo_semFFun_fun:
"[| Pf : Procfun ; QF : ProcFun |] ==>
[[Pf o QF]]Ffun = [[Pf]]Ffun o [[QF]]FFun"
apply (simp add: expand_fun_eq)
apply (simp add: semFfun_compo_semFFun_SFf)
done
lemmas semFfun_compo_ProcFun = semFfun_compo_semFFun_SFf semFfun_compo_semFFun_fun
semFfun_compo_semFFun_SFf[simplified comp_def]
semFfun_compo_semFFun_fun[simplified comp_def]
(*** semFFun ***)
lemma semFFun_compo_semFFun_SFf_lm:
"[| PF : ProcFun; QF : ProcFun |]
==> [[%SFf. PF (QF SFf) p]]Ffun SFf =
[[%SFf. PF SFf p]]Ffun (%p. [[%SFf. QF SFf p]]Ffun SFf)"
apply (insert semFfun_compo_semFFun_fun[of "(%SFf. PF SFf p)" QF])
apply (simp add: ProcFun_def comp_def)
apply (simp add: semFFun_def)
done
lemma semFFun_compo_semFFun_SFf:
"[| PF : ProcFun ; QF : ProcFun |] ==>
[[PF o QF]]FFun SFf = [[PF]]FFun ([[QF]]FFun SFf)"
apply (simp add: semFFun_def)
apply (simp add: semFFun_compo_semFFun_SFf_lm)
done
(*** composition of process functions ***)
lemma semFFun_compo_semFFun_fun:
"[| PF : ProcFun ; QF : ProcFun |] ==>
[[PF o QF]]FFun = [[PF]]FFun o [[QF]]FFun"
apply (simp add: expand_fun_eq)
apply (simp add: semFFun_compo_semFFun_SFf)
done
lemmas semFFun_compo_semFFun = semFFun_compo_semFFun_SFf semFFun_compo_semFFun_fun
semFFun_compo_semFFun_SFf[simplified comp_def]
semFFun_compo_semFFun_fun[simplified comp_def]
lemma semFFun_compo_n_SFf:
"PF : ProcFun ==> [[PF ^ n]]FFun SFf = ([[PF]]FFun ^ n) SFf"
apply (induct_tac n)
apply (simp add: semFFun_def semFfun_def)
apply (simp add: semF_Proc_F)
apply (simp add: semFFun_compo_semFFun iteration_in_ProcFun)
done
lemma semFFun_compo_n:
"PF : ProcFun ==> [[PF ^ n]]FFun = ([[PF]]FFun ^ n)"
apply (simp add: expand_fun_eq)
apply (simp add: semFFun_compo_n_SFf)
done
(**************************************************
tracesfun failuresfun in domF
**************************************************)
lemma tracesfun_failuresfun_in_domF1:
"Pf : Procfun ==> (tracesfun Pf (%p. fstF (SFf p)) , failuresfun Pf SFf) : domF"
apply (subgoal_tac
"(traces (Pf (%p. Proc_F(SFf p))) , failures (Pf (%p. Proc_F(SFf p)))) : domF")
apply (simp only: tracesfun_f failuresfun_f)
apply (simp add: traces_Proc_F failures_Proc_F)
apply (simp)
done
lemma tracesfun_failuresfun_in_domF2:
"Pf : Procfun ==> (tracesfun Pf (fstF o SFf) , failuresfun Pf SFf) : domF"
by (simp add: comp_def tracesfun_failuresfun_in_domF1)
lemmas tracesfun_failuresfun_in_domF = tracesfun_failuresfun_in_domF1
tracesfun_failuresfun_in_domF2
lemma tracesFun_failuresFun_in_domF1:
"PF : ProcFun ==> (tracesFun PF (%p. fstF (SFf p)) p , failuresFun PF SFf p) : domF"
apply (simp add: tracesFun_def)
apply (simp add: failuresFun_def)
apply (simp add: ProcFun_def)
apply (simp add: tracesfun_failuresfun_in_domF)
done
lemma tracesFun_failuresFun_in_domF2:
"PF : ProcFun ==> (tracesFun PF (fstF o SFf) p , failuresFun PF SFf p) : domF"
by (simp add: comp_def tracesFun_failuresFun_in_domF1)
lemmas tracesFun_failuresFun_in_domF = tracesFun_failuresFun_in_domF1
tracesFun_failuresFun_in_domF2
lemmas fun_in_domF = tracesfun_failuresfun_in_domF
tracesFun_failuresFun_in_domF
(**************************************************
fstF and sndF
**************************************************)
lemma fstF_semFfun:
"Pf : Procfun ==> fstF ([[Pf]]Ffun SFf) = tracesfun Pf (fstF o SFf)"
apply (simp add: semF_decompo_fun)
apply (simp add: tracesfun_failuresfun_in_domF pairF)
done
lemma sndF_semFfun:
"Pf : Procfun ==> sndF ([[Pf]]Ffun SFf) = failuresfun Pf SFf"
apply (simp add: semF_decompo_fun)
apply (simp add: tracesfun_failuresfun_in_domF pairF)
done
lemma fstF_semFFun:
"PF : ProcFun ==> fstF ([[PF]]FFun SFf p) = tracesFun PF (fstF o SFf) p"
apply (simp add: semF_decompo_fun)
apply (simp add: tracesFun_failuresFun_in_domF pairF)
done
lemma sndF_semFFun:
"PF : ProcFun ==> sndF ([[PF]]FFun SFf p) = failuresFun PF SFf p"
apply (simp add: semF_decompo_fun)
apply (simp add: tracesFun_failuresFun_in_domF pairF)
done
lemmas pairF_semF = pairF fstF_semFfun sndF_semFfun fstF_semFFun sndF_semFFun
(**************************************************
ProcFun_congruence
**************************************************)
lemma cspF_ProcFun_cong:
"[| PF : ProcFun ; f =F' g |] ==> PF f =F' PF g"
apply (simp add: eqF_prod_def)
apply (rule allI)
apply (simp add: cspF_semantics)
apply (simp add: tracesFun_f_p)
apply (simp add: failuresFun_f_p)
done
lemma cspF_Procfun_cong:
"[| Pf : Procfun ; f =F' g |] ==> Pf f =F Pf g"
apply (insert cspF_ProcFun_cong[of "(%f p. Pf f)" f g])
apply (simp add: ProcFun_def)
apply (simp add: eqF_prod_def)
done
lemma cspF_ProcX_cong:
"[| PX : ProcX ; X1 =F X2 |] ==> PX X1 =F PX X2"
apply (insert cspF_Procfun_cong[of "(%X. PX (X MUp))" "(%p. X1)" "(%p. X2)"])
apply (simp add: ProcX_def)
apply (simp add: eqF_prod_def)
done
lemma cspF_ProcX_cong_traces:
"[| PX : ProcX ; X1 =F X2 |] ==> traces (PX X1) = traces (PX X2)"
apply (insert cspF_ProcX_cong[of PX X1 X2])
apply (simp add: cspF_semantics)
done
lemma cspF_ProcX_cong_failures:
"[| PX : ProcX ; X1 =F X2 |] ==> failures (PX X1) = failures(PX X2)"
apply (insert cspF_ProcX_cong[of PX X1 X2])
apply (simp add: cspF_semantics)
done
end
lemma traces_Pf_Proc_T_F:
Pf ∈ Procfun ==> traces (Pf (%p. Proc_T (fstF (F p)))) = traces (Pf (%p. Proc_F (F p)))
lemma failuresfun_p:
failuresfun (%f. f p) = (%SFf. sndF (SFf p))
lemma failuresfun_STOP:
failuresfun (%f. STOP) = (%SFf. {f. ∃X. f = (<>, X)}f)
lemma failuresfun_SKIP:
failuresfun (%f. SKIP) = (%SFf. {f. (∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X))}f)
lemma failuresfun_DIV:
failuresfun (%f. DIV) = (%SFf. {}f)
lemma failuresfun_Act_prefix:
failuresfun (%f. a -> Pf f) = (%SFf. {f. (∃X. f = (<>, X) ∧ Ev a ∉ X) ∨ (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f failuresfun Pf SFf)}f)
lemma failuresfun_Ext_pre_choice:
failuresfun (%f. ? a:X -> Pff a f) = (%SFf. {f. (∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨ (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f failuresfun (Pff a) SFf ∧ a ∈ X)}f)
lemma failuresfun_Ext_choice:
[| Pf ∈ Procfun; Qf ∈ Procfun |] ==> failuresfun (%f. Pf f [+] Qf f) = (%SFf. {f. (∃X. f = (<>, X)) ∧ f :f failuresfun Pf SFf ∧ f :f failuresfun Qf SFf ∨ (∃s. (∃X. f = (s, X)) ∧ (f :f failuresfun Pf SFf ∨ f :f failuresfun Qf SFf) ∧ s ≠ <>) ∨ (∃X. f = (<>, X) ∧ (<Tick> :t tracesfun Pf (fstF o SFf) ∨ <Tick> :t tracesfun Qf (fstF o SFf)) ∧ X ⊆ Evset)}f)
lemma failuresfun_Int_choice:
failuresfun (%f. Pf f |~| Qf f) = (%SFf. failuresfun Pf SFf UnF failuresfun Qf SFf)
lemma failuresfun_Rep_int_choice_var:
failuresfun (%f. !! c:C .. Pff c f) = (%SFf. {f. ∃c∈C. f :f failuresfun (Pff c) SFf}f)
lemma failuresfun_Rep_int_choice_fun:
inj f ==> failuresfun (%g. !!<f> a:X .. Pff a g) = (%SFf. {f. ∃a∈X. f :f failuresfun (Pff a) SFf}f)
lemma failuresfun_Rep_int_choice_com:
failuresfun (%f. ! a:X .. Pff a f) = (%SFf. {f. ∃a∈X. f :f failuresfun (Pff a) SFf}f)
lemmas failuresfun_Rep_int_choice:
failuresfun (%f. !! c:C .. Pff c f) = (%SFf. {f. ∃c∈C. f :f failuresfun (Pff c) SFf}f)
inj f ==> failuresfun (%g. !!<f> a:X .. Pff a g) = (%SFf. {f. ∃a∈X. f :f failuresfun (Pff a) SFf}f)
failuresfun (%f. ! a:X .. Pff a f) = (%SFf. {f. ∃a∈X. f :f failuresfun (Pff a) SFf}f)
lemmas failuresfun_Rep_int_choice:
failuresfun (%f. !! c:C .. Pff c f) = (%SFf. {f. ∃c∈C. f :f failuresfun (Pff c) SFf}f)
inj f ==> failuresfun (%g. !!<f> a:X .. Pff a g) = (%SFf. {f. ∃a∈X. f :f failuresfun (Pff a) SFf}f)
failuresfun (%f. ! a:X .. Pff a f) = (%SFf. {f. ∃a∈X. f :f failuresfun (Pff a) SFf}f)
lemma failuresfun_IF:
failuresfun (%f. IF b THEN Pf f ELSE Qf f) = (%SFf. if b then failuresfun Pf SFf else failuresfun Qf SFf)
lemma failuresfun_Parallel:
failuresfun (%f. Pf f |[X]| Qf f) = (%SFf. Abs_setF {(u, Y ∪ Z) |u Y Z. Y - (Ev ` X ∪ {Tick}) = Z - (Ev ` X ∪ {Tick}) ∧ (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f failuresfun Pf SFf ∧ (t, Z) :f failuresfun Qf SFf)})
lemma failuresfun_Hiding:
failuresfun (%f. Pf f -- X) = (%SFf. Abs_setF {(s --tr X, Y) |s Y. (s, Ev ` X ∪ Y) :f failuresfun Pf SFf})
lemma failuresfun_Renaming:
failuresfun (%f. Pf f [[r]]) = (%SFf. {f. ∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f failuresfun Pf SFf}f)
lemma failuresfun_Seq_compo:
Pf ∈ Procfun ==> failuresfun (%f. Pf f ;; Qf f) = (%SFf. {f. (∃t X. f = (t, X) ∧ (t, X ∪ {Tick}) :f failuresfun Pf SFf ∧ noTick t) ∨ (∃s t X. f = (s ^^ t, X) ∧ s ^^ <Tick> :t tracesfun Pf (fstF o SFf) ∧ (t, X) :f failuresfun Qf SFf ∧ noTick s)}f)
lemma failuresfun_Depth_rest:
failuresfun (%f. Pf f |. n) = (%SFf. {(t, X). (t, X) :f failuresfun Pf SFf ∧ (lengtht t < n ∨ lengtht t = n ∧ (∃s. t = s ^^ <Tick> ∧ noTick s))}f)
lemmas failuresfun_simp:
failuresfun (%f. f p) = (%SFf. sndF (SFf p))
failuresfun (%f. STOP) = (%SFf. {f. ∃X. f = (<>, X)}f)
failuresfun (%f. SKIP) = (%SFf. {f. (∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X))}f)
failuresfun (%f. DIV) = (%SFf. {}f)
failuresfun (%f. a -> Pf f) = (%SFf. {f. (∃X. f = (<>, X) ∧ Ev a ∉ X) ∨ (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f failuresfun Pf SFf)}f)
failuresfun (%f. ? a:X -> Pff a f) = (%SFf. {f. (∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨ (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f failuresfun (Pff a) SFf ∧ a ∈ X)}f)
[| Pf ∈ Procfun; Qf ∈ Procfun |] ==> failuresfun (%f. Pf f [+] Qf f) = (%SFf. {f. (∃X. f = (<>, X)) ∧ f :f failuresfun Pf SFf ∧ f :f failuresfun Qf SFf ∨ (∃s. (∃X. f = (s, X)) ∧ (f :f failuresfun Pf SFf ∨ f :f failuresfun Qf SFf) ∧ s ≠ <>) ∨ (∃X. f = (<>, X) ∧ (<Tick> :t tracesfun Pf (fstF o SFf) ∨ <Tick> :t tracesfun Qf (fstF o SFf)) ∧ X ⊆ Evset)}f)
failuresfun (%f. Pf f |~| Qf f) = (%SFf. failuresfun Pf SFf UnF failuresfun Qf SFf)
failuresfun (%f. !! c:C .. Pff c f) = (%SFf. {f. ∃c∈C. f :f failuresfun (Pff c) SFf}f)
inj f ==> failuresfun (%g. !!<f> a:X .. Pff a g) = (%SFf. {f. ∃a∈X. f :f failuresfun (Pff a) SFf}f)
failuresfun (%f. ! a:X .. Pff a f) = (%SFf. {f. ∃a∈X. f :f failuresfun (Pff a) SFf}f)
failuresfun (%f. IF b THEN Pf f ELSE Qf f) = (%SFf. if b then failuresfun Pf SFf else failuresfun Qf SFf)
failuresfun (%f. Pf f |[X]| Qf f) = (%SFf. Abs_setF {(u, Y ∪ Z) |u Y Z. Y - (Ev ` X ∪ {Tick}) = Z - (Ev ` X ∪ {Tick}) ∧ (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f failuresfun Pf SFf ∧ (t, Z) :f failuresfun Qf SFf)})
failuresfun (%f. Pf f -- X) = (%SFf. Abs_setF {(s --tr X, Y) |s Y. (s, Ev ` X ∪ Y) :f failuresfun Pf SFf})
failuresfun (%f. Pf f [[r]]) = (%SFf. {f. ∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f failuresfun Pf SFf}f)
Pf ∈ Procfun ==> failuresfun (%f. Pf f ;; Qf f) = (%SFf. {f. (∃t X. f = (t, X) ∧ (t, X ∪ {Tick}) :f failuresfun Pf SFf ∧ noTick t) ∨ (∃s t X. f = (s ^^ t, X) ∧ s ^^ <Tick> :t tracesfun Pf (fstF o SFf) ∧ (t, X) :f failuresfun Qf SFf ∧ noTick s)}f)
failuresfun (%f. Pf f |. n) = (%SFf. {(t, X). (t, X) :f failuresfun Pf SFf ∧ (lengtht t < n ∨ lengtht t = n ∧ (∃s. t = s ^^ <Tick> ∧ noTick s))}f)
lemmas failuresfun_simp:
failuresfun (%f. f p) = (%SFf. sndF (SFf p))
failuresfun (%f. STOP) = (%SFf. {f. ∃X. f = (<>, X)}f)
failuresfun (%f. SKIP) = (%SFf. {f. (∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X))}f)
failuresfun (%f. DIV) = (%SFf. {}f)
failuresfun (%f. a -> Pf f) = (%SFf. {f. (∃X. f = (<>, X) ∧ Ev a ∉ X) ∨ (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f failuresfun Pf SFf)}f)
failuresfun (%f. ? a:X -> Pff a f) = (%SFf. {f. (∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨ (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f failuresfun (Pff a) SFf ∧ a ∈ X)}f)
[| Pf ∈ Procfun; Qf ∈ Procfun |] ==> failuresfun (%f. Pf f [+] Qf f) = (%SFf. {f. (∃X. f = (<>, X)) ∧ f :f failuresfun Pf SFf ∧ f :f failuresfun Qf SFf ∨ (∃s. (∃X. f = (s, X)) ∧ (f :f failuresfun Pf SFf ∨ f :f failuresfun Qf SFf) ∧ s ≠ <>) ∨ (∃X. f = (<>, X) ∧ (<Tick> :t tracesfun Pf (fstF o SFf) ∨ <Tick> :t tracesfun Qf (fstF o SFf)) ∧ X ⊆ Evset)}f)
failuresfun (%f. Pf f |~| Qf f) = (%SFf. failuresfun Pf SFf UnF failuresfun Qf SFf)
failuresfun (%f. !! c:C .. Pff c f) = (%SFf. {f. ∃c∈C. f :f failuresfun (Pff c) SFf}f)
inj f ==> failuresfun (%g. !!<f> a:X .. Pff a g) = (%SFf. {f. ∃a∈X. f :f failuresfun (Pff a) SFf}f)
failuresfun (%f. ! a:X .. Pff a f) = (%SFf. {f. ∃a∈X. f :f failuresfun (Pff a) SFf}f)
failuresfun (%f. IF b THEN Pf f ELSE Qf f) = (%SFf. if b then failuresfun Pf SFf else failuresfun Qf SFf)
failuresfun (%f. Pf f |[X]| Qf f) = (%SFf. Abs_setF {(u, Y ∪ Z) |u Y Z. Y - (Ev ` X ∪ {Tick}) = Z - (Ev ` X ∪ {Tick}) ∧ (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f failuresfun Pf SFf ∧ (t, Z) :f failuresfun Qf SFf)})
failuresfun (%f. Pf f -- X) = (%SFf. Abs_setF {(s --tr X, Y) |s Y. (s, Ev ` X ∪ Y) :f failuresfun Pf SFf})
failuresfun (%f. Pf f [[r]]) = (%SFf. {f. ∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f failuresfun Pf SFf}f)
Pf ∈ Procfun ==> failuresfun (%f. Pf f ;; Qf f) = (%SFf. {f. (∃t X. f = (t, X) ∧ (t, X ∪ {Tick}) :f failuresfun Pf SFf ∧ noTick t) ∨ (∃s t X. f = (s ^^ t, X) ∧ s ^^ <Tick> :t tracesfun Pf (fstF o SFf) ∧ (t, X) :f failuresfun Qf SFf ∧ noTick s)}f)
failuresfun (%f. Pf f |. n) = (%SFf. {(t, X). (t, X) :f failuresfun Pf SFf ∧ (lengtht t < n ∨ lengtht t = n ∧ (∃s. t = s ^^ <Tick> ∧ noTick s))}f)
lemma in_failuresfun_p:
(f :f failuresfun (%f. f p) SFf) = (f :f sndF (SFf p))
lemma in_failuresfun_STOP:
(f :f failuresfun (%f. STOP) SFf) = (∃X. f = (<>, X))
lemma in_failuresfun_SKIP:
(f :f failuresfun (%f. SKIP) SFf) = ((∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X)))
lemma in_failuresfun_DIV:
f ~:f failuresfun (%f. DIV) SFf
lemma in_failuresfun_Act_prefix:
(f :f failuresfun (%f. a -> Pf f) SFf) = ((∃X. f = (<>, X) ∧ Ev a ∉ X) ∨ (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f failuresfun Pf SFf))
lemma in_failuresfun_Ext_pre_choice:
(f :f failuresfun (%f. ? a:X -> Pff a f) SFf) = ((∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨ (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f failuresfun (Pff a) SFf ∧ a ∈ X))
lemma in_failuresfun_Ext_choice:
[| Pf ∈ Procfun; Qf ∈ Procfun |] ==> (f :f failuresfun (%f. Pf f [+] Qf f) SFf) = ((∃X. f = (<>, X)) ∧ f :f failuresfun Pf SFf ∧ f :f failuresfun Qf SFf ∨ (∃s. (∃X. f = (s, X)) ∧ (f :f failuresfun Pf SFf ∨ f :f failuresfun Qf SFf) ∧ s ≠ <>) ∨ (∃X. f = (<>, X) ∧ (<Tick> :t tracesfun Pf (fstF o SFf) ∨ <Tick> :t tracesfun Qf (fstF o SFf)) ∧ X ⊆ Evset))
lemma in_failuresfun_Int_choice:
(f :f failuresfun (%f. Pf f |~| Qf f) SFf) = (f :f failuresfun Pf SFf ∨ f :f failuresfun Qf SFf)
lemma in_failuresfun_Rep_int_choice_var:
(f :f failuresfun (%f. !! c:C .. Pff c f) SFf) = (∃c∈C. f :f failuresfun (Pff c) SFf)
lemma in_failuresfun_Rep_int_choice_fun:
inj g ==> (f :f failuresfun (%f. !!<g> a:X .. Pff a f) SFf) = (∃a∈X. f :f failuresfun (Pff a) SFf)
lemma in_failuresfun_Rep_int_choice_com:
(f :f failuresfun (%f. ! a:X .. Pff a f) SFf) = (∃a∈X. f :f failuresfun (Pff a) SFf)
lemmas in_failuresfun_Rep_int_choice:
(f :f failuresfun (%f. !! c:C .. Pff c f) SFf) = (∃c∈C. f :f failuresfun (Pff c) SFf)
inj g ==> (f :f failuresfun (%f. !!<g> a:X .. Pff a f) SFf) = (∃a∈X. f :f failuresfun (Pff a) SFf)
(f :f failuresfun (%f. ! a:X .. Pff a f) SFf) = (∃a∈X. f :f failuresfun (Pff a) SFf)
lemmas in_failuresfun_Rep_int_choice:
(f :f failuresfun (%f. !! c:C .. Pff c f) SFf) = (∃c∈C. f :f failuresfun (Pff c) SFf)
inj g ==> (f :f failuresfun (%f. !!<g> a:X .. Pff a f) SFf) = (∃a∈X. f :f failuresfun (Pff a) SFf)
(f :f failuresfun (%f. ! a:X .. Pff a f) SFf) = (∃a∈X. f :f failuresfun (Pff a) SFf)
lemma in_failuresfun_IF:
(f :f failuresfun (%f. IF b THEN Pf f ELSE Qf f) SFf) = (if b then f :f failuresfun Pf SFf else f :f failuresfun Qf SFf)
lemma in_failuresfun_Parallel:
(f :f failuresfun (%f. Pf f |[X]| Qf f) SFf) = (∃u Y Z. f = (u, Y ∪ Z) ∧ Y - (Ev ` X ∪ {Tick}) = Z - (Ev ` X ∪ {Tick}) ∧ (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f failuresfun Pf SFf ∧ (t, Z) :f failuresfun Qf SFf))
lemma in_failuresfun_Hiding:
(f :f failuresfun (%f. Pf f -- X) SFf) = (∃s Y. f = (s --tr X, Y) ∧ (s, Ev ` X ∪ Y) :f failuresfun Pf SFf)
lemma in_failuresfun_Renaming:
(f :f failuresfun (%f. Pf f [[r]]) SFf) = (∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f failuresfun Pf SFf)
lemma in_failuresfun_Seq_compo:
Pf ∈ Procfun ==> (f :f failuresfun (%f. Pf f ;; Qf f) SFf) = ((∃t X. f = (t, X) ∧ (t, insert Tick X) :f failuresfun Pf SFf ∧ noTick t) ∨ (∃s t X. f = (s ^^ t, X) ∧ s ^^ <Tick> :t tracesfun Pf (fstF o SFf) ∧ (t, X) :f failuresfun Qf SFf ∧ noTick s))
lemma in_failuresfun_Depth_rest:
(f :f failuresfun (%f. Pf f |. n) SFf) = (∃t X. f = (t, X) ∧ (t, X) :f failuresfun Pf SFf ∧ (lengtht t < n ∨ lengtht t = n ∧ (∃s. t = s ^^ <Tick> ∧ noTick s)))
lemmas in_failuresfun:
(f :f failuresfun (%f. f p) SFf) = (f :f sndF (SFf p))
(f :f failuresfun (%f. STOP) SFf) = (∃X. f = (<>, X))
(f :f failuresfun (%f. SKIP) SFf) = ((∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X)))
f ~:f failuresfun (%f. DIV) SFf
(f :f failuresfun (%f. a -> Pf f) SFf) = ((∃X. f = (<>, X) ∧ Ev a ∉ X) ∨ (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f failuresfun Pf SFf))
(f :f failuresfun (%f. ? a:X -> Pff a f) SFf) = ((∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨ (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f failuresfun (Pff a) SFf ∧ a ∈ X))
[| Pf ∈ Procfun; Qf ∈ Procfun |] ==> (f :f failuresfun (%f. Pf f [+] Qf f) SFf) = ((∃X. f = (<>, X)) ∧ f :f failuresfun Pf SFf ∧ f :f failuresfun Qf SFf ∨ (∃s. (∃X. f = (s, X)) ∧ (f :f failuresfun Pf SFf ∨ f :f failuresfun Qf SFf) ∧ s ≠ <>) ∨ (∃X. f = (<>, X) ∧ (<Tick> :t tracesfun Pf (fstF o SFf) ∨ <Tick> :t tracesfun Qf (fstF o SFf)) ∧ X ⊆ Evset))
(f :f failuresfun (%f. Pf f |~| Qf f) SFf) = (f :f failuresfun Pf SFf ∨ f :f failuresfun Qf SFf)
(f :f failuresfun (%f. !! c:C .. Pff c f) SFf) = (∃c∈C. f :f failuresfun (Pff c) SFf)
inj g ==> (f :f failuresfun (%f. !!<g> a:X .. Pff a f) SFf) = (∃a∈X. f :f failuresfun (Pff a) SFf)
(f :f failuresfun (%f. ! a:X .. Pff a f) SFf) = (∃a∈X. f :f failuresfun (Pff a) SFf)
(f :f failuresfun (%f. IF b THEN Pf f ELSE Qf f) SFf) = (if b then f :f failuresfun Pf SFf else f :f failuresfun Qf SFf)
(f :f failuresfun (%f. Pf f |[X]| Qf f) SFf) = (∃u Y Z. f = (u, Y ∪ Z) ∧ Y - (Ev ` X ∪ {Tick}) = Z - (Ev ` X ∪ {Tick}) ∧ (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f failuresfun Pf SFf ∧ (t, Z) :f failuresfun Qf SFf))
(f :f failuresfun (%f. Pf f -- X) SFf) = (∃s Y. f = (s --tr X, Y) ∧ (s, Ev ` X ∪ Y) :f failuresfun Pf SFf)
(f :f failuresfun (%f. Pf f [[r]]) SFf) = (∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f failuresfun Pf SFf)
Pf ∈ Procfun ==> (f :f failuresfun (%f. Pf f ;; Qf f) SFf) = ((∃t X. f = (t, X) ∧ (t, insert Tick X) :f failuresfun Pf SFf ∧ noTick t) ∨ (∃s t X. f = (s ^^ t, X) ∧ s ^^ <Tick> :t tracesfun Pf (fstF o SFf) ∧ (t, X) :f failuresfun Qf SFf ∧ noTick s))
(f :f failuresfun (%f. Pf f |. n) SFf) = (∃t X. f = (t, X) ∧ (t, X) :f failuresfun Pf SFf ∧ (lengtht t < n ∨ lengtht t = n ∧ (∃s. t = s ^^ <Tick> ∧ noTick s)))
lemmas in_failuresfun:
(f :f failuresfun (%f. f p) SFf) = (f :f sndF (SFf p))
(f :f failuresfun (%f. STOP) SFf) = (∃X. f = (<>, X))
(f :f failuresfun (%f. SKIP) SFf) = ((∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X)))
f ~:f failuresfun (%f. DIV) SFf
(f :f failuresfun (%f. a -> Pf f) SFf) = ((∃X. f = (<>, X) ∧ Ev a ∉ X) ∨ (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f failuresfun Pf SFf))
(f :f failuresfun (%f. ? a:X -> Pff a f) SFf) = ((∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨ (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f failuresfun (Pff a) SFf ∧ a ∈ X))
[| Pf ∈ Procfun; Qf ∈ Procfun |] ==> (f :f failuresfun (%f. Pf f [+] Qf f) SFf) = ((∃X. f = (<>, X)) ∧ f :f failuresfun Pf SFf ∧ f :f failuresfun Qf SFf ∨ (∃s. (∃X. f = (s, X)) ∧ (f :f failuresfun Pf SFf ∨ f :f failuresfun Qf SFf) ∧ s ≠ <>) ∨ (∃X. f = (<>, X) ∧ (<Tick> :t tracesfun Pf (fstF o SFf) ∨ <Tick> :t tracesfun Qf (fstF o SFf)) ∧ X ⊆ Evset))
(f :f failuresfun (%f. Pf f |~| Qf f) SFf) = (f :f failuresfun Pf SFf ∨ f :f failuresfun Qf SFf)
(f :f failuresfun (%f. !! c:C .. Pff c f) SFf) = (∃c∈C. f :f failuresfun (Pff c) SFf)
inj g ==> (f :f failuresfun (%f. !!<g> a:X .. Pff a f) SFf) = (∃a∈X. f :f failuresfun (Pff a) SFf)
(f :f failuresfun (%f. ! a:X .. Pff a f) SFf) = (∃a∈X. f :f failuresfun (Pff a) SFf)
(f :f failuresfun (%f. IF b THEN Pf f ELSE Qf f) SFf) = (if b then f :f failuresfun Pf SFf else f :f failuresfun Qf SFf)
(f :f failuresfun (%f. Pf f |[X]| Qf f) SFf) = (∃u Y Z. f = (u, Y ∪ Z) ∧ Y - (Ev ` X ∪ {Tick}) = Z - (Ev ` X ∪ {Tick}) ∧ (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f failuresfun Pf SFf ∧ (t, Z) :f failuresfun Qf SFf))
(f :f failuresfun (%f. Pf f -- X) SFf) = (∃s Y. f = (s --tr X, Y) ∧ (s, Ev ` X ∪ Y) :f failuresfun Pf SFf)
(f :f failuresfun (%f. Pf f [[r]]) SFf) = (∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f failuresfun Pf SFf)
Pf ∈ Procfun ==> (f :f failuresfun (%f. Pf f ;; Qf f) SFf) = ((∃t X. f = (t, X) ∧ (t, insert Tick X) :f failuresfun Pf SFf ∧ noTick t) ∨ (∃s t X. f = (s ^^ t, X) ∧ s ^^ <Tick> :t tracesfun Pf (fstF o SFf) ∧ (t, X) :f failuresfun Qf SFf ∧ noTick s))
(f :f failuresfun (%f. Pf f |. n) SFf) = (∃t X. f = (t, X) ∧ (t, X) :f failuresfun Pf SFf ∧ (lengtht t < n ∨ lengtht t = n ∧ (∃s. t = s ^^ <Tick> ∧ noTick s)))
lemma proj_failuresFun_failuresfun:
proj_fun p o failuresFun PF = failuresfun (%f. PF f p)
lemma proj_semFFun_semFfun:
proj_fun p o [[PF]]FFun = [[%f. PF f p]]Ffun
lemma failuresfun_f:
Pf ∈ Procfun ==> failures (Pf f) = failuresfun Pf (%p. (traces (f p) ,, failures (f p)))
lemma failuresFun_f_p:
PF ∈ ProcFun ==> failures (PF f p) = failuresFun PF (%p. (traces (f p) ,, failures (f p))) p
lemma semFfun_traces_failures:
Pf ∈ Procfun ==> [[Pf]]Ffun = (%SFf. (traces (Pf (%p. Proc_F (SFf p))) ,, failures (Pf (%p. Proc_F (SFf p)))))
lemma semFfun_tracesfun_failuresfun:
Pf ∈ Procfun ==> [[Pf]]Ffun = (%SFf. (tracesfun Pf (fstF o SFf) ,, failuresfun Pf SFf))
lemma semFFun_traces_failures:
PF ∈ ProcFun ==> [[PF]]FFun = (%SFf p. (traces (PF (%p. Proc_F (SFf p)) p) ,, failures (PF (%p. Proc_F (SFf p)) p)))
lemma semFFun_tracesFun_failuresFun:
PF ∈ ProcFun ==> [[PF]]FFun = (%SFf p. (tracesFun PF (fstF o SFf) p ,, failuresFun PF SFf p))
lemmas semF_decompo:
[[P]]F == (traces P ,, failures P)
Pf ∈ Procfun ==> [[Pf]]Ffun = (%SFf. (traces (Pf (%p. Proc_F (SFf p))) ,, failures (Pf (%p. Proc_F (SFf p)))))
PF ∈ ProcFun ==> [[PF]]FFun = (%SFf p. (traces (PF (%p. Proc_F (SFf p)) p) ,, failures (PF (%p. Proc_F (SFf p)) p)))
lemmas semF_decompo:
[[P]]F == (traces P ,, failures P)
Pf ∈ Procfun ==> [[Pf]]Ffun = (%SFf. (traces (Pf (%p. Proc_F (SFf p))) ,, failures (Pf (%p. Proc_F (SFf p)))))
PF ∈ ProcFun ==> [[PF]]FFun = (%SFf p. (traces (PF (%p. Proc_F (SFf p)) p) ,, failures (PF (%p. Proc_F (SFf p)) p)))
lemmas semF_decompo_fun:
[[P]]F == (traces P ,, failures P)
Pf ∈ Procfun ==> [[Pf]]Ffun = (%SFf. (tracesfun Pf (fstF o SFf) ,, failuresfun Pf SFf))
PF ∈ ProcFun ==> [[PF]]FFun = (%SFf p. (tracesFun PF (fstF o SFf) p ,, failuresFun PF SFf p))
lemmas semF_decompo_fun:
[[P]]F == (traces P ,, failures P)
Pf ∈ Procfun ==> [[Pf]]Ffun = (%SFf. (tracesfun Pf (fstF o SFf) ,, failuresfun Pf SFf))
PF ∈ ProcFun ==> [[PF]]FFun = (%SFf p. (tracesFun PF (fstF o SFf) p ,, failuresFun PF SFf p))
lemma semFfun_variable:
[[%F. F p]]Ffun = (%SFf. SFf p)
lemma failuresfun_compo_failuresFun_SFf:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> failuresfun (Pf o QF) SFf = failuresfun Pf (%p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
lemma failuresfun_compo_failuresFun_fun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> failuresfun (Pf o QF) = failuresfun Pf o (%SFf p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
lemmas failuresfun_compo_failuresFun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> failuresfun (Pf o QF) SFf = failuresfun Pf (%p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> failuresfun (Pf o QF) = failuresfun Pf o (%SFf p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> failuresfun (%x. Pf (QF x)) SFf = failuresfun Pf (%p. (tracesFun QF (%x. fstF (SFf x)) p ,, failuresFun QF SFf p))
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> failuresfun (%x. Pf (QF x)) = (%x. failuresfun Pf (%p. (tracesFun QF (%xa. fstF (x xa)) p ,, failuresFun QF x p)))
lemmas failuresfun_compo_failuresFun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> failuresfun (Pf o QF) SFf = failuresfun Pf (%p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> failuresfun (Pf o QF) = failuresfun Pf o (%SFf p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> failuresfun (%x. Pf (QF x)) SFf = failuresfun Pf (%p. (tracesFun QF (%x. fstF (SFf x)) p ,, failuresFun QF SFf p))
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> failuresfun (%x. Pf (QF x)) = (%x. failuresfun Pf (%p. (tracesFun QF (%xa. fstF (x xa)) p ,, failuresFun QF x p)))
lemma failuresFun_compo_failuresFun_SFf_lm:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresfun (%f. PF (QF f) p) SFf = failuresfun (%SFf. PF SFf p) (%p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
lemma failuresFun_compo_failuresFun_SFf:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresFun (PF o QF) SFf = failuresFun PF (%p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
lemma failuresFun_compo_failuresFun_fun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresFun (PF o QF) = failuresFun PF o (%SFf p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
lemmas failuresFun_compo_failuresFun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresFun (PF o QF) SFf = failuresFun PF (%p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresFun (PF o QF) = failuresFun PF o (%SFf p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresFun (%x. PF (QF x)) SFf = failuresFun PF (%p. (tracesFun QF (%x. fstF (SFf x)) p ,, failuresFun QF SFf p))
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresFun (%x. PF (QF x)) = (%x. failuresFun PF (%p. (tracesFun QF (%xa. fstF (x xa)) p ,, failuresFun QF x p)))
lemmas failuresFun_compo_failuresFun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresFun (PF o QF) SFf = failuresFun PF (%p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresFun (PF o QF) = failuresFun PF o (%SFf p. (tracesFun QF (fstF o SFf) p ,, failuresFun QF SFf p))
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresFun (%x. PF (QF x)) SFf = failuresFun PF (%p. (tracesFun QF (%x. fstF (SFf x)) p ,, failuresFun QF SFf p))
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> failuresFun (%x. PF (QF x)) = (%x. failuresFun PF (%p. (tracesFun QF (%xa. fstF (x xa)) p ,, failuresFun QF x p)))
lemma semFfun_f:
Pf ∈ Procfun ==> [[Pf f]]F = [[Pf]]Ffun (%p. [[f p]]F)
lemma semFFun_f_p:
PF ∈ ProcFun ==> [[PF f p]]F = [[PF]]FFun (%p. [[f p]]F) p
lemma semFfun_compo_semFFun_SFf:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Ffun SFf = [[Pf]]Ffun ([[QF]]FFun SFf)
lemma semFfun_compo_semFFun_fun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Ffun = [[Pf]]Ffun o [[QF]]FFun
lemmas semFfun_compo_ProcFun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Ffun SFf = [[Pf]]Ffun ([[QF]]FFun SFf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Ffun = [[Pf]]Ffun o [[QF]]FFun
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[%x. Pf (QF x)]]Ffun SFf = [[Pf]]Ffun ([[QF]]FFun SFf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[%x. Pf (QF x)]]Ffun = (%x. [[Pf]]Ffun ([[QF]]FFun x))
lemmas semFfun_compo_ProcFun:
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Ffun SFf = [[Pf]]Ffun ([[QF]]FFun SFf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[Pf o QF]]Ffun = [[Pf]]Ffun o [[QF]]FFun
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[%x. Pf (QF x)]]Ffun SFf = [[Pf]]Ffun ([[QF]]FFun SFf)
[| Pf ∈ Procfun; QF ∈ ProcFun |] ==> [[%x. Pf (QF x)]]Ffun = (%x. [[Pf]]Ffun ([[QF]]FFun x))
lemma semFFun_compo_semFFun_SFf_lm:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[%SFf. PF (QF SFf) p]]Ffun SFf = [[%SFf. PF SFf p]]Ffun (%p. [[%SFf. QF SFf p]]Ffun SFf)
lemma semFFun_compo_semFFun_SFf:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]FFun SFf = [[PF]]FFun ([[QF]]FFun SFf)
lemma semFFun_compo_semFFun_fun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]FFun = [[PF]]FFun o [[QF]]FFun
lemmas semFFun_compo_semFFun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]FFun SFf = [[PF]]FFun ([[QF]]FFun SFf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]FFun = [[PF]]FFun o [[QF]]FFun
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[%x. PF (QF x)]]FFun SFf = [[PF]]FFun ([[QF]]FFun SFf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[%x. PF (QF x)]]FFun = (%x. [[PF]]FFun ([[QF]]FFun x))
lemmas semFFun_compo_semFFun:
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]FFun SFf = [[PF]]FFun ([[QF]]FFun SFf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[PF o QF]]FFun = [[PF]]FFun o [[QF]]FFun
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[%x. PF (QF x)]]FFun SFf = [[PF]]FFun ([[QF]]FFun SFf)
[| PF ∈ ProcFun; QF ∈ ProcFun |] ==> [[%x. PF (QF x)]]FFun = (%x. [[PF]]FFun ([[QF]]FFun x))
lemma semFFun_compo_n_SFf:
PF ∈ ProcFun ==> [[PF ^ n]]FFun SFf = ([[PF]]FFun ^ n) SFf
lemma semFFun_compo_n:
PF ∈ ProcFun ==> [[PF ^ n]]FFun = [[PF]]FFun ^ n
lemma tracesfun_failuresfun_in_domF1:
Pf ∈ Procfun ==> (tracesfun Pf (%p. fstF (SFf p)), failuresfun Pf SFf) ∈ domF
lemma tracesfun_failuresfun_in_domF2:
Pf ∈ Procfun ==> (tracesfun Pf (fstF o SFf), failuresfun Pf SFf) ∈ domF
lemmas tracesfun_failuresfun_in_domF:
Pf ∈ Procfun ==> (tracesfun Pf (%p. fstF (SFf p)), failuresfun Pf SFf) ∈ domF
Pf ∈ Procfun ==> (tracesfun Pf (fstF o SFf), failuresfun Pf SFf) ∈ domF
lemmas tracesfun_failuresfun_in_domF:
Pf ∈ Procfun ==> (tracesfun Pf (%p. fstF (SFf p)), failuresfun Pf SFf) ∈ domF
Pf ∈ Procfun ==> (tracesfun Pf (fstF o SFf), failuresfun Pf SFf) ∈ domF
lemma tracesFun_failuresFun_in_domF1:
PF ∈ ProcFun ==> (tracesFun PF (%p. fstF (SFf p)) p, failuresFun PF SFf p) ∈ domF
lemma tracesFun_failuresFun_in_domF2:
PF ∈ ProcFun ==> (tracesFun PF (fstF o SFf) p, failuresFun PF SFf p) ∈ domF
lemmas tracesFun_failuresFun_in_domF:
PF ∈ ProcFun ==> (tracesFun PF (%p. fstF (SFf p)) p, failuresFun PF SFf p) ∈ domF
PF ∈ ProcFun ==> (tracesFun PF (fstF o SFf) p, failuresFun PF SFf p) ∈ domF
lemmas tracesFun_failuresFun_in_domF:
PF ∈ ProcFun ==> (tracesFun PF (%p. fstF (SFf p)) p, failuresFun PF SFf p) ∈ domF
PF ∈ ProcFun ==> (tracesFun PF (fstF o SFf) p, failuresFun PF SFf p) ∈ domF
lemmas fun_in_domF:
Pf ∈ Procfun ==> (tracesfun Pf (%p. fstF (SFf p)), failuresfun Pf SFf) ∈ domF
Pf ∈ Procfun ==> (tracesfun Pf (fstF o SFf), failuresfun Pf SFf) ∈ domF
PF ∈ ProcFun ==> (tracesFun PF (%p. fstF (SFf p)) p, failuresFun PF SFf p) ∈ domF
PF ∈ ProcFun ==> (tracesFun PF (fstF o SFf) p, failuresFun PF SFf p) ∈ domF
lemmas fun_in_domF:
Pf ∈ Procfun ==> (tracesfun Pf (%p. fstF (SFf p)), failuresfun Pf SFf) ∈ domF
Pf ∈ Procfun ==> (tracesfun Pf (fstF o SFf), failuresfun Pf SFf) ∈ domF
PF ∈ ProcFun ==> (tracesFun PF (%p. fstF (SFf p)) p, failuresFun PF SFf p) ∈ domF
PF ∈ ProcFun ==> (tracesFun PF (fstF o SFf) p, failuresFun PF SFf p) ∈ domF
lemma fstF_semFfun:
Pf ∈ Procfun ==> fstF ([[Pf]]Ffun SFf) = tracesfun Pf (fstF o SFf)
lemma sndF_semFfun:
Pf ∈ Procfun ==> sndF ([[Pf]]Ffun SFf) = failuresfun Pf SFf
lemma fstF_semFFun:
PF ∈ ProcFun ==> fstF ([[PF]]FFun SFf p) = tracesFun PF (fstF o SFf) p
lemma sndF_semFFun:
PF ∈ ProcFun ==> sndF ([[PF]]FFun SFf p) = failuresFun PF SFf p
lemmas pairF_semF:
(S, F) ∈ domF ==> fstF (S ,, F) = S
(S, F) ∈ domF ==> sndF (S ,, F) = F
(SF = SE) = (fstF SF = fstF SE ∧ sndF SF = sndF SE)
Pf ∈ Procfun ==> fstF ([[Pf]]Ffun SFf) = tracesfun Pf (fstF o SFf)
Pf ∈ Procfun ==> sndF ([[Pf]]Ffun SFf) = failuresfun Pf SFf
PF ∈ ProcFun ==> fstF ([[PF]]FFun SFf p) = tracesFun PF (fstF o SFf) p
PF ∈ ProcFun ==> sndF ([[PF]]FFun SFf p) = failuresFun PF SFf p
lemmas pairF_semF:
(S, F) ∈ domF ==> fstF (S ,, F) = S
(S, F) ∈ domF ==> sndF (S ,, F) = F
(SF = SE) = (fstF SF = fstF SE ∧ sndF SF = sndF SE)
Pf ∈ Procfun ==> fstF ([[Pf]]Ffun SFf) = tracesfun Pf (fstF o SFf)
Pf ∈ Procfun ==> sndF ([[Pf]]Ffun SFf) = failuresfun Pf SFf
PF ∈ ProcFun ==> fstF ([[PF]]FFun SFf p) = tracesFun PF (fstF o SFf) p
PF ∈ ProcFun ==> sndF ([[PF]]FFun SFf p) = failuresFun PF SFf p
lemma cspF_ProcFun_cong:
[| PF ∈ ProcFun; f =F' g |] ==> PF f =F' PF g
lemma cspF_Procfun_cong:
[| Pf ∈ Procfun; f =F' g |] ==> Pf f =F Pf g
lemma cspF_ProcX_cong:
[| PX ∈ ProcX; X1.0 =F X2.0 |] ==> PX X1.0 =F PX X2.0
lemma cspF_ProcX_cong_traces:
[| PX ∈ ProcX; X1.0 =F X2.0 |] ==> traces (PX X1.0) = traces (PX X2.0)
lemma cspF_ProcX_cong_failures:
[| PX ∈ ProcX; X1.0 =F X2.0 |] ==> failures (PX X1.0) = failures (PX X2.0)