Quelle Guar.thy Sprache: Isabelle

(*  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 \<and> (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X \<and> 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 \<and> (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow>(F \<in> X \<and> G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X)))"

definition
  guar :: "[i, i] \ i" (infixl \guarantees\ 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" (\(\indent=3 notation=\mixfix refines wrt\\_ refines _ wrt _)\ [10,10,10] 10) where
  "G refines F wrt X \
   \<forall>H \<in> program. (F ok H  \<and> G ok H \<and> F \<squnion> H \<in> welldef \<inter> X)
    \<longrightarrow> (G \<squnion> H \<in> welldef \<inter> X)"

definition
  iso_refines :: "[i,i, i] \ o" (\(\indent=3 notation=\mixfix iso_refines wrt\\_ iso'_refines _ wrt _)\ [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)
  \<Longrightarrow> ex_prop(X) \<longrightarrow> GG \<inter> X\<noteq>0 \<longrightarrow> OK(GG, (\<lambda>G. G)) \<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X"
  unfolding 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,(\<lambda>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 \<and> 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 \<and> OK(GG,(\<lambda>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 \<and> (\<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"
  unfolding uv_prop_def
apply (simp (no_asm_simp))
done

lemma uv1 [rule_format]:
     "GG \ Fin(program) \
      (uv_prop(X)\<longrightarrow> GG \<subseteq> X \<and> OK(GG, (\<lambda>G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)"
  unfolding 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 \<and> OK(GG,(\<lambda>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 \<and> Sanders take this as a definition*)
lemma uv_prop_finite:
"uv_prop(X) \ X\program \
  (\<forall>GG \<in> Fin(program). GG \<subseteq> X \<and> OK(GG, \<lambda>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\<rbrakk>
    \<Longrightarrow> 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\
      \<Longrightarrow> 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\
      \<Longrightarrow> 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)"
  unfolding 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)"
  unfolding 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)"
  unfolding 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))"
  unfolding 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\
     \<Longrightarrow> 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\
     \<Longrightarrow> F \<in> (V \<inter> Y) guarantees Z"
by (unfold guar_def, blast)

lemma combining2:
    "\F \ V guarantees (X \ Y); F \ Y guarantees Z\
     \<Longrightarrow> 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 (\<And>i. i \<in> I \<Longrightarrow> F \<in> X guarantees Y i) *)
lemma all_guarantees:
     "\\i \ I. F \ X guarantees Y(i); i \ I\
    \<Longrightarrow> F \<in> X guarantees (\<Inter>i \<in> I. Y(i))"
by (unfold guar_def, blast)

(*Premises should be \<lbrakk>F \<in> X guarantees Y i; i \<in> I\<rbrakk> *)
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\
     \<Longrightarrow> F \<squnion> G: (U \<inter> X) guarantees (V \<inter> Y)"

  unfolding 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\
     \<Longrightarrow> F \<squnion> G: (U \<union> X) guarantees (V \<union> Y)"
  unfolding 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\
      \<Longrightarrow> (\<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)\
     \<Longrightarrow> 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)\
      \<Longrightarrow> (\<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 \<and> 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 \<and> (\<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) \<and> F \<in> program \<and> 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}"
  unfolding 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)\
      \<Longrightarrow> 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

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.