src/HOL/UNITY/Lift_prog.ML

--- a/src/HOL/UNITY/Lift_prog.ML	Wed Aug 25 10:58:08 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Wed Aug 25 10:59:32 1999 +0200
@@ -66,6 +66,8 @@
 qed "Acts_drop_prog";
 Addsimps [Acts_drop_prog];
 
+(** These monotonicity results look natural but are UNUSED **)
+
 Goal "F component G ==> lift_prog i F component lift_prog i G";
 by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
 by Auto_tac;
@@ -177,16 +179,16 @@
 	      simpset() addsimps [constrains_def]));
 by (Blast_tac 2);
 by (Force_tac 1);
-qed "lift_prog_constrains_eq";
+qed "lift_prog_constrains";
 
 Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)";
-by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains_eq]) 1);
-qed "lift_prog_stable_eq";
+by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains]) 1);
+qed "lift_prog_stable";
 
 Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
 by (auto_tac (claset(),
-	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
-qed "lift_prog_invariant_eq";
+	      simpset() addsimps [invariant_def, lift_prog_stable]));
+qed "lift_prog_invariant";
 
 (*This one looks strange!  Proof probably is by case analysis on i=j.
   If i~=j then lift_prog j (F j) does nothing to lift_set i, and the 
@@ -207,14 +209,14 @@
 by (force_tac (claset(), 
 	       simpset() addsimps [drop_act_def]) 2);
 by (blast_tac (claset() addIs [drop_act_I]) 1);
-qed "drop_prog_constrains_eq";
+qed "drop_prog_constrains";
 
 Goal "(drop_prog i F : stable A)  =  (F : stable (lift_set i A))";
-by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains_eq]) 1);
-qed "drop_prog_stable_eq";
+by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1);
+qed "drop_prog_stable";
 
 
-(** Diff, needed for localTo **)
+(*** Diff, needed for localTo ***)
 
 Goal "Diff G (lift_act i `` Acts F) : (lift_set i A) co (lift_set i B)  \
 \     ==> Diff (drop_prog i G) (Acts F) : A co B";
@@ -232,12 +234,12 @@
 by (etac Diff_drop_prog_co 1);
 qed "Diff_drop_prog_stable";
 
-Goal "Diff G (Acts F) : A co B  \
+Goalw [constrains_def, Diff_def]
+     "Diff G (Acts F) : A co B  \
 \     ==> Diff (lift_prog i G) (lift_act i `` Acts F) \
 \         : (lift_set i A) co (lift_set i B)";
-by (auto_tac (claset(), 
-	      simpset() addsimps [constrains_def, Diff_def]));
-by (auto_tac (claset(), simpset() addsimps [drop_act_def]));
+by Auto_tac;
+by (Blast_tac 1);
 qed "Diff_lift_prog_co";
 
 Goalw [stable_def]
@@ -247,7 +249,7 @@
 qed "Diff_lift_prog_stable";
 
 
-(*** Weak versions: Co, Stable ***)
+(*** Weak safety primitives: Co, Stable ***)
 
 (** Reachability **)
 
@@ -276,12 +278,12 @@
 \     (F : A Co B)";
 by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog,
 				  lift_set_Int RS sym,
-				  lift_prog_constrains_eq]) 1);
-qed "lift_prog_Constrains_eq";
+				  lift_prog_constrains]) 1);
+qed "lift_prog_Constrains";
 
 Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
-by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains_eq]) 1);
-qed "lift_prog_Stable_eq";
+by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1);
+qed "lift_prog_Stable";
 
 (** Reachability and drop_prog **)
 
@@ -298,7 +300,7 @@
 *)
 Goalw [Constrains_def]
      "drop_prog i F : A Co B ==> F : (lift_set i A) Co (lift_set i B)";
-by (full_simp_tac (simpset() addsimps [drop_prog_constrains_eq]) 1);
+by (full_simp_tac (simpset() addsimps [drop_prog_constrains]) 1);
 by (etac constrains_weaken_L 1);
 by Auto_tac;
 by (etac reachable_imp_reachable_drop_prog 1);
