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) |
| March 2007 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_T_traces
imports CSP_T_semantics
begin
(* 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) M) = (t = <>)"
by (simp add: traces_def)
(*--------------------------------*
| SKIP |
*--------------------------------*)
lemma in_traces_SKIP: "(t :t traces(SKIP) M) = (t = <> | t = <Tick>)"
by (simp add: traces_def)
(*--------------------------------*
| DIV |
*--------------------------------*)
(*** DIV ***)
lemma in_traces_DIV: "(t :t traces(DIV) M) = (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) M = (t = <> | (EX s. t = <Ev a> ^^ s & s :t traces(P) M))"
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) M) =
(t = <> | (EX a s. t = <Ev a> ^^ s & s :t traces(Pf a) M & 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) M) = (t :t traces(P) M | t :t traces(Q) M)"
by (simp add: traces_def)
(*--------------------------------*
| Int_choice |
*--------------------------------*)
(*** Int_choice_memT ***)
lemma in_traces_Int_choice:
"(t :t traces(P |~| Q) M) = (t :t traces(P) M| t :t traces(Q) M)"
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_sum:
"(t :t traces(!! :C .. Pf) M) =
(t = <> | (EX c: sumset C. t :t traces(Pf c) M))"
apply (simp add: traces_def)
apply (simp add: in_traces_Union_proc)
done
lemma in_traces_Rep_int_choice_nat:
"(t :t traces(!nat :N .. Pf) M) = (t = <> | (EX n:N. t :t traces(Pf n) M))"
by (simp add: Rep_int_choice_ss_def in_traces_Rep_int_choice_sum)
lemma in_traces_Rep_int_choice_set:
"(t :t traces(!set :Xs .. Pf) M) = (t = <> | (EX X:Xs. t :t traces(Pf X) M))"
by (simp add: Rep_int_choice_ss_def in_traces_Rep_int_choice_sum)
lemma in_traces_Rep_int_choice_com:
"(t :t traces(! :X .. Pf) M) = (t = <> | (EX a:X. t :t traces(Pf a) M))"
apply (simp add: traces_def)
apply (simp add: in_traces_Union_proc)
done
lemma in_traces_Rep_int_choice_f:
"inj f ==> (t :t traces(!<f> :X .. Pf) M) = (t = <> | (EX a:X. t :t traces(Pf a) M))"
apply (simp add: traces_def)
apply (simp add: in_traces_Union_proc)
done
lemmas in_traces_Rep_int_choice = in_traces_Rep_int_choice_sum
in_traces_Rep_int_choice_set
in_traces_Rep_int_choice_nat
in_traces_Rep_int_choice_com
in_traces_Rep_int_choice_f
(*--------------------------------*
| IF |
*--------------------------------*)
(*** IF ***)
lemma in_traces_IF:
"(t :t traces(IF b THEN P ELSE Q) M)
= (if b then t :t traces(P) M else t :t traces(Q) M)"
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) M) =
(EX s t. u : s |[X]|tr t & s :t traces(P) M & t :t traces(Q) M)"
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) M) =
(EX s. t = s --tr X & s :t traces(P) M)"
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]]) M) = (EX s. s [[r]]* t & s :t traces(P) M)"
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) M) =
((EX s. u = rmTick s & s :t traces(P) M) |
(EX s t. u = s ^^ t & s ^^ <Tick> :t traces(P) M & t :t traces(Q) M & 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) M) = (t :t traces(P) M & (lengtht t) <= n)"
apply (simp add: traces_def)
apply (simp add: in_rest_domT)
done
(*--------------------------------*
| Proc_name |
*--------------------------------*)
(*** Proc_name ***)
lemma in_traces_Proc_name:
"(t :t traces($p) M) = (t :t M p)"
apply (simp add: traces_def)
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 in_traces_Proc_name
(*--------------------------------*
| Timeout |
*--------------------------------*)
(*** Timemout ***)
lemma in_traces_Timeout1:
"(t :t traces(P [> Q) M) = (t :t traces(P) M | t :t traces(Q) M)"
apply (simp add: traces_def)
done
lemma in_traces_Timeout2:
"(t :t traces(P [>def Q) M) = (t :t traces(P) M | t :t traces(Q) M)"
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 M) = (t = <>)
lemma in_traces_SKIP:
(t :t traces SKIP M) = (t = <> ∨ t = <Tick>)
lemma in_traces_DIV:
(t :t traces DIV M) = (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) M) = (t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t traces P M))
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) M) =
(t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t traces (Pf a) M ∧ a ∈ X))
lemma in_traces_Ext_choice:
(t :t traces (P [+] Q) M) = (t :t traces P M ∨ t :t traces Q M)
lemma in_traces_Int_choice:
(t :t traces (P |~| Q) M) = (t :t traces P M ∨ t :t traces Q M)
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_sum:
(t :t traces (!! :C .. Pf) M) = (t = <> ∨ (∃c∈sumset C. t :t traces (Pf c) M))
lemma in_traces_Rep_int_choice_nat:
(t :t traces (!nat :N .. Pf) M) = (t = <> ∨ (∃n∈N. t :t traces (Pf n) M))
lemma in_traces_Rep_int_choice_set:
(t :t traces (!set :Xs .. Pf) M) = (t = <> ∨ (∃X∈Xs. t :t traces (Pf X) M))
lemma in_traces_Rep_int_choice_com:
(t :t traces (! :X .. Pf) M) = (t = <> ∨ (∃a∈X. t :t traces (Pf a) M))
lemma in_traces_Rep_int_choice_f:
inj f
==> (t :t traces (!<f> :X .. Pf) M) = (t = <> ∨ (∃a∈X. t :t traces (Pf a) M))
lemma in_traces_Rep_int_choice:
(t :t traces (!! :C .. Pf) M) = (t = <> ∨ (∃c∈sumset C. t :t traces (Pf c) M))
(t :t traces (!set :Xs .. Pf) M) = (t = <> ∨ (∃X∈Xs. t :t traces (Pf X) M))
(t :t traces (!nat :N .. Pf) M) = (t = <> ∨ (∃n∈N. t :t traces (Pf n) M))
(t :t traces (! :X .. Pf) M) = (t = <> ∨ (∃a∈X. t :t traces (Pf a) M))
inj f
==> (t :t traces (!<f> :X .. Pf) M) = (t = <> ∨ (∃a∈X. t :t traces (Pf a) M))
lemma in_traces_IF:
(t :t traces (IF b THEN P ELSE Q) M) =
(if b then t :t traces P M else t :t traces Q M)
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) M) =
(∃s t. u ∈ s |[X]|tr t ∧ s :t traces P M ∧ t :t traces Q M)
lemma Hiding_domT:
{s --tr X |s. s :t T} ∈ domT
lemma in_traces_Hiding:
(t :t traces (P -- X) M) = (∃s. t = s --tr X ∧ s :t traces P M)
lemma Renaming_domT:
{t. ∃s. s [[r]]* t ∧ s :t T} ∈ domT
lemma in_traces_Renaming:
(t :t traces (P [[r]]) M) = (∃s. s [[r]]* t ∧ s :t traces P M)
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) M) =
((∃s. u = rmTick s ∧ s :t traces P M) ∨
(∃s t. u = s ^^ t ∧ s ^^ <Tick> :t traces P M ∧ t :t traces Q M ∧ noTick s))
lemma in_traces_Depth_rest:
(t :t traces (P |. n) M) = (t :t traces P M ∧ lengtht t ≤ n)
lemma in_traces_Proc_name:
(t :t traces ($p) M) = (t :t M p)
lemma 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
lemma in_traces:
(t :t traces STOP M) = (t = <>)
(t :t traces SKIP M) = (t = <> ∨ t = <Tick>)
(t :t traces DIV M) = (t = <>)
(t :t traces (a -> P) M) = (t = <> ∨ (∃s. t = <Ev a> ^^ s ∧ s :t traces P M))
(t :t traces (? :X -> Pf) M) =
(t = <> ∨ (∃a s. t = <Ev a> ^^ s ∧ s :t traces (Pf a) M ∧ a ∈ X))
(t :t traces (P [+] Q) M) = (t :t traces P M ∨ t :t traces Q M)
(t :t traces (P |~| Q) M) = (t :t traces P M ∨ t :t traces Q M)
(t :t traces (!! :C .. Pf) M) = (t = <> ∨ (∃c∈sumset C. t :t traces (Pf c) M))
(t :t traces (!set :Xs .. Pf) M) = (t = <> ∨ (∃X∈Xs. t :t traces (Pf X) M))
(t :t traces (!nat :N .. Pf) M) = (t = <> ∨ (∃n∈N. t :t traces (Pf n) M))
(t :t traces (! :X .. Pf) M) = (t = <> ∨ (∃a∈X. t :t traces (Pf a) M))
inj f
==> (t :t traces (!<f> :X .. Pf) M) = (t = <> ∨ (∃a∈X. t :t traces (Pf a) M))
(t :t traces (IF b THEN P ELSE Q) M) =
(if b then t :t traces P M else t :t traces Q M)
(u :t traces (P |[X]| Q) M) =
(∃s t. u ∈ s |[X]|tr t ∧ s :t traces P M ∧ t :t traces Q M)
(t :t traces (P -- X) M) = (∃s. t = s --tr X ∧ s :t traces P M)
(t :t traces (P [[r]]) M) = (∃s. s [[r]]* t ∧ s :t traces P M)
(u :t traces (P ;; Q) M) =
((∃s. u = rmTick s ∧ s :t traces P M) ∨
(∃s t. u = s ^^ t ∧ s ^^ <Tick> :t traces P M ∧ t :t traces Q M ∧ 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) M) = (t :t traces P M ∧ lengtht t ≤ n)
(t :t traces ($p) M) = (t :t M p)
lemma in_traces_Timeout1:
(t :t traces (P [> Q) M) = (t :t traces P M ∨ t :t traces Q M)
lemma in_traces_Timeout2:
(t :t traces (P [>def Q) M) = (t :t traces P M ∨ t :t traces Q M)
lemma in_traces_Timeout:
(t :t traces (P [> Q) M) = (t :t traces P M ∨ t :t traces Q M)
(t :t traces (P [>def Q) M) = (t :t traces P M ∨ t :t traces Q M)