Theory DFP_Proof_Rule1

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F/DFP

theory DFP_Proof_Rule1
imports DFP_Block
begin
           (*-------------------------------------------*
            |                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_Proof_Rule1
imports DFP_Block
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. 

 *****************************************************************)

(*--------------------------------------------------*
 |        Theorem 1 [Roscoe_Dathi_1987 P.8]         |
 *--------------------------------------------------*)

theorem Theorem1_Roscoe_Dathi_1987:
  "[| (I,FXf) isFailureOf (I,PXf) ; I ~= {} ; finite I ; 
      triple_disjoint (I,FXf) ; BusyNetwork (I,FXf) ; 
      EX f::('i => 'a failure => ('pi::order)).
      ALL t Yf. (t,Yf) isStateOf (I,FXf) -->
      (ALL i j. (I,FXf) >> i --[(t,Yf), (VocabularyOf (I,FXf))]-->o j
                --> f j (t rest-tr (snd (FXf j)), Yf j)
                  < f i (t rest-tr (snd (FXf i)), Yf i)) |]
   ==> DeadlockFreeNetwork (I,PXf)"
apply (simp add: DeadlockFree_notDeadlockState)
apply (case_tac "ALL t Yf. ~ (t, Yf) isDeadlockStateOf (I, FXf)", simp)

      (* by contradiction *)
apply (simp)
apply (elim conjE exE)
apply (subgoal_tac "(t,Yf) isStateOf (I,FXf)")
apply (simp add: Lemma1_Roscoe_Dathi_1987)
apply (subgoal_tac "EX j:I. ALL i:I. ~(f i (t rest-tr (snd (FXf i)), Yf i) 
                                     < f j (t rest-tr (snd (FXf j)), Yf j))")
apply (elim bexE)
apply (drule_tac x="j" in bspec, simp)
apply (simp add: isBlockedIn_def)
apply (elim conjE exE)
apply (drule_tac x="x" in spec)
apply (simp)

apply (drule_tac x="t" in spec)
apply (drule_tac x="Yf" in spec)
apply (simp)
apply (drule_tac x="j" in spec)
apply (drule_tac x="x" in spec)
apply (simp)
apply (drule_tac x="x" in bspec, simp add: isRequestOf_def)
apply (simp)

apply (simp add: nonempty_finite_set_exists_min_fun)
apply (simp add: isDeadlockStateOf_def)
done

(*--------------------------------------------------*
 |         Lemma 2 [Roscoe_Dathi_1987 P.9]          |
 *--------------------------------------------------*)

lemma Lemma2_Roscoe_Dathi_1987:
  "[| I ~= {} ; finite I ;
      triple_disjoint (I,FXf) ; BusyNetwork (I,FXf) ; 
      EX f::('i => 'a failure => ('pi::order)).
      ALL i:I. ALL j:I. i ~= j -->
      (ALL t Yf.
       (t,Yf) isStateOf ({i,j},FXf) &
       ({i,j},FXf) >> i --[(t,Yf), (VocabularyOf (I,FXf))]-->o j
                 --> f j (t rest-tr (snd (FXf j)), Yf j)
                   < f i (t rest-tr (snd (FXf i)), Yf i)) |]
   ==> EX f::('i => 'a failure => ('pi::order)).
       ALL t Yf. (t,Yf) isStateOf (I,FXf) -->
      (ALL i j. (I,FXf) >> i --[(t,Yf), (VocabularyOf (I,FXf))]-->o j
                --> f j (t rest-tr (snd (FXf j)), Yf j)
                  < f i (t rest-tr (snd (FXf i)), Yf i))"
apply (elim exE)
apply (rule_tac x="f" in exI)
apply (intro allI impI)
apply (drule_tac x="i" in bspec)
apply (simp add: in_index_I)
apply (drule_tac x="j" in bspec)
apply (simp add: in_index_I)
apply (simp add: in_index_I)

apply (drule_tac x="t rest-tr ((snd (FXf i) Un snd (FXf j)))" in spec)
apply (drule_tac x="Yf" in spec)
apply (drule mp)
 apply (rule conjI)
 apply (rule isStateOf_subsetI)
 apply (simp)
 apply (simp add: in_index_I)
 apply (blast)
 apply (rule isUngrantedRequestOfwrt_subsetI)
 apply (simp_all add: in_index_I)
 apply (simp add: in_index_I)
 apply (fast)
 apply (fast)

 apply (subgoal_tac 
    "t rest-tr ((snd (FXf i) Un snd (FXf j))) rest-tr (snd (FXf i))
   = t rest-tr (snd (FXf i))")
 apply (subgoal_tac 
    "t rest-tr ((snd (FXf i) Un snd (FXf j))) rest-tr (snd (FXf j))
   = t rest-tr (snd (FXf j))")
 apply (simp)
 apply (rule rest_tr_of_rest_tr_subset)
 apply (force)
 apply (rule rest_tr_of_rest_tr_subset)
 apply (force)
done

(*--------------------------------------------------*
 |         Rule 1 [Roscoe_Dathi_1987 P.9]           |
 *--------------------------------------------------*)

lemma Rule1_Roscoe_Dathi_1987:
  "[| (I,FXf) isFailureOf (I,PXf) ; I ~= {} ; finite I ;
      triple_disjoint (I,FXf) ; BusyNetwork (I,FXf) ; 
      EX f::('i => 'a failure => ('pi::order)).
      ALL i:I. ALL j:I. i ~= j -->
      (ALL t Yf.
       ({i,j},FXf) >> i --[(t,Yf), (VocabularyOf (I,FXf))]-->o j
                 --> f j (t rest-tr (snd (FXf j)), Yf j)
                   < f i (t rest-tr (snd (FXf i)), Yf i)) |]
   ==> DeadlockFreeNetwork (I,PXf)"
apply (rule Theorem1_Roscoe_Dathi_1987)
apply (simp_all)
apply (rule Lemma2_Roscoe_Dathi_1987)
apply (simp_all)
apply (simp add: isUngrantedRequestOfwrt_def)
apply (simp add: isUngrantedRequestOf_def)
apply (simp add: isRequestOf_def)
done

lemma Rule1_Roscoe_Dathi_1987_I:
  "[| (I,FXf) isFailureOf V ; I ~= {} ; finite I ;
      triple_disjoint (I,FXf) ; BusyNetwork (I,FXf) ; 
      EX f::('i => 'a failure => ('pi::order)).
      ALL i:I. ALL j:I. i ~= j -->
      (ALL t Yf.
       ({i,j},FXf) >> i --[(t,Yf), (VocabularyOf (I,FXf))]-->o j
                 --> f j (t rest-tr (snd (FXf j)), Yf j)
                   < f i (t rest-tr (snd (FXf i)), Yf i)) |]
   ==> DeadlockFreeNetwork V"
apply (insert decompo_V[of V])
apply (rotate_tac -1, erule exE)
apply (rotate_tac -1, erule exE)
apply (subgoal_tac "Ia = I")
apply (simp add: Rule1_Roscoe_Dathi_1987)
apply (simp add: isFailureOf_def)
done

(*** looks test ***)

theorem Rule1_Roscoe_Dathi_1987_simp:
  "[| VF = {(F i, X i) | i:I}Fnet ; V = {(P i, X i) | i:I}net ;
      VF isFailureOf V ; I ~= {} ; finite I ;
      triple_disjoint VF ; BusyNetwork VF ;
      EX f::('i => 'a failure => ('pi::order)).
      ALL i:I. ALL j:I. i ~= j -->
      (ALL t Y.
       {(F i, X i) | i:{i,j}}Fnet >> 
               i --[(t,Y), (VocabularyOf VF)]-->o j
                 --> f j (t rest-tr (X j), Y j)
                   < f i (t rest-tr (X i), Y i)) |]
   ==> DeadlockFreeNetwork V"
apply (simp)
apply (rule Rule1_Roscoe_Dathi_1987_I)
apply (simp_all)
apply (elim conjE exE)
apply (rule_tac x="f" in exI)
apply (auto)
done

(****************** to add it again ******************)

declare disj_not1   [simp]

declare Union_image_eq [simp]
declare Inter_image_eq [simp]

end

theorem Theorem1_Roscoe_Dathi_1987: 

  [| (I, FXf) isFailureOf (I, PXf); I ≠ {}; finite I; triple_disjoint (I, FXf);
     BusyNetwork (I, FXf);
     ∃f. ∀t Yf. (t, Yf) isStateOf (I, FXf) -->
                (∀i j. (I, FXf) >> i --[(t, Yf),VocabularyOf (I, FXf)]-->o j -->
                       f j (t rest-tr snd (FXf j), Yf j)
                       < f i (t rest-tr snd (FXf i), Yf i)) |]
  ==> DeadlockFreeNetwork (I, PXf)

lemma Lemma2_Roscoe_Dathi_1987: 

  [| I ≠ {}; finite I; triple_disjoint (I, FXf); BusyNetwork (I, FXf);
     ∃f. ∀i∈I. ∀j∈I. i ≠ j -->
                     (∀t Yf. (t, Yf) isStateOf ({i, j}, FXf) ∧
                             ({i, j}, FXf) >> 
                              i --[(t, Yf),VocabularyOf (I, FXf)]-->o j -->
                             f j (t rest-tr snd (FXf j), Yf j)
                             < f i (t rest-tr snd (FXf i), Yf i)) |]
  ==> ∃f. ∀t Yf. (t, Yf) isStateOf (I, FXf) -->
                 (∀i j. (I, FXf) >> i --[(t, Yf),VocabularyOf (I, FXf)]-->o j -->
                        f j (t rest-tr snd (FXf j), Yf j)
                        < f i (t rest-tr snd (FXf i), Yf i))

lemma Rule1_Roscoe_Dathi_1987: 

  [| (I, FXf) isFailureOf (I, PXf); I ≠ {}; finite I; triple_disjoint (I, FXf);
     BusyNetwork (I, FXf);
     ∃f. ∀i∈I. ∀j∈I. i ≠ j -->
                     (∀t Yf. ({i, j}, FXf) >> 
                              i --[(t, Yf),VocabularyOf (I, FXf)]-->o j -->
                             f j (t rest-tr snd (FXf j), Yf j)
                             < f i (t rest-tr snd (FXf i), Yf i)) |]
  ==> DeadlockFreeNetwork (I, PXf)

lemma Rule1_Roscoe_Dathi_1987_I: 

  [| (I, FXf) isFailureOf V; I ≠ {}; finite I; triple_disjoint (I, FXf);
     BusyNetwork (I, FXf);
     ∃f. ∀i∈I. ∀j∈I. i ≠ j -->
                     (∀t Yf. ({i, j}, FXf) >> 
                              i --[(t, Yf),VocabularyOf (I, FXf)]-->o j -->
                             f j (t rest-tr snd (FXf j), Yf j)
                             < f i (t rest-tr snd (FXf i), Yf i)) |]
  ==> DeadlockFreeNetwork V

theorem Rule1_Roscoe_Dathi_1987_simp: 

  [| VF = { (F i, X i) | i:I }Fnet; V = { (P i, X i) | i:I }Fnet;
     VF isFailureOf V; I ≠ {}; finite I; triple_disjoint VF; BusyNetwork VF;
     ∃f. ∀i∈I. ∀j∈I. i ≠ j -->
                     (∀t Y. { (F i, X i) | i:{i, j} }Fnet >> 
                             i --[(t, Y),VocabularyOf VF]-->o j -->
                            f j (t rest-tr X j, Y j)
                            < f i (t rest-tr X i, Y i)) |]
  ==> DeadlockFreeNetwork V