# HG changeset patch
# User paulson
# Date 1056465179 -7200
# Node ID 3738065456569b4692f9a1eef9d3b704da9afe58
# Parent  86c56794b6410fa4ac5e8f2804060a088e4a90cc
Converting ZF/UNITY to Isar

diff -r 86c56794b641 -r 373806545656 src/ZF/Induct/FoldSet.ML
--- a/src/ZF/Induct/FoldSet.ML	Tue Jun 24 10:42:34 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,464 +0,0 @@
-(*  Title:      ZF/Induct/FoldSet.thy
-    ID:         $Id$
-    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
-    Copyright   2001  University of Cambridge
-
-
-A "fold" functional for finite sets.  For n non-negative we have
-fold f e {x1,...,xn} = f x1 (... (f xn e)) where f is at
-least left-commutative.  
-*)
-
-(** foldSet **)
-
-bind_thm("empty_fold_setE", 
-             fold_set.mk_cases "<0, x> : fold_set(A, B, f,e)");
-bind_thm("cons_fold_setE", 
-             fold_set.mk_cases "<cons(x,C), y> : fold_set(A, B, f,e)");
-
-(* add-hoc lemmas *)
-
-Goal "[| x~:C; x~:B |] ==> cons(x,B)=cons(x,C) <-> B = C";
-by (auto_tac (claset() addEs [equalityE], simpset()));
-qed "cons_lemma1";
-
-Goal "[| cons(x, B)=cons(y, C); x~=y; x~:B; y~:C |] \
-\   ==>  B - {y} = C-{x} & x:C & y:B";
-by (auto_tac (claset() addEs [equalityE], simpset()));
-qed "cons_lemma2";
-
-(* fold_set monotonicity *)
-Goal "<C, x> : fold_set(A, B, f, e) \
-\     ==> ALL D. A<=D --> <C, x> : fold_set(D, B, f, e)";
-by (etac fold_set.induct 1);
-by (auto_tac (claset() addIs fold_set.intrs, simpset()));
-qed "fold_set_mono_lemma";
-
-Goal " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)";
-by (Clarify_tac 1);
-by (forward_tac [impOfSubs fold_set.dom_subset] 1);
-by (Clarify_tac 1);
-by (auto_tac (claset() addDs [fold_set_mono_lemma], simpset()));
-qed "fold_set_mono";
-
-Goal "<C, x>:fold_set(A, B, f, e) ==> <C, x>:fold_set(C, B, f, e) & C<=A";
-by (etac fold_set.induct 1);
-by (auto_tac (claset() addSIs fold_set.intrs
-                       addIs [fold_set_mono RS subsetD], simpset()));
-qed "fold_set_lemma";
-
-(* Proving that fold_set is deterministic *)
-Goal "[| <C-{x},y> : fold_set(A, B, f,e);  x:C; x:A; f(x, y):B |] \
-\     ==> <C, f(x, y)> : fold_set(A, B, f, e)";
-by (ftac (fold_set.dom_subset RS subsetD) 1);
-by (etac (cons_Diff RS subst) 1 THEN resolve_tac fold_set.intrs 1);
-by Auto_tac;
-qed "Diff1_fold_set";
-
-Goal "[| C:Fin(A); e:B; ALL x:A. ALL y:B. f(x, y):B |] ==>\
-\  (EX x. <C, x> : fold_set(A, B, f,e))";
-by (etac Fin_induct 1);
-by Auto_tac;
-by (ftac (fold_set.dom_subset RS subsetD) 2);
-by (auto_tac (claset() addDs [fold_set.dom_subset RS subsetD]
-                       addIs fold_set.intrs, simpset()));
-qed_spec_mp "Fin_imp_fold_set";
-
-Goal 
-"[| n:nat; e:B; \
-\ ALL x:A. ALL y:B. f(x, y):B; \
-\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
-\ ==> ALL C. |C|<n --> \
-\  (ALL x. <C, x> : fold_set(A, B, f,e)-->\
-\          (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x))";
-by (etac nat_induct 1);
-by (auto_tac (claset(), simpset() addsimps [le_iff]));
-by (Blast_tac 1);
-by (etac fold_set.elim 1);
-by (force_tac (claset() addSEs [empty_fold_setE], simpset()) 1);
-by (etac fold_set.elim 1);
-by (force_tac (claset() addSEs [empty_fold_setE], simpset()) 1);
-by (Clarify_tac 1);
-(*force simplification of "|C| < |cons(...)|"*)
-by (rotate_tac 4 1);
-by (etac rev_mp 1);
-by (forw_inst_tac [("a", "Ca")] 
-     (fold_set.dom_subset RS subsetD RS SigmaD1) 1);
-by (forw_inst_tac [("a", "Cb")] 
-     (fold_set.dom_subset RS subsetD RS SigmaD1) 1);
-by (asm_simp_tac (simpset() addsimps 
-    [Fin_into_Finite RS Finite_imp_cardinal_cons])  1);
-by (rtac impI 1);
-(** LEVEL 14 **)
-by (case_tac "x=xb" 1 THEN Auto_tac); (*SLOW*)
-by (asm_full_simp_tac (simpset() addsimps [cons_lemma1]) 1);
-by (REPEAT(thin_tac "ALL x:A. ?u(x)" 1) THEN Blast_tac 1);
-(*case x ~= xb*)
-by (dtac cons_lemma2 1 THEN ALLGOALS Clarify_tac);
-by (subgoal_tac "Ca = cons(xb, Cb) - {x}" 1);
-by (REPEAT(thin_tac "ALL C. ?P(C)" 2));
-by (REPEAT(thin_tac "ALL x:?u. ?P(x)" 2));
-by (blast_tac (claset() addEs [equalityE]) 2);
-(** LEVEL 22 **)
-by (subgoal_tac "|Ca| le |Cb|" 1);
-by (rtac succ_le_imp_le 2);
-by (hyp_subst_tac 2);
-by (subgoal_tac "Finite(cons(xb, Cb)) & x:cons(xb, Cb) " 2);
-by (asm_full_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, 
-                       Fin_into_Finite RS Finite_imp_cardinal_cons]) 2);
-by (asm_simp_tac (simpset() addsimps [Fin_into_Finite]) 2);
-by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A"), ("f1", "f")] 
-    (Fin_imp_fold_set RS exE) 1);
-by (blast_tac (claset() addIs [Diff_subset RS Fin_subset]) 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addSDs [FinD]) 1);
-(** LEVEL 32 **)
-by (ftac Diff1_fold_set 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addSDs [fold_set.dom_subset RS subsetD]) 1);
-by (subgoal_tac "ya = f(xb, xa)" 1);
-by (dres_inst_tac [("x", "Ca")] spec 2);
-by (blast_tac (claset() delrules [equalityCE]) 2);
-by (subgoal_tac "<Cb-{x}, xa>: fold_set(A, B, f, e)" 1);
-by (Asm_full_simp_tac 2);
-by (subgoal_tac "yb = f(x, xa)" 1);
-by (dres_inst_tac [("C", "Cb")] Diff1_fold_set 2);
-by (ALLGOALS(Asm_simp_tac));
-by (force_tac (claset() addSDs [fold_set.dom_subset RS subsetD], simpset()) 2);
-by (force_tac (claset() addSDs [fold_set.dom_subset RS subsetD], simpset()) 1);
-by (dres_inst_tac [("x", "Cb")] spec 1);
-by Auto_tac;
-qed_spec_mp "fold_set_determ_lemma";
-
-Goal
-"[| <C, x>:fold_set(A, B, f, e); \
-\        <C, y>:fold_set(A, B, f, e); e:B; \
-\ ALL x:A. ALL y:B. f(x, y):B; \
-\ ALL x:A. ALL y:A. ALL z:B.  f(x,f(y, z))=f(y, f(x, z)) |]\
-\ ==> y=x";
-by (forward_tac [fold_set.dom_subset RS subsetD] 1);
-by (Clarify_tac 1);
-by (dtac Fin_into_Finite 1);
-by (rewtac Finite_def);
-by (Clarify_tac 1);
-by (res_inst_tac [("n", "succ(n)"), ("e", "e"), ("A", "A"),
-                   ("f", "f"), ("B", "B")] fold_set_determ_lemma 1);
-by (auto_tac (claset() addIs [eqpoll_imp_lepoll RS 
-                              lepoll_cardinal_le], simpset()));
-qed "fold_set_determ";
-
-(** The fold function **)
-
-Goalw [fold_def] 
-"[| <C, y>:fold_set(A, B, f, e); e:B; \
-\ ALL x:A. ALL y:B. f(x, y):B; \
-\ ALL x:A. ALL y:A. ALL z:B.  f(x, f(y, z))=f(y, f(x, z)) |] \
-\  ==> fold[B](f, e, C) = y";
-by (forward_tac [fold_set.dom_subset RS subsetD] 1);
-by (Clarify_tac 1);
-by (rtac the_equality 1);
-by (res_inst_tac [("f", "f"), ("e", "e"), ("B", "B")] fold_set_determ 2);
-by (auto_tac (claset() addDs [fold_set_lemma], simpset()));
-by (blast_tac (claset() addSDs [FinD]) 1);
-qed "fold_equality";
-
-Goalw [fold_def] "e:B ==> fold[B](f,e,0) = e";
-by (blast_tac (claset() addSEs [empty_fold_setE]
-            addIs fold_set.intrs) 1);
-qed "fold_0";
-Addsimps [fold_0];
-
-Goal 
-"[| C:Fin(A); c:A; c~:C; e:B; ALL x:A. ALL y:B. f(x, y):B;  \
-\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x,z)) |]  \
-\    ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <->  \
-\         (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))";
-by Auto_tac;
-by (forward_tac [inst "a" "c" (thm"Fin.consI") RS FinD RS fold_set_mono RS subsetD] 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (forward_tac [FinD RS fold_set_mono RS subsetD] 2);
-by (assume_tac 2);
-by (ALLGOALS(forward_tac [inst "A" "A" fold_set.dom_subset RS subsetD]));
-by (ALLGOALS(dresolve_tac [FinD]));
-by (res_inst_tac [("A1", "cons(c, C)"), ("f1", "f"),
-                  ("B1", "B"), ("C1", "C")] (Fin_imp_fold_set RS exE) 1);
-by (res_inst_tac [("b", "cons(c, C)")] Fin_subset 1);
-by (resolve_tac [Finite_into_Fin] 2);
-by (resolve_tac [Fin_into_Finite] 2);
-by (Blast_tac 2);
-by (res_inst_tac [("x", "x")] exI 4);
-by (auto_tac (claset() addIs fold_set.intrs, simpset()));
-by (dresolve_tac [inst "C" "C" fold_set_lemma] 1);
-by (Blast_tac 1);
-by (resolve_tac fold_set.intrs 2);
-by Auto_tac;
-by (blast_tac (claset() addIs [fold_set_mono RS subsetD]) 2);
-by (resolve_tac [fold_set_determ] 1);
-by (assume_tac 5);
-by Auto_tac;
-by (resolve_tac fold_set.intrs 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [fold_set_mono RS subsetD]) 1);
-by (blast_tac (claset() addDs [fold_set.dom_subset RS subsetD]) 1);
-qed_spec_mp "fold_cons_lemma";
-
-Goalw [fold_def]
-"[| C:Fin(A); c:A; c~:C; e:B; \
-\ (ALL x:A. ALL y:B. f(x, y):B); \
-\ (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z))) |]\
-\   ==> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))";
-by (asm_simp_tac (simpset() addsimps [fold_cons_lemma]) 1);
-by (rtac the_equality 1);
-by (dres_inst_tac [("e", "e"), ("f", "f")] Fin_imp_fold_set 1);
-by Auto_tac;
-by (res_inst_tac [("x", "x")] exI 1);
-by Auto_tac;
-by (blast_tac (claset() addDs [fold_set_lemma]) 1);
-by (ALLGOALS(dtac fold_equality));
-by (auto_tac (claset(), simpset() addsimps [symmetric fold_def]));
-by (REPEAT(blast_tac (claset() addDs [FinD]) 1));
-qed "fold_cons";
-
-Goal 
-"[| C:Fin(A); e:B;  \
-\ (ALL x:A. ALL y:B. f(x, y):B); \
-\ (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z))) |] ==> \
-\  fold[B](f, e,C):B";
-by (etac Fin_induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [fold_cons])));
-qed_spec_mp "fold_type";
-AddTCs [fold_type];
-Addsimps [fold_type];
-
-Goal 
-"[| C:Fin(A); c:A; \
-\ ALL x:A. ALL y:B. f(x, y):B; \
-\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
-\ ==> (ALL y:B. f(c, fold[B](f, y, C)) = fold[B](f, f(c, y), C))";
-by (etac Fin_induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [fold_cons])));
-qed_spec_mp "fold_commute";
-
-Goal "x:D ==> cons(x, C) Int D = cons(x, C Int D)";
-by Auto_tac;
-qed "cons_Int_right_lemma1";
-
-Goal "x~:D ==> cons(x, C) Int D = C Int D";
-by Auto_tac;
-qed "cons_Int_right_lemma2";
-
-Goal 
-"[| C:Fin(A); D:Fin(A); e:B; \
-\ ALL x:A. ALL y:B. f(x, y):B; \
-\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
-\ ==> \
-\  fold[B](f, fold[B](f, e, D), C)  \
-\  =  fold[B](f, fold[B](f, e, (C Int D)), C Un D)";
-by (etac Fin_induct 1);
-by Auto_tac;
-by (subgoal_tac  "cons(x, y) Un D = cons(x, y Un D)" 1);
-by Auto_tac;
-by (subgoal_tac "y Int D:Fin(A) & y Un D:Fin(A)" 1);
-by (Clarify_tac 1);
-by (case_tac "x:D" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps 
-            [cons_Int_right_lemma1,cons_Int_right_lemma2,
-             fold_cons, fold_commute,cons_absorb])));
-qed "fold_nest_Un_Int";
-
-Goal "[| C:Fin(A); D:Fin(A); C Int D = 0; e:B; \
-\ ALL x:A. ALL y:B. f(x, y):B; \
-\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
-\     ==> fold[B](f,e,C Un D) =  fold[B](f, fold[B](f,e,D), C)";
-by (asm_simp_tac (simpset() addsimps [fold_nest_Un_Int]) 1);
-qed "fold_nest_Un_disjoint";
-
-Goal "Finite(C) ==> C:Fin(cons(c, C))";
-by (dtac Finite_into_Fin 1);
-by (blast_tac (claset() addIs [Fin_mono RS subsetD]) 1);
-qed "Finite_cons_lemma";
-
-(** setsum **)
-
-Goalw [setsum_def] "setsum(g, 0) = #0";
-by (Simp_tac 1);
-qed "setsum_0";
-Addsimps [setsum_0];
-
-Goalw [setsum_def]
-     "[| Finite(C); c~:C |] \
-\     ==> setsum(g, cons(c, C)) = g(c) $+ setsum(g, C)";
-by (auto_tac (claset(), simpset() addsimps [Finite_cons]));
-by (res_inst_tac [("A", "cons(c, C)")] fold_cons 1);
-by (auto_tac (claset() addIs [Finite_cons_lemma], simpset()));
-qed "setsum_cons";
-Addsimps [setsum_cons];
-
-Goal "setsum((%i. #0), C) = #0";
-by (case_tac "Finite(C)" 1);
-by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
-by (etac Finite_induct 1);
-by Auto_tac;
-qed "setsum_K0";
-
-(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
-Goal "[| Finite(C); Finite(D) |] \
-\     ==> setsum(g, C Un D) $+ setsum(g, C Int D) \
-\       = setsum(g, C) $+ setsum(g, D)";
-by (etac Finite_induct 1);
-by (subgoal_tac "cons(x, B) Un D = cons(x, B Un D) & \
-                \ Finite(B Un D) & Finite(B Int D)" 2);
-by (auto_tac (claset() addIs [Finite_Un, Int_lower1 RS subset_Finite], 
-              simpset()));
-by (case_tac "x:D" 1);
-by (subgoal_tac "cons(x, B) Int D = B Int D" 2);
-by (subgoal_tac "cons(x, B) Int D = cons(x, B Int D)" 1);
-by Auto_tac;
-by (subgoal_tac "cons(x, B Un D) = B Un D" 1);
-by Auto_tac;
-qed "setsum_Un_Int";
-
-Goal "setsum(g, C):int";
-by (case_tac "Finite(C)" 1);
-by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
-by (etac Finite_induct 1);
-by Auto_tac;
-qed "setsum_type";
-Addsimps [setsum_type];  AddTCs [setsum_type];
-
-Goal "[| Finite(C); Finite(D); C Int D = 0 |] \
-\     ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)";  
-by (stac (setsum_Un_Int RS sym) 1);
-by (subgoal_tac "Finite(C Un D)" 3);
-by (auto_tac (claset() addIs [Finite_Un], simpset()));
-qed "setsum_Un_disjoint";
-
-Goal "Finite(I) ==> (ALL i:I. Finite(C(i))) --> Finite(RepFun(I, C))";
-by (etac Finite_induct 1);
-by Auto_tac;
-qed_spec_mp "Finite_RepFun";
-
-Goal "Finite(I) \
-\     ==> (ALL i:I. Finite(C(i))) --> \
-\         (ALL i:I. ALL j:I. i~=j --> C(i) Int C(j) = 0) --> \
-\         setsum(f, UN i:I. C(i)) = setsum (%i. setsum(f, C(i)), I)"; 
-by (etac Finite_induct 1);
-by (ALLGOALS(Clarify_tac));
-by Auto_tac;
-by (subgoal_tac "ALL i:B. x ~= i" 1);
- by (Blast_tac 2); 
-by (subgoal_tac "C(x) Int (UN i:B. C(i)) = 0" 1);
- by (Blast_tac 2);
-by (subgoal_tac "Finite(UN i:B. C(i)) & Finite(C(x)) & Finite(B)" 1);
-by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1);
-by (auto_tac (claset() addIs [Finite_Union, Finite_RepFun], simpset()));
-qed_spec_mp "setsum_UN_disjoint";
-
-
-Goal "setsum(%x. f(x) $+ g(x),C) = setsum(f, C) $+ setsum(g, C)";
-by (case_tac "Finite(C)" 1);
-by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
-by (etac Finite_induct 1);
-by Auto_tac;
-qed "setsum_addf";
-
-
-Goal "[| A=A'; B=B'; e=e';  \
-\ (ALL x:A'. ALL y:B'. f(x,y) = f'(x,y)) |] ==> \
-\  fold_set(A,B,f,e) = fold_set(A',B',f',e')";
-by (asm_full_simp_tac (simpset() addsimps [thm"fold_set_def"]) 1); 
-by (rtac (thm"lfp_cong") 1); 
-by (rtac refl 1); 
-by (rtac Collect_cong 1);  
-by (rtac refl 1); 
-by (rtac disj_cong 1);  
-by (rtac iff_refl 1); 
-by (REPEAT (rtac ex_cong 1));  
-by Auto_tac; 
-qed "fold_set_cong";
-
-val prems = Goal 
-"[| B=B'; A=A'; e=e';  \
-\   !!x y. [|x:A'; y:B'|] ==> f(x,y) = f'(x,y) |] ==> \
-\  fold[B](f,e,A) = fold[B'](f', e', A')";
-by (asm_full_simp_tac (simpset() addsimps fold_def::prems) 1); 
-by (stac fold_set_cong 1); 
-by (rtac refl 5); 
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps prems)));
-qed "fold_cong";
-
-val prems = Goal
- "[| A=B; !!x. x:B ==> f(x) = g(x) |] ==> \
-\    setsum(f, A) = setsum(g, B)";
-by (asm_simp_tac (simpset() addsimps setsum_def::prems addcongs [fold_cong]) 1);
-qed  "setsum_cong";
-
-Goal "[| Finite(A); Finite(B) |] \
-\     ==> setsum(f, A Un B) = \
-\         setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)";
-by (stac (setsum_Un_Int RS sym) 1);
-by Auto_tac;
-qed "setsum_Un";
-
-
-Goal "Finite(A) ==> (ALL x:A. g(x) $<= #0) --> setsum(g, A) $<= #0";
-by (etac Finite_induct 1);
-by (auto_tac (claset() addIs [zneg_or_0_add_zneg_or_0_imp_zneg_or_0], simpset()));
-qed_spec_mp "setsum_zneg_or_0";
-
-Goal "Finite(A) \
-\     ==> ALL n:nat. setsum(f,A) = $# succ(n) --> (EX a:A. #0 $< f(a))";
-by (etac Finite_induct 1);
-by (auto_tac (claset(), simpset() 
-           delsimps [int_of_0, int_of_succ]
-           addsimps [not_zless_iff_zle, int_of_0 RS sym]));
-by (subgoal_tac "setsum(f, B) $<= #0" 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by (blast_tac (claset() addIs [setsum_zneg_or_0]) 2);
-by (subgoal_tac "$# 1 $<= f(x) $+ setsum(f, B)" 1);
-by (dtac  (zdiff_zle_iff RS iffD2) 1);
-by (subgoal_tac "$# 1 $<= $# 1 $- setsum(f,B)" 1);
-by (dres_inst_tac [("x",  "$# 1")] zle_trans 1);
-by (res_inst_tac [("j", "#1")] zless_zle_trans 2);
-by Auto_tac;
-qed "setsum_succD_lemma";
-
-Goal "[| setsum(f, A) = $# succ(n); n:nat |]==> EX a:A. #0 $< f(a)";
-by (case_tac "Finite(A)" 1);
-by (blast_tac (claset() 
-     addIs [setsum_succD_lemma RS bspec RS mp]) 1);
-by (rewtac setsum_def);
-by (auto_tac (claset(), 
-       simpset() delsimps [int_of_0, int_of_succ] 
-                 addsimps [int_succ_int_1 RS sym, int_of_0 RS sym]));
-qed "setsum_succD";
-
-Goal "Finite(A) ==> (ALL x:A. #0 $<= g(x)) --> #0 $<= setsum(g, A)";
-by (etac Finite_induct 1);
-by (Simp_tac 1);
-by (auto_tac (claset() addIs [zpos_add_zpos_imp_zpos],  simpset()));
-qed_spec_mp "g_zpos_imp_setsum_zpos";
-
-Goal "[| Finite(A); ALL x. #0 $<= g(x) |] ==> #0 $<= setsum(g, A)";
-by (etac Finite_induct 1);
-by (auto_tac (claset() addIs [zpos_add_zpos_imp_zpos], simpset()));
-qed_spec_mp "g_zpos_imp_setsum_zpos2";
-
-Goal "Finite(A) \
-\     ==> (ALL x:A. #0 $< g(x)) --> A ~= 0 --> (#0 $< setsum(g, A))";
-by (etac Finite_induct 1);
-by (auto_tac (claset() addIs [zspos_add_zspos_imp_zspos],simpset()));
-qed_spec_mp "g_zspos_imp_setsum_zspos";
-
-Goal "Finite(A) \
-\     ==> ALL a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})";
-by (etac Finite_induct 1);
-by (ALLGOALS(Clarify_tac));
-by (Simp_tac 1);
-by (case_tac "x=a" 1);
-by (subgoal_tac "cons(x, B) - {a} = cons(x, B -{a}) & Finite(B - {a})" 2);
-by (subgoal_tac "cons(a, B) - {a} = B" 1);
-by (auto_tac (claset() addIs [Finite_Diff], simpset()));
-qed_spec_mp "setsum_Diff";
diff -r 86c56794b641 -r 373806545656 src/ZF/Induct/FoldSet.thy
--- a/src/ZF/Induct/FoldSet.thy	Tue Jun 24 10:42:34 2003 +0200
+++ b/src/ZF/Induct/FoldSet.thy	Tue Jun 24 16:32:59 2003 +0200
@@ -8,24 +8,419 @@
 least left-commutative.  
 *)
 
