*** empty log message ***

--- a/src/HOL/UNITY/Comp.ML	Fri Mar 02 13:18:31 2001 +0100
+++ b/src/HOL/UNITY/Comp.ML	Fri Mar 02 13:18:56 2001 +0100
@@ -4,12 +4,12 @@
     Copyright   1998  University of Cambridge
 
 Composition
+From Chandy and Sanders, "Reasoning About Program Composition"
 
-From Chandy and Sanders, "Reasoning About Program Composition"
+Revised by Sidi Ehmety on January 2001
+
 *)
-
-(*** component ***)
-
+(*** component <= ***)
 Goalw [component_def]
      "H <= F | H <= G ==> H <= (F Join G)";
 by Auto_tac;
@@ -214,3 +214,50 @@
 by (Blast_tac 1);
 qed "Increasing_preserves_Stable";
 
+(** component_of **)
+
+(*  component_of is stronger than <= *)
+Goalw [component_def, component_of_def]
+"F component_of H ==> F <= H";
+by (Blast_tac 1);
+qed "component_of_imp_component";
+
+
+(* component_of satisfies many of the <='s properties *)
+Goalw [component_of_def]
+"F component_of F";
+by (res_inst_tac [("x", "SKIP")] exI 1);
+by Auto_tac;
+qed "component_of_refl";
+
+Goalw [component_of_def]
+"SKIP component_of F";
+by Auto_tac;
+qed "component_of_SKIP";
+
+Addsimps [component_of_refl, component_of_SKIP];
+
+Goalw [component_of_def]
+"[| F component_of G; G component_of H |] ==> F component_of H";
+by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
+qed "component_of_trans";
+
+bind_thm ("strict_component_of_eq", strict_component_of_def RS meta_eq_to_obj_eq);
+
+(** localize **)
+Goalw [localize_def]
+ "Init (localize v F) = Init F";
+by (Simp_tac 1);
+qed "localize_Init_eq";
+
+Goalw [localize_def]
+ "Acts (localize v F) = Acts F";
+by (Simp_tac 1);
+qed "localize_Acts_eq";
+
+Goalw [localize_def]
+ "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)";
+by Auto_tac;
+qed "localize_AllowedActs_eq";
+
+Addsimps [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq];

--- a/src/HOL/UNITY/Comp.thy	Fri Mar 02 13:18:31 2001 +0100
+++ b/src/HOL/UNITY/Comp.thy	Fri Mar 02 13:18:56 2001 +0100
@@ -4,8 +4,13 @@
     Copyright   1998  University of Cambridge
 
 Composition
+From Chandy and Sanders, "Reasoning About Program Composition",
+Technical Report 2000-003, University of Florida, 2000.
 
-From Chandy and Sanders, "Reasoning About Program Composition"
+Revised by Sidi Ehmety on January  2001 
+
+Added: a strong form of the <= relation (component_of) and localize 
+
 *)
 
 Comp = Union +
@@ -14,16 +19,26 @@
   program :: (term)ord
 
 defs
-
   component_def   "F <= H == EX G. F Join G = H"
-
   strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
 
+
 constdefs
+  component_of :: "'a program=>'a program=> bool"
+                                    (infixl "component'_of" 50)
+  "F component_of H == EX G. F ok G & F Join G = H"
+
+  strict_component_of :: "'a program\\<Rightarrow>'a program=> bool"
+                                    (infixl "strict'_component'_of" 50)
+  "F strict_component_of H == F component_of H & F~=H"
+  
   preserves :: "('a=>'b) => 'a program set"
     "preserves v == INT z. stable {s. v s = z}"
 
+  localize  :: "('a=>'b) => 'a program => 'a program"
+  "localize v F == mk_program(Init F, Acts F,
+			      AllowedActs F Int (UN G:preserves v. Acts G))"
+
   funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
-    "funPair f g == %x. (f x, g x)"
-
+  "funPair f g == %x. (f x, g x)"
 end

