# HG changeset patch
# User paulson
# Date 947848673 -3600
# Node ID 3a5864b465e2e1154ecfaad5334fbd7a399e492a
# Parent  68c6159440f151bb356722bfa77c08608dcece43
still working; a bit of polishing

diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Alloc.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -380,8 +380,7 @@
 qed "Always_tokens_allocRel_le_rel";
 
 (*safety (1), step 4 (final result!) *)
-Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \
-\              <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}";
+Goalw [system_safety_def] "System : system_safety";
 by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv, 
 			   Always_tokens_allocRel_le_rel] RS Always_weaken) 1);
 by Auto_tac;
@@ -393,7 +392,6 @@
 qed "System_safety";
 
 
-
 (*** Proof of the progress property (2) ***)
 
 (*Now there are proofs identical to System_Increasing_rel and
@@ -422,7 +420,7 @@
 Goal "i < Nclients \
 \     ==> System : Always \
 \                   {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
-br Always_weaken 1;
+by (rtac Always_weaken 1);
 by (rtac ([guarantees_PLam_I RS client_export UNIV_guar_Always,
 	   Client_component_System] MRS component_guaranteesD) 1);
 by (rtac Client_i_Bounded 1);
@@ -463,11 +461,11 @@
 \               (reachable (lift_prog i Client Join G) Int      \
 \                {s. h <= (giv o sub i) s & h pfixGe (ask o sub i) s} -      \
 \                {s. tokens h <= tokens ((rel o sub i) s)})";
-auto();
+by Auto_tac;
 by (REPEAT (dres_inst_tac [("x", "rel (xa i)")] spec 2));
 by (REPEAT (dres_inst_tac [("x", "ask (xa i)")] spec 1));
 by (REPEAT_FIRST ball_tac);
-auto();
+by Auto_tac;
 qed "G_stable_lift_prog";
 
 Goal "lift_prog i Client \
@@ -477,12 +475,12 @@
 \                             h pfixGe (ask o sub i) s}  \
 \                  Ensures {s. tokens h <= (tokens o rel o sub i) s})";
 by (rtac (Client_Progress RS drop_prog_guarantees_raw) 1);
-br (lift_export (subset_refl RS project_Increasing_I)) 1;
+by (rtac (lift_export project_Increasing_I) 1);
 by (full_simp_tac (simpset() addsimps [fold_o_sub, lift_prog_correct]) 1);
-br INT_I 1;
+by (rtac INT_I 1);
 by (simp_tac (simpset() addsimps [o_apply]) 1);
 by (REPEAT (stac (lift_export Collect_eq_extend_set) 1));
-br (lift_export project_Ensures_D) 1;
+by (rtac (lift_export project_Ensures_D) 1);
 by (asm_full_simp_tac (simpset() addsimps [o_apply, lift_prog_correct, 
 					   drop_prog_correct]) 1);
 by (asm_full_simp_tac
@@ -492,7 +490,7 @@
 			 Collect_eq_lift_set RS sym,
 			 lift_prog_correct RS sym]) 1);
 by (Clarify_tac 1);
-bd G_stable_lift_prog 1;
+by (dtac G_stable_lift_prog 1);
 by (auto_tac (claset(), 
 	      simpset() addsimps [o_apply]));
 qed "Client_i_Progress";
@@ -505,7 +503,7 @@
 \                             h pfixGe (ask o sub i) s}  \
 \                  Ensures {s. tokens h <= (tokens o rel o sub i) s})";
 by (rtac guarantees_PLam_I 1);
-br Client_i_Progress 1;
+by (rtac Client_i_Progress 1);
 by Auto_tac;
 val lemma2 = result();
 
@@ -523,11 +521,11 @@
 \           {s. h <= (giv o sub i o client) s & \
 \               h pfixGe (ask o sub i o client) s} - \
 \           {s. tokens h <= tokens ((rel o sub i o client) s)})";