-FoldSet = Main +
+theory FoldSet = Main:
 
 consts fold_set :: "[i, i, [i,i]=>i, i] => i"
 
 inductive
   domains "fold_set(A, B, f,e)" <= "Fin(A)*B"
-  intrs
-  emptyI   "e:B ==> <0, e>:fold_set(A, B, f,e)"
-  consI  "[| x:A; x ~:C;  <C,y> : fold_set(A, B,f,e); f(x,y):B |]
-              ==>  <cons(x,C), f(x,y)>:fold_set(A, B, f, e)"
-   type_intrs "Fin_intros"
+  intros
+    emptyI: "e\<in>B ==> <0, e>\<in>fold_set(A, B, f,e)"
+    consI:  "[| x\<in>A; x \<notin>C;  <C,y> : fold_set(A, B,f,e); f(x,y):B |]
+		==>  <cons(x,C), f(x,y)>\<in>fold_set(A, B, f, e)"
+  type_intros Fin.intros
   
 constdefs
   
   fold :: "[i, [i,i]=>i, i, i] => i"  ("fold[_]'(_,_,_')")
-  "fold[B](f,e, A) == THE x. <A, x>:fold_set(A, B, f,e)"
+   "fold[B](f,e, A) == THE x. <A, x>\<in>fold_set(A, B, f,e)"
 
    setsum :: "[i=>i, i] => i"