--- a/src/HOL/UNITY/Guar.ML	Fri Mar 02 13:18:31 2001 +0100
+++ b/src/HOL/UNITY/Guar.ML	Fri Mar 02 13:18:56 2001 +0100
@@ -6,62 +6,76 @@
 Guarantees, etc.
 
 From Chandy and Sanders, "Reasoning About Program Composition"
+Revised by Sidi Ehmety on January 2001
 *)
 
+Goal "(OK (insert i I) F) = (if i:I then OK I F else OK I F & (F i ok JOIN I F))";
+by (auto_tac (claset() addIs [ok_sym], 
+              simpset() addsimps [OK_iff_ok]));
+qed "OK_insert_iff";
+
+
+
 (*** existential properties ***)
-
 Goalw [ex_prop_def]
-     "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
+ "[| ex_prop X; finite GG |] ==> \
+\    GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X";
 by (etac finite_induct 1);
-by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
+by (auto_tac (claset(), simpset() addsimps [OK_insert_iff,Int_insert_left]));
 qed_spec_mp "ex1";
 
+
 Goalw [ex_prop_def]
-     "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
+     "ALL GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X ==> ex_prop X";
 by (Clarify_tac 1);
 by (dres_inst_tac [("x", "{F,G}")] spec 1);
-by Auto_tac;
+by (auto_tac (claset() addDs [ok_sym], 
+              simpset() addsimps [OK_iff_ok]));
 qed "ex2";
 
+
 (*Chandy & Sanders take this as a definition*)
-Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
+Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)";
 by (blast_tac (claset() addIs [ex1,ex2]) 1);
 qed "ex_prop_finite";
 
+
 (*Their "equivalent definition" given at the end of section 3*)
-Goal "ex_prop X = (ALL G. G:X = (ALL H. G <= H --> H: X))";
+Goal
+ "ex_prop X = (ALL G. G:X = (ALL H. (G component_of H) --> H: X))";
 by Auto_tac;
-by (rewrite_goals_tac [ex_prop_def, component_def]);
-by (Blast_tac 1);
+by (rewrite_goals_tac 
+          [ex_prop_def, component_of_def]);
 by Safe_tac;
-by (stac Join_commute 2);
-by (ALLGOALS Blast_tac);
+by (stac Join_commute 3);
+by (dtac  ok_sym 3);
+by (REPEAT(Blast_tac 1));
 qed "ex_prop_equiv";
 
 
 (*** universal properties ***)
-
 Goalw [uv_prop_def]
-     "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
+     "[| uv_prop X; finite GG |] ==>  \
+\  GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X";
 by (etac finite_induct 1);
-by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
+by (auto_tac (claset(), simpset() addsimps 
+           [Int_insert_left, OK_insert_iff]));
 qed_spec_mp "uv1";
 
 Goalw [uv_prop_def]
-     "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X  ==> uv_prop X";
+     "ALL GG. finite GG & GG <= X & OK GG (%G. G)-->(JN G:GG. G):X  ==> uv_prop X";
 by (rtac conjI 1);
 by (Clarify_tac 2);
 by (dres_inst_tac [("x", "{F,G}")] spec 2);
 by (dres_inst_tac [("x", "{}")] spec 1);
-by Auto_tac;
+by (auto_tac (claset() addDs [ok_sym], simpset() addsimps [OK_iff_ok]));
 qed "uv2";
 
 (*Chandy & Sanders take this as a definition*)
-Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
+Goal "uv_prop X = (ALL GG. finite GG & GG <= X & OK GG (%G. G)--> (JN G:GG. G): X)";
 by (blast_tac (claset() addIs [uv1,uv2]) 1);
 qed "uv_prop_finite";
 
-
 (*** guarantees ***)
 
 val prems = Goal
@@ -99,12 +113,35 @@
 by (Blast_tac 1);
 qed "subset_imp_guarantees";
 