-auto();
+by Auto_tac;
 by (REPEAT (dres_inst_tac [("x", "rel (client xa i)")] spec 2));
 by (REPEAT (dres_inst_tac [("x", "ask (client xa i)")] spec 1));
 by (REPEAT_FIRST ball_tac);
-auto();
+by Auto_tac;
 qed "G_stable_sysOfClient";
 
 Goal "i < Nclients \
@@ -538,20 +536,20 @@
 \                            h pfixGe (ask o sub i o client) s}  \
 \                 Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
 by (rtac (lemma2 RS client_export project_guarantees_raw) 1);
-ba 1;
-br (client_export (subset_refl RS project_Increasing_I)) 1;
+by (assume_tac 1);
+by (rtac (client_export project_Increasing_I) 1);
 by (Simp_tac 1);
-br INT_I 1;
+by (rtac INT_I 1);
 by (simp_tac (simpset() addsimps [o_apply]) 1);
 by (REPEAT (stac (client_export Collect_eq_extend_set) 1));
-br (client_export project_Ensures_D) 1;
+by (rtac (client_export project_Ensures_D) 1);
 by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1);
 by (asm_full_simp_tac
     (simpset() addsimps [all_conj_distrib,
 			 Increasing_def, Stable_eq_stable, Join_stable,
 			 Collect_eq_extend_set RS sym]) 1);
 by (Clarify_tac 1);
-bd G_stable_sysOfClient 1;
+by (dtac G_stable_sysOfClient 1);
 by (auto_tac (claset(), 
 	      simpset() addsimps [o_apply,
 				client_export Collect_eq_extend_set RS sym]));
@@ -570,7 +568,7 @@
 	   Client_component_System] MRS component_guaranteesD) 1);
 by (asm_full_simp_tac
     (simpset() addsimps [System_Increasing_giv]) 2);
-auto();
+by Auto_tac;
 qed "System_Client_Progress";
 
 val lemma =
@@ -627,50 +625,24 @@
 	      simpset() addsimps [System_Increasing_allocRel,
 				  System_Increasing_allocAsk]));
 by (rtac System_Bounded_allocAsk 1);
-by (etac System_Alloc_Progress 1);
+by (etac System_Alloc_Client_Progress 1);
 qed "System_Alloc_Progress";
 
 
+(*progress (2), step 10 (final result!) *)
+Goalw [system_progress_def] "System : system_progress";
+by (Clarify_tac 1);
+by (rtac LeadsTo_Trans 1);
+by (etac (System_Follows_allocGiv RS Follows_LeadsTo_pfixLe) 2);
+by (rtac LeadsTo_Trans 1);
+by (cut_facts_tac [System_Alloc_Progress] 2);
+by (Blast_tac 2);
+by (etac (System_Follows_ask RS Follows_LeadsTo) 1);
+qed "System_Progress";
+
 
 (*Ultimate goal*)
-Goal "System : system_spec";
-
-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
-
-
-(*progress (2), step 10*)
-Goal
- "System : (INT i : lessThan Nclients. \
-\           INT h. {s. h <= (ask o sub i o client) s}  \
-\                  LeadsTo {s. h pfixLe (giv o sub i o client) s})";
-by (Clarify_tac 1);
-by (rtac LeadsTo_Trans 1);
-by (dtac (System_Follows_allocGiv RS Follows_LeadsTo) 2);
-by (blast_tac (claset() addIs [prefix_imp_pfixLe, LeadsTo_weaken_R]) 2);
-
-prefix_imp_pfixLe
-
-
-System_Follows_ask
+Goalw [system_spec_def] "System : system_spec";
+by (blast_tac (claset() addIs [System_safety, System_Progress]) 1);
+qed "System_correct";
 
