|
(* Title: ZF/UNITY/Guar.thy
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
Guarantees, etc.
From Chandy and Sanders, "Reasoning About Program Composition",
Technical Report 2000-003, University of Florida, 2000.
Revised by Sidi Ehmety on January 2001
Added \<in> Compatibility, weakest guarantees, etc.
and Weakest existential property,
from Charpentier and Chandy "Theorems about Composition",
Fifth International Conference on Mathematics of Program, 2000.
Theory ported from HOL.
*)
section\<open>The Chandy-Sanders Guarantees Operator\<close>
theory Guar imports Comp begin
(* To be moved to theory WFair???? *)
lemma leadsTo_Basis': "[| F \ A co A \ B; F \ transient(A); st_set(B) |] ==> F \ A \ B"
apply (frule constrainsD2)
apply (drule_tac B = "A-B" in constrains_weaken_L, blast)
apply (drule_tac B = "A-B" in transient_strengthen, blast)
apply (blast intro: ensuresI [THEN leadsTo_Basis])
done
(*Existential and Universal properties. We formalize the two-program
case, proving equivalence with Chandy and Sanders's n-ary definitions*)
definition
ex_prop :: "i => o" where
"ex_prop(X) == X<=program &
(\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X | G \<in> X \<longrightarrow> (F \<squnion> G) \<in> X)"
definition
strict_ex_prop :: "i => o" where
"strict_ex_prop(X) == X<=program &
(\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<in> X | G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X))"
definition
uv_prop :: "i => o" where
"uv_prop(X) == X<=program &
(SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X & G \<in> X \<longrightarrow> (F \<squnion> G) \<in> X))"
definition
strict_uv_prop :: "i => o" where
"strict_uv_prop(X) == X<=program &
(SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow>(F \<in> X & G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X)))"
definition
guar :: "[i, i] => i" (infixl \<open>guarantees\<close> 55) where
(*higher than membership, lower than Co*)
"X guarantees Y == {F \ program. \G \ program. F ok G \ F \ G \ X \ F \ G \ Y}"
definition
(* Weakest guarantees *)
wg :: "[i,i] => i" where
"wg(F,Y) == \({X \ Pow(program). F:(X guarantees Y)})"
definition
(* Weakest existential property stronger than X *)
wx :: "i =>i" where
"wx(X) == \({Y \ Pow(program). Y<=X & ex_prop(Y)})"
definition
(*Ill-defined programs can arise through "\<squnion>"*)
welldef :: i where
"welldef == {F \ program. Init(F) \ 0}"
definition
refines :: "[i, i, i] => o" (\<open>(3_ refines _ wrt _)\<close> [10,10,10] 10) where
"G refines F wrt X ==
\<forall>H \<in> program. (F ok H & G ok H & F \<squnion> H \<in> welldef \<inter> X)
\<longrightarrow> (G \<squnion> H \<in> welldef \<inter> X)"
definition
iso_refines :: "[i,i, i] => o" (\<open>(3_ iso'_refines _ wrt _)\<close> [10,10,10] 10) where
"G iso_refines F wrt X == F \ welldef \ X \ G \ welldef \ X"
(*** existential properties ***)
lemma ex_imp_subset_program: "ex_prop(X) ==> X\program"
by (simp add: ex_prop_def)
lemma ex1 [rule_format]:
"GG \ Fin(program)
==> ex_prop(X) \<longrightarrow> GG \<inter> X\<noteq>0 \<longrightarrow> OK(GG, (%G. G)) \<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X"
apply (unfold ex_prop_def)
apply (erule Fin_induct)
apply (simp_all add: OK_cons_iff)
apply (safe elim!: not_emptyE, auto)
done
lemma ex2 [rule_format]:
"X \ program ==>
(\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 \<longrightarrow> OK(GG,(%G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X)
\<longrightarrow> ex_prop(X)"
apply (unfold ex_prop_def, clarify)
apply (drule_tac x = "{F,G}" in bspec)
apply (simp_all add: OK_iff_ok)
apply (auto intro: ok_sym)
done
(*Chandy & Sanders take this as a definition*)
lemma ex_prop_finite:
"ex_prop(X) \ (X\program &
(\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 & OK(GG,(%G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X))"
apply auto
apply (blast intro: ex1 ex2 dest: ex_imp_subset_program)+
done
(* Equivalent definition of ex_prop given at the end of section 3*)
lemma ex_prop_equiv:
"ex_prop(X) \
X\<subseteq>program & (\<forall>G \<in> program. (G \<in> X \<longleftrightarrow> (\<forall>H \<in> program. (G component_of H) \<longrightarrow> H \<in> X)))"
apply (unfold ex_prop_def component_of_def, safe, force, force, blast)
apply (subst Join_commute)
apply (blast intro: ok_sym)
done
(*** universal properties ***)
lemma uv_imp_subset_program: "uv_prop(X)==> X\program"
apply (unfold uv_prop_def)
apply (simp (no_asm_simp))
done
lemma uv1 [rule_format]:
"GG \ Fin(program) ==>
(uv_prop(X)\<longrightarrow> GG \<subseteq> X & OK(GG, (%G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)"
apply (unfold uv_prop_def)
apply (erule Fin_induct)
apply (auto simp add: OK_cons_iff)
done
lemma uv2 [rule_format]:
"X\program ==>
(\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG,(%G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)
\<longrightarrow> uv_prop(X)"
apply (unfold uv_prop_def, auto)
apply (drule_tac x = 0 in bspec, simp+)
apply (drule_tac x = "{F,G}" in bspec, simp)
apply (force dest: ok_sym simp add: OK_iff_ok)
done
(*Chandy & Sanders take this as a definition*)
lemma uv_prop_finite:
"uv_prop(X) \ X\program &
(\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG, %G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)"
apply auto
apply (blast dest: uv_imp_subset_program)
apply (blast intro: uv1)
apply (blast intro!: uv2 dest:)
done
(*** guarantees ***)
lemma guaranteesI:
"[| (!!G. [| F ok G; F \ G \ X; G \ program |] ==> F \ G \ Y);
F \<in> program |]
==> F \<in> X guarantees Y"
by (simp add: guar_def component_def)
lemma guaranteesD:
"[| F \ X guarantees Y; F ok G; F \ G \ X; G \ program |]
==> F \<squnion> G \<in> Y"
by (simp add: guar_def component_def)
(*This version of guaranteesD matches more easily in the conclusion
The major premise can no longer be F\<subseteq>H since we need to reason about G*)
lemma component_guaranteesD:
"[| F \ X guarantees Y; F \ G = H; H \ X; F ok G; G \ program |]
==> H \<in> Y"
by (simp add: guar_def, blast)
lemma guarantees_weaken:
"[| F \ X guarantees X'; Y \ X; X' \ Y' |] ==> F \ Y guarantees Y'"
by (simp add: guar_def, auto)
lemma subset_imp_guarantees_program:
"X \ Y ==> X guarantees Y = program"
by (unfold guar_def, blast)
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
lemma subset_imp_guarantees:
"[| X \ Y; F \ program |] ==> F \ X guarantees Y"
by (unfold guar_def, blast)
lemma component_of_Join1: "F ok G ==> F component_of (F \ G)"
by (unfold component_of_def, blast)
lemma component_of_Join2: "F ok G ==> G component_of (F \ G)"
apply (subst Join_commute)
apply (blast intro: ok_sym component_of_Join1)
done
(*Remark at end of section 4.1 *)
lemma ex_prop_imp:
"ex_prop(Y) ==> (Y = (program guarantees Y))"
apply (simp (no_asm_use) add: ex_prop_equiv guar_def component_of_def)
apply clarify
apply (rule equalityI, blast, safe)
apply (drule_tac x = x in bspec, assumption, force)
done
lemma guarantees_imp: "(Y = program guarantees Y) ==> ex_prop(Y)"
apply (unfold guar_def)
apply (simp (no_asm_simp) add: ex_prop_equiv)
apply safe
apply (blast intro: elim: equalityE)
apply (simp_all (no_asm_use) add: component_of_def)
apply (force elim: equalityE)+
done
lemma ex_prop_equiv2: "(ex_prop(Y)) \ (Y = program guarantees Y)"
by (blast intro: ex_prop_imp guarantees_imp)
(** Distributive laws. Re-orient to perform miniscoping **)
lemma guarantees_UN_left:
"i \ I ==>(\i \ I. X(i)) guarantees Y = (\i \ I. X(i) guarantees Y)"
apply (unfold guar_def)
apply (rule equalityI, safe)
prefer 2 apply force
apply blast+
done
lemma guarantees_Un_left:
"(X \ Y) guarantees Z = (X guarantees Z) \ (Y guarantees Z)"
apply (unfold guar_def)
apply (rule equalityI, safe, blast+)
done
lemma guarantees_INT_right:
"i \ I ==> X guarantees (\i \ I. Y(i)) = (\i \ I. X guarantees Y(i))"
apply (unfold guar_def)
apply (rule equalityI, safe, blast+)
done
lemma guarantees_Int_right:
"Z guarantees (X \ Y) = (Z guarantees X) \ (Z guarantees Y)"
by (unfold guar_def, blast)
lemma guarantees_Int_right_I:
"[| F \ Z guarantees X; F \ Z guarantees Y |]
==> F \<in> Z guarantees (X \<inter> Y)"
by (simp (no_asm_simp) add: guarantees_Int_right)
lemma guarantees_INT_right_iff:
"i \ I==> (F \ X guarantees (\i \ I. Y(i))) \
(\<forall>i \<in> I. F \<in> X guarantees Y(i))"
by (simp add: guarantees_INT_right INT_iff, blast)
lemma shunting: "(X guarantees Y) = (program guarantees ((program-X) \ Y))"
by (unfold guar_def, auto)
lemma contrapositive:
"(X guarantees Y) = (program - Y) guarantees (program -X)"
by (unfold guar_def, blast)
(** The following two can be expressed using intersection and subset, which
is more faithful to the text but looks cryptic.
**)
lemma combining1:
"[| F \ V guarantees X; F \ (X \ Y) guarantees Z |]
==> F \<in> (V \<inter> Y) guarantees Z"
by (unfold guar_def, blast)
lemma combining2:
"[| F \ V guarantees (X \ Y); F \ Y guarantees Z |]
==> F \<in> V guarantees (X \<union> Z)"
by (unfold guar_def, blast)
(** The following two follow Chandy-Sanders, but the use of object-quantifiers
does not suit Isabelle... **)
(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
lemma all_guarantees:
"[| \i \ I. F \ X guarantees Y(i); i \ I |]
==> F \<in> X guarantees (\<Inter>i \<in> I. Y(i))"
by (unfold guar_def, blast)
(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
lemma ex_guarantees:
"\i \ I. F \ X guarantees Y(i) ==> F \ X guarantees (\i \ I. Y(i))"
by (unfold guar_def, blast)
(*** Additional guarantees laws, by lcp ***)
lemma guarantees_Join_Int:
"[| F \ U guarantees V; G \ X guarantees Y; F ok G |]
==> F \<squnion> G: (U \<inter> X) guarantees (V \<inter> Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
apply (simp add: Join_assoc)
apply (subgoal_tac "F \ G \ Ga = G \ (F \ Ga) ")
apply (simp add: ok_commute)
apply (simp (no_asm_simp) add: Join_ac)
done
lemma guarantees_Join_Un:
"[| F \ U guarantees V; G \ X guarantees Y; F ok G |]
==> F \<squnion> G: (U \<union> X) guarantees (V \<union> Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
apply (simp add: Join_assoc)
apply (subgoal_tac "F \ G \ Ga = G \ (F \ Ga) ")
apply (rotate_tac 4)
apply (drule_tac x = "F \ Ga" in bspec)
apply (simp (no_asm))
apply (force simp add: ok_commute)
apply (simp (no_asm_simp) add: Join_ac)
done
lemma guarantees_JOIN_INT:
"[| \i \ I. F(i) \ X(i) guarantees Y(i); OK(I,F); i \ I |]
==> (\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. X(i)) guarantees (\<Inter>i \<in> I. Y(i))"
apply (unfold guar_def, safe)
prefer 2 apply blast
apply (drule_tac x = xa in bspec)
apply (simp_all add: INT_iff, safe)
apply (drule_tac x = "(\x \ (I-{xa}) . F (x)) \ G" and A=program in bspec)
apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JOIN_Join_diff JOIN_absorb)
done
lemma guarantees_JOIN_UN:
"[| \i \ I. F(i) \ X(i) guarantees Y(i); OK(I,F) |]
==> JOIN(I,F) \<in> (\<Union>i \<in> I. X(i)) guarantees (\<Union>i \<in> I. Y(i))"
apply (unfold guar_def, auto)
apply (drule_tac x = y in bspec, simp_all, safe)
apply (rename_tac G y)
apply (drule_tac x = "JOIN (I-{y}, F) \ G" and A=program in bspec)
apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JOIN_Join_diff JOIN_absorb)
done
(*** guarantees laws for breaking down the program, by lcp ***)
lemma guarantees_Join_I1:
"[| F \ X guarantees Y; F ok G |] ==> F \ G \ X guarantees Y"
apply (simp add: guar_def, safe)
apply (simp add: Join_assoc)
done
lemma guarantees_Join_I2:
"[| G \ X guarantees Y; F ok G |] ==> F \ G \ X guarantees Y"
apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
apply (blast intro: guarantees_Join_I1)
done
lemma guarantees_JOIN_I:
"[| i \ I; F(i) \ X guarantees Y; OK(I,F) |]
==> (\<Squnion>i \<in> I. F(i)) \<in> X guarantees Y"
apply (unfold guar_def, safe)
apply (drule_tac x = "JOIN (I-{i},F) \ G" in bspec)
apply (simp (no_asm))
apply (auto intro: OK_imp_ok simp add: JOIN_Join_diff Join_assoc [symmetric])
done
(*** well-definedness ***)
lemma Join_welldef_D1: "F \ G \ welldef ==> programify(F) \ welldef"
by (unfold welldef_def, auto)
lemma Join_welldef_D2: "F \ G \ welldef ==> programify(G) \ welldef"
by (unfold welldef_def, auto)
(*** refinement ***)
lemma refines_refl: "F refines F wrt X"
by (unfold refines_def, blast)
(* More results on guarantees, added by Sidi Ehmety from Chandy & Sander, section 6 *)
lemma wg_type: "wg(F, X) \ program"
by (unfold wg_def, auto)
lemma guarantees_type: "X guarantees Y \ program"
by (unfold guar_def, auto)
lemma wgD2: "G \ wg(F, X) ==> G \ program & F \ program"
apply (unfold wg_def, auto)
apply (blast dest: guarantees_type [THEN subsetD])
done
lemma guarantees_equiv:
"(F \ X guarantees Y) \
F \<in> program & (\<forall>H \<in> program. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
by (unfold guar_def component_of_def, force)
lemma wg_weakest:
"!!X. [| F \ (X guarantees Y); X \ program |] ==> X \ wg(F,Y)"
by (unfold wg_def, auto)
lemma wg_guarantees: "F \ program ==> F \ wg(F,Y) guarantees Y"
by (unfold wg_def guar_def, blast)
lemma wg_equiv:
"H \ wg(F,X) \
((F component_of H \<longrightarrow> H \<in> X) & F \<in> program & H \<in> program)"
apply (simp add: wg_def guarantees_equiv)
apply (rule iffI, safe)
apply (rule_tac [4] x = "{H}" in bexI)
apply (rule_tac [3] x = "{H}" in bexI, blast+)
done
lemma component_of_wg:
"F component_of H ==> H \ wg(F,X) \ (H \ X & F \ program & H \ program)"
by (simp (no_asm_simp) add: wg_equiv)
lemma wg_finite [rule_format]:
"\FF \ Fin(program). FF \ X \ 0 \ OK(FF, %F. F)
\<longrightarrow> (\<forall>F \<in> FF. ((\<Squnion>F \<in> FF. F) \<in> wg(F,X)) \<longleftrightarrow> ((\<Squnion>F \<in> FF. F) \<in> X))"
apply clarify
apply (subgoal_tac "F component_of (\F \ FF. F) ")
apply (drule_tac X = X in component_of_wg)
apply (force dest!: Fin.dom_subset [THEN subsetD, THEN PowD])
apply (simp_all add: component_of_def)
apply (rule_tac x = "\F \ (FF-{F}) . F" in exI)
apply (auto intro: JOIN_Join_diff dest: ok_sym simp add: OK_iff_ok)
done
lemma wg_ex_prop:
"ex_prop(X) ==> (F \ X) \ (\H \ program. H \ wg(F,X) & F \ program)"
apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
apply blast
done
(** From Charpentier and Chandy "Theorems About Composition" **)
(* Proposition 2 *)
lemma wx_subset: "wx(X)\X"
by (unfold wx_def, auto)
lemma wx_ex_prop: "ex_prop(wx(X))"
apply (simp (no_asm_use) add: ex_prop_def wx_def)
apply safe
apply blast
apply (rule_tac x=x in bexI, force, simp)+
done
lemma wx_weakest: "\Z. Z\program \ Z\ X \ ex_prop(Z) \ Z \ wx(X)"
by (unfold wx_def, auto)
(* Proposition 6 *)
lemma wx'_ex_prop:
"ex_prop({F \ program. \G \ program. F ok G \ F \ G \ X})"
apply (unfold ex_prop_def, safe)
apply (drule_tac x = "G \ Ga" in bspec)
apply (simp (no_asm))
apply (force simp add: Join_assoc)
apply (drule_tac x = "F \ Ga" in bspec)
apply (simp (no_asm))
apply (simp (no_asm_use))
apply safe
apply (simp (no_asm_simp) add: ok_commute)
apply (subgoal_tac "F \ G = G \ F")
apply (simp (no_asm_simp) add: Join_assoc)
apply (simp (no_asm) add: Join_commute)
done
(* Equivalence with the other definition of wx *)
lemma wx_equiv:
"wx(X) = {F \ program. \G \ program. F ok G \ (F \ G) \ X}"
apply (unfold wx_def)
apply (rule equalityI, safe, blast)
apply (simp (no_asm_use) add: ex_prop_def)
apply blast
apply (rule_tac B = "{F \ program. \G \ program. F ok G \ F \ G \ X}"
in UnionI,
safe)
apply (rule_tac [2] wx'_ex_prop)
apply (drule_tac x=SKIP in bspec, simp)+
apply auto
done
(* Propositions 7 to 11 are all about this second definition of wx. And
by equivalence between the two definition, they are the same as the ones proved *)
(* Proposition 12 *)
(* Main result of the paper *)
lemma guarantees_wx_eq: "(X guarantees Y) = wx((program-X) \ Y)"
by (auto simp add: guar_def wx_equiv)
(*
{* Corollary, but this result has already been proved elsewhere *}
"ex_prop(X guarantees Y)"
*)
(* Rules given in section 7 of Chandy and Sander's
Reasoning About Program composition paper *)
lemma stable_guarantees_Always:
"[| Init(F) \ A; F \ program |] ==> F \ stable(A) guarantees Always(A)"
apply (rule guaranteesI)
prefer 2 apply assumption
apply (simp (no_asm) add: Join_commute)
apply (rule stable_Join_Always1)
apply (simp_all add: invariant_def)
apply (auto simp add: programify_def initially_def)
done
lemma constrains_guarantees_leadsTo:
"[| F \ transient(A); st_set(B) |]
==> F: (A co A \<union> B) guarantees (A \<longmapsto> (B-A))"
apply (rule guaranteesI)
prefer 2 apply (blast dest: transient_type [THEN subsetD])
apply (rule leadsTo_Basis')
apply (blast intro: constrains_weaken_R)
apply (blast intro!: Join_transient_I1, blast)
done
end
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
