# HG changeset patch
# User paulson
# Date 935571302 -7200
# Node ID a22efb7a522b2c0c2e766e44b321221f44d4afa9
# Parent  1b4d7a851b343e6d4945573ab19090d530dd0030
new guarantees laws; also better natural deduction style for old ones

diff -r 1b4d7a851b34 -r a22efb7a522b src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Wed Aug 25 10:53:19 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Wed Aug 25 10:55:02 1999 +0200
@@ -247,14 +247,29 @@
 \    ==> (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";
+bind_thm ("guarantees_JN_INT", ballI RS result());
 
 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";
+bind_thm ("guarantees_JN_UN", ballI RS result());
+
+
+(*** guarantees laws for breaking down the program, by lcp ***)
+
+Goalw [guarantees_def]
+    "F: X guar Y | G: X guar Y ==> F Join G: X guar Y";
+by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
+by (Blast_tac 1);
+qed "guarantees_Join_I";
+
+Goalw [guarantees_def]
+     "[| i : I;  F i: X guar Y |] ==> (JN i:I. (F i)) : X guar Y";
+by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
+by (Blast_tac 1);
+qed "guarantees_JN_I";
 
 
 (*** well-definedness ***)