-by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS 
-	  Follows_LeadsTo) 2);
-
-by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
-by (rtac LeadsTo_Trans 1);
-by (cut_facts_tac [System_Client_Progress] 2);
-by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
-by (etac lemma3 1);
-
-by (rtac ([Alloc_Progress, Alloc_component_System] 
-	  MRS component_guaranteesD) 1);
-(*preserves*)
-by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
-(*the guarantees precondition*)
-by (auto_tac (claset(), 
-	      simpset() addsimps [System_Increasing_allocRel,
-				  System_Increasing_allocAsk]));
-by (rtac System_Bounded_allocAsk 1);
-by (etac System_Alloc_Progress 1);
-qed "System_Alloc_Progress";
-
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Comp.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -173,74 +173,3 @@
 by (Blast_tac 1);
 qed "Increasing_preserves_Stable";
 
-
-(*** givenBy ***)
-
-Goalw [givenBy_def] "givenBy id = UNIV";
-by Auto_tac;
-qed "givenBy_id";
-Addsimps [givenBy_id];
-
-Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
-by Safe_tac;
-by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
-by Auto_tac;
-qed "givenBy_eq_all";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by Safe_tac;
-by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
-by (Blast_tac 1);
-by Auto_tac;
-qed "givenBy_eq_Collect";
-
-val prems =
-Goal "(!!x y. [| x:A;  v x = v y |] ==> y: A) ==> A: givenBy v";
-by (stac givenBy_eq_all 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "givenByI";
-
-Goalw [givenBy_def] "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A";
-by Auto_tac;
-qed "givenByD";
-
-Goal "{} : givenBy v";
-by (blast_tac (claset() addSIs [givenByI]) 1);
-qed "empty_mem_givenBy";
-
-AddIffs [empty_mem_givenBy];
-
-Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
-by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
-by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by (Blast_tac 1);
-qed "givenBy_imp_eq_Collect";
-
-Goalw [givenBy_def] "{s. P(v s)} : givenBy v";
-by (Best_tac 1);
-qed "Collect_mem_givenBy";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (blast_tac (claset() addIs [Collect_mem_givenBy,
-			       givenBy_imp_eq_Collect]) 1);
-qed "givenBy_eq_eq_Collect";
-
-(*preserving v preserves properties given by v*)
-Goal "[| F : preserves v;  D : givenBy v |] ==> F : stable D";
-by (force_tac (claset(), 
-	       simpset() addsimps [impOfSubs preserves_subset_stable, 
-				   givenBy_eq_Collect]) 1);
-qed "preserves_givenBy_imp_stable";
-
-Goal "givenBy (w o v) <= givenBy v";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_o_subset";
-
-Goal "[| A : givenBy v;  B : givenBy v |] ==> A-B : givenBy v";
-by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by Safe_tac;
-by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
-by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
-qed "givenBy_DiffI";
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Comp.thy	Fri Jan 14 12:17:53 2000 +0100
@@ -26,8 +26,4 @@
   funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
     "funPair f g == %x. (f x, g x)"
 
-  (*the set of all sets determined by f alone*)
-  givenBy :: "['a => 'b] => 'a set set"
-    "givenBy f == range (%B. f-`` B)"
-
 end
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/ELT.ML
--- a/src/HOL/UNITY/ELT.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/ELT.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -6,6 +6,93 @@
 leadsTo strengthened with a specification of the allowable sets transient parts
 *)
 
