# HG changeset patch
# User paulson
# Date 935571669 -7200
# Node ID d54e871d77e0d1b2819f0a5285bac29f5c478f1e
# Parent  4fa705cedbdb0b7ad132fec24a0a866d8ae59fe7
new guarantees laws; also better natural deduction style for old ones

diff -r 4fa705cedbdb -r d54e871d77e0 src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Wed Aug 25 10:59:32 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Wed Aug 25 11:01:09 1999 +0200
@@ -52,7 +52,7 @@
 \     (PLam I F : (lift_set i A) co (lift_set i B))  =  \
 \     (F i : A co B)";
 by (asm_simp_tac (simpset() addsimps [PLam_def, constrains_JN]) 1);
-by (blast_tac (claset() addIs [lift_prog_constrains_eq RS iffD1, 
+by (blast_tac (claset() addIs [lift_prog_constrains RS iffD1, 
 			       constrains_imp_lift_prog_constrains]) 1);
 qed "PLam_constrains";
 
@@ -263,15 +263,20 @@
 (*** guarantees properties ***)
 
 Goalw [PLam_def]
+     "[| i : I;  lift_prog i (F i): X guar Y |] ==> (PLam I F) : X guar Y";
+by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
+qed "guarantees_PLam_I";
+
+Goalw [PLam_def]
     "[| ALL i:I. F i : X guar Y |] \
 \    ==> (PLam I F) : (INT i: I. lift_prog i `` X) \
 \                 guar (INT i: I. lift_prog i `` Y)";
 by (blast_tac (claset() addIs [guarantees_JN_INT, lift_prog_guarantees]) 1);
-qed "guarantees_PLam_INT";
+bind_thm ("guarantees_PLam_INT", ballI RS result());
 
 Goalw [PLam_def]
     "[| ALL i:I. F i : X guar Y |] \
 \    ==> (PLam I F) : (UN i: I. lift_prog i `` X) \
 \                 guar (UN i: I. lift_prog i `` Y)";
 by (blast_tac (claset() addIs [guarantees_JN_UN, lift_prog_guarantees]) 1);
-qed "guarantees_PLam_UN";
+bind_thm ("guarantees_PLam_UN", ballI RS result());