src/HOL/UNITY/Comp.ML

 by (blast_tac (claset() addIs [Join_SKIP_right]) 1);
 qed "component_refl";
 
 AddIffs [component_SKIP, component_refl];
 
+Goal "F component SKIP ==> F = SKIP";
+by (auto_tac (claset() addSIs [program_equalityI],
+	      simpset() addsimps [component_eq_subset]));
+qed "SKIP_minimal";
+
 Goalw [component_def] "F component (F Join G)";
 by (Blast_tac 1);
 qed "component_Join1";
 
 Goalw [component_def] "G component (F Join G)";

 
 Goalw [component_def]
       "F component H = (EX G. F Join G = H & Disjoint F G)";
 by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
 qed "component_eq";
+
+Goal "((F Join G) component H) = (F component H & G component H)";
+by (simp_tac (simpset() addsimps [component_eq_subset, Acts_Join]) 1);
+by (Blast_tac 1);
+qed "Join_component_iff";
 
 
 (*** existential properties ***)
 
 Goalw [ex_prop_def]

 qed "uv_prop_finite";
 
 
 (*** guarantees ***)
 
-(*This equation is more intuitive than the official definition*)
-Goal "(F : X guar Y) = \
-\     (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
-by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
-by (Blast_tac 1);
-qed "guarantees_eq";
-
-Goalw [guarantees_def] "X <= Y ==> X guar Y = UNIV";
-by (Blast_tac 1);
-qed "subset_imp_guarantees_UNIV";
-
-(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-Goalw [guarantees_def] "X <= Y ==> F : X guar Y";
-by (Blast_tac 1);
-qed "subset_imp_guarantees";
-
-(*Remark at end of section 4.1*)
-Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guar Y)";
-by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
-qed "ex_prop_equiv2";
-
-(** Distributive laws.  Re-orient to perform miniscoping **)
-
-Goalw [guarantees_def]
-     "(UN X:XX. X) guar Y = (INT X:XX. X guar Y)";
-by (Blast_tac 1);
-qed "guarantees_UN_left";
-
-Goalw [guarantees_def]
-    "(X Un Y) guar Z = (X guar Z) Int (Y guar Z)";
-by (Blast_tac 1);
-qed "guarantees_Un_left";
-
-Goalw [guarantees_def]
-     "X guar (INT Y:YY. Y) = (INT Y:YY. X guar Y)";
-by (Blast_tac 1);
-qed "guarantees_INT_right";
-
-Goalw [guarantees_def]
-    "Z guar (X Int Y) = (Z guar X) Int (Z guar Y)";
-by (Blast_tac 1);
-qed "guarantees_Int_right";
-
-Goalw [guarantees_def] "(X guar Y) = (UNIV guar (-X Un Y))";
-by (Blast_tac 1);
-qed "shunting";
-
-Goalw [guarantees_def] "(X guar Y) = -Y guar -X";
-by (Blast_tac 1);
-qed "contrapositive";
-
-(** The following two can be expressed using intersection and subset, which
-    is more faithful to the text but looks cryptic.
-**)
-
-Goalw [guarantees_def]
-    "[| F : V guar X;  F : (X Int Y) guar Z |]\
-\    ==> F : (V Int Y) guar Z";
-by (Blast_tac 1);
-qed "combining1";
-
-Goalw [guarantees_def]
-    "[| F : V guar (X Un Y);  F : Y guar Z |]\
-\    ==> F : V guar (X Un Z)";
-by (Blast_tac 1);
-qed "combining2";
-
-(** The following two follow Chandy-Sanders, but the use of object-quantifiers
-    does not suit Isabelle... **)
-
-(*Premise should be (!!i. i: I ==> F: X guar Y i) *)
-Goalw [guarantees_def]
-     "ALL i:I. F : X guar (Y i) ==> F : X guar (INT i:I. Y i)";
-by (Blast_tac 1);
-qed "all_guarantees";
-
-(*Premises should be [| F: X guar Y i; i: I |] *)
-Goalw [guarantees_def]
-     "EX i:I. F : X guar (Y i) ==> F : X guar (UN i:I. Y i)";
-by (Blast_tac 1);
-qed "ex_guarantees";
-
 val prems = Goal
      "(!!G. [| F Join G : X;  Disjoint F G |] ==> F Join G : Y) \
 \     ==> F : X guar Y";
 by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
 by (blast_tac (claset() addIs prems) 1);

 
 Goalw [guarantees_def, component_def]
      "[| F : X guar Y;  F Join G : X |] ==> F Join G : Y";
 by (Blast_tac 1);
 qed "guaranteesD";