+(*** givenBy ***)
+
+Goalw [givenBy_def] "givenBy id = UNIV";
+by Auto_tac;
+qed "givenBy_id";
+Addsimps [givenBy_id];
+
+Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
+by Safe_tac;
+by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
+by Auto_tac;
+qed "givenBy_eq_all";
+
+Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
+by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by Safe_tac;
+by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
+by (Blast_tac 1);
+by Auto_tac;
+qed "givenBy_eq_Collect";
+
+val prems =
+Goal "(!!x y. [| x:A;  v x = v y |] ==> y: A) ==> A: givenBy v";
+by (stac givenBy_eq_all 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "givenByI";
+
+Goalw [givenBy_def] "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A";
+by Auto_tac;
+qed "givenByD";
+
+Goal "{} : givenBy v";
+by (blast_tac (claset() addSIs [givenByI]) 1);
+qed "empty_mem_givenBy";
+
+AddIffs [empty_mem_givenBy];
+
+Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
+by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
+by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by (Blast_tac 1);
+qed "givenBy_imp_eq_Collect";
+
+Goalw [givenBy_def] "{s. P(v s)} : givenBy v";
+by (Best_tac 1);
+qed "Collect_mem_givenBy";
+
+Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
+by (blast_tac (claset() addIs [Collect_mem_givenBy,
+			       givenBy_imp_eq_Collect]) 1);
+qed "givenBy_eq_eq_Collect";
+
+(*preserving v preserves properties given by v*)
+Goal "[| F : preserves v;  D : givenBy v |] ==> F : stable D";
+by (force_tac (claset(), 
+	       simpset() addsimps [impOfSubs preserves_subset_stable, 
+				   givenBy_eq_Collect]) 1);
+qed "preserves_givenBy_imp_stable";
+
+Goal "givenBy (w o v) <= givenBy v";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_o_subset";
+
+Goal "[| A : givenBy v;  B : givenBy v |] ==> A-B : givenBy v";
+by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by Safe_tac;
+by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
+by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
+qed "givenBy_DiffI";
+
+Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_o_eq_extend_set";
+
+Goal "givenBy f = range (extend_set h)";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_eq_extend_set";
+
+Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
+by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by (Blast_tac 1);
+qed "extend_set_givenBy_I";
+
+
 (** Standard leadsTo rules **)
 
 Goalw [leadsETo_def]
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/ELT.thy	Fri Jan 14 12:17:53 2000 +0100
@@ -43,6 +43,10 @@
 
 
 constdefs
+  
+  (*the set of all sets determined by f alone*)
+  givenBy :: "['a => 'b] => 'a set set"
+    "givenBy f == range (%B. f-`` B)"
 
   (*visible version of the LEADS-TO relation*)
   leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Extend.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -569,24 +569,6 @@
 qed "extend_LeadsTo";
 
 
-(*** givenBy: USEFUL??? ***)
-
-Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_o_eq_extend_set";
-
-Goal "givenBy f = range (extend_set h)";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_eq_extend_set";
-
-Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
-by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by (Blast_tac 1);
-qed "extend_set_givenBy_I";
-
-
 Close_locale "Extend";
 
 (*Close_locale should do this!
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/Follows.ML
--- a/src/HOL/UNITY/Follows.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Follows.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -22,7 +22,6 @@
 by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
 qed "mono_LeadsTo_o";
 
-(*NOT PROVABLE USING leadsETo because givenBy f <= givenBy (h o f) fails*)
 Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";
 by (Clarify_tac 1);
 by (asm_full_simp_tac
@@ -31,34 +30,17 @@
 			 impOfSubs mono_LeadsTo_o RS INT_D]) 1);
 qed "mono_Follows_o";
 
-(*NOT PROVABLE USING leadsETo since it needs the previous thm*)
 Goal "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))";
 by (dtac mono_Follows_o 1);
 by (force_tac (claset(), simpset() addsimps [o_def]) 1);
 qed "mono_Follows_apply";
 
-(*NOT PROVABLE USING leadsETo since givenBy g doesn't imply givenBy f*)
 Goalw [Follows_def]
      "[| F : f Fols g;  F: g Fols h |] ==> F : f Fols h";
 by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
 by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);
 qed "Follows_trans";
 
-(*
-try:
-by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [order_trans, LeadsETo_Trans]) 1);
-by (rtac LeadsETo_Trans 1);
-by (Blast_tac 2);
-by (dtac spec 1);
-by (etac LeadsETo_weaken 1);
-by Auto_tac;
-by (thin_tac "All ?P" 1);
-by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by Safe_tac;
-**)
-
 
 (** Destructiom rules **)
 
@@ -82,6 +64,24 @@
 by (Blast_tac 1);
 qed "Follows_LeadsTo";
 
