Conversion of AllocBase to new-style
authorpaulson
Fri Jun 27 13:15:40 2003 +0200 (2003-06-27)
changeset 140765cfc8b9fb880
parent 14075 ab2e26ae90e3
child 14077 37c964462747
Conversion of AllocBase to new-style
src/ZF/Cardinal.thy
src/ZF/IsaMakefile
src/ZF/List.thy
src/ZF/UNITY/AllocBase.ML
src/ZF/UNITY/AllocBase.thy
src/ZF/UNITY/AllocImpl.thy
src/ZF/UNITY/Guar.ML
src/ZF/UNITY/Merge.thy
src/ZF/UNITY/Union.ML
src/ZF/ZF.thy
src/ZF/equalities.thy
     1.1 --- a/src/ZF/Cardinal.thy	Thu Jun 26 18:20:00 2003 +0200
     1.2 +++ b/src/ZF/Cardinal.thy	Fri Jun 27 13:15:40 2003 +0200
     1.3 @@ -1019,6 +1019,15 @@
     1.4  apply (fast intro!: eqpoll_refl)
     1.5  done
     1.6  
     1.7 +lemma nat_not_Finite: "~Finite(nat)"
     1.8 +apply (unfold Finite_def, clarify) 
     1.9 +apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp) 
    1.10 +apply (insert Card_nat) 
    1.11 +apply (simp add: Card_def)
    1.12 +apply (drule le_imp_subset)
    1.13 +apply (blast elim: mem_irrefl)
    1.14 +done
    1.15 +
    1.16  ML
    1.17  {*
    1.18  val Least_def = thm "Least_def";
     2.1 --- a/src/ZF/IsaMakefile	Thu Jun 26 18:20:00 2003 +0200
     2.2 +++ b/src/ZF/IsaMakefile	Fri Jun 27 13:15:40 2003 +0200
     2.3 @@ -120,7 +120,7 @@
     2.4    UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
     2.5    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
     2.6    UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
     2.7 -  UNITY/AllocBase.ML UNITY/AllocBase.thy UNITY/AllocImpl.thy\
     2.8 +  UNITY/AllocBase.thy UNITY/AllocImpl.thy\
     2.9    UNITY/ClientImpl.thy UNITY/Distributor.thy\
    2.10    UNITY/Follows.ML UNITY/Follows.thy\
    2.11    UNITY/Increasing.ML UNITY/Increasing.thy UNITY/Merge.thy\
     3.1 --- a/src/ZF/List.thy	Thu Jun 26 18:20:00 2003 +0200
     3.2 +++ b/src/ZF/List.thy	Fri Jun 27 13:15:40 2003 +0200
     3.3 @@ -831,6 +831,12 @@
     3.4  apply (erule_tac n = i in natE, simp_all)
     3.5  done
     3.6  
     3.7 +lemma length_take:
     3.8 +     "l\<in>list(A) ==> \<forall>n\<in>nat. length(take(n,l)) = min(n, length(l))"
     3.9 +apply (induct_tac "l", safe, simp_all)
    3.10 +apply (erule natE, simp_all)
    3.11 +done
    3.12 +
    3.13  subsection{*The function zip*}
    3.14  
    3.15  text{*Crafty definition to eliminate a type argument*}
     4.1 --- a/src/ZF/UNITY/AllocBase.ML	Thu Jun 26 18:20:00 2003 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,438 +0,0 @@
     4.4 -(*  Title:      ZF/UNITY/AllocBase.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     4.7 -    Copyright   2001  University of Cambridge
     4.8 -
     4.9 -Common declarations for Chandy and Charpentier's Allocator
    4.10 -*)
    4.11 -
    4.12 -(*????remove from Union.ML:AddSEs [not_emptyE];*)
    4.13 -Delrules [not_emptyE];
    4.14 -
    4.15 -Goal "0 < Nclients & 0 < NbT";
    4.16 -by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
    4.17 -by (auto_tac (claset() addIs [Ord_0_lt], simpset()));
    4.18 -qed "Nclients_NbT_gt_0";
    4.19 -Addsimps [Nclients_NbT_gt_0 RS conjunct1, Nclients_NbT_gt_0 RS conjunct2];
    4.20 -
    4.21 -Goal "Nclients \\<noteq> 0 & NbT \\<noteq> 0";
    4.22 -by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
    4.23 -by Auto_tac;
    4.24 -qed "Nclients_NbT_not_0";
    4.25 -Addsimps [Nclients_NbT_not_0 RS conjunct1, Nclients_NbT_not_0  RS conjunct2];
    4.26 -
    4.27 -Goal "Nclients\\<in>nat & NbT\\<in>nat";
    4.28 -by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
    4.29 -by Auto_tac;
    4.30 -qed "Nclients_NbT_type";
    4.31 -Addsimps [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
    4.32 -AddTCs [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
    4.33 -
    4.34 -Goal "b\\<in>Inter(RepFun(Nclients, B)) <-> (\\<forall>x\\<in>Nclients. b\\<in>B(x))";
    4.35 -by (auto_tac (claset(), simpset() addsimps [INT_iff]));
    4.36 -by (res_inst_tac [("x", "0")] exI 1);
    4.37 -by (rtac ltD 1); 
    4.38 -by Auto_tac; 
    4.39 -qed "INT_Nclient_iff";
    4.40 -AddIffs [INT_Nclient_iff];
    4.41 -
    4.42 -val succ_def = thm "succ_def";
    4.43 -
    4.44 -Goal "n\\<in>nat ==> \
    4.45 -\     (\\<forall>i\\<in>nat. i<n --> f(i) $<= g(i)) --> \
    4.46 -\     setsum(f, n) $<= setsum(g,n)";
    4.47 -by (induct_tac "n" 1);
    4.48 -by (ALLGOALS Asm_full_simp_tac);
    4.49 -by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x\\<notin>x" 1);
    4.50 -by (Clarify_tac 1);
    4.51 -by (Asm_simp_tac 1);
    4.52 -by (subgoal_tac "\\<forall>i\\<in>nat. i<x--> f(i) $<= g(i)" 1);
    4.53 -by (resolve_tac [zadd_zle_mono] 1);
    4.54 -by (thin_tac "succ(x)=cons(x,x)" 1);
    4.55 -by (ALLGOALS(Asm_simp_tac));
    4.56 -by (thin_tac "succ(x)=cons(x, x)" 1);
    4.57 -by (Clarify_tac 1);
    4.58 -by (dtac leI 1);
    4.59 -by (Asm_simp_tac 1);
    4.60 -by (asm_simp_tac (simpset() addsimps [nat_into_Finite, mem_not_refl, succ_def]) 1);
    4.61 -qed_spec_mp "setsum_fun_mono";
    4.62 -
    4.63 -Goal "l\\<in>list(A) ==> tokens(l)\\<in>nat";
    4.64 -by (etac list.induct 1);
    4.65 -by Auto_tac;
    4.66 -qed "tokens_type";
    4.67 -AddTCs [tokens_type];
    4.68 -Addsimps [tokens_type];
    4.69 -
    4.70 -Goal "xs\\<in>list(A) ==> \\<forall>ys\\<in>list(A). <xs, ys>\\<in>prefix(A) \
    4.71 -\  --> tokens(xs) \\<le> tokens(ys)";
    4.72 -by (induct_tac "xs" 1);
    4.73 -by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], 
    4.74 -              simpset() addsimps [prefix_def]));
    4.75 -qed_spec_mp "tokens_mono_aux";
    4.76 -
    4.77 -Goal "<xs, ys>\\<in>prefix(A) ==> tokens(xs) \\<le> tokens(ys)";
    4.78 -by (cut_facts_tac [prefix_type] 1);
    4.79 -by (blast_tac (claset() addIs [tokens_mono_aux]) 1);
    4.80 -qed "tokens_mono";
    4.81 -
    4.82 -Goalw [mono1_def] "mono1(list(A), prefix(A), nat, Le ,tokens)";
    4.83 -by (auto_tac (claset() addIs [tokens_mono],
    4.84 -             simpset() addsimps [Le_def]));
    4.85 -qed "mono_tokens";
    4.86 -Addsimps [mono_tokens];
    4.87 -AddIs [mono_tokens];
    4.88 -
    4.89 -Goal 
    4.90 -"[| xs\\<in>list(A); ys\\<in>list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)";
    4.91 -by (induct_tac "xs" 1);
    4.92 -by Auto_tac;
    4.93 -qed "tokens_append";
    4.94 -Addsimps [tokens_append];
    4.95 -
    4.96 -(*????????????????List.thy*)
    4.97 -Goal "l\\<in>list(A) ==> \\<forall>n\\<in>nat. length(take(n, l))=min(n, length(l))";
    4.98 -by (induct_tac "l" 1);
    4.99 -by Safe_tac;
   4.100 -by (ALLGOALS(Asm_simp_tac));
   4.101 -by (etac natE 1);
   4.102 -by (ALLGOALS(Asm_simp_tac));
   4.103 -qed "length_take";
   4.104 -
   4.105 -(** bag_of **)
   4.106 -
   4.107 -Goal "l\\<in>list(A) ==>bag_of(l)\\<in>Mult(A)";
   4.108 -by (induct_tac "l" 1);
   4.109 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   4.110 -qed "bag_of_type";
   4.111 -AddTCs [bag_of_type];
   4.112 -Addsimps [bag_of_type];
   4.113 -
   4.114 -Goal "l\\<in>list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A";
   4.115 -by (dtac bag_of_type 1);
   4.116 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   4.117 -qed "bag_of_multiset";
   4.118 -
   4.119 -Goal "[| xs\\<in>list(A); ys\\<in>list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)";
   4.120 -by (induct_tac "xs" 1);
   4.121 -by (auto_tac (claset(), simpset() 
   4.122 -       addsimps [bag_of_multiset, munion_assoc]));
   4.123 -qed "bag_of_append";
   4.124 -Addsimps [bag_of_append];
   4.125 -
   4.126 -Goal "xs\\<in>list(A) ==> \\<forall>ys\\<in>list(A). <xs, ys>\\<in>prefix(A) \
   4.127 -\  --> <bag_of(xs), bag_of(ys)>\\<in>MultLe(A, r)";
   4.128 -by (induct_tac "xs" 1);
   4.129 -by (ALLGOALS(Clarify_tac));
   4.130 -by (ftac bag_of_multiset 1);
   4.131 -by (forw_inst_tac [("l", "ys")] bag_of_multiset 2);
   4.132 -by (auto_tac (claset() addIs [empty_le_MultLe], 
   4.133 -              simpset() addsimps [prefix_def]));
   4.134 -by (rtac munion_mono 1);
   4.135 -by (force_tac (claset(), simpset() addsimps 
   4.136 -               [MultLe_def, Mult_iff_multiset]) 1);
   4.137 -by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 1);
   4.138 -qed_spec_mp "bag_of_mono_aux";
   4.139 -
   4.140 -Goal "[|  <xs, ys>\\<in>prefix(A); xs\\<in>list(A); ys\\<in>list(A) |] ==> \
   4.141 -\  <bag_of(xs), bag_of(ys)>\\<in>MultLe(A, r)";
   4.142 -by (blast_tac (claset() addIs [bag_of_mono_aux]) 1);
   4.143 -qed "bag_of_mono";
   4.144 -AddIs [bag_of_mono];
   4.145 -
   4.146 -Goalw [mono1_def]
   4.147 - "mono1(list(A), prefix(A), Mult(A), MultLe(A,r), bag_of)";
   4.148 -by (auto_tac (claset(), simpset() addsimps [bag_of_type]));
   4.149 -qed "mono_bag_of";
   4.150 -Addsimps [mono_bag_of];
   4.151 -
   4.152 -
   4.153 -(** msetsum **)
   4.154 -
   4.155 -bind_thm("nat_into_Fin", eqpoll_refl RSN (2,thm"Fin_lemma"));
   4.156 -
   4.157 -Goal "l \\<in> list(A) ==> C Int length(l) \\<in> Fin(length(l))";
   4.158 -by (dtac length_type 1); 
   4.159 -by (rtac Fin_subset 1); 
   4.160 -by (rtac Int_lower2 1);
   4.161 -by (etac nat_into_Fin 1); 
   4.162 -qed "list_Int_length_Fin";
   4.163 -
   4.164 -
   4.165 -
   4.166 -Goal "[|xs \\<in> list(A); k \\<in> C \\<inter> length(xs)|] ==> k < length(xs)"; 
   4.167 -by (asm_full_simp_tac (simpset() addsimps [ltI]) 1); 
   4.168 -qed "mem_Int_imp_lt_length";
   4.169 -
   4.170 -
   4.171 -Goal "[|C \\<subseteq> nat; x \\<in> A; xs \\<in> list(A)|]  \
   4.172 -\ ==>  msetsum(\\<lambda>i. {#nth(i, xs @ [x])#}, C \\<inter> succ(length(xs)), A) = \
   4.173 -\      (if length(xs) \\<in> C then \
   4.174 -\         {#x#} +# msetsum(\\<lambda>x. {#nth(x, xs)#}, C \\<inter> length(xs), A) \
   4.175 -\       else msetsum(\\<lambda>x. {#nth(x, xs)#}, C \\<inter> length(xs), A))"; 
   4.176 -by (asm_full_simp_tac (simpset() addsimps [subsetD, nth_append, lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); 
   4.177 -by (asm_full_simp_tac (simpset() addsimps [Int_succ_right]) 1);
   4.178 -by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); 
   4.179 -by (Clarify_tac 1);
   4.180 -by (stac msetsum_cons 1);
   4.181 -by (rtac succI1 3);  
   4.182 -by (blast_tac (claset() addIs [list_Int_length_Fin, subset_succI RS Fin_mono RS subsetD]) 1); 
   4.183 -by (asm_full_simp_tac (simpset() addsimps [mem_not_refl]) 1); 
   4.184 -by (asm_full_simp_tac (simpset() addsimps [nth_type, lt_not_refl]) 1); 
   4.185 -by (blast_tac (claset() addIs [nat_into_Ord, ltI, length_type]) 1);
   4.186 -by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); 
   4.187 -qed "bag_of_sublist_lemma";
   4.188 -
   4.189 -Goal "l\\<in>list(A) ==> \
   4.190 -\ C <= nat ==> \
   4.191 -\ bag_of(sublist(l, C)) = \
   4.192 -\     msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
   4.193 -by (etac list_append_induct  1);
   4.194 -by (Simp_tac 1);
   4.195 -by (asm_simp_tac (simpset() addsimps [sublist_append, nth_append, 
   4.196 -          bag_of_sublist_lemma, munion_commute, bag_of_sublist_lemma, 
   4.197 -          msetsum_multiset, munion_0]) 1);  
   4.198 -qed "bag_of_sublist_lemma2";
   4.199 -
   4.200 -
   4.201 -Goal "l \\<in> list(A) ==> nat \\<inter> length(l) = length(l)";
   4.202 -by (rtac Int_absorb1 1);
   4.203 -by (rtac OrdmemD 1);  
   4.204 -by Auto_tac; 
   4.205 -qed "nat_Int_length_eq";
   4.206 -
   4.207 -(*eliminating the assumption C<=nat*)
   4.208 -Goal "l\\<in>list(A) ==> \
   4.209 -\ bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
   4.210 -by (subgoal_tac
   4.211 -      " bag_of(sublist(l, C Int nat)) = \
   4.212 -\     msetsum(%i. {#nth(i, l)#}, C Int length(l), A)" 1);
   4.213 -by (asm_full_simp_tac (simpset() addsimps [sublist_Int_eq]) 1); 
   4.214 -by (asm_full_simp_tac (simpset() addsimps [bag_of_sublist_lemma2, Int_lower2, Int_assoc, nat_Int_length_eq]) 1); 
   4.215 -qed "bag_of_sublist";
   4.216 -
   4.217 -Goal 
   4.218 -"l\\<in>list(A) ==> \
   4.219 -\ bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) = \
   4.220 -\     bag_of(sublist(l, B)) +# bag_of(sublist(l, C))";
   4.221 -by (subgoal_tac
   4.222 -      "B Int C Int length(l) = \
   4.223 -\      (B Int length(l)) Int (C Int length(l))" 1);
   4.224 -by (Blast_tac 2);
   4.225 -by (asm_simp_tac (simpset() addsimps [bag_of_sublist, 
   4.226 -                                      Int_Un_distrib2, msetsum_Un_Int]) 1); 
   4.227 -by (resolve_tac [msetsum_Un_Int] 1);
   4.228 -by (REPEAT (etac list_Int_length_Fin 1)); 
   4.229 - by (asm_full_simp_tac (simpset() addsimps [ltI, nth_type]) 1); 
   4.230 -qed "bag_of_sublist_Un_Int";
   4.231 -
   4.232 -
   4.233 -Goal "[| l\\<in>list(A); B Int C = 0  |]\
   4.234 -\     ==> bag_of(sublist(l, B Un C)) = \
   4.235 -\         bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"; 
   4.236 -by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym, 
   4.237 -                  sublist_type,  bag_of_multiset]) 1);
   4.238 -qed "bag_of_sublist_Un_disjoint";
   4.239 -
   4.240 -Goal "[|Finite(I); \\<forall>i\\<in>I. \\<forall>j\\<in>I. i\\<noteq>j --> A(i) \\<inter> A(j) = 0; \
   4.241 -\       l\\<in>list(B) |] \
   4.242 -\     ==> bag_of(sublist(l, \\<Union>i\\<in>I. A(i))) =  \
   4.243 -\         (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) ";  
   4.244 -by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
   4.245 -                            addsimps [bag_of_sublist]) 1);
   4.246 -by (stac (inst "A" "length(l)" msetsum_UN_disjoint) 1);
   4.247 -by (dresolve_tac [Finite_into_Fin] 1);
   4.248 -by (assume_tac 1);
   4.249 -by (Force_tac 3);
   4.250 -by (auto_tac (claset() addSIs [Fin_IntI2, Finite_into_Fin], 
   4.251 -              simpset() addsimps [ltI, nth_type, length_type, nat_into_Finite]));
   4.252 -qed_spec_mp "bag_of_sublist_UN_disjoint";
   4.253 -
   4.254 -
   4.255 -Goalw [part_ord_def, Lt_def, irrefl_def, trans_on_def]
   4.256 -  "part_ord(nat, Lt)";
   4.257 -by (auto_tac (claset() addIs [lt_trans], simpset()));
   4.258 -qed "part_ord_Lt";
   4.259 -Addsimps [part_ord_Lt];
   4.260 -
   4.261 -
   4.262 -(** all_distinct **)
   4.263 -
   4.264 -Goalw [all_distinct_def] "all_distinct(Nil)";
   4.265 -by Auto_tac;
   4.266 -qed "all_distinct_Nil";
   4.267 -
   4.268 -Goalw [all_distinct_def] 
   4.269 -"all_distinct(Cons(a, l)) <-> \
   4.270 -\ (a\\<in>set_of_list(l) --> False) & (a \\<notin> set_of_list(l) --> all_distinct(l))";
   4.271 -by (auto_tac (claset() addEs [list.elim], simpset()));
   4.272 -qed "all_distinct_Cons";
   4.273 -Addsimps [all_distinct_Nil, all_distinct_Cons];
   4.274 -
   4.275 -(** state_of **)
   4.276 -Goalw [state_of_def] "s\\<in>state ==> state_of(s)=s";
   4.277 -by Auto_tac;
   4.278 -qed "state_of_state";
   4.279 -Addsimps [state_of_state];
   4.280 -
   4.281 -
   4.282 -Goalw [state_of_def] "state_of(state_of(s))=state_of(s)";
   4.283 -by Auto_tac;
   4.284 -qed "state_of_idem";
   4.285 -Addsimps [state_of_idem];
   4.286 -
   4.287 -
   4.288 -Goalw [state_of_def] "state_of(s)\\<in>state";
   4.289 -by Auto_tac;
   4.290 -qed "state_of_type";
   4.291 -Addsimps [state_of_type];
   4.292 -AddTCs [state_of_type];
   4.293 -
   4.294 -Goalw [lift_def] "lift(x, s)=s`x";
   4.295 -by (Simp_tac 1);
   4.296 -qed "lift_apply";
   4.297 -Addsimps [lift_apply];
   4.298 -
   4.299 -(** Used in ClientImp **)
   4.300 -
   4.301 -Goalw [Increasing_def]
   4.302 -"Increasing(A, r, %s. f(state_of(s))) = \
   4.303 -\ Increasing(A, r, f)";
   4.304 -by Auto_tac;
   4.305 -qed "gen_Increains_state_of_eq";
   4.306 -bind_thm("Increasing_state_ofD1", 
   4.307 -gen_Increains_state_of_eq RS equalityD1 RS subsetD);
   4.308 -bind_thm("Increasing_state_ofD2", 
   4.309 -gen_Increains_state_of_eq RS equalityD2 RS subsetD);
   4.310 -
   4.311 -Goalw [Follows_def, Increasing_def] 
   4.312 -"Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) =  \
   4.313 -\ Follows(A, r, f, g)";
   4.314 -by Auto_tac;
   4.315 -qed "Follows_state_of_eq";
   4.316 -bind_thm("Follows_state_ofD1", Follows_state_of_eq RS equalityD1 RS subsetD);
   4.317 -bind_thm("Follows_state_ofD2", Follows_state_of_eq RS equalityD2 RS subsetD);
   4.318 -
   4.319 -(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
   4.320 -fun list_of_Int th = list_of_Int_aux (Drule.freeze_all th)
   4.321 -and list_of_Int_aux th =
   4.322 -    (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
   4.323 -    handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
   4.324 -    handle THM _ => (list_of_Int (th RS InterD))
   4.325 -    handle THM _ => (list_of_Int (th RS bspec))
   4.326 -    handle THM _ => [th];
   4.327 -
   4.328 -(*Used just once, for Alloc_Increasing*)
   4.329 -
   4.330 -fun normalize th = 
   4.331 -     normalize (th RS spec
   4.332 -                handle THM _ => th RS bspec
   4.333 -                handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
   4.334 -     handle THM _ => th;
   4.335 -
   4.336 -Goal "n\\<in>nat ==> nat_list_inj(n)\\<in>list(nat)";
   4.337 -by (induct_tac "n" 1);
   4.338 -by Auto_tac;
   4.339 -qed "nat_list_inj_type";
   4.340 -
   4.341 -Goal "n\\<in>nat ==> length(nat_list_inj(n)) = n";
   4.342 -by (induct_tac "n" 1);
   4.343 -by Auto_tac;
   4.344 -qed "length_nat_list_inj";
   4.345 -
   4.346 -Goalw [nat_var_inj_def]
   4.347 -  "(\\<lambda>x\\<in>nat. nat_var_inj(x))\\<in>inj(nat, var)";
   4.348 -by (res_inst_tac [("d", "var_inj")] lam_injective 1); 
   4.349 -by (asm_simp_tac (simpset() addsimps [length_nat_list_inj]) 2);
   4.350 -by (auto_tac (claset(), simpset() addsimps var.intrs@[nat_list_inj_type]));
   4.351 -qed "var_infinite_lemma";
   4.352 -
   4.353 -Goalw [lepoll_def] "nat lepoll var";
   4.354 -by (res_inst_tac [("x", "(\\<lambda>x\\<in>nat. nat_var_inj(x))")] exI 1);
   4.355 -by (rtac var_infinite_lemma 1);
   4.356 -qed "nat_lepoll_var";
   4.357 -
   4.358 -Goalw [Finite_def] "~Finite(var)";
   4.359 -by Auto_tac;
   4.360 -by (dtac eqpoll_imp_lepoll 1);
   4.361 -by (cut_facts_tac [nat_lepoll_var] 1);
   4.362 -by (subgoal_tac "nat lepoll x" 1);
   4.363 -by (blast_tac (claset() addIs [lepoll_trans]) 2);
   4.364 -by (dres_inst_tac [("i", "x"), ("A", "nat")] lepoll_cardinal_le 1);
   4.365 -by Auto_tac;
   4.366 -by (subgoal_tac "Card(nat)" 1);
   4.367 -by (rewrite_goal_tac [Card_def] 1);
   4.368 -by (dtac sym 1);
   4.369 -by Auto_tac;
   4.370 -by (dtac le_imp_subset 1);
   4.371 -by (dtac subsetD 1);
   4.372 -by (auto_tac (claset(), simpset() addsimps [Card_nat]));
   4.373 -by (blast_tac (claset() addEs [mem_irrefl]) 1);
   4.374 -qed "var_not_Finite";
   4.375 -
   4.376 -Goal "~Finite(A) ==> \\<exists>x. x\\<in>A";
   4.377 -by (etac swap 1);
   4.378 -by Auto_tac;
   4.379 -by (subgoal_tac "A=0" 1);
   4.380 -by (auto_tac (claset(), simpset() addsimps [Finite_0]));
   4.381 -qed "not_Finite_imp_exist";
   4.382 -
   4.383 -Goal "Finite(A) ==> b\\<in>(Inter(RepFun(var-A, B))) <-> (\\<forall>x\\<in>var-A. b\\<in>B(x))";
   4.384 -by (subgoal_tac "\\<exists>x. x\\<in>var-A" 1);
   4.385 -by Auto_tac;
   4.386 -by (subgoal_tac "~Finite(var-A)" 1);
   4.387 -by (dtac not_Finite_imp_exist 1);
   4.388 -by Auto_tac;
   4.389 -by (cut_facts_tac [var_not_Finite] 1);
   4.390 -by (etac swap  1);
   4.391 -by (res_inst_tac [("B", "A")] Diff_Finite 1);
   4.392 -by Auto_tac;
   4.393 -qed "Inter_Diff_var_iff";
   4.394 -
   4.395 -Goal "[| b\\<in>Inter(RepFun(var-A, B)); Finite(A); x\\<in>var-A |] ==> b\\<in>B(x)";
   4.396 -by (rotate_tac 1 1);
   4.397 -by (asm_full_simp_tac (simpset() addsimps [Inter_Diff_var_iff]) 1);
   4.398 -qed "Inter_var_DiffD";
   4.399 -
   4.400 -(* [| Finite(A); (\\<forall>x\\<in>var-A. b\\<in>B(x)) |] ==> b\\<in>Inter(RepFun(var-A, B)) *)
   4.401 -bind_thm("Inter_var_DiffI", Inter_Diff_var_iff RS iffD2);
   4.402 -
   4.403 -AddSIs [Inter_var_DiffI];
   4.404 -Addsimps [Finite_0, Finite_cons];
   4.405 -
   4.406 -Goal "Acts(F)<= A \\<inter> Pow(state*state)  <-> Acts(F)<=A";
   4.407 -by (cut_facts_tac [inst "F" "F" Acts_type] 1);
   4.408 -by Auto_tac;
   4.409 -qed "Acts_subset_Int_Pow_simp";
   4.410 -Addsimps [Acts_subset_Int_Pow_simp];
   4.411 -
   4.412 -(*for main zf?????*)
   4.413 -Goal "cons(x, A \\<inter> B) = cons(x, A) \\<inter> cons(x, B)";
   4.414 -by Auto_tac;
   4.415 -qed "cons_Int_distrib";
   4.416 -
   4.417 -
   4.418 -(* Currently not used, but of potential interest *)
   4.419 -Goal 
   4.420 -"[| Finite(A); \\<forall>x\\<in>A. g(x)\\<in>nat |] ==> \
   4.421 -\ setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)";
   4.422 -by (etac Finite_induct 1);
   4.423 -by (auto_tac (claset(), simpset() addsimps [int_of_add]));
   4.424 -qed "setsum_nsetsum_eq";
   4.425 -
   4.426 -Goal 
   4.427 -"[| A=B;  \\<forall>x\\<in>A. f(x)=g(x);  \\<forall>x\\<in>A. g(x)\\<in>nat; \
   4.428 -\     Finite(A) |]  ==> nsetsum(f, A) = nsetsum(g, B)";
   4.429 -by (subgoal_tac "$# nsetsum(f, A) = $# nsetsum(g, B)" 1);
   4.430 -by (rtac trans 2);
   4.431 -by (rtac setsum_nsetsum_eq 3);
   4.432 -by (rtac trans 2);
   4.433 -by (rtac (setsum_nsetsum_eq RS sym) 2);
   4.434 -by Auto_tac;
   4.435 -by (rtac setsum_cong 1);
   4.436 -by Auto_tac;
   4.437 -qed "nsetsum_cong";  
   4.438 -
   4.439 -
   4.440 -
   4.441 -
     5.1 --- a/src/ZF/UNITY/AllocBase.thy	Thu Jun 26 18:20:00 2003 +0200
     5.2 +++ b/src/ZF/UNITY/AllocBase.thy	Fri Jun 27 13:15:40 2003 +0200
     5.3 @@ -3,65 +3,65 @@
     5.4      Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     5.5      Copyright   2001  University of Cambridge
     5.6  
     5.7 -Common declarations for Chandy and Charpentier's Allocator
     5.8  *)
     5.9  
    5.10 -AllocBase = Follows + MultisetSum + Guar +
    5.11 +header{*Common declarations for Chandy and Charpentier's Allocator*}
    5.12 +
    5.13 +theory AllocBase = Follows + MultisetSum + Guar:
    5.14  
    5.15  consts
    5.16    tokbag   :: i  (* tokbags could be multisets...or any ordered type?*)
    5.17    NbT      :: i  (* Number of tokens in system *)
    5.18    Nclients :: i  (* Number of clients *)
    5.19 -translations
    5.20 -"tokbag" => "nat" 
    5.21 -rules
    5.22 -  NbT_pos  "NbT:nat-{0}"
    5.23 -  Nclients_pos "Nclients:nat-{0}"
    5.24 +
    5.25 +translations "tokbag" => "nat" 
    5.26 +
    5.27 +axioms
    5.28 +  NbT_pos:      "NbT \<in> nat-{0}"
    5.29 +  Nclients_pos: "Nclients \<in> nat-{0}"
    5.30    
    5.31 -(*This function merely sums the elements of a list*)
    5.32 -consts tokens     :: i =>i
    5.33 +text{*This function merely sums the elements of a list*}
    5.34 +consts tokens :: "i =>i"
    5.35         item :: i (* Items to be merged/distributed *)
    5.36  primrec 
    5.37    "tokens(Nil) = 0"
    5.38    "tokens (Cons(x,xs)) = x #+ tokens(xs)"
    5.39  
    5.40  consts
    5.41 -  bag_of :: i => i
    5.42 +  bag_of :: "i => i"
    5.43  
    5.44  primrec
    5.45    "bag_of(Nil)    = 0"
    5.46    "bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"
    5.47  
    5.48 -(* definitions needed in Client.thy *)
    5.49 -consts
    5.50 -  all_distinct0:: i=>i
    5.51 -  all_distinct:: i=>o
    5.52 -  
    5.53 -primrec
    5.54 +
    5.55 +text{*Definitions needed in Client.thy.  We define a recursive predicate
    5.56 +using 0 and 1 to code the truth values.*}
    5.57 +consts all_distinct0 :: "i=>i"
    5.58 + primrec
    5.59    "all_distinct0(Nil) = 1"
    5.60    "all_distinct0(Cons(a, l)) =
    5.61 -     (if a:set_of_list(l) then 0 else all_distinct0(l))"
    5.62 +     (if a \<in> set_of_list(l) then 0 else all_distinct0(l))"
    5.63  
    5.64 -defs
    5.65 -all_distinct_def
    5.66 -  "all_distinct(l) == all_distinct0(l)=1"
    5.67 +constdefs
    5.68 +  all_distinct  :: "i=>o"
    5.69 +   "all_distinct(l) == all_distinct0(l)=1"
    5.70    
    5.71  constdefs  
    5.72 -  (* coersion from anyting to state *)
    5.73 -  state_of :: i =>i
    5.74 -  "state_of(s) == if s:state then s else st0"
    5.75 +  state_of :: "i =>i" --{* coersion from anyting to state *}
    5.76 +   "state_of(s) == if s \<in> state then s else st0"
    5.77  
    5.78 -  (* simplifies the expression of programs  *)
    5.79 +  lift :: "i =>(i=>i)" --{* simplifies the expression of programs*}
    5.80 +   "lift(x) == %s. s`x"
    5.81  
    5.82 -  lift :: "i =>(i=>i)"
    5.83 -  "lift(x) == %s. s`x"
    5.84 +text{* function to show that the set of variables is infinite *}
    5.85 +consts
    5.86 +  nat_list_inj :: "i=>i"
    5.87 +  nat_var_inj  :: "i=>i"
    5.88 +  var_inj      :: "i=>i"
    5.89  
    5.90 -consts (* to show that the set of variables is infinite *)
    5.91 -  nat_list_inj :: i=>i
    5.92 -  nat_var_inj  :: i=>i
    5.93 -  var_inj :: i=>i
    5.94  defs
    5.95 -  nat_var_inj_def "nat_var_inj(n) == Var(nat_list_inj(n))"
    5.96 +  nat_var_inj_def: "nat_var_inj(n) == Var(nat_list_inj(n))"
    5.97  primrec
    5.98    "nat_list_inj(0) = Nil"
    5.99    "nat_list_inj(succ(n)) = Cons(n, nat_list_inj(n))"
   5.100 @@ -69,4 +69,343 @@
   5.101  primrec
   5.102    "var_inj(Var(l)) = length(l)"
   5.103  
   5.104 +
   5.105 +subsection{*Various simple lemmas*}
   5.106 +
   5.107 +lemma Nclients_NbT_gt_0 [simp]: "0 < Nclients & 0 < NbT"
   5.108 +apply (cut_tac Nclients_pos NbT_pos)
   5.109 +apply (auto intro: Ord_0_lt)
   5.110 +done
   5.111 +
   5.112 +lemma Nclients_NbT_not_0 [simp]: "Nclients \<noteq> 0 & NbT \<noteq> 0"
   5.113 +by (cut_tac Nclients_pos NbT_pos, auto)
   5.114 +
   5.115 +lemma Nclients_type [simp,TC]: "Nclients\<in>nat"
   5.116 +by (cut_tac Nclients_pos NbT_pos, auto)
   5.117 +
   5.118 +lemma NbT_type [simp,TC]: "NbT\<in>nat"
   5.119 +by (cut_tac Nclients_pos NbT_pos, auto)
   5.120 +
   5.121 +lemma INT_Nclient_iff [iff]:
   5.122 +     "b\<in>Inter(RepFun(Nclients, B)) <-> (\<forall>x\<in>Nclients. b\<in>B(x))"
   5.123 +apply (auto simp add: INT_iff)
   5.124 +apply (rule_tac x = 0 in exI)
   5.125 +apply (rule ltD, auto)
   5.126 +done
   5.127 +
   5.128 +lemma setsum_fun_mono [rule_format]:
   5.129 +     "n\<in>nat ==>  
   5.130 +      (\<forall>i\<in>nat. i<n --> f(i) $<= g(i)) -->  
   5.131 +      setsum(f, n) $<= setsum(g,n)"
   5.132 +apply (induct_tac "n", simp_all)
   5.133 +apply (subgoal_tac "Finite(x) & x\<notin>x")
   5.134 + prefer 2 apply (simp add: nat_into_Finite mem_not_refl, clarify)
   5.135 +apply (simp (no_asm_simp) add: succ_def)
   5.136 +apply (subgoal_tac "\<forall>i\<in>nat. i<x--> f(i) $<= g(i) ")
   5.137 + prefer 2 apply (force dest: leI) 
   5.138 +apply (rule zadd_zle_mono, simp_all)
   5.139 +done
   5.140 +
   5.141 +lemma tokens_type [simp,TC]: "l\<in>list(A) ==> tokens(l)\<in>nat"
   5.142 +by (erule list.induct, auto)
   5.143 +
   5.144 +lemma tokens_mono_aux [rule_format]:
   5.145 +     "xs\<in>list(A) ==> \<forall>ys\<in>list(A). <xs, ys>\<in>prefix(A)  
   5.146 +   --> tokens(xs) \<le> tokens(ys)"
   5.147 +apply (induct_tac "xs")
   5.148 +apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: prefix_def)
   5.149 +done
   5.150 +
   5.151 +lemma tokens_mono: "<xs, ys>\<in>prefix(A) ==> tokens(xs) \<le> tokens(ys)"
   5.152 +apply (cut_tac prefix_type)
   5.153 +apply (blast intro: tokens_mono_aux)
   5.154 +done
   5.155 +
   5.156 +lemma mono_tokens [iff]: "mono1(list(A), prefix(A), nat, Le,tokens)"
   5.157 +apply (unfold mono1_def)
   5.158 +apply (auto intro: tokens_mono simp add: Le_def)
   5.159 +done
   5.160 +
   5.161 +lemma tokens_append [simp]: 
   5.162 +"[| xs\<in>list(A); ys\<in>list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)"
   5.163 +apply (induct_tac "xs", auto)
   5.164 +done
   5.165 +
   5.166 +subsection{*The function @{term bag_of}*}
   5.167 +
   5.168 +lemma bag_of_type [simp,TC]: "l\<in>list(A) ==>bag_of(l)\<in>Mult(A)"
   5.169 +apply (induct_tac "l")
   5.170 +apply (auto simp add: Mult_iff_multiset)
   5.171 +done
   5.172 +
   5.173 +lemma bag_of_multiset:
   5.174 +     "l\<in>list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A"
   5.175 +apply (drule bag_of_type)
   5.176 +apply (auto simp add: Mult_iff_multiset)
   5.177 +done
   5.178 +
   5.179 +lemma bag_of_append [simp]:
   5.180 +    "[| xs\<in>list(A); ys\<in>list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)"
   5.181 +apply (induct_tac "xs")
   5.182 +apply (auto simp add: bag_of_multiset munion_assoc)
   5.183 +done
   5.184 +
   5.185 +lemma bag_of_mono_aux [rule_format]:
   5.186 +     "xs\<in>list(A) ==> \<forall>ys\<in>list(A). <xs, ys>\<in>prefix(A)  
   5.187 +      --> <bag_of(xs), bag_of(ys)>\<in>MultLe(A, r)"
   5.188 +apply (induct_tac "xs", simp_all, clarify) 
   5.189 +apply (frule_tac l = ys in bag_of_multiset)
   5.190 +apply (auto intro: empty_le_MultLe simp add: prefix_def)
   5.191 +apply (rule munion_mono)
   5.192 +apply (force simp add: MultLe_def Mult_iff_multiset)
   5.193 +apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
   5.194 +done
   5.195 +
   5.196 +lemma bag_of_mono [intro]:
   5.197 +     "[|  <xs, ys>\<in>prefix(A); xs\<in>list(A); ys\<in>list(A) |]
   5.198 +      ==> <bag_of(xs), bag_of(ys)>\<in>MultLe(A, r)"
   5.199 +apply (blast intro: bag_of_mono_aux)
   5.200 +done
   5.201 +
   5.202 +lemma mono_bag_of [simp]: 
   5.203 +     "mono1(list(A), prefix(A), Mult(A), MultLe(A,r), bag_of)"
   5.204 +by (auto simp add:  mono1_def bag_of_type)
   5.205 +
   5.206 +
   5.207 +subsection{*The function @{term msetsum}*}
   5.208 +
   5.209 +lemmas nat_into_Fin = eqpoll_refl [THEN [2] Fin_lemma]
   5.210 +
   5.211 +lemma list_Int_length_Fin: "l \<in> list(A) ==> C Int length(l) \<in> Fin(length(l))"
   5.212 +apply (drule length_type)
   5.213 +apply (rule Fin_subset)
   5.214 +apply (rule Int_lower2)
   5.215 +apply (erule nat_into_Fin)
   5.216 +done
   5.217 +
   5.218 +
   5.219 +
   5.220 +lemma mem_Int_imp_lt_length:
   5.221 +     "[|xs \<in> list(A); k \<in> C \<inter> length(xs)|] ==> k < length(xs)"
   5.222 +apply (simp add: ltI)
   5.223 +done
   5.224 +
   5.225 +
   5.226 +lemma bag_of_sublist_lemma:
   5.227 +     "[|C \<subseteq> nat; x \<in> A; xs \<in> list(A)|]   
   5.228 +  ==>  msetsum(\<lambda>i. {#nth(i, xs @ [x])#}, C \<inter> succ(length(xs)), A) =  
   5.229 +       (if length(xs) \<in> C then  
   5.230 +          {#x#} +# msetsum(\<lambda>x. {#nth(x, xs)#}, C \<inter> length(xs), A)  
   5.231 +        else msetsum(\<lambda>x. {#nth(x, xs)#}, C \<inter> length(xs), A))"
   5.232 +apply (simp add: subsetD nth_append lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong)
   5.233 +apply (simp add: Int_succ_right)
   5.234 +apply (simp add: lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong, clarify)
   5.235 +apply (subst msetsum_cons)
   5.236 +apply (rule_tac [3] succI1)
   5.237 +apply (blast intro: list_Int_length_Fin subset_succI [THEN Fin_mono, THEN subsetD])
   5.238 +apply (simp add: mem_not_refl)
   5.239 +apply (simp add: nth_type lt_not_refl)
   5.240 +apply (blast intro: nat_into_Ord ltI length_type)
   5.241 +apply (simp add: lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong)
   5.242 +done
   5.243 +
   5.244 +lemma bag_of_sublist_lemma2:
   5.245 +     "l\<in>list(A) ==>  
   5.246 +  C <= nat ==>  
   5.247 +  bag_of(sublist(l, C)) =  
   5.248 +      msetsum(%i. {#nth(i, l)#}, C Int length(l), A)"
   5.249 +apply (erule list_append_induct)
   5.250 +apply (simp (no_asm))
   5.251 +apply (simp (no_asm_simp) add: sublist_append nth_append bag_of_sublist_lemma munion_commute bag_of_sublist_lemma msetsum_multiset munion_0)
   5.252 +done
   5.253 +
   5.254 +
   5.255 +lemma nat_Int_length_eq: "l \<in> list(A) ==> nat \<inter> length(l) = length(l)"
   5.256 +apply (rule Int_absorb1)
   5.257 +apply (rule OrdmemD, auto)
   5.258 +done
   5.259 +
   5.260 +(*eliminating the assumption C<=nat*)
   5.261 +lemma bag_of_sublist:
   5.262 +     "l\<in>list(A) ==>  
   5.263 +  bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)"
   5.264 +apply (subgoal_tac " bag_of (sublist (l, C Int nat)) = msetsum (%i. {#nth (i, l) #}, C Int length (l), A) ")
   5.265 +apply (simp add: sublist_Int_eq)
   5.266 +apply (simp add: bag_of_sublist_lemma2 Int_lower2 Int_assoc nat_Int_length_eq)
   5.267 +done
   5.268 +
   5.269 +lemma bag_of_sublist_Un_Int: 
   5.270 +"l\<in>list(A) ==>  
   5.271 +  bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) =  
   5.272 +      bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"
   5.273 +apply (subgoal_tac "B Int C Int length (l) = (B Int length (l)) Int (C Int length (l))")
   5.274 +prefer 2 apply blast
   5.275 +apply (simp (no_asm_simp) add: bag_of_sublist Int_Un_distrib2 msetsum_Un_Int)
   5.276 +apply (rule msetsum_Un_Int)
   5.277 +apply (erule list_Int_length_Fin)+
   5.278 + apply (simp add: ltI nth_type)
   5.279 +done
   5.280 +
   5.281 +
   5.282 +lemma bag_of_sublist_Un_disjoint:
   5.283 +     "[| l\<in>list(A); B Int C = 0  |] 
   5.284 +      ==> bag_of(sublist(l, B Un C)) =  
   5.285 +          bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"
   5.286 +by (simp add: bag_of_sublist_Un_Int [symmetric] bag_of_multiset)
   5.287 +
   5.288 +
   5.289 +lemma bag_of_sublist_UN_disjoint [rule_format]:
   5.290 +     "[|Finite(I); \<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j --> A(i) \<inter> A(j) = 0;  
   5.291 +        l\<in>list(B) |]  
   5.292 +      ==> bag_of(sublist(l, \<Union>i\<in>I. A(i))) =   
   5.293 +          (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) "
   5.294 +apply (simp (no_asm_simp) del: UN_simps
   5.295 +           add: UN_simps [symmetric] bag_of_sublist)
   5.296 +apply (subst  msetsum_UN_disjoint [of _ _ _ "length (l)"])
   5.297 +apply (drule Finite_into_Fin, assumption)
   5.298 +prefer 3 apply force
   5.299 +apply (auto intro!: Fin_IntI2 Finite_into_Fin simp add: ltI nth_type length_type nat_into_Finite)
   5.300 +done
   5.301 +
   5.302 +
   5.303 +lemma part_ord_Lt [simp]: "part_ord(nat, Lt)"
   5.304 +apply (unfold part_ord_def Lt_def irrefl_def trans_on_def)
   5.305 +apply (auto intro: lt_trans)
   5.306 +done
   5.307 +
   5.308 +subsubsection{*The function @{term all_distinct}*}
   5.309 +
   5.310 +lemma all_distinct_Nil [simp]: "all_distinct(Nil)"
   5.311 +by (unfold all_distinct_def, auto)
   5.312 +
   5.313 +lemma all_distinct_Cons [simp]: 
   5.314 +    "all_distinct(Cons(a,l)) <->  
   5.315 +      (a\<in>set_of_list(l) --> False) & (a \<notin> set_of_list(l) --> all_distinct(l))"
   5.316 +apply (unfold all_distinct_def)
   5.317 +apply (auto elim: list.cases)
   5.318 +done
   5.319 +
   5.320 +subsubsection{*The function @{term state_of}*}
   5.321 +
   5.322 +lemma state_of_state: "s\<in>state ==> state_of(s)=s"
   5.323 +by (unfold state_of_def, auto)
   5.324 +declare state_of_state [simp]
   5.325 +
   5.326 +
   5.327 +lemma state_of_idem: "state_of(state_of(s))=state_of(s)"
   5.328 +
   5.329 +apply (unfold state_of_def, auto)
   5.330 +done
   5.331 +declare state_of_idem [simp]
   5.332 +
   5.333 +
   5.334 +lemma state_of_type [simp,TC]: "state_of(s)\<in>state"
   5.335 +by (unfold state_of_def, auto)
   5.336 +
   5.337 +lemma lift_apply [simp]: "lift(x, s)=s`x"
   5.338 +by (simp add: lift_def)
   5.339 +
   5.340 +
   5.341 +(** Used in ClientImp **)
   5.342 +
   5.343 +lemma gen_Increains_state_of_eq: 
   5.344 +     "Increasing(A, r, %s. f(state_of(s))) = Increasing(A, r, f)"
   5.345 +apply (unfold Increasing_def, auto)
   5.346 +done
   5.347 +
   5.348 +lemmas Increasing_state_ofD1 =  
   5.349 +      gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD, standard]
   5.350 +lemmas Increasing_state_ofD2 =  
   5.351 +      gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD, standard]
   5.352 +
   5.353 +lemma Follows_state_of_eq: 
   5.354 +     "Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) =   
   5.355 +      Follows(A, r, f, g)"
   5.356 +apply (unfold Follows_def Increasing_def, auto)
   5.357 +done
   5.358 +
   5.359 +lemmas Follows_state_ofD1 =
   5.360 +      Follows_state_of_eq [THEN equalityD1, THEN subsetD, standard]
   5.361 +lemmas Follows_state_ofD2 =
   5.362 +      Follows_state_of_eq [THEN equalityD2, THEN subsetD, standard]
   5.363 +
   5.364 +lemma nat_list_inj_type: "n\<in>nat ==> nat_list_inj(n)\<in>list(nat)"
   5.365 +by (induct_tac "n", auto)
   5.366 +
   5.367 +lemma length_nat_list_inj: "n\<in>nat ==> length(nat_list_inj(n)) = n"
   5.368 +by (induct_tac "n", auto)
   5.369 +
   5.370 +lemma var_infinite_lemma: 
   5.371 +  "(\<lambda>x\<in>nat. nat_var_inj(x))\<in>inj(nat, var)"
   5.372 +apply (unfold nat_var_inj_def)
   5.373 +apply (rule_tac d = var_inj in lam_injective)
   5.374 +apply (auto simp add: var.intros nat_list_inj_type)
   5.375 +apply (simp add: length_nat_list_inj)
   5.376 +done
   5.377 +
   5.378 +lemma nat_lepoll_var: "nat lepoll var"
   5.379 +apply (unfold lepoll_def)
   5.380 +apply (rule_tac x = " (\<lambda>x\<in>nat. nat_var_inj (x))" in exI)
   5.381 +apply (rule var_infinite_lemma)
   5.382 +done
   5.383 +
   5.384 +(*Surely a simpler proof uses lepoll_Finite and the following lemma:*)
   5.385 +
   5.386 +    (*????Cardinal*)
   5.387 +    lemma nat_not_Finite: "~Finite(nat)"
   5.388 +    apply (unfold Finite_def, clarify) 
   5.389 +    apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp) 
   5.390 +    apply (insert Card_nat) 
   5.391 +    apply (simp add: Card_def)
   5.392 +    apply (drule le_imp_subset)
   5.393 +    apply (blast elim: mem_irrefl)
   5.394 +    done
   5.395 +
   5.396 +lemma var_not_Finite: "~Finite(var)"
   5.397 +apply (insert nat_not_Finite) 
   5.398 +apply (blast intro: lepoll_Finite [OF 	nat_lepoll_var]) 
   5.399 +done
   5.400 +
   5.401 +lemma not_Finite_imp_exist: "~Finite(A) ==> \<exists>x. x\<in>A"
   5.402 +apply (subgoal_tac "A\<noteq>0")
   5.403 +apply (auto simp add: Finite_0)
   5.404 +done
   5.405 +
   5.406 +lemma Inter_Diff_var_iff:
   5.407 +     "Finite(A) ==> b\<in>(Inter(RepFun(var-A, B))) <-> (\<forall>x\<in>var-A. b\<in>B(x))"
   5.408 +apply (subgoal_tac "\<exists>x. x\<in>var-A", auto)
   5.409 +apply (subgoal_tac "~Finite (var-A) ")
   5.410 +apply (drule not_Finite_imp_exist, auto)
   5.411 +apply (cut_tac var_not_Finite)
   5.412 +apply (erule swap)
   5.413 +apply (rule_tac B = A in Diff_Finite, auto)
   5.414 +done
   5.415 +
   5.416 +lemma Inter_var_DiffD:
   5.417 +     "[| b\<in>Inter(RepFun(var-A, B)); Finite(A); x\<in>var-A |] ==> b\<in>B(x)"
   5.418 +by (simp add: Inter_Diff_var_iff)
   5.419 +
   5.420 +(* [| Finite(A); (\<forall>x\<in>var-A. b\<in>B(x)) |] ==> b\<in>Inter(RepFun(var-A, B)) *)
   5.421 +lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2, standard]
   5.422 +
   5.423 +declare Inter_var_DiffI [intro!]
   5.424 +
   5.425 +lemma Acts_subset_Int_Pow_simp [simp]:
   5.426 +     "Acts(F)<= A \<inter> Pow(state*state)  <-> Acts(F)<=A"
   5.427 +by (insert Acts_type [of F], auto)
   5.428 +
   5.429 +lemma setsum_nsetsum_eq: 
   5.430 +     "[| Finite(A); \<forall>x\<in>A. g(x)\<in>nat |] 
   5.431 +      ==> setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)"
   5.432 +apply (erule Finite_induct)
   5.433 +apply (auto simp add: int_of_add)
   5.434 +done
   5.435 +
   5.436 +lemma nsetsum_cong: 
   5.437 +     "[| A=B;  \<forall>x\<in>A. f(x)=g(x);  \<forall>x\<in>A. g(x)\<in>nat;  Finite(A) |]  
   5.438 +      ==> nsetsum(f, A) = nsetsum(g, B)"
   5.439 +apply (subgoal_tac "$# nsetsum (f, A) = $# nsetsum (g, B)", simp)
   5.440 +apply (simp add: setsum_nsetsum_eq [symmetric] cong: setsum_cong) 
   5.441 +done
   5.442 +
   5.443  end
     6.1 --- a/src/ZF/UNITY/AllocImpl.thy	Thu Jun 26 18:20:00 2003 +0200
     6.2 +++ b/src/ZF/UNITY/AllocImpl.thy	Fri Jun 27 13:15:40 2003 +0200
     6.3 @@ -394,10 +394,11 @@
     6.4  apply (simp_all add: refl_prefix Le_def comp_def length_type)
     6.5  done
     6.6  
     6.7 -(* Lemma 51, page 29.
     6.8 +
     6.9 +text{*Lemma 51, page 29.
    6.10    This theorem states as invariant that if the number of
    6.11    tokens given does not exceed the number returned, then the upper limit
    6.12 -  (NbT) does not exceed the number currently available.*)
    6.13 +  (@{term NbT}) does not exceed the number currently available.*}
    6.14  lemma alloc_prog_Always_lemma:
    6.15  "[| G \<in> program; alloc_prog ok G;
    6.16      alloc_prog \<squnion> G \<in> Incr(lift(ask));
    6.17 @@ -405,22 +406,24 @@
    6.18    ==> alloc_prog \<squnion> G \<in>
    6.19          Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) -->
    6.20                  NbT \<le> s`available_tok})"
    6.21 -apply (subgoal_tac "alloc_prog \<squnion> 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))}) ")
    6.22 +apply (subgoal_tac
    6.23 +       "alloc_prog \<squnion> G
    6.24 +          \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter>
    6.25 +                    {s\<in>state. s`available_tok #+ tokens(s`giv) = 
    6.26 +                              NbT #+ tokens(take (s`NbR, s`rel))})")
    6.27  apply (rule_tac [2] AlwaysI)
    6.28  apply (rule_tac [3] giv_Bounded_lemma2, auto)
    6.29  apply (rule Always_weaken, assumption, auto)
    6.30  apply (subgoal_tac "0 \<le> tokens(take (x ` NbR, x ` rel)) #- tokens(x`giv) ")
    6.31 -apply (rule_tac [2] nat_diff_split [THEN iffD2])
    6.32 - prefer 2 apply force
    6.33 + prefer 2 apply (force)
    6.34  apply (subgoal_tac "x`available_tok =
    6.35                      NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
    6.36 -apply (simp (no_asm_simp))
    6.37 -apply (rule nat_diff_split [THEN iffD2], auto)
    6.38 -apply (drule_tac j = "tokens(x ` giv)" in lt_trans2)
    6.39 -apply assumption
    6.40 -apply auto
    6.41 +apply (simp add: );
    6.42 +apply (auto split add: nat_diff_split dest: lt_trans2)
    6.43  done
    6.44  
    6.45 +
    6.46 +
    6.47  subsubsection{* Main lemmas towards proving property (31)*}
    6.48  
    6.49  lemma LeadsTo_strength_R:
     7.1 --- a/src/ZF/UNITY/Guar.ML	Thu Jun 26 18:20:00 2003 +0200
     7.2 +++ b/src/ZF/UNITY/Guar.ML	Fri Jun 27 13:15:40 2003 +0200
     7.3 @@ -34,7 +34,7 @@
     7.4  by (ALLGOALS(asm_full_simp_tac 
     7.5           (simpset() addsimps [OK_cons_iff])));
     7.6  (* Auto_tac proves the goal in one step *)
     7.7 -by Safe_tac;
     7.8 +by (safe_tac (claset() addSEs [not_emptyE]));
     7.9  by (ALLGOALS(Asm_full_simp_tac));
    7.10  by (Fast_tac 1);
    7.11  qed_spec_mp "ex1";
     8.1 --- a/src/ZF/UNITY/Merge.thy	Thu Jun 26 18:20:00 2003 +0200
     8.2 +++ b/src/ZF/UNITY/Merge.thy	Fri Jun 27 13:15:40 2003 +0200
     8.3 @@ -87,14 +87,12 @@
     8.4  
     8.5  lemma (in merge) Out_value_type [TC,simp]: "s \<in> state ==> s`Out \<in> list(A)"
     8.6  apply (unfold state_def)
     8.7 -apply (drule_tac a = "Out" in apply_type)
     8.8 -apply auto
     8.9 +apply (drule_tac a = Out in apply_type, auto)
    8.10  done
    8.11  
    8.12  lemma (in merge) iOut_value_type [TC,simp]: "s \<in> state ==> s`iOut \<in> list(nat)"
    8.13  apply (unfold state_def)
    8.14 -apply (drule_tac a = "iOut" in apply_type)
    8.15 -apply auto
    8.16 +apply (drule_tac a = iOut in apply_type, auto)
    8.17  done
    8.18  
    8.19  lemma (in merge) M_in_program [intro,simp]: "M \<in> program"
    8.20 @@ -123,7 +121,7 @@
    8.21        ==> M \<squnion> G \<in> Always({s \<in> state. length(s`Out)=length(s`iOut)})"
    8.22  apply (frule preserves_type [THEN subsetD])
    8.23  apply (subgoal_tac "G \<in> program")
    8.24 - prefer 2 apply (assumption)
    8.25 + prefer 2 apply assumption
    8.26  apply (frule M_ok_iff)
    8.27  apply (cut_tac merge_spec)
    8.28  apply (force dest: guaranteesD simp add: merge_spec_def merge_eq_Out_def)
    8.29 @@ -148,8 +146,7 @@
    8.30                     Nclients, A) = bag_of(s`Out)})"
    8.31  apply (rule Always_Diff_Un_eq [THEN iffD1]) 
    8.32  apply (rule_tac [2] state_AlwaysI [THEN Always_weaken]) 
    8.33 -apply (rule Always_Int_I [OF merge_Always_Out_eq_iOut merge_Bounded]) 
    8.34 -apply auto
    8.35 +apply (rule Always_Int_I [OF merge_Always_Out_eq_iOut merge_Bounded], auto)
    8.36  apply (subst bag_of_sublist_UN_disjoint [symmetric])
    8.37  apply (auto simp add: nat_into_Finite set_of_list_conv_nth  [OF iOut_value_type])
    8.38  apply (subgoal_tac " (\<Union>i \<in> Nclients. {k \<in> nat. k < length (x`iOut) & nth (k, x`iOut) = i}) = length (x`iOut) ")
    8.39 @@ -158,10 +155,9 @@
    8.40                        take_all [OF _ Out_value_type] 
    8.41                        length_type [OF iOut_value_type])
    8.42  apply (rule equalityI)
    8.43 -apply (blast dest: ltD)
    8.44 -apply clarify
    8.45 +apply (blast dest: ltD, clarify)
    8.46  apply (subgoal_tac "length (x ` iOut) \<in> nat")
    8.47 - prefer 2 apply (simp add: length_type [OF iOut_value_type]); 
    8.48 + prefer 2 apply (simp add: length_type [OF iOut_value_type]) 
    8.49  apply (subgoal_tac "xa \<in> nat")
    8.50  apply (simp_all add: Ord_mem_iff_lt)
    8.51  prefer 2 apply (blast intro: lt_trans)
    8.52 @@ -177,19 +173,15 @@
    8.53        (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)"
    8.54  apply (cut_tac merge_spec)
    8.55  apply (rule merge_bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI])
    8.56 -     apply (simp_all add: M_ok_iff)
    8.57 -apply clarify
    8.58 +     apply (simp_all add: M_ok_iff, clarify)
    8.59  apply (rule Follows_state_ofD1 [OF Follows_msetsum_UN])
    8.60     apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
    8.61 -apply (simp add: INT_iff merge_spec_def merge_follows_def)
    8.62 -apply clarify
    8.63 +apply (simp add: INT_iff merge_spec_def merge_follows_def, clarify)
    8.64  apply (cut_tac merge_spec)
    8.65  apply (subgoal_tac "M ok G")
    8.66   prefer 2 apply (force intro: M_ok_iff [THEN iffD2])
    8.67 -apply (drule guaranteesD)
    8.68 -apply assumption
    8.69 -  apply (simp add: merge_spec_def merge_follows_def)
    8.70 - apply blast
    8.71 +apply (drule guaranteesD, assumption)
    8.72 +  apply (simp add: merge_spec_def merge_follows_def, blast)
    8.73  apply (simp cong add: Follows_cong
    8.74      add: refl_prefix
    8.75         mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
     9.1 --- a/src/ZF/UNITY/Union.ML	Thu Jun 26 18:20:00 2003 +0200
     9.2 +++ b/src/ZF/UNITY/Union.ML	Fri Jun 27 13:15:40 2003 +0200
     9.3 @@ -164,12 +164,11 @@
     9.4  by Auto_tac;
     9.5  qed "JN_empty";
     9.6  AddIffs [JN_empty];
     9.7 -AddSEs [not_emptyE];
     9.8  Addsimps [Inter_0];
     9.9  
    9.10  Goal "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))";
    9.11  by (simp_tac (simpset() addsimps [JOIN_def]) 1);
    9.12 -by (auto_tac (claset(), simpset() addsimps [INT_Int_distrib]));
    9.13 +by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [INT_Int_distrib]));
    9.14  qed "Init_JN";
    9.15  
    9.16  Goalw [JOIN_def]
    9.17 @@ -183,7 +182,7 @@
    9.18  "AllowedActs(JN i:I. F(i)) = (if I=0 then Pow(state*state) else (INT i:I. AllowedActs(F(i))))";
    9.19  by Auto_tac;
    9.20  by (rtac equalityI 1);
    9.21 -by (auto_tac (claset() addDs [AllowedActs_type RS subsetD], simpset()));
    9.22 +by (auto_tac (claset()  addSEs [not_emptyE] addDs [AllowedActs_type RS subsetD], simpset()));
    9.23  qed "AllowedActs_JN";
    9.24  AddIffs [Init_JN, Acts_JN, AllowedActs_JN];
    9.25  
    9.26 @@ -225,22 +224,21 @@
    9.27  Goal "(JN i:I. F(i) Join G(i)) = (JN i:I. F(i))  Join  (JN i:I. G(i))";
    9.28  by (rtac program_equalityI 1);
    9.29  by (ALLGOALS(simp_tac (simpset() addsimps [Int_absorb])));
    9.30 -by Safe_tac;
    9.31 +by (safe_tac (claset() addSEs [not_emptyE]));
    9.32  by (ALLGOALS(asm_full_simp_tac (simpset() addsimps 
    9.33                [INT_Int_distrib, Int_absorb])));
    9.34  by (Force_tac 1);
    9.35  qed "JN_Join_distrib";
    9.36  
    9.37  Goal "(JN i:I. F(i) Join G) = ((JN i:I. F(i) Join G))";
    9.38 -by (asm_simp_tac (simpset() 
    9.39 -    addsimps [JN_Join_distrib, JN_constant]) 1);
    9.40 +by (asm_simp_tac (simpset() addsimps [JN_Join_distrib, JN_constant]) 1);
    9.41  qed "JN_Join_miniscope";
    9.42  
    9.43  (*Used to prove guarantees_JN_I*)
    9.44  
    9.45  Goal "i:I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)";
    9.46  by (rtac program_equalityI 1);
    9.47 -by Auto_tac;
    9.48 +by (auto_tac (claset() addSEs [not_emptyE], simpset()));
    9.49  qed "JN_Join_diff";
    9.50  
    9.51  (*** Safety: co, stable, FP ***)
    9.52 @@ -309,9 +307,7 @@
    9.53  val [major, minor] = Goalw [initially_def]
    9.54   "[| (!!i. i:I ==>F(i):initially(A)); i:I |] ==> (JN i:I. F(i)):initially(A)";
    9.55  by (cut_facts_tac [minor] 1);
    9.56 -by (Asm_full_simp_tac 1);
    9.57 -by Safe_tac;
    9.58 -by (asm_full_simp_tac (simpset() addsimps [Inter_iff]) 1);
    9.59 +by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [Inter_iff]));
    9.60  by (forw_inst_tac [("i", "x")] major 1);
    9.61  by Auto_tac;
    9.62  qed "initially_JN_I";
    9.63 @@ -500,13 +496,13 @@
    9.64  qed "ok_Join_commute_I";
    9.65  
    9.66  Goal "F ok JOIN(I,G) <-> (ALL i:I. F ok G(i))";
    9.67 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
    9.68 +by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [ok_def]));
    9.69  by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
    9.70  qed "ok_JN_iff1";
    9.71  
    9.72  
    9.73  Goal "JOIN(I,G) ok F   <->  (ALL i:I. G(i) ok F)";
    9.74 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
    9.75 +by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [ok_def]));
    9.76  by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
    9.77  qed "ok_JN_iff2";
    9.78  AddIffs [ok_JN_iff1, ok_JN_iff2];
    10.1 --- a/src/ZF/ZF.thy	Thu Jun 26 18:20:00 2003 +0200
    10.2 +++ b/src/ZF/ZF.thy	Fri Jun 27 13:15:40 2003 +0200
    10.3 @@ -2,41 +2,43 @@
    10.4      ID:         $Id$
    10.5      Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
    10.6      Copyright   1993  University of Cambridge
    10.7 +*)
    10.8  
    10.9 -Zermelo-Fraenkel Set Theory
   10.10 -*)
   10.11 +header{*Zermelo-Fraenkel Set Theory*}
   10.12  
   10.13  theory ZF = FOL:
   10.14  
   10.15  global
   10.16  
   10.17 -typedecl
   10.18 -  i
   10.19 -
   10.20 -arities
   10.21 -  i :: "term"
   10.22 +typedecl i
   10.23 +arities  i :: "term"
   10.24  
   10.25  consts
   10.26  
   10.27 -  "0"         :: "i"                  ("0")   (*the empty set*)
   10.28 -  Pow         :: "i => i"                     (*power sets*)
   10.29 -  Inf         :: "i"                          (*infinite set*)
   10.30 +  "0"         :: "i"                  ("0")   --{*the empty set*}
   10.31 +  Pow         :: "i => i"                     --{*power sets*}
   10.32 +  Inf         :: "i"                          --{*infinite set*}
   10.33  
   10.34 -  (* Bounded Quantifiers *)
   10.35 +text {*Bounded Quantifiers *}
   10.36 +consts
   10.37    Ball   :: "[i, i => o] => o"
   10.38    Bex   :: "[i, i => o] => o"
   10.39  
   10.40 -  (* General Union and Intersection *)
   10.41 +text {*General Union and Intersection *}
   10.42 +consts
   10.43    Union :: "i => i"
   10.44    Inter :: "i => i"
   10.45  
   10.46 -  (* Variations on Replacement *)
   10.47 +text {*Variations on Replacement *}
   10.48 +consts
   10.49    PrimReplace :: "[i, [i, i] => o] => i"
   10.50    Replace     :: "[i, [i, i] => o] => i"
   10.51    RepFun      :: "[i, i => i] => i"
   10.52    Collect     :: "[i, i => o] => i"
   10.53  
   10.54 -  (* Descriptions *)
   10.55 +
   10.56 +text {*Descriptions *}
   10.57 +consts
   10.58    The         :: "(i => o) => i"      (binder "THE " 10)
   10.59    If          :: "[o, i, i] => i"     ("(if (_)/ then (_)/ else (_))" [10] 10)
   10.60  
   10.61 @@ -47,46 +49,49 @@
   10.62    "if(P,a,b)" => "If(P,a,b)"
   10.63  
   10.64  
   10.65 +
   10.66 +text {*Finite Sets *}
   10.67  consts
   10.68 -
   10.69 -  (* Finite Sets *)
   10.70    Upair :: "[i, i] => i"
   10.71    cons  :: "[i, i] => i"
   10.72    succ  :: "i => i"
   10.73  
   10.74 -  (* Ordered Pairing *)
   10.75 +text {*Ordered Pairing *}
   10.76 +consts
   10.77    Pair  :: "[i, i] => i"
   10.78    fst   :: "i => i"
   10.79    snd   :: "i => i"
   10.80 -  split :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
   10.81 +  split :: "[[i, i] => 'a, i] => 'a::logic"  --{*for pattern-matching*}
   10.82  
   10.83 -  (* Sigma and Pi Operators *)
   10.84 +text {*Sigma and Pi Operators *}
   10.85 +consts
   10.86    Sigma :: "[i, i => i] => i"
   10.87    Pi    :: "[i, i => i] => i"
   10.88  
   10.89 -  (* Relations and Functions *)
   10.90 -
   10.91 -  "domain"      :: "i => i"
   10.92 +text {*Relations and Functions *}
   10.93 +consts
   10.94 +  "domain"    :: "i => i"
   10.95    range       :: "i => i"
   10.96    field       :: "i => i"
   10.97    converse    :: "i => i"
   10.98 -  relation    :: "i => o"         (*recognizes sets of pairs*)
   10.99 -  function    :: "i => o"         (*recognizes functions; can have non-pairs*)
  10.100 +  relation    :: "i => o"        --{*recognizes sets of pairs*}
  10.101 +  function    :: "i => o"        --{*recognizes functions; can have non-pairs*}
  10.102    Lambda      :: "[i, i => i] => i"
  10.103    restrict    :: "[i, i] => i"
  10.104  
  10.105 -  (* Infixes in order of decreasing precedence *)
  10.106 +text {*Infixes in order of decreasing precedence *}
  10.107 +consts
  10.108  
  10.109 -  "``"        :: "[i, i] => i"    (infixl 90) (*image*)
  10.110 -  "-``"       :: "[i, i] => i"    (infixl 90) (*inverse image*)
  10.111 -  "`"         :: "[i, i] => i"    (infixl 90) (*function application*)
  10.112 +  "``"        :: "[i, i] => i"    (infixl 90) --{*image*}
  10.113 +  "-``"       :: "[i, i] => i"    (infixl 90) --{*inverse image*}
  10.114 +  "`"         :: "[i, i] => i"    (infixl 90) --{*function application*}
  10.115  (*"*"         :: "[i, i] => i"    (infixr 80) [virtual] Cartesian product*)
  10.116 -  "Int"       :: "[i, i] => i"    (infixl 70) (*binary intersection*)
  10.117 -  "Un"        :: "[i, i] => i"    (infixl 65) (*binary union*)
  10.118 -  "-"         :: "[i, i] => i"    (infixl 65) (*set difference*)
  10.119 +  "Int"       :: "[i, i] => i"    (infixl 70) --{*binary intersection*}
  10.120 +  "Un"        :: "[i, i] => i"    (infixl 65) --{*binary union*}
  10.121 +  "-"         :: "[i, i] => i"    (infixl 65) --{*set difference*}
  10.122  (*"->"        :: "[i, i] => i"    (infixr 60) [virtual] function spac\<epsilon>*)
  10.123 -  "<="        :: "[i, i] => o"    (infixl 50) (*subset relation*)
  10.124 -  ":"         :: "[i, i] => o"    (infixl 50) (*membership relation*)
  10.125 +  "<="        :: "[i, i] => o"    (infixl 50) --{*subset relation*}
  10.126 +  ":"         :: "[i, i] => o"    (infixl 50) --{*membership relation*}
  10.127  (*"~:"        :: "[i, i] => o"    (infixl 50) (*negated membership relation*)*)
  10.128  
  10.129  
    11.1 --- a/src/ZF/equalities.thy	Thu Jun 26 18:20:00 2003 +0200
    11.2 +++ b/src/ZF/equalities.thy	Fri Jun 27 13:15:40 2003 +0200
    11.3 @@ -238,6 +238,9 @@
    11.4       "A Int cons(a, B) = (if a : A then cons(a, A Int B) else A Int B)"
    11.5  by auto
    11.6  
    11.7 +lemma cons_Int_distrib: "cons(x, A \<inter> B) = cons(x, A) \<inter> cons(x, B)"
    11.8 +by auto
    11.9 +
   11.10  subsection{*Binary Union*}
   11.11  
   11.12  (** Union is the least upper bound of two sets *)