Theory DFP_subseteqEX

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

theory DFP_subseteqEX
imports CSP_F
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_subseteqEX
imports CSP_F
begin

(*****************************************************************

  1. safe subsets of [[P]]F, used for deadlock-free verification.

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

(*********************************************************
                    safe cut of [[_]]F
        This is used for deadlock-free verification.
 *********************************************************)

consts 
  restRefusal :: "'a setF => 'a event set => 'a failure set"
                                     ("(0_/ restRefusal /_)" [52,990] 52)
  subseteqEX   :: "'a failure set => 'a failure set => bool"
                                     ("(0_/ <=EX /_)" [50,50] 50)

defs
  restRefusal_def :
    "F restRefusal A == {(s,Y)| s Y. (s,Y) :f F & Y <= A}"
  subseteqEX_def :
    "F <=EX E == (F <= E) & (ALL s Y. (s,Y) : E --> (EX Z. (s,Z) : F & Y <= Z))"

(*********************************************************
                subseteqEX &  restRefusal
 *********************************************************)

lemma subseteqEX_reflex[simp]:  "F <=EX F"
apply (simp add: subseteqEX_def)
apply (auto)
done

lemma subseteqEX_Int:
   "F restRefusal A = {(s,Y Int A)|s Y. (s,Y) :f F}"
apply (simp add: restRefusal_def)
apply (auto)
apply (rule memF_F2)
apply (simp)
apply (fast)
done

lemma subseteqEX_restRefusal_iff:
  "(F <=EX E restRefusal A)
   = ((ALL s Y. (s, Y) : F --> (s, Y) :f E & Y <= A) &
      (ALL s Y. (s, Y) :f E --> (EX Z. (s, Z) : F & Y Int A <= Z)))"
apply (simp add: subseteqEX_def)
apply (simp add: restRefusal_def)
apply (rule iffI)

(* --> *)

 apply (rule conjI)

  apply (intro allI impI)
  apply (elim conjE)
  apply (erule subsetE)
  apply (drule_tac x="(s,Y)" in bspec, simp)
  apply (simp)

  apply (intro allI impI)
  apply (elim conjE)
  apply (drule_tac x="s" in spec)
  apply (drule_tac x="Y Int A" in spec)
  apply (drule mp)
   apply (rule conjI)
   apply (rule memF_F2, simp_all)
   apply (fast)
  apply (fast)

(* <-- *)

 apply (rule conjI)
  apply (elim conjE)
  apply (rule subsetI)
  apply (drule_tac x="fst x" in spec)
  apply (drule_tac x="snd x" in spec)
  apply (force)

  apply (intro allI impI)
  apply (elim conjE)
  apply (rotate_tac 1)
  apply (drule_tac x="s" in spec)
  apply (drule_tac x="Y" in spec)
  apply (simp)
  apply (elim conjE exE)
  apply (rule_tac x="Z" in exI)
  apply (simp)
  apply (force)
done

(*********************************************************
        How to prove F <=EX ([[P]]F restRefusal A)
 *********************************************************)

(*--------------------*
 |        DIV         |
 *--------------------*)

lemma subseteqEX_DIV[simp]: "{} <=EX failures (DIV) MF restRefusal A"
apply (simp add: subseteqEX_def)
apply (simp add: restRefusal_def)
apply (simp add: in_failures)
done

(*-----------*
 | csp rules |
 *-----------*)

lemma cspF_subseteqEX_DIV:
  "P =F DIV ==> {} <=EX failures (DIV) MF restRefusal A"
by (simp add: eqF_def)

(*--------------------*
 |     Int_choice     |
 *--------------------*)

(* eq *)

lemma subseteqEX_Int_choice: 
  "[| F1 <=EX failures P1 MF restRefusal A ; 
      F2 <=EX failures P2 MF restRefusal A |]
    ==> F1 Un F2 <=EX failures (P1 |~| P2) MF restRefusal A"
apply (simp add: subseteqEX_restRefusal_iff)
apply (simp add: in_failures)
apply (intro allI impI)
apply (elim conjE)
apply (rule conjI)

 apply (rotate_tac 1)
 apply (drule_tac x="s" in spec)
 apply (drule_tac x="Y" in spec)
 apply (fast)

 apply (rotate_tac 3)
 apply (drule_tac x="s" in spec)
 apply (drule_tac x="Y" in spec)
 apply (fast)
done

(*-----------*
 | csp rules |
 *-----------*)

