# HG changeset patch
# User paulson
# Date 929608501 -7200
# Node ID 15d6c121d75f19ac7df01a0e6469bd114beac4d6
# Parent  0c92ccb3c4ba968490424f4840064e7d65c9937d
many new guarantees laws

diff -r 0c92ccb3c4ba -r 15d6c121d75f src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Thu Jun 17 10:34:23 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Thu Jun 17 10:35:01 1999 +0200
@@ -26,6 +26,11 @@
 
 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";
@@ -53,6 +58,11 @@
 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 ***)
 
@@ -110,6 +120,18 @@
 
 (*** 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);
+qed "guaranteesI";
+
+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)";
@@ -117,6 +139,14 @@
 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";
@@ -193,17 +223,38 @@
 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);
-qed "guaranteesI";
+(*** 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";
 
-Goalw [guarantees_def, component_def]
-     "[| F : X guar Y;  F Join G : X |] ==> F Join G : Y";
+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 "guaranteesD";
+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 ***)