Introduction of the theories UNITY/Merge, UNITY/ClientImpl
authorpaulson
Thu May 29 17:10:00 2003 +0200 (2003-05-29)
changeset 140534daa384f4fd7
parent 14052 e9c9f69e4f63
child 14054 dc281bd5ca0a
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
src/ZF/IsaMakefile
src/ZF/UNITY/AllocBase.ML
src/ZF/UNITY/ClientImpl.ML
src/ZF/UNITY/ClientImpl.thy
src/ZF/UNITY/Distributor.ML
src/ZF/UNITY/Follows.ML
src/ZF/UNITY/Merge.ML
src/ZF/UNITY/Merge.thy
src/ZF/UNITY/ROOT.ML
src/ZF/UNITY/WFair.ML
     1.1 --- a/src/ZF/IsaMakefile	Wed May 28 18:13:41 2003 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Thu May 29 17:10:00 2003 +0200
     1.3 @@ -121,9 +121,11 @@
     1.4    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
     1.5    UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
     1.6    UNITY/AllocBase.ML UNITY/AllocBase.thy\
     1.7 +  UNITY/ClientImpl.ML UNITY/ClientImpl.thy\
     1.8    UNITY/Distributor.ML UNITY/Distributor.thy\
     1.9    UNITY/Follows.ML UNITY/Follows.thy\
    1.10    UNITY/Increasing.ML UNITY/Increasing.thy\
    1.11 +  UNITY/Merge.ML UNITY/Merge.thy\
    1.12    UNITY/Monotonicity.ML UNITY/Monotonicity.thy\
    1.13    UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
    1.14    UNITY/WFair.ML UNITY/WFair.thy
     2.1 --- a/src/ZF/UNITY/AllocBase.ML	Wed May 28 18:13:41 2003 +0200
     2.2 +++ b/src/ZF/UNITY/AllocBase.ML	Thu May 29 17:10:00 2003 +0200
     2.3 @@ -42,7 +42,7 @@
     2.4  \     (ALL i:nat. i<n --> f(i) $<= g(i)) --> \
     2.5  \     setsum(f, n) $<= setsum(g,n)";
     2.6  by (induct_tac "n" 1);
     2.7 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [])));
     2.8 +by (ALLGOALS Asm_full_simp_tac);
     2.9  by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x~:x" 1);
    2.10  by (Clarify_tac 1);
    2.11  by (Asm_simp_tac 1);
    2.12 @@ -54,8 +54,7 @@
    2.13  by (Clarify_tac 1);
    2.14  by (dtac leI 1);
    2.15  by (Asm_simp_tac 1);
    2.16 -by (asm_simp_tac (simpset() addsimps [nat_into_Finite,
    2.17 -                                      mem_not_refl, succ_def]) 1);
    2.18 +by (asm_simp_tac (simpset() addsimps [nat_into_Finite, mem_not_refl, succ_def]) 1);
    2.19  qed_spec_mp "setsum_fun_mono";
    2.20  
    2.21  Goal "l:list(A) ==> tokens(l):nat";
    2.22 @@ -218,7 +217,7 @@
    2.23  by (subgoal_tac
    2.24        "B Int C Int length(l) = \
    2.25  \      (B Int length(l)) Int (C Int length(l))" 1);
    2.26 -by (blast_tac (claset() addIs []) 2);
    2.27 +by (Blast_tac 2);
    2.28  by (asm_simp_tac (simpset() addsimps [bag_of_sublist, 
    2.29                                        Int_Un_distrib2, msetsum_Un_Int]) 1); 
    2.30  by (resolve_tac [msetsum_Un_Int] 1);
    2.31 @@ -314,7 +313,8 @@
    2.32  bind_thm("Follows_state_ofD2", Follows_state_of_eq RS equalityD2 RS subsetD);
    2.33  
    2.34  (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
    2.35 -fun list_of_Int th = 
    2.36 +fun list_of_Int th = list_of_Int_aux (Drule.freeze_all th)
    2.37 +and list_of_Int_aux th =
    2.38      (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
    2.39      handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
    2.40      handle THM _ => (list_of_Int (th RS InterD))
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/UNITY/ClientImpl.ML	Thu May 29 17:10:00 2003 +0200
     3.3 @@ -0,0 +1,309 @@
     3.4 +(*  Title:      ZF/UNITY/Client.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     3.7 +    Copyright   2002  University of Cambridge
     3.8 +
     3.9 +Distributed Resource Management System: the Client
    3.10 +*)
    3.11 +Addsimps [type_assumes, default_val_assumes];
    3.12 +(* This part should be automated *)
    3.13 +
    3.14 +Goalw [state_def] "s:state ==> s`ask:list(nat)";
    3.15 +by (dres_inst_tac [("a", "ask")] apply_type 1);
    3.16 +by Auto_tac;
    3.17 +qed "ask_value_type";
    3.18 +AddTCs [ask_value_type];
    3.19 +Addsimps [ask_value_type];
    3.20 +
    3.21 +Goalw [state_def] "s:state ==> s`giv:list(nat)";
    3.22 +by (dres_inst_tac [("a", "giv")] apply_type 1);
    3.23 +by Auto_tac;
    3.24 +qed "giv_value_type";
    3.25 +AddTCs [giv_value_type];
    3.26 +Addsimps [giv_value_type];
    3.27 +
    3.28 +Goalw [state_def]
    3.29 +"s:state ==> s`rel:list(nat)";
    3.30 +by (dres_inst_tac [("a", "rel")] apply_type 1);
    3.31 +by Auto_tac;
    3.32 +qed "rel_value_type";
    3.33 +AddTCs [rel_value_type];
    3.34 +Addsimps [rel_value_type];
    3.35 +
    3.36 +Goalw [state_def] "s:state ==> s`tok:nat";
    3.37 +by (dres_inst_tac [("a", "tok")] apply_type 1);
    3.38 +by Auto_tac;
    3.39 +qed "tok_value_type";
    3.40 +AddTCs [tok_value_type];
    3.41 +Addsimps [tok_value_type];
    3.42 +
    3.43 +(** The Client Program **)
    3.44 +
    3.45 +Goalw [client_prog_def] "client_prog:program";
    3.46 +by (Simp_tac 1);
    3.47 +qed "client_type";
    3.48 +Addsimps [client_type];
    3.49 +AddTCs [client_type];
    3.50 +
    3.51 +Addsimps [client_prog_def RS def_prg_Init, 
    3.52 +          client_prog_def RS def_prg_AllowedActs];
    3.53 +program_defs_ref := [client_prog_def];
    3.54 +
    3.55 +Addsimps (map simp_of_act [client_rel_act_def, 
    3.56 +client_tok_act_def, client_ask_act_def]);
    3.57 +
    3.58 +Goal "ALL G:program. (client_prog ok G) <-> \
    3.59 +\  (G:preserves(lift(rel)) & G:preserves(lift(ask)) & \
    3.60 +\   G:preserves(lift(tok)) &  client_prog:Allowed(G))";
    3.61 +by (auto_tac (claset(), 
    3.62 +     simpset() addsimps [ok_iff_Allowed, client_prog_def RS def_prg_Allowed]));  
    3.63 +qed "client_prog_ok_iff";
    3.64 +
    3.65 +Goal "client_prog:(INT x:var-{ask, rel, tok}. preserves(lift(x)))";
    3.66 +by (rtac Inter_var_DiffI 1);
    3.67 +by (rtac ballI 2);
    3.68 +by (rtac preservesI 2);
    3.69 +by (constrains_tac 2);
    3.70 +by Auto_tac;
    3.71 +qed "client_prog_preserves";
    3.72 +
    3.73 +
    3.74 +(*Safety property 1: ask, rel are increasing : (24) *)
    3.75 +Goalw [guar_def]
    3.76 +"client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))";
    3.77 +by (auto_tac (claset() addSIs [increasing_imp_Increasing],
    3.78 +        simpset() addsimps [client_prog_ok_iff, increasing_def]));
    3.79 +by (ALLGOALS(constrains_tac));
    3.80 +by (ALLGOALS(thin_tac "mk_program(?u, ?v, ?w):Allowed(?x)"));
    3.81 +by (auto_tac (claset() addDs [ActsD], simpset()));
    3.82 +by (dres_inst_tac [("f", "lift(rel)")] preserves_imp_eq 2);
    3.83 +by (dres_inst_tac [("f", "lift(ask)")] preserves_imp_eq 1);
    3.84 +by (TRYALL(assume_tac));
    3.85 +by (ALLGOALS(dtac ActsD));
    3.86 +by (TRYALL(assume_tac));
    3.87 +by (ALLGOALS(Clarify_tac));
    3.88 +by (ALLGOALS(rotate_tac ~2));
    3.89 +by Auto_tac;
    3.90 +qed "client_prog_Increasing_ask_rel";
    3.91 +
    3.92 +Addsimps [nth_append, append_one_prefix];
    3.93 +
    3.94 +Goal  "0<NbT";
    3.95 +by (cut_facts_tac [NbT_pos] 1);
    3.96 +by (resolve_tac [Ord_0_lt] 1);
    3.97 +by Auto_tac;
    3.98 +qed "NbT_pos2";
    3.99 +
   3.100 +(*Safety property 2: the client never requests too many tokens.
   3.101 +With no Substitution Axiom, we must prove the two invariants simultaneously. *)
   3.102 +
   3.103 +Goal 
   3.104 +"[| client_prog ok G; G:program |]\
   3.105 +\     ==> client_prog Join G :  \
   3.106 +\             Always({s:state. s`tok le NbT}  Int  \
   3.107 +\                     {s:state. ALL elt:set_of_list(s`ask). elt le NbT})";
   3.108 +by (rotate_tac ~1 1);
   3.109 +by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff]));
   3.110 +by (rtac (invariantI RS stable_Join_Always2) 1);
   3.111 +by (ALLGOALS(Clarify_tac));
   3.112 +by (ALLGOALS(Asm_full_simp_tac)); 
   3.113 +by (rtac stable_Int 2);
   3.114 +by (dres_inst_tac [("f", "lift(ask)")] preserves_imp_stable 3);
   3.115 +by (dres_inst_tac [("f", "lift(tok)")] preserves_imp_stable 2);
   3.116 +by (REPEAT(Force_tac 2));
   3.117 +by (constrains_tac 1);
   3.118 +by (auto_tac (claset() addDs [ActsD], simpset()));
   3.119 +by (cut_facts_tac [NbT_pos] 1);
   3.120 +by (resolve_tac [NbT_pos2 RS mod_less_divisor] 1);
   3.121 +by (auto_tac (claset() addDs [ActsD, preserves_imp_eq], 
   3.122 +               simpset() addsimps [set_of_list_append]));
   3.123 +qed "ask_Bounded_lemma";
   3.124 +
   3.125 +(* Export version, with no mention of tok in the postcondition, but
   3.126 +  unfortunately tok must be declared local.*)
   3.127 +Goal 
   3.128 +"client_prog: program guarantees \
   3.129 +\            Always({s:state. ALL elt: set_of_list(s`ask). elt le NbT})";
   3.130 +by (rtac guaranteesI 1);
   3.131 +by (etac (ask_Bounded_lemma RS Always_weaken) 1);
   3.132 +by Auto_tac;
   3.133 +qed "client_prog_ask_Bounded";
   3.134 +
   3.135 +(*** Towards proving the liveness property ***)
   3.136 +
   3.137 +Goal 
   3.138 +"client_prog: stable({s:state. <s`rel, s`giv>:prefix(nat)})";
   3.139 +by (constrains_tac 1);
   3.140 +by Auto_tac;
   3.141 +qed "client_prog_stable_rel_le_giv";
   3.142 +
   3.143 +Goal
   3.144 +"[| client_prog Join G: Incr(lift(giv)); G:preserves(lift(rel)) |] \
   3.145 +\   ==> client_prog Join G:  Stable({s:state. <s`rel, s`giv>:prefix(nat)})";
   3.146 +by (rtac (client_prog_stable_rel_le_giv RS Increasing_preserves_Stable) 1);
   3.147 +by (auto_tac (claset(), simpset() addsimps [lift_def]));
   3.148 +qed "client_prog_Join_Stable_rel_le_giv";
   3.149 +
   3.150 +Goal "[| client_prog Join G: Incr(lift(giv)); G:preserves(lift(rel)) |] \
   3.151 +\   ==> client_prog Join G : Always({s:state. <s`rel, s`giv>:prefix(nat)})";
   3.152 +by (force_tac (claset() addSIs [AlwaysI, client_prog_Join_Stable_rel_le_giv], 
   3.153 +            simpset()) 1);
   3.154 +qed "client_prog_Join_Always_rel_le_giv";
   3.155 +
   3.156 +Goal "xs:list(A) ==> xs@[a]=xs --> False";
   3.157 +by (etac list.induct 1);
   3.158 +by Auto_tac;
   3.159 +qed "list_app_lemma";
   3.160 +
   3.161 +Goal "A == {<s, t>:state*state. P(s, t)} ==> A={<s, t>:state*state. P(s, t)}";
   3.162 +by Auto_tac;
   3.163 +qed "def_act_eq";
   3.164 +
   3.165 +Goal "A={<s,t>:state*state. P(s, t)} ==> A<=state*state";
   3.166 +by Auto_tac;
   3.167 +qed "act_subset";
   3.168 +
   3.169 +Goal 
   3.170 +"client_prog: \
   3.171 +\ transient({s:state. s`rel = k & <k, h>:strict_prefix(nat) \
   3.172 +\  & <h, s`giv>:prefix(nat) & h pfixGe s`ask})";
   3.173 +by (res_inst_tac [("act", "client_rel_act")] transientI 1);
   3.174 +by (simp_tac (simpset() addsimps 
   3.175 +                 [client_prog_def RS def_prg_Acts]) 1);
   3.176 +by (simp_tac (simpset() addsimps 
   3.177 +             [client_rel_act_def RS def_act_eq RS act_subset]) 1);
   3.178 +by (auto_tac (claset(),
   3.179 +              simpset() addsimps [client_prog_def RS def_prg_Acts,domain_def]));
   3.180 +by (resolve_tac [ReplaceI] 1);
   3.181 +by (res_inst_tac [("x", "x(rel:= x`rel @\
   3.182 +        \            [nth(length(x`rel), x`giv)])")] exI 1);
   3.183 +by (auto_tac (claset() addSIs [state_update_type, 
   3.184 +                               app_type, length_type, nth_type], 
   3.185 +              simpset()));
   3.186 +by Auto_tac;
   3.187 +by (blast_tac (claset() addIs [lt_trans2, prefix_length_le,
   3.188 +                               strict_prefix_length_lt]) 1);
   3.189 +by (blast_tac (claset() addIs [lt_trans2, prefix_length_le,
   3.190 +                               strict_prefix_length_lt]) 1);
   3.191 +by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1);
   3.192 +by (ALLGOALS(subgoal_tac "h:list(nat)"));
   3.193 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1])));
   3.194 +by (auto_tac (claset(), 
   3.195 +              simpset() addsimps [prefix_def, Ge_def]));
   3.196 +by (dtac strict_prefix_length_lt 1);
   3.197 +by (dres_inst_tac [("x", "length(x`rel)")] bspec 1);
   3.198 +by Auto_tac;
   3.199 +by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1);
   3.200 +by (auto_tac (claset(), simpset() addsimps [id_def, lam_def]));
   3.201 +qed "transient_lemma";
   3.202 +
   3.203 +Goalw [strict_prefix_def,id_def, lam_def]
   3.204 +"<xs, ys>:strict_prefix(A) <->  <xs, ys>:prefix(A) & xs~=ys";
   3.205 +by (auto_tac (claset() addDs [prefix_type RS subsetD], simpset()));
   3.206 +qed "strict_prefix_is_prefix";
   3.207 +
   3.208 +Goal 
   3.209 +"[| client_prog Join G: Incr(lift(giv)); client_prog ok G; G:program |] \
   3.210 +\ ==> client_prog Join G: \
   3.211 +\ {s:state. s`rel = k & <k,h>:strict_prefix(nat) \
   3.212 +\  & <h , s`giv>:prefix(nat) & h pfixGe s`ask}  \
   3.213 +\       LeadsTo {s:state. <k, s`rel>:strict_prefix(nat) \
   3.214 +\                         & <s`rel, s`giv>:prefix(nat) & \
   3.215 +\                                 <h, s`giv>:prefix(nat) & \
   3.216 +\               h pfixGe s`ask}";
   3.217 +by (rtac single_LeadsTo_I 1);
   3.218 +by (Asm_simp_tac 2);
   3.219 +by (ftac (client_prog_Increasing_ask_rel RS guaranteesD) 1);
   3.220 +by (rotate_tac 2 3);
   3.221 +by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff]));
   3.222 +by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS 
   3.223 +          leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
   3.224 +by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
   3.225 +by (eres_inst_tac [("f", "lift(giv)"), ("a", "s`giv")] Increasing_imp_Stable 1);
   3.226 +by (Asm_simp_tac 1);
   3.227 +by (eres_inst_tac [("f", "lift(ask)"), ("a", "s`ask")] Increasing_imp_Stable 1);
   3.228 +by (Asm_simp_tac 1);
   3.229 +by (eres_inst_tac [("f", "lift(rel)"), ("a", "s`rel")] Increasing_imp_Stable 1);
   3.230 +by (Asm_simp_tac 1);
   3.231 +by (etac client_prog_Join_Stable_rel_le_giv 1);
   3.232 +by (Blast_tac 1);
   3.233 +by (Asm_simp_tac 1);
   3.234 +by (Asm_simp_tac 2);
   3.235 +by (blast_tac (claset() addIs [sym, strict_prefix_is_prefix RS iffD2, 
   3.236 +                               prefix_trans, prefix_imp_pfixGe, 
   3.237 +                               pfixGe_trans]) 2);
   3.238 +by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD1 RS conjunct1, 
   3.239 +                               prefix_trans], simpset()));
   3.240 +qed "induct_lemma";
   3.241 +
   3.242 +Goal 
   3.243 +"[| client_prog Join G : Incr(lift(giv)); client_prog ok G; G:program |] \
   3.244 +\ ==> client_prog Join G : \
   3.245 +\    {s:state. <s`rel, h>:strict_prefix(nat) \
   3.246 +\          & <h, s`giv>:prefix(nat) & h pfixGe s`ask}  \
   3.247 +\                     LeadsTo {s:state. <h, s`rel>:prefix(nat)}";
   3.248 +by (res_inst_tac [("f", "lam x:state. length(h) #- length(x`rel)")] 
   3.249 +                                 LessThan_induct 1);
   3.250 +by (auto_tac (claset(), simpset() addsimps [vimage_def]));
   3.251 +by (rtac single_LeadsTo_I 1);
   3.252 +by (rtac (induct_lemma RS LeadsTo_weaken) 1);
   3.253 +by Auto_tac;
   3.254 +by (resolve_tac [imageI] 3);
   3.255 +by (resolve_tac [converseI] 3);
   3.256 +by (asm_simp_tac (simpset() addsimps [lam_def]) 3);
   3.257 +by (asm_simp_tac (simpset() addsimps [length_type]) 3);
   3.258 +by (etac swap 2);
   3.259 +by (resolve_tac [imageI] 2);
   3.260 +by (resolve_tac [converseI] 2);
   3.261 +by (asm_full_simp_tac (simpset() addsimps [lam_def]) 2);
   3.262 +by (REPEAT (dtac strict_prefix_length_lt 2));
   3.263 +by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 2);
   3.264 +by (ALLGOALS(subgoal_tac "h:list(nat)"));
   3.265 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1])));
   3.266 +by (dtac less_imp_succ_add 2);
   3.267 +by (dtac less_imp_succ_add 3);
   3.268 +by (ALLGOALS(Clarify_tac));
   3.269 +by (ALLGOALS(Asm_simp_tac));
   3.270 +by (etac (diff_le_self RS ltD) 2); 
   3.271 +by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 1);
   3.272 +by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD2]
   3.273 +                        addDs [rotate_prems 2 common_prefix_linear,
   3.274 +                               prefix_type RS subsetD], simpset()));
   3.275 +qed "rel_progress_lemma";
   3.276 +
   3.277 +Goal 
   3.278 +"[| client_prog Join G: Incr(lift(giv)); client_prog ok G; G:program |] ==> \
   3.279 +\ client_prog Join G : \
   3.280 +\  {s:state. <h, s`giv>:prefix(nat) & h pfixGe s`ask}  \
   3.281 +\              LeadsTo {s:state. <h, s`rel>:prefix(nat)}";
   3.282 +by (rtac (client_prog_Join_Always_rel_le_giv RS Always_LeadsToI) 1);
   3.283 +by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS 
   3.284 +    LeadsTo_Un RS LeadsTo_weaken_L) 3);
   3.285 +by Auto_tac;
   3.286 +by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD2]
   3.287 +                        addDs [rotate_prems 3 common_prefix_linear,
   3.288 +                               prefix_type RS subsetD], simpset()));
   3.289 +by (rotate_tac ~1 1);
   3.290 +by (force_tac (claset(), simpset() addsimps [client_prog_ok_iff]) 1);
   3.291 +qed "progress_lemma";
   3.292 +
   3.293 +(*Progress property: all tokens that are given will be released*)
   3.294 +Goal 
   3.295 +"client_prog: Incr(lift(giv))  guarantees  \
   3.296 +\     (INT h:list(nat). {s:state. <h, s`giv>:prefix(nat) &\
   3.297 +\             h pfixGe s`ask} LeadsTo {s:state. <h, s`rel>:prefix(nat)})";
   3.298 +by (rtac guaranteesI 1);
   3.299 +by (Clarify_tac 1);
   3.300 +by (blast_tac (claset() addIs [progress_lemma]) 1);
   3.301 +by Auto_tac;
   3.302 +qed "client_prog_progress";
   3.303 +
   3.304 +Goal "Allowed(client_prog) = \
   3.305 +\ preserves(lift(rel)) Int preserves(lift(ask)) Int preserves(lift(tok))";
   3.306 +by (cut_facts_tac [inst "v"  "lift(ask)" preserves_type] 1);
   3.307 +by (auto_tac (claset(), 
   3.308 +              simpset() addsimps [Allowed_def, 
   3.309 +               client_prog_def RS def_prg_Allowed, 
   3.310 +                  cons_Int_distrib, safety_prop_Acts_iff]));
   3.311 +qed "client_prog_Allowed";
   3.312 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/UNITY/ClientImpl.thy	Thu May 29 17:10:00 2003 +0200
     4.3 @@ -0,0 +1,63 @@
     4.4 +(*  Title:      ZF/UNITY/ClientImpl.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     4.7 +    Copyright   2002  University of Cambridge
     4.8 +
     4.9 +Distributed Resource Management System:  Client Implementation
    4.10 +*)
    4.11 +
    4.12 +
    4.13 +ClientImpl = AllocBase + Guar +
    4.14 +consts
    4.15 +  ask :: i (* input history:  tokens requested *)
    4.16 +  giv :: i (* output history: tokens granted *)
    4.17 +  rel :: i (* input history: tokens released *)
    4.18 +  tok :: i (* the number of available tokens *)
    4.19 +
    4.20 +translations
    4.21 +  "ask" == "Var(Nil)"
    4.22 +  "giv" == "Var([0])"
    4.23 +  "rel" == "Var([1])"
    4.24 +  "tok" == "Var([2])"
    4.25 +
    4.26 +rules
    4.27 +  type_assumes
    4.28 +  "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) & 
    4.29 +   type_of(rel) = list(tokbag) & type_of(tok) = nat"
    4.30 +  default_val_assumes
    4.31 +  "default_val(ask) = Nil & default_val(giv)  = Nil & 
    4.32 +   default_val(rel)  = Nil & default_val(tok)  = 0"
    4.33 +
    4.34 +
    4.35 +(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
    4.36 +
    4.37 +constdefs
    4.38 + (** Release some client_tokens **)
    4.39 +  
    4.40 +  client_rel_act ::i
    4.41 +    "client_rel_act ==
    4.42 +     {<s,t>:state*state. EX nrel:nat. nrel = length(s`rel)
    4.43 +		    &  t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
    4.44 +                  nrel < length(s`giv) &
    4.45 +                  nth(nrel, s`ask) le nth(nrel, s`giv)}"
    4.46 +  
    4.47 +  (** Choose a new token requirement **)
    4.48 +  (** Including s'=s suppresses fairness, allowing the non-trivial part
    4.49 +      of the action to be ignored **)
    4.50 +
    4.51 +  client_tok_act :: i
    4.52 + "client_tok_act == {<s,t>:state*state. t=s |
    4.53 +		 (t = s(tok:=succ(s`tok mod NbT)))}"
    4.54 +
    4.55 +  client_ask_act :: i
    4.56 +  "client_ask_act == {<s,t>:state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
    4.57 +  
    4.58 +  client_prog :: i
    4.59 +  "client_prog ==
    4.60 +   mk_program({s:state. s`tok le NbT & s`giv = Nil &
    4.61 +	               s`ask = Nil & s`rel = Nil},
    4.62 +                    {client_rel_act, client_tok_act, client_ask_act},
    4.63 +                   UN G: preserves(lift(rel)) Int
    4.64 +			 preserves(lift(ask)) Int
    4.65 +	                 preserves(lift(tok)).  Acts(G))"
    4.66 +end
    4.67 \ No newline at end of file
     5.1 --- a/src/ZF/UNITY/Distributor.ML	Wed May 28 18:13:41 2003 +0200
     5.2 +++ b/src/ZF/UNITY/Distributor.ML	Thu May 29 17:10:00 2003 +0200
     5.3 @@ -74,7 +74,7 @@
     5.4  by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); 
     5.5  by (auto_tac (claset() addSIs [guaranteesI]  addIs [Follows_imp_Increasing_left]
     5.6                          addSDs [guaranteesD], 
     5.7 -               simpset() addsimps []));
     5.8 +               simpset()));
     5.9  qed "distr_Increasing_Out";
    5.10  
    5.11  val state_AlwaysI2 = state_AlwaysI RS Always_weaken;
    5.12 @@ -116,13 +116,6 @@
    5.13  by (blast_tac (claset() addIs [lt_trans]) 1);
    5.14  qed "distr_bag_Follows_lemma";
    5.15  
    5.16 -
    5.17 -val prems =
    5.18 -Goal "[|A=A'; r=r'; !!x. x:state ==> f(x)=f'(x); !!x. x:state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')";
    5.19 -by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
    5.20 -qed "Follows_cong";
    5.21 -(*????????????????*)
    5.22 -
    5.23  Goal
    5.24   "D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
    5.25  \      (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int  \
    5.26 @@ -150,8 +143,8 @@
    5.27  by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 5);
    5.28  by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 6);
    5.29  by (Clarify_tac 4);
    5.30 -by (asm_full_simp_tac (simpset() addsimps []) 3);
    5.31 -by (asm_full_simp_tac (simpset() addsimps []) 3);
    5.32 +by (Asm_full_simp_tac 3);
    5.33 +by (Asm_full_simp_tac 3);
    5.34  by (ALLGOALS(asm_simp_tac (simpset() addsimps [nat_into_Finite])));
    5.35  by (rotate_tac 2 1);
    5.36  by (asm_full_simp_tac (simpset() addsimps [D_ok_iff]) 1);
    5.37 @@ -159,8 +152,8 @@
    5.38                simpset() addsimps [distr_spec_def, distr_follows_def]));
    5.39  by (dtac guaranteesD 1); 
    5.40  by (assume_tac 1);
    5.41 -by (force_tac (claset(), simpset() addsimps []) 1); 
    5.42 -by (force_tac (claset(), simpset() addsimps []) 1); 
    5.43 +by (Force_tac 1); 
    5.44 +by (Force_tac 1); 
    5.45  by (asm_full_simp_tac
    5.46      (simpset() addsimps [rewrite_rule [comp_def] (mono_bag_of RS subset_Follows_comp RS subsetD), 
    5.47               refl_prefix, trans_on_MultLe] 
     6.1 --- a/src/ZF/UNITY/Follows.ML	Wed May 28 18:13:41 2003 +0200
     6.2 +++ b/src/ZF/UNITY/Follows.ML	Thu May 29 17:10:00 2003 +0200
     6.3 @@ -8,6 +8,10 @@
     6.4   
     6.5  (*Does this hold for "invariant"?*)
     6.6  
     6.7 +val prems =
     6.8 +Goal "[|A=A'; r=r'; !!x. x:state ==> f(x)=f'(x); !!x. x:state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')";
     6.9 +by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
    6.10 +qed "Follows_cong";
    6.11  
    6.12  Goalw [mono1_def, comp_def] 
    6.13  "[| mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/ZF/UNITY/Merge.ML	Thu May 29 17:10:00 2003 +0200
     7.3 @@ -0,0 +1,163 @@
     7.4 +(*  Title: ZF/UNITY/Merge
     7.5 +    ID:         $Id$
     7.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     7.7 +    Copyright   2002  University of Cambridge
     7.8 +
     7.9 +A multiple-client allocator from a single-client allocator:
    7.10 +Merge specification
    7.11 +*)
    7.12 +Open_locale "Merge";
    7.13 +val all_distinct_vars = thm "all_distinct_vars";
    7.14 +val var_assumes = thm "var_assumes";
    7.15 +val type_assumes = thm "type_assumes";
    7.16 +val default_val_assumes  = thm "default_val_assumes";
    7.17 +
    7.18 +Addsimps [var_assumes, default_val_assumes,  type_assumes];
    7.19 +
    7.20 +Goalw [state_def]
    7.21 +"s:state ==> s`In(n):list(A)";
    7.22 +by (dres_inst_tac [("a", "In(n)")] apply_type 1);
    7.23 +by Auto_tac;
    7.24 +qed "In_value_type";
    7.25 +AddTCs [In_value_type];
    7.26 +Addsimps [In_value_type];
    7.27 +
    7.28 +Goalw [state_def]
    7.29 +"s:state ==> s`Out:list(A)";
    7.30 +by (dres_inst_tac [("a", "Out")] apply_type 1);
    7.31 +by Auto_tac;
    7.32 +qed "Out_value_type";
    7.33 +AddTCs [Out_value_type];
    7.34 +Addsimps [Out_value_type];
    7.35 +
    7.36 +Goalw [state_def]
    7.37 +"s:state ==> s`iOut:list(nat)";
    7.38 +by (dres_inst_tac [("a", "iOut")] apply_type 1);
    7.39 +by Auto_tac;
    7.40 +qed "Out_value_type";
    7.41 +AddTCs [Out_value_type];
    7.42 +Addsimps [Out_value_type];
    7.43 +
    7.44 +
    7.45 +val merge = thm "merge_spec";
    7.46 +
    7.47 +Goal "M:program";
    7.48 +by (cut_facts_tac [merge] 1);
    7.49 +by (auto_tac (claset() addDs [guarantees_type RS subsetD], 
    7.50 +              simpset() addsimps [merge_spec_def, merge_increasing_def]));
    7.51 +qed "M_in_program";
    7.52 +Addsimps [M_in_program];
    7.53 +AddTCs [M_in_program];
    7.54 +
    7.55 +Goal 
    7.56 +"Allowed(M) = (preserves(lift(Out)) Int preserves(lift(iOut)))";
    7.57 +by (cut_facts_tac [merge, inst "v"  "lift(Out)" preserves_type] 1);
    7.58 +by (auto_tac (claset(), simpset() addsimps 
    7.59 +         [merge_spec_def, merge_allowed_acts_def, 
    7.60 +          Allowed_def,  safety_prop_Acts_iff]));
    7.61 +qed "merge_Allowed";
    7.62 +
    7.63 +Goal 
    7.64 +"G:program ==> \
    7.65 +\ M ok G <-> (G:preserves(lift(Out)) &  \
    7.66 +\      G:preserves(lift(iOut)) & M:Allowed(G))";
    7.67 +by (cut_facts_tac [merge] 1); 
    7.68 +by (auto_tac (claset(), simpset() 
    7.69 +         addsimps [merge_Allowed, ok_iff_Allowed]));  
    7.70 +qed "M_ok_iff";
    7.71 +
    7.72 +Goal
    7.73 +"[| G:preserves(lift(Out)); G:preserves(lift(iOut)); \
    7.74 +\  M:Allowed(G) |] ==> \
    7.75 +\ M Join G:Always({s:state. length(s`Out)=length(s`iOut)})";
    7.76 +by (ftac (preserves_type RS subsetD) 1);
    7.77 +by (subgoal_tac "G:program" 1);
    7.78 +by (assume_tac 2);
    7.79 +by (ftac M_ok_iff 1);
    7.80 +by (cut_facts_tac [merge] 1);
    7.81 +by (force_tac (claset() addDs [guaranteesD], 
    7.82 +               simpset() addsimps [merge_spec_def, merge_eq_Out_def]) 1); 
    7.83 +qed "merge_Always_Out_eq_iOut";
    7.84 +
    7.85 +Goal 
    7.86 +"[| G:preserves(lift(iOut)); G:preserves(lift(Out)); \
    7.87 +\   M:Allowed(G) |] ==> \
    7.88 +\ M Join G: Always({s:state. ALL elt:set_of_list(s`iOut). elt<Nclients})";
    7.89 +by (ftac (preserves_type RS subsetD) 1);
    7.90 +by (ftac M_ok_iff 1);
    7.91 +by (cut_facts_tac [merge] 1);
    7.92 +by (force_tac (claset() addDs [guaranteesD], 
    7.93 +               simpset() addsimps [merge_spec_def, merge_bounded_def]) 1); 
    7.94 +qed "merge_Bounded";
    7.95 +
    7.96 +Goal 
    7.97 +"[| G:preserves(lift(iOut)); \
    7.98 +\   G: preserves(lift(Out)); M:Allowed(G) |] \
    7.99 +\ ==> M Join G : Always \
   7.100 +\   ({s:state. msetsum(%i. bag_of(sublist(s`Out, \
   7.101 +\     {k:nat. k < length(s`iOut) & nth(k, s`iOut)=i})), \
   7.102 +\                  Nclients, A) = bag_of(s`Out)})";
   7.103 +by (rtac ([[merge_Always_Out_eq_iOut, merge_Bounded] MRS Always_Int_I,
   7.104 +           state_AlwaysI RS Always_weaken] MRS (Always_Diff_Un_eq RS iffD1)) 1)
   7.105 +;
   7.106 +by Auto_tac; 
   7.107 +by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
   7.108 +by (auto_tac (claset(), simpset() 
   7.109 +              addsimps [nat_into_Finite, set_of_list_conv_nth])); 
   7.110 +by (subgoal_tac
   7.111 +    "(UN i:Nclients. {k:nat. k < length(x`iOut) & nth(k, x`iOut) = i}) = length(x`iOut)" 1);
   7.112 +by Auto_tac;
   7.113 +by (resolve_tac [equalityI] 1);
   7.114 +by (blast_tac (claset() addDs [ltD]) 1); 
   7.115 +by (Clarify_tac 1); 
   7.116 +by (subgoal_tac "length(x ` iOut) : nat" 1);
   7.117 +by Typecheck_tac; 
   7.118 +by (subgoal_tac "xa : nat" 1); 
   7.119 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt]))); 
   7.120 +by (blast_tac (claset() addIs [lt_trans]) 2);
   7.121 +by (dres_inst_tac [("x", "nth(xa, x`iOut)"),("P","%elt. ?X(elt) --> elt<Nclients")] bspec 1);
   7.122 +by (asm_full_simp_tac (simpset() addsimps [ltI, nat_into_Ord]) 1); 
   7.123 +by (blast_tac (claset() addDs [ltD]) 1); 
   7.124 +qed "merge_bag_Follows_lemma";
   7.125 +
   7.126 +Goal
   7.127 +"M : (INT n:Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A)) \
   7.128 +\       guarantees  \
   7.129 +\ (%s. bag_of(s`Out)) Fols \
   7.130 +\ (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)";
   7.131 +by (cut_facts_tac [merge] 1);
   7.132 +by (rtac (merge_bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
   7.133 +by (ALLGOALS(rotate_tac ~1 ));
   7.134 +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [M_ok_iff])));
   7.135 +by Auto_tac;
   7.136 +by (rtac Follows_state_ofD1 1);
   7.137 +by (rtac Follows_msetsum_UN 1);
   7.138 +by (ALLGOALS(Clarify_tac));
   7.139 +by (resolve_tac [conjI] 2);
   7.140 +by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 2);
   7.141 +by (resolve_tac [conjI] 3);
   7.142 +by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 3);
   7.143 +by (resolve_tac [conjI] 4);
   7.144 +by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 4);
   7.145 +by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 5);
   7.146 +by (ALLGOALS(Asm_simp_tac));
   7.147 +by (resolve_tac [nat_into_Finite] 2);
   7.148 +by (Asm_simp_tac 2);
   7.149 +by (asm_full_simp_tac (simpset() addsimps [INT_iff,
   7.150 +                      merge_spec_def, merge_follows_def]) 1);
   7.151 +by Auto_tac;
   7.152 +by (cut_facts_tac [merge] 1);
   7.153 +by (subgoal_tac "M ok G" 1);
   7.154 +by (dtac guaranteesD 1); 
   7.155 +by (assume_tac 1);
   7.156 +by (force_tac (claset() addIs[M_ok_iff RS iffD2], simpset()) 4);
   7.157 +by (rewrite_goal_tac [merge_spec_def, merge_follows_def] 1);
   7.158 +by (Blast_tac 1);
   7.159 +by (Asm_simp_tac 1);
   7.160 +by (asm_full_simp_tac
   7.161 +    (simpset() addsimps [rewrite_rule [comp_def] (mono_bag_of RS subset_Follows_comp RS subsetD), 
   7.162 +             refl_prefix, trans_on_MultLe] 
   7.163 +            addcongs [Follows_cong]) 1); 
   7.164 +qed "merge_bag_Follows";
   7.165 +Close_locale "Merge";
   7.166 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/ZF/UNITY/Merge.thy	Thu May 29 17:10:00 2003 +0200
     8.3 @@ -0,0 +1,78 @@
     8.4 +(*  Title: ZF/UNITY/Merge
     8.5 +    ID:         $Id$
     8.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     8.7 +    Copyright   2002  University of Cambridge
     8.8 +
     8.9 +A multiple-client allocator from a single-client allocator:
    8.10 +Merge specification
    8.11 +*)
    8.12 +
    8.13 +Merge = AllocBase + Follows +  Guar + GenPrefix +
    8.14 +(** Merge specification (the number of inputs is Nclients) ***)
    8.15 +(** Parameter A represents the type of items to Merge **)
    8.16 +constdefs
    8.17 +  (*spec (10)*)
    8.18 +  merge_increasing :: [i, i, i] =>i
    8.19 +    "merge_increasing(A, Out, iOut) == program guarantees
    8.20 +         (lift(Out) IncreasingWrt  prefix(A)/list(A)) Int
    8.21 +         (lift(iOut) IncreasingWrt prefix(nat)/list(nat))"
    8.22 +
    8.23 +  (*spec (11)*)
    8.24 +  merge_eq_Out :: [i, i] =>i
    8.25 +  "merge_eq_Out(Out, iOut) == program guarantees
    8.26 +         Always({s:state. length(s`Out) = length(s`iOut)})"
    8.27 +
    8.28 +  (*spec (12)*)
    8.29 +  merge_bounded :: i=>i
    8.30 +  "merge_bounded(iOut) == program guarantees
    8.31 +         Always({s:state. ALL elt:set_of_list(s`iOut). elt<Nclients})"
    8.32 +  
    8.33 +  (*spec (13)*)
    8.34 +  (* Parameter A represents the type of tokens *)
    8.35 +  merge_follows :: [i, i=>i, i, i] =>i
    8.36 +    "merge_follows(A, In, Out, iOut) ==
    8.37 +     (INT n:Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
    8.38 +		   guarantees
    8.39 +     (INT n:Nclients. 
    8.40 +        (%s. sublist(s`Out, {k:nat. k < length(s`iOut) &
    8.41 +                      nth(k, s`iOut) = n})) Fols lift(In(n))
    8.42 +         Wrt prefix(A)/list(A))"
    8.43 +
    8.44 +  (*spec: preserves part*)
    8.45 +  merge_preserves :: [i=>i] =>i
    8.46 +    "merge_preserves(In) == INT n:nat. preserves(lift(In(n)))"
    8.47 +
    8.48 +(* environmental constraints*)
    8.49 +  merge_allowed_acts :: [i, i] =>i
    8.50 +  "merge_allowed_acts(Out, iOut) ==
    8.51 +         {F:program. AllowedActs(F) =
    8.52 +            cons(id(state), (UN G:preserves(lift(Out)) Int
    8.53 +                                  preserves(lift(iOut)). Acts(G)))}"
    8.54 +  
    8.55 +  merge_spec :: [i, i =>i, i, i]=>i
    8.56 +  "merge_spec(A, In, Out, iOut) ==
    8.57 +   merge_increasing(A, Out, iOut) Int merge_eq_Out(Out, iOut) Int
    8.58 +   merge_bounded(iOut) Int  merge_follows(A, In, Out, iOut)
    8.59 +   Int merge_allowed_acts(Out, iOut) Int merge_preserves(In)"
    8.60 +
    8.61 +(** State definitions.  OUTPUT variables are locals **)
    8.62 +locale Merge =
    8.63 +  fixes In :: i=>i (*merge's INPUT histories: streams to merge*)
    8.64 +        Out :: i   (*merge's OUTPUT history: merged items*)
    8.65 +        iOut :: i  (*merge's OUTPUT history: origins of merged items*)
    8.66 +        A  :: i    (*the type of items being merged *)
    8.67 +        M :: i
    8.68 + assumes
    8.69 +    var_assumes       "(ALL n. In(n):var) & Out:var & iOut:var"
    8.70 +    all_distinct_vars "ALL n. all_distinct([In(n), Out, iOut])"
    8.71 +    type_assumes      "(ALL n. type_of(In(n))=list(A))&
    8.72 +		       type_of(Out)=list(A) &
    8.73 +                       type_of(iOut)=list(nat)"
    8.74 +   default_val_assumes "(ALL n. default_val(In(n))=Nil) &
    8.75 +                        default_val(Out)=Nil &
    8.76 +                        default_val(iOut)=Nil"
    8.77 +
    8.78 +   merge_spec  "M:merge_spec(A, In, Out, iOut)"
    8.79 +end
    8.80 +
    8.81 +  
    8.82 \ No newline at end of file
     9.1 --- a/src/ZF/UNITY/ROOT.ML	Wed May 28 18:13:41 2003 +0200
     9.2 +++ b/src/ZF/UNITY/ROOT.ML	Thu May 29 17:10:00 2003 +0200
     9.3 @@ -18,4 +18,5 @@
     9.4  time_use_thy "GenPrefix";
     9.5  
     9.6  time_use_thy "Distributor";
     9.7 -
     9.8 +time_use_thy "Merge";
     9.9 +time_use_thy "ClientImpl";
    10.1 --- a/src/ZF/UNITY/WFair.ML	Wed May 28 18:13:41 2003 +0200
    10.2 +++ b/src/ZF/UNITY/WFair.ML	Thu May 29 17:10:00 2003 +0200
    10.3 @@ -544,7 +544,7 @@
    10.4  by (auto_tac (claset(), simpset() addsimps [measure_def]));
    10.5  by (blast_tac (claset() addIs [ltD]) 1); 
    10.6  by (rtac vimageI 1); 
    10.7 -by (blast_tac (claset() addIs []) 2); 
    10.8 +by (Blast_tac 2); 
    10.9  by (asm_full_simp_tac (simpset() addsimps [lt_Ord, lt_Ord2, Ord_mem_iff_lt]) 1); 
   10.10  by (blast_tac (claset() addIs [lt_trans]) 1); 
   10.11  qed "Image_inverse_lessThan";