-  "setsum(g, C) == if Finite(C) then
-                    fold[int](%x y. g(x) $+ y, #0, C) else #0"
+   "setsum(g, C) == if Finite(C) then
+                     fold[int](%x y. g(x) $+ y, #0, C) else #0"
+
+(** foldSet **)
+
+inductive_cases empty_fold_setE: "<0, x> : fold_set(A, B, f,e)"
+inductive_cases cons_fold_setE: "<cons(x,C), y> : fold_set(A, B, f,e)"
+
+(* add-hoc lemmas *)                                                
+
+lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) <-> B = C"
+by (auto elim: equalityE)
+
+lemma cons_lemma2: "[| cons(x, B)=cons(y, C); x\<noteq>y; x\<notin>B; y\<notin>C |]  
+    ==>  B - {y} = C-{x} & x\<in>C & y\<in>B"
+apply (auto elim: equalityE)
+done
+
+(* fold_set monotonicity *)
+lemma fold_set_mono_lemma:
+     "<C, x> : fold_set(A, B, f, e)  
+      ==> ALL D. A<=D --> <C, x> : fold_set(D, B, f, e)"
+apply (erule fold_set.induct)
+apply (auto intro: fold_set.intros)
+done
+
+lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)"
+apply clarify
+apply (frule fold_set.dom_subset [THEN subsetD], clarify)
+apply (auto dest: fold_set_mono_lemma)
+done
+
+lemma fold_set_lemma:
+     "<C, x>\<in>fold_set(A, B, f, e) ==> <C, x>\<in>fold_set(C, B, f, e) & C<=A"
+apply (erule fold_set.induct)
+apply (auto intro!: fold_set.intros intro: fold_set_mono [THEN subsetD])
+done
+
+(* Proving that fold_set is deterministic *)
+lemma Diff1_fold_set:
+     "[| <C-{x},y> : fold_set(A, B, f,e);  x\<in>C; x\<in>A; f(x, y):B |]  
+      ==> <C, f(x, y)> : fold_set(A, B, f, e)"
+apply (frule fold_set.dom_subset [THEN subsetD])
+apply (erule cons_Diff [THEN subst], rule fold_set.intros, auto)
+done
+
+
+locale fold_typing =
+ fixes A and B and e and f
+ assumes ftype [intro,simp]:  "[|x \<in> A; y \<in> B|] ==> f(x,y) \<in> B"
+     and etype [intro,simp]:  "e \<in> B"
+     and fcomm:  "[|x \<in> A; y \<in> A; z \<in> B|] ==> f(x, f(y, z))=f(y, f(x, z))"
+
+
+lemma (in fold_typing) Fin_imp_fold_set:
+     "C\<in>Fin(A) ==> (EX x. <C, x> : fold_set(A, B, f,e))"
+apply (erule Fin_induct)
+apply (auto dest: fold_set.dom_subset [THEN subsetD] 
+            intro: fold_set.intros etype ftype)
+done
+
+lemma Diff_sing_imp:
+     "[|C - {b} = D - {a}; a \<noteq> b; b \<in> C|] ==> C = cons(b,D) - {a}"
+by (blast elim: equalityE)
+
+lemma (in fold_typing) fold_set_determ_lemma [rule_format]: 
+"n\<in>nat
+ ==> ALL C. |C|<n -->  
+   (ALL x. <C, x> : fold_set(A, B, f,e)--> 
+           (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x))"
+apply (erule nat_induct)
+ apply (auto simp add: le_iff)
+apply (erule fold_set.cases)
+ apply (force elim!: empty_fold_setE)
+apply (erule fold_set.cases)
+ apply (force elim!: empty_fold_setE, clarify)
+(*force simplification of "|C| < |cons(...)|"*)
+apply (frule_tac a = Ca in fold_set.dom_subset [THEN subsetD, THEN SigmaD1])
+apply (frule_tac a = Cb in fold_set.dom_subset [THEN subsetD, THEN SigmaD1])
+apply (simp add: Fin_into_Finite [THEN Finite_imp_cardinal_cons])
+apply (case_tac "x=xb", auto) 
+apply (simp add: cons_lemma1, blast)
+txt{*case @{term "x\<noteq>xb"}*}
+apply (drule cons_lemma2, safe)
+apply (frule Diff_sing_imp, assumption+) 
+txt{** LEVEL 17*}
+apply (subgoal_tac "|Ca| le |Cb|")
+ prefer 2
+ apply (rule succ_le_imp_le)
+ apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff 
+                  Fin_into_Finite [THEN Finite_imp_cardinal_cons])
+apply (rule_tac C1 = "Ca-{xb}" in Fin_imp_fold_set [THEN exE])
+ apply (blast intro: Diff_subset [THEN Fin_subset])
+txt{** LEVEL 24 **}
+apply (frule Diff1_fold_set, blast, blast)
+apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD])
+apply (subgoal_tac "ya = f(xb,xa) ")
+ prefer 2 apply (blast del: equalityCE)
+apply (subgoal_tac "<Cb-{x}, xa> : fold_set(A,B,f,e)")
+ prefer 2 apply simp
+apply (subgoal_tac "yb = f (x, xa) ")
+ apply (drule_tac [2] C = Cb in Diff1_fold_set, simp_all)
+  apply (blast intro: fcomm dest!: fold_set.dom_subset [THEN subsetD])
+ apply (blast intro: ftype dest!: fold_set.dom_subset [THEN subsetD], blast) 
+done
+
+lemma (in fold_typing) fold_set_determ: 
+     "[| <C, x>\<in>fold_set(A, B, f, e);  
+         <C, y>\<in>fold_set(A, B, f, e)|] ==> y=x"
+apply (frule fold_set.dom_subset [THEN subsetD], clarify)
+apply (drule Fin_into_Finite)
+apply (unfold Finite_def, clarify)
+apply (rule_tac n = "succ (n)" in fold_set_determ_lemma) 
+apply (auto intro: eqpoll_imp_lepoll [THEN lepoll_cardinal_le])
+done
+
+(** The fold function **)
+
+lemma (in fold_typing) fold_equality: 
+     "<C,y> : fold_set(A,B,f,e) ==> fold[B](f,e,C) = y"
+apply (unfold fold_def)
+apply (frule fold_set.dom_subset [THEN subsetD], clarify)
+apply (rule the_equality)
+ apply (rule_tac [2] A=C in fold_typing.fold_set_determ)
+apply (force dest: fold_set_lemma)
+apply (auto dest: fold_set_lemma)
+apply (simp add: fold_typing_def, auto) 
+apply (auto dest: fold_set_lemma intro: ftype etype fcomm)
+done
+
+lemma fold_0 [simp]: "e : B ==> fold[B](f,e,0) = e"
+apply (unfold fold_def)
+apply (blast elim!: empty_fold_setE intro: fold_set.intros)
+done
+
+text{*This result is the right-to-left direction of the subsequent result*}
+lemma (in fold_typing) fold_set_imp_cons: 
+     "[| <C, y> : fold_set(C, B, f, e); C : Fin(A); c : A; c\<notin>C |]
+      ==> <cons(c, C), f(c,y)> : fold_set(cons(c, C), B, f, e)"
+apply (frule FinD [THEN fold_set_mono, THEN subsetD])
+ apply assumption
+apply (frule fold_set.dom_subset [of A, THEN subsetD])
+apply (blast intro!: fold_set.consI intro: fold_set_mono [THEN subsetD])
+done
+
+lemma (in fold_typing) fold_cons_lemma [rule_format]: 
+"[| C : Fin(A); c : A; c\<notin>C |]   
+     ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <->   
+         (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))"
+apply auto
+ prefer 2 apply (blast intro: fold_set_imp_cons) 
+ apply (frule_tac Fin.consI [of c, THEN FinD, THEN fold_set_mono, THEN subsetD], assumption+)
+apply (frule_tac fold_set.dom_subset [of A, THEN subsetD])
+apply (drule FinD) 
+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])
+apply (blast intro: fold_typing.intro ftype etype fcomm) 
+apply (blast intro: Fin_subset [of _ "cons(c,C)"] Finite_into_Fin 
+             dest: Fin_into_Finite)  
+apply (rule_tac x = x in exI)
+apply (auto intro: fold_set.intros)
+apply (drule_tac fold_set_lemma [of C], blast)
+apply (blast intro!: fold_set.consI
+             intro: fold_set_determ fold_set_mono [THEN subsetD] 
+             dest: fold_set.dom_subset [THEN subsetD]) 
+done
+
+lemma (in fold_typing) fold_cons: 
+     "[| C\<in>Fin(A); c\<in>A; c\<notin>C|] 
+      ==> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))"
+apply (unfold fold_def)
+apply (simp add: fold_cons_lemma)
+apply (rule the_equality, auto) 
+ apply (subgoal_tac [2] "\<langle>C, y\<rangle> \<in> fold_set(A, B, f, e)")
+  apply (drule Fin_imp_fold_set)
+apply (auto dest: fold_set_lemma  simp add: fold_def [symmetric] fold_equality) 
+apply (blast intro: fold_set_mono [THEN subsetD] dest!: FinD) 
+done
+
+lemma (in fold_typing) fold_type [simp,TC]: 
+     "C\<in>Fin(A) ==> fold[B](f,e,C):B"
+apply (erule Fin_induct)
+apply (simp_all add: fold_cons ftype etype)
+done
+
+lemma (in fold_typing) fold_commute [rule_format]: 
+     "[| C\<in>Fin(A); c\<in>A |]  
+      ==> (\<forall>y\<in>B. f(c, fold[B](f, y, C)) = fold[B](f, f(c, y), C))"
+apply (erule Fin_induct)
+apply (simp_all add: fold_typing.fold_cons [of A B _ f] 
+                     fold_typing.fold_type [of A B _ f] 
+                     fold_typing_def fcomm)
+done
+
+lemma (in fold_typing) fold_nest_Un_Int: 
+     "[| C\<in>Fin(A); D\<in>Fin(A) |]
+      ==> fold[B](f, fold[B](f, e, D), C) =
+          fold[B](f, fold[B](f, e, (C Int D)), C Un D)"
+apply (erule Fin_induct, auto)
+apply (simp add: Un_cons Int_cons_left fold_type fold_commute
+                 fold_typing.fold_cons [of A _ _ f] 
+                 fold_typing_def fcomm cons_absorb)
+done
+
+lemma (in fold_typing) fold_nest_Un_disjoint:
+     "[| C\<in>Fin(A); D\<in>Fin(A); C Int D = 0 |]  
+      ==> fold[B](f,e,C Un D) =  fold[B](f, fold[B](f,e,D), C)"
+by (simp add: fold_nest_Un_Int)
+
+lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))"
+apply (drule Finite_into_Fin)
+apply (blast intro: Fin_mono [THEN subsetD])
+done
+
+subsection{*The Operator @{term setsum}*}
+
+lemma setsum_0 [simp]: "setsum(g, 0) = #0"
+by (simp add: setsum_def)
+
+lemma setsum_cons [simp]: 
+     "Finite(C) ==> 
+      setsum(g, cons(c,C)) = 
+        (if c : C then setsum(g,C) else g(c) $+ setsum(g,C))"
+apply (auto simp add: setsum_def Finite_cons cons_absorb)
+apply (rule_tac A = "cons (c, C)" in fold_typing.fold_cons)
+apply (auto intro: fold_typing.intro Finite_cons_lemma)
+done
+
+lemma setsum_K0: "setsum((%i. #0), C) = #0"
+apply (case_tac "Finite (C) ")
+ prefer 2 apply (simp add: setsum_def)
+apply (erule Finite_induct, auto)
+done
+
+(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
+lemma setsum_Un_Int:
+     "[| Finite(C); Finite(D) |]  
+      ==> setsum(g, C Un D) $+ setsum(g, C Int D)  
+        = setsum(g, C) $+ setsum(g, D)"
+apply (erule Finite_induct)
+apply (simp_all add: Int_cons_right cons_absorb Un_cons Int_commute Finite_Un
+                     Int_lower1 [THEN subset_Finite]) 
+done
+
+lemma setsum_type [simp,TC]: "setsum(g, C):int"
+apply (case_tac "Finite (C) ")
+ prefer 2 apply (simp add: setsum_def)
+apply (erule Finite_induct, auto)
+done
+
+lemma setsum_Un_disjoint:
+     "[| Finite(C); Finite(D); C Int D = 0 |]  
+      ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)"
+apply (subst setsum_Un_Int [symmetric])
+apply (subgoal_tac [3] "Finite (C Un D) ")
+apply (auto intro: Finite_Un)
+done
+
+lemma Finite_RepFun [rule_format (no_asm)]:
+     "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) --> Finite(RepFun(I, C))"
+apply (erule Finite_induct, auto)
+done
+
+lemma setsum_UN_disjoint [rule_format (no_asm)]:
+     "Finite(I)  
+      ==> (\<forall>i\<in>I. Finite(C(i))) -->  
+          (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j --> C(i) Int C(j) = 0) -->  
+          setsum(f, \<Union>i\<in>I. C(i)) = setsum (%i. setsum(f, C(i)), I)"
+apply (erule Finite_induct, auto)
+apply (subgoal_tac "\<forall>i\<in>B. x \<noteq> i")
+ prefer 2 apply blast
+apply (subgoal_tac "C (x) Int (\<Union>i\<in>B. C (i)) = 0")
+ prefer 2 apply blast
+apply (subgoal_tac "Finite (\<Union>i\<in>B. C (i)) & Finite (C (x)) & Finite (B) ")
+apply (simp (no_asm_simp) add: setsum_Un_disjoint)
+apply (auto intro: Finite_Union Finite_RepFun)
+done
+
+
+lemma setsum_addf: "setsum(%x. f(x) $+ g(x),C) = setsum(f, C) $+ setsum(g, C)"
+apply (case_tac "Finite (C) ")
+ prefer 2 apply (simp add: setsum_def)
+apply (erule Finite_induct, auto)
+done
+
+
+lemma fold_set_cong:
+     "[| A=A'; B=B'; e=e'; (\<forall>x\<in>A'. \<forall>y\<in>B'. f(x,y) = f'(x,y)) |] 
+      ==> fold_set(A,B,f,e) = fold_set(A',B',f',e')"
+apply (simp add: fold_set_def)
+apply (intro refl iff_refl lfp_cong Collect_cong disj_cong ex_cong, auto)
+done
+
+lemma fold_cong:
+"[| B=B'; A=A'; e=e';   
+    !!x y. [|x\<in>A'; y\<in>B'|] ==> f(x,y) = f'(x,y) |] ==>  
+   fold[B](f,e,A) = fold[B'](f', e', A')"
+apply (simp add: fold_def)
+apply (subst fold_set_cong)
+apply (rule_tac [5] refl, simp_all)
+done
+
+lemma setsum_cong:
+ "[| A=B; !!x. x\<in>B ==> f(x) = g(x) |] ==>  
+     setsum(f, A) = setsum(g, B)"
+by (simp add: setsum_def cong add: fold_cong)
+
+lemma setsum_Un:
+     "[| Finite(A); Finite(B) |]  
+      ==> setsum(f, A Un B) =  
+          setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)"
+apply (subst setsum_Un_Int [symmetric], auto)
+done
+
+
+lemma setsum_zneg_or_0 [rule_format (no_asm)]:
+     "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) --> setsum(g, A) $<= #0"
+apply (erule Finite_induct)
+apply (auto intro: zneg_or_0_add_zneg_or_0_imp_zneg_or_0)
+done
+
+lemma setsum_succD_lemma [rule_format]:
+     "Finite(A)  
+      ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) --> (\<exists>a\<in>A. #0 $< f(a))"
+apply (erule Finite_induct)
+apply (auto simp del: int_of_0 int_of_succ simp add: not_zless_iff_zle int_of_0 [symmetric])
+apply (subgoal_tac "setsum (f, B) $<= #0")
+apply simp_all
+prefer 2 apply (blast intro: setsum_zneg_or_0)
+apply (subgoal_tac "$# 1 $<= f (x) $+ setsum (f, B) ")
+apply (drule zdiff_zle_iff [THEN iffD2])
+apply (subgoal_tac "$# 1 $<= $# 1 $- setsum (f,B) ")
+apply (drule_tac x = "$# 1" in zle_trans)
+apply (rule_tac [2] j = "#1" in zless_zle_trans, auto)
+done
+
+lemma setsum_succD:
+     "[| setsum(f, A) = $# succ(n); n\<in>nat |]==> \<exists>a\<in>A. #0 $< f(a)"
+apply (case_tac "Finite (A) ")
+apply (blast intro: setsum_succD_lemma)
+apply (unfold setsum_def)
+apply (auto simp del: int_of_0 int_of_succ simp add: int_succ_int_1 [symmetric] int_of_0 [symmetric])
+done
+
+lemma g_zpos_imp_setsum_zpos [rule_format]:
+     "Finite(A) ==> (\<forall>x\<in>A. #0 $<= g(x)) --> #0 $<= setsum(g, A)"
+apply (erule Finite_induct)
+apply (simp (no_asm))
+apply (auto intro: zpos_add_zpos_imp_zpos)
+done
+
+lemma g_zpos_imp_setsum_zpos2 [rule_format]:
+     "[| Finite(A); \<forall>x. #0 $<= g(x) |] ==> #0 $<= setsum(g, A)"
+apply (erule Finite_induct)
+apply (auto intro: zpos_add_zpos_imp_zpos)
+done
+
+lemma g_zspos_imp_setsum_zspos [rule_format]:
+     "Finite(A)  
+      ==> (\<forall>x\<in>A. #0 $< g(x)) --> A \<noteq> 0 --> (#0 $< setsum(g, A))"
+apply (erule Finite_induct)
+apply (auto intro: zspos_add_zspos_imp_zspos)
+done
+
+lemma setsum_Diff [rule_format]:
+     "Finite(A) ==> \<forall>a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})"
+apply (erule Finite_induct) 
+apply (simp_all add: Diff_cons_eq Finite_Diff) 
+done
+
+ML
+{*
+val fold_set_mono = thm "fold_set_mono";
+val Diff1_fold_set = thm "Diff1_fold_set";
+val Diff_sing_imp = thm "Diff_sing_imp";
+val fold_0 = thm "fold_0";
+val setsum_0 = thm "setsum_0";
+val setsum_cons = thm "setsum_cons";
+val setsum_K0 = thm "setsum_K0";
+val setsum_Un_Int = thm "setsum_Un_Int";
+val setsum_type = thm "setsum_type";
+val setsum_Un_disjoint = thm "setsum_Un_disjoint";
+val Finite_RepFun = thm "Finite_RepFun";
+val setsum_UN_disjoint = thm "setsum_UN_disjoint";
+val setsum_addf = thm "setsum_addf";
+val fold_set_cong = thm "fold_set_cong";
+val fold_cong = thm "fold_cong";
+val setsum_cong = thm "setsum_cong";
+val setsum_Un = thm "setsum_Un";
+val setsum_zneg_or_0 = thm "setsum_zneg_or_0";
+val setsum_succD = thm "setsum_succD";
+val g_zpos_imp_setsum_zpos = thm "g_zpos_imp_setsum_zpos";
+val g_zpos_imp_setsum_zpos2 = thm "g_zpos_imp_setsum_zpos2";
+val g_zspos_imp_setsum_zspos = thm "g_zspos_imp_setsum_zspos";
+val setsum_Diff = thm "setsum_Diff";
+*}
+
+
 end
\ No newline at end of file
diff -r 86c56794b641 -r 373806545656 src/ZF/Induct/Multiset.ML
--- a/src/ZF/Induct/Multiset.ML	Tue Jun 24 10:42:34 2003 +0200
+++ b/src/ZF/Induct/Multiset.ML	Tue Jun 24 16:32:59 2003 +0200
@@ -398,11 +398,6 @@
        addsimps [int_of_add RS sym, int_of_0 RS sym]));
 qed "msize_eq_0_iff";
 