-(*Remark at end of section 4.1
-Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
+(*Remark at end of section 4.1 *)
+
+Goalw [guar_def] "ex_prop Y ==> (Y = UNIV guarantees Y)";
+by (full_simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
+by Safe_tac;
+by (dres_inst_tac [("x", "x")] spec 1);
+by (dres_inst_tac [("x", "x")] spec 2);
+by (dtac sym 2);
+by (ALLGOALS(etac iffE));
+by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
+by (REPEAT(Blast_tac 1));
+qed "ex_prop_imp";
+
+Goalw [guar_def] "(Y = UNIV guarantees Y) ==> ex_prop(Y)";
 by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
+by Safe_tac;
+by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
+by (dtac sym 2);
+by (ALLGOALS(etac equalityE));
+by (REPEAT(Blast_tac 1));
+qed "guarantees_imp";
+
+Goal "(ex_prop Y) = (Y = UNIV guarantees Y)";
+by (rtac iffI 1);
+by (rtac ex_prop_imp 1);
+by (rtac guarantees_imp 2);
+by (ALLGOALS(Asm_simp_tac));
 qed "ex_prop_equiv2";
-*)
+
 
 (** Distributive laws.  Re-orient to perform miniscoping **)
 
@@ -177,6 +214,7 @@
 by (Blast_tac 1);
 qed "ex_guarantees";
 
+
 (*** Additional guarantees laws, by lcp ***)
 
 Goalw [guar_def]
@@ -279,20 +317,23 @@
 by (Blast_tac 1);
 qed "refines_refl";
 
-Goalw [refines_def]
-     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X";
+(* Goalw [refines_def]
+     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X"; 
 by Auto_tac;
-qed "refines_trans";
+qed "refines_trans"; *)
+
+
 
 Goalw [strict_ex_prop_def]
      "strict_ex_prop X \
-\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
-by (Blast_tac 1);
+\     ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) \
+\             = (F:X --> G:X)";
+by Auto_tac;
 qed "strict_ex_refine_lemma";
 
 Goalw [strict_ex_prop_def]
      "strict_ex_prop X \
-\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
+\     ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \
 \         (F: welldef Int X --> G:X)";
 by Safe_tac;
 by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
@@ -300,7 +341,7 @@
 qed "strict_ex_refine_lemma_v";
 
 Goal "[| strict_ex_prop X;  \
-\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
+\        ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \
 \     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
 by (res_inst_tac [("x","SKIP")] allE 1
     THEN assume_tac 1);
@@ -312,13 +353,13 @@
 
 Goalw [strict_uv_prop_def]
      "strict_uv_prop X \
-\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
+\     ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)";
 by (Blast_tac 1);
 qed "strict_uv_refine_lemma";
 
 Goalw [strict_uv_prop_def]
      "strict_uv_prop X \
-\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
+\     ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \
 \         (F: welldef Int X --> G:X)";
 by Safe_tac;
 by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
@@ -327,10 +368,165 @@
 qed "strict_uv_refine_lemma_v";
 
 Goal "[| strict_uv_prop X;  \
-\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
+\        ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \
 \     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
 by (res_inst_tac [("x","SKIP")] allE 1
     THEN assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
 					   strict_uv_refine_lemma_v]) 1);
 qed "uv_refinement_thm";
