Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T
theory CSP_T_law_step (*-------------------------------------------*
| CSP-Prover on Isabelle2004 |
| December 2004 |
| June 2005 (modified) |
| September 2005 (modified) |
| |
| CSP-Prover on Isabelle2005 |
| October 2005 (modified) |
| April 2006 (modified) |
| March 2007 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_T_law_step
imports CSP_T_traces
begin
(*****************************************************************
1. step laws
2.
3.
4.
*****************************************************************)
(*********************************************************
stop expansion
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_STOP_step: "STOP =T[M1,M2] ? :{} -> Pf"
apply (simp add: cspT_semantics)
apply (simp add: traces_def)
done
(*********************************************************
Act_prefix expansion
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Act_prefix_step: "a -> P =T[M,M] ? x:{a} -> P"
apply (simp add: cspT_semantics)
apply (simp add: traces_def)
done
(*********************************************************
Ext choice expansion
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Ext_choice_step:
"(? :X -> Pf) [+] (? :Y -> Qf) =T[M,M]
? x:(X Un Y) ->
(IF (x : X & x : Y) THEN Pf x |~| Qf x
ELSE IF (x : X) THEN Pf x
ELSE Qf x)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
(* => *)
apply (rule)
apply (simp add: in_traces)
apply (elim disjE conjE exE)
apply (simp_all)
apply (rule_tac x="a" in exI)
apply (rule_tac x="s" in exI)
apply (simp)
apply (rule_tac x="a" in exI)
apply (rule_tac x="s" in exI)
apply (simp)
(* <= *)
apply (rule)
apply (simp add: in_traces)
apply (elim disjE conjE exE)
apply (simp_all)
apply (case_tac "a : Y")
apply (simp_all add: in_traces)
apply (case_tac "a : X")
apply (simp_all add: in_traces)
done
(*********************************************************
Parallel expansion
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Parallel_step:
"(? :Y -> Pf) |[X]| (? :Z -> Qf) =T[M,M]
? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ? x:Z -> Qf x)
|~| (? x:Y -> Pf x |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| ? x:Z -> Qf x)
ELSE (? x:Y -> Pf x |[X]| Qf x)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
(* => *)
apply (rule)
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="t" in spec)
apply (elim disjE conjE exE)
(* <> *)
apply (simp)
(* [Tick]t *)
apply (simp add: in_traces)
(* [Ev .]t *)
apply (simp add: in_traces)
apply (elim disjE conjE exE)
(* 1 *)
apply (simp)
(* 2 *)
apply (simp add: par_tr_head)
apply (elim conjE exE)
apply (case_tac "a : Y")
apply (simp)
apply (rule disjI2)
apply (rule_tac x="<>" in exI)
apply (rule_tac x="sb" in exI)
apply (simp)
(* a ~: Y *)
apply (simp)
apply (rule_tac x="<>" in exI)
apply (rule_tac x="sb" in exI)
apply (simp)
(* 3 *)
apply (simp add: par_tr_head)
apply (elim conjE exE)
apply (case_tac "a : Z")
apply (simp)
apply (rule disjI1)
apply (rule_tac x="sb" in exI)
apply (rule_tac x="<>" in exI)
apply (simp)
(* a ~: Z *)
apply (simp)
apply (rule_tac x="sb" in exI)
apply (rule_tac x="<>" in exI)
apply (simp)
(* 4 *)
apply (simp add: par_tr_head)
apply (elim disjE conjE exE)
(* 4-1 *)
apply (simp)
apply (rule_tac x="sb" in exI)
apply (rule_tac x="sc" in exI)
apply (simp)
(* 4-2 *)
apply (case_tac "a : Z")
apply (simp)
apply (rule disjI1)
apply (rule_tac x="sb" in exI)
apply (rule_tac x="<Ev ab> ^^ sc" in exI)
apply (simp)
(* a ~: Z *)
apply (simp)
apply (rule_tac x="sb" in exI)
apply (rule_tac x="<Ev ab> ^^ sc" in exI)
apply (simp)
(* 4-3 *)
apply (simp)
apply (case_tac "a : Y")
apply (simp)
apply (rule disjI2)
apply (rule_tac x="<Ev aa> ^^ sb" in exI)
apply (rule_tac x="sc" in exI)
apply (simp)
(* a ~: Y *)
apply (simp)
apply (rule_tac x="<Ev aa> ^^ sb" in exI)
apply (rule_tac x="sc" in exI)
apply (simp)
(* <= *)
apply (rule)+
apply (drule_tac x="t" in spec)
apply (elim disjE conjE exE)
(* <> *)
apply (simp)
(* [Tick]t *)
apply (simp add: in_traces)
(* [Ev .]t *)
apply (simp add: in_traces)
apply (elim disjE conjE exE)
(* 1 *)
apply (simp add: in_traces)
apply (elim conjE exE)
apply (rule_tac x="<Ev a> ^^ sa" in exI)
apply (rule_tac x="<Ev a> ^^ ta" in exI)
apply (simp add: par_tr_head)
(* 2 *)
apply (simp add: in_traces)
apply (case_tac "a : Z")
apply (simp add: in_traces)
apply (erule disjE)
apply (elim conjE exE)
apply (rule_tac x="<Ev a> ^^ sa" in exI)
apply (rule_tac x="ta" in exI)
apply (simp add: par_tr_head)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (rule_tac x="<Ev a> ^^ ta" in exI)
apply (simp add: par_tr_head)
(* 3 *)
apply (simp add: in_traces)
apply (elim conjE exE)
apply (rule_tac x="<Ev a> ^^ sa" in exI)
apply (rule_tac x="ta" in exI)
apply (simp add: par_tr_head)
apply (simp add: in_traces)
apply (case_tac "a : Y")
apply (simp add: in_traces)
apply (erule disjE)
apply (elim conjE exE)
apply (rule_tac x="<Ev a> ^^ sa" in exI)
apply (rule_tac x="ta" in exI)
apply (simp add: par_tr_head)
(* *)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (rule_tac x="<Ev a> ^^ ta" in exI)
apply (simp add: par_tr_head)
apply (simp add: in_traces)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (rule_tac x="<Ev a> ^^ ta" in exI)
apply (simp add: par_tr_head)
done
(*********************************************************
Hide expansion
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Hiding_step:
"(? :Y -> Pf) -- X =T[M,M]
IF (Y Int X = {}) THEN (? x:Y -> (Pf x -- X))
ELSE ((? x:(Y-X) -> (Pf x -- X))
[> (! x:(Y Int X) .. (Pf x -- X)))"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
(* => *)
apply (rule)
apply (simp add: in_traces)
apply (elim conjE exE)
apply (erule disjE, simp)
apply (elim conjE exE)
apply (case_tac "Y Int X = {}")
apply (simp)
apply (case_tac "a : X", fast)
apply (simp)
apply (rule_tac x="sa" in exI)
apply (simp)
(* Y Int X ~= {} *)
apply (simp)
apply (case_tac "a : X")
apply (simp)
apply (fast)
(* a ~: X *)
apply (simp)
apply (fast)
(* <= *)
apply (rule)
apply (case_tac "Y Int X = {}")
apply (simp add: in_traces)
apply (erule disjE, simp)
apply (rule_tac x="<>" in exI)
apply (simp)
apply (elim conjE exE)
apply (case_tac "a : X", fast)
apply (rule_tac x="<Ev a> ^^ sa" in exI)
apply (simp)
(* Y Int X = {} *)
apply (simp add: in_traces)
apply (erule disjE, simp)
apply (rule_tac x="<>" in exI)
apply (simp)
apply (erule disjE)
(* a~:X *)
apply (elim conjE exE)
apply (rule_tac x="<Ev a> ^^ sa" in exI)
apply (simp)
(* a:X *)
apply (erule disjE, simp)
apply (rule_tac x="<>" in exI)
apply (simp)
apply (elim conjE exE bexE)
apply (rule_tac x="<Ev a> ^^ s" in exI)
apply (simp)
done
(*********************************************************
Renaming expansion
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Renaming_step:
"(? :X -> Pf) [[r]] =T[M,M]
? y:(r `` X) -> (! x:{x. x:X & (x,y):r} .. (Pf x)[[r]])"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
(* => *)
apply (rule)
apply (simp add: in_traces)
apply (elim disjE conjE exE)
(* 1 *)
apply (simp)
(* 2 *)
apply (rule disjI2)
apply (simp add: ren_tr_decompo)
apply (elim conjE exE)
apply (rule_tac x="b" in exI)
apply (rule_tac x="ta" in exI)
apply (simp)
apply (fast)
(* <= *)
apply (rule)
apply (simp add: in_traces)
apply (erule disjE, simp)
apply (elim disjE conjE exE)
apply (simp add: Image_iff)
apply (erule bexE)
apply (rule_tac x="<Ev x>" in exI)
apply (simp)
(* *)
apply (rule_tac x="<Ev aa> ^^ sa" in exI)
apply (simp)
done
(*********************************************************
Sequential composition expansion
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Seq_compo_step:
"(? :X -> Pf) ;; Q =T[M,M] ? x:X -> (Pf x ;; Q)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
(* => *)
apply (rule)
apply (simp add: in_traces)
apply (elim conjE exE disjE)
apply (simp_all)
(* 1 *)
apply (fast)
(* 2 *)
apply (insert trace_last_nil_or_unnil)
apply (drule_tac x="sa" in spec)
apply (erule disjE, simp)
apply (elim conjE exE, simp)
apply (simp add: appt_assoc_sym)
apply (rule_tac x="a" in exI)
apply (rule_tac x="sb ^^ ta" in exI)
apply (simp add: appt_assoc)
apply (fast)
(* <= *)
apply (rule)
apply (simp add: in_traces)
apply (erule disjE, simp)
apply (rule disjI1)
apply (rule_tac x="<>" in exI)
apply (simp)
apply (elim disjE conjE exE)
(* 1 *)
apply (rule disjI1)
apply (rule_tac x="<Ev a> ^^ sa" in exI, simp)
(* 2 *)
apply (rule disjI2)
apply (rule_tac x="<Ev a> ^^ sa" in exI)
apply (rule_tac x="ta" in exI)
apply (simp add: appt_assoc)
done
(*********************************************************
Depth_rest expansion
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Depth_rest_step:
"(? :X -> Pf) |. (Suc n) =T[M,M] ? x:X -> (Pf x |. n)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
(* => *)
apply (rule)
apply (simp add: in_traces)
apply (elim disjE conjE exE)
apply (simp_all)
(* <= *)
apply (rule)
apply (simp add: in_traces)
apply (elim disjE conjE exE)
apply (simp_all)
done
(*********************************************************)
lemmas cspT_step = cspT_STOP_step cspT_Act_prefix_step
cspT_Ext_choice_step cspT_Parallel_step
cspT_Hiding_step cspT_Renaming_step
cspT_Seq_compo_step cspT_Depth_rest_step
lemmas cspT_light_step = cspT_STOP_step cspT_Act_prefix_step
end
lemma cspT_STOP_step:
STOP =T[M1.0,M2.0] ? :{} -> Pf
lemma cspT_Act_prefix_step:
a -> P =T[M,M] ? x:{a} -> P
lemma cspT_Ext_choice_step:
? :X -> Pf [+] ? :Y -> Qf =T[M,M] ? x:(X ∪ Y) -> IF (x ∈ X ∧ x ∈ Y) THEN Pf x |~| Qf x ELSE IF (x ∈ X) THEN Pf x ELSE Qf x
lemma cspT_Parallel_step:
? :Y -> Pf |[X]| ? :Z -> Qf =T[M,M] ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) -> IF (x ∈ X) THEN Pf x |[X]| Qf x ELSE IF (x ∈ Y ∧ x ∈ Z) THEN Pf x |[X]| ? :Z -> Qf |~| ? :Y -> Pf |[X]| Qf x ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf ELSE ? :Y -> Pf |[X]| Qf x
lemma cspT_Hiding_step:
(? :Y -> Pf) -- X =T[M,M] IF (Y ∩ X = {}) THEN ? x:Y -> Pf x -- X ELSE ? x:(Y - X) -> Pf x -- X [> (! x:(Y ∩ X) .. Pf x -- X)
lemma cspT_Renaming_step:
(? :X -> Pf) [[r]] =T[M,M] ? y:(r `` X) -> (! x:{x : X. (x, y) ∈ r} .. Pf x [[r]])
lemma cspT_Seq_compo_step:
? :X -> Pf ;; Q =T[M,M] ? x:X -> (Pf x ;; Q)
lemma cspT_Depth_rest_step:
(? :X -> Pf) |. Suc n =T[M,M] ? x:X -> Pf x |. n
lemmas cspT_step:
STOP =T[M1.0,M2.0] ? :{} -> Pf
a -> P =T[M,M] ? x:{a} -> P
? :X -> Pf [+] ? :Y -> Qf =T[M,M] ? x:(X ∪ Y) -> IF (x ∈ X ∧ x ∈ Y) THEN Pf x |~| Qf x ELSE IF (x ∈ X) THEN Pf x ELSE Qf x
? :Y -> Pf |[X]| ? :Z -> Qf =T[M,M] ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) -> IF (x ∈ X) THEN Pf x |[X]| Qf x ELSE IF (x ∈ Y ∧ x ∈ Z) THEN Pf x |[X]| ? :Z -> Qf |~| ? :Y -> Pf |[X]| Qf x ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf ELSE ? :Y -> Pf |[X]| Qf x
(? :Y -> Pf) -- X =T[M,M] IF (Y ∩ X = {}) THEN ? x:Y -> Pf x -- X ELSE ? x:(Y - X) -> Pf x -- X [> (! x:(Y ∩ X) .. Pf x -- X)
(? :X -> Pf) [[r]] =T[M,M] ? y:(r `` X) -> (! x:{x : X. (x, y) ∈ r} .. Pf x [[r]])
? :X -> Pf ;; Q =T[M,M] ? x:X -> (Pf x ;; Q)
(? :X -> Pf) |. Suc n =T[M,M] ? x:X -> Pf x |. n
lemmas cspT_step:
STOP =T[M1.0,M2.0] ? :{} -> Pf
a -> P =T[M,M] ? x:{a} -> P
? :X -> Pf [+] ? :Y -> Qf =T[M,M] ? x:(X ∪ Y) -> IF (x ∈ X ∧ x ∈ Y) THEN Pf x |~| Qf x ELSE IF (x ∈ X) THEN Pf x ELSE Qf x
? :Y -> Pf |[X]| ? :Z -> Qf =T[M,M] ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) -> IF (x ∈ X) THEN Pf x |[X]| Qf x ELSE IF (x ∈ Y ∧ x ∈ Z) THEN Pf x |[X]| ? :Z -> Qf |~| ? :Y -> Pf |[X]| Qf x ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf ELSE ? :Y -> Pf |[X]| Qf x
(? :Y -> Pf) -- X =T[M,M] IF (Y ∩ X = {}) THEN ? x:Y -> Pf x -- X ELSE ? x:(Y - X) -> Pf x -- X [> (! x:(Y ∩ X) .. Pf x -- X)
(? :X -> Pf) [[r]] =T[M,M] ? y:(r `` X) -> (! x:{x : X. (x, y) ∈ r} .. Pf x [[r]])
? :X -> Pf ;; Q =T[M,M] ? x:X -> (Pf x ;; Q)
(? :X -> Pf) |. Suc n =T[M,M] ? x:X -> Pf x |. n
lemmas cspT_light_step:
STOP =T[M1.0,M2.0] ? :{} -> Pf
a -> P =T[M,M] ? x:{a} -> P
lemmas cspT_light_step:
STOP =T[M1.0,M2.0] ? :{} -> Pf
a -> P =T[M,M] ? x:{a} -> P