-Goal 
-"cons(x, A) Int B = (if x:B then cons(x, A Int B) else A Int B)";
-by Auto_tac;
-qed "cons_Int_right_cases";
-
 Goal
 "Finite(A) ==> setsum(%a. $# mcount(N, a), A Int mset_of(N)) \
 \            = setsum(%a. $# mcount(N, a), A)";
@@ -411,7 +406,7 @@
 by (subgoal_tac "Finite(B Int mset_of(N))" 1);
 by (blast_tac (claset() addIs [subset_Finite]) 2);
 by (auto_tac (claset(), 
-         simpset() addsimps [mcount_def, cons_Int_right_cases]));
+         simpset() addsimps [mcount_def, Int_cons_left]));
 qed "setsum_mcount_Int";
 
 Goalw [msize_def]
diff -r 86c56794b641 -r 373806545656 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Tue Jun 24 10:42:34 2003 +0200
+++ b/src/ZF/IsaMakefile	Tue Jun 24 16:32:59 2003 +0200
@@ -138,7 +138,7 @@
 
 $(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.thy \
   Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \
-  Induct/Datatypes.thy Induct/FoldSet.ML Induct/FoldSet.thy \
+  Induct/Datatypes.thy Induct/FoldSet.thy \
   Induct/ListN.thy Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
   Induct/Ntree.thy Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \
   Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
diff -r 86c56794b641 -r 373806545656 src/ZF/UNITY/AllocImpl.thy
--- a/src/ZF/UNITY/AllocImpl.thy	Tue Jun 24 10:42:34 2003 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy	Tue Jun 24 16:32:59 2003 +0200
@@ -7,21 +7,6 @@
 Charpentier and Chandy, section 7 (page 17).
 *)
 