+
+(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
+Goalw [guar_def, component_of_def]
+"(F:X guarantees Y) = (ALL H. H:X \\<longrightarrow> (F component_of H \\<longrightarrow> H:Y))";
+by Auto_tac;
+qed "guarantees_equiv";
+
+Goalw [wg_def] "!!X. F:(X guarantees Y) ==> X <= (wg F Y)";
+by Auto_tac;
+qed "wg_weakest";
+
+Goalw [wg_def, guar_def] "F:((wg F Y) guarantees Y)";
+by (Blast_tac 1);
+qed "wg_guarantees";
+
+Goalw [wg_def]
+  "(H: wg F X) = (F component_of H --> H:X)";
+by (simp_tac (simpset() addsimps [guarantees_equiv]) 1);
+by (rtac iffI 1);
+by (res_inst_tac [("x", "{H}")] exI 2);
+by (REPEAT(Blast_tac 1));
+qed "wg_equiv";
+
+
+Goal
+"F component_of H ==> (H:wg F X) = (H:X)";
+by (asm_simp_tac (simpset() addsimps [wg_equiv]) 1);
+qed "component_of_wg";
+
+
+Goal
+"ALL FF. finite FF & FF Int X ~= {} --> OK FF (%F. F) \
+\  --> (ALL F:FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))";
+by (Clarify_tac 1);
+by (subgoal_tac "F component_of (JN F:FF. F)" 1);
+by (dres_inst_tac [("X", "X")] component_of_wg 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [component_of_def]) 1);
+by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1);
+by (auto_tac (claset() addIs [JN_Join_diff] addDs [ok_sym], 
+              simpset() addsimps [OK_iff_ok]));
+qed "wg_finite";
+
+Goal "ex_prop X ==> (F:X) = (ALL H. H : wg F X)";
+by (full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1);
+by (Blast_tac 1);
+qed "wg_ex_prop";
+
+(** From Charpentier and Chandy "Theorems About Composition" **)
+(* Proposition 2 *)
+Goalw [wx_def] "(wx X)<=X";
+by Auto_tac;
+qed "wx_subset";
+
+Goalw [wx_def]
+"ex_prop (wx X)";
+by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
+by Safe_tac;
+by (Blast_tac 1);
+by Auto_tac;
+qed "wx_ex_prop";
+
+Goalw [wx_def]
+"ALL Z. Z<= X --> ex_prop Z --> Z <= wx X";
+by Auto_tac;
+qed "wx_weakest";
+
+
+(* Proposition 6 *)
+Goalw [ex_prop_def]
+ "ex_prop({F. ALL G. F ok G --> F Join G:X})";
+by Safe_tac;
+by (dres_inst_tac [("x", "G Join Ga")] spec 1);
+by (force_tac (claset(), simpset() addsimps [ok_Join_iff1, Join_assoc]) 1);
+by (dres_inst_tac [("x", "F Join Ga")] spec 1);
+by (full_simp_tac (simpset() addsimps [ok_Join_iff1]) 1);
+by Safe_tac;
+by (asm_simp_tac (simpset() addsimps [ok_commute]) 1);
+by (subgoal_tac "F Join G = G Join F" 1);
+by (asm_simp_tac (simpset() addsimps [Join_assoc]) 1);
+by (simp_tac (simpset() addsimps [Join_commute]) 1);
+qed "wx'_ex_prop";
+
+(* Equivalence with the other definition of wx *)
+
+Goalw [wx_def]
+ "wx X = {F. ALL G. F ok G --> (F Join G):X}";
+by Safe_tac;
+by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1);
+by (dres_inst_tac [("x", "x")] spec 1);
+by (dres_inst_tac [("x", "G")] spec 1);
+by (forw_inst_tac [("c", "x Join G")] subsetD 1);
+by Safe_tac;
+by (Simp_tac 1);
+by (res_inst_tac [("x", "{F. ALL G. F ok G --> F Join G:X}")] exI 1);
+by Safe_tac;
+by (rtac wx'_ex_prop 2);
+by (rotate_tac 1 1);
+by (dres_inst_tac [("x", "SKIP")] spec 1);
+by Auto_tac;
+qed "wx_equiv";
+
+
+(* Propositions 7 to 11 are about this second definition of wx. And
+   they are the same as the ones proved for the first definition of wx by equivalence *)
+   
+(* Proposition 12 *)
+(* Main result of the paper *)
+Goalw [guar_def] 
+   "(X guarantees Y) = wx(-X Un Y)";
+by (simp_tac (simpset() addsimps [wx_equiv]) 1);
+qed "guarantees_wx_eq";
+
+(* {* Corollary, but this result has already been proved elsewhere *}
+ "ex_prop(X guarantees Y)";
+  by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1);
+  qed "guarantees_ex_prop";
+*)
+
+(* Rules given in section 7 of Chandy and Sander's
+    Reasoning About Program composition paper *)
+
+Goal "Init F <= A ==> F:(stable A) guarantees (Always A)";
+by (rtac guaranteesI 1);
+by (simp_tac (simpset() addsimps [Join_commute]) 1);
+by (rtac stable_Join_Always1 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() 
+     addsimps [invariant_def, Join_stable])));
+qed "stable_guarantees_Always";
+
+(* To be moved to WFair.ML *)
+Goal "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B";
+by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1);
+by (dres_inst_tac [("B", "A-B")] transient_strengthen 2);
+by (rtac (ensuresI RS leadsTo_Basis) 3);
+by (ALLGOALS(Blast_tac));
+qed "leadsTo_Basis'";
+
+
+
+Goal "F:transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))";
+by (rtac guaranteesI 1);
+by (rtac leadsTo_Basis' 1);
+by (dtac constrains_weaken_R 1);
+by (assume_tac 2);
+by (Blast_tac 1);
+by (blast_tac (claset() addIs [Join_transient_I1]) 1);
+qed "constrains_guarantees_leadsTo";
+
+
+
+
+
+
+

--- a/src/HOL/UNITY/Guar.thy	Fri Mar 02 13:18:31 2001 +0100
+++ b/src/HOL/UNITY/Guar.thy	Fri Mar 02 13:18:56 2001 +0100
@@ -5,7 +5,17 @@
 
 Guarantees, etc.
 
-From Chandy and Sanders, "Reasoning About Program Composition"
+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.
+
 *)
 
 Guar = Comp +
