Theory Guar

(*  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‹Guarantees Specifications›

theory Guar
imports Comp
begin

instance program :: (type) order
  by standard (auto simp add: program_less_le dest: component_antisym intro: component_trans)

text‹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 ∈ X & (∀F G. F ok G --> (F ∈ X & G ∈ X) = (F⊔G ∈ X))"


text‹Guarantees properties›

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 ==
     ∀H. (F ok H & G ok H & F⊔H ∈ welldef ∩ X) --> 
         (G⊔H ∈ welldef ∩ 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 ∈ welldef ∩ X --> G ∈ welldef ∩ X"


lemma OK_insert_iff:
     "(OK (insert i I) F) = 
      (if i ∈ 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‹Existential Properties›

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 
      ⟹ 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 = 
      (∀GG. finite GG & GG ∩ X ≠ {} & OK GG (%G. G)--> (⨆G ∈ GG. G) ∈ 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‹Universal Properties›

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 = 
      (∀GG. finite GG ∧ GG ⊆ X ∧ OK GG (λG. G) ⟶ (⨆G ∈ GG. G) ∈ X)"
by (blast intro: uv1 uv2)

subsection‹Guarantees›

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 ⊆ 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‹Distributive Laws.  Re-Orient to Perform Miniscoping›

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 ∈ Z guarantees (X ∩ 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 ∈ (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) ==> 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)


subsection‹Guarantees: Additional 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 (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⊔G ∈ (U ∪ X) guarantees (V ∪ 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) ∈ (⋂(X ` I)) guarantees (⋂(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) ∈ (⋃(X ` I)) guarantees (⋃(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‹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"
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 |]  
      ==> (⨆i ∈ I. (F i)) ∈ 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  
      ==> (∀H. F ok H & G ok H & F⊔H ∈ X --> G⊔H ∈ X)  
              = (F ∈ X --> G ∈ X)"
by (unfold strict_ex_prop_def, auto)

lemma strict_ex_refine_lemma_v: 
     "strict_ex_prop X  
      ==> (∀H. F ok H & G ok H & F⊔H ∈ welldef & F⊔H ∈ X --> G⊔H ∈ X) =  
          (F ∈ welldef ∩ X --> G ∈ 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;   
         ∀H. F ok H & G ok H & F⊔H ∈ welldef ∩ X --> G⊔H ∈ 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 ==> 
      (∀H. F ok H & G ok H & F⊔H ∈ X --> G⊔H ∈ X) = (F ∈ X --> G ∈ X)"
by (unfold strict_uv_prop_def, blast)

lemma strict_uv_refine_lemma_v: 
     "strict_uv_prop X  
      ==> (∀H. F ok H & G ok H & F⊔H ∈ welldef & F⊔H ∈ X --> G⊔H ∈ X) =  
          (F ∈ welldef ∩ X --> G ∈ 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;   
         ∀H. F ok H & G ok H & F⊔H ∈ welldef ∩ X --> 
             G⊔H ∈ 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)
          ⟶ (∀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, 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‹Equivalence with the other definition of wx›

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