-(*LOCALE NEEDED FOR PROOF OF GUARANTEES THEOREM*)
-
-(*????FIXME: sort out this mess
-FoldSet.cons_Int_right_lemma1:
-  ?x \<in> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = cons(?x, ?C \<inter> ?D)
-FoldSet.cons_Int_right_lemma2: ?x \<notin> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = ?C \<inter> ?D
-Multiset.cons_Int_right_cases:
-  cons(?x, ?A) \<inter> ?B = (if ?x \<in> ?B then cons(?x, ?A \<inter> ?B) else ?A \<inter> ?B)
-UNITYMisc.Int_cons_right:
-  ?A \<inter> cons(?a, ?B) = (if ?a \<in> ?A then cons(?a, ?A \<inter> ?B) else ?A \<inter> ?B)
-UNITYMisc.Int_succ_right:
-  ?A \<inter> succ(?k) = (if ?k \<in> ?A then cons(?k, ?A \<inter> ?k) else ?A \<inter> ?k)
-*)
-
-
 theory AllocImpl = ClientImpl:
 
 consts
@@ -34,10 +19,10 @@
   "available_tok" == "Var([succ(succ(2))])"
 
 axioms
-  alloc_type_assumes:
+  alloc_type_assumes [simp]:
   "type_of(NbR) = nat & type_of(available_tok)=nat"
 
-  alloc_default_val_assumes:
+  alloc_default_val_assumes [simp]:
   "default_val(NbR)  = 0 & default_val(available_tok)=0"
 
 constdefs
@@ -67,25 +52,20 @@
 		        preserves(lift(giv)). Acts(G))"
 
 
-declare alloc_type_assumes [simp] alloc_default_val_assumes [simp]
-
 lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat"
 apply (unfold state_def)
-apply (drule_tac a = "available_tok" in apply_type)
-apply auto
+apply (drule_tac a = available_tok in apply_type, auto)
 done
 
 lemma NbR_value_type [simp,TC]: "s\<in>state ==> s`NbR \<in> nat"
 apply (unfold state_def)
-apply (drule_tac a = "NbR" in apply_type)
-apply auto
+apply (drule_tac a = NbR in apply_type, auto)
 done
 
 (** The Alloc Program **)
 
 lemma alloc_prog_type [simp,TC]: "alloc_prog \<in> program"
-apply (simp add: alloc_prog_def)
-done
+by (simp add: alloc_prog_def)
 
 declare alloc_prog_def [THEN def_prg_Init, simp]
 declare alloc_prog_def [THEN def_prg_AllowedActs, simp]
@@ -107,11 +87,9 @@
 
 lemma alloc_prog_preserves:
     "alloc_prog \<in> (\<Inter>x \<in> var-{giv, available_tok, NbR}. preserves(lift(x)))"
-apply (rule Inter_var_DiffI)
-apply (force );
+apply (rule Inter_var_DiffI, force)
 apply (rule ballI)
-apply (rule preservesI)
-apply (constrains)
+apply (rule preservesI, constrains)
 done
 
 (* As a special case of the rule above *)
@@ -121,10 +99,9 @@
        preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))"
 apply auto
 apply (insert alloc_prog_preserves)
-apply (drule_tac [3] x = "tok" in Inter_var_DiffD)
-apply (drule_tac [2] x = "ask" in Inter_var_DiffD)
-apply (drule_tac x = "rel" in Inter_var_DiffD)
-apply auto
+apply (drule_tac [3] x = tok in Inter_var_DiffD)
+apply (drule_tac [2] x = ask in Inter_var_DiffD)
+apply (drule_tac x = rel in Inter_var_DiffD, auto)
 done
 
 lemma alloc_prog_Allowed:
@@ -152,8 +129,7 @@
 
 (** Safety property: (28) **)
 lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))"
-apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed)
-apply constrains+
+apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed, constrains+)
 apply (auto dest: ActsD)
 apply (drule_tac f = "lift (giv) " in preserves_imp_eq)
 apply auto
@@ -163,7 +139,7 @@
 "alloc_prog \<in> stable({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))})"
-apply (constrains)
+apply constrains
 apply auto
 apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse)
 apply (simp (no_asm_simp) add: take_succ)
@@ -180,13 +156,13 @@
 apply (subgoal_tac "G \<in> preserves (fun_pair (lift (available_tok), fun_pair (lift (NbR), lift (giv))))")
 apply (rotate_tac -1)
 apply (cut_tac A = "nat * nat * list(nat)"
-             and P = "%<m,n,l> y. n \<le> length(y) & 
+             and P = "%<m,n,l> y. n \<le> length(y) &
                                   m #+ tokens(l) = NbT #+ tokens(take(n,y))"
-             and g = "lift(rel)" and F = "alloc_prog"
+             and g = "lift(rel)" and F = alloc_prog
        in stable_Join_Stable)
-prefer 3 apply assumption;
+prefer 3 apply assumption
 apply (auto simp add: Collect_conj_eq)
-apply (frule_tac g = "length" in imp_Increasing_comp)
+apply (frule_tac g = length in imp_Increasing_comp)
 apply (blast intro: mono_length)
 apply (auto simp add: refl_prefix)
 apply (drule_tac a=xa and f = "length comp lift(rel)" in Increasing_imp_Stable)
@@ -200,11 +176,9 @@
 apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl)
 apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable)
 apply (auto simp add: Stable_def Constrains_def constrains_def)
-apply (drule bspec)
-apply force
+apply (drule bspec, force)
 apply (drule subsetD)
-apply (rule imageI)
-apply assumption
+apply (rule imageI, assumption)
 apply (auto simp add: prefix_take_iff)
 apply (rotate_tac -1)
 apply (erule ssubst)
@@ -219,9 +193,8 @@
 apply (auto simp add: guar_def)
 apply (rule Always_weaken)
 apply (rule AlwaysI)
-apply (rule_tac [2] giv_Bounded_lemma2)
-apply auto
-apply (rule_tac j = "NbT #+ tokens (take (x` NbR, x`rel))" in le_trans)
+apply (rule_tac [2] giv_Bounded_lemma2, auto)
+apply (rule_tac j = "NbT #+ tokens(take (x` NbR, x`rel))" in le_trans)
 apply (erule subst)
 apply (auto intro!: tokens_mono simp add: prefix_take_iff min_def length_take)
 done
@@ -234,105 +207,96 @@
 apply (auto intro!: AlwaysI simp add: guar_def)
 apply (subgoal_tac "G \<in> preserves (lift (giv))")
  prefer 2 apply (simp add: alloc_prog_ok_iff)
-apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)" 
+apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)"
        in stable_Join_Stable)
-apply (constrains)
- prefer 2 apply (simp add: lift_def); 
- apply (clarify ); 
-apply (drule_tac a = "k" in Increasing_imp_Stable)
-apply auto
+apply constrains
+ prefer 2 apply (simp add: lift_def, clarify)
+apply (drule_tac a = k in Increasing_imp_Stable, auto)
 done
 
-(**** Towards proving the liveness property, (31) ****)
+subsection{* Towards proving the liveness property, (31) *}
 
-(*** First, we lead up to a proof of Lemma 49, page 28. ***)
+subsubsection{*First, we lead up to a proof of Lemma 49, page 28.*}
 
 lemma alloc_prog_transient_lemma:
-"G \<in> program ==> \<forall>k\<in>nat. alloc_prog Join G \<in>
-                   transient({s\<in>state. k \<le> length(s`rel)}
-                   \<inter> {s\<in>state. succ(s`NbR) = k})"
+     "[|G \<in> program; k\<in>nat|]
+      ==> alloc_prog Join G \<in>
+             transient({s\<in>state. k \<le> length(s`rel)} \<inter>
+             {s\<in>state. succ(s`NbR) = k})"
 apply auto
 apply (erule_tac V = "G\<notin>?u" in thin_rl)
-apply (rule_tac act = "alloc_rel_act" in transientI)
+apply (rule_tac act = alloc_rel_act in transientI)
 apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts])
 apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset])
 apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
 apply (rule ReplaceI)
 apply (rule_tac x = "x (available_tok:= x`available_tok #+ nth (x`NbR, x`rel),
-                        NbR:=succ (x`NbR))" 
+                        NbR:=succ (x`NbR))"
        in exI)
 apply (auto intro!: state_update_type)
 done
 
 lemma alloc_prog_rel_Stable_NbR_lemma:
-"[| G \<in> program; alloc_prog ok G; k\<in>nat |] ==>
-    alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
-apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff)
-apply constrains
-apply auto
+    "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
+     ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
+apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains, auto)
 apply (blast intro: le_trans leI)
-apply (drule_tac f = "lift (NbR)" and A = "nat" in preserves_imp_increasing)
-apply (drule_tac [2] g = "succ" in imp_increasing_comp)
+apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing)
+apply (drule_tac [2] g = succ in imp_increasing_comp)
 apply (rule_tac [2] mono_succ)
