# HG changeset patch
# User paulson
# Date 945423048 -3600
# Node ID 225e3b45b76601e6b090016c0cd269ecb3261324
# Parent  54d37e491ac2e30ce71449f5031bd19799332dcc
now workign as far as System_Alloc_Progress

diff -r 54d37e491ac2 -r 225e3b45b766 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Thu Dec 16 17:01:16 1999 +0100
+++ b/src/HOL/UNITY/Alloc.ML	Fri Dec 17 10:30:48 1999 +0100
@@ -13,6 +13,8 @@
 AddIs [impOfSubs subset_preserves_o];
 Addsimps [funPair_o_distrib];
 
+Delsimps [o_apply];
+
 (*Eliminating the "o" operator gives associativity for free*)
 val o_simp = simplify (simpset() addsimps [o_def]);
 
@@ -35,6 +37,27 @@
 		handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
      handle THM _ => th;
 
+(*Currently UNUSED, but possibly of interest*)
+Goal "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}";
+by (asm_full_simp_tac
+    (simpset() addsimps [Increasing_def, Stable_def, Constrains_def, 
+			 constrains_def]) 1); 
+by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
+			       prefix_imp_pfixGe]) 1);
+qed "Increasing_imp_Stable_pfixGe";
+
+(*Currently UNUSED, but possibly of interest*)
+Goal "ALL z. F : {s. z <= f s} LeadsTo {s. z <= g s} \
+\     ==> F : {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}";
+by (rtac single_LeadsTo_I 1);
+by (dres_inst_tac [("x", "f s")] spec 1);
+by (etac LeadsTo_weaken 1);
+by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
+			       prefix_imp_pfixGe]) 2);
+by (Blast_tac 1);
+qed "LeadsTo_le_imp_pfixGe";
+
+
 Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
 by (induct_tac "n" 1);
 by Auto_tac;
@@ -282,8 +305,7 @@
 	  RS guaranteesD) 1);
 by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
 by (auto_tac (claset(), 
-	      simpset() delsimps [o_apply]
-			addsimps [sub_fold, Network_preserves_rel_ask]));
+	      simpset() addsimps [Network_preserves_rel_ask]));
 qed "System_Increasing_ask";
 
 Goalw [System_def]
@@ -293,13 +315,10 @@
 by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
 (*gets Client_Increasing_rel from simpset*)
 by (auto_tac (claset(), 
-	      simpset() delsimps [o_apply]
-			addsimps [sub_fold, Network_preserves_rel_ask]));
+	      simpset() addsimps [Network_preserves_rel_ask]));
 qed "System_Increasing_rel";
 
-
-(*Not sure what to say about the other components because they involve
-  extend*)
+(** Components lemmas **)
 
 (*Alternative is to say that System = Network Join F such that F preserves
   certain state variables*)
@@ -323,28 +342,45 @@
     The "Always (INT ...) formulation expresses the general safety property
     and allows it to be combined using Always_Int_rule below. **)
 
+Goal
+  "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))";
+by (auto_tac (claset() addSIs [System_Increasing_rel, 
+			       Network_Rel RS component_guaranteesD], 
+	      simpset()));
+qed "System_Follows_rel";
+
+Goal
+  "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))";
+by (auto_tac (claset() addSIs [System_Increasing_ask, 
+			       Network_Ask RS component_guaranteesD], 
+	      simpset()));
+qed "System_Follows_ask";
+
+Goal
+  "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)";
+by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD, 
+		 extend_Alloc_Increasing_allocGiv RS component_guaranteesD], 
+	      simpset()));
+qed "System_Follows_allocGiv";
+
 Goal "System : Always (INT i: lessThan Nclients. \
 \                      {s. (giv o sub i o client) s <= (sub i o allocGiv) s})";
 by (auto_tac (claset(), 
-	      simpset() delsimps [o_apply] addsimps [Always_INT_distrib]));
-br Follows_Bounded 1;
-br (Network_Giv RS component_guaranteesD) 1;
-br (extend_Alloc_Increasing_allocGiv RS component_guaranteesD) 2;
-by Auto_tac;
+	      simpset() addsimps [Always_INT_distrib]));
+by (etac (System_Follows_allocGiv RS Follows_Bounded) 1);
 qed "Always_giv_le_allocGiv";
 
 Goal "System : Always (INT i: lessThan Nclients. \
 \                      {s. (sub i o allocAsk) s <= (ask o sub i o client) s})";