+Goal "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}";
+by (rtac single_LeadsTo_I 1);
+by (Clarify_tac 1);
+by (dtac Follows_LeadsTo 1);
+by (etac LeadsTo_weaken 1);
+by (blast_tac set_cs 1);
+by (blast_tac (claset() addIs [pfixLe_trans, prefix_imp_pfixLe]) 1);
+qed "Follows_LeadsTo_pfixLe";
+
+Goal "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}";
+by (rtac single_LeadsTo_I 1);
+by (Clarify_tac 1);
+by (dtac Follows_LeadsTo 1);
+by (etac LeadsTo_weaken 1);
+by (blast_tac set_cs 1);
+by (blast_tac (claset() addIs [pfixGe_trans, prefix_imp_pfixGe]) 1);
+qed "Follows_LeadsTo_pfixGe";
+
 
 (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
 
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Follows.thy	Fri Jan 14 12:17:53 2000 +0100
@@ -3,13 +3,10 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-The Follows relation of Charpentier and Sivilotte
-
-The safety conditions ensures that "givenBy f" is implementable in the
-  progress part: g cannot do anything silly.
+The "Follows" relation of Charpentier and Sivilotte
 *)
 
-Follows = Project +
+Follows = SubstAx +
 
 constdefs
 
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/GenPrefix.ML
--- a/src/HOL/UNITY/GenPrefix.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/GenPrefix.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -313,9 +313,17 @@
 by (Force_tac 1);
 qed "prefix_append_iff";
 
+Goal "r<=s ==> genPrefix r <= genPrefix s";
+by (Clarify_tac 1);
+by (etac genPrefix.induct 1);
+by (auto_tac (claset() addIs [genPrefix.append], simpset()));
+qed "genPrefix_mono";
+
 
 (*** pfixLe, pfixGe: properties inherited from the translations ***)
 
+(** pfixLe **)
+
 Goalw [refl_def, Le_def] "reflexive Le";
 by Auto_tac;
 qed "reflexive_Le";
@@ -330,6 +338,23 @@
 
 AddIffs [reflexive_Le, antisym_Le, trans_Le];
 
+Goal "x pfixLe x";
+by (Simp_tac 1);
+qed "pfixLe_refl";
+AddIffs[pfixLe_refl];
+
+Goal "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z";
+by (blast_tac (claset() addIs [genPrefix_trans]) 1);
+qed "pfixLe_trans";
+
+Goal "[| x pfixLe y; y pfixLe x |] ==> x = y";
+by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
+qed "pfixLe_antisym";
+
+Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys";
+by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
+qed "prefix_imp_pfixLe";
+
 Goalw [refl_def, Ge_def] "reflexive Ge";
 by Auto_tac;
 qed "reflexive_Ge";
@@ -344,15 +369,18 @@
 
 AddIffs [reflexive_Ge, antisym_Ge, trans_Ge];
 
-Goal "r<=s ==> genPrefix r <= genPrefix s";
-by (Clarify_tac 1);
-by (etac genPrefix.induct 1);
-by (auto_tac (claset() addIs [genPrefix.append], simpset()));
-qed "genPrefix_mono";
+Goal "x pfixGe x";
+by (Simp_tac 1);
+qed "pfixGe_refl";
+AddIffs[pfixGe_refl];
 
-Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys";
-by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
-qed "prefix_imp_pfixLe";
+Goal "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z";
+by (blast_tac (claset() addIs [genPrefix_trans]) 1);
+qed "pfixGe_trans";
+
+Goal "[| x pfixGe y; y pfixGe x |] ==> x = y";
+by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
+qed "pfixGe_antisym";
 
 Goalw [prefix_def, Ge_def] "xs<=ys ==> xs pfixGe ys";
 by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/LessThan.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -50,17 +50,6 @@
 by Auto_tac;
 qed "Restrict_imageI";
 
