Converting ZF/UNITY to Isar
authorpaulson
Tue Jun 24 16:32:59 2003 +0200 (2003-06-24)
changeset 14071373806545656
parent 14070 86c56794b641
child 14072 f932be305381
Converting ZF/UNITY to Isar
src/ZF/Induct/FoldSet.ML
src/ZF/Induct/FoldSet.thy
src/ZF/Induct/Multiset.ML
src/ZF/IsaMakefile
src/ZF/UNITY/AllocImpl.thy
src/ZF/UNITY/MultisetSum.ML
src/ZF/UNITY/UNITYMisc.ML
src/ZF/equalities.thy
     1.1 --- a/src/ZF/Induct/FoldSet.ML	Tue Jun 24 10:42:34 2003 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,464 +0,0 @@
     1.4 -(*  Title:      ZF/Induct/FoldSet.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     1.7 -    Copyright   2001  University of Cambridge
     1.8 -
     1.9 -
    1.10 -A "fold" functional for finite sets.  For n non-negative we have
    1.11 -fold f e {x1,...,xn} = f x1 (... (f xn e)) where f is at
    1.12 -least left-commutative.  
    1.13 -*)
    1.14 -
    1.15 -(** foldSet **)
    1.16 -
    1.17 -bind_thm("empty_fold_setE", 
    1.18 -             fold_set.mk_cases "<0, x> : fold_set(A, B, f,e)");
    1.19 -bind_thm("cons_fold_setE", 
    1.20 -             fold_set.mk_cases "<cons(x,C), y> : fold_set(A, B, f,e)");
    1.21 -
    1.22 -(* add-hoc lemmas *)
    1.23 -
    1.24 -Goal "[| x~:C; x~:B |] ==> cons(x,B)=cons(x,C) <-> B = C";
    1.25 -by (auto_tac (claset() addEs [equalityE], simpset()));
    1.26 -qed "cons_lemma1";
    1.27 -
    1.28 -Goal "[| cons(x, B)=cons(y, C); x~=y; x~:B; y~:C |] \
    1.29 -\   ==>  B - {y} = C-{x} & x:C & y:B";
    1.30 -by (auto_tac (claset() addEs [equalityE], simpset()));
    1.31 -qed "cons_lemma2";
    1.32 -
    1.33 -(* fold_set monotonicity *)
    1.34 -Goal "<C, x> : fold_set(A, B, f, e) \
    1.35 -\     ==> ALL D. A<=D --> <C, x> : fold_set(D, B, f, e)";
    1.36 -by (etac fold_set.induct 1);
    1.37 -by (auto_tac (claset() addIs fold_set.intrs, simpset()));
    1.38 -qed "fold_set_mono_lemma";
    1.39 -
    1.40 -Goal " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)";
    1.41 -by (Clarify_tac 1);
    1.42 -by (forward_tac [impOfSubs fold_set.dom_subset] 1);
    1.43 -by (Clarify_tac 1);
    1.44 -by (auto_tac (claset() addDs [fold_set_mono_lemma], simpset()));
    1.45 -qed "fold_set_mono";
    1.46 -
    1.47 -Goal "<C, x>:fold_set(A, B, f, e) ==> <C, x>:fold_set(C, B, f, e) & C<=A";
    1.48 -by (etac fold_set.induct 1);
    1.49 -by (auto_tac (claset() addSIs fold_set.intrs
    1.50 -                       addIs [fold_set_mono RS subsetD], simpset()));
    1.51 -qed "fold_set_lemma";
    1.52 -
    1.53 -(* Proving that fold_set is deterministic *)
    1.54 -Goal "[| <C-{x},y> : fold_set(A, B, f,e);  x:C; x:A; f(x, y):B |] \
    1.55 -\     ==> <C, f(x, y)> : fold_set(A, B, f, e)";
    1.56 -by (ftac (fold_set.dom_subset RS subsetD) 1);
    1.57 -by (etac (cons_Diff RS subst) 1 THEN resolve_tac fold_set.intrs 1);
    1.58 -by Auto_tac;
    1.59 -qed "Diff1_fold_set";
    1.60 -
    1.61 -Goal "[| C:Fin(A); e:B; ALL x:A. ALL y:B. f(x, y):B |] ==>\
    1.62 -\  (EX x. <C, x> : fold_set(A, B, f,e))";
    1.63 -by (etac Fin_induct 1);
    1.64 -by Auto_tac;
    1.65 -by (ftac (fold_set.dom_subset RS subsetD) 2);
    1.66 -by (auto_tac (claset() addDs [fold_set.dom_subset RS subsetD]
    1.67 -                       addIs fold_set.intrs, simpset()));
    1.68 -qed_spec_mp "Fin_imp_fold_set";
    1.69 -
    1.70 -Goal 
    1.71 -"[| n:nat; e:B; \
    1.72 -\ ALL x:A. ALL y:B. f(x, y):B; \
    1.73 -\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
    1.74 -\ ==> ALL C. |C|<n --> \
    1.75 -\  (ALL x. <C, x> : fold_set(A, B, f,e)-->\
    1.76 -\          (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x))";
    1.77 -by (etac nat_induct 1);
    1.78 -by (auto_tac (claset(), simpset() addsimps [le_iff]));
    1.79 -by (Blast_tac 1);
    1.80 -by (etac fold_set.elim 1);
    1.81 -by (force_tac (claset() addSEs [empty_fold_setE], simpset()) 1);
    1.82 -by (etac fold_set.elim 1);
    1.83 -by (force_tac (claset() addSEs [empty_fold_setE], simpset()) 1);
    1.84 -by (Clarify_tac 1);
    1.85 -(*force simplification of "|C| < |cons(...)|"*)
    1.86 -by (rotate_tac 4 1);
    1.87 -by (etac rev_mp 1);
    1.88 -by (forw_inst_tac [("a", "Ca")] 
    1.89 -     (fold_set.dom_subset RS subsetD RS SigmaD1) 1);
    1.90 -by (forw_inst_tac [("a", "Cb")] 
    1.91 -     (fold_set.dom_subset RS subsetD RS SigmaD1) 1);
    1.92 -by (asm_simp_tac (simpset() addsimps 
    1.93 -    [Fin_into_Finite RS Finite_imp_cardinal_cons])  1);
    1.94 -by (rtac impI 1);
    1.95 -(** LEVEL 14 **)
    1.96 -by (case_tac "x=xb" 1 THEN Auto_tac); (*SLOW*)
    1.97 -by (asm_full_simp_tac (simpset() addsimps [cons_lemma1]) 1);
    1.98 -by (REPEAT(thin_tac "ALL x:A. ?u(x)" 1) THEN Blast_tac 1);
    1.99 -(*case x ~= xb*)
   1.100 -by (dtac cons_lemma2 1 THEN ALLGOALS Clarify_tac);
   1.101 -by (subgoal_tac "Ca = cons(xb, Cb) - {x}" 1);
   1.102 -by (REPEAT(thin_tac "ALL C. ?P(C)" 2));
   1.103 -by (REPEAT(thin_tac "ALL x:?u. ?P(x)" 2));
   1.104 -by (blast_tac (claset() addEs [equalityE]) 2);
   1.105 -(** LEVEL 22 **)
   1.106 -by (subgoal_tac "|Ca| le |Cb|" 1);
   1.107 -by (rtac succ_le_imp_le 2);
   1.108 -by (hyp_subst_tac 2);
   1.109 -by (subgoal_tac "Finite(cons(xb, Cb)) & x:cons(xb, Cb) " 2);
   1.110 -by (asm_full_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, 
   1.111 -                       Fin_into_Finite RS Finite_imp_cardinal_cons]) 2);
   1.112 -by (asm_simp_tac (simpset() addsimps [Fin_into_Finite]) 2);
   1.113 -by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A"), ("f1", "f")] 
   1.114 -    (Fin_imp_fold_set RS exE) 1);
   1.115 -by (blast_tac (claset() addIs [Diff_subset RS Fin_subset]) 1);
   1.116 -by (Blast_tac 1);
   1.117 -by (blast_tac (claset() addSDs [FinD]) 1);
   1.118 -(** LEVEL 32 **)
   1.119 -by (ftac Diff1_fold_set 1);
   1.120 -by (Blast_tac 1);
   1.121 -by (Blast_tac 1);
   1.122 -by (blast_tac (claset() addSDs [fold_set.dom_subset RS subsetD]) 1);
   1.123 -by (subgoal_tac "ya = f(xb, xa)" 1);
   1.124 -by (dres_inst_tac [("x", "Ca")] spec 2);
   1.125 -by (blast_tac (claset() delrules [equalityCE]) 2);
   1.126 -by (subgoal_tac "<Cb-{x}, xa>: fold_set(A, B, f, e)" 1);
   1.127 -by (Asm_full_simp_tac 2);
   1.128 -by (subgoal_tac "yb = f(x, xa)" 1);
   1.129 -by (dres_inst_tac [("C", "Cb")] Diff1_fold_set 2);
   1.130 -by (ALLGOALS(Asm_simp_tac));
   1.131 -by (force_tac (claset() addSDs [fold_set.dom_subset RS subsetD], simpset()) 2);
   1.132 -by (force_tac (claset() addSDs [fold_set.dom_subset RS subsetD], simpset()) 1);
   1.133 -by (dres_inst_tac [("x", "Cb")] spec 1);
   1.134 -by Auto_tac;
   1.135 -qed_spec_mp "fold_set_determ_lemma";
   1.136 -
   1.137 -Goal
   1.138 -"[| <C, x>:fold_set(A, B, f, e); \
   1.139 -\        <C, y>:fold_set(A, B, f, e); e:B; \
   1.140 -\ ALL x:A. ALL y:B. f(x, y):B; \
   1.141 -\ ALL x:A. ALL y:A. ALL z:B.  f(x,f(y, z))=f(y, f(x, z)) |]\
   1.142 -\ ==> y=x";
   1.143 -by (forward_tac [fold_set.dom_subset RS subsetD] 1);
   1.144 -by (Clarify_tac 1);
   1.145 -by (dtac Fin_into_Finite 1);
   1.146 -by (rewtac Finite_def);
   1.147 -by (Clarify_tac 1);
   1.148 -by (res_inst_tac [("n", "succ(n)"), ("e", "e"), ("A", "A"),
   1.149 -                   ("f", "f"), ("B", "B")] fold_set_determ_lemma 1);
   1.150 -by (auto_tac (claset() addIs [eqpoll_imp_lepoll RS 
   1.151 -                              lepoll_cardinal_le], simpset()));
   1.152 -qed "fold_set_determ";
   1.153 -
   1.154 -(** The fold function **)
   1.155 -
   1.156 -Goalw [fold_def] 
   1.157 -"[| <C, y>:fold_set(A, B, f, e); e:B; \
   1.158 -\ ALL x:A. ALL y:B. f(x, y):B; \
   1.159 -\ ALL x:A. ALL y:A. ALL z:B.  f(x, f(y, z))=f(y, f(x, z)) |] \
   1.160 -\  ==> fold[B](f, e, C) = y";
   1.161 -by (forward_tac [fold_set.dom_subset RS subsetD] 1);
   1.162 -by (Clarify_tac 1);
   1.163 -by (rtac the_equality 1);
   1.164 -by (res_inst_tac [("f", "f"), ("e", "e"), ("B", "B")] fold_set_determ 2);
   1.165 -by (auto_tac (claset() addDs [fold_set_lemma], simpset()));
   1.166 -by (blast_tac (claset() addSDs [FinD]) 1);
   1.167 -qed "fold_equality";
   1.168 -
   1.169 -Goalw [fold_def] "e:B ==> fold[B](f,e,0) = e";
   1.170 -by (blast_tac (claset() addSEs [empty_fold_setE]
   1.171 -            addIs fold_set.intrs) 1);
   1.172 -qed "fold_0";
   1.173 -Addsimps [fold_0];
   1.174 -
   1.175 -Goal 
   1.176 -"[| C:Fin(A); c:A; c~:C; e:B; ALL x:A. ALL y:B. f(x, y):B;  \
   1.177 -\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x,z)) |]  \
   1.178 -\    ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <->  \
   1.179 -\         (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))";
   1.180 -by Auto_tac;
   1.181 -by (forward_tac [inst "a" "c" (thm"Fin.consI") RS FinD RS fold_set_mono RS subsetD] 1);
   1.182 -by (assume_tac 1);
   1.183 -by (assume_tac 1);
   1.184 -by (forward_tac [FinD RS fold_set_mono RS subsetD] 2);
   1.185 -by (assume_tac 2);
   1.186 -by (ALLGOALS(forward_tac [inst "A" "A" fold_set.dom_subset RS subsetD]));
   1.187 -by (ALLGOALS(dresolve_tac [FinD]));
   1.188 -by (res_inst_tac [("A1", "cons(c, C)"), ("f1", "f"),
   1.189 -                  ("B1", "B"), ("C1", "C")] (Fin_imp_fold_set RS exE) 1);
   1.190 -by (res_inst_tac [("b", "cons(c, C)")] Fin_subset 1);
   1.191 -by (resolve_tac [Finite_into_Fin] 2);
   1.192 -by (resolve_tac [Fin_into_Finite] 2);
   1.193 -by (Blast_tac 2);
   1.194 -by (res_inst_tac [("x", "x")] exI 4);
   1.195 -by (auto_tac (claset() addIs fold_set.intrs, simpset()));
   1.196 -by (dresolve_tac [inst "C" "C" fold_set_lemma] 1);
   1.197 -by (Blast_tac 1);
   1.198 -by (resolve_tac fold_set.intrs 2);
   1.199 -by Auto_tac;
   1.200 -by (blast_tac (claset() addIs [fold_set_mono RS subsetD]) 2);
   1.201 -by (resolve_tac [fold_set_determ] 1);
   1.202 -by (assume_tac 5);
   1.203 -by Auto_tac;
   1.204 -by (resolve_tac fold_set.intrs 1);
   1.205 -by Auto_tac;
   1.206 -by (blast_tac (claset() addIs [fold_set_mono RS subsetD]) 1);
   1.207 -by (blast_tac (claset() addDs [fold_set.dom_subset RS subsetD]) 1);
   1.208 -qed_spec_mp "fold_cons_lemma";
   1.209 -
   1.210 -Goalw [fold_def]
   1.211 -"[| C:Fin(A); c:A; c~:C; e:B; \
   1.212 -\ (ALL x:A. ALL y:B. f(x, y):B); \
   1.213 -\ (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z))) |]\
   1.214 -\   ==> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))";
   1.215 -by (asm_simp_tac (simpset() addsimps [fold_cons_lemma]) 1);
   1.216 -by (rtac the_equality 1);
   1.217 -by (dres_inst_tac [("e", "e"), ("f", "f")] Fin_imp_fold_set 1);
   1.218 -by Auto_tac;
   1.219 -by (res_inst_tac [("x", "x")] exI 1);
   1.220 -by Auto_tac;
   1.221 -by (blast_tac (claset() addDs [fold_set_lemma]) 1);
   1.222 -by (ALLGOALS(dtac fold_equality));
   1.223 -by (auto_tac (claset(), simpset() addsimps [symmetric fold_def]));
   1.224 -by (REPEAT(blast_tac (claset() addDs [FinD]) 1));
   1.225 -qed "fold_cons";
   1.226 -
   1.227 -Goal 
   1.228 -"[| C:Fin(A); e:B;  \
   1.229 -\ (ALL x:A. ALL y:B. f(x, y):B); \
   1.230 -\ (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z))) |] ==> \
   1.231 -\  fold[B](f, e,C):B";
   1.232 -by (etac Fin_induct 1);
   1.233 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [fold_cons])));
   1.234 -qed_spec_mp "fold_type";
   1.235 -AddTCs [fold_type];
   1.236 -Addsimps [fold_type];
   1.237 -
   1.238 -Goal 
   1.239 -"[| C:Fin(A); c:A; \
   1.240 -\ ALL x:A. ALL y:B. f(x, y):B; \
   1.241 -\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
   1.242 -\ ==> (ALL y:B. f(c, fold[B](f, y, C)) = fold[B](f, f(c, y), C))";
   1.243 -by (etac Fin_induct 1);
   1.244 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [fold_cons])));
   1.245 -qed_spec_mp "fold_commute";
   1.246 -
   1.247 -Goal "x:D ==> cons(x, C) Int D = cons(x, C Int D)";
   1.248 -by Auto_tac;
   1.249 -qed "cons_Int_right_lemma1";
   1.250 -
   1.251 -Goal "x~:D ==> cons(x, C) Int D = C Int D";
   1.252 -by Auto_tac;
   1.253 -qed "cons_Int_right_lemma2";
   1.254 -
   1.255 -Goal 
   1.256 -"[| C:Fin(A); D:Fin(A); e:B; \
   1.257 -\ ALL x:A. ALL y:B. f(x, y):B; \
   1.258 -\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
   1.259 -\ ==> \
   1.260 -\  fold[B](f, fold[B](f, e, D), C)  \
   1.261 -\  =  fold[B](f, fold[B](f, e, (C Int D)), C Un D)";
   1.262 -by (etac Fin_induct 1);
   1.263 -by Auto_tac;
   1.264 -by (subgoal_tac  "cons(x, y) Un D = cons(x, y Un D)" 1);
   1.265 -by Auto_tac;
   1.266 -by (subgoal_tac "y Int D:Fin(A) & y Un D:Fin(A)" 1);
   1.267 -by (Clarify_tac 1);
   1.268 -by (case_tac "x:D" 1);
   1.269 -by (ALLGOALS(asm_simp_tac (simpset() addsimps 
   1.270 -            [cons_Int_right_lemma1,cons_Int_right_lemma2,
   1.271 -             fold_cons, fold_commute,cons_absorb])));
   1.272 -qed "fold_nest_Un_Int";
   1.273 -
   1.274 -Goal "[| C:Fin(A); D:Fin(A); C Int D = 0; e:B; \
   1.275 -\ ALL x:A. ALL y:B. f(x, y):B; \
   1.276 -\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
   1.277 -\     ==> fold[B](f,e,C Un D) =  fold[B](f, fold[B](f,e,D), C)";
   1.278 -by (asm_simp_tac (simpset() addsimps [fold_nest_Un_Int]) 1);
   1.279 -qed "fold_nest_Un_disjoint";
   1.280 -
   1.281 -Goal "Finite(C) ==> C:Fin(cons(c, C))";
   1.282 -by (dtac Finite_into_Fin 1);
   1.283 -by (blast_tac (claset() addIs [Fin_mono RS subsetD]) 1);
   1.284 -qed "Finite_cons_lemma";
   1.285 -
   1.286 -(** setsum **)
   1.287 -
   1.288 -Goalw [setsum_def] "setsum(g, 0) = #0";
   1.289 -by (Simp_tac 1);
   1.290 -qed "setsum_0";
   1.291 -Addsimps [setsum_0];
   1.292 -
   1.293 -Goalw [setsum_def]
   1.294 -     "[| Finite(C); c~:C |] \
   1.295 -\     ==> setsum(g, cons(c, C)) = g(c) $+ setsum(g, C)";
   1.296 -by (auto_tac (claset(), simpset() addsimps [Finite_cons]));
   1.297 -by (res_inst_tac [("A", "cons(c, C)")] fold_cons 1);
   1.298 -by (auto_tac (claset() addIs [Finite_cons_lemma], simpset()));
   1.299 -qed "setsum_cons";
   1.300 -Addsimps [setsum_cons];
   1.301 -
   1.302 -Goal "setsum((%i. #0), C) = #0";
   1.303 -by (case_tac "Finite(C)" 1);
   1.304 -by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
   1.305 -by (etac Finite_induct 1);
   1.306 -by Auto_tac;
   1.307 -qed "setsum_K0";
   1.308 -
   1.309 -(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
   1.310 -Goal "[| Finite(C); Finite(D) |] \
   1.311 -\     ==> setsum(g, C Un D) $+ setsum(g, C Int D) \
   1.312 -\       = setsum(g, C) $+ setsum(g, D)";
   1.313 -by (etac Finite_induct 1);
   1.314 -by (subgoal_tac "cons(x, B) Un D = cons(x, B Un D) & \
   1.315 -                \ Finite(B Un D) & Finite(B Int D)" 2);
   1.316 -by (auto_tac (claset() addIs [Finite_Un, Int_lower1 RS subset_Finite], 
   1.317 -              simpset()));
   1.318 -by (case_tac "x:D" 1);
   1.319 -by (subgoal_tac "cons(x, B) Int D = B Int D" 2);
   1.320 -by (subgoal_tac "cons(x, B) Int D = cons(x, B Int D)" 1);
   1.321 -by Auto_tac;
   1.322 -by (subgoal_tac "cons(x, B Un D) = B Un D" 1);
   1.323 -by Auto_tac;
   1.324 -qed "setsum_Un_Int";
   1.325 -
   1.326 -Goal "setsum(g, C):int";
   1.327 -by (case_tac "Finite(C)" 1);
   1.328 -by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
   1.329 -by (etac Finite_induct 1);
   1.330 -by Auto_tac;
   1.331 -qed "setsum_type";
   1.332 -Addsimps [setsum_type];  AddTCs [setsum_type];
   1.333 -
   1.334 -Goal "[| Finite(C); Finite(D); C Int D = 0 |] \
   1.335 -\     ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)";  
   1.336 -by (stac (setsum_Un_Int RS sym) 1);
   1.337 -by (subgoal_tac "Finite(C Un D)" 3);
   1.338 -by (auto_tac (claset() addIs [Finite_Un], simpset()));
   1.339 -qed "setsum_Un_disjoint";
   1.340 -
   1.341 -Goal "Finite(I) ==> (ALL i:I. Finite(C(i))) --> Finite(RepFun(I, C))";
   1.342 -by (etac Finite_induct 1);
   1.343 -by Auto_tac;
   1.344 -qed_spec_mp "Finite_RepFun";
   1.345 -
   1.346 -Goal "Finite(I) \
   1.347 -\     ==> (ALL i:I. Finite(C(i))) --> \
   1.348 -\         (ALL i:I. ALL j:I. i~=j --> C(i) Int C(j) = 0) --> \
   1.349 -\         setsum(f, UN i:I. C(i)) = setsum (%i. setsum(f, C(i)), I)"; 
   1.350 -by (etac Finite_induct 1);
   1.351 -by (ALLGOALS(Clarify_tac));
   1.352 -by Auto_tac;
   1.353 -by (subgoal_tac "ALL i:B. x ~= i" 1);
   1.354 - by (Blast_tac 2); 
   1.355 -by (subgoal_tac "C(x) Int (UN i:B. C(i)) = 0" 1);
   1.356 - by (Blast_tac 2);
   1.357 -by (subgoal_tac "Finite(UN i:B. C(i)) & Finite(C(x)) & Finite(B)" 1);
   1.358 -by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1);
   1.359 -by (auto_tac (claset() addIs [Finite_Union, Finite_RepFun], simpset()));
   1.360 -qed_spec_mp "setsum_UN_disjoint";
   1.361 -
   1.362 -
   1.363 -Goal "setsum(%x. f(x) $+ g(x),C) = setsum(f, C) $+ setsum(g, C)";
   1.364 -by (case_tac "Finite(C)" 1);
   1.365 -by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
   1.366 -by (etac Finite_induct 1);
   1.367 -by Auto_tac;
   1.368 -qed "setsum_addf";
   1.369 -
   1.370 -
   1.371 -Goal "[| A=A'; B=B'; e=e';  \
   1.372 -\ (ALL x:A'. ALL y:B'. f(x,y) = f'(x,y)) |] ==> \
   1.373 -\  fold_set(A,B,f,e) = fold_set(A',B',f',e')";
   1.374 -by (asm_full_simp_tac (simpset() addsimps [thm"fold_set_def"]) 1); 
   1.375 -by (rtac (thm"lfp_cong") 1); 
   1.376 -by (rtac refl 1); 
   1.377 -by (rtac Collect_cong 1);  
   1.378 -by (rtac refl 1); 
   1.379 -by (rtac disj_cong 1);  
   1.380 -by (rtac iff_refl 1); 
   1.381 -by (REPEAT (rtac ex_cong 1));  
   1.382 -by Auto_tac; 
   1.383 -qed "fold_set_cong";
   1.384 -
   1.385 -val prems = Goal 
   1.386 -"[| B=B'; A=A'; e=e';  \
   1.387 -\   !!x y. [|x:A'; y:B'|] ==> f(x,y) = f'(x,y) |] ==> \
   1.388 -\  fold[B](f,e,A) = fold[B'](f', e', A')";
   1.389 -by (asm_full_simp_tac (simpset() addsimps fold_def::prems) 1); 
   1.390 -by (stac fold_set_cong 1); 
   1.391 -by (rtac refl 5); 
   1.392 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps prems)));
   1.393 -qed "fold_cong";
   1.394 -
   1.395 -val prems = Goal
   1.396 - "[| A=B; !!x. x:B ==> f(x) = g(x) |] ==> \
   1.397 -\    setsum(f, A) = setsum(g, B)";
   1.398 -by (asm_simp_tac (simpset() addsimps setsum_def::prems addcongs [fold_cong]) 1);
   1.399 -qed  "setsum_cong";
   1.400 -
   1.401 -Goal "[| Finite(A); Finite(B) |] \
   1.402 -\     ==> setsum(f, A Un B) = \
   1.403 -\         setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)";
   1.404 -by (stac (setsum_Un_Int RS sym) 1);
   1.405 -by Auto_tac;
   1.406 -qed "setsum_Un";
   1.407 -
   1.408 -
   1.409 -Goal "Finite(A) ==> (ALL x:A. g(x) $<= #0) --> setsum(g, A) $<= #0";
   1.410 -by (etac Finite_induct 1);
   1.411 -by (auto_tac (claset() addIs [zneg_or_0_add_zneg_or_0_imp_zneg_or_0], simpset()));
   1.412 -qed_spec_mp "setsum_zneg_or_0";
   1.413 -
   1.414 -Goal "Finite(A) \
   1.415 -\     ==> ALL n:nat. setsum(f,A) = $# succ(n) --> (EX a:A. #0 $< f(a))";
   1.416 -by (etac Finite_induct 1);
   1.417 -by (auto_tac (claset(), simpset() 
   1.418 -           delsimps [int_of_0, int_of_succ]
   1.419 -           addsimps [not_zless_iff_zle, int_of_0 RS sym]));
   1.420 -by (subgoal_tac "setsum(f, B) $<= #0" 1);
   1.421 -by (ALLGOALS(Asm_full_simp_tac));
   1.422 -by (blast_tac (claset() addIs [setsum_zneg_or_0]) 2);
   1.423 -by (subgoal_tac "$# 1 $<= f(x) $+ setsum(f, B)" 1);
   1.424 -by (dtac  (zdiff_zle_iff RS iffD2) 1);
   1.425 -by (subgoal_tac "$# 1 $<= $# 1 $- setsum(f,B)" 1);
   1.426 -by (dres_inst_tac [("x",  "$# 1")] zle_trans 1);
   1.427 -by (res_inst_tac [("j", "#1")] zless_zle_trans 2);
   1.428 -by Auto_tac;
   1.429 -qed "setsum_succD_lemma";
   1.430 -
   1.431 -Goal "[| setsum(f, A) = $# succ(n); n:nat |]==> EX a:A. #0 $< f(a)";
   1.432 -by (case_tac "Finite(A)" 1);
   1.433 -by (blast_tac (claset() 
   1.434 -     addIs [setsum_succD_lemma RS bspec RS mp]) 1);
   1.435 -by (rewtac setsum_def);
   1.436 -by (auto_tac (claset(), 
   1.437 -       simpset() delsimps [int_of_0, int_of_succ] 
   1.438 -                 addsimps [int_succ_int_1 RS sym, int_of_0 RS sym]));
   1.439 -qed "setsum_succD";
   1.440 -
   1.441 -Goal "Finite(A) ==> (ALL x:A. #0 $<= g(x)) --> #0 $<= setsum(g, A)";
   1.442 -by (etac Finite_induct 1);
   1.443 -by (Simp_tac 1);
   1.444 -by (auto_tac (claset() addIs [zpos_add_zpos_imp_zpos],  simpset()));
   1.445 -qed_spec_mp "g_zpos_imp_setsum_zpos";
   1.446 -
   1.447 -Goal "[| Finite(A); ALL x. #0 $<= g(x) |] ==> #0 $<= setsum(g, A)";
   1.448 -by (etac Finite_induct 1);
   1.449 -by (auto_tac (claset() addIs [zpos_add_zpos_imp_zpos], simpset()));
   1.450 -qed_spec_mp "g_zpos_imp_setsum_zpos2";
   1.451 -
   1.452 -Goal "Finite(A) \
   1.453 -\     ==> (ALL x:A. #0 $< g(x)) --> A ~= 0 --> (#0 $< setsum(g, A))";
   1.454 -by (etac Finite_induct 1);
   1.455 -by (auto_tac (claset() addIs [zspos_add_zspos_imp_zspos],simpset()));
   1.456 -qed_spec_mp "g_zspos_imp_setsum_zspos";
   1.457 -
   1.458 -Goal "Finite(A) \
   1.459 -\     ==> ALL a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})";
   1.460 -by (etac Finite_induct 1);
   1.461 -by (ALLGOALS(Clarify_tac));
   1.462 -by (Simp_tac 1);
   1.463 -by (case_tac "x=a" 1);
   1.464 -by (subgoal_tac "cons(x, B) - {a} = cons(x, B -{a}) & Finite(B - {a})" 2);
   1.465 -by (subgoal_tac "cons(a, B) - {a} = B" 1);
   1.466 -by (auto_tac (claset() addIs [Finite_Diff], simpset()));
   1.467 -qed_spec_mp "setsum_Diff";
     2.1 --- a/src/ZF/Induct/FoldSet.thy	Tue Jun 24 10:42:34 2003 +0200
     2.2 +++ b/src/ZF/Induct/FoldSet.thy	Tue Jun 24 16:32:59 2003 +0200
     2.3 @@ -8,24 +8,419 @@
     2.4  least left-commutative.  
     2.5  *)
     2.6  
     2.7 -FoldSet = Main +
     2.8 +theory FoldSet = Main:
     2.9  
    2.10  consts fold_set :: "[i, i, [i,i]=>i, i] => i"
    2.11  
    2.12  inductive
    2.13    domains "fold_set(A, B, f,e)" <= "Fin(A)*B"
    2.14 -  intrs
    2.15 -  emptyI   "e:B ==> <0, e>:fold_set(A, B, f,e)"
    2.16 -  consI  "[| x:A; x ~:C;  <C,y> : fold_set(A, B,f,e); f(x,y):B |]
    2.17 -              ==>  <cons(x,C), f(x,y)>:fold_set(A, B, f, e)"
    2.18 -   type_intrs "Fin_intros"
    2.19 +  intros
    2.20 +    emptyI: "e\<in>B ==> <0, e>\<in>fold_set(A, B, f,e)"
    2.21 +    consI:  "[| x\<in>A; x \<notin>C;  <C,y> : fold_set(A, B,f,e); f(x,y):B |]
    2.22 +		==>  <cons(x,C), f(x,y)>\<in>fold_set(A, B, f, e)"
    2.23 +  type_intros Fin.intros
    2.24    
    2.25  constdefs
    2.26    
    2.27    fold :: "[i, [i,i]=>i, i, i] => i"  ("fold[_]'(_,_,_')")
    2.28 -  "fold[B](f,e, A) == THE x. <A, x>:fold_set(A, B, f,e)"
    2.29 +   "fold[B](f,e, A) == THE x. <A, x>\<in>fold_set(A, B, f,e)"
    2.30  
    2.31     setsum :: "[i=>i, i] => i"
    2.32 -  "setsum(g, C) == if Finite(C) then
    2.33 -                    fold[int](%x y. g(x) $+ y, #0, C) else #0"
    2.34 +   "setsum(g, C) == if Finite(C) then
    2.35 +                     fold[int](%x y. g(x) $+ y, #0, C) else #0"
    2.36 +
    2.37 +(** foldSet **)
    2.38 +
    2.39 +inductive_cases empty_fold_setE: "<0, x> : fold_set(A, B, f,e)"
    2.40 +inductive_cases cons_fold_setE: "<cons(x,C), y> : fold_set(A, B, f,e)"
    2.41 +
    2.42 +(* add-hoc lemmas *)                                                
    2.43 +
    2.44 +lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) <-> B = C"
    2.45 +by (auto elim: equalityE)
    2.46 +
    2.47 +lemma cons_lemma2: "[| cons(x, B)=cons(y, C); x\<noteq>y; x\<notin>B; y\<notin>C |]  
    2.48 +    ==>  B - {y} = C-{x} & x\<in>C & y\<in>B"
    2.49 +apply (auto elim: equalityE)
    2.50 +done
    2.51 +
    2.52 +(* fold_set monotonicity *)
    2.53 +lemma fold_set_mono_lemma:
    2.54 +     "<C, x> : fold_set(A, B, f, e)  
    2.55 +      ==> ALL D. A<=D --> <C, x> : fold_set(D, B, f, e)"
    2.56 +apply (erule fold_set.induct)
    2.57 +apply (auto intro: fold_set.intros)
    2.58 +done
    2.59 +
    2.60 +lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)"
    2.61 +apply clarify
    2.62 +apply (frule fold_set.dom_subset [THEN subsetD], clarify)
    2.63 +apply (auto dest: fold_set_mono_lemma)
    2.64 +done
    2.65 +
    2.66 +lemma fold_set_lemma:
    2.67 +     "<C, x>\<in>fold_set(A, B, f, e) ==> <C, x>\<in>fold_set(C, B, f, e) & C<=A"
    2.68 +apply (erule fold_set.induct)
    2.69 +apply (auto intro!: fold_set.intros intro: fold_set_mono [THEN subsetD])
    2.70 +done
    2.71 +
    2.72 +(* Proving that fold_set is deterministic *)
    2.73 +lemma Diff1_fold_set:
    2.74 +     "[| <C-{x},y> : fold_set(A, B, f,e);  x\<in>C; x\<in>A; f(x, y):B |]  
    2.75 +      ==> <C, f(x, y)> : fold_set(A, B, f, e)"
    2.76 +apply (frule fold_set.dom_subset [THEN subsetD])
    2.77 +apply (erule cons_Diff [THEN subst], rule fold_set.intros, auto)
    2.78 +done
    2.79 +
    2.80 +
    2.81 +locale fold_typing =
    2.82 + fixes A and B and e and f
    2.83 + assumes ftype [intro,simp]:  "[|x \<in> A; y \<in> B|] ==> f(x,y) \<in> B"
    2.84 +     and etype [intro,simp]:  "e \<in> B"
    2.85 +     and fcomm:  "[|x \<in> A; y \<in> A; z \<in> B|] ==> f(x, f(y, z))=f(y, f(x, z))"
    2.86 +
    2.87 +
    2.88 +lemma (in fold_typing) Fin_imp_fold_set:
    2.89 +     "C\<in>Fin(A) ==> (EX x. <C, x> : fold_set(A, B, f,e))"
    2.90 +apply (erule Fin_induct)
    2.91 +apply (auto dest: fold_set.dom_subset [THEN subsetD] 
    2.92 +            intro: fold_set.intros etype ftype)
    2.93 +done
    2.94 +
    2.95 +lemma Diff_sing_imp:
    2.96 +     "[|C - {b} = D - {a}; a \<noteq> b; b \<in> C|] ==> C = cons(b,D) - {a}"
    2.97 +by (blast elim: equalityE)
    2.98 +
    2.99 +lemma (in fold_typing) fold_set_determ_lemma [rule_format]: 
   2.100 +"n\<in>nat
   2.101 + ==> ALL C. |C|<n -->  
   2.102 +   (ALL x. <C, x> : fold_set(A, B, f,e)--> 
   2.103 +           (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x))"
   2.104 +apply (erule nat_induct)
   2.105 + apply (auto simp add: le_iff)
   2.106 +apply (erule fold_set.cases)
   2.107 + apply (force elim!: empty_fold_setE)
   2.108 +apply (erule fold_set.cases)
   2.109 + apply (force elim!: empty_fold_setE, clarify)
   2.110 +(*force simplification of "|C| < |cons(...)|"*)
   2.111 +apply (frule_tac a = Ca in fold_set.dom_subset [THEN subsetD, THEN SigmaD1])
   2.112 +apply (frule_tac a = Cb in fold_set.dom_subset [THEN subsetD, THEN SigmaD1])
   2.113 +apply (simp add: Fin_into_Finite [THEN Finite_imp_cardinal_cons])
   2.114 +apply (case_tac "x=xb", auto) 
   2.115 +apply (simp add: cons_lemma1, blast)
   2.116 +txt{*case @{term "x\<noteq>xb"}*}
   2.117 +apply (drule cons_lemma2, safe)
   2.118 +apply (frule Diff_sing_imp, assumption+) 
   2.119 +txt{** LEVEL 17*}
   2.120 +apply (subgoal_tac "|Ca| le |Cb|")
   2.121 + prefer 2
   2.122 + apply (rule succ_le_imp_le)
   2.123 + apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff 
   2.124 +                  Fin_into_Finite [THEN Finite_imp_cardinal_cons])
   2.125 +apply (rule_tac C1 = "Ca-{xb}" in Fin_imp_fold_set [THEN exE])
   2.126 + apply (blast intro: Diff_subset [THEN Fin_subset])
   2.127 +txt{** LEVEL 24 **}
   2.128 +apply (frule Diff1_fold_set, blast, blast)
   2.129 +apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD])
   2.130 +apply (subgoal_tac "ya = f(xb,xa) ")
   2.131 + prefer 2 apply (blast del: equalityCE)
   2.132 +apply (subgoal_tac "<Cb-{x}, xa> : fold_set(A,B,f,e)")
   2.133 + prefer 2 apply simp
   2.134 +apply (subgoal_tac "yb = f (x, xa) ")
   2.135 + apply (drule_tac [2] C = Cb in Diff1_fold_set, simp_all)
   2.136 +  apply (blast intro: fcomm dest!: fold_set.dom_subset [THEN subsetD])
   2.137 + apply (blast intro: ftype dest!: fold_set.dom_subset [THEN subsetD], blast) 
   2.138 +done
   2.139 +
   2.140 +lemma (in fold_typing) fold_set_determ: 
   2.141 +     "[| <C, x>\<in>fold_set(A, B, f, e);  
   2.142 +         <C, y>\<in>fold_set(A, B, f, e)|] ==> y=x"
   2.143 +apply (frule fold_set.dom_subset [THEN subsetD], clarify)
   2.144 +apply (drule Fin_into_Finite)
   2.145 +apply (unfold Finite_def, clarify)
   2.146 +apply (rule_tac n = "succ (n)" in fold_set_determ_lemma) 
   2.147 +apply (auto intro: eqpoll_imp_lepoll [THEN lepoll_cardinal_le])
   2.148 +done
   2.149 +
   2.150 +(** The fold function **)
   2.151 +
   2.152 +lemma (in fold_typing) fold_equality: 
   2.153 +     "<C,y> : fold_set(A,B,f,e) ==> fold[B](f,e,C) = y"
   2.154 +apply (unfold fold_def)
   2.155 +apply (frule fold_set.dom_subset [THEN subsetD], clarify)
   2.156 +apply (rule the_equality)
   2.157 + apply (rule_tac [2] A=C in fold_typing.fold_set_determ)
   2.158 +apply (force dest: fold_set_lemma)
   2.159 +apply (auto dest: fold_set_lemma)
   2.160 +apply (simp add: fold_typing_def, auto) 
   2.161 +apply (auto dest: fold_set_lemma intro: ftype etype fcomm)
   2.162 +done
   2.163 +
   2.164 +lemma fold_0 [simp]: "e : B ==> fold[B](f,e,0) = e"
   2.165 +apply (unfold fold_def)
   2.166 +apply (blast elim!: empty_fold_setE intro: fold_set.intros)
   2.167 +done
   2.168 +
   2.169 +text{*This result is the right-to-left direction of the subsequent result*}
   2.170 +lemma (in fold_typing) fold_set_imp_cons: 
   2.171 +     "[| <C, y> : fold_set(C, B, f, e); C : Fin(A); c : A; c\<notin>C |]
   2.172 +      ==> <cons(c, C), f(c,y)> : fold_set(cons(c, C), B, f, e)"
   2.173 +apply (frule FinD [THEN fold_set_mono, THEN subsetD])
   2.174 + apply assumption
   2.175 +apply (frule fold_set.dom_subset [of A, THEN subsetD])
   2.176 +apply (blast intro!: fold_set.consI intro: fold_set_mono [THEN subsetD])
   2.177 +done
   2.178 +
   2.179 +lemma (in fold_typing) fold_cons_lemma [rule_format]: 
   2.180 +"[| C : Fin(A); c : A; c\<notin>C |]   
   2.181 +     ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <->   
   2.182 +         (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))"
   2.183 +apply auto
   2.184 + prefer 2 apply (blast intro: fold_set_imp_cons) 
   2.185 + apply (frule_tac Fin.consI [of c, THEN FinD, THEN fold_set_mono, THEN subsetD], assumption+)
   2.186 +apply (frule_tac fold_set.dom_subset [of A, THEN subsetD])
   2.187 +apply (drule FinD) 
   2.188 +apply (rule_tac A1 = "cons(c,C)" and f1=f and B1=B and C1=C and e1=e in fold_typing.Fin_imp_fold_set [THEN exE])
   2.189 +apply (blast intro: fold_typing.intro ftype etype fcomm) 
   2.190 +apply (blast intro: Fin_subset [of _ "cons(c,C)"] Finite_into_Fin 
   2.191 +             dest: Fin_into_Finite)  
   2.192 +apply (rule_tac x = x in exI)
   2.193 +apply (auto intro: fold_set.intros)
   2.194 +apply (drule_tac fold_set_lemma [of C], blast)
   2.195 +apply (blast intro!: fold_set.consI
   2.196 +             intro: fold_set_determ fold_set_mono [THEN subsetD] 
   2.197 +             dest: fold_set.dom_subset [THEN subsetD]) 
   2.198 +done
   2.199 +
   2.200 +lemma (in fold_typing) fold_cons: 
   2.201 +     "[| C\<in>Fin(A); c\<in>A; c\<notin>C|] 
   2.202 +      ==> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))"
   2.203 +apply (unfold fold_def)
   2.204 +apply (simp add: fold_cons_lemma)
   2.205 +apply (rule the_equality, auto) 
   2.206 + apply (subgoal_tac [2] "\<langle>C, y\<rangle> \<in> fold_set(A, B, f, e)")
   2.207 +  apply (drule Fin_imp_fold_set)
   2.208 +apply (auto dest: fold_set_lemma  simp add: fold_def [symmetric] fold_equality) 
   2.209 +apply (blast intro: fold_set_mono [THEN subsetD] dest!: FinD) 
   2.210 +done
   2.211 +
   2.212 +lemma (in fold_typing) fold_type [simp,TC]: 
   2.213 +     "C\<in>Fin(A) ==> fold[B](f,e,C):B"
   2.214 +apply (erule Fin_induct)
   2.215 +apply (simp_all add: fold_cons ftype etype)
   2.216 +done
   2.217 +
   2.218 +lemma (in fold_typing) fold_commute [rule_format]: 
   2.219 +     "[| C\<in>Fin(A); c\<in>A |]  
   2.220 +      ==> (\<forall>y\<in>B. f(c, fold[B](f, y, C)) = fold[B](f, f(c, y), C))"
   2.221 +apply (erule Fin_induct)
   2.222 +apply (simp_all add: fold_typing.fold_cons [of A B _ f] 
   2.223 +                     fold_typing.fold_type [of A B _ f] 
   2.224 +                     fold_typing_def fcomm)
   2.225 +done
   2.226 +
   2.227 +lemma (in fold_typing) fold_nest_Un_Int: 
   2.228 +     "[| C\<in>Fin(A); D\<in>Fin(A) |]
   2.229 +      ==> fold[B](f, fold[B](f, e, D), C) =
   2.230 +          fold[B](f, fold[B](f, e, (C Int D)), C Un D)"
   2.231 +apply (erule Fin_induct, auto)
   2.232 +apply (simp add: Un_cons Int_cons_left fold_type fold_commute
   2.233 +                 fold_typing.fold_cons [of A _ _ f] 
   2.234 +                 fold_typing_def fcomm cons_absorb)
   2.235 +done
   2.236 +
   2.237 +lemma (in fold_typing) fold_nest_Un_disjoint:
   2.238 +     "[| C\<in>Fin(A); D\<in>Fin(A); C Int D = 0 |]  
   2.239 +      ==> fold[B](f,e,C Un D) =  fold[B](f, fold[B](f,e,D), C)"
   2.240 +by (simp add: fold_nest_Un_Int)
   2.241 +
   2.242 +lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))"
   2.243 +apply (drule Finite_into_Fin)
   2.244 +apply (blast intro: Fin_mono [THEN subsetD])
   2.245 +done
   2.246 +
   2.247 +subsection{*The Operator @{term setsum}*}
   2.248 +
   2.249 +lemma setsum_0 [simp]: "setsum(g, 0) = #0"
   2.250 +by (simp add: setsum_def)
   2.251 +
   2.252 +lemma setsum_cons [simp]: 
   2.253 +     "Finite(C) ==> 
   2.254 +      setsum(g, cons(c,C)) = 
   2.255 +        (if c : C then setsum(g,C) else g(c) $+ setsum(g,C))"
   2.256 +apply (auto simp add: setsum_def Finite_cons cons_absorb)
   2.257 +apply (rule_tac A = "cons (c, C)" in fold_typing.fold_cons)
   2.258 +apply (auto intro: fold_typing.intro Finite_cons_lemma)
   2.259 +done
   2.260 +
   2.261 +lemma setsum_K0: "setsum((%i. #0), C) = #0"
   2.262 +apply (case_tac "Finite (C) ")
   2.263 + prefer 2 apply (simp add: setsum_def)
   2.264 +apply (erule Finite_induct, auto)
   2.265 +done
   2.266 +
   2.267 +(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
   2.268 +lemma setsum_Un_Int:
   2.269 +     "[| Finite(C); Finite(D) |]  
   2.270 +      ==> setsum(g, C Un D) $+ setsum(g, C Int D)  
   2.271 +        = setsum(g, C) $+ setsum(g, D)"
   2.272 +apply (erule Finite_induct)
   2.273 +apply (simp_all add: Int_cons_right cons_absorb Un_cons Int_commute Finite_Un
   2.274 +                     Int_lower1 [THEN subset_Finite]) 
   2.275 +done
   2.276 +
   2.277 +lemma setsum_type [simp,TC]: "setsum(g, C):int"
   2.278 +apply (case_tac "Finite (C) ")
   2.279 + prefer 2 apply (simp add: setsum_def)
   2.280 +apply (erule Finite_induct, auto)
   2.281 +done
   2.282 +
   2.283 +lemma setsum_Un_disjoint:
   2.284 +     "[| Finite(C); Finite(D); C Int D = 0 |]  
   2.285 +      ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)"
   2.286 +apply (subst setsum_Un_Int [symmetric])
   2.287 +apply (subgoal_tac [3] "Finite (C Un D) ")
   2.288 +apply (auto intro: Finite_Un)
   2.289 +done
   2.290 +
   2.291 +lemma Finite_RepFun [rule_format (no_asm)]:
   2.292 +     "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) --> Finite(RepFun(I, C))"
   2.293 +apply (erule Finite_induct, auto)
   2.294 +done
   2.295 +
   2.296 +lemma setsum_UN_disjoint [rule_format (no_asm)]:
   2.297 +     "Finite(I)  
   2.298 +      ==> (\<forall>i\<in>I. Finite(C(i))) -->  
   2.299 +          (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j --> C(i) Int C(j) = 0) -->  
   2.300 +          setsum(f, \<Union>i\<in>I. C(i)) = setsum (%i. setsum(f, C(i)), I)"
   2.301 +apply (erule Finite_induct, auto)
   2.302 +apply (subgoal_tac "\<forall>i\<in>B. x \<noteq> i")
   2.303 + prefer 2 apply blast
   2.304 +apply (subgoal_tac "C (x) Int (\<Union>i\<in>B. C (i)) = 0")
   2.305 + prefer 2 apply blast
   2.306 +apply (subgoal_tac "Finite (\<Union>i\<in>B. C (i)) & Finite (C (x)) & Finite (B) ")
   2.307 +apply (simp (no_asm_simp) add: setsum_Un_disjoint)
   2.308 +apply (auto intro: Finite_Union Finite_RepFun)
   2.309 +done
   2.310 +
   2.311 +
   2.312 +lemma setsum_addf: "setsum(%x. f(x) $+ g(x),C) = setsum(f, C) $+ setsum(g, C)"
   2.313 +apply (case_tac "Finite (C) ")
   2.314 + prefer 2 apply (simp add: setsum_def)
   2.315 +apply (erule Finite_induct, auto)
   2.316 +done
   2.317 +
   2.318 +
   2.319 +lemma fold_set_cong:
   2.320 +     "[| A=A'; B=B'; e=e'; (\<forall>x\<in>A'. \<forall>y\<in>B'. f(x,y) = f'(x,y)) |] 
   2.321 +      ==> fold_set(A,B,f,e) = fold_set(A',B',f',e')"
   2.322 +apply (simp add: fold_set_def)
   2.323 +apply (intro refl iff_refl lfp_cong Collect_cong disj_cong ex_cong, auto)
   2.324 +done
   2.325 +
   2.326 +lemma fold_cong:
   2.327 +"[| B=B'; A=A'; e=e';   
   2.328 +    !!x y. [|x\<in>A'; y\<in>B'|] ==> f(x,y) = f'(x,y) |] ==>  
   2.329 +   fold[B](f,e,A) = fold[B'](f', e', A')"
   2.330 +apply (simp add: fold_def)
   2.331 +apply (subst fold_set_cong)
   2.332 +apply (rule_tac [5] refl, simp_all)
   2.333 +done
   2.334 +
   2.335 +lemma setsum_cong:
   2.336 + "[| A=B; !!x. x\<in>B ==> f(x) = g(x) |] ==>  
   2.337 +     setsum(f, A) = setsum(g, B)"
   2.338 +by (simp add: setsum_def cong add: fold_cong)
   2.339 +
   2.340 +lemma setsum_Un:
   2.341 +     "[| Finite(A); Finite(B) |]  
   2.342 +      ==> setsum(f, A Un B) =  
   2.343 +          setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)"
   2.344 +apply (subst setsum_Un_Int [symmetric], auto)
   2.345 +done
   2.346 +
   2.347 +
   2.348 +lemma setsum_zneg_or_0 [rule_format (no_asm)]:
   2.349 +     "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) --> setsum(g, A) $<= #0"
   2.350 +apply (erule Finite_induct)
   2.351 +apply (auto intro: zneg_or_0_add_zneg_or_0_imp_zneg_or_0)
   2.352 +done
   2.353 +
   2.354 +lemma setsum_succD_lemma [rule_format]:
   2.355 +     "Finite(A)  
   2.356 +      ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) --> (\<exists>a\<in>A. #0 $< f(a))"
   2.357 +apply (erule Finite_induct)
   2.358 +apply (auto simp del: int_of_0 int_of_succ simp add: not_zless_iff_zle int_of_0 [symmetric])
   2.359 +apply (subgoal_tac "setsum (f, B) $<= #0")
   2.360 +apply simp_all
   2.361 +prefer 2 apply (blast intro: setsum_zneg_or_0)
   2.362 +apply (subgoal_tac "$# 1 $<= f (x) $+ setsum (f, B) ")
   2.363 +apply (drule zdiff_zle_iff [THEN iffD2])
   2.364 +apply (subgoal_tac "$# 1 $<= $# 1 $- setsum (f,B) ")
   2.365 +apply (drule_tac x = "$# 1" in zle_trans)
   2.366 +apply (rule_tac [2] j = "#1" in zless_zle_trans, auto)
   2.367 +done
   2.368 +
   2.369 +lemma setsum_succD:
   2.370 +     "[| setsum(f, A) = $# succ(n); n\<in>nat |]==> \<exists>a\<in>A. #0 $< f(a)"
   2.371 +apply (case_tac "Finite (A) ")
   2.372 +apply (blast intro: setsum_succD_lemma)
   2.373 +apply (unfold setsum_def)
   2.374 +apply (auto simp del: int_of_0 int_of_succ simp add: int_succ_int_1 [symmetric] int_of_0 [symmetric])
   2.375 +done
   2.376 +
   2.377 +lemma g_zpos_imp_setsum_zpos [rule_format]:
   2.378 +     "Finite(A) ==> (\<forall>x\<in>A. #0 $<= g(x)) --> #0 $<= setsum(g, A)"
   2.379 +apply (erule Finite_induct)
   2.380 +apply (simp (no_asm))
   2.381 +apply (auto intro: zpos_add_zpos_imp_zpos)
   2.382 +done
   2.383 +
   2.384 +lemma g_zpos_imp_setsum_zpos2 [rule_format]:
   2.385 +     "[| Finite(A); \<forall>x. #0 $<= g(x) |] ==> #0 $<= setsum(g, A)"
   2.386 +apply (erule Finite_induct)
   2.387 +apply (auto intro: zpos_add_zpos_imp_zpos)
   2.388 +done
   2.389 +
   2.390 +lemma g_zspos_imp_setsum_zspos [rule_format]:
   2.391 +     "Finite(A)  
   2.392 +      ==> (\<forall>x\<in>A. #0 $< g(x)) --> A \<noteq> 0 --> (#0 $< setsum(g, A))"
   2.393 +apply (erule Finite_induct)
   2.394 +apply (auto intro: zspos_add_zspos_imp_zspos)
   2.395 +done
   2.396 +
   2.397 +lemma setsum_Diff [rule_format]:
   2.398 +     "Finite(A) ==> \<forall>a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})"
   2.399 +apply (erule Finite_induct) 
   2.400 +apply (simp_all add: Diff_cons_eq Finite_Diff) 
   2.401 +done
   2.402 +
   2.403 +ML
   2.404 +{*
   2.405 +val fold_set_mono = thm "fold_set_mono";
   2.406 +val Diff1_fold_set = thm "Diff1_fold_set";
   2.407 +val Diff_sing_imp = thm "Diff_sing_imp";
   2.408 +val fold_0 = thm "fold_0";
   2.409 +val setsum_0 = thm "setsum_0";
   2.410 +val setsum_cons = thm "setsum_cons";
   2.411 +val setsum_K0 = thm "setsum_K0";
   2.412 +val setsum_Un_Int = thm "setsum_Un_Int";
   2.413 +val setsum_type = thm "setsum_type";
   2.414 +val setsum_Un_disjoint = thm "setsum_Un_disjoint";
   2.415 +val Finite_RepFun = thm "Finite_RepFun";
   2.416 +val setsum_UN_disjoint = thm "setsum_UN_disjoint";
   2.417 +val setsum_addf = thm "setsum_addf";
   2.418 +val fold_set_cong = thm "fold_set_cong";
   2.419 +val fold_cong = thm "fold_cong";
   2.420 +val setsum_cong = thm "setsum_cong";
   2.421 +val setsum_Un = thm "setsum_Un";
   2.422 +val setsum_zneg_or_0 = thm "setsum_zneg_or_0";
   2.423 +val setsum_succD = thm "setsum_succD";
   2.424 +val g_zpos_imp_setsum_zpos = thm "g_zpos_imp_setsum_zpos";
   2.425 +val g_zpos_imp_setsum_zpos2 = thm "g_zpos_imp_setsum_zpos2";
   2.426 +val g_zspos_imp_setsum_zspos = thm "g_zspos_imp_setsum_zspos";
   2.427 +val setsum_Diff = thm "setsum_Diff";
   2.428 +*}
   2.429 +
   2.430 +
   2.431  end
   2.432 \ No newline at end of file
     3.1 --- a/src/ZF/Induct/Multiset.ML	Tue Jun 24 10:42:34 2003 +0200
     3.2 +++ b/src/ZF/Induct/Multiset.ML	Tue Jun 24 16:32:59 2003 +0200
     3.3 @@ -398,11 +398,6 @@
     3.4         addsimps [int_of_add RS sym, int_of_0 RS sym]));
     3.5  qed "msize_eq_0_iff";
     3.6  
     3.7 -Goal 
     3.8 -"cons(x, A) Int B = (if x:B then cons(x, A Int B) else A Int B)";
     3.9 -by Auto_tac;
    3.10 -qed "cons_Int_right_cases";
    3.11 -
    3.12  Goal
    3.13  "Finite(A) ==> setsum(%a. $# mcount(N, a), A Int mset_of(N)) \
    3.14  \            = setsum(%a. $# mcount(N, a), A)";
    3.15 @@ -411,7 +406,7 @@
    3.16  by (subgoal_tac "Finite(B Int mset_of(N))" 1);
    3.17  by (blast_tac (claset() addIs [subset_Finite]) 2);
    3.18  by (auto_tac (claset(), 
    3.19 -         simpset() addsimps [mcount_def, cons_Int_right_cases]));
    3.20 +         simpset() addsimps [mcount_def, Int_cons_left]));
    3.21  qed "setsum_mcount_Int";
    3.22  
    3.23  Goalw [msize_def]
     4.1 --- a/src/ZF/IsaMakefile	Tue Jun 24 10:42:34 2003 +0200
     4.2 +++ b/src/ZF/IsaMakefile	Tue Jun 24 16:32:59 2003 +0200
     4.3 @@ -138,7 +138,7 @@
     4.4  
     4.5  $(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.thy \
     4.6    Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \
     4.7 -  Induct/Datatypes.thy Induct/FoldSet.ML Induct/FoldSet.thy \
     4.8 +  Induct/Datatypes.thy Induct/FoldSet.thy \
     4.9    Induct/ListN.thy Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
    4.10    Induct/Ntree.thy Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \
    4.11    Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
     5.1 --- a/src/ZF/UNITY/AllocImpl.thy	Tue Jun 24 10:42:34 2003 +0200
     5.2 +++ b/src/ZF/UNITY/AllocImpl.thy	Tue Jun 24 16:32:59 2003 +0200
     5.3 @@ -7,21 +7,6 @@
     5.4  Charpentier and Chandy, section 7 (page 17).
     5.5  *)
     5.6  
     5.7 -(*LOCALE NEEDED FOR PROOF OF GUARANTEES THEOREM*)
     5.8 -
     5.9 -(*????FIXME: sort out this mess
    5.10 -FoldSet.cons_Int_right_lemma1:
    5.11 -  ?x \<in> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = cons(?x, ?C \<inter> ?D)
    5.12 -FoldSet.cons_Int_right_lemma2: ?x \<notin> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = ?C \<inter> ?D
    5.13 -Multiset.cons_Int_right_cases:
    5.14 -  cons(?x, ?A) \<inter> ?B = (if ?x \<in> ?B then cons(?x, ?A \<inter> ?B) else ?A \<inter> ?B)
    5.15 -UNITYMisc.Int_cons_right:
    5.16 -  ?A \<inter> cons(?a, ?B) = (if ?a \<in> ?A then cons(?a, ?A \<inter> ?B) else ?A \<inter> ?B)
    5.17 -UNITYMisc.Int_succ_right:
    5.18 -  ?A \<inter> succ(?k) = (if ?k \<in> ?A then cons(?k, ?A \<inter> ?k) else ?A \<inter> ?k)
    5.19 -*)
    5.20 -
    5.21 -
    5.22  theory AllocImpl = ClientImpl:
    5.23  
    5.24  consts
    5.25 @@ -34,10 +19,10 @@
    5.26    "available_tok" == "Var([succ(succ(2))])"
    5.27  
    5.28  axioms
    5.29 -  alloc_type_assumes:
    5.30 +  alloc_type_assumes [simp]:
    5.31    "type_of(NbR) = nat & type_of(available_tok)=nat"
    5.32  
    5.33 -  alloc_default_val_assumes:
    5.34 +  alloc_default_val_assumes [simp]:
    5.35    "default_val(NbR)  = 0 & default_val(available_tok)=0"
    5.36  
    5.37  constdefs
    5.38 @@ -67,25 +52,20 @@
    5.39  		        preserves(lift(giv)). Acts(G))"
    5.40  
    5.41  
    5.42 -declare alloc_type_assumes [simp] alloc_default_val_assumes [simp]
    5.43 -
    5.44  lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat"
    5.45  apply (unfold state_def)
    5.46 -apply (drule_tac a = "available_tok" in apply_type)
    5.47 -apply auto
    5.48 +apply (drule_tac a = available_tok in apply_type, auto)
    5.49  done
    5.50  
    5.51  lemma NbR_value_type [simp,TC]: "s\<in>state ==> s`NbR \<in> nat"
    5.52  apply (unfold state_def)
    5.53 -apply (drule_tac a = "NbR" in apply_type)
    5.54 -apply auto
    5.55 +apply (drule_tac a = NbR in apply_type, auto)
    5.56  done
    5.57  
    5.58  (** The Alloc Program **)
    5.59  
    5.60  lemma alloc_prog_type [simp,TC]: "alloc_prog \<in> program"
    5.61 -apply (simp add: alloc_prog_def)
    5.62 -done
    5.63 +by (simp add: alloc_prog_def)
    5.64  
    5.65  declare alloc_prog_def [THEN def_prg_Init, simp]
    5.66  declare alloc_prog_def [THEN def_prg_AllowedActs, simp]
    5.67 @@ -107,11 +87,9 @@
    5.68  
    5.69  lemma alloc_prog_preserves:
    5.70      "alloc_prog \<in> (\<Inter>x \<in> var-{giv, available_tok, NbR}. preserves(lift(x)))"
    5.71 -apply (rule Inter_var_DiffI)
    5.72 -apply (force );
    5.73 +apply (rule Inter_var_DiffI, force)
    5.74  apply (rule ballI)
    5.75 -apply (rule preservesI)
    5.76 -apply (constrains)
    5.77 +apply (rule preservesI, constrains)
    5.78  done
    5.79  
    5.80  (* As a special case of the rule above *)
    5.81 @@ -121,10 +99,9 @@
    5.82         preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))"
    5.83  apply auto
    5.84  apply (insert alloc_prog_preserves)
    5.85 -apply (drule_tac [3] x = "tok" in Inter_var_DiffD)
    5.86 -apply (drule_tac [2] x = "ask" in Inter_var_DiffD)
    5.87 -apply (drule_tac x = "rel" in Inter_var_DiffD)
    5.88 -apply auto
    5.89 +apply (drule_tac [3] x = tok in Inter_var_DiffD)
    5.90 +apply (drule_tac [2] x = ask in Inter_var_DiffD)
    5.91 +apply (drule_tac x = rel in Inter_var_DiffD, auto)
    5.92  done
    5.93  
    5.94  lemma alloc_prog_Allowed:
    5.95 @@ -152,8 +129,7 @@
    5.96  
    5.97  (** Safety property: (28) **)
    5.98  lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))"
    5.99 -apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed)
   5.100 -apply constrains+
   5.101 +apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed, constrains+)
   5.102  apply (auto dest: ActsD)
   5.103  apply (drule_tac f = "lift (giv) " in preserves_imp_eq)
   5.104  apply auto
   5.105 @@ -163,7 +139,7 @@
   5.106  "alloc_prog \<in> stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
   5.107                       {s\<in>state. s`available_tok #+ tokens(s`giv) =
   5.108                                   NbT #+ tokens(take(s`NbR, s`rel))})"
   5.109 -apply (constrains)
   5.110 +apply constrains
   5.111  apply auto
   5.112  apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse)
   5.113  apply (simp (no_asm_simp) add: take_succ)
   5.114 @@ -180,13 +156,13 @@
   5.115  apply (subgoal_tac "G \<in> preserves (fun_pair (lift (available_tok), fun_pair (lift (NbR), lift (giv))))")
   5.116  apply (rotate_tac -1)
   5.117  apply (cut_tac A = "nat * nat * list(nat)"
   5.118 -             and P = "%<m,n,l> y. n \<le> length(y) & 
   5.119 +             and P = "%<m,n,l> y. n \<le> length(y) &
   5.120                                    m #+ tokens(l) = NbT #+ tokens(take(n,y))"
   5.121 -             and g = "lift(rel)" and F = "alloc_prog"
   5.122 +             and g = "lift(rel)" and F = alloc_prog
   5.123         in stable_Join_Stable)
   5.124 -prefer 3 apply assumption;
   5.125 +prefer 3 apply assumption
   5.126  apply (auto simp add: Collect_conj_eq)
   5.127 -apply (frule_tac g = "length" in imp_Increasing_comp)
   5.128 +apply (frule_tac g = length in imp_Increasing_comp)
   5.129  apply (blast intro: mono_length)
   5.130  apply (auto simp add: refl_prefix)
   5.131  apply (drule_tac a=xa and f = "length comp lift(rel)" in Increasing_imp_Stable)
   5.132 @@ -200,11 +176,9 @@
   5.133  apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl)
   5.134  apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable)
   5.135  apply (auto simp add: Stable_def Constrains_def constrains_def)
   5.136 -apply (drule bspec)
   5.137 -apply force
   5.138 +apply (drule bspec, force)
   5.139  apply (drule subsetD)
   5.140 -apply (rule imageI)
   5.141 -apply assumption
   5.142 +apply (rule imageI, assumption)
   5.143  apply (auto simp add: prefix_take_iff)
   5.144  apply (rotate_tac -1)
   5.145  apply (erule ssubst)
   5.146 @@ -219,9 +193,8 @@
   5.147  apply (auto simp add: guar_def)
   5.148  apply (rule Always_weaken)
   5.149  apply (rule AlwaysI)
   5.150 -apply (rule_tac [2] giv_Bounded_lemma2)
   5.151 -apply auto
   5.152 -apply (rule_tac j = "NbT #+ tokens (take (x` NbR, x`rel))" in le_trans)
   5.153 +apply (rule_tac [2] giv_Bounded_lemma2, auto)
   5.154 +apply (rule_tac j = "NbT #+ tokens(take (x` NbR, x`rel))" in le_trans)
   5.155  apply (erule subst)
   5.156  apply (auto intro!: tokens_mono simp add: prefix_take_iff min_def length_take)
   5.157  done
   5.158 @@ -234,105 +207,96 @@
   5.159  apply (auto intro!: AlwaysI simp add: guar_def)
   5.160  apply (subgoal_tac "G \<in> preserves (lift (giv))")
   5.161   prefer 2 apply (simp add: alloc_prog_ok_iff)
   5.162 -apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)" 
   5.163 +apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)"
   5.164         in stable_Join_Stable)
   5.165 -apply (constrains)
   5.166 - prefer 2 apply (simp add: lift_def); 
   5.167 - apply (clarify ); 
   5.168 -apply (drule_tac a = "k" in Increasing_imp_Stable)
   5.169 -apply auto
   5.170 +apply constrains
   5.171 + prefer 2 apply (simp add: lift_def, clarify)
   5.172 +apply (drule_tac a = k in Increasing_imp_Stable, auto)
   5.173  done
   5.174  
   5.175 -(**** Towards proving the liveness property, (31) ****)
   5.176 +subsection{* Towards proving the liveness property, (31) *}
   5.177  
   5.178 -(*** First, we lead up to a proof of Lemma 49, page 28. ***)
   5.179 +subsubsection{*First, we lead up to a proof of Lemma 49, page 28.*}
   5.180  
   5.181  lemma alloc_prog_transient_lemma:
   5.182 -"G \<in> program ==> \<forall>k\<in>nat. alloc_prog Join G \<in>
   5.183 -                   transient({s\<in>state. k \<le> length(s`rel)}
   5.184 -                   \<inter> {s\<in>state. succ(s`NbR) = k})"
   5.185 +     "[|G \<in> program; k\<in>nat|]
   5.186 +      ==> alloc_prog Join G \<in>
   5.187 +             transient({s\<in>state. k \<le> length(s`rel)} \<inter>
   5.188 +             {s\<in>state. succ(s`NbR) = k})"
   5.189  apply auto
   5.190  apply (erule_tac V = "G\<notin>?u" in thin_rl)
   5.191 -apply (rule_tac act = "alloc_rel_act" in transientI)
   5.192 +apply (rule_tac act = alloc_rel_act in transientI)
   5.193  apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts])
   5.194  apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset])
   5.195  apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
   5.196  apply (rule ReplaceI)
   5.197  apply (rule_tac x = "x (available_tok:= x`available_tok #+ nth (x`NbR, x`rel),
   5.198 -                        NbR:=succ (x`NbR))" 
   5.199 +                        NbR:=succ (x`NbR))"
   5.200         in exI)
   5.201  apply (auto intro!: state_update_type)
   5.202  done
   5.203  
   5.204  lemma alloc_prog_rel_Stable_NbR_lemma:
   5.205 -"[| G \<in> program; alloc_prog ok G; k\<in>nat |] ==>
   5.206 -    alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
   5.207 -apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff)
   5.208 -apply constrains
   5.209 -apply auto
   5.210 +    "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
   5.211 +     ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
   5.212 +apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains, auto)
   5.213  apply (blast intro: le_trans leI)
   5.214 -apply (drule_tac f = "lift (NbR)" and A = "nat" in preserves_imp_increasing)
   5.215 -apply (drule_tac [2] g = "succ" in imp_increasing_comp)
   5.216 +apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing)
   5.217 +apply (drule_tac [2] g = succ in imp_increasing_comp)
   5.218  apply (rule_tac [2] mono_succ)
   5.219 -apply (drule_tac [4] x = "k" in increasing_imp_stable)
   5.220 -    prefer 5 apply (simp add: Le_def comp_def) 
   5.221 -apply auto
   5.222 +apply (drule_tac [4] x = k in increasing_imp_stable)
   5.223 +    prefer 5 apply (simp add: Le_def comp_def, auto)
   5.224  done
   5.225  
   5.226 -lemma alloc_prog_NbR_LeadsTo_lemma [rule_format (no_asm)]:
   5.227 -"[| G \<in> program; alloc_prog ok G;
   5.228 -    alloc_prog Join G \<in> Incr(lift(rel)) |] ==>
   5.229 -     \<forall>k\<in>nat. alloc_prog Join G \<in>
   5.230 -       {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
   5.231 -       LeadsTo {s\<in>state. k \<le> s`NbR}"
   5.232 -apply clarify
   5.233 -apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
   5.234 -apply (drule_tac [2] a = "k" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
   5.235 +lemma alloc_prog_NbR_LeadsTo_lemma:
   5.236 +     "[| G \<in> program; alloc_prog ok G;
   5.237 +	 alloc_prog Join G \<in> Incr(lift(rel)); k\<in>nat |]
   5.238 +      ==> alloc_prog Join G \<in>
   5.239 +	    {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
   5.240 +	    LeadsTo {s\<in>state. k \<le> s`NbR}"
   5.241 +apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})")
   5.242 +apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
   5.243  apply (rule_tac [2] mono_length)
   5.244 -    prefer 3 apply (simp add: ); 
   5.245 +    prefer 3 apply simp
   5.246  apply (simp_all add: refl_prefix Le_def comp_def length_type)
   5.247  apply (rule LeadsTo_weaken)
   5.248  apply (rule PSP_Stable)
   5.249 -prefer 2 apply (assumption)
   5.250 +prefer 2 apply assumption
   5.251  apply (rule PSP_Stable)
   5.252  apply (rule_tac [2] alloc_prog_rel_Stable_NbR_lemma)
   5.253 -apply (rule alloc_prog_transient_lemma [THEN bspec, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo])
   5.254 -apply assumption+
   5.255 +apply (rule alloc_prog_transient_lemma [THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo], assumption+)
   5.256  apply (auto dest: not_lt_imp_le elim: lt_asym simp add: le_iff)
   5.257  done
   5.258  
   5.259  lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]:
   5.260 -    "[| G :program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel)) |]
   5.261 -      ==> \<forall>k\<in>nat. \<forall>n \<in> nat. n < k -->
   5.262 -       alloc_prog Join G \<in>
   5.263 -       {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
   5.264 -	  LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
   5.265 -	    (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
   5.266 +    "[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
   5.267 +        k\<in>nat; n \<in> nat; n < k |]
   5.268 +      ==> alloc_prog Join G \<in>
   5.269 +	    {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
   5.270 +	       LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
   5.271 +		 (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
   5.272  apply (unfold greater_than_def)
   5.273 -apply clarify
   5.274 -apply (rule_tac A' = "{x \<in> state. k \<le> length (x`rel) } \<inter> {x \<in> state. n < x`NbR}" in LeadsTo_weaken_R)
   5.275 +apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
   5.276 +       in LeadsTo_weaken_R)
   5.277  apply safe
   5.278  apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
   5.279 -apply (drule_tac [2] a = "k" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
   5.280 +apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
   5.281  apply (rule_tac [2] mono_length)
   5.282 -    prefer 3 apply (simp add: ); 
   5.283 +    prefer 3 apply simp
   5.284  apply (simp_all add: refl_prefix Le_def comp_def length_type)
   5.285  apply (subst Int_commute)
   5.286  apply (rule_tac A = " ({s \<in> state . k \<le> length (s ` rel) } \<inter> {s\<in>state . s ` NbR = n}) \<inter> {s\<in>state. k \<le> length (s`rel) }" in LeadsTo_weaken_L)
   5.287 -apply (rule PSP_Stable)
   5.288 -apply safe
   5.289 +apply (rule PSP_Stable, safe)
   5.290  apply (rule_tac B = "{x \<in> state . n < length (x ` rel) } \<inter> {s\<in>state . s ` NbR = n}" in LeadsTo_Trans)
   5.291  apply (rule_tac [2] LeadsTo_weaken)
   5.292  apply (rule_tac [2] k = "succ (n)" in alloc_prog_NbR_LeadsTo_lemma)
   5.293 -apply (simp_all add: ) 
   5.294 -apply (rule subset_imp_LeadsTo)
   5.295 -apply auto
   5.296 +apply simp_all
   5.297 +apply (rule subset_imp_LeadsTo, auto)
   5.298  apply (blast intro: lt_trans2)
   5.299  done
   5.300  
   5.301 -lemma Collect_vimage_eq: "u\<in>nat ==> {<s, f(s)>. s \<in> state} -`` u = {s\<in>state. f(s) < u}"
   5.302 -apply (force simp add: lt_def)
   5.303 -done
   5.304 +lemma Collect_vimage_eq: "u\<in>nat ==> {<s,f(s)>. s \<in> A} -`` u = {s\<in>A. f(s) < u}"
   5.305 +by (force simp add: lt_def)
   5.306  
   5.307  (* Lemma 49, page 28 *)
   5.308  
   5.309 @@ -343,26 +307,22 @@
   5.310             {s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
   5.311  (* Proof by induction over the difference between k and n *)
   5.312  apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct)
   5.313 -apply (simp_all add: lam_def)
   5.314 -apply auto
   5.315 -apply (rule single_LeadsTo_I)
   5.316 -apply auto
   5.317 +apply (simp_all add: lam_def, auto)
   5.318 +apply (rule single_LeadsTo_I, auto)
   5.319  apply (simp (no_asm_simp) add: Collect_vimage_eq)
   5.320  apply (rename_tac "s0")
   5.321  apply (case_tac "s0`NbR < k")
   5.322 -apply (rule_tac [2] subset_imp_LeadsTo)
   5.323 -apply safe
   5.324 +apply (rule_tac [2] subset_imp_LeadsTo, safe)
   5.325  apply (auto dest!: not_lt_imp_le)
   5.326  apply (rule LeadsTo_weaken)
   5.327 -apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2)
   5.328 -apply safe
   5.329 -prefer 3 apply (assumption)
   5.330 +apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2, safe)
   5.331 +prefer 3 apply assumption
   5.332  apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
   5.333  apply (blast dest: lt_asym)
   5.334  apply (force dest: add_lt_elim2)
   5.335  done
   5.336  
   5.337 -(** Towards proving lemma 50, page 29 **)
   5.338 +subsubsection{*Towards proving lemma 50, page 29*}
   5.339  
   5.340  lemma alloc_prog_giv_Ensures_lemma:
   5.341  "[| G \<in> program; k\<in>nat; alloc_prog ok G;
   5.342 @@ -371,27 +331,23 @@
   5.343    {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   5.344    {s\<in>state.  k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k}
   5.345    Ensures {s\<in>state. ~ k <length(s`ask)} Un {s\<in>state. length(s`giv) \<noteq> k}"
   5.346 -apply (rule EnsuresI)
   5.347 -apply auto
   5.348 +apply (rule EnsuresI, auto)
   5.349  apply (erule_tac [2] V = "G\<notin>?u" in thin_rl)
   5.350 -apply (rule_tac [2] act = "alloc_giv_act" in transientI)
   5.351 +apply (rule_tac [2] act = alloc_giv_act in transientI)
   5.352   prefer 2
   5.353   apply (simp add: alloc_prog_def [THEN def_prg_Acts])
   5.354   apply (simp add: alloc_giv_act_def [THEN def_act_eq, THEN act_subset])
   5.355  apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
   5.356  apply (erule_tac [2] swap)
   5.357  apply (rule_tac [2] ReplaceI)
   5.358 -apply (rule_tac [2] x = "x (giv := x ` giv @ [nth (length(x`giv), x ` ask) ], available_tok := x ` available_tok #- nth (length (x`giv), x ` ask))" in exI)
   5.359 +apply (rule_tac [2] x = "x (giv := x ` giv @ [nth (length(x`giv), x ` ask) ], available_tok := x ` available_tok #- nth (length(x`giv), x ` ask))" in exI)
   5.360  apply (auto intro!: state_update_type simp add: app_type)
   5.361 -apply (rule_tac A = "{s\<in>state . nth (length (s ` giv), s ` ask) \<le> s ` available_tok} \<inter> {s\<in>state . k < length (s ` ask) } \<inter> {s\<in>state. length (s`giv) =k}" and A' = "{s\<in>state . nth (length (s ` giv), s ` ask) \<le> s ` available_tok} Un {s\<in>state. ~ k < length (s`ask) } Un {s\<in>state . length (s ` giv) \<noteq> k}" in Constrains_weaken)
   5.362 -apply safe
   5.363 -apply (auto dest: ActsD simp add: Constrains_def constrains_def length_app alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff)
   5.364 -apply (subgoal_tac "length (xa ` giv @ [nth (length (xa ` giv), xa ` ask) ]) = length (xa ` giv) #+ 1")
   5.365 +apply (rule_tac A = "{s\<in>state . nth (length(s ` giv), s ` ask) \<le> s ` available_tok} \<inter> {s\<in>state . k < length(s ` ask) } \<inter> {s\<in>state. length(s`giv) =k}" and A' = "{s\<in>state . nth (length(s ` giv), s ` ask) \<le> s ` available_tok} Un {s\<in>state. ~ k < length(s`ask) } Un {s\<in>state . length(s ` giv) \<noteq> k}" in Constrains_weaken)
   5.366 +apply (auto dest: ActsD simp add: Constrains_def constrains_def alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff)
   5.367 +apply (subgoal_tac "length(xa ` giv @ [nth (length(xa ` giv), xa ` ask) ]) = length(xa ` giv) #+ 1")
   5.368  apply (rule_tac [2] trans)
   5.369 -apply (rule_tac [2] length_app)
   5.370 -apply auto
   5.371 -apply (rule_tac j = "xa ` available_tok" in le_trans)
   5.372 -apply auto
   5.373 +apply (rule_tac [2] length_app, auto)
   5.374 +apply (rule_tac j = "xa ` available_tok" in le_trans, auto)
   5.375  apply (drule_tac f = "lift (available_tok)" in preserves_imp_eq)
   5.376  apply assumption+
   5.377  apply auto
   5.378 @@ -399,19 +355,17 @@
   5.379         in Increasing_imp_Stable)
   5.380  apply (auto simp add: prefix_iff)
   5.381  apply (drule StableD)
   5.382 -apply (auto simp add: Constrains_def constrains_def)
   5.383 -apply force
   5.384 +apply (auto simp add: Constrains_def constrains_def, force)
   5.385  done
   5.386  
   5.387  lemma alloc_prog_giv_Stable_lemma:
   5.388  "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
   5.389    ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
   5.390 -apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff)
   5.391 -apply (constrains)
   5.392 -apply (auto intro: leI simp add: length_app)
   5.393 -apply (drule_tac f = "lift (giv)" and g = "length" in imp_preserves_comp)
   5.394 -apply (drule_tac f = "length comp lift (giv)" and A = "nat" and r = "Le" in preserves_imp_increasing)
   5.395 -apply (drule_tac [2] x = "k" in increasing_imp_stable)
   5.396 +apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains)
   5.397 +apply (auto intro: leI)
   5.398 +apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp)
   5.399 +apply (drule_tac f = "length comp lift (giv)" and A = nat and r = Le in preserves_imp_increasing)
   5.400 +apply (drule_tac [2] x = k in increasing_imp_stable)
   5.401   prefer 3 apply (simp add: Le_def comp_def)
   5.402  apply (auto simp add: length_type)
   5.403  done
   5.404 @@ -420,24 +374,23 @@
   5.405  
   5.406  lemma alloc_prog_giv_LeadsTo_lemma:
   5.407  "[| G \<in> program; alloc_prog ok G;
   5.408 -    alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |] ==>
   5.409 -  alloc_prog Join G \<in>
   5.410 -    {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   5.411 -    {s\<in>state.  k < length(s`ask)} \<inter>
   5.412 -    {s\<in>state. length(s`giv) = k}
   5.413 -    LeadsTo {s\<in>state. k < length(s`giv)}"
   5.414 -apply (subgoal_tac "alloc_prog Join G \<in> {s\<in>state. nth (length (s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length (s`ask) } \<inter> {s\<in>state. length (s`giv) = k} LeadsTo {s\<in>state. ~ k <length (s`ask) } Un {s\<in>state. length (s`giv) \<noteq> k}")
   5.415 +    alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |]
   5.416 + ==> alloc_prog Join G \<in>
   5.417 +	{s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   5.418 +	{s\<in>state.  k < length(s`ask)} \<inter>
   5.419 +	{s\<in>state. length(s`giv) = k}
   5.420 +	LeadsTo {s\<in>state. k < length(s`giv)}"
   5.421 +apply (subgoal_tac "alloc_prog Join G \<in> {s\<in>state. nth (length(s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length(s`ask) } \<inter> {s\<in>state. length(s`giv) = k} LeadsTo {s\<in>state. ~ k <length(s`ask) } Un {s\<in>state. length(s`giv) \<noteq> k}")
   5.422  prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis])
   5.423 -apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k < length (s`ask) }) ")
   5.424 -apply (drule PSP_Stable)
   5.425 -apply assumption
   5.426 +apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
   5.427 +apply (drule PSP_Stable, assumption)
   5.428  apply (rule LeadsTo_weaken)
   5.429  apply (rule PSP_Stable)
   5.430 -apply (rule_tac [2] k = "k" in alloc_prog_giv_Stable_lemma)
   5.431 +apply (rule_tac [2] k = k in alloc_prog_giv_Stable_lemma)
   5.432  apply (auto simp add: le_iff)
   5.433 -apply (drule_tac a = "succ (k)" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
   5.434 +apply (drule_tac a = "succ (k)" and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
   5.435  apply (rule mono_length)
   5.436 - prefer 2 apply (simp add: ); 
   5.437 + prefer 2 apply simp
   5.438  apply (simp_all add: refl_prefix Le_def comp_def length_type)
   5.439  done
   5.440  
   5.441 @@ -452,69 +405,72 @@
   5.442    ==> alloc_prog Join G \<in>
   5.443          Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) -->
   5.444                  NbT \<le> s`available_tok})"
   5.445 -apply (subgoal_tac "alloc_prog Join G \<in> Always ({s\<in>state. s`NbR \<le> length (s`rel) } \<inter> {s\<in>state. s`available_tok #+ tokens (s`giv) = NbT #+ tokens (take (s`NbR, s`rel))}) ")
   5.446 +apply (subgoal_tac "alloc_prog Join G \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter> {s\<in>state. s`available_tok #+ tokens(s`giv) = NbT #+ tokens(take (s`NbR, s`rel))}) ")
   5.447  apply (rule_tac [2] AlwaysI)
   5.448 -apply (rule_tac [3] giv_Bounded_lemma2)
   5.449 -apply auto
   5.450 -apply (rule Always_weaken)
   5.451 -apply assumption
   5.452 -apply auto
   5.453 -apply (subgoal_tac "0 \<le> tokens (take (x ` NbR, x ` rel)) #- tokens (x`giv) ")
   5.454 +apply (rule_tac [3] giv_Bounded_lemma2, auto)
   5.455 +apply (rule Always_weaken, assumption, auto)
   5.456 +apply (subgoal_tac "0 \<le> tokens(take (x ` NbR, x ` rel)) #- tokens(x`giv) ")
   5.457  apply (rule_tac [2] nat_diff_split [THEN iffD2])
   5.458 - prefer 2 apply (force ); 
   5.459 + prefer 2 apply force
   5.460  apply (subgoal_tac "x`available_tok =
   5.461 -                    NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens (x`giv))")
   5.462 +                    NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
   5.463  apply (simp (no_asm_simp))
   5.464 -apply (rule nat_diff_split [THEN iffD2])
   5.465 -apply auto
   5.466 -apply (drule_tac j = "tokens (x ` giv)" in lt_trans2)
   5.467 +apply (rule nat_diff_split [THEN iffD2], auto)
   5.468 +apply (drule_tac j = "tokens(x ` giv)" in lt_trans2)
   5.469  apply assumption
   5.470  apply auto
   5.471  done
   5.472  
   5.473 -(* Main lemmas towards proving property (31) *)
   5.474 +subsubsection{* Main lemmas towards proving property (31)*}
   5.475  
   5.476  lemma LeadsTo_strength_R:
   5.477      "[|  F \<in> C LeadsTo B'; F \<in> A-C LeadsTo B; B'<=B |] ==> F \<in> A LeadsTo  B"
   5.478 -by (blast intro: LeadsTo_weaken LeadsTo_Un_Un) 
   5.479 +by (blast intro: LeadsTo_weaken LeadsTo_Un_Un)
   5.480  
   5.481  lemma PSP_StableI:
   5.482  "[| F \<in> Stable(C); F \<in> A - C LeadsTo B;
   5.483     F \<in> A \<inter> C LeadsTo B Un (state - C) |] ==> F \<in> A LeadsTo  B"
   5.484  apply (rule_tac A = " (A-C) Un (A \<inter> C)" in LeadsTo_weaken_L)
   5.485 - prefer 2 apply (blast)
   5.486 -apply (rule LeadsTo_Un)
   5.487 -apply assumption
   5.488 -apply (blast intro: LeadsTo_weaken dest: PSP_Stable) 
   5.489 + prefer 2 apply blast
   5.490 +apply (rule LeadsTo_Un, assumption)
   5.491 +apply (blast intro: LeadsTo_weaken dest: PSP_Stable)
   5.492  done
   5.493  
   5.494  lemma state_compl_eq [simp]: "state - {s\<in>state. P(s)} = {s\<in>state. ~P(s)}"
   5.495 -apply auto
   5.496 -done
   5.497 +by auto
   5.498  
   5.499  (*needed?*)
   5.500  lemma single_state_Diff_eq [simp]: "{s}-{x \<in> state. P(x)} = (if s\<in>state & P(s) then 0 else {s})"
   5.501 -apply auto
   5.502 -done
   5.503 +by auto
   5.504 +
   5.505  
   5.506 +locale alloc_progress =
   5.507 + fixes G
   5.508 + assumes Gprog [intro,simp]: "G \<in> program"
   5.509 +     and okG [iff]:          "alloc_prog ok G"
   5.510 +     and Incr_rel [intro]:   "alloc_prog Join G \<in> Incr(lift(rel))"
   5.511 +     and Incr_ask [intro]:   "alloc_prog Join G \<in> Incr(lift(ask))"
   5.512 +     and safety:   "alloc_prog Join G
   5.513 +                      \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT})"
   5.514 +     and progress: "alloc_prog Join G
   5.515 +                      \<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
   5.516 +                        {s\<in>state. k \<le> tokens(s`rel)})"
   5.517  
   5.518  (*First step in proof of (31) -- the corrected version from Charpentier.
   5.519    This lemma implies that if a client releases some tokens then the Allocator
   5.520    will eventually recognize that they've been released.*)
   5.521 -lemma alloc_prog_LeadsTo_tokens_take_NbR_lemma:
   5.522 -"[| alloc_prog Join G \<in> Incr(lift(rel));
   5.523 -    G \<in> program; alloc_prog ok G; k \<in> tokbag |]
   5.524 +lemma (in alloc_progress) tokens_take_NbR_lemma:
   5.525 + "k \<in> tokbag
   5.526    ==> alloc_prog Join G \<in>
   5.527          {s\<in>state. k \<le> tokens(s`rel)}
   5.528          LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   5.529 -apply (rule single_LeadsTo_I)
   5.530 -apply safe
   5.531 +apply (rule single_LeadsTo_I, safe)
   5.532  apply (rule_tac a1 = "s`rel" in Increasing_imp_Stable [THEN PSP_StableI])
   5.533 -apply (rule_tac [4] k1 = "length (s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R])
   5.534 +apply (rule_tac [4] k1 = "length(s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R])
   5.535  apply (rule_tac [8] subset_imp_LeadsTo)
   5.536 -apply auto
   5.537 -apply (rule_tac j = "tokens (take (length (s`rel), x`rel))" in le_trans)
   5.538 -apply (rule_tac j = "tokens (take (length (s`rel), s`rel))" in le_trans)
   5.539 +apply (auto intro!: Incr_rel)
   5.540 +apply (rule_tac j = "tokens(take (length(s`rel), x`rel))" in le_trans)
   5.541 +apply (rule_tac j = "tokens(take (length(s`rel), s`rel))" in le_trans)
   5.542  apply (auto intro!: tokens_mono take_mono simp add: prefix_iff)
   5.543  done
   5.544  
   5.545 @@ -522,256 +478,184 @@
   5.546  
   5.547  (*Second step in proof of (31): by LHS of the guarantee and transivity of
   5.548    LeadsTo *)
   5.549 -lemma alloc_prog_LeadsTo_tokens_take_NbR_lemma2:
   5.550 -"[| alloc_prog Join G \<in> Incr(lift(rel));
   5.551 -    G \<in> program; alloc_prog ok G; k \<in> tokbag;
   5.552 -    alloc_prog Join G \<in>
   5.553 -       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   5.554 -  ==> alloc_prog Join G \<in>
   5.555 -        {s\<in>state. tokens(s`giv) = k}
   5.556 -        LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   5.557 +lemma (in alloc_progress) tokens_take_NbR_lemma2:
   5.558 +     "k \<in> tokbag
   5.559 +      ==> alloc_prog Join G \<in>
   5.560 +	    {s\<in>state. tokens(s`giv) = k}
   5.561 +	    LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   5.562  apply (rule LeadsTo_Trans)
   5.563 -apply (rule_tac [2] alloc_prog_LeadsTo_tokens_take_NbR_lemma)
   5.564 -apply (blast intro: LeadsTo_weaken_L nat_into_Ord)
   5.565 -apply assumption+
   5.566 + apply (rule_tac [2] tokens_take_NbR_lemma)
   5.567 + prefer 2 apply assumption
   5.568 +apply (insert progress) 
   5.569 +apply (blast intro: LeadsTo_weaken_L progress nat_into_Ord)
   5.570  done
   5.571  
   5.572  (*Third step in proof of (31): by PSP with the fact that giv increases *)
   5.573 -lemma alloc_prog_LeadsTo_length_giv_disj:
   5.574 -"[| alloc_prog Join G \<in> Incr(lift(rel));
   5.575 -    G \<in> program; alloc_prog ok G; k \<in> tokbag; n \<in> nat;
   5.576 -    alloc_prog Join G \<in>
   5.577 -       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   5.578 -  ==> alloc_prog Join G \<in>
   5.579 -        {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   5.580 -        LeadsTo
   5.581 -          {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
   5.582 -                     k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}"
   5.583 -apply (rule single_LeadsTo_I)
   5.584 -apply safe
   5.585 +lemma (in alloc_progress) length_giv_disj:
   5.586 +     "[| k \<in> tokbag; n \<in> nat |]
   5.587 +      ==> alloc_prog Join G \<in>
   5.588 +	    {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   5.589 +	    LeadsTo
   5.590 +	      {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
   5.591 +			 k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}"
   5.592 +apply (rule single_LeadsTo_I, safe)
   5.593  apply (rule_tac a1 = "s`giv" in Increasing_imp_Stable [THEN PSP_StableI])
   5.594  apply (rule alloc_prog_Increasing_giv [THEN guaranteesD])
   5.595  apply (simp_all add: Int_cons_left)
   5.596  apply (rule LeadsTo_weaken)
   5.597 -apply (rule_tac k = "tokens (s`giv)" in alloc_prog_LeadsTo_tokens_take_NbR_lemma2)
   5.598 -apply simp_all
   5.599 -apply safe
   5.600 -apply (drule prefix_length_le [THEN le_iff [THEN iffD1]]) 
   5.601 -apply (force simp add:)
   5.602 +apply (rule_tac k = "tokens(s`giv)" in tokens_take_NbR_lemma2)
   5.603 +apply auto
   5.604 +apply (force dest: prefix_length_le [THEN le_iff [THEN iffD1]]) 
   5.605  apply (simp add: not_lt_iff_le)
   5.606 -apply (drule prefix_length_le_equal)
   5.607 -apply assumption
   5.608 -apply (simp add:)
   5.609 +apply (force dest: prefix_length_le_equal) 
   5.610  done
   5.611  
   5.612  (*Fourth step in proof of (31): we apply lemma (51) *)
   5.613 -lemma alloc_prog_LeadsTo_length_giv_disj2:
   5.614 -"[| alloc_prog Join G \<in> Incr(lift(rel));
   5.615 -    alloc_prog Join G \<in> Incr(lift(ask));
   5.616 -    G \<in> program; alloc_prog ok G; k \<in> tokbag; n \<in> nat;
   5.617 -    alloc_prog Join G \<in>
   5.618 -       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   5.619 -  ==> alloc_prog Join G \<in>
   5.620 -        {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   5.621 -        LeadsTo
   5.622 -          {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   5.623 -                    n < length(s`giv)}"
   5.624 +lemma (in alloc_progress) length_giv_disj2:
   5.625 +     "[|k \<in> tokbag; n \<in> nat|]
   5.626 +      ==> alloc_prog Join G \<in>
   5.627 +	    {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   5.628 +	    LeadsTo
   5.629 +	      {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   5.630 +			n < length(s`giv)}"
   5.631  apply (rule LeadsTo_weaken_R)
   5.632 -apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma alloc_prog_LeadsTo_length_giv_disj])
   5.633 -apply auto
   5.634 +apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma length_giv_disj], auto)
   5.635  done
   5.636  
   5.637  (*Fifth step in proof of (31): from the fourth step, taking the union over all
   5.638    k\<in>nat *)
   5.639 -lemma alloc_prog_LeadsTo_length_giv_disj3:
   5.640 -"[| alloc_prog Join G \<in> Incr(lift(rel));
   5.641 -    alloc_prog Join G \<in> Incr(lift(ask));
   5.642 -    G \<in> program; alloc_prog ok G;  n \<in> nat;
   5.643 -    alloc_prog Join G \<in>
   5.644 -       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   5.645 -  ==> alloc_prog Join G \<in>
   5.646 -        {s\<in>state. length(s`giv) = n}
   5.647 -        LeadsTo
   5.648 -          {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   5.649 -                    n < length(s`giv)}"
   5.650 +lemma (in alloc_progress) length_giv_disj3:
   5.651 +     "n \<in> nat
   5.652 +      ==> alloc_prog Join G \<in>
   5.653 +	    {s\<in>state. length(s`giv) = n}
   5.654 +	    LeadsTo
   5.655 +	      {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   5.656 +			n < length(s`giv)}"
   5.657  apply (rule LeadsTo_weaken_L)
   5.658 -apply (rule_tac I = "nat" in LeadsTo_UN)
   5.659 -apply (rule_tac k = "i" in alloc_prog_LeadsTo_length_giv_disj2)
   5.660 +apply (rule_tac I = nat in LeadsTo_UN)
   5.661 +apply (rule_tac k = i in length_giv_disj2)
   5.662  apply (simp_all add: UN_conj_eq)
   5.663  done
   5.664  
   5.665  (*Sixth step in proof of (31): from the fifth step, by PSP with the
   5.666    assumption that ask increases *)
   5.667 -lemma alloc_prog_LeadsTo_length_ask_giv:
   5.668 -"[| alloc_prog Join G \<in> Incr(lift(rel));
   5.669 -    alloc_prog Join G \<in> Incr(lift(ask));
   5.670 -    G \<in> program; alloc_prog ok G;  k \<in> nat;  n < k;
   5.671 -    alloc_prog Join G \<in>
   5.672 -       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   5.673 +lemma (in alloc_progress) length_ask_giv:
   5.674 + "[|k \<in> nat;  n < k|]
   5.675    ==> alloc_prog Join G \<in>
   5.676          {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   5.677          LeadsTo
   5.678            {s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
   5.679                       length(s`giv) = n) |
   5.680                      n < length(s`giv)}"
   5.681 -apply (rule single_LeadsTo_I)
   5.682 -apply safe
   5.683 -apply (rule_tac a1 = "s`ask" and f1 = "lift (ask)" in Increasing_imp_Stable [THEN PSP_StableI])
   5.684 -apply assumption
   5.685 -apply simp_all
   5.686 +apply (rule single_LeadsTo_I, safe)
   5.687 +apply (rule_tac a1 = "s`ask" and f1 = "lift(ask)" 
   5.688 +       in Increasing_imp_Stable [THEN PSP_StableI])
   5.689 +apply (rule Incr_ask, simp_all)
   5.690  apply (rule LeadsTo_weaken)
   5.691 -apply (rule_tac n = "length (s ` giv)" in alloc_prog_LeadsTo_length_giv_disj3)
   5.692 +apply (rule_tac n = "length(s ` giv)" in length_giv_disj3)
   5.693  apply simp_all
   5.694 -apply (blast intro:)
   5.695 +apply blast
   5.696  apply clarify
   5.697 -apply (simp add:)
   5.698 +apply simp
   5.699  apply (blast dest!: prefix_length_le intro: lt_trans2)
   5.700  done
   5.701  
   5.702  
   5.703  (*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
   5.704 -lemma alloc_prog_LeadsTo_length_ask_giv2:
   5.705 -"[| alloc_prog Join G \<in> Incr(lift(rel));
   5.706 -    alloc_prog Join G \<in> Incr(lift(ask));
   5.707 -    G \<in> program; alloc_prog ok G;  k \<in> nat;  n < k;
   5.708 -    alloc_prog Join G \<in>
   5.709 -      Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
   5.710 -    alloc_prog Join G \<in>
   5.711 -       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   5.712 -  ==> alloc_prog Join G \<in>
   5.713 -        {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   5.714 -        LeadsTo
   5.715 -          {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
   5.716 -                     length(s`giv) < length(s`ask) & length(s`giv) = n) |
   5.717 -                    n < length(s`giv)}"
   5.718 +lemma (in alloc_progress) length_ask_giv2:
   5.719 +     "[|k \<in> nat;  n < k|]
   5.720 +      ==> alloc_prog Join G \<in>
   5.721 +	    {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   5.722 +	    LeadsTo
   5.723 +	      {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
   5.724 +			 length(s`giv) < length(s`ask) & length(s`giv) = n) |
   5.725 +			n < length(s`giv)}"
   5.726  apply (rule LeadsTo_weaken_R)
   5.727 -apply (erule Always_LeadsToD [OF asm_rl alloc_prog_LeadsTo_length_ask_giv])
   5.728 -apply assumption+
   5.729 -apply clarify
   5.730 -apply (simp add: INT_iff)
   5.731 -apply clarify
   5.732 -apply (drule_tac x = "length (x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
   5.733 -apply (simp add:)
   5.734 +apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify)
   5.735 +apply (simp add: INT_iff, clarify)
   5.736 +apply (drule_tac x = "length(x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
   5.737 +apply simp
   5.738  apply (blast intro: le_trans)
   5.739  done
   5.740  
   5.741 -(*Eighth step in proof of (31): by (50), we get |giv| > n. *)
   5.742 -lemma alloc_prog_LeadsTo_extend_giv:
   5.743 -"[| alloc_prog Join G \<in> Incr(lift(rel));
   5.744 -    alloc_prog Join G \<in> Incr(lift(ask));
   5.745 -    G \<in> program; alloc_prog ok G;  k \<in> nat;  n < k;
   5.746 -    alloc_prog Join G \<in>
   5.747 -      Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
   5.748 -    alloc_prog Join G \<in>
   5.749 -       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   5.750 -  ==> alloc_prog Join G \<in>
   5.751 -        {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   5.752 -        LeadsTo {s\<in>state. n < length(s`giv)}"
   5.753 +(*Eighth step in proof of (31): by 50, we get |giv| > n. *)
   5.754 +lemma (in alloc_progress) extend_giv:
   5.755 +     "[| k \<in> nat;  n < k|]
   5.756 +      ==> alloc_prog Join G \<in>
   5.757 +	    {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   5.758 +	    LeadsTo {s\<in>state. n < length(s`giv)}"
   5.759  apply (rule LeadsTo_Un_duplicate)
   5.760  apply (rule LeadsTo_cancel1)
   5.761  apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma)
   5.762 -apply safe;
   5.763 - prefer 2 apply (simp add: lt_nat_in_nat)
   5.764 +apply (simp_all add: Incr_ask lt_nat_in_nat)
   5.765  apply (rule LeadsTo_weaken_R)
   5.766 -apply (rule alloc_prog_LeadsTo_length_ask_giv2)
   5.767 -apply auto
   5.768 +apply (rule length_ask_giv2, auto)
   5.769  done
   5.770  
   5.771 -(*Ninth and tenth steps in proof of (31): by (50), we get |giv| > n.
   5.772 +(*Ninth and tenth steps in proof of (31): by 50, we get |giv| > n.
   5.773    The report has an error: putting |ask|=k for the precondition fails because
   5.774    we can't expect |ask| to remain fixed until |giv| increases.*)
   5.775 -lemma alloc_prog_ask_LeadsTo_giv:
   5.776 -"[| alloc_prog Join G \<in> Incr(lift(rel));
   5.777 -    alloc_prog Join G \<in> Incr(lift(ask));
   5.778 -    G \<in> program; alloc_prog ok G;  k \<in> nat;
   5.779 -    alloc_prog Join G \<in>
   5.780 -      Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
   5.781 -    alloc_prog Join G \<in>
   5.782 -       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
   5.783 +lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
   5.784 + "k \<in> nat
   5.785    ==> alloc_prog Join G \<in>
   5.786          {s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
   5.787  (* Proof by induction over the difference between k and n *)
   5.788 -apply (rule_tac f = "\<lambda>s\<in>state. k #- length (s`giv)" in LessThan_induct)
   5.789 -apply (simp_all add: lam_def)
   5.790 - prefer 2 apply (force)
   5.791 -apply clarify
   5.792 -apply (simp add: Collect_vimage_eq)
   5.793 -apply (rule single_LeadsTo_I)
   5.794 -apply safe
   5.795 -apply simp
   5.796 +apply (rule_tac f = "\<lambda>s\<in>state. k #- length(s`giv)" in LessThan_induct)
   5.797 +apply (auto simp add: lam_def Collect_vimage_eq)
   5.798 +apply (rule single_LeadsTo_I, auto)
   5.799  apply (rename_tac "s0")
   5.800 -apply (case_tac "length (s0 ` giv) < length (s0 ` ask) ")
   5.801 +apply (case_tac "length(s0 ` giv) < length(s0 ` ask) ")
   5.802   apply (rule_tac [2] subset_imp_LeadsTo)
   5.803 -  apply safe
   5.804 - prefer 2 
   5.805 - apply (simp add: not_lt_iff_le)
   5.806 - apply (blast dest: le_imp_not_lt intro: lt_trans2)
   5.807 -apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)" 
   5.808 +  apply (auto simp add: not_lt_iff_le)
   5.809 + prefer 2 apply (blast dest: le_imp_not_lt intro: lt_trans2)
   5.810 +apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
   5.811         in Increasing_imp_Stable [THEN PSP_StableI])
   5.812 -apply assumption
   5.813 -apply (simp add:)
   5.814 -apply (force simp add:)
   5.815 +apply (rule Incr_ask, simp)
   5.816 +apply (force)
   5.817  apply (rule LeadsTo_weaken)
   5.818 -apply (rule_tac n = "length (s0 ` giv)" and k = "length (s0 ` ask)" 
   5.819 -       in alloc_prog_LeadsTo_extend_giv)
   5.820 -apply simp_all
   5.821 - apply (force simp add:)
   5.822 -apply clarify
   5.823 -apply (simp add:)
   5.824 -apply (erule disjE)
   5.825 - apply (blast dest!: prefix_length_le intro: lt_trans2)
   5.826 -apply (rule not_lt_imp_le)
   5.827 -apply clarify
   5.828 -apply (simp_all add: leI diff_lt_iff_lt)
   5.829 +apply (rule_tac n = "length(s0 ` giv)" and k = "length(s0 ` ask)"
   5.830 +       in extend_giv) 
   5.831 +apply (auto dest: not_lt_imp_le simp add: leI diff_lt_iff_lt) 
   5.832 +apply (blast dest!: prefix_length_le intro: lt_trans2)
   5.833  done
   5.834  
   5.835  (*Final lemma: combine previous result with lemma (30)*)
   5.836 -lemma alloc_prog_progress_lemma:
   5.837 -"[| alloc_prog Join G \<in> Incr(lift(rel));
   5.838 -    alloc_prog Join G \<in> Incr(lift(ask));
   5.839 -    G \<in> program; alloc_prog ok G;  h \<in> list(tokbag);
   5.840 -    alloc_prog Join G \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
   5.841 -    alloc_prog Join G \<in>
   5.842 -       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo 
   5.843 -                 {s\<in>state. k \<le> tokens(s`rel)}) |]
   5.844 -  ==> alloc_prog Join G \<in>
   5.845 -        {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
   5.846 -        {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
   5.847 +lemma (in alloc_progress) final:
   5.848 +     "h \<in> list(tokbag)
   5.849 +      ==> alloc_prog Join G \<in>
   5.850 +	    {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
   5.851 +	    {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
   5.852  apply (rule single_LeadsTo_I)
   5.853 - prefer 2 apply (simp)
   5.854 + prefer 2 apply simp
   5.855  apply (rename_tac s0)
   5.856 -apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)" 
   5.857 +apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
   5.858         in Increasing_imp_Stable [THEN PSP_StableI])
   5.859 -   apply assumption
   5.860 -  prefer 2 apply (force simp add:)
   5.861 -apply (simp_all add: Int_cons_left)
   5.862 +   apply (rule Incr_ask)
   5.863 +  apply (simp_all add: Int_cons_left)
   5.864  apply (rule LeadsTo_weaken)
   5.865 -apply (rule_tac k1 = "length (s0 ` ask)" 
   5.866 +apply (rule_tac k1 = "length(s0 ` ask)"
   5.867         in Always_LeadsToD [OF alloc_prog_ask_prefix_giv [THEN guaranteesD]
   5.868                                alloc_prog_ask_LeadsTo_giv])
   5.869 -apply simp_all
   5.870 -apply (force simp add:)
   5.871 -apply (force simp add:)
   5.872 -apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le lt_trans2)
   5.873 +apply (auto simp add: Incr_ask)
   5.874 +apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le 
   5.875 +                    lt_trans2)
   5.876  done
   5.877  
   5.878  (** alloc_prog liveness property (31), page 18 **)
   5.879  
   5.880 -(*missing the LeadsTo assumption on the lhs!?!?!*)
   5.881 -lemma alloc_prog_progress:
   5.882 +theorem alloc_prog_progress:
   5.883  "alloc_prog \<in>
   5.884      Incr(lift(ask)) \<inter> Incr(lift(rel)) \<inter>
   5.885      Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT}) \<inter>
   5.886 -    (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo 
   5.887 +    (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
   5.888                {s\<in>state. k \<le> tokens(s`rel)})
   5.889    guarantees (\<Inter>h \<in> list(tokbag).
   5.890                {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
   5.891                {s\<in>state. <h, s`giv> \<in> prefix(tokbag)})"
   5.892  apply (rule guaranteesI)
   5.893 -apply (rule INT_I)
   5.894 -apply (rule alloc_prog_progress_lemma)
   5.895 -apply simp_all
   5.896 -apply (blast intro:)
   5.897 +apply (rule INT_I [OF _ list.Nil])
   5.898 +apply (rule alloc_progress.final)
   5.899 +apply (simp_all add: alloc_progress_def)
   5.900  done
   5.901  
   5.902  
     6.1 --- a/src/ZF/UNITY/MultisetSum.ML	Tue Jun 24 10:42:34 2003 +0200
     6.2 +++ b/src/ZF/UNITY/MultisetSum.ML	Tue Jun 24 16:32:59 2003 +0200
     6.3 @@ -22,8 +22,8 @@
     6.4  by  (auto_tac (claset(), simpset() addsimps [Fin_into_Finite RS Finite_cons, 
     6.5                                               cons_absorb]));
     6.6  by (blast_tac (claset() addDs [Fin_into_Finite]) 2);
     6.7 -by (resolve_tac [fold_cons] 1);
     6.8 -by (auto_tac (claset(), simpset() addsimps [lcomm_def]));
     6.9 +by (resolve_tac [thm"fold_typing.fold_cons"] 1);
    6.10 +by (auto_tac (claset(), simpset() addsimps [thm "fold_typing_def", lcomm_def]));
    6.11  qed "general_setsum_cons";
    6.12  Addsimps [general_setsum_cons];
    6.13  
    6.14 @@ -185,8 +185,9 @@
    6.15  "[| Finite(C); x~:C |] \
    6.16  \  ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)";
    6.17  by (auto_tac (claset(), simpset() addsimps [Finite_cons]));
    6.18 -by (res_inst_tac [("A", "cons(x, C)")] fold_cons 1);
    6.19 -by (auto_tac (claset() addIs [Finite_cons_lemma], simpset()));
    6.20 +by (res_inst_tac [("A", "cons(x, C)")] (thm"fold_typing.fold_cons") 1);
    6.21 +by (auto_tac (claset() addIs [thm"Finite_cons_lemma"], 
    6.22 +              simpset() addsimps [thm "fold_typing_def"]));
    6.23  qed "nsetsum_cons";
    6.24  Addsimps [nsetsum_cons];
    6.25  
     7.1 --- a/src/ZF/UNITY/UNITYMisc.ML	Tue Jun 24 10:42:34 2003 +0200
     7.2 +++ b/src/ZF/UNITY/UNITYMisc.ML	Tue Jun 24 16:32:59 2003 +0200
     7.3 @@ -37,9 +37,10 @@
     7.4  by (assume_tac 1);
     7.5  qed "list_nat_into_univ";
     7.6  
     7.7 -(** To be moved to Update theory **)
     7.8  
     7.9 -(** Simplication rules for Collect; To be moved elsewhere **)
    7.10 +(** Simplication rules for Collect; ????
    7.11 +  At least change to "{x:A. P(x)} Int A = {x : A Int B. P(x)} **)
    7.12 +
    7.13  Goal "{x:A. P(x)} Int A = {x:A. P(x)}";
    7.14  by Auto_tac;
    7.15  qed "Collect_Int2";
    7.16 @@ -48,6 +49,7 @@
    7.17  by Auto_tac;
    7.18  qed "Collect_Int3";
    7.19  
    7.20 +(*????????????????*)
    7.21  AddIffs [Collect_Int2, Collect_Int3];
    7.22  
    7.23  
    7.24 @@ -65,15 +67,6 @@
    7.25  by (Blast_tac 1);
    7.26  qed "Int_Union2";
    7.27  
    7.28 -Goal "A Int cons(a, B) = (if a : A then cons(a, A Int B) else A Int B)";
    7.29 -by Auto_tac;
    7.30 -qed "Int_cons_right";
    7.31 -
    7.32  Goal "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)";
    7.33  by Auto_tac;
    7.34  qed "Int_succ_right";
    7.35 -
    7.36 -Goal "cons(a,B) Int A = (if a : A then cons(a, A Int B) else A Int B)";
    7.37 -by Auto_tac;
    7.38 -qed "Int_cons_left";
    7.39 -
     8.1 --- a/src/ZF/equalities.thy	Tue Jun 24 10:42:34 2003 +0200
     8.2 +++ b/src/ZF/equalities.thy	Tue Jun 24 16:32:59 2003 +0200
     8.3 @@ -136,6 +136,9 @@
     8.4  lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
     8.5  by blast
     8.6  
     8.7 +lemma Diff_cons_eq: "cons(a,B) - C = (if a\<in>C then B-C else cons(a,B-C))" 
     8.8 +by auto
     8.9 +
    8.10  lemma equal_singleton [rule_format]: "[| a: C;  \<forall>y\<in>C. y=b |] ==> C = {b}"
    8.11  by blast
    8.12  
    8.13 @@ -227,6 +230,14 @@
    8.14  lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B"
    8.15  by blast
    8.16  
    8.17 +lemma Int_cons_left:
    8.18 +     "cons(a,A) Int B = (if a : B then cons(a, A Int B) else A Int B)"
    8.19 +by auto
    8.20 +
    8.21 +lemma Int_cons_right:
    8.22 +     "A Int cons(a, B) = (if a : A then cons(a, A Int B) else A Int B)"
    8.23 +by auto
    8.24 +
    8.25  subsection{*Binary Union*}
    8.26  
    8.27  (** Union is the least upper bound of two sets *)
    8.28 @@ -1084,6 +1095,8 @@
    8.29  val subset_Int_iff = thm "subset_Int_iff";
    8.30  val subset_Int_iff2 = thm "subset_Int_iff2";
    8.31  val Int_Diff_eq = thm "Int_Diff_eq";
    8.32 +val Int_cons_left = thm "Int_cons_left";
    8.33 +val Int_cons_right = thm "Int_cons_right";
    8.34  val Un_cons = thm "Un_cons";
    8.35  val Un_absorb = thm "Un_absorb";
    8.36  val Un_left_absorb = thm "Un_left_absorb";