# HG changeset patch
# User paulson
# Date 907925086 -7200
# Node ID fc2c299187c01f249b636d8a02dfc53a8b846a59
# Parent  9baad17accb9eecf099076e0f2f8ef19f3a5fa6e
new guarantees laws

diff -r 9baad17accb9 -r fc2c299187c0 src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Fri Oct 09 11:16:52 1998 +0200
+++ b/src/HOL/UNITY/Comp.ML	Fri Oct 09 11:24:46 1998 +0200
@@ -138,6 +138,26 @@
 by (Blast_tac 1);
 qed "combining2";
 
+Goalw [guarantees_def]
+     "ALL z:I. F : A guarantees (B z) ==> F : A guarantees (INT z:I. B z)";
+by (Blast_tac 1);
+qed "all_guarantees";
+
+Goalw [guarantees_def]
+     "EX z:I. F : A guarantees (B z) ==> F : A guarantees (UN z:I. B z)";
+by (Blast_tac 1);
+qed "ex_guarantees";
+
+Goalw [guarantees_def, component_def]
+      "(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)";
+by (Blast_tac 1);
+qed "guarantees_eq";
+
+val prems = Goalw [guarantees_def, component_def]
+      "(!!G. F Join G : A ==> F Join G : B) ==> F : A guarantees B";
+by (blast_tac (claset() addIs prems) 1);
+qed "guaranteesI";
+
 
 (*** well-definedness ***)