@@ -20,33 +30,42 @@
     case, proving equivalence with Chandy and Sanders's n-ary definitions*)
 
   ex_prop  :: 'a program set => bool
-   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
+   "ex_prop X == ALL F G. F ok G -->F:X | G: X --> (F Join G) : X"
 
   strict_ex_prop  :: 'a program set => bool
-   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
+   "strict_ex_prop X == ALL F G.  F ok G --> (F:X | G: X) = (F Join G : X)"
 
   uv_prop  :: 'a program set => bool
-   "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"
+   "uv_prop X == SKIP : X & (ALL F G. F ok G --> F:X & G: X --> (F Join G) : X)"
 
   strict_uv_prop  :: 'a program set => bool
-   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
-
-  (*Ill-defined programs can arise through "Join"*)
-  welldef :: 'a program set  
-   "welldef == {F. Init F ~= {}}"
+   "strict_uv_prop X == SKIP : X & (ALL F G. F ok G -->(F:X & G: X) = (F Join G : X))"
 
   guar :: ['a program set, 'a program set] => 'a program set
           (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
    "X guarantees Y == {F. ALL G. F ok G --> F Join G : X --> F Join G : Y}"
+  
 
+  (* Weakest guarantees *)
+   wg :: ['a program, 'a program set] =>  'a program set
+  "wg F Y == Union({X. F:X guarantees Y})"
+
+   (* Weakest existential property stronger than X *)
+   wx :: "('a program) set => ('a program)set"
+   "wx X == Union({Y. Y<=X & ex_prop Y})"
+  
+  (*Ill-defined programs can arise through "Join"*)
+  welldef :: 'a program set  
+  "welldef == {F. Init F ~= {}}"
+  
   refines :: ['a program, 'a program, 'a program set] => bool
 			("(3_ refines _ wrt _)" [10,10,10] 10)
-   "G refines F wrt X ==
-      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
+  "G refines F wrt X ==
+   ALL H. (F ok H  & G ok H & F Join H:welldef Int X) --> (G Join H:welldef Int X)"
 
   iso_refines :: ['a program, 'a program, 'a program set] => bool
-			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
-   "G iso_refines F wrt X ==
-      F : welldef Int X --> G : welldef Int X"
+                              ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
+  "G iso_refines F wrt X ==
+   F : welldef Int X --> G : welldef Int X"
 
 end