Up to index of Isabelle/HOL/CSP/CSP_T/CSP_F/DFP
theory DFP_Block(*-------------------------------------------* | DFP package | | May 2005 | | December 2005 (modified) | | | | DFP on CSP-Prover ver.3.0 | | September 2006 (modified) | | April 2007 (modified) | | | | Yoshinao Isobe (AIST JAPAN) | *-------------------------------------------*) theory DFP_Block imports DFP_Deadlock 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 *********************************************************) consts triple_disjoint :: "('i,'a) NetworkF => bool" defs triple_disjoint_def : "triple_disjoint VF == (ALL i: fst VF. ALL j: fst VF. ALL k: fst VF. i ~= j & j ~= k & k ~= i --> (snd ((snd VF) i) Int snd ((snd VF) j) Int snd ((snd VF) k) = {}))" consts VocabularyOf :: "('i,'a) NetworkF => 'a set" BusyNetworkP :: "('i,'p,'a) Network => bool" BusyNetwork :: "('i,'a) NetworkF => bool" defs VocabularyOf_def : "VocabularyOf VF == Union {X. EX i: fst VF. EX j: fst VF. i ~= j & X = snd((snd VF) i) Int snd((snd VF) j)}" (* internal communication *) BusyNetworkP_def : "BusyNetworkP V == ALL i: fst V. DeadlockFreeNetwork ({i}, snd V)" BusyNetwork_def : "BusyNetwork VF == ALL i: fst VF. (ALL sigma. ~(sigma isDeadlockStateOf ({i}, snd VF)))" consts isRequestOf :: "('i,'a) NetworkF => 'i => ('i,'a) net_state => 'i => bool" ("(1_ >> /(0_ (1/--[_]-->) /_))" [800, 800,100,800] 900) isStrongRequestOf :: "('i,'a) NetworkF => 'i => ('i,'a) net_state => 'i => bool" ("(1_ >> /(0_ (1/==[_]==>) /_))" [800, 800,100,800] 900) defs isRequestOf_def : "VF >> i --[sigma]--> j == sigma isStateOf VF & i ~= j & i : fst VF & j : fst VF & (Ev ` (snd (snd VF i)) - (snd sigma) i) Int Ev ` (snd (snd VF j)) ~= {}" isStrongRequestOf_def : "VF >> i ==[sigma]==> j == sigma isStateOf VF & i ~= j & i : fst VF & j : fst VF & Ev ` (snd (snd VF i)) - (snd sigma) i ~= {} & Ev ` (snd (snd VF i)) - (snd sigma) i <= Ev ` (snd (snd VF j))" consts isUngrantedRequestOf :: "('i,'a) NetworkF => 'i => ('i,'a) net_state => 'i => bool" ("(1_ >> /(0_ (1/--[_]-->o) /_))" [800, 800,0,800] 900) isUngrantedStrongRequestOf :: "('i,'a) NetworkF => 'i => ('i,'a) net_state => 'i => bool" ("(1_ >> /(0_ (1/==[_]==>o) /_))" [800, 800,0,800] 900) defs isUngrantedRequestOf_def : "VF >> i --[sigma]-->o j == VF >> i --[sigma]--> j & Ev ` (snd (snd VF i)) Int Ev ` (snd (snd VF j)) <= (snd sigma) i Un (snd sigma) j" isUngrantedStrongRequestOf_def : "VF >> i ==[sigma]==>o j == VF >> i ==[sigma]==> j & Ev ` (snd (snd VF i)) Int Ev ` (snd (snd VF j)) <= (snd sigma) i Un (snd sigma) j" consts isUngrantedRequestOfwrt :: "('i,'a) NetworkF => 'i => ('i,'a) net_state => 'a set => 'i => bool" ("(1_ >> /(0_ (1/--[(0_,/_)]-->o) /_))" [800, 800,0,0,800] 900) defs isUngrantedRequestOfwrt_def : "VF >> i --[sigma,Lambda]-->o j == VF >> i --[sigma]-->o j & ((Ev ` (snd (snd VF i))) - (snd sigma) i) Un ((Ev ` (snd (snd VF j))) - (snd sigma) j) <= Ev ` Lambda" (*** Block ***) consts isBlockedIn :: "('i,'a) NetworkF => 'i => ('i,'a) net_state => bool" ("(_ >> _ isBlockedIn _)" [800, 800, 800] 900) defs isBlockedIn_def : "VF >> i isBlockedIn sigma == triple_disjoint VF & (EX j. VF >> i --[sigma]--> j) & (ALL j. VF >> i --[sigma]--> j --> (VF >> i --[sigma, (VocabularyOf VF)]-->o j))" (********************************************************* BusyNetwork lemmas *********************************************************) lemma BusyNetwork_BusyNetworkP : "[| I ~= {} ; finite I ; (I,FXf) isFailureOf (I,PXf) |] ==> BusyNetwork (I,FXf) = BusyNetworkP (I,PXf)" apply (simp add: BusyNetwork_def) apply (simp add: BusyNetworkP_def) apply (rule) apply (rule ballI) apply (drule_tac x="i" in bspec, simp) apply (subgoal_tac "({i}, FXf) isFailureOf ({i}, PXf)") apply (simp add: DeadlockFree_notDeadlockState) apply (rule isFailureOf_subset_index) apply (simp) apply (simp) apply (rule ballI) apply (drule_tac x="i" in bspec, simp) apply (subgoal_tac "({i}, FXf) isFailureOf ({i}, PXf)") apply (simp add: DeadlockFree_notDeadlockState) apply (rule isFailureOf_subset_index) apply (simp) apply (simp) done (*-----------------------------------* | How to check BusyNetworkF | *-----------------------------------*) lemma check_BusyNetwork: "[| ALL i:I. ALL s Y. (s, Y) : fst (FXf i) --> Y ~= Ev ` (snd (FXf i)) |] ==> BusyNetwork (I,FXf)" apply (simp add: BusyNetwork_def) apply (intro allI ballI) apply (rename_tac s Yf) apply (drule_tac x="i" in bspec, simp) apply (simp add: isDeadlockStateOf_def) apply (simp add: disj_not1) apply (intro impI) apply (simp add: isStateOf_def) apply (drule_tac x="s rest-tr (snd (FXf i))" in spec) apply (drule_tac x="Yf i" in spec) apply (simp) apply (simp add: ALP_def) done (********************************************************* in index I *********************************************************) lemma in_index_I1: "(I, FXf) >> i --[sigma]--> j ==> i : I & j : I & i ~= j" by (simp add: isRequestOf_def) lemma in_index_I2: "(I, FXf) >> i ==[sigma]==> j ==> i : I & j : I & i ~= j" by (simp add: isStrongRequestOf_def) lemma in_index_I3: "(I, FXf) >> i --[sigma]-->o j ==> i : I & j : I & i ~= j" apply (simp add: isUngrantedRequestOf_def) apply (elim conjE) by (simp add: in_index_I1) lemma in_index_I4: "(I, FXf) >> i ==[sigma]==>o j ==> i : I & j : I & i ~= j" apply (simp add: isUngrantedStrongRequestOf_def) apply (elim conjE) by (simp add: in_index_I2) lemma in_index_I5: "(I, FXf) >> i --[sigma,Lambda]-->o j ==> i : I & j : I & i ~= j" apply (simp add: isUngrantedRequestOfwrt_def) apply (elim conjE) by (simp add: in_index_I3) lemmas in_index_I = in_index_I1 in_index_I2 in_index_I3 in_index_I4 in_index_I5 (********************************************************* note (P.7) *********************************************************) lemma isUngrantedRequestOfwrt_note1: "[| Lambda1 <= Lambda2 ; VF >> i --[sigma,Lambda1]-->o j |] ==> VF >> i --[sigma,Lambda2]-->o j" apply (simp add: isUngrantedRequestOfwrt_def) by (blast) lemma isUngrantedRequestOfwrt_note2: "(snd (snd VF i)) Un (snd (snd VF j)) <= Lambda ==> (VF >> i --[sigma,Lambda]-->o j) = (VF >> i --[sigma]-->o j)" by (auto simp add: isUngrantedRequestOfwrt_def) (********************************************************* sub request *********************************************************) lemma isRequestOf_subsetI: "[| (I, FXf) >> i --[(t,Yf)]--> j; J <= I; i:J ; j:J ; X = Union {snd (FXf i)|i. i:J} |] ==> (J, FXf) >> i --[(t rest-tr X,Yf)]--> j" apply (simp add: isRequestOf_def) apply (rule isStateOf_subsetI) apply (simp_all) done lemma isStrongRequestOf_subsetI: "[| (I, FXf) >> i ==[(t,Yf)]==> j; J <= I; i:J ; j:J ; X = Union {snd (FXf i)|i. i:J} |] ==> (J, FXf) >> i ==[(t rest-tr X,Yf)]==> j" apply (simp add: isStrongRequestOf_def) apply (rule isStateOf_subsetI) apply (simp_all) done lemma isUngrantedRequestOf_subsetI: "[| (I, FXf) >> i --[(t,Yf)]-->o j; J <= I; i:J ; j:J ; X = Union {snd (FXf i)|i. i:J} |] ==> (J, FXf) >> i --[(t rest-tr X,Yf)]-->o j" apply (simp add: isUngrantedRequestOf_def) apply (rule isRequestOf_subsetI) apply (simp_all) done lemma isUngrantedStrongRequestOf_subsetI: "[| (I, FXf) >> i ==[(t,Yf)]==>o j; J <= I; i:J ; j:J ; X = Union {snd (FXf i)|i. i:J} |] ==> (J, FXf) >> i ==[(t rest-tr X,Yf)]==>o j" apply (simp add: isUngrantedStrongRequestOf_def) apply (rule isStrongRequestOf_subsetI) apply (simp_all) done lemma isUngrantedRequestOfwrt_subsetI: "[| (I, FXf) >> i --[(t,Yf), Lambda1]-->o j; J <= I; i:J ; j:J ; Lambda1 <= Lambda2 ; X = Union {snd (FXf i)|i. i:J} |] ==> (J, FXf) >> i --[(t rest-tr X,Yf), Lambda2]-->o j" apply (simp add: isUngrantedRequestOfwrt_def) apply (rule conjI) apply (rule isUngrantedRequestOf_subsetI) apply (simp_all) apply (blast) done (********************************************************* blocked *********************************************************) (*---------------------------------* | lemma 1 [Roscoe_Dathi_1987 P.7] | *---------------------------------*) (*** only if ***) lemma Lemma1_Roscoe_Dathi_1987_only_if: "[| triple_disjoint (I,FXf) ; BusyNetwork (I,FXf) ; (t,Yf) isDeadlockStateOf (I,FXf) |] ==> ALL i:I. (I,FXf) >> i isBlockedIn (t,Yf)" apply (intro ballI) apply (subgoal_tac "ALL i:I. Yf i <= (Ev ` (snd (FXf i)))") apply (simp only: isBlockedIn_def) apply (rule conjI) apply (simp) apply (rule conjI) (* 1 *) (* busy --> i is deadlock-free *) apply (simp add: isRequestOf_def) apply (simp add: BusyNetwork_def) apply (drule_tac x="i" in bspec, simp) (* i is deadlock-free --> EX j *) apply (rule conjI) apply (simp add: isDeadlockStateOf_def) apply (simp add: isDeadlockStateOf_def) apply (simp add: disj_not1) apply (elim conjE) apply (drule_tac x="t rest-tr (snd (FXf i))" in spec) apply (drule_tac x="Yf" in spec) apply (simp add: isStateOf_each_element) apply (simp add: ALP_def) apply (subgoal_tac "EX a: Ev ` snd (FXf i). a ~: Yf i") (* ... sub 1 *) apply (elim bexE) apply (subgoal_tac "a : Ev ` {a. EX i:I. a : snd (FXf i)}") (* ... sub 2 *) apply (rotate_tac 4) apply (drule sym) apply (simp) apply (elim conjE exE) apply (simp) apply (rule_tac x="ia" in exI) apply (case_tac "i = ia", simp) apply (simp) apply (drule_tac x="ia" in bspec, simp) apply (blast) (* sub 2 *) apply (blast) (* sub 1 *) apply (blast) (* 2 *) apply (intro allI impI) apply (unfold isUngrantedRequestOfwrt_def) apply (rule conjI) (* 2-1 *) apply (simp add: isUngrantedRequestOf_def) apply (rule) apply (subgoal_tac "x : Union {Yf i |i. i : I}") apply (simp) apply (elim conjE bexE exE) apply (case_tac "ia = i", simp) apply (case_tac "ia = j", simp) (* ia ~= i & ia ~= j ==> contradict with triple_dijoint *) apply (drule_tac x="ia" in bspec, simp) apply (simp add: isDeadlockStateOf_def isStateOf_def) apply (simp add: triple_disjoint_def) apply (drule_tac x="i" in bspec, simp) apply (drule_tac x="j" in bspec, simp add: isRequestOf_def) apply (drule_tac x="ia" in bspec, simp) apply (drule mp) apply (simp add: isRequestOf_def) apply (rotate_tac -1) apply (erule contrapos_pp) apply (blast) apply (simp add: isDeadlockStateOf_def) apply (simp add: ALP_def) apply (simp add: image_iff) apply (elim conjE bexE, simp) apply (rule_tac x="i" in bexI) apply (simp) apply (simp) (* 2-2 *) apply (rule) apply (simp add: VocabularyOf_def) apply (subgoal_tac "x : Union {Yf i |i. i : I}") apply (simp) apply (elim conjE bexE exE) apply (simp add: image_iff) apply (elim disjE conjE bexE) apply (case_tac "i = ia", simp) apply (drule_tac x="ia" in bspec, simp) apply (simp add: isDeadlockStateOf_def isStateOf_def) apply (rule_tac x="snd (FXf i) Int snd (FXf ia)" in exI) apply (rule conjI) apply (rule_tac x="i" in bexI) apply (rule_tac x="ia" in bexI) apply (simp) apply (simp) apply (simp) apply (blast) apply (case_tac "j = ia", simp) apply (drule_tac x="ia" in bspec, simp) apply (simp add: isDeadlockStateOf_def isStateOf_def) apply (rule_tac x="snd (FXf j) Int snd (FXf ia)" in exI) apply (rule conjI) apply (rule_tac x="j" in bexI) apply (rule_tac x="ia" in bexI) apply (simp) apply (simp) apply (simp add: isRequestOf_def) apply (blast) apply (simp add: isDeadlockStateOf_def) apply (simp add: ALP_def) apply (simp add: image_iff) apply (elim disjE conjE bexE) apply (rule_tac x="xa" in exI) apply (simp) apply (fast) apply (rule_tac x="xa" in exI) apply (simp) apply (rule_tac x="j" in bexI) apply (simp) apply (simp add: isRequestOf_def) apply (simp add: isDeadlockStateOf_def) apply (simp add: isStateOf_def) done (*** if ***) lemma Lemma1_Roscoe_Dathi_1987_if: "[| triple_disjoint (I,FXf) ; BusyNetwork (I,FXf) ; (t,Yf) isStateOf (I,FXf) ; ALL i:I. (I,FXf) >> i isBlockedIn (t,Yf) |] ==> (t,Yf) isDeadlockStateOf (I,FXf)" apply (simp add: isDeadlockStateOf_def) apply (simp add: ALP_def) apply (rule) (* <= *) apply (rule) apply (simp) apply (elim exE conjE) apply (simp) apply (drule_tac x="i" in bspec, simp) apply (simp add: isStateOf_def) apply (elim conjE) apply (drule_tac x="i" in bspec, simp) apply (simp add: ALP_def) apply (force) (* => *) apply (rule) apply (simp) apply (simp only: isBlockedIn_def) apply (simp add: image_iff) apply (elim conjE exE bexE) apply (simp) apply (case_tac "Ev xa : Yf i") apply (rule_tac x="Yf i" in exI) apply (fast) (* Ev xa ~: Yf i *) apply (subgoal_tac "xa : VocabularyOf (I,FXf)") apply (simp add: VocabularyOf_def) apply (elim conjE exE bexE) apply (simp) apply (case_tac "ia = i") apply (simp) apply (drule_tac x="i" in bspec, simp) apply (elim conjE exE) apply (drule_tac x="j" in spec) apply (drule mp) apply (simp add: isRequestOf_def) apply (blast) apply (simp add: isUngrantedRequestOfwrt_def) apply (simp add: isUngrantedRequestOf_def) apply (rule_tac x="Yf j" in exI) apply (fast) apply (case_tac "j = i") apply (simp) apply (drule_tac x="i" in bspec, simp) apply (elim conjE exE) apply (drule_tac x="ia" in spec) apply (drule mp) apply (simp add: isRequestOf_def) apply (blast) apply (simp add: isUngrantedRequestOfwrt_def) apply (simp add: isUngrantedRequestOf_def) apply (rule_tac x="Yf ia" in exI) apply (fast) (* ia ~= i; j ~= i; ia ~= j, but xa : snd (PXf i), ... *) apply (simp add: triple_disjoint_def) apply (drule_tac x="i" in bspec, simp) apply (rotate_tac -1) apply (drule_tac x="ia" in bspec, simp) apply (rotate_tac -1) apply (drule_tac x="j" in bspec, simp) apply (fast) (* xa : VocabularyOf VF *) apply (drule_tac x="i" in bspec, simp) apply (elim exE conjE) apply (drule_tac x="xb" in spec) apply (simp add: isUngrantedRequestOfwrt_def) apply (fast) done lemma Lemma1_Roscoe_Dathi_1987: "[| triple_disjoint (I,FXf) ; BusyNetwork (I,FXf) ; (t,Yf) isStateOf (I,FXf) |] ==> (t,Yf) isDeadlockStateOf (I,FXf) = (ALL i:I. (I,FXf) >> i isBlockedIn (t,Yf))" apply (rule) apply (simp add: Lemma1_Roscoe_Dathi_1987_only_if) apply (simp add: Lemma1_Roscoe_Dathi_1987_if) done (****************** to add it again ******************) declare disj_not1 [simp] declare Union_image_eq [simp] declare Inter_image_eq [simp] end