src/HOL/UNITY/Lift_prog.ML
changeset 7826 c6a8b73b6c2a
parent 7688 d106cad8f515
child 7840 e1fd12b864a1
     1.1 --- a/src/HOL/UNITY/Lift_prog.ML	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -3,13 +3,10 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1998  University of Cambridge
     1.6  
     1.7 -THESE PROOFS CAN BE REPLACED BY INVOCATIONS OF RESULTS FROM EXTEND.ML
     1.8 +Arrays of processes.  Many results are instances of those in Extend & Project.
     1.9  *)
    1.10  
    1.11  
    1.12 -val image_eqI' = read_instantiate_sg (sign_of thy)
    1.13 -                     [("x", "?ff(i := ?u)")] image_eqI;
    1.14 -
    1.15  (*** Basic properties ***)
    1.16  
    1.17  (** lift_set and drop_set **)
    1.18 @@ -283,6 +280,13 @@
    1.19  	      simpset() addsimps [invariant_def, lift_prog_stable]));
    1.20  qed "lift_prog_invariant";
    1.21  
    1.22 +Goal "[| lift_prog i F : A co B |] \
    1.23 +\     ==> F : (drop_set i A) co (drop_set i B)";
    1.24 +by (asm_full_simp_tac
    1.25 +    (simpset() addsimps [drop_set_correct, lift_prog_correct, 
    1.26 +			 lift_export extend_constrains_project_set]) 1);
    1.27 +qed "lift_prog_constrains_drop_set";
    1.28 +
    1.29  (*This one looks strange!  Proof probably is by case analysis on i=j.
    1.30    If i~=j then lift_prog j (F j) does nothing to lift_set i, and the 
    1.31    premise ensures A<=B.*)
    1.32 @@ -316,14 +320,14 @@
    1.33  by (asm_full_simp_tac
    1.34      (simpset() addsimps [drop_set_correct, drop_prog_correct, 
    1.35  			 lift_set_correct, lift_act_correct, 
    1.36 -			 lift_export Diff_project_co]) 1);
    1.37 -qed "Diff_drop_prog_co";
    1.38 +			 lift_export Diff_project_constrains]) 1);
    1.39 +qed "Diff_drop_prog_constrains";
    1.40  
    1.41  Goalw [stable_def]
    1.42       "[| (UN act:acts. Domain act) <= drop_set i C; \
    1.43  \        Diff G (lift_act i `` acts) : stable (lift_set i A) |]  \
    1.44  \     ==> Diff (drop_prog C i G) acts : stable A";
    1.45 -by (etac Diff_drop_prog_co 1);
    1.46 +by (etac Diff_drop_prog_constrains 1);
    1.47  by (assume_tac 1);
    1.48  qed "Diff_drop_prog_stable";
    1.49  
    1.50 @@ -487,11 +491,3 @@
    1.51      (simpset() addsimps [lift_set_correct, lift_prog_correct, 
    1.52  			 lift_export extend_guar_Always]) 1);
    1.53  qed "lift_prog_guar_Always";
    1.54 -
    1.55 -(*No analogue of this in Extend.ML!*)
    1.56 -Goal "[| lift_prog i F : A co B |] \
    1.57 -\     ==> F : (drop_set i A) co (drop_set i B)";
    1.58 -by (auto_tac (claset(), 
    1.59 -	      simpset() addsimps [constrains_def, drop_set_def]));
    1.60 -by (force_tac (claset() addSIs [image_eqI'], simpset()) 1);
    1.61 -qed "lift_prog_constrains_drop_set";