-Goal "(Restrict A `` (Restrict A `` r - s)) = (Restrict A `` r - s)";
-by Auto_tac;
-by (rewrite_goals_tac [image_def, Restrict_def]);
-by (Blast_tac 1);
-qed "Restrict_image_Diff";
-
-(*Nothing to do with Restrict, but to specialized for Fun.ML?*)
-Goal "f``(g``A - B) = (UN x: (A - g-`` B). {f(g(x))})";
-by (Blast_tac 1);
-qed "image_Diff_image_eq";
-
 Goal "Domain (Restrict A r) = A Int Domain r";
 by (Blast_tac 1);
 qed "Domain_Restrict";
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -211,27 +211,11 @@
 qed "drop_set_INT";
 
 Goal "lift_set i UNIV = UNIV";
-by (simp_tac
-    (simpset() addsimps [lift_set_correct, lift_export0 extend_set_UNIV_eq]) 1);
+by (simp_tac (simpset() addsimps [lift_set_correct, 
+				  lift_export0 extend_set_UNIV_eq]) 1);
 qed "lift_set_UNIV_eq";
 Addsimps [lift_set_UNIV_eq];
 
-(*
-Goal "Domain act <= drop_set i C ==> drop_act i (Restrict C (lift_act i act)) = act";
-by (asm_full_simp_tac
-    (simpset() addsimps [drop_set_correct, drop_act_correct, 
-			 lift_act_correct, lift_export0 extend_act_inverse]) 1);
-qed "lift_act_inverse";
-Addsimps [lift_act_inverse];
-*)
-
-Goal "UNIV <= drop_set i C ==> drop_prog i C (lift_prog i F) = F";
-by (asm_full_simp_tac
-    (simpset() addsimps [drop_set_correct, drop_prog_correct, 
-			 lift_prog_correct, lift_export0 extend_inverse]) 1);
-qed "lift_prog_inverse";
-Addsimps [lift_prog_inverse];
-
 Goal "inj (lift_prog i)";
 by (simp_tac
     (simpset() addsimps [lift_prog_correct, lift_export0 inj_extend]) 1);
@@ -291,8 +275,8 @@
 Goal "(drop_prog i C F : A co B)  =  \
 \     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
 by (simp_tac
-    (simpset() addsimps [drop_prog_correct, 
-			 lift_set_correct, lift_export0 project_constrains]) 1);
+    (simpset() addsimps [drop_prog_correct, lift_set_correct, 
+			 lift_export0 project_constrains]) 1);
 qed "drop_prog_constrains";
 
 Goal "(drop_prog i UNIV F : stable A)  =  (F : stable (lift_set i A))";
@@ -321,8 +305,7 @@
 by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1);
 qed "lift_prog_Stable";
 
-Goal "[| reachable (lift_prog i F Join G) <= C;    \
-\        F Join drop_prog i C G : A Co B |] \
+Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : A Co B  \
 \     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
 by (asm_full_simp_tac
     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
@@ -330,14 +313,12 @@
 qed "drop_prog_Constrains_D";
 
 Goalw [Stable_def]
-     "[| reachable (lift_prog i F Join G) <= C;    \
-\        F Join drop_prog i C G : Stable A |]  \
+     "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Stable A  \
 \     ==> lift_prog i F Join G : Stable (lift_set i A)";
 by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
 qed "drop_prog_Stable_D";
 
-Goal "[| reachable (lift_prog i F Join G) <= C;  \
-\        F Join drop_prog i C G : Always A |]   \
+Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Always A  \
 \     ==> lift_prog i F Join G : Always (lift_set i A)";
 by (asm_full_simp_tac
     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
@@ -345,24 +326,14 @@
 qed "drop_prog_Always_D";
 
 Goalw [Increasing_def]
-     "[| reachable (lift_prog i F Join G) <= C;  \
-\        F Join drop_prog i C G : Increasing func |] \
-\     ==> lift_prog i F Join G : Increasing (func o (sub i))";
+ "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Increasing func \
+\ ==> lift_prog i F Join G : Increasing (func o (sub i))";
 by Auto_tac;
 by (stac Collect_eq_lift_set 1);
 by (asm_simp_tac (simpset() addsimps [drop_prog_Stable_D]) 1); 
 qed "project_Increasing_D";
 
 
-(*UNUSED*)
-Goal "UNIV <= drop_set i C \
-\     ==> drop_prog i C ((lift_prog i F) Join G) = F Join (drop_prog i C G)";
-by (asm_full_simp_tac
-    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
-		     drop_set_correct, lift_export0 project_extend_Join]) 1);
-qed "drop_prog_lift_prog_Join";
-
-
 (*** Progress: transient, ensures ***)
 
 Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Project.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -6,16 +6,8 @@
 Projections of state sets (also of actions and programs)
 
 Inheritance of GUARANTEES properties under extension
