Up to index of Isabelle/HOL/CSP/CSP_T/CSP_F/DFP
theory DFP_Network(*-------------------------------------------* | DFP package | | June 2005 | | December 2005 (modified) | | | | DFP on CSP-Prover ver.3.0 | | September 2006 (modified) | | April 2007 (modified) | | | | Yoshinao Isobe (AIST JAPAN) | *-------------------------------------------*) theory DFP_Network imports DFP_subseteqEX begin (* The following simplification rules are deleted in this theory file *) (* because they unexpectly rewrite UnionT and InterT. *) (* Union (B ` A) = (UN x:A. B x) *) (* Inter (B ` A) = (INT x:A. B x) *) declare Union_image_eq [simp del] declare Inter_image_eq [simp del] (* The following simplification rules are deleted in this theory file *) (* because they unexpectly rewrite (notick | t = []t) *) (* *) (* disj_not1: (~ P | Q) = (P --> Q) *) declare disj_not1 [simp del] (***************************************************************** 1. 2. 3. 4. *****************************************************************) (********************************************************* definitions *********************************************************) (*** network ***) types ('i,'p,'a) Network = "('i set * ('i => (('p,'a) proc * 'a set)))" consts PAR :: "('i,'p,'a) Network => ('p,'a) proc" ("(1PAR _)" [77] 77) defs PAR_def : "PAR V == [||]i:(fst V) .. ((snd V) i)" syntax "@Network" :: "(('p,'a) proc * 'a set) => pttrn => 'i set => ('i,'p,'a) Network" ("(1{ _ | /_:_ }net)" [77,900,90] 900) translations "{ PX | i:I }net" == "(I, (%i. PX))" (*** failure set of network ***) types ('i,'a) NetworkF = "('i set * ('i => (('a failure set) * 'a set)))" syntax "@NetworkF" :: "(('a failure set) * 'a set) => pttrn => 'i set => ('i,'a) NetworkF" ("(1{ _ | /_:_ }Fnet)" [77,900,90] 900) translations "{ FX | i:I }Fnet" == "(I, (%i. FX))" (*** Network and NetworkF ***) syntax "@Network_pro" :: "('i set * ('i => ('b * 'a set))) => 'i => 'b" ("netElement _<_>" [900,0] 1000) "@Network_alp" :: "('i set * ('i => ('b * 'a set))) => 'i => 'a set" ("netAlpha _<_>" [900,0] 1000) translations "netElement V<i>" == "fst ((snd V) i)" "netAlpha V<i>" == "snd ((snd V) i)" consts isFailureOf :: "('i,'a) NetworkF => ('i,'p,'a) Network => bool" ("(1_ /isFailureOf /_)" [55,55] 55) defs isFailureOf_def : "VF isFailureOf V == fst V = fst VF & (ALL i : fst VF. fst (snd VF i) <=EX failures (fst (snd V i)) MF restRefusal (Ev ` snd (snd VF i)) & snd (snd V i) = snd (snd VF i))" (*** short notations ***) consts ALP :: "('i set * ('i => ('b * 'a set))) => 'a set" defs ALP_def : "ALP V == {a. EX i:(fst V). a : snd((snd V) i)}" (*** state ***) types ('i,'a) net_state = "('a trace * ('i => 'a event set))" consts isStateOf :: "('i,'a) net_state => ('i,'a) NetworkF => bool" ("(1_ /isStateOf /_)" [55,55] 55) defs isStateOf_def : "sigma isStateOf VF == sett(fst sigma) <= Ev ` (ALP VF) & (ALL i: fst VF. (fst sigma rest-tr snd ((snd VF) i), (snd sigma) i) : fst ((snd VF) i) & (snd sigma) i <= Ev ` snd ((snd VF) i))" (********************************************************* small lemmas *********************************************************) lemma decompo_V: "EX I PXf. (V::('i,'p,'a) Network) = (I,PXf)" apply (rule_tac x="fst V" in exI) apply (rule_tac x="snd V" in exI) by (simp) lemma isFailureOf_subset_index: "[| (I, FXf) isFailureOf (I, PXf) ; J <= I |] ==> (J, FXf) isFailureOf (J, PXf)" apply (simp add: isFailureOf_def) by (auto) lemma isFailureOf_subset_alpha1: "[| (I, FXf) isFailureOf (I, PXf) ; i : I ; (s, Y) : fst (FXf i) ; e : Y |] ==> e : Ev ` snd (PXf i)" apply (simp add: isFailureOf_def) apply (drule_tac x="i" in bspec, simp) apply (simp add: subseteqEX_def restRefusal_def) apply (auto) done lemma isFailureOf_subset_alpha2: "[| (I, FXf) isFailureOf (I, PXf) ; i : I ; (s, Y) : fst (FXf i) ; e : Y |] ==> e : Ev ` snd (FXf i)" apply (simp add: isFailureOf_def) apply (drule_tac x="i" in bspec, simp) apply (simp add: subseteqEX_def restRefusal_def) apply (auto) done lemmas isFailureOf_subset_alpha = isFailureOf_subset_alpha1 isFailureOf_subset_alpha2 lemma isFailureOf_not_Tick[simp]: "[| (I, FXf) isFailureOf (I, PXf) ; i : I ; (s, Y) : fst (FXf i) |] ==> Tick ~: Y" apply (simp add: isFailureOf_def) apply (drule_tac x="i" in bspec, simp) apply (simp add: subseteqEX_def restRefusal_def) apply (auto) done lemma isFailureOf_same_alpha: "(I, FXf) isFailureOf (I, PXf) ==> ALL i:I. snd (PXf i) = snd (FXf i)" by (simp add: isFailureOf_def) (********************************************************* StateOf subset *********************************************************) lemma isStateOf_subset_alpha1: "[| (I, FXf) isFailureOf (I, PXf) ; (t, Yf) isStateOf (I, FXf) ; i : I ; e : Yf i|] ==> e : (Ev ` (snd (PXf i)))" apply (simp add: isStateOf_def) apply (auto simp add: isFailureOf_same_alpha) done lemma isStateOf_subset_alpha2: "[| (I, FXf) isFailureOf (I, PXf) ; (t, Yf) isStateOf (I, FXf) ; i : I ; e : Yf i|] ==> e : (Ev ` (snd (FXf i)))" apply (simp add: isStateOf_def) apply (auto) done lemmas isStateOf_subset_alpha = isStateOf_subset_alpha1 isStateOf_subset_alpha2 lemma isStateOf_each_element: "[| (t, Yf) isStateOf (I, FXf) ; i : I |] ==> (t rest-tr snd (FXf i), Yf) isStateOf ({i}, FXf)" apply (simp add: isStateOf_def) apply (rule conjI) apply (simp add: ALP_def) apply (case_tac "Tick : sett t") apply (force) apply (subgoal_tac "sett (t rest-tr snd (FXf i)) <= sett (t rest-tr UNIV)") apply (case_tac "Tick : sett (t rest-tr snd (FXf i))", simp) apply (insert rest_tr_subset_event[of t "snd (FXf i)"]) apply (blast) apply (rule rest_tr_sett_subseteq_sett) apply (simp) apply (simp add: rest_tr_of_rest_tr_subset) done (********************************************************* PAR *********************************************************) (*---------------------------------* | flattening | *---------------------------------*) (*** SF ***) (* lemmas *) lemma domSF_PAR_flattening_lm1: "ALP (V x) = Union (snd ` (%(i, j). snd (V j) i) ` {(i, x) |i. i : fst (V x)})" by (auto simp add: ALP_def) lemma domSF_PAR_flattening_lm2: "Union (snd ` (%i. ([||]:(fst (V i)) (snd (V i)), ALP (V i))) ` F) = Union (snd ` (%(i, j). snd (V j) i) ` {(i, j). j : F & i : fst (V j)})" apply (auto simp add: ALP_def) apply (rule_tac x="ia" in exI) apply (rule_tac x="i" in exI) apply (simp) apply (rule_tac x="ba" in bexI) apply (rule_tac x="aa" in bexI) apply (simp_all) done (* main *) (*------------------* | csp law | *------------------*) lemma cspF_PAR_flattening: "[| finite J ; ALL j:J. finite (fst (V j)) |] ==> (PAR { (PAR (V j), ALP (V j)) | j:J }net) =F[M,M] (PAR { ((snd (V j)) i) | (i,j):{(i, j). j : J & i : fst (V j)}}net)" (* apply (induct set: Finites) Isabelle 2005 *) apply (induct set: finite) (* Isabelle 2007 *) (* base *) apply (simp add: PAR_def) (* step *) apply (simp add: PAR_def) apply (rule cspF_rw_left) apply (rule cspF_Rep_parallel_induct) apply (simp_all) apply (rule cspF_rw_left) apply (rule cspF_Alpha_parallel_cong) apply (simp) apply (simp) apply (rule cspF_reflex) apply (subgoal_tac "[||] i:F .. ([||]:(fst (V i)) (snd (V i)), ALP (V i)) =F[M,M] [||] (i, j):{(i, j). j : F & i : (fst (V j))} .. (snd (V j)) i") (* ... sub 1 *) apply (simp) (* sub 1 *) apply (simp add: eqF_semF[THEN sym]) apply (subgoal_tac "{(i, j). (j = x | j : F) & i : fst (V j)} = {(i,x) |i. i : fst (V x)} Un {(i, j). j : F & i : fst (V j)}") (* ... sub 2 *) apply (simp) apply (subgoal_tac "finite {(i, x)|i. i : fst (V x)}") (* ... sub 3 *) apply (subgoal_tac "finite {(i, j). j : F & i : fst (V j)}") (* ... sub 4 *) apply (rule cspF_rw_right) apply (rule cspF_Rep_parallel_assoc) apply (force) apply (simp)+ apply (rule cspF_Alpha_parallel_cong) apply (simp add: domSF_PAR_flattening_lm1) apply (simp add: domSF_PAR_flattening_lm2) apply (rule cspF_Rep_parallel_index_eq) apply (simp) apply (rule_tac x="(%i. (i, x))" in exI) apply (simp) apply (simp add: inj_on_def) apply (force) apply (simp) (* sub 4 *) apply (simp add: finite_pair_set) (* sub 3 *) apply (subgoal_tac "{(i, x) |i. i : fst (V x)} = (%i. (i,x)) ` (fst (V x))") apply (force) apply (force) (* sub 2 *) apply (force) done (*** T and F ***) lemma traces_PAR_flattening: "[| finite J ; ALL j:J. finite (fst (V j)) |] ==> traces (PAR { (PAR (V j), ALP (V j)) | j:J }net) M = traces (PAR { ((snd (V j)) i) | (i,j):{(i, j). j : J & i : fst (V j)} }net) M" apply (insert cspF_PAR_flattening[of J V "(%p. (M p,,maxFof (M p)))"]) apply (simp add: cspF_eqF_semantics) apply (subgoal_tac "(fstF o (%p. (M p ,, maxFof (M p)))) = M") apply (simp) apply (simp add: expand_fun_eq) apply (rule allI) apply (simp add: maxFof_domF pairF_fstF) done lemma failures_PAR_flattening: "[| finite J ; ALL j:J. finite (fst (V j)) |] ==> failures (PAR { (PAR (V j), ALP (V j)) | j:J }net) M = failures (PAR { ((snd (V j)) i) | (i,j):{(i, j). j : J & i : fst (V j)} }net) M" apply (insert cspF_PAR_flattening[of J V M]) apply (simp add: cspF_eqF_semantics) done (********************************************************* sub network *********************************************************) (*** state ***) lemma isStateOf_subset: "[| (t,Yf) isStateOf (I,FXf) ; J <= I ; X = {sY. EX i:J. sY : snd (FXf i)} |] ==> (t rest-tr X, Yf) isStateOf (J, FXf)" apply (simp add: isStateOf_def ALP_def) apply (rule conjI) apply (insert rest_tr_subset_event[of t "X"]) apply (subgoal_tac "Tick ~: sett (t rest-tr X)") apply (blast) apply (force) apply (rule ballI) apply (elim conjE) apply (drule_tac x="i" in bspec, fast) apply (subgoal_tac "snd (FXf i) <= {sY. EX i:J. sY : snd (FXf i)}") apply (simp add: rest_tr_of_rest_tr_subset) by (auto) lemma isStateOf_subsetI: "[| (t,Yf) isStateOf (I,FXf) ; J <= I ; X = Union {(snd (FXf i))|i. i:J} |] ==> (t rest-tr X, Yf) isStateOf (J, FXf)" apply (subgoal_tac "Union {(snd (FXf i))|i. i:J} = {sY. EX i:J. sY : snd (FXf i)}") apply (simp add: isStateOf_subset) by (auto) (********************************************************* isFailureOf *********************************************************) lemma isFailureOf_largest: "{ ({(s,Y Int (Ev ` snd (PXf i)))|s Y. (s,Y) :f failures (fst (PXf i)) MF}, snd (PXf i)) | i:I }Fnet isFailureOf (I, PXf)" apply (simp add: isFailureOf_def) apply (simp add: subseteqEX_Int) done lemma isFailureOf_EX: "EX VF. VF isFailureOf V" apply (rule_tac x= "{ ({(s,Y Int (Ev ` snd ((snd V) i))) |s Y. (s,Y) :f failures (fst ((snd V) i)) MF}, snd ((snd V) i)) | i: fst V }Fnet" in exI) apply (insert decompo_V[of V]) apply (elim exE) apply (simp add: isFailureOf_largest) done (****************** to add it again ******************) declare disj_not1 [simp] declare Union_image_eq [simp] declare Inter_image_eq [simp] end