# HG changeset patch
# User paulson
# Date 939809051 -7200
# Node ID e1fd12b864a1b668ccae8db22aec1247714d5992
# Parent  03fd460cb8b80737b3f62364477516c22bbc598d
projecting/extending version of drop_prog_guarantees

diff -r 03fd460cb8b8 -r e1fd12b864a1 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Wed Oct 13 12:03:22 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Wed Oct 13 12:04:11 1999 +0200
@@ -426,17 +426,12 @@
 
 (*** guarantees properties ***)
 
-val [xguary,project,lift_prog] =
 Goal "[| F : X guarantees Y;  \
-\        !!G. lift_prog i F Join G : X' ==> F Join proj G : X;  \
-\        !!G. [| F Join proj G : Y; lift_prog i F Join G : X'; \
-\                Disjoint (lift_prog i F) G |] \
-\             ==> lift_prog i F Join G : Y' |] \
+\        projecting C (lift_map i) F X' X;  \
+\        extending  C (lift_map i) F X' Y' Y |] \
 \     ==> lift_prog i F : X' guarantees Y'";
-by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
-by (etac project 1);
-by (assume_tac 1);
-by (assume_tac 1);
+by (asm_simp_tac 
+    (simpset() addsimps [lift_prog_correct, project_guarantees]) 1);
 qed "drop_prog_guarantees";