src/HOL/UNITY/Lift_prog.ML
changeset 7840 e1fd12b864a1
parent 7826 c6a8b73b6c2a
child 7878 43b03d412b82
     1.1 --- a/src/HOL/UNITY/Lift_prog.ML	Wed Oct 13 12:03:22 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Wed Oct 13 12:04:11 1999 +0200
     1.3 @@ -426,17 +426,12 @@
     1.4  
     1.5  (*** guarantees properties ***)
     1.6  
     1.7 -val [xguary,project,lift_prog] =
     1.8  Goal "[| F : X guarantees Y;  \
     1.9 -\        !!G. lift_prog i F Join G : X' ==> F Join proj G : X;  \
    1.10 -\        !!G. [| F Join proj G : Y; lift_prog i F Join G : X'; \
    1.11 -\                Disjoint (lift_prog i F) G |] \
    1.12 -\             ==> lift_prog i F Join G : Y' |] \
    1.13 +\        projecting C (lift_map i) F X' X;  \
    1.14 +\        extending  C (lift_map i) F X' Y' Y |] \
    1.15  \     ==> lift_prog i F : X' guarantees Y'";
    1.16 -by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
    1.17 -by (etac project 1);
    1.18 -by (assume_tac 1);
    1.19 -by (assume_tac 1);
    1.20 +by (asm_simp_tac 
    1.21 +    (simpset() addsimps [lift_prog_correct, project_guarantees]) 1);
    1.22  qed "drop_prog_guarantees";
    1.23  
    1.24