-by (auto_tac (claset() addSIs [Follows_Bounded, System_Increasing_ask, 
-			       Network_Ask RS component_guaranteesD], 
-	      simpset() delsimps [o_apply] addsimps [Always_INT_distrib]));
+by (auto_tac (claset(), 
+	      simpset() addsimps [Always_INT_distrib]));
+by (etac (System_Follows_ask RS Follows_Bounded) 1);
 qed "Always_allocAsk_le_ask";
 
 Goal "System : Always (INT i: lessThan Nclients. \
 \                      {s. (sub i o allocRel) s <= (rel o sub i o client) s})";
-by (auto_tac (claset() addSIs [Follows_Bounded, System_Increasing_rel, 
-			       Network_Rel RS component_guaranteesD], 
-	      simpset() delsimps [o_apply] addsimps [Always_INT_distrib]));
+by (auto_tac (claset() addSIs [Follows_Bounded, System_Follows_rel], 
+	      simpset() addsimps [Always_INT_distrib]));
 qed "Always_allocRel_le_rel";
 
 
@@ -354,9 +390,7 @@
 
 (*safety (1), step 2*)
 Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
-by (rtac Follows_Increasing1 1);
-by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
-			       System_Increasing_rel]) 1);
+by (etac (System_Follows_rel RS Follows_Increasing1) 1);
 qed "System_Increasing_allocRel";
 
 (*safety (1), step 3*)
@@ -386,14 +420,16 @@
 \                         {s. (tokens o giv o sub i o client) s \
 \                          <= (tokens o sub i o allocGiv) s})";
 by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1);
-by (auto_tac (claset() addIs [tokens_mono_prefix], simpset()));
+by (auto_tac (claset() addIs [tokens_mono_prefix], 
+	      simpset() addsimps [o_apply]));
 qed "Always_tokens_giv_le_allocGiv";
 
 Goal "System : Always (INT i: lessThan Nclients. \
 \                         {s. (tokens o sub i o allocRel) s \
 \                          <= (tokens o rel o sub i o client) s})";
 by (rtac (Always_allocRel_le_rel RS Always_weaken) 1);
-by (auto_tac (claset() addIs [tokens_mono_prefix], simpset()));
+by (auto_tac (claset() addIs [tokens_mono_prefix], 
+	      simpset() addsimps [o_apply]));
 qed "Always_tokens_allocRel_le_rel";
 
 (*safety (1), step 4 (final result!) *)
@@ -444,7 +480,7 @@
 	  guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
 by (rtac Client_i_Bounded 1);
 by (auto_tac(claset(),
-	 simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
+	 simpset() addsimps [o_apply, lift_export Collect_eq_extend_set RS sym,
 			     client_export Collect_eq_extend_set RS sym]));
 qed "System_Bounded_ask";
 
@@ -509,7 +545,47 @@
 by (rtac (client_export extending_LeadsETo RS extending_weaken RS 
 	  extending_INT) 1);
 by (auto_tac (claset(), 
-	   simpset() addsimps [client_export Collect_eq_extend_set RS sym]));
+  simpset() addsimps [o_apply, client_export Collect_eq_extend_set RS sym]));
 qed "System_Client_Progress";
 
+val lemma =
+    [System_Follows_ask RS Follows_Bounded,
+     System_Follows_allocGiv RS Follows_LeadsTo] MRS Always_LeadsToD;
 
+val lemma2 = [lemma, 
+	      System_Follows_ask RS Follows_Increasing1 RS IncreasingD]
+             MRS PSP_Stable;
+
+Goal "i < Nclients \
+\     ==> System : {s. h <= (sub i o allocGiv) s &      \
+\                      h pfixGe (sub i o allocAsk) s}   \
+\                  LeadsTo  \
+\                  {s. h <= (giv o sub i o client) s &  \
+\                      h pfixGe (ask o sub i o client) s}";
+by (rtac single_LeadsTo_I 1);
+by (res_inst_tac [("k6", "h"), ("x2", "(sub i o allocAsk) s")]
+    (lemma2 RS LeadsTo_weaken) 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
+			       prefix_imp_pfixGe]) 1);
+val lemma3 = result();
+
+
+(*progress (2), step 8*)
+Goal
+ "System : (INT i : lessThan Nclients. \
+\           INT h. {s. h <= (sub i o allocGiv) s & \
+\                      h pfixGe (sub i o allocAsk) s}  \
+\                  LeadsTo {s. tokens h <= (tokens o sub i o allocRel) s})";
+by Auto_tac;
+by (rtac LeadsTo_Trans 1);
+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 (rtac (impOfSubs LeadsETo_subset_LeadsTo) 2);
+by (cut_facts_tac [System_Client_Progress] 2);
+by (Force_tac 2);
+by (simp_tac (simpset() addsimps [Collect_conj_eq]) 1); 
+by (etac lemma3 1);
+qed "System_Alloc_Progress";
diff -r 54d37e491ac2 -r 225e3b45b766 src/HOL/UNITY/ELT.ML
--- a/src/HOL/UNITY/ELT.ML	Thu Dec 16 17:01:16 1999 +0100
+++ b/src/HOL/UNITY/ELT.ML	Fri Dec 17 10:30:48 1999 +0100
@@ -120,7 +120,6 @@
 by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
 qed "leadsETo_mono";
 
