a bit further with property (1)
authorpaulson
Thu Aug 26 11:46:04 1999 +0200 (1999-08-26)
changeset 7365b5bb32e0861c
parent 7364 a979e8a2ee18
child 7366 22a64baa7013
a bit further with property (1)
src/HOL/UNITY/Alloc.ML
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Thu Aug 26 11:39:18 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Thu Aug 26 11:46:04 1999 +0200
     1.3 @@ -6,21 +6,6 @@
     1.4  Specification of Chandy and Charpentier's Allocator
     1.5  *)
     1.6  
     1.7 -		Goal "(%(x,y). f(x,y)) = f";
     1.8 -		by (rtac ext 1);
     1.9 -		by (pair_tac "x" 1);
    1.10 -		by (Simp_tac 1);
    1.11 -		qed "split_Pair_apply";
    1.12 -
    1.13 -		Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
    1.14 -		by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
    1.15 -		qed "split_paired_Eps";
    1.16 -
    1.17 -		Goal "[| inj(f);  f x = y |] ==> inv f y = x";
    1.18 -		by (etac subst 1);
    1.19 -		by (etac inv_f_f 1);
    1.20 -		qed "inv_f_eq";
    1.21 -
    1.22  (*Generalized version allowing different clients*)
    1.23  Goal "[| Alloc : alloc_spec;  \
    1.24  \        Client : (lessThan Nclients) funcset client_spec;  \
    1.25 @@ -47,8 +32,8 @@
    1.26  
    1.27  AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
    1.28  
    1.29 -(**THESE SHOULD NOT BE NECESSARY...THE VARIOUS INJECTIONS INTO THE SYSTEM
    1.30 -   STATE NEED TO BE TREATED SYMMETRICALLY OR DONE AUTOMATICALLY*)
    1.31 +(**SHOULD NOT BE NECESSARY: The various injections into the system
    1.32 +   state need to be treated symmetrically or done automatically*)
    1.33  Goalw [sysOfClient_def] "inj sysOfClient";
    1.34  by (rtac injI 1);
    1.35  by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD]
    1.36 @@ -65,59 +50,6 @@
    1.37  AddIffs [inj_sysOfClient, surj_sysOfClient];
    1.38  
    1.39  
    1.40 -Open_locale "System";
    1.41 -
    1.42 -val Alloc = thm "Alloc";
    1.43 -val Client = thm "Client";
    1.44 -val Network = thm "Network";
    1.45 -val System_def = thm "System_def";
    1.46 -
    1.47 -AddIffs [finite_lessThan];
    1.48 -
    1.49 -
    1.50 -Goal "Client : UNIV guar Increasing ask";
    1.51 -by (cut_facts_tac [Client] 1);
    1.52 -by (asm_full_simp_tac
    1.53 -    (simpset() addsimps [client_spec_def, client_increasing_def,
    1.54 -			 guarantees_Int_right]) 1);
    1.55 -qed "Client_Increasing_ask";
    1.56 -
    1.57 -Goal "Client : UNIV guar Increasing rel";
    1.58 -by (cut_facts_tac [Client] 1);
    1.59 -by (asm_full_simp_tac
    1.60 -    (simpset() addsimps [client_spec_def, client_increasing_def,
    1.61 -			 guarantees_Int_right]) 1);
    1.62 -qed "Client_Increasing_rel";
    1.63 -
    1.64 -AddIffs [Client_Increasing_ask, Client_Increasing_rel];
    1.65 -
    1.66 -Goal "Client : UNIV guar Always {s. ALL elt : set (ask s). elt <= NbT}";
    1.67 -by (cut_facts_tac [Client] 1);
    1.68 -by (asm_full_simp_tac
    1.69 -    (simpset() addsimps [client_spec_def, client_bounded_def]) 1);
    1.70 -qed "Client_Bounded";
    1.71 -
    1.72 -(*Client_Progress we omit for now, since it's cumbersome to state*)
    1.73 -
    1.74 -
    1.75 -
    1.76 -Goal "lift_prog i Client : UNIV guar Increasing (rel o sub i)";
    1.77 -by (rtac (Client_Increasing_rel RS lift_prog_guar_Increasing) 1);
    1.78 -qed "lift_prog_Client_Increasing_rel";
    1.79 -
    1.80 -
    1.81 -
    1.82 -(*Comp.ML??????????*)
    1.83 -
    1.84 -
    1.85 -
    1.86 -val project_guarantees' =
    1.87 -  [inj_sysOfClient, surj_sysOfClient] MRS export project_guarantees;
    1.88 -
    1.89 -val extend_guar_Increasing' =
    1.90 -  [inj_sysOfClient, surj_sysOfClient] MRS export extend_guar_Increasing;
    1.91 -
    1.92 -
    1.93  (*MUST BE AUTOMATED: even the statement of such results*)
    1.94  Goal "!!s. inv sysOfClient s = \
    1.95  \            (client s, \
    1.96 @@ -127,81 +59,123 @@
    1.97  by (rtac (inj_sysOfClient RS inv_f_eq) 1);
    1.98  by (rewrite_goals_tac [sysOfAlloc_def, sysOfClient_def]);
    1.99  by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
   1.100 -qed "inv_sysOfClient";
   1.101 -
   1.102 -
   1.103 +qed "inv_sysOfClient_eq";
   1.104  
   1.105  
   1.106 -val prems =
   1.107 -Goalw [PLam_def]
   1.108 -     "[| !!i. i:I ==> F i : X i guar Y i;  \
   1.109 -\        !!i H. [| i:I; H : XX i |] ==> drop_prog i H : X i;  \
   1.110 -\        !!i G. [| i:I; F i Join drop_prog i G : Y i |] \
   1.111 -\               ==> lift_prog i (F i) Join G : YY i |] \
   1.112 -\        ==> (PLam I F) : (INTER I XX) guar (INTER I YY)";
   1.113 -by (rtac (drop_prog_guarantees RS guarantees_JN_INT) 1);
   1.114 -by (REPEAT (ares_tac prems 1));
   1.115 -qed "drop_prog_guarantees_PLam";
   1.116 +Open_locale "System";
   1.117 +
   1.118 +val Alloc = thm "Alloc";
   1.119 +val Client = thm "Client";
   1.120 +val Network = thm "Network";
   1.121 +val System_def = thm "System_def";
   1.122 +
   1.123 +AddIffs [finite_lessThan];
   1.124 +
   1.125 +(*Client : <unfolded specification> *)
   1.126 +val Client_Spec =
   1.127 +    rewrite_rule [client_spec_def, client_increasing_def,
   1.128 +		  client_bounded_def, client_progress_def] Client;
   1.129 +
   1.130 +Goal "Client : UNIV guarantees Increasing ask";
   1.131 +by (cut_facts_tac [Client_Spec] 1);
   1.132 +by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
   1.133 +qed "Client_Increasing_ask";
   1.134 +
   1.135 +Goal "Client : UNIV guarantees Increasing rel";
   1.136 +by (cut_facts_tac [Client_Spec] 1);
   1.137 +by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
   1.138 +qed "Client_Increasing_rel";
   1.139 +
   1.140 +AddIffs [Client_Increasing_ask, Client_Increasing_rel];
   1.141 +
   1.142 +Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
   1.143 +by (cut_facts_tac [Client_Spec] 1);
   1.144 +by Auto_tac;
   1.145 +qed "Client_Bounded";
   1.146 +
   1.147 +(*Client_Progress is cumbersome to state*)
   1.148 +val Client_Progress = Client_Spec RS IntD2;
   1.149  
   1.150  
   1.151 -(*for proof of property (1) *)
   1.152 -Goal "i < Nclients ==> System : Increasing (rel o sub i o client)";
   1.153 -by (full_simp_tac (simpset() addsimps [System_def]) 1);
   1.154 -by (rtac ([asm_rl, UNIV_I] MRS guaranteesD) 1);
   1.155 -by (rtac (disjI2 RS guarantees_Join_I) 1);
   1.156 -by (rtac project_guarantees' 1);
   1.157 -by (rtac subset_refl 2);
   1.158 -by (Clarify_tac 2);
   1.159 -by (rtac ([extend_guar_Increasing',subset_refl] MRS 
   1.160 -    guarantees_weaken RS guaranteesD) 2);
   1.161 -by (rtac UNIV_I 4);
   1.162 -by (force_tac (claset(),
   1.163 -	       simpset() addsimps [inv_sysOfClient]) 3);
   1.164 -by (asm_simp_tac (simpset() addsimps [guarantees_PLam_I, 
   1.165 -		      Client_Increasing_rel RS lift_prog_guar_Increasing]) 2);
   1.166 +(*Network : <unfolded specification> *)
   1.167 +val Network_Spec =
   1.168 +    rewrite_rule [network_spec_def, network_ask_def,
   1.169 +		  network_giv_def, network_rel_def] Network;
   1.170 +
   1.171 +(*CANNOT use bind_thm: it puts the theorem into standard form, in effect
   1.172 +  exporting it from the locale*)
   1.173 +val Network_Ask = Network_Spec RS IntD1 RS IntD1;
   1.174 +val Network_Giv = Network_Spec RS IntD1 RS IntD2;
   1.175 +val Network_Rel = Network_Spec RS IntD2 RS INT_D;
   1.176 +
   1.177 +
   1.178 +(*Alloc : <unfolded specification> *)
   1.179 +val Alloc_Spec =
   1.180 +    rewrite_rule [alloc_spec_def, alloc_increasing_def,
   1.181 +		  alloc_safety_def, alloc_progress_def] Alloc;
   1.182 +
   1.183 +Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocAsk)";
   1.184 +by (cut_facts_tac [Alloc_Spec] 1);
   1.185 +by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
   1.186 +qed "Alloc_Increasing";
   1.187 +
   1.188 +val Alloc_Safety = Alloc_Spec RS IntD1 RS IntD2;
   1.189 +val Alloc_Progress = (Alloc_Spec RS IntD2
   1.190 +                      |> simplify (simpset() addsimps [guarantees_INT_right]))
   1.191 +                     RS bspec RS spec;
   1.192 +		     
   1.193 +
   1.194  
   1.195 -by (rtac (Client_Increasing_rel RS drop_prog_guarantees_PLam RS guarantees_weaken) 1);
   1.196 -by (force_tac (claset() addIs [lift_prog_Join_Stable],
   1.197 -	       simpset() addsimps [Increasing_def]) 2);
   1.198 -by Auto_tac;
   1.199 +(*Not sure what to say about the other components because they involve
   1.200 +  extend*)
   1.201 +Goalw [System_def] "Network component System";
   1.202 +by (blast_tac (claset() addIs [componentI]) 1);
   1.203 +qed "Network_component_System";
   1.204 +
   1.205 +AddIffs [Network_component_System];
   1.206 +
   1.207 +
   1.208 +val project_guarantees' =
   1.209 +  [surj_sysOfClient, inj_sysOfClient] MRS export project_guarantees;
   1.210 +
   1.211 +(* F : UNIV guarantees Increasing func
   1.212 +   ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
   1.213 +val extend_guar_Increasing' =
   1.214 +  [surj_sysOfClient, inj_sysOfClient] MRS export extend_guar_Increasing
   1.215 +  |> simplify (simpset() addsimps [inv_sysOfClient_eq]);
   1.216 +
   1.217 +
   1.218 +(** Proof of property (1) **)
   1.219 +
   1.220 +(*step 1*)
   1.221 +Goalw [System_def]
   1.222 +     "i < Nclients ==> System : Increasing (rel o sub i o client)";
   1.223 +by (rtac ([guaranteesI RS disjI2 RS guarantees_Join_I, UNIV_I] 
   1.224 +	  MRS guaranteesD) 1);
   1.225 +by (asm_simp_tac 
   1.226 +    (simpset() addsimps [guarantees_PLam_I, 
   1.227 +			 extend_guar_Increasing' RS guaranteesD,
   1.228 +			 lift_prog_guar_Increasing]) 1);
   1.229  qed "System_Increasing_rel";
   1.230  
   1.231 -
   1.232 -yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy;
   1.233 -
   1.234 -
   1.235 -
   1.236 -(*partial system...*)
   1.237 -Goal "[| Alloc : alloc_spec;  Network : network_spec |] \
   1.238 -\     ==> (extend sysOfAlloc Alloc) Join Network : system_spec";
   1.239 -
   1.240 -(*partial system...*)
   1.241 -Goal "[| Client : client_spec;  Network : network_spec |] \
   1.242 -\     ==> (extend sysOfClient (plam x: lessThan Nclients. Client)) \
   1.243 -\         Join Network : system_spec";
   1.244 -
   1.245 +(*Note: the first step above performs simple quantifier reasoning.  It could
   1.246 +  be replaced by a proof mentioning no guarantees primitives*)
   1.247  
   1.248  
   1.249 -Goal "[| Alloc : alloc_spec;  Client : client_spec;  \
   1.250 -\        Network : network_spec |] \
   1.251 -\     ==> (extend sysOfAlloc Alloc) \
   1.252 -\         Join (extend sysOfClient (plam x: lessThan Nclients. Client)) \
   1.253 -\         Join Network : system_spec";
   1.254 -by (full_simp_tac
   1.255 -    (simpset() addsimps [system_spec_def, system_safety_def]) 1);
   1.256 -by Auto_tac;
   1.257 -by (full_simp_tac
   1.258 -    (simpset() addsimps [client_spec_def, client_increasing_def,
   1.259 -			 guarantees_Int_right]) 1);
   1.260 -by Auto_tac;
   1.261 -by (dtac (UNIV_I RSN (2, guaranteesD)) 1);
   1.262 -back();
   1.263 -by (full_simp_tac
   1.264 -    (simpset() addsimps [network_spec_def, network_rel_def]) 1);
   1.265 +(*step 2*)
   1.266 +Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
   1.267 +by (rtac Follows_Increasing1 1);
   1.268 +by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
   1.269 +			       System_Increasing_rel, Network]) 1);
   1.270 +qed "System_Increasing_allocRel";
   1.271  
   1.272 +Goal "i < Nclients \
   1.273 +\ ==> System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
   1.274 +\                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
   1.275 +fr component_guaranteesD;
   1.276  
   1.277 -by (full_simp_tac
   1.278 -    (simpset() addsimps [alloc_spec_def, alloc_safety_def]) 1);
   1.279 -by Auto_tac;
   1.280 +val extend_guar_Increasing'' =
   1.281 +  [surj_sysOfAlloc, inj_sysOfAlloc] MRS export extend_guar_Increasing
   1.282 +  |> simplify (simpset() addsimps [inv_sysOfAlloc_eq]);
   1.283  
   1.284 -by (Simp_tac 1);
   1.285 +by (rtac (Alloc_Safety RS component_guaranteesD) 1);