Finished proofs to end of section 5.1 of Chandy and Sanders

--- a/src/HOL/UNITY/Comp.ML	Mon Oct 05 10:22:49 1998 +0200
+++ b/src/HOL/UNITY/Comp.ML	Mon Oct 05 10:27:04 1998 +0200
@@ -8,8 +8,6 @@
 From Chandy and Sanders, "Reasoning About Program Composition"
 *)
 
-Addsimps [Join_SKIP, Join_absorb];
-
 (*split_all_tac causes a big blow-up*)
 claset_ref() := claset() delSWrapper "split_all_tac";
 
@@ -18,22 +16,26 @@
 
 (*** component ***)
 
+Goalw [component_def] "component SKIP F";
+by (blast_tac (claset() addIs [Join_SKIP_left]) 1);
+qed "component_SKIP";
+
 Goalw [component_def] "component F F";
-by (blast_tac (claset() addIs [Join_SKIP]) 1);
+by (blast_tac (claset() addIs [Join_SKIP_right]) 1);
 qed "component_refl";
 
-AddIffs [component_refl];
+AddIffs [component_SKIP, component_refl];
 
 Goalw [component_def] "[| component F G; component G H |] ==> component F H";
 by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
 qed "component_trans";
 
 Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G";
-auto();
+by Auto_tac;
 qed "componet_Acts";
 
 Goalw [component_def,Join_def] "component F G ==> Init G <= Init F";
-auto();
+by Auto_tac;
 qed "componet_Init";
 
 Goal "[| component F G; component G F |] ==> F=G";
@@ -51,11 +53,10 @@
 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 ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
 by (Clarify_tac 1);
 by (dres_inst_tac [("x", "{F,G}")] spec 1);
-auto();
+by Auto_tac;
 qed "ex2";
 
 (*Chandy & Sanders take this as a definition*)
@@ -65,8 +66,8 @@
 
 (*Their "equivalent definition" given at the end of section 3*)
 Goal "ex_prop X = (ALL G. G:X = (ALL H. component G H --> H: X))";
-auto();
-bws [ex_prop_def, component_def];
+by Auto_tac;
+by (rewrite_goals_tac [ex_prop_def, component_def]);
 by (Blast_tac 1);
 by Safe_tac;
 by (stac Join_commute 2);
@@ -84,11 +85,11 @@
 
 Goalw [uv_prop_def]
      "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X  ==> uv_prop X";
-br conjI 1;
+by (rtac conjI 1);
 by (Clarify_tac 2);
 by (dres_inst_tac [("x", "{F,G}")] spec 2);
 by (dres_inst_tac [("x", "{}")] spec 1);
-auto();
+by Auto_tac;
 qed "uv2";
 
 (*Chandy & Sanders take this as a definition*)
@@ -103,7 +104,107 @@
 by (Blast_tac 1);
 qed "subset_imp_guarantees";
 
+(*Remark at end of section 4.1*)
 Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guarantees Y)";
-ex_prop_equiv
+by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
+by (blast_tac (claset() addEs [equalityE]) 1);
+qed "ex_prop_equiv2";
+
+Goalw [guarantees_def]
+     "(INT X:XX. X guarantees Y) = (UN X:XX. X) guarantees Y";
+by (Blast_tac 1);
+qed "INT_guarantees_left";
+
+Goalw [guarantees_def]
+     "(INT Y:YY. X guarantees Y) = X guarantees (INT Y:YY. Y)";
+by (Blast_tac 1);
+qed "INT_guarantees_right";
+
+Goalw [guarantees_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
+by (Blast_tac 1);
+qed "shunting";
+
+Goalw [guarantees_def] "(X guarantees Y) = -Y guarantees -X";
+by (Blast_tac 1);
+qed "contrapositive";
+
+Goalw [guarantees_def]
+    "V guarantees X Int ((X Int Y) guarantees Z) <= (V Int Y) guarantees Z";
+by (Blast_tac 1);
+qed "combining1";
+
+Goalw [guarantees_def]
+    "V guarantees (X Un Y) Int (Y guarantees Z) <= V guarantees (X Un Z)";
+by (Blast_tac 1);
+qed "combining2";
+
+
+(*** well-definedness ***)
+
+Goalw [welldef_def] "F Join G: welldef ==> F: welldef";
+by Auto_tac;
+qed "Join_welldef_D1";
+
+Goalw [welldef_def] "F Join G: welldef ==> G: welldef";
+by Auto_tac;
+qed "Join_welldef_D2";
+
+(*** refinement ***)
+
+Goalw [refines_def] "F refines F wrt X";
 by (Blast_tac 1);
-qed "subset_imp_guarantees";
+qed "refines_refl";
+
+Goalw [refines_def]
+     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X";
+by (Blast_tac 1);
+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);
+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) = \
+\         (F: welldef Int X --> G:X)";
+by Safe_tac;
+by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
+by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset()));
+qed "strict_ex_refine_lemma_v";
+
+Goal "[| strict_ex_prop X;  \
+\        ALL 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_ex_refine_lemma_v]) 1);
+qed "ex_refinement_thm";
+
+Goalw [strict_uv_prop_def]
+     "strict_uv_prop X \
+\     ==> (ALL 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) = \
+\         (F: welldef Int X --> G:X)";
+by Safe_tac;
+by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
+by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2],
+	      simpset()));
+qed "strict_uv_refine_lemma_v";
+
+Goal "[| strict_uv_prop X;  \
+\        ALL 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";

--- a/src/HOL/UNITY/Comp.thy	Mon Oct 05 10:22:49 1998 +0200
+++ b/src/HOL/UNITY/Comp.thy	Mon Oct 05 10:27:04 1998 +0200
@@ -16,24 +16,35 @@
     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 --> (Join F G) : X"
+   "ex_prop X == ALL F 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) = (Join F G : X)"
+   "strict_ex_prop X == ALL F 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 --> (Join F G) : X)"
+   "uv_prop X == SKIP: X & (ALL F 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) = (Join F G : X))"
+   "strict_uv_prop X == SKIP: X & (ALL F G. (F:X & G: X) = (F Join G : X))"
 
-  compatible :: ['a program, 'a program] => bool
-   "compatible F G == Init F Int Init G ~= {}"
+  (*Ill-defined programs can arise through "Join"*)
+  welldef :: 'a program set  
+   "welldef == {F. Init F ~= {}}"
 
   component :: ['a program, 'a program] => bool
-   "component F H == EX G. Join F G = H"
+   "component F H == EX G. F Join G = H"
 
   guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
    "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
 
+  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"
+
+  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"
+
 end