# Theory Guar

theory Guar
imports Comp
```(*  Title:      ZF/UNITY/Guar.thy
Author:     Sidi O Ehmety, Computer Laboratory

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 ∈ 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 "⊔"*)
welldef :: i  where
"welldef == {F ∈ program. Init(F) ≠ 0}"

definition
refines :: "[i, i, i] => o" ("(3_ 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"  ("(3_ 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"

lemma ex1 [rule_format]:
"GG ∈ Fin(program)
==> ex_prop(X) ⟶ GG ∩ X≠0 ⟶ OK(GG, (%G. G)) ⟶(⨆G ∈ GG. G) ∈ X"
apply (unfold ex_prop_def)
apply (erule Fin_induct)
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 (auto intro: ok_sym)
done

(*Chandy & 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"
apply (unfold 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)"
apply (unfold uv_prop_def)
apply (erule Fin_induct)
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 & 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"

lemma guaranteesD:
"[| F ∈ X guarantees Y;  F ok G;  F ⊔ G ∈ X; G ∈ program |]
==> F ⊔ G ∈ Y"

(*This version of guaranteesD matches more easily in the conclusion
The major premise can no longer be  F⊆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"

lemma guarantees_weaken:
"[| F ∈ X guarantees X'; Y ⊆ X; X' ⊆ Y' |] ==> F ∈ Y guarantees Y'"

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 safe
apply (blast intro: elim: equalityE)
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 ∈ Z guarantees (X ∩ Y)"

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 (!!i. i ∈ I ==> F ∈ 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 [| F ∈ X guarantees Y i; i ∈ 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 ⊔ G: (U ∩ X) guarantees (V ∩ Y)"

apply (unfold guar_def)
apply (simp (no_asm))
apply safe
apply (subgoal_tac "F ⊔ G ⊔ Ga = G ⊔ (F ⊔ Ga) ")
done

lemma guarantees_Join_Un:
"[| F ∈ U guarantees V;  G ∈ X guarantees Y; F ok G |]
==> F ⊔ G: (U ∪ X) guarantees (V ∪ Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
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))
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 (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"
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 & 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 (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)"

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 (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 (drule_tac x = "F ⊔ Ga" in bspec)
apply (simp (no_asm))
apply (simp (no_asm_use))
apply safe
apply (subgoal_tac "F ⊔ G = G ⊔ F")
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 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

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 (rule stable_Join_Always1)
apply (auto simp add: programify_def initially_def)
done