1.1 --- a/src/HOL/UNITY/AllocImpl.ML Thu Jun 22 11:35:28 2000 +0200
1.2 +++ b/src/HOL/UNITY/AllocImpl.ML Thu Jun 22 11:36:08 2000 +0200
1.3 @@ -14,30 +14,37 @@
1.4 Addsimps [Always_INT_distrib];
1.5 Delsimps [o_apply];
1.6
1.7 -(*Eliminate the "o" operator*)
1.8 -val o_simp = simplify (simpset() addsimps [o_def]);
1.9 -
1.10 Goalw [merge_spec_def,merge_eqOut_def]
1.11 "[| M: merge_spec; G: preserves merge.Out; G: preserves merge.iOut |] \
1.12 \ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
1.13 by (force_tac (claset() addDs [guaranteesD], simpset()) 1);
1.14 qed "Merge_Always_Out_eq_iOut";
1.15
1.16 -(*******ALLOCBASE.ML***)
1.17 -Goal "[| finite A; finite B; A Int B = {} |] \
1.18 -\ ==> bag_of (sublist l (A Un B)) = \
1.19 -\ bag_of (sublist l A) + bag_of (sublist l B)";
1.20 -by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1);
1.21 -qed "bag_of_sublist_Un_disjoint";
1.22 +Goalw [merge_spec_def,merge_bounded_def]
1.23 + "[| M: merge_spec; G: preserves merge.iOut |] \
1.24 +\ ==> M Join G : Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";
1.25 +by (force_tac (claset() addDs [guaranteesD], simpset()) 1);
1.26 +qed "Merge_Bounded";
1.27
1.28 -Goal "[| finite I; ALL i:I. finite (A i); \
1.29 -\ ALL i:I. ALL j:I. A i Int A j = {} |] \
1.30 -\ ==> bag_of (sublist l (UNION I A)) = \
1.31 -\ setsum (%i. bag_of (sublist l (A i))) I";
1.32 -by (asm_simp_tac (simpset() addcongs [setsum_cong]
1.33 - addsimps [bag_of_sublist, setsum_UN_disjoint]) 1);
1.34 -qed_spec_mp "bag_of_sublist_UN_disjoint";
1.35 -
1.36 +Goal "[| M : merge_spec; G : preserves (funPair merge.Out iOut) |] \
1.37 +\ ==> M Join G : Always \
1.38 +\ {s. setsum (%i. bag_of (sublist (merge.Out s) \
1.39 +\ {k. k < length (iOut s) & iOut s ! k = i})) \
1.40 +\ (lessThan Nclients) = \
1.41 +\ (bag_of o merge.Out) s}";
1.42 +by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I,
1.43 + UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
1.44 + by Auto_tac;
1.45 +by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
1.46 + by (Simp_tac 1);
1.47 + by (Blast_tac 1);
1.48 +by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1);
1.49 +by (subgoal_tac
1.50 + "(UN i:lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) = \
1.51 +\ lessThan (length (iOut x))" 1);
1.52 + by (Blast_tac 2);
1.53 +by (asm_simp_tac (simpset() addsimps [o_def]) 1);
1.54 +qed "Merge_Bag_Follows_lemma";
1.55
1.56 Goal "M : merge_spec \
1.57 \ ==> M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
1.58 @@ -45,97 +52,92 @@
1.59 \ (bag_of o merge.Out) Fols \
1.60 \ (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
1.61 \ (lessThan Nclients))";
1.62 -by (rtac guaranteesI 1);
1.63 -by (res_inst_tac
1.64 - [("f", "%s. setsum (%i. bag_of (sublist (merge.Out s)
1.65 - {k. k < size(merge.iOut s) &
1.66 - nth(merge.iOut s)k = i}))
1.67 - (lessThan Nclients)")]
1.68 - Always_Follows 1);
1.69 -by (rtac UNIV_AlwaysI 1);
1.70 -by (Clarify_tac 1);
1.71 -by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
1.72 -by (force_tac (claset(), simpset() addsimps []) 1);
1.73 -by (blast_tac (claset() addIs [bounded_nat_set_is_finite]) 1);
1.74 -by (Clarify_tac 1);
1.75 +by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
1.76 +by Auto_tac;
1.77 +by (rtac Follows_setsum 1);
1.78 +by (auto_tac (claset(),
1.79 + simpset() addsimps [merge_spec_def,merge_follows_def, o_def]));
1.80 +by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]
1.81 + addDs [guaranteesD]) 1);
1.82 +qed "Merge_Bag_Follows";
1.83
1.84 -by (simp_tac (simpset() addsimps [o_def]) 1);
1.85 -by (asm_full_simp_tac (simpset() delsimps [sublist_upt_eq_take]
1.86 - addsimps [bag_of_sublist]) 1);
1.87 -by (rtac Follows_trans 1);
1.88 -by (rtac Follows_setsum 2);
1.89 -by (asm_full_simp_tac (simpset() addsimps []) 3);
1.90 -by (Clarify_tac 2);
1.91 -by (asm_full_simp_tac (simpset() addsimps [o_assoc RS sym]) 2);
1.92 -by (rtac (impOfSubs (mono_bag_of RS mono_Follows_o)) 2);
1.93 -
1.94 -(*Now need to invoke the merge_follows guarantee*)
1.95 -
1.96 -by (asm_full_simp_tac (simpset() addsimps [merge_spec_def,merge_follows_def]) 2);
1.97 -
1.98 -
1.99 -by (res_inst_tac [("f", "%s. bag_of (sublist (merge.Out s) {..length(merge.iOut s)(})")]
1.100 - Always_Follows 1);
1.101 -
1.102 -
1.103 -
1.104 -
1.105 -
1.106 +(*Declare a locale for M : merge_spec and
1.107 + G : preserves (funPair merge.Out iOut)? *)
1.108
1.109
1.110
1.111 -by (rtac guaranteesI 1);
1.112 -by (res_inst_tac
1.113 - [("f", "%s. bag_of (sublist (merge.Out s) {..length(merge.iOut s)(})")]
1.114 - Always_Follows 1);
1.115 -by (etac (Merge_Always_Out_eq_iOut RS Always_Compl_Un_eq RS iffD1) 1);
1.116 -by (force_tac (claset() addIs [UNIV_AlwaysI], simpset() addsimps [o_apply]) 3);
1.117 -by (Asm_full_simp_tac 1);
1.118 -by (Asm_full_simp_tac 1);
1.119 -by (asm_full_simp_tac (simpset() delsimps [sublist_upt_eq_take]
1.120 - addsimps [bag_of_sublist]) 1);
1.121 -by (rtac Follows_trans 1);
1.122 -by (rtac Follows_setsum 2);
1.123 -by (asm_full_simp_tac (simpset() addsimps []) 3);
1.124 -by (Clarify_tac 2);
1.125 -by (asm_full_simp_tac (simpset() addsimps [o_assoc RS sym]) 2);
1.126 -by (rtac (impOfSubs (mono_bag_of RS mono_Follows_o)) 2);
1.127 +(** Distributor **)
1.128 +
1.129 +Goalw [distr_follows_def]
1.130 + "D : distr_follows \
1.131 +\ ==> D : Increasing distr.In Int Increasing distr.iIn Int \
1.132 +\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
1.133 +\ guarantees[distr.Out] \
1.134 +\ (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
1.135 +by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1]
1.136 + addDs [guaranteesD]) 1);
1.137 +qed "Distr_Increasing_Out";
1.138 +
1.139
1.140 -(*Now need to invoke the merge_follows guarantee*)
1.141 -
1.142 -by (asm_full_simp_tac (simpset() addsimps [merge_spec_def,merge_follows_def]) 2);
1.143 +Goal "[| G : preserves distr.Out; \
1.144 +\ D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
1.145 +\ ==> D Join G : Always \
1.146 +\ {s. setsum (%i. bag_of (sublist (distr.In s) \
1.147 +\ {k. k < length (iIn s) & iIn s ! k = i})) \
1.148 +\ (lessThan Nclients) = \
1.149 +\ bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}";
1.150 +by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
1.151 +by Auto_tac;
1.152 +by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
1.153 + by (Simp_tac 1);
1.154 + by (Blast_tac 1);
1.155 +by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1);
1.156 +by (subgoal_tac
1.157 + "(UN i:lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = \
1.158 +\ lessThan (length (iIn x))" 1);
1.159 + by (Blast_tac 2);
1.160 +by (Asm_simp_tac 1);
1.161 +qed "Distr_Bag_Follows_lemma";
1.162
1.163
1.164 -by (res_inst_tac [("f", "%s. bag_of (sublist (merge.Out s) {..length(merge.iOut s)(})")]
1.165 - Always_Follows 1);
1.166 -
1.167 -setsum (%i. if i < length l then {# nth l i #} else {#}) {..length (iOut s)(}
1.168 -
1.169 - : (%s. bag_of
1.170 - (sublist (merge.Out s) {..length (iOut s)(})) Fols
1.171 - (%s. setsum (%i. (bag_of o sub i o merge.In) s)
1.172 - {..Nclients(})
1.173 -
1.174 -
1.175 - (%s. sublist (merge.Out s)
1.176 - {k. k < size(merge.iOut s) & nth(merge.iOut s)k = i})
1.177 - Fols (sub i o merge.In))"
1.178 -
1.179 -
1.180 +Goal "D : distr_follows \
1.181 +\ ==> D : Increasing distr.In Int Increasing distr.iIn Int \
1.182 +\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
1.183 +\ guarantees[distr.Out] \
1.184 +\ (INT i : lessThan Nclients. \
1.185 +\ (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \
1.186 +\ Fols \
1.187 +\ (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
1.188 +by (rtac guaranteesI 1);
1.189 +by (Clarify_tac 1);
1.190 +by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1);
1.191 by Auto_tac;
1.192 -by (dtac guaranteesD 1);
1.193 -by Auto_tac;
1.194 -by (rtac guaranteesI 1);
1.195 -
1.196 -merge_eqOut
1.197 -
1.198 -Always_Int_eq
1.199 +by (rtac Follows_setsum 1);
1.200 +by (auto_tac (claset(),
1.201 + simpset() addsimps [distr_follows_def, o_def]));
1.202 +by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]
1.203 + addDs [guaranteesD]) 1);
1.204 +qed "Distr_Bag_Follows";
1.205
1.206 -
1.207 -by (simp_tac (simpset() addsimps [o_def]) 1);
1.208 -by (subgoal_tac
1.209 - "ALL s. merge.Out s = sublist (merge.Out s) {..length(merge.iOut s)(}" 1);
1.210 -by (etac ssubst 1);
1.211 -by (asm_simp_tac (simpset() addsimps [bag_of_sublist]) 1);
1.212 -by (stac bag_of_sublist 1);
1.213 -
1.214 +(*
1.215 +(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
1.216 + Increasing (sub i o allocRel))
1.217 + Int
1.218 + Always {s. ALL i. i<Nclients -->
1.219 + (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}
1.220 + Int
1.221 + (INT i : lessThan Nclients.
1.222 + INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
1.223 + LeadsTo
1.224 + {s. tokens h <= (tokens o sub i o allocRel)s})
1.225 +<=
1.226 +(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
1.227 + Increasing (sub i o allocRel))
1.228 + Int
1.229 + Always {s. ALL i. i<Nclients -->
1.230 + (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}
1.231 + Int
1.232 + (INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
1.233 + LeadsTo
1.234 + {s. tokens h <= (tokens o sub i o allocRel)s})
1.235 +*)