Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F/DFP
theory DFP_subseteqEX (*-------------------------------------------*
| 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, Y ∩ A) |s Y. (s, Y) :f F}
lemma subseteqEX_restRefusal_iff:
(F <=EX E restRefusal A) = ((∀s Y. (s, Y) ∈ F --> (s, Y) :f E ∧ Y ⊆ A) ∧ (∀s Y. (s, Y) :f E --> (∃Z. (s, Z) ∈ F ∧ Y ∩ A ⊆ Z)))
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.0 ∪ F2.0 <=EX failures (P1.0 |~| P2.0) MF restRefusal A
lemma cspF_subseteqEX_Int_choice:
[| P =F P1.0 |~| P2.0; F = F1.0 ∪ F2.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:
∀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
lemma cspF_subseteqEX_Rep_int_choice_nat:
[| P =F !nat :N .. Pf; F = Union {Ff n |n. n ∈ N}; ∀n∈N. Ff n <=EX failures (Pf n) MF restRefusal A |] ==> F <=EX failures (!nat :N .. Pf) MF restRefusal A
lemma subseteqEX_Rep_int_choice_set:
∀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
lemma cspF_subseteqEX_Rep_int_choice_set:
[| P =F !set :Xs .. Pf; F = Union {Ff X |X. X ∈ Xs}; ∀X∈Xs. 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. a ∈ X}; ∀a∈X. 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. a ∈ X}; ∀a∈X. 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. n ∈ N}; ∀n∈N. 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. X ∈ Xs}; ∀X∈Xs. 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. a ∈ X}; ∀a∈X. 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. a ∈ X}; ∀a∈X. 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. n ∈ N}; ∀n∈N. 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. X ∈ Xs}; ∀X∈Xs. 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. a ∈ X}; ∀a∈X. 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. a ∈ X}; ∀a∈X. 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:
∀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
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}; ∀a∈X. 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