still working; a bit of polishing
authorpaulson
Fri Jan 14 12:17:53 2000 +0100 (2000-01-14)
changeset 81283a5864b465e2
parent 8127 68c6159440f1
child 8129 29e239c7b8c2
still working; a bit of polishing
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/ELT.ML
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Follows.ML
src/HOL/UNITY/Follows.thy
src/HOL/UNITY/GenPrefix.ML
src/HOL/UNITY/LessThan.ML
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Project.ML
src/HOL/UNITY/ROOT.ML
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Thu Jan 13 17:36:58 2000 +0100
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Fri Jan 14 12:17:53 2000 +0100
     1.3 @@ -380,8 +380,7 @@
     1.4  qed "Always_tokens_allocRel_le_rel";
     1.5  
     1.6  (*safety (1), step 4 (final result!) *)
     1.7 -Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \
     1.8 -\              <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}";
     1.9 +Goalw [system_safety_def] "System : system_safety";
    1.10  by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv, 
    1.11  			   Always_tokens_allocRel_le_rel] RS Always_weaken) 1);
    1.12  by Auto_tac;
    1.13 @@ -393,7 +392,6 @@
    1.14  qed "System_safety";
    1.15  
    1.16  
    1.17 -
    1.18  (*** Proof of the progress property (2) ***)
    1.19  
    1.20  (*Now there are proofs identical to System_Increasing_rel and
    1.21 @@ -422,7 +420,7 @@
    1.22  Goal "i < Nclients \
    1.23  \     ==> System : Always \
    1.24  \                   {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
    1.25 -br Always_weaken 1;
    1.26 +by (rtac Always_weaken 1);
    1.27  by (rtac ([guarantees_PLam_I RS client_export UNIV_guar_Always,
    1.28  	   Client_component_System] MRS component_guaranteesD) 1);
    1.29  by (rtac Client_i_Bounded 1);
    1.30 @@ -463,11 +461,11 @@
    1.31  \               (reachable (lift_prog i Client Join G) Int      \
    1.32  \                {s. h <= (giv o sub i) s & h pfixGe (ask o sub i) s} -      \
    1.33  \                {s. tokens h <= tokens ((rel o sub i) s)})";
    1.34 -auto();
    1.35 +by Auto_tac;
    1.36  by (REPEAT (dres_inst_tac [("x", "rel (xa i)")] spec 2));
    1.37  by (REPEAT (dres_inst_tac [("x", "ask (xa i)")] spec 1));
    1.38  by (REPEAT_FIRST ball_tac);
    1.39 -auto();
    1.40 +by Auto_tac;
    1.41  qed "G_stable_lift_prog";
    1.42  
    1.43  Goal "lift_prog i Client \
    1.44 @@ -477,12 +475,12 @@
    1.45  \                             h pfixGe (ask o sub i) s}  \
    1.46  \                  Ensures {s. tokens h <= (tokens o rel o sub i) s})";
    1.47  by (rtac (Client_Progress RS drop_prog_guarantees_raw) 1);
    1.48 -br (lift_export (subset_refl RS project_Increasing_I)) 1;
    1.49 +by (rtac (lift_export project_Increasing_I) 1);
    1.50  by (full_simp_tac (simpset() addsimps [fold_o_sub, lift_prog_correct]) 1);
    1.51 -br INT_I 1;
    1.52 +by (rtac INT_I 1);
    1.53  by (simp_tac (simpset() addsimps [o_apply]) 1);
    1.54  by (REPEAT (stac (lift_export Collect_eq_extend_set) 1));
    1.55 -br (lift_export project_Ensures_D) 1;
    1.56 +by (rtac (lift_export project_Ensures_D) 1);
    1.57  by (asm_full_simp_tac (simpset() addsimps [o_apply, lift_prog_correct, 
    1.58  					   drop_prog_correct]) 1);
    1.59  by (asm_full_simp_tac
    1.60 @@ -492,7 +490,7 @@
    1.61  			 Collect_eq_lift_set RS sym,
    1.62  			 lift_prog_correct RS sym]) 1);
    1.63  by (Clarify_tac 1);
    1.64 -bd G_stable_lift_prog 1;
    1.65 +by (dtac G_stable_lift_prog 1);
    1.66  by (auto_tac (claset(), 
    1.67  	      simpset() addsimps [o_apply]));
    1.68  qed "Client_i_Progress";
    1.69 @@ -505,7 +503,7 @@
    1.70  \                             h pfixGe (ask o sub i) s}  \
    1.71  \                  Ensures {s. tokens h <= (tokens o rel o sub i) s})";
    1.72  by (rtac guarantees_PLam_I 1);
    1.73 -br Client_i_Progress 1;
    1.74 +by (rtac Client_i_Progress 1);
    1.75  by Auto_tac;
    1.76  val lemma2 = result();
    1.77  
    1.78 @@ -523,11 +521,11 @@
    1.79  \           {s. h <= (giv o sub i o client) s & \
    1.80  \               h pfixGe (ask o sub i o client) s} - \
    1.81  \           {s. tokens h <= tokens ((rel o sub i o client) s)})";
    1.82 -auto();
    1.83 +by Auto_tac;
    1.84  by (REPEAT (dres_inst_tac [("x", "rel (client xa i)")] spec 2));
    1.85  by (REPEAT (dres_inst_tac [("x", "ask (client xa i)")] spec 1));
    1.86  by (REPEAT_FIRST ball_tac);
    1.87 -auto();
    1.88 +by Auto_tac;
    1.89  qed "G_stable_sysOfClient";
    1.90  
    1.91  Goal "i < Nclients \
    1.92 @@ -538,20 +536,20 @@
    1.93  \                            h pfixGe (ask o sub i o client) s}  \
    1.94  \                 Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
    1.95  by (rtac (lemma2 RS client_export project_guarantees_raw) 1);
    1.96 -ba 1;
    1.97 -br (client_export (subset_refl RS project_Increasing_I)) 1;
    1.98 +by (assume_tac 1);
    1.99 +by (rtac (client_export project_Increasing_I) 1);
   1.100  by (Simp_tac 1);
   1.101 -br INT_I 1;
   1.102 +by (rtac INT_I 1);
   1.103  by (simp_tac (simpset() addsimps [o_apply]) 1);
   1.104  by (REPEAT (stac (client_export Collect_eq_extend_set) 1));
   1.105 -br (client_export project_Ensures_D) 1;
   1.106 +by (rtac (client_export project_Ensures_D) 1);
   1.107  by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1);
   1.108  by (asm_full_simp_tac
   1.109      (simpset() addsimps [all_conj_distrib,
   1.110  			 Increasing_def, Stable_eq_stable, Join_stable,
   1.111  			 Collect_eq_extend_set RS sym]) 1);
   1.112  by (Clarify_tac 1);
   1.113 -bd G_stable_sysOfClient 1;
   1.114 +by (dtac G_stable_sysOfClient 1);
   1.115  by (auto_tac (claset(), 
   1.116  	      simpset() addsimps [o_apply,
   1.117  				client_export Collect_eq_extend_set RS sym]));
   1.118 @@ -570,7 +568,7 @@
   1.119  	   Client_component_System] MRS component_guaranteesD) 1);
   1.120  by (asm_full_simp_tac
   1.121      (simpset() addsimps [System_Increasing_giv]) 2);
   1.122 -auto();
   1.123 +by Auto_tac;
   1.124  qed "System_Client_Progress";
   1.125  
   1.126  val lemma =
   1.127 @@ -627,50 +625,24 @@
   1.128  	      simpset() addsimps [System_Increasing_allocRel,
   1.129  				  System_Increasing_allocAsk]));
   1.130  by (rtac System_Bounded_allocAsk 1);
   1.131 -by (etac System_Alloc_Progress 1);
   1.132 +by (etac System_Alloc_Client_Progress 1);
   1.133  qed "System_Alloc_Progress";
   1.134  
   1.135  
   1.136 +(*progress (2), step 10 (final result!) *)
   1.137 +Goalw [system_progress_def] "System : system_progress";
   1.138 +by (Clarify_tac 1);
   1.139 +by (rtac LeadsTo_Trans 1);
   1.140 +by (etac (System_Follows_allocGiv RS Follows_LeadsTo_pfixLe) 2);
   1.141 +by (rtac LeadsTo_Trans 1);
   1.142 +by (cut_facts_tac [System_Alloc_Progress] 2);
   1.143 +by (Blast_tac 2);
   1.144 +by (etac (System_Follows_ask RS Follows_LeadsTo) 1);
   1.145 +qed "System_Progress";
   1.146 +
   1.147  
   1.148  (*Ultimate goal*)
   1.149 -Goal "System : system_spec";
   1.150 -
   1.151 -xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
   1.152 -
   1.153 -
   1.154 -(*progress (2), step 10*)
   1.155 -Goal
   1.156 - "System : (INT i : lessThan Nclients. \
   1.157 -\           INT h. {s. h <= (ask o sub i o client) s}  \
   1.158 -\                  LeadsTo {s. h pfixLe (giv o sub i o client) s})";
   1.159 -by (Clarify_tac 1);
   1.160 -by (rtac LeadsTo_Trans 1);
   1.161 -by (dtac (System_Follows_allocGiv RS Follows_LeadsTo) 2);
   1.162 -by (blast_tac (claset() addIs [prefix_imp_pfixLe, LeadsTo_weaken_R]) 2);
   1.163 -
   1.164 -prefix_imp_pfixLe
   1.165 -
   1.166 -
   1.167 -System_Follows_ask
   1.168 +Goalw [system_spec_def] "System : system_spec";
   1.169 +by (blast_tac (claset() addIs [System_safety, System_Progress]) 1);
   1.170 +qed "System_correct";
   1.171  
   1.172 -by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS 
   1.173 -	  Follows_LeadsTo) 2);
   1.174 -
   1.175 -by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
   1.176 -by (rtac LeadsTo_Trans 1);
   1.177 -by (cut_facts_tac [System_Client_Progress] 2);
   1.178 -by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
   1.179 -by (etac lemma3 1);
   1.180 -
   1.181 -by (rtac ([Alloc_Progress, Alloc_component_System] 
   1.182 -	  MRS component_guaranteesD) 1);
   1.183 -(*preserves*)
   1.184 -by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
   1.185 -(*the guarantees precondition*)
   1.186 -by (auto_tac (claset(), 
   1.187 -	      simpset() addsimps [System_Increasing_allocRel,
   1.188 -				  System_Increasing_allocAsk]));
   1.189 -by (rtac System_Bounded_allocAsk 1);
   1.190 -by (etac System_Alloc_Progress 1);
   1.191 -qed "System_Alloc_Progress";
   1.192 -
     2.1 --- a/src/HOL/UNITY/Comp.ML	Thu Jan 13 17:36:58 2000 +0100
     2.2 +++ b/src/HOL/UNITY/Comp.ML	Fri Jan 14 12:17:53 2000 +0100
     2.3 @@ -173,74 +173,3 @@
     2.4  by (Blast_tac 1);
     2.5  qed "Increasing_preserves_Stable";
     2.6  
     2.7 -
     2.8 -(*** givenBy ***)
     2.9 -
    2.10 -Goalw [givenBy_def] "givenBy id = UNIV";
    2.11 -by Auto_tac;
    2.12 -qed "givenBy_id";
    2.13 -Addsimps [givenBy_id];
    2.14 -
    2.15 -Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
    2.16 -by Safe_tac;
    2.17 -by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
    2.18 -by Auto_tac;
    2.19 -qed "givenBy_eq_all";
    2.20 -
    2.21 -Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
    2.22 -by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    2.23 -by Safe_tac;
    2.24 -by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
    2.25 -by (Blast_tac 1);
    2.26 -by Auto_tac;
    2.27 -qed "givenBy_eq_Collect";
    2.28 -
    2.29 -val prems =
    2.30 -Goal "(!!x y. [| x:A;  v x = v y |] ==> y: A) ==> A: givenBy v";
    2.31 -by (stac givenBy_eq_all 1);
    2.32 -by (blast_tac (claset() addIs prems) 1);
    2.33 -qed "givenByI";
    2.34 -
    2.35 -Goalw [givenBy_def] "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A";
    2.36 -by Auto_tac;
    2.37 -qed "givenByD";
    2.38 -
    2.39 -Goal "{} : givenBy v";
    2.40 -by (blast_tac (claset() addSIs [givenByI]) 1);
    2.41 -qed "empty_mem_givenBy";
    2.42 -
    2.43 -AddIffs [empty_mem_givenBy];
    2.44 -
    2.45 -Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
    2.46 -by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
    2.47 -by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    2.48 -by (Blast_tac 1);
    2.49 -qed "givenBy_imp_eq_Collect";
    2.50 -
    2.51 -Goalw [givenBy_def] "{s. P(v s)} : givenBy v";
    2.52 -by (Best_tac 1);
    2.53 -qed "Collect_mem_givenBy";
    2.54 -
    2.55 -Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
    2.56 -by (blast_tac (claset() addIs [Collect_mem_givenBy,
    2.57 -			       givenBy_imp_eq_Collect]) 1);
    2.58 -qed "givenBy_eq_eq_Collect";
    2.59 -
    2.60 -(*preserving v preserves properties given by v*)
    2.61 -Goal "[| F : preserves v;  D : givenBy v |] ==> F : stable D";
    2.62 -by (force_tac (claset(), 
    2.63 -	       simpset() addsimps [impOfSubs preserves_subset_stable, 
    2.64 -				   givenBy_eq_Collect]) 1);
    2.65 -qed "preserves_givenBy_imp_stable";
    2.66 -
    2.67 -Goal "givenBy (w o v) <= givenBy v";
    2.68 -by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    2.69 -by (Deepen_tac 0 1);
    2.70 -qed "givenBy_o_subset";
    2.71 -
    2.72 -Goal "[| A : givenBy v;  B : givenBy v |] ==> A-B : givenBy v";
    2.73 -by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    2.74 -by Safe_tac;
    2.75 -by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
    2.76 -by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
    2.77 -qed "givenBy_DiffI";
     3.1 --- a/src/HOL/UNITY/Comp.thy	Thu Jan 13 17:36:58 2000 +0100
     3.2 +++ b/src/HOL/UNITY/Comp.thy	Fri Jan 14 12:17:53 2000 +0100
     3.3 @@ -26,8 +26,4 @@
     3.4    funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
     3.5      "funPair f g == %x. (f x, g x)"
     3.6  
     3.7 -  (*the set of all sets determined by f alone*)
     3.8 -  givenBy :: "['a => 'b] => 'a set set"
     3.9 -    "givenBy f == range (%B. f-`` B)"
    3.10 -
    3.11  end
     4.1 --- a/src/HOL/UNITY/ELT.ML	Thu Jan 13 17:36:58 2000 +0100
     4.2 +++ b/src/HOL/UNITY/ELT.ML	Fri Jan 14 12:17:53 2000 +0100
     4.3 @@ -6,6 +6,93 @@
     4.4  leadsTo strengthened with a specification of the allowable sets transient parts
     4.5  *)
     4.6  
     4.7 +(*** givenBy ***)
     4.8 +
     4.9 +Goalw [givenBy_def] "givenBy id = UNIV";
    4.10 +by Auto_tac;
    4.11 +qed "givenBy_id";
    4.12 +Addsimps [givenBy_id];
    4.13 +
    4.14 +Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
    4.15 +by Safe_tac;
    4.16 +by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
    4.17 +by Auto_tac;
    4.18 +qed "givenBy_eq_all";
    4.19 +
    4.20 +Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
    4.21 +by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    4.22 +by Safe_tac;
    4.23 +by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
    4.24 +by (Blast_tac 1);
    4.25 +by Auto_tac;
    4.26 +qed "givenBy_eq_Collect";
    4.27 +
    4.28 +val prems =
    4.29 +Goal "(!!x y. [| x:A;  v x = v y |] ==> y: A) ==> A: givenBy v";
    4.30 +by (stac givenBy_eq_all 1);
    4.31 +by (blast_tac (claset() addIs prems) 1);
    4.32 +qed "givenByI";
    4.33 +
    4.34 +Goalw [givenBy_def] "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A";
    4.35 +by Auto_tac;
    4.36 +qed "givenByD";
    4.37 +
    4.38 +Goal "{} : givenBy v";
    4.39 +by (blast_tac (claset() addSIs [givenByI]) 1);
    4.40 +qed "empty_mem_givenBy";
    4.41 +
    4.42 +AddIffs [empty_mem_givenBy];
    4.43 +
    4.44 +Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
    4.45 +by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
    4.46 +by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    4.47 +by (Blast_tac 1);
    4.48 +qed "givenBy_imp_eq_Collect";
    4.49 +
    4.50 +Goalw [givenBy_def] "{s. P(v s)} : givenBy v";
    4.51 +by (Best_tac 1);
    4.52 +qed "Collect_mem_givenBy";
    4.53 +
    4.54 +Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
    4.55 +by (blast_tac (claset() addIs [Collect_mem_givenBy,
    4.56 +			       givenBy_imp_eq_Collect]) 1);
    4.57 +qed "givenBy_eq_eq_Collect";
    4.58 +
    4.59 +(*preserving v preserves properties given by v*)
    4.60 +Goal "[| F : preserves v;  D : givenBy v |] ==> F : stable D";
    4.61 +by (force_tac (claset(), 
    4.62 +	       simpset() addsimps [impOfSubs preserves_subset_stable, 
    4.63 +				   givenBy_eq_Collect]) 1);
    4.64 +qed "preserves_givenBy_imp_stable";
    4.65 +
    4.66 +Goal "givenBy (w o v) <= givenBy v";
    4.67 +by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    4.68 +by (Deepen_tac 0 1);
    4.69 +qed "givenBy_o_subset";
    4.70 +
    4.71 +Goal "[| A : givenBy v;  B : givenBy v |] ==> A-B : givenBy v";
    4.72 +by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    4.73 +by Safe_tac;
    4.74 +by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
    4.75 +by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
    4.76 +qed "givenBy_DiffI";
    4.77 +
    4.78 +Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
    4.79 +by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    4.80 +by (Deepen_tac 0 1);
    4.81 +qed "givenBy_o_eq_extend_set";
    4.82 +
    4.83 +Goal "givenBy f = range (extend_set h)";
    4.84 +by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    4.85 +by (Deepen_tac 0 1);
    4.86 +qed "givenBy_eq_extend_set";
    4.87 +
    4.88 +Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
    4.89 +by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    4.90 +by (Blast_tac 1);
    4.91 +qed "extend_set_givenBy_I";
    4.92 +
    4.93 +
    4.94  (** Standard leadsTo rules **)
    4.95  
    4.96  Goalw [leadsETo_def]
     5.1 --- a/src/HOL/UNITY/ELT.thy	Thu Jan 13 17:36:58 2000 +0100
     5.2 +++ b/src/HOL/UNITY/ELT.thy	Fri Jan 14 12:17:53 2000 +0100
     5.3 @@ -43,6 +43,10 @@
     5.4  
     5.5  
     5.6  constdefs
     5.7 +  
     5.8 +  (*the set of all sets determined by f alone*)
     5.9 +  givenBy :: "['a => 'b] => 'a set set"
    5.10 +    "givenBy f == range (%B. f-`` B)"
    5.11  
    5.12    (*visible version of the LEADS-TO relation*)
    5.13    leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
     6.1 --- a/src/HOL/UNITY/Extend.ML	Thu Jan 13 17:36:58 2000 +0100
     6.2 +++ b/src/HOL/UNITY/Extend.ML	Fri Jan 14 12:17:53 2000 +0100
     6.3 @@ -569,24 +569,6 @@
     6.4  qed "extend_LeadsTo";
     6.5  
     6.6  
     6.7 -(*** givenBy: USEFUL??? ***)
     6.8 -
     6.9 -Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
    6.10 -by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    6.11 -by (Deepen_tac 0 1);
    6.12 -qed "givenBy_o_eq_extend_set";
    6.13 -
    6.14 -Goal "givenBy f = range (extend_set h)";
    6.15 -by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    6.16 -by (Deepen_tac 0 1);
    6.17 -qed "givenBy_eq_extend_set";
    6.18 -
    6.19 -Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
    6.20 -by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    6.21 -by (Blast_tac 1);
    6.22 -qed "extend_set_givenBy_I";
    6.23 -
    6.24 -
    6.25  Close_locale "Extend";
    6.26  
    6.27  (*Close_locale should do this!
     7.1 --- a/src/HOL/UNITY/Follows.ML	Thu Jan 13 17:36:58 2000 +0100
     7.2 +++ b/src/HOL/UNITY/Follows.ML	Fri Jan 14 12:17:53 2000 +0100
     7.3 @@ -22,7 +22,6 @@
     7.4  by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
     7.5  qed "mono_LeadsTo_o";
     7.6  
     7.7 -(*NOT PROVABLE USING leadsETo because givenBy f <= givenBy (h o f) fails*)
     7.8  Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";
     7.9  by (Clarify_tac 1);
    7.10  by (asm_full_simp_tac
    7.11 @@ -31,34 +30,17 @@
    7.12  			 impOfSubs mono_LeadsTo_o RS INT_D]) 1);
    7.13  qed "mono_Follows_o";
    7.14  
    7.15 -(*NOT PROVABLE USING leadsETo since it needs the previous thm*)
    7.16  Goal "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))";
    7.17  by (dtac mono_Follows_o 1);
    7.18  by (force_tac (claset(), simpset() addsimps [o_def]) 1);
    7.19  qed "mono_Follows_apply";
    7.20  
    7.21 -(*NOT PROVABLE USING leadsETo since givenBy g doesn't imply givenBy f*)
    7.22  Goalw [Follows_def]
    7.23       "[| F : f Fols g;  F: g Fols h |] ==> F : f Fols h";
    7.24  by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    7.25  by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);
    7.26  qed "Follows_trans";
    7.27  
    7.28 -(*
    7.29 -try:
    7.30 -by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    7.31 -by Auto_tac;
    7.32 -by (blast_tac (claset() addIs [order_trans, LeadsETo_Trans]) 1);
    7.33 -by (rtac LeadsETo_Trans 1);
    7.34 -by (Blast_tac 2);
    7.35 -by (dtac spec 1);
    7.36 -by (etac LeadsETo_weaken 1);
    7.37 -by Auto_tac;
    7.38 -by (thin_tac "All ?P" 1);
    7.39 -by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    7.40 -by Safe_tac;
    7.41 -**)
    7.42 -
    7.43  
    7.44  (** Destructiom rules **)
    7.45  
    7.46 @@ -82,6 +64,24 @@
    7.47  by (Blast_tac 1);
    7.48  qed "Follows_LeadsTo";
    7.49  
    7.50 +Goal "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}";
    7.51 +by (rtac single_LeadsTo_I 1);
    7.52 +by (Clarify_tac 1);
    7.53 +by (dtac Follows_LeadsTo 1);
    7.54 +by (etac LeadsTo_weaken 1);
    7.55 +by (blast_tac set_cs 1);
    7.56 +by (blast_tac (claset() addIs [pfixLe_trans, prefix_imp_pfixLe]) 1);
    7.57 +qed "Follows_LeadsTo_pfixLe";
    7.58 +
    7.59 +Goal "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}";
    7.60 +by (rtac single_LeadsTo_I 1);
    7.61 +by (Clarify_tac 1);
    7.62 +by (dtac Follows_LeadsTo 1);
    7.63 +by (etac LeadsTo_weaken 1);
    7.64 +by (blast_tac set_cs 1);
    7.65 +by (blast_tac (claset() addIs [pfixGe_trans, prefix_imp_pfixGe]) 1);
    7.66 +qed "Follows_LeadsTo_pfixGe";
    7.67 +
    7.68  
    7.69  (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
    7.70  
     8.1 --- a/src/HOL/UNITY/Follows.thy	Thu Jan 13 17:36:58 2000 +0100
     8.2 +++ b/src/HOL/UNITY/Follows.thy	Fri Jan 14 12:17:53 2000 +0100
     8.3 @@ -3,13 +3,10 @@
     8.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.5      Copyright   1998  University of Cambridge
     8.6  
     8.7 -The Follows relation of Charpentier and Sivilotte
     8.8 -
     8.9 -The safety conditions ensures that "givenBy f" is implementable in the
    8.10 -  progress part: g cannot do anything silly.
    8.11 +The "Follows" relation of Charpentier and Sivilotte
    8.12  *)
    8.13  
    8.14 -Follows = Project +
    8.15 +Follows = SubstAx +
    8.16  
    8.17  constdefs
    8.18  
     9.1 --- a/src/HOL/UNITY/GenPrefix.ML	Thu Jan 13 17:36:58 2000 +0100
     9.2 +++ b/src/HOL/UNITY/GenPrefix.ML	Fri Jan 14 12:17:53 2000 +0100
     9.3 @@ -313,9 +313,17 @@
     9.4  by (Force_tac 1);
     9.5  qed "prefix_append_iff";
     9.6  
     9.7 +Goal "r<=s ==> genPrefix r <= genPrefix s";
     9.8 +by (Clarify_tac 1);
     9.9 +by (etac genPrefix.induct 1);
    9.10 +by (auto_tac (claset() addIs [genPrefix.append], simpset()));
    9.11 +qed "genPrefix_mono";
    9.12 +
    9.13  
    9.14  (*** pfixLe, pfixGe: properties inherited from the translations ***)
    9.15  
    9.16 +(** pfixLe **)
    9.17 +
    9.18  Goalw [refl_def, Le_def] "reflexive Le";
    9.19  by Auto_tac;
    9.20  qed "reflexive_Le";
    9.21 @@ -330,6 +338,23 @@
    9.22  
    9.23  AddIffs [reflexive_Le, antisym_Le, trans_Le];
    9.24  
    9.25 +Goal "x pfixLe x";
    9.26 +by (Simp_tac 1);
    9.27 +qed "pfixLe_refl";
    9.28 +AddIffs[pfixLe_refl];
    9.29 +
    9.30 +Goal "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z";
    9.31 +by (blast_tac (claset() addIs [genPrefix_trans]) 1);
    9.32 +qed "pfixLe_trans";
    9.33 +
    9.34 +Goal "[| x pfixLe y; y pfixLe x |] ==> x = y";
    9.35 +by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
    9.36 +qed "pfixLe_antisym";
    9.37 +
    9.38 +Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys";
    9.39 +by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
    9.40 +qed "prefix_imp_pfixLe";
    9.41 +
    9.42  Goalw [refl_def, Ge_def] "reflexive Ge";
    9.43  by Auto_tac;
    9.44  qed "reflexive_Ge";
    9.45 @@ -344,15 +369,18 @@
    9.46  
    9.47  AddIffs [reflexive_Ge, antisym_Ge, trans_Ge];
    9.48  
    9.49 -Goal "r<=s ==> genPrefix r <= genPrefix s";
    9.50 -by (Clarify_tac 1);
    9.51 -by (etac genPrefix.induct 1);
    9.52 -by (auto_tac (claset() addIs [genPrefix.append], simpset()));
    9.53 -qed "genPrefix_mono";
    9.54 +Goal "x pfixGe x";
    9.55 +by (Simp_tac 1);
    9.56 +qed "pfixGe_refl";
    9.57 +AddIffs[pfixGe_refl];
    9.58  
    9.59 -Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys";
    9.60 -by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
    9.61 -qed "prefix_imp_pfixLe";
    9.62 +Goal "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z";
    9.63 +by (blast_tac (claset() addIs [genPrefix_trans]) 1);
    9.64 +qed "pfixGe_trans";
    9.65 +
    9.66 +Goal "[| x pfixGe y; y pfixGe x |] ==> x = y";
    9.67 +by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
    9.68 +qed "pfixGe_antisym";
    9.69  
    9.70  Goalw [prefix_def, Ge_def] "xs<=ys ==> xs pfixGe ys";
    9.71  by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
    10.1 --- a/src/HOL/UNITY/LessThan.ML	Thu Jan 13 17:36:58 2000 +0100
    10.2 +++ b/src/HOL/UNITY/LessThan.ML	Fri Jan 14 12:17:53 2000 +0100
    10.3 @@ -50,17 +50,6 @@
    10.4  by Auto_tac;
    10.5  qed "Restrict_imageI";
    10.6  
    10.7 -Goal "(Restrict A `` (Restrict A `` r - s)) = (Restrict A `` r - s)";
    10.8 -by Auto_tac;
    10.9 -by (rewrite_goals_tac [image_def, Restrict_def]);
   10.10 -by (Blast_tac 1);
   10.11 -qed "Restrict_image_Diff";
   10.12 -
   10.13 -(*Nothing to do with Restrict, but to specialized for Fun.ML?*)
   10.14 -Goal "f``(g``A - B) = (UN x: (A - g-`` B). {f(g(x))})";
   10.15 -by (Blast_tac 1);
   10.16 -qed "image_Diff_image_eq";
   10.17 -
   10.18  Goal "Domain (Restrict A r) = A Int Domain r";
   10.19  by (Blast_tac 1);
   10.20  qed "Domain_Restrict";
    11.1 --- a/src/HOL/UNITY/Lift_prog.ML	Thu Jan 13 17:36:58 2000 +0100
    11.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Fri Jan 14 12:17:53 2000 +0100
    11.3 @@ -211,27 +211,11 @@
    11.4  qed "drop_set_INT";
    11.5  
    11.6  Goal "lift_set i UNIV = UNIV";
    11.7 -by (simp_tac
    11.8 -    (simpset() addsimps [lift_set_correct, lift_export0 extend_set_UNIV_eq]) 1);
    11.9 +by (simp_tac (simpset() addsimps [lift_set_correct, 
   11.10 +				  lift_export0 extend_set_UNIV_eq]) 1);
   11.11  qed "lift_set_UNIV_eq";
   11.12  Addsimps [lift_set_UNIV_eq];
   11.13  
   11.14 -(*
   11.15 -Goal "Domain act <= drop_set i C ==> drop_act i (Restrict C (lift_act i act)) = act";
   11.16 -by (asm_full_simp_tac
   11.17 -    (simpset() addsimps [drop_set_correct, drop_act_correct, 
   11.18 -			 lift_act_correct, lift_export0 extend_act_inverse]) 1);
   11.19 -qed "lift_act_inverse";
   11.20 -Addsimps [lift_act_inverse];
   11.21 -*)
   11.22 -
   11.23 -Goal "UNIV <= drop_set i C ==> drop_prog i C (lift_prog i F) = F";
   11.24 -by (asm_full_simp_tac
   11.25 -    (simpset() addsimps [drop_set_correct, drop_prog_correct, 
   11.26 -			 lift_prog_correct, lift_export0 extend_inverse]) 1);
   11.27 -qed "lift_prog_inverse";
   11.28 -Addsimps [lift_prog_inverse];
   11.29 -
   11.30  Goal "inj (lift_prog i)";
   11.31  by (simp_tac
   11.32      (simpset() addsimps [lift_prog_correct, lift_export0 inj_extend]) 1);
   11.33 @@ -291,8 +275,8 @@
   11.34  Goal "(drop_prog i C F : A co B)  =  \
   11.35  \     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
   11.36  by (simp_tac
   11.37 -    (simpset() addsimps [drop_prog_correct, 
   11.38 -			 lift_set_correct, lift_export0 project_constrains]) 1);
   11.39 +    (simpset() addsimps [drop_prog_correct, lift_set_correct, 
   11.40 +			 lift_export0 project_constrains]) 1);
   11.41  qed "drop_prog_constrains";
   11.42  
   11.43  Goal "(drop_prog i UNIV F : stable A)  =  (F : stable (lift_set i A))";
   11.44 @@ -321,8 +305,7 @@
   11.45  by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1);
   11.46  qed "lift_prog_Stable";
   11.47  
   11.48 -Goal "[| reachable (lift_prog i F Join G) <= C;    \
   11.49 -\        F Join drop_prog i C G : A Co B |] \
   11.50 +Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : A Co B  \
   11.51  \     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
   11.52  by (asm_full_simp_tac
   11.53      (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   11.54 @@ -330,14 +313,12 @@
   11.55  qed "drop_prog_Constrains_D";
   11.56  
   11.57  Goalw [Stable_def]
   11.58 -     "[| reachable (lift_prog i F Join G) <= C;    \
   11.59 -\        F Join drop_prog i C G : Stable A |]  \
   11.60 +     "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Stable A  \
   11.61  \     ==> lift_prog i F Join G : Stable (lift_set i A)";
   11.62  by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
   11.63  qed "drop_prog_Stable_D";
   11.64  
   11.65 -Goal "[| reachable (lift_prog i F Join G) <= C;  \
   11.66 -\        F Join drop_prog i C G : Always A |]   \
   11.67 +Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Always A  \
   11.68  \     ==> lift_prog i F Join G : Always (lift_set i A)";
   11.69  by (asm_full_simp_tac
   11.70      (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   11.71 @@ -345,24 +326,14 @@
   11.72  qed "drop_prog_Always_D";
   11.73  
   11.74  Goalw [Increasing_def]
   11.75 -     "[| reachable (lift_prog i F Join G) <= C;  \
   11.76 -\        F Join drop_prog i C G : Increasing func |] \
   11.77 -\     ==> lift_prog i F Join G : Increasing (func o (sub i))";
   11.78 + "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Increasing func \
   11.79 +\ ==> lift_prog i F Join G : Increasing (func o (sub i))";
   11.80  by Auto_tac;
   11.81  by (stac Collect_eq_lift_set 1);
   11.82  by (asm_simp_tac (simpset() addsimps [drop_prog_Stable_D]) 1); 
   11.83  qed "project_Increasing_D";
   11.84  
   11.85  
   11.86 -(*UNUSED*)
   11.87 -Goal "UNIV <= drop_set i C \
   11.88 -\     ==> drop_prog i C ((lift_prog i F) Join G) = F Join (drop_prog i C G)";
   11.89 -by (asm_full_simp_tac
   11.90 -    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   11.91 -		     drop_set_correct, lift_export0 project_extend_Join]) 1);
   11.92 -qed "drop_prog_lift_prog_Join";
   11.93 -
   11.94 -
   11.95  (*** Progress: transient, ensures ***)
   11.96  
   11.97  Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
    12.1 --- a/src/HOL/UNITY/Project.ML	Thu Jan 13 17:36:58 2000 +0100
    12.2 +++ b/src/HOL/UNITY/Project.ML	Fri Jan 14 12:17:53 2000 +0100
    12.3 @@ -6,16 +6,8 @@
    12.4  Projections of state sets (also of actions and programs)
    12.5  
    12.6  Inheritance of GUARANTEES properties under extension
    12.7 -
    12.8 -POSSIBLY CAN DELETE Restrict_image_Diff
    12.9  *)
   12.10  
   12.11 -(*EQUALITIES.ML*)
   12.12 -		Goal "(A <= -A) = (A = {})";
   12.13 -		by (Blast_tac 1);
   12.14 -		qed "subset_Compl_self_eq";
   12.15 -
   12.16 -
   12.17  Open_locale "Extend";
   12.18  
   12.19  (** projection: monotonicity for safety **)
   12.20 @@ -297,37 +289,30 @@
   12.21  by (etac extend_act_D 1);
   12.22  qed "reachable_imp_reachable_project";
   12.23  
   12.24 -(*The extra generality in the first premise allows guarantees with STRONG
   12.25 -  preconditions (localT) and WEAK postconditions.*)
   12.26 -(*LOCALTO NO LONGER EXISTS: replace C by reachable...??*)
   12.27  Goalw [Constrains_def]
   12.28 -     "[| reachable (extend h F Join G) <= C;    \
   12.29 -\        F Join project h C G : A Co B |] \
   12.30 +     "F Join project h (reachable (extend h F Join G)) G : A Co B  \
   12.31  \     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
   12.32  by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
   12.33  by (Clarify_tac 1);
   12.34  by (etac constrains_weaken 1);
   12.35 -by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
   12.36 +by (auto_tac (claset() addIs [reachable_imp_reachable_project], simpset()));
   12.37  qed "project_Constrains_D";
   12.38  
   12.39  Goalw [Stable_def]
   12.40 -     "[| reachable (extend h F Join G) <= C;  \
   12.41 -\        F Join project h C G : Stable A |]   \
   12.42 +     "F Join project h (reachable (extend h F Join G)) G : Stable A  \
   12.43  \     ==> extend h F Join G : Stable (extend_set h A)";
   12.44  by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
   12.45  qed "project_Stable_D";
   12.46  
   12.47  Goalw [Always_def]
   12.48 -     "[| reachable (extend h F Join G) <= C;  \
   12.49 -\        F Join project h C G : Always A |]   \
   12.50 +     "F Join project h (reachable (extend h F Join G)) G : Always A  \
   12.51  \     ==> extend h F Join G : Always (extend_set h A)";
   12.52  by (force_tac (claset() addIs [reachable.Init],
   12.53                 simpset() addsimps [project_Stable_D, split_extended_all]) 1);
   12.54  qed "project_Always_D";
   12.55  
   12.56  Goalw [Increasing_def]
   12.57 -     "[| reachable (extend h F Join G) <= C;  \
   12.58 -\        F Join project h C G : Increasing func |] \
   12.59 +     "F Join project h (reachable (extend h F Join G)) G : Increasing func  \
   12.60  \     ==> extend h F Join G : Increasing (func o f)";
   12.61  by Auto_tac;
   12.62  by (stac Collect_eq_extend_set 1);
   12.63 @@ -364,45 +349,37 @@
   12.64  	      simpset()));
   12.65  qed "reachable_extend_Join_subset";
   12.66  
   12.67 -(*Perhaps should replace C by reachable...*)
   12.68  Goalw [Constrains_def]
   12.69 -     "[| C <= reachable (extend h F Join G);  \
   12.70 -\        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
   12.71 -\     ==> F Join project h C G : A Co B";
   12.72 +     "extend h F Join G : (extend_set h A) Co (extend_set h B)  \
   12.73 +\     ==> F Join project h (reachable (extend h F Join G)) G : A Co B";
   12.74  by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
   12.75  				       extend_set_Int_distrib]) 1);
   12.76  by (rtac conjI 1);
   12.77 -by (etac constrains_weaken 1);
   12.78 -by Auto_tac;
   12.79 -by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1);
   12.80 -(*Some generalization of constrains_weaken_L would be better, but what is it?*)
   12.81 -by (rewtac constrains_def);
   12.82 -by Auto_tac;
   12.83 -by (thin_tac "ALL act : Acts G. ?P act" 1);
   12.84 -by (force_tac (claset() addSDs [reachable_project_imp_reachable], 
   12.85 -	       simpset()) 1);
   12.86 +by (force_tac
   12.87 +    (claset() addEs [constrains_weaken_L]
   12.88 +              addSDs [extend_constrains_project_set,
   12.89 +		      subset_refl RS reachable_project_imp_reachable], 
   12.90 +     simpset() addsimps [Join_constrains]) 2);
   12.91 +by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
   12.92  qed "project_Constrains_I";
   12.93  
   12.94  Goalw [Stable_def]
   12.95 -     "[| C <= reachable (extend h F Join G);  \
   12.96 -\        extend h F Join G : Stable (extend_set h A) |] \
   12.97 -\     ==> F Join project h C G : Stable A";
   12.98 +     "extend h F Join G : Stable (extend_set h A)  \
   12.99 +\     ==> F Join project h (reachable (extend h F Join G)) G : Stable A";
  12.100  by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
  12.101  qed "project_Stable_I";
  12.102  
  12.103  Goalw [Always_def]
  12.104 -     "[| C <= reachable (extend h F Join G);  \
  12.105 -\        extend h F Join G : Always (extend_set h A) |]   \
  12.106 -\     ==> F Join project h C G : Always A";
  12.107 +     "extend h F Join G : Always (extend_set h A)  \
  12.108 +\     ==> F Join project h (reachable (extend h F Join G)) G : Always A";
  12.109  by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
  12.110  by (rewtac extend_set_def);
  12.111  by (Blast_tac 1);
  12.112  qed "project_Always_I";
  12.113  
  12.114  Goalw [Increasing_def]
  12.115 -     "[| C <= reachable (extend h F Join G);  \
  12.116 -\        extend h F Join G : Increasing (func o f) |] \
  12.117 -\     ==> F Join project h C G : Increasing func";
  12.118 +    "extend h F Join G : Increasing (func o f)  \
  12.119 +\    ==> F Join project h (reachable (extend h F Join G)) G : Increasing func";
  12.120  by Auto_tac;
  12.121  by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
  12.122  				      project_Stable_I]) 1); 
  12.123 @@ -471,11 +448,10 @@
  12.124  by (blast_tac (claset() addIs [project_Always_D]) 1);
  12.125  qed "extending_Always";
  12.126  
  12.127 -val [prem] = 
  12.128  Goalw [extending_def]
  12.129 -     "(!!G. reachable (extend h F Join G) <= C G)  \
  12.130 -\     ==> extending v C h F (Increasing (func o f)) (Increasing func)";
  12.131 -by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1);
  12.132 +     "extending v (%G. reachable (extend h F Join G)) h F \
  12.133 +\                 (Increasing (func o f)) (Increasing func)";
  12.134 +by (blast_tac (claset() addIs [project_Increasing_D]) 1);
  12.135  qed "extending_Increasing";
  12.136  
  12.137  
  12.138 @@ -630,10 +606,10 @@
  12.139  by (auto_tac (claset(), 
  12.140  	      simpset() addsimps [Int_Diff,
  12.141  				  extend_set_Diff_distrib RS sym]));
  12.142 -bd act_subset_imp_project_act_subset 1;
  12.143 +by (dtac act_subset_imp_project_act_subset 1);
  12.144  by (subgoal_tac
  12.145      "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1);
  12.146 -bws [Restrict_def, project_set_def, extend_set_def, project_act_def];
  12.147 +by (rewrite_goals_tac [Restrict_def, project_set_def, extend_set_def, project_act_def]);
  12.148  (*using Int_greatest actually slows the next step!*)
  12.149  by (Blast_tac 2);
  12.150  by (force_tac (claset(), 
  12.151 @@ -670,9 +646,9 @@
  12.152  Goal "[| F Join project h UNIV G : A ensures B;  \
  12.153  \        G : stable (extend_set h A - extend_set h B) |] \
  12.154  \     ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
  12.155 -br (project_ensures_D_lemma RS revcut_rl) 1;
  12.156 +by (rtac (project_ensures_D_lemma RS revcut_rl) 1);
  12.157  by (stac stable_UNIV 3);
  12.158 -auto();
  12.159 +by Auto_tac;
  12.160  qed "project_ensures_D";
  12.161  
  12.162  Goalw [Ensures_def]
  12.163 @@ -680,7 +656,7 @@
  12.164  \        G : stable (reachable (extend h F Join G) Int extend_set h A - \
  12.165  \                    extend_set h B) |] \
  12.166  \     ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)";
  12.167 -br (project_ensures_D_lemma RS revcut_rl) 1;
  12.168 +by (rtac (project_ensures_D_lemma RS revcut_rl) 1);
  12.169  by (auto_tac (claset(), 
  12.170  	      simpset() addsimps [project_set_reachable_extend_eq RS sym]));
  12.171  qed "project_Ensures_D";
    13.1 --- a/src/HOL/UNITY/ROOT.ML	Thu Jan 13 17:36:58 2000 +0100
    13.2 +++ b/src/HOL/UNITY/ROOT.ML	Fri Jan 14 12:17:53 2000 +0100
    13.3 @@ -28,7 +28,7 @@
    13.4  time_use_thy "Extend";
    13.5  time_use_thy "PPROD";
    13.6  time_use_thy "TimerArray";
    13.7 -time_use_thy "Follows";
    13.8 +time_use_thy "Alloc";
    13.9  
   13.10  add_path "../Auth";	(*to find Public.thy*)
   13.11  use_thy"NSP_Bad";