-
-POSSIBLY CAN DELETE Restrict_image_Diff
 *)
 
-(*EQUALITIES.ML*)
-		Goal "(A <= -A) = (A = {})";
-		by (Blast_tac 1);
-		qed "subset_Compl_self_eq";
-
-
 Open_locale "Extend";
 
 (** projection: monotonicity for safety **)
@@ -297,37 +289,30 @@
 by (etac extend_act_D 1);
 qed "reachable_imp_reachable_project";
 
-(*The extra generality in the first premise allows guarantees with STRONG
-  preconditions (localT) and WEAK postconditions.*)
-(*LOCALTO NO LONGER EXISTS: replace C by reachable...??*)
 Goalw [Constrains_def]
-     "[| reachable (extend h F Join G) <= C;    \
-\        F Join project h C G : A Co B |] \
+     "F Join project h (reachable (extend h F Join G)) G : A Co B  \
 \     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
 by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
 by (Clarify_tac 1);
 by (etac constrains_weaken 1);
-by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
+by (auto_tac (claset() addIs [reachable_imp_reachable_project], simpset()));
 qed "project_Constrains_D";
 
 Goalw [Stable_def]
-     "[| reachable (extend h F Join G) <= C;  \
-\        F Join project h C G : Stable A |]   \
+     "F Join project h (reachable (extend h F Join G)) G : Stable A  \
 \     ==> extend h F Join G : Stable (extend_set h A)";
 by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
 qed "project_Stable_D";
 
 Goalw [Always_def]
-     "[| reachable (extend h F Join G) <= C;  \
-\        F Join project h C G : Always A |]   \
+     "F Join project h (reachable (extend h F Join G)) G : Always A  \
 \     ==> extend h F Join G : Always (extend_set h A)";
 by (force_tac (claset() addIs [reachable.Init],
                simpset() addsimps [project_Stable_D, split_extended_all]) 1);
 qed "project_Always_D";
 
 Goalw [Increasing_def]
-     "[| reachable (extend h F Join G) <= C;  \
-\        F Join project h C G : Increasing func |] \
+     "F Join project h (reachable (extend h F Join G)) G : Increasing func  \
 \     ==> extend h F Join G : Increasing (func o f)";
 by Auto_tac;
 by (stac Collect_eq_extend_set 1);
@@ -364,45 +349,37 @@
 	      simpset()));
 qed "reachable_extend_Join_subset";
 
-(*Perhaps should replace C by reachable...*)
 Goalw [Constrains_def]
-     "[| C <= reachable (extend h F Join G);  \
-\        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
-\     ==> F Join project h C G : A Co B";
+     "extend h F Join G : (extend_set h A) Co (extend_set h B)  \
+\     ==> F Join project h (reachable (extend h F Join G)) G : A Co B";
 by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
 				       extend_set_Int_distrib]) 1);
 by (rtac conjI 1);
-by (etac constrains_weaken 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1);
-(*Some generalization of constrains_weaken_L would be better, but what is it?*)
-by (rewtac constrains_def);
-by Auto_tac;
-by (thin_tac "ALL act : Acts G. ?P act" 1);
-by (force_tac (claset() addSDs [reachable_project_imp_reachable], 
-	       simpset()) 1);
+by (force_tac
+    (claset() addEs [constrains_weaken_L]
+              addSDs [extend_constrains_project_set,
+		      subset_refl RS reachable_project_imp_reachable], 
+     simpset() addsimps [Join_constrains]) 2);
+by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
 qed "project_Constrains_I";
 
 Goalw [Stable_def]