-apply (drule_tac [4] x = "k" in increasing_imp_stable)
-    prefer 5 apply (simp add: Le_def comp_def) 
-apply auto
+apply (drule_tac [4] x = k in increasing_imp_stable)
+    prefer 5 apply (simp add: Le_def comp_def, auto)
 done
 
-lemma alloc_prog_NbR_LeadsTo_lemma [rule_format (no_asm)]:
-"[| G \<in> program; alloc_prog ok G;
-    alloc_prog Join G \<in> Incr(lift(rel)) |] ==>
-     \<forall>k\<in>nat. alloc_prog Join G \<in>
-       {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
-       LeadsTo {s\<in>state. k \<le> s`NbR}"
-apply clarify
-apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
-apply (drule_tac [2] a = "k" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
+lemma alloc_prog_NbR_LeadsTo_lemma:
+     "[| G \<in> program; alloc_prog ok G;
+	 alloc_prog Join G \<in> Incr(lift(rel)); k\<in>nat |]
+      ==> alloc_prog Join G \<in>
+	    {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
+	    LeadsTo {s\<in>state. k \<le> s`NbR}"
+apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})")
+apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
 apply (rule_tac [2] mono_length)
-    prefer 3 apply (simp add: ); 
+    prefer 3 apply simp
 apply (simp_all add: refl_prefix Le_def comp_def length_type)
 apply (rule LeadsTo_weaken)
 apply (rule PSP_Stable)
-prefer 2 apply (assumption)
+prefer 2 apply assumption
 apply (rule PSP_Stable)
 apply (rule_tac [2] alloc_prog_rel_Stable_NbR_lemma)
-apply (rule alloc_prog_transient_lemma [THEN bspec, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo])
-apply assumption+
+apply (rule alloc_prog_transient_lemma [THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo], assumption+)
 apply (auto dest: not_lt_imp_le elim: lt_asym simp add: le_iff)
 done
 
 lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]:
-    "[| G :program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel)) |]
-      ==> \<forall>k\<in>nat. \<forall>n \<in> nat. n < k -->
-       alloc_prog Join G \<in>
-       {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
-	  LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
-	    (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
+    "[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
+        k\<in>nat; n \<in> nat; n < k |]
+      ==> alloc_prog Join G \<in>
+	    {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
+	       LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
+		 (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
 apply (unfold greater_than_def)
-apply clarify
-apply (rule_tac A' = "{x \<in> state. k \<le> length (x`rel) } \<inter> {x \<in> state. n < x`NbR}" in LeadsTo_weaken_R)
+apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
+       in LeadsTo_weaken_R)
 apply safe
 apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
-apply (drule_tac [2] a = "k" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
+apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
 apply (rule_tac [2] mono_length)
-    prefer 3 apply (simp add: ); 
+    prefer 3 apply simp
 apply (simp_all add: refl_prefix Le_def comp_def length_type)
 apply (subst Int_commute)
 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)
-apply (rule PSP_Stable)
-apply safe
+apply (rule PSP_Stable, safe)
 apply (rule_tac B = "{x \<in> state . n < length (x ` rel) } \<inter> {s\<in>state . s ` NbR = n}" in LeadsTo_Trans)
 apply (rule_tac [2] LeadsTo_weaken)
 apply (rule_tac [2] k = "succ (n)" in alloc_prog_NbR_LeadsTo_lemma)
-apply (simp_all add: ) 
-apply (rule subset_imp_LeadsTo)
-apply auto
+apply simp_all
+apply (rule subset_imp_LeadsTo, auto)
 apply (blast intro: lt_trans2)
 done
 
-lemma Collect_vimage_eq: "u\<in>nat ==> {<s, f(s)>. s \<in> state} -`` u = {s\<in>state. f(s) < u}"
-apply (force simp add: lt_def)
-done
+lemma Collect_vimage_eq: "u\<in>nat ==> {<s,f(s)>. s \<in> A} -`` u = {s\<in>A. f(s) < u}"
+by (force simp add: lt_def)
 
 (* Lemma 49, page 28 *)
 
@@ -343,26 +307,22 @@
            {s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
 (* Proof by induction over the difference between k and n *)
 apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct)
-apply (simp_all add: lam_def)
-apply auto
-apply (rule single_LeadsTo_I)
-apply auto
+apply (simp_all add: lam_def, auto)
+apply (rule single_LeadsTo_I, auto)
 apply (simp (no_asm_simp) add: Collect_vimage_eq)
 apply (rename_tac "s0")
 apply (case_tac "s0`NbR < k")
-apply (rule_tac [2] subset_imp_LeadsTo)
-apply safe
+apply (rule_tac [2] subset_imp_LeadsTo, safe)
 apply (auto dest!: not_lt_imp_le)
 apply (rule LeadsTo_weaken)
-apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2)
-apply safe
-prefer 3 apply (assumption)
+apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2, safe)
+prefer 3 apply assumption
 apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
 apply (blast dest: lt_asym)
 apply (force dest: add_lt_elim2)
 done
 
-(** Towards proving lemma 50, page 29 **)
+subsubsection{*Towards proving lemma 50, page 29*}
 
 lemma alloc_prog_giv_Ensures_lemma:
 "[| G \<in> program; k\<in>nat; alloc_prog ok G;
@@ -371,27 +331,23 @@
   {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}
   Ensures {s\<in>state. ~ k <length(s`ask)} Un {s\<in>state. length(s`giv) \<noteq> k}"
-apply (rule EnsuresI)
-apply auto
+apply (rule EnsuresI, auto)
 apply (erule_tac [2] V = "G\<notin>?u" in thin_rl)
-apply (rule_tac [2] act = "alloc_giv_act" in transientI)
+apply (rule_tac [2] act = alloc_giv_act in transientI)
  prefer 2
  apply (simp add: alloc_prog_def [THEN def_prg_Acts])
  apply (simp add: alloc_giv_act_def [THEN def_act_eq, THEN act_subset])
 apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
 apply (erule_tac [2] swap)
 apply (rule_tac [2] ReplaceI)
-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)
+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)
 apply (auto intro!: state_update_type simp add: app_type)
-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)
-apply safe
-apply (auto dest: ActsD simp add: Constrains_def constrains_def length_app alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff)
-apply (subgoal_tac "length (xa ` giv @ [nth (length (xa ` giv), xa ` ask) ]) = length (xa ` giv) #+ 1")
+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)
+apply (auto dest: ActsD simp add: Constrains_def constrains_def alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff)
+apply (subgoal_tac "length(xa ` giv @ [nth (length(xa ` giv), xa ` ask) ]) = length(xa ` giv) #+ 1")
 apply (rule_tac [2] trans)
-apply (rule_tac [2] length_app)
-apply auto
-apply (rule_tac j = "xa ` available_tok" in le_trans)
-apply auto
+apply (rule_tac [2] length_app, auto)
+apply (rule_tac j = "xa ` available_tok" in le_trans, auto)
 apply (drule_tac f = "lift (available_tok)" in preserves_imp_eq)
 apply assumption+
 apply auto
@@ -399,19 +355,17 @@
        in Increasing_imp_Stable)
 apply (auto simp add: prefix_iff)
 apply (drule StableD)
-apply (auto simp add: Constrains_def constrains_def)
-apply force
+apply (auto simp add: Constrains_def constrains_def, force)
 done
 
 lemma alloc_prog_giv_Stable_lemma:
 "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
   ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
-apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff)
-apply (constrains)
-apply (auto intro: leI simp add: length_app)
-apply (drule_tac f = "lift (giv)" and g = "length" in imp_preserves_comp)
-apply (drule_tac f = "length comp lift (giv)" and A = "nat" and r = "Le" in preserves_imp_increasing)
-apply (drule_tac [2] x = "k" in increasing_imp_stable)
+apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains)
+apply (auto intro: leI)
+apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp)
+apply (drule_tac f = "length comp lift (giv)" and A = nat and r = Le in preserves_imp_increasing)
+apply (drule_tac [2] x = k in increasing_imp_stable)
  prefer 3 apply (simp add: Le_def comp_def)
 apply (auto simp add: length_type)
 done
@@ -420,24 +374,23 @@
 
 lemma alloc_prog_giv_LeadsTo_lemma:
 "[| G \<in> program; alloc_prog ok G;
-    alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |] ==>
-  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`giv)}"
-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}")
+    alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |]
+ ==> 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`giv)}"
+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}")
 prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis])
-apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k < length (s`ask) }) ")
-apply (drule PSP_Stable)
-apply assumption
+apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
+apply (drule PSP_Stable, assumption)
 apply (rule LeadsTo_weaken)
 apply (rule PSP_Stable)
-apply (rule_tac [2] k = "k" in alloc_prog_giv_Stable_lemma)
+apply (rule_tac [2] k = k in alloc_prog_giv_Stable_lemma)
 apply (auto simp add: le_iff)
-apply (drule_tac a = "succ (k)" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
+apply (drule_tac a = "succ (k)" and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
 apply (rule mono_length)
- prefer 2 apply (simp add: ); 
+ prefer 2 apply simp
 apply (simp_all add: refl_prefix Le_def comp_def length_type)
 done
 
@@ -452,69 +405,72 @@
   ==> alloc_prog Join G \<in>
         Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) -->
                 NbT \<le> s`available_tok})"
-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))}) ")
+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))}) ")
 apply (rule_tac [2] AlwaysI)
-apply (rule_tac [3] giv_Bounded_lemma2)
-apply auto
-apply (rule Always_weaken)
-apply assumption
-apply auto
-apply (subgoal_tac "0 \<le> tokens (take (x ` NbR, x ` rel)) #- tokens (x`giv) ")
+apply (rule_tac [3] giv_Bounded_lemma2, auto)
+apply (rule Always_weaken, assumption, auto)
+apply (subgoal_tac "0 \<le> tokens(take (x ` NbR, x ` rel)) #- tokens(x`giv) ")
 apply (rule_tac [2] nat_diff_split [THEN iffD2])
- prefer 2 apply (force ); 
+ prefer 2 apply force
 apply (subgoal_tac "x`available_tok =
-                    NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens (x`giv))")
+                    NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
 apply (simp (no_asm_simp))
-apply (rule nat_diff_split [THEN iffD2])
-apply auto
-apply (drule_tac j = "tokens (x ` giv)" in lt_trans2)
+apply (rule nat_diff_split [THEN iffD2], auto)
+apply (drule_tac j = "tokens(x ` giv)" in lt_trans2)
 apply assumption
 apply auto
 done
 
-(* Main lemmas towards proving property (31) *)
+subsubsection{* Main lemmas towards proving property (31)*}
 
 lemma LeadsTo_strength_R:
     "[|  F \<in> C LeadsTo B'; F \<in> A-C LeadsTo B; B'<=B |] ==> F \<in> A LeadsTo  B"
-by (blast intro: LeadsTo_weaken LeadsTo_Un_Un) 
+by (blast intro: LeadsTo_weaken LeadsTo_Un_Un)
 
 lemma PSP_StableI:
 "[| F \<in> Stable(C); F \<in> A - C LeadsTo B;
    F \<in> A \<inter> C LeadsTo B Un (state - C) |] ==> F \<in> A LeadsTo  B"
 apply (rule_tac A = " (A-C) Un (A \<inter> C)" in LeadsTo_weaken_L)