lemma cspF_subseteqEX_Int_choice: 
  "[| P =F P1 |~| P2 ;
      F = F1 Un F2 ;
      F1 <=EX failures P1 MF restRefusal A ;
      F2 <=EX failures P2 MF restRefusal A |]
   ==> F <=EX failures P  MF restRefusal A"
apply (simp add: eqF_def)
apply (simp add: eqF_decompo)
apply (simp add: subseteqEX_Int_choice)
done

(*------------------------*
 |   Rep_int_choice_nat   |
 *------------------------*)

(* eq *)

lemma subseteqEX_Rep_int_choice_nat: 
  "[| ALL n : N. Ff n <=EX failures(Pf n) MF restRefusal A |]
    ==> Union {Ff n |n. n : N} <=EX failures (!nat :N .. Pf) MF restRefusal A"
apply (simp add: subseteqEX_restRefusal_iff)
apply (simp add: in_failures)
apply (rule conjI)

 (* 1 *)
 apply (force)

 (* 2 *)
 apply (intro allI impI)
 apply (elim conjE bexE)
 apply (drule_tac x="n" in bspec, simp)
 apply (elim conjE)
 apply (rotate_tac -1)
 apply (drule_tac x="s" in spec)
 apply (drule_tac x="Y" in spec)
 apply (auto)
done

(*-----------*
 | csp rules |
 *-----------*)

lemma cspF_subseteqEX_Rep_int_choice_nat: 
  "[| P =F !nat :N .. Pf ;
      F = Union {Ff n |n. n : N} ;
      ALL n : N. Ff n <=EX failures(Pf n) MF restRefusal A |]
   ==> F <=EX failures (!nat :N .. Pf) MF restRefusal A"
by (simp add: subseteqEX_Rep_int_choice_nat)

(*------------------------*
 |   Rep_int_choice_set   |
 *------------------------*)

(* eq *)

lemma subseteqEX_Rep_int_choice_set: 
  "[| ALL X : Xs. Ff X <=EX failures(Pf X) MF restRefusal A |]
    ==> Union {Ff X |X. X : Xs} <=EX failures (!set :Xs .. Pf) MF restRefusal A"
apply (simp add: subseteqEX_restRefusal_iff)
apply (simp add: in_failures)
apply (rule conjI)

 (* 1 *)
 apply (force)

 (* 2 *)
 apply (intro allI impI)
 apply (elim conjE bexE)
 apply (drule_tac x="X" in bspec, simp)
 apply (elim conjE)
 apply (rotate_tac -1)
 apply (drule_tac x="s" in spec)
 apply (drule_tac x="Y" in spec)
 apply (auto)
done

(*-----------*
 | csp rules |
 *-----------*)

lemma cspF_subseteqEX_Rep_int_choice_set: 
  "[| P =F !set :Xs .. Pf ;
      F = Union {Ff X |X. X : Xs} ;
      ALL X : Xs. Ff X <=EX failures(Pf X) MF restRefusal A |]
   ==> F <=EX failures (!set :Xs .. Pf) MF restRefusal A"
by (simp add: subseteqEX_Rep_int_choice_set)

(* com *)

lemma cspF_subseteqEX_Rep_int_choice_com: 
  "[| P =F ! :X .. Pf ;
      F = Union {Ff a |a. a : X} ;
      ALL a : X. Ff a <=EX failures(Pf a) MF restRefusal A |]
   ==> F <=EX failures (! :X .. Pf) MF restRefusal A"
apply (unfold Rep_int_choice_com_def)
apply (rule cspF_subseteqEX_Rep_int_choice_set[of _ _ _ _ "(%X. Ff(contents X))"])
apply (auto)
apply (rule_tac x="Ff (contents {aa})" in exI)
apply (simp)
apply (rule_tac x="{aa}" in exI)
apply (simp)
done

(* f *)

lemma cspF_subseteqEX_Rep_int_choice_f: 
  "[| inj f;  P =F !<f> :X .. Pf ;
      F = Union {Ff a |a. a : X} ;
      ALL a : X. Ff a <=EX failures(Pf a) MF restRefusal A |]
   ==> F <=EX failures (!<f> :X .. Pf) MF restRefusal A"
apply (unfold Rep_int_choice_f_def)
apply (rule cspF_subseteqEX_Rep_int_choice_com[of _ _ _ _ "(%x. Ff(inv f x))"])
apply (auto)

 apply (rule_tac x="Ff aa" in exI)
 apply (simp)
 apply (rule_tac x="f aa" in exI)
 apply (simp)
done