-     "[| C <= reachable (extend h F Join G);  \
-\        extend h F Join G : Stable (extend_set h A) |] \
-\     ==> F Join project h C G : Stable A";
+     "extend h F Join G : Stable (extend_set h A)  \
+\     ==> F Join project h (reachable (extend h F Join G)) G : Stable A";
 by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
 qed "project_Stable_I";
 
 Goalw [Always_def]
-     "[| C <= reachable (extend h F Join G);  \
-\        extend h F Join G : Always (extend_set h A) |]   \
-\     ==> F Join project h C G : Always A";
+     "extend h F Join G : Always (extend_set h A)  \
+\     ==> F Join project h (reachable (extend h F Join G)) G : Always A";
 by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
 by (rewtac extend_set_def);
 by (Blast_tac 1);
 qed "project_Always_I";
 
 Goalw [Increasing_def]
-     "[| C <= reachable (extend h F Join G);  \
-\        extend h F Join G : Increasing (func o f) |] \
-\     ==> F Join project h C G : Increasing func";
+    "extend h F Join G : Increasing (func o f)  \
+\    ==> F Join project h (reachable (extend h F Join G)) G : Increasing func";
 by Auto_tac;
 by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
 				      project_Stable_I]) 1); 
@@ -471,11 +448,10 @@
 by (blast_tac (claset() addIs [project_Always_D]) 1);
 qed "extending_Always";
 
-val [prem] = 
 Goalw [extending_def]
-     "(!!G. reachable (extend h F Join G) <= C G)  \
-\     ==> extending v C h F (Increasing (func o f)) (Increasing func)";
-by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1);
+     "extending v (%G. reachable (extend h F Join G)) h F \
+\                 (Increasing (func o f)) (Increasing func)";
+by (blast_tac (claset() addIs [project_Increasing_D]) 1);
 qed "extending_Increasing";
 
 
@@ -630,10 +606,10 @@
 by (auto_tac (claset(), 
 	      simpset() addsimps [Int_Diff,
 				  extend_set_Diff_distrib RS sym]));
-bd act_subset_imp_project_act_subset 1;
+by (dtac act_subset_imp_project_act_subset 1);
 by (subgoal_tac
     "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1);
-bws [Restrict_def, project_set_def, extend_set_def, project_act_def];
+by (rewrite_goals_tac [Restrict_def, project_set_def, extend_set_def, project_act_def]);
 (*using Int_greatest actually slows the next step!*)
 by (Blast_tac 2);
 by (force_tac (claset(), 
@@ -670,9 +646,9 @@
 Goal "[| F Join project h UNIV G : A ensures B;  \
 \        G : stable (extend_set h A - extend_set h B) |] \
 \     ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
-br (project_ensures_D_lemma RS revcut_rl) 1;
+by (rtac (project_ensures_D_lemma RS revcut_rl) 1);
 by (stac stable_UNIV 3);
-auto();
+by Auto_tac;
 qed "project_ensures_D";
 
 Goalw [Ensures_def]
@@ -680,7 +656,7 @@
 \        G : stable (reachable (extend h F Join G) Int extend_set h A - \
 \                    extend_set h B) |] \
 \     ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)";
-br (project_ensures_D_lemma RS revcut_rl) 1;
+by (rtac (project_ensures_D_lemma RS revcut_rl) 1);
 by (auto_tac (claset(), 
 	      simpset() addsimps [project_set_reachable_extend_eq RS sym]));
 qed "project_Ensures_D";
diff -r 68c6159440f1 -r 3a5864b465e2 src/HOL/UNITY/ROOT.ML
--- a/src/HOL/UNITY/ROOT.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/ROOT.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -28,7 +28,7 @@
 time_use_thy "Extend";
 time_use_thy "PPROD";
 time_use_thy "TimerArray";
-time_use_thy "Follows";
+time_use_thy "Alloc";
 
 add_path "../Auth";	(*to find Public.thy*)
 use_thy"NSP_Bad";