@@ -353,19 +355,20 @@
 \    co lift_set i A" 1);
 by (asm_full_simp_tac 
     (simpset() addsimps [lift_set_Int RS sym,
-			 lift_prog_constrains_eq,
-			 drop_prog_constrains_eq RS sym,
+			 lift_prog_constrains,
+			 drop_prog_constrains RS sym,
 			 drop_prog_lift_prog_Join]) 2);
 by (blast_tac (claset() addIs [constrains_weaken, 
 			       reachable_lift_prog_Join_D]) 1);
-qed "lift_prog_Join_Stable_eq";
+qed "lift_prog_Join_Stable";
 
 
 (*** guarantees properties ***)
 
 (** It seems that neither of these can be proved from the other. **)
 
-(*Strong precondition and postcondition; doesn't seem very useful*)
+(*Strong precondition and postcondition; doesn't seem very useful.
+  Probably can be strengthened to an equivalance.*)
 Goal "F : X guar Y \
 \     ==> lift_prog i F : (lift_prog i `` X) guar (lift_prog i `` Y)";
 by (rtac guaranteesI 1);
@@ -373,15 +376,15 @@
 by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
 qed "lift_prog_guarantees";
 
-(*Weak precondition and postcondition; doesn't seem very useful*)
-Goal "[| F : X guar Y;  drop_prog i `` XX <= X;  \
-\        ALL G. F Join drop_prog i G : Y --> lift_prog i F Join G : YY |] \
+(*Weak precondition and postcondition; this is the good one!*)
+val [xguary,drop_prog,lift_prog] =
+Goal "[| F : X guar Y;  \
+\        !!H. H : XX ==> drop_prog i H : X;  \
+\        !!G. F Join drop_prog i G : Y ==> lift_prog i F Join G : YY |] \
 \     ==> lift_prog i F : XX guar YY";
-by (rtac guaranteesI 1);
-by (dtac guaranteesD 1);
-by (etac subsetD 1);
-by (rtac image_eqI 1);
-by (auto_tac (claset(), simpset() addsimps [drop_prog_lift_prog_Join]));
+by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
+by (dtac drop_prog 1);
+by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
 qed "drop_prog_guarantees";
 
 
@@ -405,7 +408,7 @@
 Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}";
 by Auto_tac;
 by (stac Collect_eq_lift_set 1); 
-by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [lift_prog_Stable]) 1);
 qed "image_lift_prog_Stable";
 
 Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)";
@@ -424,7 +427,7 @@
 by Auto_tac;
 by (stac Collect_eq_lift_set 1); 
 by (asm_full_simp_tac
-    (simpset() addsimps [lift_prog_stable_eq, drop_prog_stable_eq, 
+    (simpset() addsimps [lift_prog_stable, drop_prog_stable, 
 			 stable_Join]) 1);
 qed "lift_prog_guar_increasing";
 
@@ -434,7 +437,7 @@
 by (etac drop_prog_guarantees 1);
 by Auto_tac;
 by (stac Collect_eq_lift_set 1); 
-by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable]) 1);
 qed "lift_prog_guar_Increasing";
 
 Goalw [localTo_def, increasing_def]
@@ -446,13 +449,13 @@
 by (stac Collect_eq_lift_set 2); 
 (*the "increasing" guarantee*)
 by (asm_full_simp_tac
-    (simpset() addsimps [lift_prog_stable_eq, drop_prog_stable_eq, 
+    (simpset() addsimps [lift_prog_stable, drop_prog_stable, 
 			 stable_Join]) 2);
 (*the "localTo" requirement*)
 by (asm_simp_tac
     (simpset() addsimps [Diff_drop_prog_stable, 
 			 Collect_eq_lift_set RS sym]) 1); 
-qed "lift_prog_guar_increasing2";
+qed "lift_prog_localTo_guar_increasing";
 
 Goalw [localTo_def, Increasing_def]
      "F : (f localTo F) guar Increasing f  \
@@ -462,12 +465,12 @@
 by Auto_tac;
 by (stac Collect_eq_lift_set 2); 
 (*the "Increasing" guarantee*)
-by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable_eq]) 2);
+by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable]) 2);
 (*the "localTo" requirement*)
 by (asm_simp_tac
     (simpset() addsimps [Diff_drop_prog_stable, 
 			 Collect_eq_lift_set RS sym]) 1); 
-qed "lift_prog_guar_Increasing2";
+qed "lift_prog_localTo_guar_Increasing";
 
 (*Converse fails.  Useful?*)
 Goal "lift_prog i `` (f localTo F) <= (f o sub i) localTo (lift_prog i F)";