lemmas cspF_subseteqEX_Rep_int_choice =
       cspF_subseteqEX_Rep_int_choice_nat
       cspF_subseteqEX_Rep_int_choice_set
       cspF_subseteqEX_Rep_int_choice_com
       cspF_subseteqEX_Rep_int_choice_f

lemma cspF_subseteqEX_Rep_int_choice_nat_UNIV: 
  "[| P =F !nat n .. Pf n ;
      F = Union {Ff a |a. True} ;
      ALL a. Ff a <=EX failures(Pf a) MF restRefusal A |]
   ==> F <=EX failures (!nat n .. Pf n) MF restRefusal A"
apply (insert cspF_subseteqEX_Rep_int_choice_nat[of P UNIV Pf F Ff A])
by (simp_all)

(*--------------------*
 |   Ext_pre_choice   |
 *--------------------*)

(* eq *)

lemma subseteqEX_Ext_pre_choice: 
  "ALL a : X. Ff a <=EX failures (Pf a) MF restRefusal A
    ==> insert (<>, A - Ev ` X) 
        {(<Ev a> ^^ s, Y) |a s Y. (s,Y) : Ff a & a : X}
        <=EX failures (? :X -> Pf) MF restRefusal A"
apply (simp add: subseteqEX_restRefusal_iff)
apply (simp add: in_failures)
apply (intro conjI)

 (* 1 *)
 apply (fast)

 (* 2 *)
 apply (intro allI impI)
 apply (rule conjI)
  apply (fast)

  apply (intro impI)
  apply (elim conjE exE)
  apply (drule_tac x="a" in bspec, simp)
  apply (elim conjE)
  apply (rotate_tac -1)
  apply (drule_tac x="sa" in spec)
  apply (drule_tac x="Y" in spec)
  apply (simp)
done

(*-----------*
 | csp rules |
 *-----------*)

lemma cspF_subseteqEX_Ext_pre_choice: 
  "[| P =F ? :X -> Pf ;
      F = insert (<>, A - Ev ` X) 
          {(<Ev a> ^^ s, Y) |a s Y. (s,Y) : Ff a & a : X} ;
      ALL a : X. Ff a <=EX failures (Pf a) MF restRefusal A |]
   ==> F <=EX failures P MF restRefusal A"
by (simp add: eqF_def eqF_decompo subseteqEX_Ext_pre_choice)

(*-----------*
 | csp rules |
 *-----------*)

lemma cspF_subseteqEX_eqF:
  "[| P =F Q ;
       FS <=EX failures Q MF restRefusal A |]
   ==> FS <=EX failures P MF restRefusal A"
by (simp add: eqF_def eqF_decompo)

(****************** to add them again ******************)

end


lemma subseteqEX_reflex:

  F <=EX F

lemma subseteqEX_Int:

  F restRefusal A = {(s, YA) |s Y. (s, Y) :f F}

lemma subseteqEX_restRefusal_iff:

  (F <=EX E restRefusal A) =
  ((∀s Y. (s, Y) ∈ F --> (s, Y) :f EYA) ∧
   (∀s Y. (s, Y) :f E --> (∃Z. (s, Z) ∈ FYAZ)))

lemma subseteqEX_DIV:

  {} <=EX failures DIV MF restRefusal A

lemma cspF_subseteqEX_DIV:

  P =F DIV ==> {} <=EX failures DIV MF restRefusal A

lemma subseteqEX_Int_choice:

  [| F1.0 <=EX failures P1.0 MF restRefusal A;
     F2.0 <=EX failures P2.0 MF restRefusal A |]
  ==> F1.0F2.0 <=EX failures (P1.0 |~| P2.0) MF restRefusal A

lemma cspF_subseteqEX_Int_choice:

  [| P =F P1.0 |~| P2.0; F = F1.0F2.0;
     F1.0 <=EX failures P1.0 MF restRefusal A;
     F2.0 <=EX failures P2.0 MF restRefusal A |]
  ==> F <=EX failures P MF restRefusal A

lemma subseteqEX_Rep_int_choice_nat:

nN. Ff n <=EX failures (Pf n) MF restRefusal A
  ==> Union {Ff n |n. nN} <=EX failures (!nat :N .. Pf) MF restRefusal A

lemma cspF_subseteqEX_Rep_int_choice_nat:

  [| P =F !nat :N .. Pf; F = Union {Ff n |n. nN};
     ∀nN. Ff n <=EX failures (Pf n) MF restRefusal A |]
  ==> F <=EX failures (!nat :N .. Pf) MF restRefusal A

lemma subseteqEX_Rep_int_choice_set:

XXs. Ff X <=EX failures (Pf X) MF restRefusal A
  ==> Union {Ff X |X. XXs} <=EX failures (!set :Xs .. Pf) MF restRefusal A

lemma cspF_subseteqEX_Rep_int_choice_set:

  [| P =F !set :Xs .. Pf; F = Union {Ff X |X. XXs};
     ∀XXs. Ff X <=EX failures (Pf X) MF restRefusal A |]
  ==> F <=EX failures (!set :Xs .. Pf) MF restRefusal A

lemma cspF_subseteqEX_Rep_int_choice_com:

  [| P =F ! :X .. Pf; F = Union {Ff a |a. aX};
     ∀aX. Ff a <=EX failures (Pf a) MF restRefusal A |]
  ==> F <=EX failures (! :X .. Pf) MF restRefusal A

lemma cspF_subseteqEX_Rep_int_choice_f:

  [| inj f; P =F !<f> :X .. Pf; F = Union {Ff a |a. aX};
     ∀aX. Ff a <=EX failures (Pf a) MF restRefusal A |]
  ==> F <=EX failures (!<f> :X .. Pf) MF restRefusal A

lemmas cspF_subseteqEX_Rep_int_choice:

  [| P =F !nat :N .. Pf; F = Union {Ff n |n. nN};
     ∀nN. Ff n <=EX failures (Pf n) MF restRefusal A |]
  ==> F <=EX failures (!nat :N .. Pf) MF restRefusal A
  [| P =F !set :Xs .. Pf; F = Union {Ff X |X. XXs};
     ∀XXs. Ff X <=EX failures (Pf X) MF restRefusal A |]
  ==> F <=EX failures (!set :Xs .. Pf) MF restRefusal A
  [| P =F ! :X .. Pf; F = Union {Ff a |a. aX};
     ∀aX. Ff a <=EX failures (Pf a) MF restRefusal A |]
  ==> F <=EX failures (! :X .. Pf) MF restRefusal A
  [| inj f; P =F !<f> :X .. Pf; F = Union {Ff a |a. aX};
     ∀aX. Ff a <=EX failures (Pf a) MF restRefusal A |]
  ==> F <=EX failures (!<f> :X .. Pf) MF restRefusal A

lemmas cspF_subseteqEX_Rep_int_choice:

  [| P =F !nat :N .. Pf; F = Union {Ff n |n. nN};
     ∀nN. Ff n <=EX failures (Pf n) MF restRefusal A |]
  ==> F <=EX failures (!nat :N .. Pf) MF restRefusal A
  [| P =F !set :Xs .. Pf; F = Union {Ff X |X. XXs};
     ∀XXs. Ff X <=EX failures (Pf X) MF restRefusal A |]
  ==> F <=EX failures (!set :Xs .. Pf) MF restRefusal A
  [| P =F ! :X .. Pf; F = Union {Ff a |a. aX};
     ∀aX. Ff a <=EX failures (Pf a) MF restRefusal A |]
  ==> F <=EX failures (! :X .. Pf) MF restRefusal A
  [| inj f; P =F !<f> :X .. Pf; F = Union {Ff a |a. aX};
     ∀aX. Ff a <=EX failures (Pf a) MF restRefusal A |]
  ==> F <=EX failures (!<f> :X .. Pf) MF restRefusal A

lemma cspF_subseteqEX_Rep_int_choice_nat_UNIV:

  [| P =F !nat :UNIV .. Pf; F = Union {Ff a |a. True};
     ∀a. Ff a <=EX failures (Pf a) MF restRefusal A |]
  ==> F <=EX failures (!nat :UNIV .. Pf) MF restRefusal A

lemma subseteqEX_Ext_pre_choice:

aX. Ff a <=EX failures (Pf a) MF restRefusal A
  ==> insert (<>, A - Ev ` X) {(<Ev a> ^^ s, Y) |a s Y. (s, Y) ∈ Ff aaX}
      <=EX failures (? :X -> Pf) MF restRefusal A

lemma cspF_subseteqEX_Ext_pre_choice:

  [| P =F ? :X -> Pf;
     F = insert (<>, A - Ev ` X) {(<Ev a> ^^ s, Y) |a s Y. (s, Y) ∈ Ff aaX};
     ∀aX. Ff a <=EX failures (Pf a) MF restRefusal A |]
  ==> F <=EX failures P MF restRefusal A

lemma cspF_subseteqEX_eqF:

  [| P =F Q; FS <=EX failures Q MF restRefusal A |]
  ==> FS <=EX failures P MF restRefusal A