- prefer 2 apply (blast)
-apply (rule LeadsTo_Un)
-apply assumption
-apply (blast intro: LeadsTo_weaken dest: PSP_Stable) 
+ prefer 2 apply blast
+apply (rule LeadsTo_Un, assumption)
+apply (blast intro: LeadsTo_weaken dest: PSP_Stable)
 done
 
 lemma state_compl_eq [simp]: "state - {s\<in>state. P(s)} = {s\<in>state. ~P(s)}"
-apply auto
-done
+by auto
 
 (*needed?*)
 lemma single_state_Diff_eq [simp]: "{s}-{x \<in> state. P(x)} = (if s\<in>state & P(s) then 0 else {s})"
-apply auto
-done
+by auto
+
 
+locale alloc_progress =
+ fixes G
+ assumes Gprog [intro,simp]: "G \<in> program"
+     and okG [iff]:          "alloc_prog ok G"
+     and Incr_rel [intro]:   "alloc_prog Join G \<in> Incr(lift(rel))"
+     and Incr_ask [intro]:   "alloc_prog Join G \<in> Incr(lift(ask))"
+     and safety:   "alloc_prog Join G
+                      \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT})"
+     and progress: "alloc_prog Join G
+                      \<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
+                        {s\<in>state. k \<le> tokens(s`rel)})"
 
 (*First step in proof of (31) -- the corrected version from Charpentier.
   This lemma implies that if a client releases some tokens then the Allocator
   will eventually recognize that they've been released.*)
-lemma alloc_prog_LeadsTo_tokens_take_NbR_lemma:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
-    G \<in> program; alloc_prog ok G; k \<in> tokbag |]
+lemma (in alloc_progress) tokens_take_NbR_lemma:
+ "k \<in> tokbag
   ==> alloc_prog Join G \<in>
         {s\<in>state. k \<le> tokens(s`rel)}
         LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
-apply (rule single_LeadsTo_I)
-apply safe
+apply (rule single_LeadsTo_I, safe)
 apply (rule_tac a1 = "s`rel" in Increasing_imp_Stable [THEN PSP_StableI])
