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‹The Chandy-Sanders Guarantees Operator›

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 \
    (∀F ∈ program. ∀G ∈ program. F ok G ⟶ F ∈ X | G ∈ X ⟶ (F ⊔ G) ∈ X)"

definition
  strict_ex_prop  :: "i \ o"  where
  "strict_ex_prop(X) \ X<=program \
   (∀F ∈ program. ∀G ∈ program. F ok G ⟶ (F ∈ X | G ∈ X) ⟷ (F ⊔ G ∈ X))"

definition
  uv_prop  :: "i \ o"  where
   "uv_prop(X) \ X<=program \
    (SKIP ∈ X ∧ (∀F ∈ program. ∀G ∈ program. F ok G ⟶ F ∈ X ∧ G ∈ X ⟶ (F ⊔ G) ∈ X))"
  
definition
 strict_uv_prop  :: "i \ o"  where
   "strict_uv_prop(X) \ X<=program \
    (SKIP ∈ X ∧ (∀F ∈ program. ∀G ∈ program. F ok G ⟶(F ∈ X ∧ G ∈ X) ⟷ (F ⊔ G ∈ 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 \
   ∀H ∈ program. (F ok H  ∧ G ok H ∧ F ⊔ H ∈ welldef ∩ X)
    ⟶ (G ⊔ H ∈ welldef ∩ 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)
  ==> ex_prop(X) ⟶ GG ∩ X≠0 ⟶ OK(GG, (λG. G)) ⟶(⊔G ∈ GG. G) ∈ 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 \
 (∀GG ∈ Fin(program). GG ∩ X ≠ 0 ⟶ OK(GG,(λG. G))⟶(⊔G ∈ GG. G) ∈ X) 
   ⟶ 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 \
  (∀GG ∈ Fin(program). GG ∩ X ≠ 0 ∧ OK(GG,(λG. G))⟶(⊔G ∈ GG. G) ∈ 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⊆program ∧ (∀G ∈ program. (G ∈ X ⟷ (∀H ∈ program. (G component_of H) ⟶ H ∈ 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)⟶ GG ⊆ X ∧ OK(GG, (λG. G)) ⟶ (⊔G ∈ GG. G) ∈ X)"
  unfolding uv_prop_def
apply (erule Fin_induct)
apply (auto simp add: OK_cons_iff)
done

lemma uv2 [rule_format]: 
     "X\program \
      (∀GG ∈ Fin(program). GG ⊆ X ∧ OK(GG,(λG. G)) ⟶ (⊔G ∈ GG. G) ∈ X)
      ⟶ 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 \
  (∀GG ∈ Fin(program). GG ⊆ X ∧ OK(GG, λG. G) ⟶ (⊔G ∈ GG. G) ∈  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 ∈ program]   
    ==> F ∈ 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 ⊔ G ∈ 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 ∈ 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\
     ==> F ∈ Z guarantees (X ∩ Y)"
by (simp (no_asm_simp) add: guarantees_Int_right)

lemma guarantees_INT_right_iff:
     "i \ I\ (F \ X guarantees (\i \ I. Y(i))) \
      (∀i ∈ I. F ∈ 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 ∈ (V ∩ Y) guarantees Z"
by (unfold guar_def, blast)

lemma combining2: 
    "\F \ V guarantees (X \ Y); F \ Y guarantees Z\
     ==> F ∈ V guarantees (X ∪ 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\
    ==> F ∈ X guarantees (∩i ∈ 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\
     ==> F ⊔ G: (U ∩ X) guarantees (V ∩ 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\
     ==> F ⊔ G: (U ∪ X) guarantees (V ∪ 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\
      ==> (⊔i ∈ I. F(i)) ∈ (∩i ∈ I. X(i)) guarantees (∩i ∈ 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) ∈ (∪i ∈ I. X(i)) guarantees (∪i ∈ 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)\
      ==> (⊔i ∈ I. F(i)) ∈ 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 ∈ program ∧ (∀H ∈ program. H ∈ X ⟶ (F component_of H ⟶ H ∈ 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 ⟶ H ∈ X) ∧ F ∈ program ∧ H ∈ 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)
   ⟶ (∀F ∈ FF. ((⊔F ∈ FF. F) ∈  wg(F,X)) ⟷ ((⊔F ∈ FF. F) ∈ 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)\
      ==> F: (A co A ∪ B) guarantees (A ⟼ (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