Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T
theory CSP_T_traces (*-------------------------------------------*
| CSP-Prover on Isabelle2004 |
| December 2004 |
| June 2005 (modified) |
| August 2005 (modified) |
| |
| CSP-Prover on Isabelle2005 |
| October 2005 (modified) |
| December 2005 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_T_traces = CSP_T_semantics:
(* The following simplification rules are deleted in this theory file *)
(* because they unexpectly rewrite UnionT and InterT. *)
(* disj_not1: (~ P | Q) = (P --> Q) *)
declare disj_not1 [simp del]
(*********************************************************
DomT
*********************************************************)
(*--------------------------------*
| STOP |
*--------------------------------*)
lemma in_traces_STOP: "(t :t traces(STOP)) = (t = <>)"
by (simp add: traces_def)
(*--------------------------------*
| SKIP |
*--------------------------------*)
lemma in_traces_SKIP: "(t :t traces(SKIP)) = (t = <> | t = <Tick>)"
by (simp add: traces_def)
(*--------------------------------*
| DIV |
*--------------------------------*)
(*** DIV ***)
lemma in_traces_DIV: "(t :t traces(DIV)) = (t = <>)"
by (simp add: traces_def)
(*--------------------------------*
| Act_prefix |
*--------------------------------*)
(*** Act_prefix_domT ***)
lemma Act_prefix_domT:
"{t. t = <> | (EX s. t = <Ev a> ^^ s & s :t T)} : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (erule disjE, simp) (* <> *)
apply (elim conjE exE, simp)
apply (erule disjE, simp) (* <> *)
apply (elim conjE exE, simp)
apply (rule memT_prefix_closed)
by (simp_all)
(*** Act_prefix ***)
lemma in_traces_Act_prefix:
"t :t traces(a -> P) = (t = <> | (EX s. t = <Ev a> ^^ s & s :t traces(P)))"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Act_prefix_domT)
(*--------------------------------*
| Ext_pre_choice |
*--------------------------------*)
(*** Ext_pre_choice_domT ***)
lemma Ext_pre_choice_domT:
"{t. t = <> |
(EX a s. t = <Ev a> ^^ s & s :t Tf a & a : X) } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (erule disjE, simp) (* <> *)
apply (elim conjE exE, simp)
apply (erule disjE, simp) (* <> *)
apply (elim conjE exE, simp)
apply (rule memT_prefix_closed)
by (simp_all)
(*** Ext_pre_choice ***)
lemma in_traces_Ext_pre_choice:
"(t :t traces(? :X -> Pf)) =
(t = <> | (EX a s. t = <Ev a> ^^ s & s :t traces(Pf a) & a : X))"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Ext_pre_choice_domT)
(*--------------------------------*
| Ext_choice |
*--------------------------------*)
(*** Ext_choice_memT ***)
lemma in_traces_Ext_choice:
"(t :t traces(P [+] Q)) = (t :t traces(P) | t :t traces(Q))"
by (simp add: traces_def)
(*--------------------------------*
| Int_choice |
*--------------------------------*)
(*** Int_choice_memT ***)
lemma in_traces_Int_choice:
"(t :t traces(P |~| Q)) = (t :t traces(P) | t :t traces(Q))"
by (simp add: traces_def)
(*--------------------------------*
| Rep_int_choice |
*--------------------------------*)
(*** Rep_int_choice_domT ***)
lemma Rep_int_choice_domT:
"{t. t = <> | (EX a:X. t :t Tf a) } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (erule disjE, simp) (* <> *)
apply (elim conjE bexE)
apply (rule disjI2)
apply (rule_tac x="a" in bexI)
apply (rule memT_prefix_closed)
by (simp_all)
(*** Union_proc ***)
lemma in_traces_Union_proc:
"(t :t {t. t = <> | (EX a:X. t :t Tf a)}t)
= (t = <> | (EX a:X. t :t Tf a))"
apply (insert Rep_int_choice_domT[of X Tf])
apply (simp add: CollectT_open_memT)
done
lemma in_traces_UNIV_Union_proc:
"(t :t {t. EX a. t :t Tf a}t)
= (EX a. t :t Tf a)"
apply (insert in_traces_Union_proc[of t UNIV Tf])
apply (simp)
apply (subgoal_tac "{t. t = <> | (EX a. t :t Tf a)}
= {t. EX a. t :t Tf a}")
by (auto)
(*** Rep_int_choice ***)
lemma in_traces_Rep_int_choice_var:
"(t :t traces(!! :C .. Pf)) = (t = <> | (EX c:C. t :t traces(Pf c)))"
apply (simp add: traces_def)
apply (simp add: in_traces_Union_proc)
done
lemma in_traces_Rep_int_choice_fun:
"inj f ==> (t :t traces(!!<f> :X .. Pf)) = (t = <> | (EX a:X. t :t traces(Pf a)))"
apply (simp add: traces_def)
apply (simp add: in_traces_Union_proc)
done
lemma in_traces_Rep_int_choice_com:
"(t :t traces(! :X .. Pf)) = (t = <> | (EX a:X. t :t traces(Pf a)))"
apply (simp add: traces_def)
apply (simp add: in_traces_Union_proc)
done
lemmas in_traces_Rep_int_choice = in_traces_Rep_int_choice_var
in_traces_Rep_int_choice_com
in_traces_Rep_int_choice_fun
(*--------------------------------*
| IF |
*--------------------------------*)
(*** IF ***)
lemma in_traces_IF:
"(t :t traces(IF b THEN P ELSE Q))
= (if b then t :t traces(P) else t :t traces(Q))"
by (simp add: traces_def)
(*--------------------------------*
| Parallel |
*--------------------------------*)
(*** Parallel_domT ***)
lemma Parallel_domT :
"{u. EX s t. u : s |[X]|tr t & s :t T & t :t S} : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)
(* prefix closed *)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (erule par_tr_prefixE, simp)
apply (rule_tac x="s'" in exI)
apply (rule_tac x="t'" in exI)
apply (simp)
apply (rule conjI)
by (rule memT_prefix_closed, simp_all)+
(*** Parallel ***)
lemma in_traces_Parallel:
"(u :t traces(P |[X]| Q)) =
(EX s t. u : s |[X]|tr t & s :t traces(P) & t :t traces(Q))"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Parallel_domT)
(*--------------------------------*
| Hiding |
*--------------------------------*)
(*** Hiding_domT ***)
lemma Hiding_domT :
"{t. EX s. t = s --tr X & s :t T } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)
(* prefix closed *)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp add: hide_tr_prefix)
apply (elim conjE exE)
apply (rule_tac x="ta" in exI)
apply (simp)
apply (rule memT_prefix_closed)
by (simp_all)
(*** Hiding ***)
lemma in_traces_Hiding:
"(t :t traces(P -- X)) =
(EX s. t = s --tr X & s :t traces(P))"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Hiding_domT)
(*--------------------------------*
| Renaming |
*--------------------------------*)
(*** Renaming_domT ***)
lemma Renaming_domT : "{t. EX s. s [[r]]* t & s :t T } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)
(* prefix closed *)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (erule ren_tr_prefixE, simp)
apply (rule_tac x="ta" in exI)
apply (simp)
apply (rule memT_prefix_closed)
by (simp_all)
(*** Renaming ***)
lemma in_traces_Renaming:
"(t :t traces(P [[r]])) = (EX s. s [[r]]* t & s :t traces(P))"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Renaming_domT)
(*--------------------------------*
| Seq_compo |
*--------------------------------*)
(*** Seq_compo_domT ***)
lemma Seq_compo_domT :
"{u. (EX s. u = rmTick s & s :t S ) |
(EX s t. u = s ^^ t & s ^^ <Tick> :t S & t :t T & noTick s ) } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI)
apply (rule disjI1)
apply (rule_tac x="<>" in exI, simp)
(* prefix closed *)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (erule disjE)
(* case 1 *)
apply (elim conjE exE)
apply (rule disjI1)
apply (simp add: rmTick_prefix)
apply (elim conjE exE)
apply (rule_tac x="u" in exI, simp)
apply (rule memT_prefix_closed, simp_all)
(* case 2 *)
apply (elim conjE exE)
apply (simp add: prefix_def)
apply (elim exE conjE)
apply (simp add: appt_decompo)
apply (erule disjE)
(* long case *)
apply (elim conjE exE)
apply (rule disjI2)
apply (rule_tac x="sa" in exI, simp)
apply (rule_tac x="ua" in exI, simp)
apply (subgoal_tac "prefix ua (ua ^^ u)")
apply (rule memT_prefix_closed, simp_all)
apply (simp)
(* short case *)
apply (elim conjE exE)
apply (rule disjI1)
apply (rule_tac x="s" in exI)
apply (case_tac "~ noTick s", simp)
apply (simp)
apply (subgoal_tac "prefix s (s ^^ ua ^^ <Tick>)")
apply (rule memT_prefix_closed, simp_all)
apply (simp)
done
(*** Seq_compo ***)
lemma in_traces_Seq_compo:
"(u :t traces(P ;; Q)) =
((EX s. u = rmTick s & s :t traces(P)) |
(EX s t. u = s ^^ t & s ^^ <Tick> :t traces(P) & t :t traces(Q) & noTick s))"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Seq_compo_domT)
(*--------------------------------*
| Depth_rest |
*--------------------------------*)
(*** Depth_rest ***)
lemma in_traces_Depth_rest:
"(t :t traces(P |. n)) = (t :t traces(P) & (lengtht t) <= n)"
apply (simp add: traces_def)
apply (simp add: in_rest_domT)
done
(*--------------------------------*
| alias |
*--------------------------------*)
lemmas traces_domT = Act_prefix_domT Ext_pre_choice_domT
Rep_int_choice_domT Parallel_domT
Hiding_domT Renaming_domT
Seq_compo_domT
lemmas in_traces = in_traces_STOP in_traces_SKIP in_traces_DIV
in_traces_Act_prefix in_traces_Ext_pre_choice
in_traces_Ext_choice in_traces_Int_choice
in_traces_Rep_int_choice in_traces_IF
in_traces_Parallel in_traces_Hiding
in_traces_Renaming in_traces_Seq_compo
in_traces_Union_proc in_traces_UNIV_Union_proc
in_traces_Depth_rest
(*--------------------------------*
| Timeout |
*--------------------------------*)
(*** Timemout ***)
lemma in_traces_Timeout1:
"(t :t traces(P [> Q)) = (t :t traces(P) | t :t traces(Q))"
apply (simp add: traces_def)
done
lemma in_traces_Timeout2:
"(t :t traces(P [>def Q)) = (t :t traces(P) | t :t traces(Q))"
apply (simp add: Timeout_def traces_def)
done
lemmas in_traces_Timeout = in_traces_Timeout1 in_traces_Timeout2
(****************** to add them again ******************)
declare disj_not1 [simp]
end
lemma in_traces_STOP:
(t :t traces STOP) = (t = <>)
lemma in_traces_SKIP:
(t :t traces SKIP) = (t = <> ∨ t = <Tick>)
lemma in_traces_DIV:
(t :t traces DIV) = (t = <>)
lemma Act_prefix_domT:
{t. t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t T)} ∈ domT
lemma in_traces_Act_prefix:
(t :t traces (a -> P)) = (t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t traces P))
lemma Ext_pre_choice_domT:
{t. t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t Tf a ∧ a ∈ X)} ∈ domT
lemma in_traces_Ext_pre_choice:
(t :t traces (? :X -> Pf)) = (t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t traces (Pf a) ∧ a ∈ X))
lemma in_traces_Ext_choice:
(t :t traces (P [+] Q)) = (t :t traces P ∨ t :t traces Q)
lemma in_traces_Int_choice:
(t :t traces (P |~| Q)) = (t :t traces P ∨ t :t traces Q)
lemma Rep_int_choice_domT:
{t. t = <> ∨ (∃a∈X. t :t Tf a)} ∈ domT
lemma in_traces_Union_proc:
(t :t {t. t = <> ∨ (∃a∈X. t :t Tf a)}t) = (t = <> ∨ (∃a∈X. t :t Tf a))
lemma in_traces_UNIV_Union_proc:
(t :t {t. ∃a. t :t Tf a}t) = (∃a. t :t Tf a)
lemma in_traces_Rep_int_choice_var:
(t :t traces (!! :C .. Pf)) = (t = <> ∨ (∃c∈C. t :t traces (Pf c)))
lemma in_traces_Rep_int_choice_fun:
inj f ==> (t :t traces (!!<f> :X .. Pf)) = (t = <> ∨ (∃a∈X. t :t traces (Pf a)))
lemma in_traces_Rep_int_choice_com:
(t :t traces (! :X .. Pf)) = (t = <> ∨ (∃a∈X. t :t traces (Pf a)))
lemmas in_traces_Rep_int_choice:
(t :t traces (!! :C .. Pf)) = (t = <> ∨ (∃c∈C. t :t traces (Pf c)))
(t :t traces (! :X .. Pf)) = (t = <> ∨ (∃a∈X. t :t traces (Pf a)))
inj f ==> (t :t traces (!!<f> :X .. Pf)) = (t = <> ∨ (∃a∈X. t :t traces (Pf a)))
lemmas in_traces_Rep_int_choice:
(t :t traces (!! :C .. Pf)) = (t = <> ∨ (∃c∈C. t :t traces (Pf c)))
(t :t traces (! :X .. Pf)) = (t = <> ∨ (∃a∈X. t :t traces (Pf a)))
inj f ==> (t :t traces (!!<f> :X .. Pf)) = (t = <> ∨ (∃a∈X. t :t traces (Pf a)))
lemma in_traces_IF:
(t :t traces (IF b THEN P ELSE Q)) = (if b then t :t traces P else t :t traces Q)
lemma Parallel_domT:
{u. ∃s t. u ∈ s |[X]|tr t ∧ s :t T ∧ t :t S} ∈ domT
lemma in_traces_Parallel:
(u :t traces (P |[X]| Q)) = (∃s t. u ∈ s |[X]|tr t ∧ s :t traces P ∧ t :t traces Q)
lemma Hiding_domT:
{s --tr X |s. s :t T} ∈ domT
lemma in_traces_Hiding:
(t :t traces (P -- X)) = (∃s. t = s --tr X ∧ s :t traces P)
lemma Renaming_domT:
{t. ∃s. s [[r]]* t ∧ s :t T} ∈ domT
lemma in_traces_Renaming:
(t :t traces (P [[r]])) = (∃s. s [[r]]* t ∧ s :t traces P)
lemma Seq_compo_domT:
{u. (∃s. u = rmTick s ∧ s :t S) ∨
(∃s t. u = s ^^ t ∧ s ^^ <Tick> :t S ∧ t :t T ∧ noTick s)}
∈ domT
lemma in_traces_Seq_compo:
(u :t traces (P ;; Q)) = ((∃s. u = rmTick s ∧ s :t traces P) ∨ (∃s t. u = s ^^ t ∧ s ^^ <Tick> :t traces P ∧ t :t traces Q ∧ noTick s))
lemma in_traces_Depth_rest:
(t :t traces (P |. n)) = (t :t traces P ∧ lengtht t ≤ n)
lemmas traces_domT:
{t. t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t T)} ∈ domT
{t. t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t Tf a ∧ a ∈ X)} ∈ domT
{t. t = <> ∨ (∃a∈X. t :t Tf a)} ∈ domT
{u. ∃s t. u ∈ s |[X]|tr t ∧ s :t T ∧ t :t S} ∈ domT
{s --tr X |s. s :t T} ∈ domT
{t. ∃s. s [[r]]* t ∧ s :t T} ∈ domT
{u. (∃s. u = rmTick s ∧ s :t S) ∨
(∃s t. u = s ^^ t ∧ s ^^ <Tick> :t S ∧ t :t T ∧ noTick s)}
∈ domT
lemmas traces_domT:
{t. t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t T)} ∈ domT
{t. t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t Tf a ∧ a ∈ X)} ∈ domT
{t. t = <> ∨ (∃a∈X. t :t Tf a)} ∈ domT
{u. ∃s t. u ∈ s |[X]|tr t ∧ s :t T ∧ t :t S} ∈ domT
{s --tr X |s. s :t T} ∈ domT
{t. ∃s. s [[r]]* t ∧ s :t T} ∈ domT
{u. (∃s. u = rmTick s ∧ s :t S) ∨
(∃s t. u = s ^^ t ∧ s ^^ <Tick> :t S ∧ t :t T ∧ noTick s)}
∈ domT
lemmas in_traces:
(t :t traces STOP) = (t = <>)
(t :t traces SKIP) = (t = <> ∨ t = <Tick>)
(t :t traces DIV) = (t = <>)
(t :t traces (a -> P)) = (t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t traces P))
(t :t traces (? :X -> Pf)) = (t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t traces (Pf a) ∧ a ∈ X))
(t :t traces (P [+] Q)) = (t :t traces P ∨ t :t traces Q)
(t :t traces (P |~| Q)) = (t :t traces P ∨ t :t traces Q)
(t :t traces (!! :C .. Pf)) = (t = <> ∨ (∃c∈C. t :t traces (Pf c)))
(t :t traces (! :X .. Pf)) = (t = <> ∨ (∃a∈X. t :t traces (Pf a)))
inj f ==> (t :t traces (!!<f> :X .. Pf)) = (t = <> ∨ (∃a∈X. t :t traces (Pf a)))
(t :t traces (IF b THEN P ELSE Q)) = (if b then t :t traces P else t :t traces Q)
(u :t traces (P |[X]| Q)) = (∃s t. u ∈ s |[X]|tr t ∧ s :t traces P ∧ t :t traces Q)
(t :t traces (P -- X)) = (∃s. t = s --tr X ∧ s :t traces P)
(t :t traces (P [[r]])) = (∃s. s [[r]]* t ∧ s :t traces P)
(u :t traces (P ;; Q)) = ((∃s. u = rmTick s ∧ s :t traces P) ∨ (∃s t. u = s ^^ t ∧ s ^^ <Tick> :t traces P ∧ t :t traces Q ∧ noTick s))
(t :t {t. t = <> ∨ (∃a∈X. t :t Tf a)}t) = (t = <> ∨ (∃a∈X. t :t Tf a))
(t :t {t. ∃a. t :t Tf a}t) = (∃a. t :t Tf a)
(t :t traces (P |. n)) = (t :t traces P ∧ lengtht t ≤ n)
lemmas in_traces:
(t :t traces STOP) = (t = <>)
(t :t traces SKIP) = (t = <> ∨ t = <Tick>)
(t :t traces DIV) = (t = <>)
(t :t traces (a -> P)) = (t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t traces P))
(t :t traces (? :X -> Pf)) = (t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t traces (Pf a) ∧ a ∈ X))
(t :t traces (P [+] Q)) = (t :t traces P ∨ t :t traces Q)
(t :t traces (P |~| Q)) = (t :t traces P ∨ t :t traces Q)
(t :t traces (!! :C .. Pf)) = (t = <> ∨ (∃c∈C. t :t traces (Pf c)))
(t :t traces (! :X .. Pf)) = (t = <> ∨ (∃a∈X. t :t traces (Pf a)))
inj f ==> (t :t traces (!!<f> :X .. Pf)) = (t = <> ∨ (∃a∈X. t :t traces (Pf a)))
(t :t traces (IF b THEN P ELSE Q)) = (if b then t :t traces P else t :t traces Q)
(u :t traces (P |[X]| Q)) = (∃s t. u ∈ s |[X]|tr t ∧ s :t traces P ∧ t :t traces Q)
(t :t traces (P -- X)) = (∃s. t = s --tr X ∧ s :t traces P)
(t :t traces (P [[r]])) = (∃s. s [[r]]* t ∧ s :t traces P)
(u :t traces (P ;; Q)) = ((∃s. u = rmTick s ∧ s :t traces P) ∨ (∃s t. u = s ^^ t ∧ s ^^ <Tick> :t traces P ∧ t :t traces Q ∧ noTick s))
(t :t {t. t = <> ∨ (∃a∈X. t :t Tf a)}t) = (t = <> ∨ (∃a∈X. t :t Tf a))
(t :t {t. ∃a. t :t Tf a}t) = (∃a. t :t Tf a)
(t :t traces (P |. n)) = (t :t traces P ∧ lengtht t ≤ n)
lemma in_traces_Timeout1:
(t :t traces (P [> Q)) = (t :t traces P ∨ t :t traces Q)
lemma in_traces_Timeout2:
(t :t traces (P [>def Q)) = (t :t traces P ∨ t :t traces Q)
lemmas in_traces_Timeout:
(t :t traces (P [> Q)) = (t :t traces P ∨ t :t traces Q)
(t :t traces (P [>def Q)) = (t :t traces P ∨ t :t traces Q)
lemmas in_traces_Timeout:
(t :t traces (P [> Q)) = (t :t traces P ∨ t :t traces Q)
(t :t traces (P [>def Q)) = (t :t traces P ∨ t :t traces Q)