-apply (rule_tac [4] k1 = "length (s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R])
+apply (rule_tac [4] k1 = "length(s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R])
 apply (rule_tac [8] subset_imp_LeadsTo)
-apply auto
-apply (rule_tac j = "tokens (take (length (s`rel), x`rel))" in le_trans)
-apply (rule_tac j = "tokens (take (length (s`rel), s`rel))" in le_trans)
+apply (auto intro!: Incr_rel)
+apply (rule_tac j = "tokens(take (length(s`rel), x`rel))" in le_trans)
+apply (rule_tac j = "tokens(take (length(s`rel), s`rel))" in le_trans)
 apply (auto intro!: tokens_mono take_mono simp add: prefix_iff)
 done
 
@@ -522,256 +478,184 @@
 
 (*Second step in proof of (31): by LHS of the guarantee and transivity of
   LeadsTo *)
-lemma alloc_prog_LeadsTo_tokens_take_NbR_lemma2:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
-    G \<in> program; alloc_prog ok G; k \<in> tokbag;
-    alloc_prog Join G \<in>
-       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
-  ==> alloc_prog Join G \<in>
-        {s\<in>state. tokens(s`giv) = k}
-        LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
+lemma (in alloc_progress) tokens_take_NbR_lemma2:
+     "k \<in> tokbag
+      ==> alloc_prog Join G \<in>
+	    {s\<in>state. tokens(s`giv) = k}
+	    LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
 apply (rule LeadsTo_Trans)
-apply (rule_tac [2] alloc_prog_LeadsTo_tokens_take_NbR_lemma)
-apply (blast intro: LeadsTo_weaken_L nat_into_Ord)
-apply assumption+
+ apply (rule_tac [2] tokens_take_NbR_lemma)
+ prefer 2 apply assumption
+apply (insert progress) 
+apply (blast intro: LeadsTo_weaken_L progress nat_into_Ord)
 done
 
 (*Third step in proof of (31): by PSP with the fact that giv increases *)
-lemma alloc_prog_LeadsTo_length_giv_disj:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
-    G \<in> program; alloc_prog ok G; k \<in> tokbag; n \<in> nat;
-    alloc_prog Join G \<in>
-       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
-  ==> alloc_prog Join G \<in>
-        {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
-        LeadsTo
-          {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
-                     k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}"
-apply (rule single_LeadsTo_I)
-apply safe
+lemma (in alloc_progress) length_giv_disj:
+     "[| k \<in> tokbag; n \<in> nat |]
+      ==> alloc_prog Join G \<in>
+	    {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
+	    LeadsTo
+	      {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
+			 k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}"
+apply (rule single_LeadsTo_I, safe)
 apply (rule_tac a1 = "s`giv" in Increasing_imp_Stable [THEN PSP_StableI])
 apply (rule alloc_prog_Increasing_giv [THEN guaranteesD])
 apply (simp_all add: Int_cons_left)
 apply (rule LeadsTo_weaken)
-apply (rule_tac k = "tokens (s`giv)" in alloc_prog_LeadsTo_tokens_take_NbR_lemma2)
-apply simp_all
-apply safe
-apply (drule prefix_length_le [THEN le_iff [THEN iffD1]]) 
-apply (force simp add:)
+apply (rule_tac k = "tokens(s`giv)" in tokens_take_NbR_lemma2)
+apply auto
+apply (force dest: prefix_length_le [THEN le_iff [THEN iffD1]]) 
 apply (simp add: not_lt_iff_le)
-apply (drule prefix_length_le_equal)
-apply assumption
-apply (simp add:)
+apply (force dest: prefix_length_le_equal) 
 done
 
 (*Fourth step in proof of (31): we apply lemma (51) *)
-lemma alloc_prog_LeadsTo_length_giv_disj2:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
-    alloc_prog Join G \<in> Incr(lift(ask));
-    G \<in> program; alloc_prog ok G; k \<in> tokbag; n \<in> nat;
-    alloc_prog Join G \<in>
-       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
-  ==> alloc_prog Join G \<in>
-        {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
-        LeadsTo
-          {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
-                    n < length(s`giv)}"
+lemma (in alloc_progress) length_giv_disj2:
+     "[|k \<in> tokbag; n \<in> nat|]
+      ==> alloc_prog Join G \<in>
+	    {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
+	    LeadsTo
+	      {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
+			n < length(s`giv)}"
 apply (rule LeadsTo_weaken_R)
-apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma alloc_prog_LeadsTo_length_giv_disj])
-apply auto
+apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma length_giv_disj], auto)
 done
 
 (*Fifth step in proof of (31): from the fourth step, taking the union over all
   k\<in>nat *)
-lemma alloc_prog_LeadsTo_length_giv_disj3:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
-    alloc_prog Join G \<in> Incr(lift(ask));
-    G \<in> program; alloc_prog ok G;  n \<in> nat;
-    alloc_prog Join G \<in>
-       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
-  ==> alloc_prog Join G \<in>
-        {s\<in>state. length(s`giv) = n}
-        LeadsTo
-          {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
-                    n < length(s`giv)}"
+lemma (in alloc_progress) length_giv_disj3:
+     "n \<in> nat
+      ==> alloc_prog Join G \<in>
+	    {s\<in>state. length(s`giv) = n}
+	    LeadsTo
+	      {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
+			n < length(s`giv)}"
 apply (rule LeadsTo_weaken_L)
-apply (rule_tac I = "nat" in LeadsTo_UN)
-apply (rule_tac k = "i" in alloc_prog_LeadsTo_length_giv_disj2)
+apply (rule_tac I = nat in LeadsTo_UN)
+apply (rule_tac k = i in length_giv_disj2)
 apply (simp_all add: UN_conj_eq)
 done
 
 (*Sixth step in proof of (31): from the fifth step, by PSP with the
   assumption that ask increases *)
-lemma alloc_prog_LeadsTo_length_ask_giv:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
-    alloc_prog Join G \<in> Incr(lift(ask));
-    G \<in> program; alloc_prog ok G;  k \<in> nat;  n < k;
-    alloc_prog Join G \<in>
-       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+lemma (in alloc_progress) length_ask_giv:
+ "[|k \<in> nat;  n < k|]
   ==> alloc_prog Join G \<in>
         {s\<in>state. length(s`ask) = k & length(s`giv) = n}
         LeadsTo
           {s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
                      length(s`giv) = n) |
                     n < length(s`giv)}"
-apply (rule single_LeadsTo_I)
-apply safe
-apply (rule_tac a1 = "s`ask" and f1 = "lift (ask)" in Increasing_imp_Stable [THEN PSP_StableI])
-apply assumption
-apply simp_all
+apply (rule single_LeadsTo_I, safe)
+apply (rule_tac a1 = "s`ask" and f1 = "lift(ask)" 
+       in Increasing_imp_Stable [THEN PSP_StableI])
+apply (rule Incr_ask, simp_all)
 apply (rule LeadsTo_weaken)
-apply (rule_tac n = "length (s ` giv)" in alloc_prog_LeadsTo_length_giv_disj3)
+apply (rule_tac n = "length(s ` giv)" in length_giv_disj3)
 apply simp_all
-apply (blast intro:)
+apply blast
 apply clarify
-apply (simp add:)
+apply simp
 apply (blast dest!: prefix_length_le intro: lt_trans2)
 done
 
 
 (*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
-lemma alloc_prog_LeadsTo_length_ask_giv2:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
-    alloc_prog Join G \<in> Incr(lift(ask));
-    G \<in> program; alloc_prog ok G;  k \<in> nat;  n < k;
-    alloc_prog Join G \<in>
-      Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
-    alloc_prog Join G \<in>
-       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
-  ==> alloc_prog Join G \<in>
-        {s\<in>state. length(s`ask) = k & length(s`giv) = n}
-        LeadsTo
-          {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
-                     length(s`giv) < length(s`ask) & length(s`giv) = n) |
-                    n < length(s`giv)}"
+lemma (in alloc_progress) length_ask_giv2:
+     "[|k \<in> nat;  n < k|]
+      ==> alloc_prog Join G \<in>
+	    {s\<in>state. length(s`ask) = k & length(s`giv) = n}
+	    LeadsTo
+	      {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
+			 length(s`giv) < length(s`ask) & length(s`giv) = n) |
+			n < length(s`giv)}"
 apply (rule LeadsTo_weaken_R)
-apply (erule Always_LeadsToD [OF asm_rl alloc_prog_LeadsTo_length_ask_giv])
-apply assumption+
-apply clarify
-apply (simp add: INT_iff)
-apply clarify
-apply (drule_tac x = "length (x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
-apply (simp add:)
+apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify)
+apply (simp add: INT_iff, clarify)
+apply (drule_tac x = "length(x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
+apply simp
 apply (blast intro: le_trans)
 done
 
-(*Eighth step in proof of (31): by (50), we get |giv| > n. *)
-lemma alloc_prog_LeadsTo_extend_giv:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
-    alloc_prog Join G \<in> Incr(lift(ask));
-    G \<in> program; alloc_prog ok G;  k \<in> nat;  n < k;
-    alloc_prog Join G \<in>
-      Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
-    alloc_prog Join G \<in>
-       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
-  ==> alloc_prog Join G \<in>
-        {s\<in>state. length(s`ask) = k & length(s`giv) = n}
-        LeadsTo {s\<in>state. n < length(s`giv)}"
+(*Eighth step in proof of (31): by 50, we get |giv| > n. *)
+lemma (in alloc_progress) extend_giv:
+     "[| k \<in> nat;  n < k|]
+      ==> alloc_prog Join G \<in>
+	    {s\<in>state. length(s`ask) = k & length(s`giv) = n}
+	    LeadsTo {s\<in>state. n < length(s`giv)}"
 apply (rule LeadsTo_Un_duplicate)
 apply (rule LeadsTo_cancel1)
 apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma)
-apply safe;
- prefer 2 apply (simp add: lt_nat_in_nat)
+apply (simp_all add: Incr_ask lt_nat_in_nat)
 apply (rule LeadsTo_weaken_R)
-apply (rule alloc_prog_LeadsTo_length_ask_giv2)
-apply auto
+apply (rule length_ask_giv2, auto)
 done
 
-(*Ninth and tenth steps in proof of (31): by (50), we get |giv| > n.
+(*Ninth and tenth steps in proof of (31): by 50, we get |giv| > n.
   The report has an error: putting |ask|=k for the precondition fails because
   we can't expect |ask| to remain fixed until |giv| increases.*)
-lemma alloc_prog_ask_LeadsTo_giv:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
-    alloc_prog Join G \<in> Incr(lift(ask));
-    G \<in> program; alloc_prog ok G;  k \<in> nat;
-    alloc_prog Join G \<in>
-      Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
-    alloc_prog Join G \<in>
-       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
+ "k \<in> nat
   ==> alloc_prog Join G \<in>
         {s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
 (* Proof by induction over the difference between k and n *)
-apply (rule_tac f = "\<lambda>s\<in>state. k #- length (s`giv)" in LessThan_induct)
-apply (simp_all add: lam_def)
- prefer 2 apply (force)
-apply clarify
-apply (simp add: Collect_vimage_eq)
-apply (rule single_LeadsTo_I)
-apply safe
-apply simp
+apply (rule_tac f = "\<lambda>s\<in>state. k #- length(s`giv)" in LessThan_induct)
+apply (auto simp add: lam_def Collect_vimage_eq)
+apply (rule single_LeadsTo_I, auto)
 apply (rename_tac "s0")
-apply (case_tac "length (s0 ` giv) < length (s0 ` ask) ")
+apply (case_tac "length(s0 ` giv) < length(s0 ` ask) ")
  apply (rule_tac [2] subset_imp_LeadsTo)
-  apply safe
- prefer 2 
- apply (simp add: not_lt_iff_le)
- apply (blast dest: le_imp_not_lt intro: lt_trans2)
-apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)" 
+  apply (auto simp add: not_lt_iff_le)
+ prefer 2 apply (blast dest: le_imp_not_lt intro: lt_trans2)
+apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
        in Increasing_imp_Stable [THEN PSP_StableI])
-apply assumption
-apply (simp add:)
-apply (force simp add:)
+apply (rule Incr_ask, simp)
+apply (force)
 apply (rule LeadsTo_weaken)
-apply (rule_tac n = "length (s0 ` giv)" and k = "length (s0 ` ask)" 
-       in alloc_prog_LeadsTo_extend_giv)
-apply simp_all
- apply (force simp add:)
-apply clarify
-apply (simp add:)
-apply (erule disjE)
- apply (blast dest!: prefix_length_le intro: lt_trans2)
-apply (rule not_lt_imp_le)
-apply clarify
-apply (simp_all add: leI diff_lt_iff_lt)
+apply (rule_tac n = "length(s0 ` giv)" and k = "length(s0 ` ask)"
+       in extend_giv) 
+apply (auto dest: not_lt_imp_le simp add: leI diff_lt_iff_lt) 
+apply (blast dest!: prefix_length_le intro: lt_trans2)
 done
 
 (*Final lemma: combine previous result with lemma (30)*)
-lemma alloc_prog_progress_lemma:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
-    alloc_prog Join G \<in> Incr(lift(ask));
-    G \<in> program; alloc_prog ok G;  h \<in> list(tokbag);
-    alloc_prog Join G \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
-    alloc_prog Join G \<in>
-       (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo 
-                 {s\<in>state. k \<le> tokens(s`rel)}) |]
-  ==> alloc_prog Join G \<in>
-        {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
-        {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
+lemma (in alloc_progress) final:
+     "h \<in> list(tokbag)
+      ==> alloc_prog Join G \<in>
+	    {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
+	    {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
 apply (rule single_LeadsTo_I)
- prefer 2 apply (simp)
+ prefer 2 apply simp
 apply (rename_tac s0)
-apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)" 
+apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
        in Increasing_imp_Stable [THEN PSP_StableI])
-   apply assumption
-  prefer 2 apply (force simp add:)
-apply (simp_all add: Int_cons_left)
+   apply (rule Incr_ask)
+  apply (simp_all add: Int_cons_left)
 apply (rule LeadsTo_weaken)
-apply (rule_tac k1 = "length (s0 ` ask)" 
+apply (rule_tac k1 = "length(s0 ` ask)"
        in Always_LeadsToD [OF alloc_prog_ask_prefix_giv [THEN guaranteesD]
                               alloc_prog_ask_LeadsTo_giv])
-apply simp_all
-apply (force simp add:)
-apply (force simp add:)
-apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le lt_trans2)
+apply (auto simp add: Incr_ask)
+apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le 
+                    lt_trans2)
 done
 
 (** alloc_prog liveness property (31), page 18 **)
 
-(*missing the LeadsTo assumption on the lhs!?!?!*)
-lemma alloc_prog_progress:
+theorem alloc_prog_progress:
 "alloc_prog \<in>
     Incr(lift(ask)) \<inter> Incr(lift(rel)) \<inter>
     Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT}) \<inter>
-    (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo 
+    (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
               {s\<in>state. k \<le> tokens(s`rel)})
   guarantees (\<Inter>h \<in> list(tokbag).
               {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
               {s\<in>state. <h, s`giv> \<in> prefix(tokbag)})"
 apply (rule guaranteesI)
-apply (rule INT_I)
-apply (rule alloc_prog_progress_lemma)
-apply simp_all
-apply (blast intro:)
+apply (rule INT_I [OF _ list.Nil])
+apply (rule alloc_progress.final)
+apply (simp_all add: alloc_progress_def)
 done
 
 
diff -r 86c56794b641 -r 373806545656 src/ZF/UNITY/MultisetSum.ML
--- a/src/ZF/UNITY/MultisetSum.ML	Tue Jun 24 10:42:34 2003 +0200
+++ b/src/ZF/UNITY/MultisetSum.ML	Tue Jun 24 16:32:59 2003 +0200
@@ -22,8 +22,8 @@
 by  (auto_tac (claset(), simpset() addsimps [Fin_into_Finite RS Finite_cons, 
                                              cons_absorb]));
 by (blast_tac (claset() addDs [Fin_into_Finite]) 2);
-by (resolve_tac [fold_cons] 1);
-by (auto_tac (claset(), simpset() addsimps [lcomm_def]));
+by (resolve_tac [thm"fold_typing.fold_cons"] 1);
+by (auto_tac (claset(), simpset() addsimps [thm "fold_typing_def", lcomm_def]));
 qed "general_setsum_cons";
 Addsimps [general_setsum_cons];
 
@@ -185,8 +185,9 @@
 "[| Finite(C); x~:C |] \
 \  ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)";
 by (auto_tac (claset(), simpset() addsimps [Finite_cons]));
-by (res_inst_tac [("A", "cons(x, C)")] fold_cons 1);
-by (auto_tac (claset() addIs [Finite_cons_lemma], simpset()));
+by (res_inst_tac [("A", "cons(x, C)")] (thm"fold_typing.fold_cons") 1);
+by (auto_tac (claset() addIs [thm"Finite_cons_lemma"], 
+              simpset() addsimps [thm "fold_typing_def"]));
 qed "nsetsum_cons";
 Addsimps [nsetsum_cons];
 
diff -r 86c56794b641 -r 373806545656 src/ZF/UNITY/UNITYMisc.ML
--- a/src/ZF/UNITY/UNITYMisc.ML	Tue Jun 24 10:42:34 2003 +0200
+++ b/src/ZF/UNITY/UNITYMisc.ML	Tue Jun 24 16:32:59 2003 +0200
@@ -37,9 +37,10 @@
 by (assume_tac 1);
 qed "list_nat_into_univ";
 
-(** To be moved to Update theory **)
 
-(** Simplication rules for Collect; To be moved elsewhere **)
+(** Simplication rules for Collect; ????
+  At least change to "{x:A. P(x)} Int A = {x : A Int B. P(x)} **)
+
 Goal "{x:A. P(x)} Int A = {x:A. P(x)}";
 by Auto_tac;
 qed "Collect_Int2";
@@ -48,6 +49,7 @@
 by Auto_tac;
 qed "Collect_Int3";
 
+(*????????????????*)
 AddIffs [Collect_Int2, Collect_Int3];
 
 
@@ -65,15 +67,6 @@
 by (Blast_tac 1);
 qed "Int_Union2";
 
-Goal "A Int cons(a, B) = (if a : A then cons(a, A Int B) else A Int B)";
-by Auto_tac;
-qed "Int_cons_right";
-
 Goal "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)";
 by Auto_tac;
 qed "Int_succ_right";
-
-Goal "cons(a,B) Int A = (if a : A then cons(a, A Int B) else A Int B)";
-by Auto_tac;
-qed "Int_cons_left";
-
diff -r 86c56794b641 -r 373806545656 src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Tue Jun 24 10:42:34 2003 +0200
+++ b/src/ZF/equalities.thy	Tue Jun 24 16:32:59 2003 +0200
@@ -136,6 +136,9 @@
 lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
 by blast
 
+lemma Diff_cons_eq: "cons(a,B) - C = (if a\<in>C then B-C else cons(a,B-C))" 
+by auto
+
 lemma equal_singleton [rule_format]: "[| a: C;  \<forall>y\<in>C. y=b |] ==> C = {b}"
 by blast
 
@@ -227,6 +230,14 @@
 lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B"
 by blast
 
+lemma Int_cons_left:
+     "cons(a,A) Int B = (if a : B then cons(a, A Int B) else A Int B)"
+by auto
+
+lemma Int_cons_right:
+     "A Int cons(a, B) = (if a : A then cons(a, A Int B) else A Int B)"
+by auto
+
 subsection{*Binary Union*}
 
 (** Union is the least upper bound of two sets *)
@@ -1084,6 +1095,8 @@
 val subset_Int_iff = thm "subset_Int_iff";
 val subset_Int_iff2 = thm "subset_Int_iff2";
 val Int_Diff_eq = thm "Int_Diff_eq";
+val Int_cons_left = thm "Int_cons_left";
+val Int_cons_right = thm "Int_cons_right";
 val Un_cons = thm "Un_cons";
 val Un_absorb = thm "Un_absorb";
 val Un_left_absorb = thm "Un_left_absorb";