+
+(*This equation is more intuitive than the official definition*)
+Goal "(F : X guar Y) = \
+\     (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
+by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
+by (Blast_tac 1);
+qed "guarantees_eq";
+
+Goalw [guarantees_def] "[| F: X guar X'; Y <= X; X' <= Y' |] ==> F: Y guar Y'";
+by (Blast_tac 1);
+qed "guarantees_weaken";
+
+Goalw [guarantees_def] "[| F: X guar Y; F component F' |] ==> F': X guar Y";
+by (blast_tac (claset() addIs [component_trans]) 1);
+qed "guarantees_weaken_prog";
+
+Goalw [guarantees_def] "X <= Y ==> X guar Y = UNIV";
+by (Blast_tac 1);
+qed "subset_imp_guarantees_UNIV";
+
+(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
+Goalw [guarantees_def] "X <= Y ==> F : X guar Y";
+by (Blast_tac 1);
+qed "subset_imp_guarantees";
+
+(*Remark at end of section 4.1*)
+Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guar Y)";
+by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
+by (blast_tac (claset() addEs [equalityE]) 1);
+qed "ex_prop_equiv2";
+
+(** Distributive laws.  Re-orient to perform miniscoping **)
+
+Goalw [guarantees_def]
+     "(UN X:XX. X) guar Y = (INT X:XX. X guar Y)";
+by (Blast_tac 1);
+qed "guarantees_UN_left";
+
+Goalw [guarantees_def]
+    "(X Un Y) guar Z = (X guar Z) Int (Y guar Z)";
+by (Blast_tac 1);
+qed "guarantees_Un_left";
+
+Goalw [guarantees_def]
+     "X guar (INT Y:YY. Y) = (INT Y:YY. X guar Y)";
+by (Blast_tac 1);
+qed "guarantees_INT_right";
+
+Goalw [guarantees_def]
+    "Z guar (X Int Y) = (Z guar X) Int (Z guar Y)";
+by (Blast_tac 1);
+qed "guarantees_Int_right";
+
+Goalw [guarantees_def] "(X guar Y) = (UNIV guar (-X Un Y))";
+by (Blast_tac 1);
+qed "shunting";
+
+Goalw [guarantees_def] "(X guar Y) = -Y guar -X";
+by (Blast_tac 1);
+qed "contrapositive";
+
+(** The following two can be expressed using intersection and subset, which
+    is more faithful to the text but looks cryptic.
+**)
+
+Goalw [guarantees_def]
+    "[| F : V guar X;  F : (X Int Y) guar Z |]\
+\    ==> F : (V Int Y) guar Z";
+by (Blast_tac 1);
+qed "combining1";
+
+Goalw [guarantees_def]
+    "[| F : V guar (X Un Y);  F : Y guar Z |]\
+\    ==> F : V guar (X Un Z)";
+by (Blast_tac 1);
+qed "combining2";
+
+(** The following two follow Chandy-Sanders, but the use of object-quantifiers
+    does not suit Isabelle... **)
+
+(*Premise should be (!!i. i: I ==> F: X guar Y i) *)
+Goalw [guarantees_def]
+     "ALL i:I. F : X guar (Y i) ==> F : X guar (INT i:I. Y i)";
+by (Blast_tac 1);
+qed "all_guarantees";
+
+(*Premises should be [| F: X guar Y i; i: I |] *)
+Goalw [guarantees_def]
+     "EX i:I. F : X guar (Y i) ==> F : X guar (UN i:I. Y i)";
+by (Blast_tac 1);
+qed "ex_guarantees";
+
+(*** Additional guarantees laws, by lcp ***)
+
+Goalw [guarantees_def]
+    "[| F: U guar V;  G: X guar Y |] ==> F Join G: (U Int X) guar (V Int Y)";
+by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
+by (Blast_tac 1);
+qed "guarantees_Join_Int";
+
+Goalw [guarantees_def]
+    "[| F: U guar V;  G: X guar Y |] ==> F Join G: (U Un X) guar (V Un Y)";
+by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
+by (Blast_tac 1);
+qed "guarantees_Join_Un";
+
+Goal "((JOIN I F) component H) = (ALL i: I. F i component H)";
+by (simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1);
+by (Blast_tac 1);
+qed "JN_component_iff";
+
+Goalw [guarantees_def]
+    "[| ALL i:I. F i : X i guar Y i |] \
+\    ==> (JOIN I F) : (INTER I X) guar (INTER I Y)";
+by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
+by (Blast_tac 1);
+qed "guarantees_JN_INT";
+
+Goalw [guarantees_def]
+    "[| ALL i:I. F i : X i guar Y i |] \
+\    ==> (JOIN I F) : (UNION I X) guar (UNION I Y)";
+by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
+by (Blast_tac 1);
+qed "guarantees_JN_UN";
 
 
 (*** well-definedness ***)
 
 Goalw [welldef_def] "F Join G: welldef ==> F: welldef";