(* Title: HOL/UNITY/Guar.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Sidi Ehmety
From Chandy and Sanders, "Reasoning About Program Composition", Technical Report 2000-003, University of Florida, 2000.
Compatibility, weakest guarantees, etc. and Weakest existential property, from Charpentier and Chandy "Theorems about Composition", Fifth International Conference on Mathematics of Program, 2000.
*)
section\<open>Guarantees Specifications\<close>
theory Guar imports Comp begin
instance program :: (type) order by standard (auto simp add: program_less_le dest: component_antisym intro: component_trans)
text\<open>Existential and Universal properties. I formalize the two-program case, proving equivalence with Chandy and Sanders's n-ary definitions\
definition ex_prop :: "'a program set => bool"where "ex_prop X == \F G. F ok G -->F \ X | G \ X --> (F\G) \ X"
definition strict_ex_prop :: "'a program set => bool"where "strict_ex_prop X == \F G. F ok G --> (F \ X | G \ X) = (F\G \ X)"
definition uv_prop :: "'a program set => bool"where "uv_prop X == SKIP \ X & (\F G. F ok G --> F \ X & G \ X --> (F\G) \ X)"
definition strict_uv_prop :: "'a program set => bool"where "strict_uv_prop X ==
SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F\<squnion>G \<in> X))"
text\<open>Guarantees properties\<close>
definition guar :: "['a program set, 'a program set] => 'a program set" (infixl\<open>guarantees\<close> 55) where (*higher than membership, lower than Co*) "X guarantees Y == {F. \G. F ok G --> F\G \ X --> F\G \ Y}"
(* Weakest guarantees *) definition wg :: "['a program, 'a program set] => 'a program set"where "wg F Y == \({X. F \ X guarantees Y})"
(* Weakest existential property stronger than X *) definition wx :: "('a program) set => ('a program)set"where "wx X == \({Y. Y \ X & ex_prop Y})"
(*Ill-defined programs can arise through "Join"*) definition welldef :: "'a program set"where "welldef == {F. Init F \ {}}"
definition refines :: "['a program, 'a program, 'a program set] => bool"
(\<open>(3_ refines _ wrt _)\<close> [10,10,10] 10) where "G refines F wrt X == \<forall>H. (F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X) -->
(G\<squnion>H \<in> welldef \<inter> X)"
definition iso_refines :: "['a program, 'a program, 'a program set] => bool"
(\<open>(3_ iso'_refines _ wrt _)\<close> [10,10,10] 10) where "G iso_refines F wrt X ==
F \<in> welldef \<inter> X --> G \<in> welldef \<inter> X"
lemma OK_insert_iff: "(OK (insert i I) F) =
(if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))" by (auto intro: ok_sym simp add: OK_iff_ok)
(*Chandy & Sanders take this as a definition*) lemma ex_prop_finite: "ex_prop X =
(\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)--> (\<Squnion>G \<in> GG. G) \<in> X)" by (blast intro: ex1 ex2)
(*Their "equivalent definition" given at the end of section 3*) lemma ex_prop_equiv: "ex_prop X = (\G. G \ X = (\H. (G component_of H) --> H \ X))" apply auto apply (unfold ex_prop_def component_of_def, safe, blast, blast) apply (subst Join_commute) apply (drule ok_sym, blast) done
(*Chandy & Sanders take this as a definition*) lemma uv_prop_finite: "uv_prop X =
(\<forall>GG. finite GG \<and> GG \<subseteq> X \<and> OK GG (\<lambda>G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)" by (blast intro: uv1 uv2)
subsection\<open>Guarantees\<close>
lemma guaranteesI: "(!!G. [| F ok G; F\G \ X |] ==> F\G \ Y) ==> F \ X guarantees Y" by (simp add: guar_def component_def)
lemma guaranteesD: "[| F \ X guarantees Y; F ok G; F\G \ X |] ==> F\G \ Y" by (unfold guar_def component_def, blast)
(*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 |] ==> H \ Y" by (unfold guar_def, blast)
lemma guarantees_weaken: "[| F \ X guarantees X'; Y \ X; X' \ Y' |] ==> F \ Y guarantees Y'" by (unfold guar_def, blast)
lemma subset_imp_guarantees_UNIV: "X \ Y ==> X guarantees Y = UNIV" by (unfold guar_def, blast)
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) lemma subset_imp_guarantees: "X \ Y ==> F \ X guarantees Y" by (unfold guar_def, blast)
(*Remark at end of section 4.1 *)
lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)" apply (simp (no_asm_use) add: guar_def ex_prop_equiv) apply safe apply (drule_tac x = x in spec) apply (drule_tac [2] x = x in spec) apply (drule_tac [2] sym) apply (auto simp add: component_of_def) done
subsection\<open>Distributive Laws. Re-Orient to Perform Miniscoping\<close>
lemma guarantees_UN_left: "(\i \ I. X i) guarantees Y = (\i \ I. X i guarantees Y)" by (unfold guar_def, blast)
lemma guarantees_Un_left: "(X \ Y) guarantees Z = (X guarantees Z) \ (Y guarantees Z)" by (unfold guar_def, blast)
lemma guarantees_INT_right: "X guarantees (\i \ I. Y i) = (\i \ I. X guarantees Y i)" by (unfold guar_def, blast)
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 add: guarantees_Int_right)
lemma guarantees_INT_right_iff: "(F \ X guarantees (\(Y ` I))) = (\i\I. F \ X guarantees (Y i))" by (simp add: guarantees_INT_right)
(** 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) ==> F \ X guarantees (\i \ 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)
lemma guarantees_Join_Int: "[| F \ U guarantees V; G \ X guarantees Y; F ok G |]
==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)" apply (simp add: guar_def, safe) apply (simp add: Join_assoc) apply (subgoal_tac "F\G\Ga = G\(F\Ga) ") apply (simp add: ok_commute) apply (simp add: Join_ac) done
lemma guarantees_Join_Un: "[| F \ U guarantees V; G \ X guarantees Y; F ok G |]
==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)" apply (simp add: guar_def, safe) apply (simp add: Join_assoc) apply (subgoal_tac "F\G\Ga = G\(F\Ga) ") apply (simp add: ok_commute) apply (simp add: Join_ac) done
lemma guarantees_JN_INT: "[| \i\I. F i \ X i guarantees Y i; OK I F |]
==> (JOIN I F) \<in> (\<Inter>(X ` I)) guarantees (\<Inter>(Y ` I))" apply (unfold guar_def, auto) apply (drule bspec, assumption) apply (rename_tac "i") apply (drule_tac x = "JOIN (I-{i}) F\G" in spec) apply (auto intro: OK_imp_ok
simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) done
lemma guarantees_JN_UN: "[| \i\I. F i \ X i guarantees Y i; OK I F |]
==> (JOIN I F) \<in> (\<Union>(X ` I)) guarantees (\<Union>(Y ` I))" apply (unfold guar_def, auto) apply (drule bspec, assumption) apply (rename_tac "i") apply (drule_tac x = "JOIN (I-{i}) F\G" in spec) apply (auto intro: OK_imp_ok
simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) done
subsection\<open>Guarantees Laws for Breaking Down the Program (by lcp)\<close>
lemma guarantees_Join_I1: "[| F \ X guarantees Y; F ok G |] ==> F\G \ X guarantees Y" by (simp add: guar_def Join_assoc)
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_JN_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, clarify) apply (drule_tac x = "JOIN (I-{i}) F\G" in spec) apply (auto intro: OK_imp_ok simp add: JN_Join_diff Join_assoc [symmetric]) done
(*** well-definedness ***)
lemma Join_welldef_D1: "F\G \ welldef ==> F \ welldef" by (unfold welldef_def, auto)
lemma Join_welldef_D2: "F\G \ welldef ==> G \ welldef" by (unfold welldef_def, auto)
(*** refinement ***)
lemma refines_refl: "F refines F wrt X" by (unfold refines_def, blast)
(*We'd like transitivity, but how do we get it?*) lemma refines_trans: "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X" apply (simp add: refines_def) oops
lemma strict_ex_refine_lemma: "strict_ex_prop X
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X)
= (F \<in> X --> G \<in> X)" by (unfold strict_ex_prop_def, auto)
lemma strict_ex_refine_lemma_v: "strict_ex_prop X
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =
(F \<in> welldef \<inter> X --> G \<in> X)" apply (unfold strict_ex_prop_def, safe) apply (erule_tac x = SKIP and P = "%H. PP H --> RR H"for PP RR in allE) apply (auto dest: Join_welldef_D1 Join_welldef_D2) done
lemma ex_refinement_thm: "[| strict_ex_prop X; \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> G\<squnion>H \<in> welldef |]
==> (G refines F wrt X) = (G iso_refines F wrt X)" apply (rule_tac x = SKIP in allE, assumption) apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v) done
lemma strict_uv_refine_lemma: "strict_uv_prop X ==>
(\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = (F \<in> X --> G \<in> X)" by (unfold strict_uv_prop_def, blast)
lemma strict_uv_refine_lemma_v: "strict_uv_prop X
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =
(F \<in> welldef \<inter> X --> G \<in> X)" apply (unfold strict_uv_prop_def, safe) apply (erule_tac x = SKIP and P = "%H. PP H --> RR H"for PP RR in allE) apply (auto dest: Join_welldef_D1 Join_welldef_D2) done
lemma uv_refinement_thm: "[| strict_uv_prop X; \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X -->
G\<squnion>H \<in> welldef |]
==> (G refines F wrt X) = (G iso_refines F wrt X)" apply (rule_tac x = SKIP in allE, assumption) apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v) done
(* Added by Sidi Ehmety from Chandy & Sander, section 6 *) lemma guarantees_equiv: "(F \ X guarantees Y) = (\H. H \ X \ (F component_of H \ H \ Y))" by (unfold guar_def component_of_def, auto)
lemma wg_weakest: "!!X. F\ (X guarantees Y) ==> X \ (wg F Y)" by (unfold wg_def, auto)
lemma wg_guarantees: "F\ ((wg F Y) guarantees Y)" by (unfold wg_def guar_def, blast)
lemma wg_equiv: "(H \ wg F X) = (F component_of H --> H \ X)" by (simp add: guarantees_equiv wg_def, blast)
lemma component_of_wg: "F component_of H ==> (H \ wg F X) = (H \ X)" by (simp add: wg_equiv)
lemma wg_finite: "\FF. finite FF \ FF \ X \ {} \ OK FF (\F. F) \<longrightarrow> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F) \<in> wg F X) = ((\<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, simp) apply (simp add: component_of_def) apply (rule_tac x = "\F \ (FF-{F}) . F" in exI) apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok) done
lemma wg_ex_prop: "ex_prop X ==> (F \ X) = (\H. H \ wg F X)" 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_weakest: "\Z. Z<= X --> ex_prop Z --> Z \ wx X" by (auto simp add: wx_def)
(* Proposition 6 *) lemma wx'_ex_prop: "ex_prop({F. \G. F ok G --> F\G \ X})" apply (unfold ex_prop_def, safe) apply (drule_tac x = "G\Ga" in spec) apply (force simp add: Join_assoc) apply (drule_tac x = "F\Ga" in spec) apply (simp add: ok_commute Join_ac) done
text\<open>Equivalence with the other definition of wx\<close>
lemma wx_equiv: "wx X = {F. \G. F ok G --> (F\G) \ X}" apply (unfold wx_def, safe) apply (simp add: ex_prop_def, blast) apply (simp (no_asm)) apply (rule_tac x = "{F. \G. F ok G --> F\G \ X}" in exI, safe) apply (rule_tac [2] wx'_ex_prop) apply (drule_tac x = SKIP in spec)+ apply auto done
text\<open>Propositions 7 to 11 are about this second definition of wx.
They are the same as the ones proved for the first definition of wx, by equivalence\<close>
(* Proposition 12 *) (* Main result of the paper *) lemma guarantees_wx_eq: "(X guarantees Y) = wx(-X \ Y)" by (simp add: guar_def wx_equiv)
(* Rules given in section 7 of Chandy and Sander's
Reasoning About Program composition paper *) lemma stable_guarantees_Always: "Init F \ A ==> F \ (stable A) guarantees (Always A)" apply (rule guaranteesI) apply (simp add: Join_commute) apply (rule stable_Join_Always1) apply (simp_all add: invariant_def) done
lemma constrains_guarantees_leadsTo: "F \ transient A ==> F \ (A co A \ B) guarantees (A leadsTo (B-A))" apply (rule guaranteesI) apply (rule leadsTo_Basis') apply (drule constrains_weaken_R) prefer 2 apply assumption apply blast apply (blast intro: Join_transient_I1) done
end
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
