working snapshot (even Alloc)
authorpaulson
Mon Oct 04 13:47:28 1999 +0200 (1999-10-04)
changeset 7689affe0c2fdfbf
parent 7688 d106cad8f515
child 7690 27676b51243d
working snapshot (even Alloc)
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Guar.ML
src/HOL/UNITY/PPROD.ML
src/HOL/UNITY/Project.ML
src/HOL/UNITY/Project.thy
src/HOL/UNITY/Union.ML
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Mon Oct 04 13:45:31 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Mon Oct 04 13:47:28 1999 +0200
     1.3 @@ -6,19 +6,11 @@
     1.4  Specification of Chandy and Charpentier's Allocator
     1.5  
     1.6  STOP USING o (COMPOSITION), since function application is naturally associative
     1.7 +
     1.8 +guarantees_PLam_I looks wrong: refers to lift_prog
     1.9  *)
    1.10  
    1.11  
    1.12 -Goal "~ f #2 ==> ~ (!t::nat. (#0 <= t & t <= #10) --> f t)";
    1.13 -
    1.14 -(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
    1.15 -Goal "[| b:A;  a=b |] ==> a:A";
    1.16 -by (etac ssubst 1);
    1.17 -by (assume_tac 1);
    1.18 -qed "subst_elem";
    1.19 -
    1.20 -
    1.21 -
    1.22  Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
    1.23  by (induct_tac "n" 1);
    1.24  by Auto_tac;
    1.25 @@ -65,6 +57,7 @@
    1.26  Goalw [good_map_def] "good_map sysOfAlloc";
    1.27  by Auto_tac;
    1.28  qed "good_map_sysOfAlloc";
    1.29 +Addsimps [good_map_sysOfAlloc];
    1.30  
    1.31  (*MUST BE AUTOMATED: even the statement of such results*)
    1.32  Goal "!!s. inv sysOfAlloc s = \
    1.33 @@ -76,7 +69,6 @@
    1.34  by (auto_tac (claset() addSWrapper record_split_wrapper, 
    1.35  	      simpset() addsimps [sysOfAlloc_def]));
    1.36  qed "inv_sysOfAlloc_eq";
    1.37 -
    1.38  Addsimps [inv_sysOfAlloc_eq];
    1.39  
    1.40  (**SHOULD NOT BE NECESSARY: The various injections into the system
    1.41 @@ -99,6 +91,7 @@
    1.42  Goalw [good_map_def] "good_map sysOfClient";
    1.43  by Auto_tac;
    1.44  qed "good_map_sysOfClient";
    1.45 +Addsimps [good_map_sysOfClient];
    1.46  
    1.47  (*MUST BE AUTOMATED: even the statement of such results*)
    1.48  Goal "!!s. inv sysOfClient s = \
    1.49 @@ -110,6 +103,7 @@
    1.50  by (auto_tac (claset() addSWrapper record_split_wrapper, 
    1.51  	      simpset() addsimps [sysOfAlloc_def, sysOfClient_def]));
    1.52  qed "inv_sysOfClient_eq";
    1.53 +Addsimps [inv_sysOfClient_eq];
    1.54  
    1.55  
    1.56  Open_locale "System";
    1.57 @@ -154,7 +148,7 @@
    1.58  
    1.59  (*CANNOT use bind_thm: it puts the theorem into standard form, in effect
    1.60    exporting it from the locale*)
    1.61 -val Network_Ask = Network_Spec RS IntD1 RS IntD1;
    1.62 +val Network_Ask = Network_Spec RS IntD1 RS IntD1 RS INT_D;
    1.63  val Network_Giv = Network_Spec RS IntD1 RS IntD2 RS INT_D;
    1.64  val Network_Rel = Network_Spec RS IntD2 RS INT_D;
    1.65  
    1.66 @@ -189,14 +183,16 @@
    1.67  AddIffs [Network_component_System, Alloc_component_System];
    1.68  
    1.69  
    1.70 +fun alloc_export th = good_map_sysOfAlloc RS export th;
    1.71 +
    1.72 +fun client_export th = good_map_sysOfClient RS export th;
    1.73 +
    1.74  (* F : UNIV guarantees Increasing func
    1.75     ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
    1.76  val extend_Client_guar_Increasing =
    1.77 -  good_map_sysOfClient RS export extend_guar_Increasing
    1.78 +  client_export extend_guar_Increasing
    1.79    |> simplify (simpset() addsimps [inv_sysOfClient_eq]);
    1.80  
    1.81 -fun alloc_export th = good_map_sysOfAlloc RS export th;
    1.82 -
    1.83  (*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
    1.84  Goal "i < Nclients \
    1.85  \ ==> extend sysOfAlloc Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
    1.86 @@ -205,31 +201,27 @@
    1.87  qed "extend_Alloc_Increasing_allocGiv";
    1.88  
    1.89  
    1.90 -(** Proof of property (1) **)
    1.91 +(*** Proof of the safety property (1) ***)
    1.92  
    1.93 -(*step 1*)
    1.94 +(*safety (1), step 1*)
    1.95  Goalw [System_def]
    1.96       "i < Nclients ==> System : Increasing (rel o sub i o client)";
    1.97 -by (rtac ([guaranteesI RS disjI2 RS guarantees_Join_I, UNIV_I] 
    1.98 -	  MRS guaranteesD) 1);
    1.99 -by (asm_simp_tac 
   1.100 -    (simpset() addsimps [guarantees_PLam_I, 
   1.101 -			 extend_Client_guar_Increasing RS guaranteesD,
   1.102 -			 lift_prog_guar_Increasing]) 1);
   1.103 +by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2 
   1.104 +	  RS guaranteesD) 1);
   1.105 +by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
   1.106 +(*gets Client_Increasing_rel from simpset*)
   1.107 +by Auto_tac;
   1.108  qed "System_Increasing_rel";
   1.109  
   1.110 -(*Note: the first step above performs simple quantifier reasoning.  It could
   1.111 -  be replaced by a proof mentioning no guarantees primitives*)
   1.112  
   1.113 -
   1.114 -(*step 2*)
   1.115 +(*safety (1), step 2*)
   1.116  Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
   1.117  by (rtac Follows_Increasing1 1);
   1.118  by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
   1.119  			       System_Increasing_rel]) 1);
   1.120  qed "System_Increasing_allocRel";
   1.121  
   1.122 -(*step 2*)
   1.123 +(*safety (1), step 3*)
   1.124  Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
   1.125  \                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
   1.126  by (res_inst_tac 
   1.127 @@ -250,7 +242,7 @@
   1.128       (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
   1.129  qed "System_sum_bounded";
   1.130  
   1.131 -(*step 3*)
   1.132 +(*safety (1), step 4*)
   1.133  Goal "System : Always (INT i: lessThan Nclients. \
   1.134  \                         {s. (tokens o giv o sub i o client) s \
   1.135  \                          <= (tokens o sub i o allocGiv) s})";
   1.136 @@ -266,6 +258,7 @@
   1.137  qed "System_Always_giv_le_allocGiv";
   1.138  
   1.139  
   1.140 +(*safety (1), step 5*)
   1.141  Goal "System : Always (INT i: lessThan Nclients. \
   1.142  \                         {s. (tokens o sub i o allocRel) s \
   1.143  \                          <= (tokens o rel o sub i o client) s})";
   1.144 @@ -281,6 +274,7 @@
   1.145  qed "System_Always_allocRel_le_rel";
   1.146  
   1.147  
   1.148 +(*safety (1), step 6*)
   1.149  Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \
   1.150  \              <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}";
   1.151  by (rtac (Always_Int_rule [System_sum_bounded, System_Always_giv_le_allocGiv, 
   1.152 @@ -293,3 +287,40 @@
   1.153  by Auto_tac;
   1.154  qed "System_safety";
   1.155  
   1.156 +
   1.157 +
   1.158 +(*** Proof of the progress property (2) ***)
   1.159 +
   1.160 +(*we begin with proofs identical to System_Increasing_rel and
   1.161 +  System_Increasing_allocRel: tactics needed!*)
   1.162 +
   1.163 +(*progress (2), step 1*)
   1.164 +Goalw [System_def]
   1.165 +     "i < Nclients ==> System : Increasing (ask o sub i o client)";
   1.166 +by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2 
   1.167 +	  RS guaranteesD) 1);
   1.168 +by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
   1.169 +by Auto_tac;
   1.170 +qed "System_Increasing_ask";
   1.171 +
   1.172 +(*progress (2), step 2*)
   1.173 +Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)";
   1.174 +by (rtac Follows_Increasing1 1);
   1.175 +by (blast_tac (claset() addIs [Network_Ask RS component_guaranteesD,
   1.176 +			       System_Increasing_ask]) 1);
   1.177 +qed "System_Increasing_allocAsk";
   1.178 +
   1.179 +(*progress (2), step 3*)
   1.180 +(*All this trouble just to lift "Client_Bounded" through two extemd ops*)
   1.181 +Goalw [System_def]
   1.182 +     "i < Nclients \
   1.183 +\   ==> System : Always \
   1.184 +\                 {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
   1.185 +by (rtac (lift_prog_guar_Always RS 
   1.186 +	  guarantees_PLam_I RS client_export extend_guar_Always RS
   1.187 +	  guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
   1.188 +by (stac Always_UNIV_eq 1 THEN rtac Client_Bounded 1);
   1.189 +by (auto_tac(claset(),
   1.190 +	 simpset() addsimps [Collect_eq_lift_set RS sym,
   1.191 +			     client_export Collect_eq_extend_set RS sym]));
   1.192 +qed "System_Bounded";
     2.1 --- a/src/HOL/UNITY/Constrains.ML	Mon Oct 04 13:45:31 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Constrains.ML	Mon Oct 04 13:47:28 1999 +0200
     2.3 @@ -282,6 +282,11 @@
     2.4  				  Always_eq_invariant_reachable]));
     2.5  qed "Always_eq_includes_reachable";
     2.6  
     2.7 +Goal "Always UNIV = UNIV";
     2.8 +by (auto_tac (claset(),
     2.9 +	      simpset() addsimps [Always_eq_includes_reachable]));
    2.10 +qed "Always_UNIV_eq";
    2.11 +Addsimps [Always_UNIV_eq];
    2.12  
    2.13  Goal "Always A = (UN I: Pow A. invariant I)";
    2.14  by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
     3.1 --- a/src/HOL/UNITY/Extend.ML	Mon Oct 04 13:45:31 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Extend.ML	Mon Oct 04 13:47:28 1999 +0200
     3.3 @@ -95,6 +95,13 @@
     3.4  by (rtac extend_set_inverse 1);
     3.5  qed "inj_extend_set";
     3.6  
     3.7 +Goalw [extend_set_def] "extend_set h UNIV = UNIV";
     3.8 +by Auto_tac;
     3.9 +by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
    3.10 +by Auto_tac;
    3.11 +qed "extend_set_UNIV_eq";
    3.12 +Addsimps [standard extend_set_UNIV_eq];
    3.13 +
    3.14  (*** project_set: basic properties ***)
    3.15  
    3.16  (*project_set is simply image!*)
    3.17 @@ -164,7 +171,7 @@
    3.18  
    3.19  (*Premise is still undesirably strong, since Domain act can include
    3.20    non-reachable states, but it seems necessary for this result.*)
    3.21 -Goalw [extend_act_def,project_set_def, project_act_def]
    3.22 +Goalw [extend_act_def, project_set_def, project_act_def]
    3.23   "Domain act <= project_set h C ==> project_act C h (extend_act h act) = act";
    3.24  by (Force_tac 1);
    3.25  qed "extend_act_inverse";
    3.26 @@ -206,8 +213,7 @@
    3.27  qed "project_act_I";
    3.28  
    3.29  Goalw [project_set_def, project_act_def]
    3.30 -    "UNIV <= project_set h C \
    3.31 -\     ==> project_act C h Id = Id";
    3.32 +    "UNIV <= project_set h C ==> project_act C h Id = Id";
    3.33  by (Force_tac 1);
    3.34  qed "project_act_Id";
    3.35  
    3.36 @@ -290,6 +296,21 @@
    3.37  qed "extend_JN";
    3.38  Addsimps [extend_JN];
    3.39  
    3.40 +
    3.41 +(** These monotonicity results look natural but are UNUSED **)
    3.42 +
    3.43 +Goal "F <= G ==> extend h F <= extend h G";
    3.44 +by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
    3.45 +by Auto_tac;
    3.46 +qed "extend_mono";
    3.47 +
    3.48 +Goal "F <= G ==> project C h F <= project C h G";
    3.49 +by (full_simp_tac
    3.50 +    (simpset() addsimps [component_eq_subset, project_set_def]) 1);
    3.51 +by Auto_tac;
    3.52 +qed "project_mono";
    3.53 +
    3.54 +
    3.55  (*** Safety: co, stable ***)
    3.56  
    3.57  Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \
     4.1 --- a/src/HOL/UNITY/Guar.ML	Mon Oct 04 13:45:31 1999 +0200
     4.2 +++ b/src/HOL/UNITY/Guar.ML	Mon Oct 04 13:47:28 1999 +0200
     4.3 @@ -219,6 +219,9 @@
     4.4  by (Blast_tac 1);
     4.5  qed "guarantees_Join_I";
     4.6  
     4.7 +bind_thm ("guarantees_Join_I1", disjI1 RS guarantees_Join_I);
     4.8 +bind_thm ("guarantees_Join_I2", disjI2 RS guarantees_Join_I);
     4.9 +
    4.10  Goalw [guar_def]
    4.11       "[| i : I;  F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y";
    4.12  by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
     5.1 --- a/src/HOL/UNITY/PPROD.ML	Mon Oct 04 13:45:31 1999 +0200
     5.2 +++ b/src/HOL/UNITY/PPROD.ML	Mon Oct 04 13:47:28 1999 +0200
     5.3 @@ -271,21 +271,7 @@
     5.4  (*** guarantees properties ***)
     5.5  
     5.6  Goalw [PLam_def]
     5.7 -    "[| i : I;  lift_prog i (F i): X guarantees Y |]  \
     5.8 +    "[| lift_prog i (F i): X guarantees Y;  i : I |]  \
     5.9  \    ==> (PLam I F) : X guarantees Y";
    5.10  by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
    5.11  qed "guarantees_PLam_I";
    5.12 -
    5.13 -Goalw [PLam_def]
    5.14 -    "[| ALL i:I. F i : X guarantees Y |] \
    5.15 -\    ==> (PLam I F) : (INT i: I. lift_prog i `` X) \
    5.16 -\                 guarantees (INT i: I. lift_prog i `` Y)";
    5.17 -by (blast_tac (claset() addIs [guarantees_JN_INT, lift_prog_guarantees]) 1);
    5.18 -bind_thm ("guarantees_PLam_INT", ballI RS result());
    5.19 -
    5.20 -Goalw [PLam_def]
    5.21 -    "[| ALL i:I. F i : X guarantees Y |] \
    5.22 -\    ==> (PLam I F) : (UN i: I. lift_prog i `` X) \
    5.23 -\                 guarantees (UN i: I. lift_prog i `` Y)";
    5.24 -by (blast_tac (claset() addIs [guarantees_JN_UN, lift_prog_guarantees]) 1);
    5.25 -bind_thm ("guarantees_PLam_UN", ballI RS result());
     6.1 --- a/src/HOL/UNITY/Project.ML	Mon Oct 04 13:45:31 1999 +0200
     6.2 +++ b/src/HOL/UNITY/Project.ML	Mon Oct 04 13:47:28 1999 +0200
     6.3 @@ -18,7 +18,7 @@
     6.4  
     6.5  Goal "[| D <= C; project C h F : A co B |] ==> project D h F : A co B";
     6.6  by (auto_tac (claset(), simpset() addsimps [constrains_def]));
     6.7 -bd project_act_mono 1;
     6.8 +by (dtac project_act_mono 1);
     6.9  by (Blast_tac 1);
    6.10  qed "project_constrains_mono";
    6.11  
    6.12 @@ -65,7 +65,7 @@
    6.13  qed "project_stable";
    6.14  
    6.15  Goal "F : stable (extend_set h A) ==> project C h F : stable A";
    6.16 -bd (project_stable RS iffD2) 1;
    6.17 +by (dtac (project_stable RS iffD2) 1);
    6.18  by (blast_tac (claset() addIs [project_stable_mono]) 1);
    6.19  qed "project_stable_I";
    6.20  
    6.21 @@ -106,6 +106,16 @@
    6.22  				  extend_stable RS iffD1]));
    6.23  qed "Join_project_increasing";
    6.24  
    6.25 +(*For using project_guarantees in particular cases*)
    6.26 +Goal "extend h F Join G : extend_set h A co extend_set h B \
    6.27 +\     ==> F Join project UNIV h G : A co B";
    6.28 +by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
    6.29 +by (asm_full_simp_tac
    6.30 +    (simpset() addsimps [project_constrains, Join_constrains, 
    6.31 +			 extend_constrains]) 1);
    6.32 +by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
    6.33 +qed "project_constrains_I";
    6.34 +
    6.35  
    6.36  (*** Diff, needed for localTo ***)
    6.37  
    6.38 @@ -140,13 +150,20 @@
    6.39  qed "Diff_project_stable";
    6.40  
    6.41  (*Converse appears to fail*)
    6.42 -Goal "[| UNIV <= project_set h C;  (H : (func o f) localTo extend h G) |] \
    6.43 -\     ==> (project C h H : func localTo G)";
    6.44 +Goal "[| UNIV <= project_set h C;  H : (func o f) localTo extend h G |] \
    6.45 +\     ==> project C h H : func localTo G";
    6.46  by (asm_full_simp_tac 
    6.47      (simpset() addsimps [localTo_def, 
    6.48  			 project_extend_Join RS sym,
    6.49  			 subset_UNIV RS subset_trans RS Diff_project_stable,
    6.50  			 Collect_eq_extend_set RS sym]) 1);
    6.51 +qed "project_localTo_lemma";
    6.52 +
    6.53 +Goal "extend h F Join G : (v o f) localTo extend h H \
    6.54 +\     ==> F Join project UNIV h G : v localTo H";
    6.55 +by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
    6.56 +by (asm_simp_tac 
    6.57 +    (simpset() addsimps [project_set_UNIV RS project_localTo_lemma]) 1);
    6.58  qed "project_localTo_I";
    6.59  
    6.60  
    6.61 @@ -166,6 +183,8 @@
    6.62  by (etac extend_act_D 1);
    6.63  qed "reachable_imp_reachable_project";
    6.64  
    6.65 +(*The extra generality in the first premise allows guarantees with STRONG
    6.66 +  preconditions (localTo) and WEAK postconditions.*)
    6.67  Goalw [Constrains_def]
    6.68       "[| reachable (extend h F Join G) <= C;    \
    6.69  \        F Join project C h G : A Co B |] \
    6.70 @@ -188,7 +207,7 @@
    6.71  \        F Join project C h G : Always A |]   \
    6.72  \     ==> extend h F Join G : Always (extend_set h A)";
    6.73  by (force_tac (claset() addIs [reachable.Init, project_set_I],
    6.74 -	       simpset() addsimps [project_Stable_D]) 1);
    6.75 +               simpset() addsimps [project_Stable_D]) 1);
    6.76  qed "project_Always_D";
    6.77  
    6.78  Goalw [Increasing_def]
    6.79 @@ -250,6 +269,15 @@
    6.80  by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
    6.81  qed "project_Stable_I";
    6.82  
    6.83 +Goalw [Always_def]
    6.84 +     "[| C <= reachable (extend h F Join G);  \
    6.85 +\        extend h F Join G : Always (extend_set h A) |]   \
    6.86 +\     ==> F Join project C h G : Always A";
    6.87 +by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
    6.88 +bws [project_set_def, extend_set_def];
    6.89 +by (Blast_tac 1);
    6.90 +qed "project_Always_I";
    6.91 +
    6.92  Goalw [Increasing_def]
    6.93       "[| C <= reachable (extend h F Join G);  \
    6.94  \        extend h F Join G : Increasing (func o f) |] \
    6.95 @@ -369,15 +397,15 @@
    6.96  by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, 
    6.97  			       leadsTo_Trans]) 2);
    6.98  by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
    6.99 -qed "Join_project_leadsTo_I";
   6.100 +qed "project_leadsTo_lemma";
   6.101  
   6.102  (*Instance of the previous theorem for STRONG progress*)
   6.103  Goal "[| ALL x. project UNIV h G ~: transient {x};  \
   6.104  \        F Join project UNIV h G : A leadsTo B |] \
   6.105  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   6.106 -by (dtac Join_project_leadsTo_I 1);
   6.107 +by (dtac project_leadsTo_lemma 1);
   6.108  by Auto_tac;
   6.109 -qed "Join_project_UNIV_leadsTo_I";
   6.110 +qed "project_UNIV_leadsTo_lemma";
   6.111  
   6.112  (** Towards the analogous theorem for WEAK progress*)
   6.113  
   6.114 @@ -397,7 +425,7 @@
   6.115  \        extend h F Join G : stable C;  \
   6.116  \        F Join project C h G : (project_set h C Int A) leadsTo B |] \
   6.117  \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
   6.118 -br (lemma RS leadsTo_weaken) 1;
   6.119 +by (rtac (lemma RS leadsTo_weaken) 1);
   6.120  by (auto_tac (claset() addIs [project_set_I], simpset()));
   6.121  val lemma2 = result();
   6.122  
   6.123 @@ -475,31 +503,31 @@
   6.124  by Auto_tac;
   6.125  qed "extend_guar_Increasing";
   6.126  
   6.127 -Goal "F : (func localTo G) guarantees increasing func  \
   6.128 -\     ==> extend h F : (func o f) localTo (extend h G)  \
   6.129 +Goal "F : (v localTo G) guarantees increasing func  \
   6.130 +\     ==> extend h F : (v o f) localTo (extend h G)  \
   6.131  \                      guarantees increasing (func o f)";
   6.132  by (etac project_guarantees 1);
   6.133  (*the "increasing" guarantee*)
   6.134 -by (asm_simp_tac
   6.135 -    (simpset() addsimps [Join_project_increasing RS sym]) 2);
   6.136 -(*the "localTo" requirement*)
   6.137 -by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   6.138 -by (asm_simp_tac 
   6.139 -    (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
   6.140 +by (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym]) 2);
   6.141 +by (etac project_localTo_I 1);
   6.142  qed "extend_localTo_guar_increasing";
   6.143  
   6.144 -Goal "F : (func localTo G) guarantees Increasing func  \
   6.145 -\     ==> extend h F : (func o f) localTo (extend h G)  \
   6.146 +Goal "F : (v localTo G) guarantees Increasing func  \
   6.147 +\     ==> extend h F : (v o f) localTo (extend h G)  \
   6.148  \                      guarantees Increasing (func o f)";
   6.149  by (etac project_guarantees 1);
   6.150  (*the "Increasing" guarantee*)
   6.151  by (etac (subset_UNIV RS project_Increasing_D) 2);
   6.152 -(*the "localTo" requirement*)
   6.153 -by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   6.154 -by (asm_simp_tac 
   6.155 -    (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
   6.156 +by (etac project_localTo_I 1);
   6.157  qed "extend_localTo_guar_Increasing";
   6.158  
   6.159 +Goal "F : Always A guarantees Always B \
   6.160 +\ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
   6.161 +by (etac project_guarantees 1);
   6.162 +by (etac (subset_refl RS project_Always_D) 2);
   6.163 +by (etac (subset_refl RS project_Always_I) 1);
   6.164 +qed "extend_guar_Always";
   6.165 +
   6.166  
   6.167  (** Guarantees with a leadsTo postcondition **)
   6.168  
   6.169 @@ -510,13 +538,38 @@
   6.170  			 extend_set_sing, project_stable_I]) 1);
   6.171  qed "localTo_imp_project_stable";
   6.172  
   6.173 -
   6.174  Goal "F : stable{s} ==> F ~: transient {s}";
   6.175  by (auto_tac (claset(), 
   6.176  	      simpset() addsimps [FP_def, transient_def,
   6.177  				  stable_def, constrains_def]));
   6.178  qed "stable_sing_imp_not_transient";
   6.179  
   6.180 +Goal "[| F Join project UNIV h G : A leadsTo B;    \
   6.181 +\        extend h F Join G : f localTo extend h F; \
   6.182 +\        Disjoint (extend h F) G |]  \
   6.183 +\     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   6.184 +by (rtac project_UNIV_leadsTo_lemma 1);
   6.185 +by Auto_tac;
   6.186 +by (asm_full_simp_tac
   6.187 +    (simpset() addsimps [Join_localTo, self_localTo,
   6.188 +			 localTo_imp_project_stable, 
   6.189 +			 stable_sing_imp_not_transient]) 1);
   6.190 +qed "project_leadsTo_D";
   6.191 +
   6.192 +
   6.193 +Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
   6.194 +\         extend h F Join G : f localTo extend h F; \
   6.195 +\         Disjoint (extend h F) G  |]  \
   6.196 +\      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
   6.197 +by (rtac Join_project_LeadsTo 1);
   6.198 +by Auto_tac;
   6.199 +by (asm_full_simp_tac
   6.200 +    (simpset() addsimps [Join_localTo, self_localTo,
   6.201 +			 localTo_imp_project_stable, 
   6.202 +			 stable_sing_imp_not_transient]) 1);
   6.203 +qed "project_LeadsTo_D";
   6.204 +
   6.205 +
   6.206  (*STRONG precondition and postcondition*)
   6.207  Goal "F : (A co A') guarantees (B leadsTo B')  \
   6.208  \ ==> extend h F : ((extend_set h A) co (extend_set h A'))  \
   6.209 @@ -524,18 +577,9 @@
   6.210  \                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
   6.211  by (etac project_guarantees 1);
   6.212  (*the safety precondition*)
   6.213 -by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   6.214 -by (asm_full_simp_tac
   6.215 -    (simpset() addsimps [project_constrains, Join_constrains, 
   6.216 -			 extend_constrains]) 1);
   6.217 -by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
   6.218 +by (fast_tac (claset() addIs [project_constrains_I]) 1);
   6.219  (*the liveness postcondition*)
   6.220 -by (rtac Join_project_UNIV_leadsTo_I 1);
   6.221 -by Auto_tac;
   6.222 -by (asm_full_simp_tac
   6.223 -    (simpset() addsimps [Join_localTo, self_localTo,
   6.224 -			 localTo_imp_project_stable, 
   6.225 -			 stable_sing_imp_not_transient]) 1);
   6.226 +by (fast_tac (claset() addIs [project_leadsTo_D]) 1);
   6.227  qed "extend_co_guar_leadsTo";
   6.228  
   6.229  (*WEAK precondition and postcondition*)
   6.230 @@ -547,13 +591,7 @@
   6.231  (*the safety precondition*)
   6.232  by (fast_tac (claset() addIs [project_Constrains_I]) 1);
   6.233  (*the liveness postcondition*)
   6.234 -by (rtac Join_project_LeadsTo 1);
   6.235 -by Auto_tac;
   6.236 -by (asm_full_simp_tac
   6.237 -    (simpset() addsimps [Join_localTo, self_localTo,
   6.238 -			 localTo_imp_project_stable, 
   6.239 -			 stable_sing_imp_not_transient]) 1);
   6.240 +by (fast_tac (claset() addIs [project_LeadsTo_D]) 1);
   6.241  qed "extend_Co_guar_LeadsTo";
   6.242  
   6.243 -
   6.244  Close_locale "Extend";
     7.1 --- a/src/HOL/UNITY/Project.thy	Mon Oct 04 13:45:31 1999 +0200
     7.2 +++ b/src/HOL/UNITY/Project.thy	Mon Oct 04 13:47:28 1999 +0200
     7.3 @@ -8,15 +8,4 @@
     7.4  Inheritance of GUARANTEES properties under extension
     7.5  *)
     7.6  
     7.7 -Project = Extend +
     7.8 -
     7.9 -
    7.10 -constdefs
    7.11 -
    7.12 -  restr_act :: "['c set, 'a*'b => 'c, ('a*'a) set] => ('a*'a) set"
    7.13 -    "restr_act C h act == project_act C h (extend_act h act)"
    7.14 -
    7.15 -  restr :: "['c set, 'a*'b => 'c, 'a program] => 'a program"
    7.16 -    "restr C h F == project C h (extend h F)"
    7.17 -
    7.18 -end
    7.19 +Project = Extend
     8.1 --- a/src/HOL/UNITY/Union.ML	Mon Oct 04 13:45:31 1999 +0200
     8.2 +++ b/src/HOL/UNITY/Union.ML	Mon Oct 04 13:47:28 1999 +0200
     8.3 @@ -329,6 +329,11 @@
     8.4  by (force_tac (claset() addSEs [allE, ballE], simpset()) 1);
     8.5  qed "localTo_imp_o_localTo";
     8.6  
     8.7 +Goalw [localTo_def, stable_def, constrains_def]
     8.8 +     "(%s. x) localTo F = UNIV";
     8.9 +by (Blast_tac 1);
    8.10 +qed "triv_localTo_eq_UNIV";
    8.11 +
    8.12  Goal "(F Join G : v localTo H) = (F : v localTo H  &  G : v localTo H)";
    8.13  by (asm_full_simp_tac 
    8.14      (simpset() addsimps [localTo_def, Diff_Join_distrib,