Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Guar.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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 "guarantees" 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"
                        ("(3_ refines _ wrt _)" [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"
                              ("(3_ iso'_refines _ wrt _)" [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)

subsection\<open>Existential Properties\<close>

lemma ex1:
  assumes "ex_prop X" and "finite GG"
  shows "GG \ X \ {} \ OK GG (%G. G) \ (\G \ GG. G) \ X"
  apply (atomize (full))
  using assms(2) apply induct
   using assms(1) apply (unfold ex_prop_def)
   apply (auto simp add: OK_insert_iff Int_insert_left)
  done

lemma ex2:
     "\GG. finite GG & GG \ X \ {} \ OK GG (\G. G) \ (\G \ GG. G) \ X
      \<Longrightarrow> ex_prop X"
apply (unfold ex_prop_def, clarify)
apply (drule_tac x = "{F,G}" in spec)
apply (auto dest: ok_sym simp add: OK_iff_ok)
done

(*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

subsection\<open>Universal Properties\<close>

lemma uv1:
  assumes "uv_prop X"
    and "finite GG"
    and "GG \ X"
    and "OK GG (%G. G)"
  shows "(\G \ GG. G) \ X"
  using assms(2-)
  apply induct
   using assms(1)
   apply (unfold uv_prop_def)
   apply (auto simp add: Int_insert_left OK_insert_iff)
  done

lemma uv2:
     "\GG. finite GG & GG \ X & OK GG (%G. G) --> (\G \ GG. G) \ X
      ==> uv_prop X"
apply (unfold uv_prop_def)
apply (rule conjI)
apply (drule_tac x = "{}" in spec)
prefer 2
apply clarify
apply (drule_tac x = "{F,G}" in spec)
apply (auto dest: ok_sym simp add: OK_iff_ok)
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

lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)"
by (auto simp add: guar_def ex_prop_equiv component_of_def dest: sym)

lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)"
apply (rule iffI)
apply (rule ex_prop_imp)
apply (auto simp add: guarantees_imp)
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)

lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \ Y))"
by (unfold guar_def, blast)

lemma contrapositive: "(X guarantees Y) = -Y guarantees -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) ==> 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)

subsection\<open>Guarantees: Additional Laws (by lcp)\<close>

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_ex_prop: "ex_prop (wx X)"
apply (simp add: wx_def ex_prop_equiv cong: bex_cong, safe, blast)
apply force
done

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.24 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.