-
 val prems = Goalw [leadsETo_def]
  "(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) ==> F : (Union S Int C) leadsTo[CC] B";
 by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
@@ -350,6 +349,58 @@
 qed "Join_leadsETo_stable_imp_leadsETo";
 
 
+(**** Relationship with traditional "leadsTo", strong & weak ****)
+
+(** strong **)
+
+Goal "(A leadsTo[CC] B) <= (A leadsTo B)";
+by Safe_tac;
+by (etac leadsETo_induct 1);
+by (blast_tac (claset() addIs [leadsTo_Union]) 3);
+by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
+by (blast_tac (claset() addIs [leadsTo_Basis]) 1);
+qed "leadsETo_subset_leadsTo";
+
+Goal "(A leadsTo[UNIV] B) = (A leadsTo B)";
+by Safe_tac;
+by (etac (impOfSubs leadsETo_subset_leadsTo) 1);
+(*right-to-left case*)
+by (etac leadsTo_induct 1);
+by (blast_tac (claset() addIs [leadsETo_Union]) 3);
+by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
+by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
+qed "leadsETo_UNIV_eq_leadsTo";
+
+(** weak **)
+
+Goalw [LeadsETo_def, LeadsTo_def] "(A LeadsTo[CC] B) <= (A LeadsTo B)";
+by (blast_tac (claset() addIs [impOfSubs leadsETo_subset_leadsTo]) 1);
+qed "LeadsETo_subset_LeadsTo";
+
+(*Postcondition can be strengthened to (reachable F Int B) *)
+Goal "F : A ensures B ==> F : (reachable F Int A) ensures B";
+by (rtac (stable_ensures_Int RS ensures_weaken_R) 1);
+by (auto_tac (claset(), simpset() addsimps [stable_reachable]));
+qed "reachable_ensures";
+
+Goal "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B";
+by (etac leadsTo_induct 1);
+by (stac Int_Union 3);
+by (blast_tac (claset() addIs [leadsETo_UN]) 3);
+by (blast_tac (claset() addDs [e_psp_stable2] 
+                        addIs [leadsETo_Trans, stable_reachable, 
+			       leadsETo_weaken_L]) 2);
+by (blast_tac (claset() addIs [reachable_ensures, leadsETo_Basis]) 1);
+val lemma = result();
+
+Goal "(A LeadsTo[UNIV] B) = (A LeadsTo B)";
+by Safe_tac;
+by (etac (impOfSubs LeadsETo_subset_LeadsTo) 1);
+(*right-to-left case*)
+by (rewrite_goals_tac [LeadsETo_def, LeadsTo_def]);
+by (fast_tac (claset() addEs [lemma RS leadsETo_weaken]) 1);
+qed "LeadsETo_UNIV_eq_LeadsTo";
+
 
 (**** EXTEND/PROJECT PROPERTIES ****)
 
diff -r 54d37e491ac2 -r 225e3b45b766 src/HOL/UNITY/GenPrefix.ML
--- a/src/HOL/UNITY/GenPrefix.ML	Thu Dec 16 17:01:16 1999 +0100
+++ b/src/HOL/UNITY/GenPrefix.ML	Fri Dec 17 10:30:48 1999 +0100
@@ -343,3 +343,18 @@
 qed "trans_Ge";
 
 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";
+
+Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys";
+by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
+qed "prefix_imp_pfixLe";
+
+Goalw [prefix_def, Ge_def] "xs<=ys ==> xs pfixGe ys";
+by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
+qed "prefix_imp_pfixGe";
+