--- a/src/ZF/Cardinal.thy Thu Jun 26 18:20:00 2003 +0200
+++ b/src/ZF/Cardinal.thy Fri Jun 27 13:15:40 2003 +0200
@@ -1019,6 +1019,15 @@
apply (fast intro!: eqpoll_refl)
done
+lemma nat_not_Finite: "~Finite(nat)"
+apply (unfold Finite_def, clarify)
+apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp)
+apply (insert Card_nat)
+apply (simp add: Card_def)
+apply (drule le_imp_subset)
+apply (blast elim: mem_irrefl)
+done
+
ML
{*
val Least_def = thm "Least_def";
--- a/src/ZF/IsaMakefile Thu Jun 26 18:20:00 2003 +0200
+++ b/src/ZF/IsaMakefile Fri Jun 27 13:15:40 2003 +0200
@@ -120,7 +120,7 @@
UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
- UNITY/AllocBase.ML UNITY/AllocBase.thy UNITY/AllocImpl.thy\
+ UNITY/AllocBase.thy UNITY/AllocImpl.thy\
UNITY/ClientImpl.thy UNITY/Distributor.thy\
UNITY/Follows.ML UNITY/Follows.thy\
UNITY/Increasing.ML UNITY/Increasing.thy UNITY/Merge.thy\
--- a/src/ZF/List.thy Thu Jun 26 18:20:00 2003 +0200
+++ b/src/ZF/List.thy Fri Jun 27 13:15:40 2003 +0200
@@ -831,6 +831,12 @@
apply (erule_tac n = i in natE, simp_all)
done
+lemma length_take:
+ "l\<in>list(A) ==> \<forall>n\<in>nat. length(take(n,l)) = min(n, length(l))"
+apply (induct_tac "l", safe, simp_all)
+apply (erule natE, simp_all)
+done
+
subsection{*The function zip*}
text{*Crafty definition to eliminate a type argument*}
--- a/src/ZF/UNITY/AllocBase.ML Thu Jun 26 18:20:00 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,438 +0,0 @@
-(* Title: ZF/UNITY/AllocBase.ML
- ID: $Id$
- Author: Sidi O Ehmety, Cambridge University Computer Laboratory
- Copyright 2001 University of Cambridge
-
-Common declarations for Chandy and Charpentier's Allocator
-*)
-
-(*????remove from Union.ML:AddSEs [not_emptyE];*)
-Delrules [not_emptyE];
-
-Goal "0 < Nclients & 0 < NbT";
-by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
-by (auto_tac (claset() addIs [Ord_0_lt], simpset()));
-qed "Nclients_NbT_gt_0";
-Addsimps [Nclients_NbT_gt_0 RS conjunct1, Nclients_NbT_gt_0 RS conjunct2];
-
-Goal "Nclients \\<noteq> 0 & NbT \\<noteq> 0";
-by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
-by Auto_tac;
-qed "Nclients_NbT_not_0";
-Addsimps [Nclients_NbT_not_0 RS conjunct1, Nclients_NbT_not_0 RS conjunct2];
-
-Goal "Nclients\\<in>nat & NbT\\<in>nat";
-by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
-by Auto_tac;
-qed "Nclients_NbT_type";
-Addsimps [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
-AddTCs [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
-
-Goal "b\\<in>Inter(RepFun(Nclients, B)) <-> (\\<forall>x\\<in>Nclients. b\\<in>B(x))";
-by (auto_tac (claset(), simpset() addsimps [INT_iff]));
-by (res_inst_tac [("x", "0")] exI 1);
-by (rtac ltD 1);
-by Auto_tac;
-qed "INT_Nclient_iff";
-AddIffs [INT_Nclient_iff];
-
-val succ_def = thm "succ_def";
-
-Goal "n\\<in>nat ==> \
-\ (\\<forall>i\\<in>nat. i<n --> f(i) $<= g(i)) --> \
-\ setsum(f, n) $<= setsum(g,n)";
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x\\<notin>x" 1);
-by (Clarify_tac 1);
-by (Asm_simp_tac 1);
-by (subgoal_tac "\\<forall>i\\<in>nat. i<x--> f(i) $<= g(i)" 1);
-by (resolve_tac [zadd_zle_mono] 1);
-by (thin_tac "succ(x)=cons(x,x)" 1);
-by (ALLGOALS(Asm_simp_tac));
-by (thin_tac "succ(x)=cons(x, x)" 1);
-by (Clarify_tac 1);
-by (dtac leI 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [nat_into_Finite, mem_not_refl, succ_def]) 1);
-qed_spec_mp "setsum_fun_mono";
-
-Goal "l\\<in>list(A) ==> tokens(l)\\<in>nat";
-by (etac list.induct 1);
-by Auto_tac;
-qed "tokens_type";
-AddTCs [tokens_type];
-Addsimps [tokens_type];
-
-Goal "xs\\<in>list(A) ==> \\<forall>ys\\<in>list(A). <xs, ys>\\<in>prefix(A) \
-\ --> tokens(xs) \\<le> tokens(ys)";
-by (induct_tac "xs" 1);
-by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD],
- simpset() addsimps [prefix_def]));
-qed_spec_mp "tokens_mono_aux";
-
-Goal "<xs, ys>\\<in>prefix(A) ==> tokens(xs) \\<le> tokens(ys)";
-by (cut_facts_tac [prefix_type] 1);
-by (blast_tac (claset() addIs [tokens_mono_aux]) 1);
-qed "tokens_mono";
-
-Goalw [mono1_def] "mono1(list(A), prefix(A), nat, Le ,tokens)";
-by (auto_tac (claset() addIs [tokens_mono],
- simpset() addsimps [Le_def]));
-qed "mono_tokens";
-Addsimps [mono_tokens];
-AddIs [mono_tokens];
-
-Goal
-"[| xs\\<in>list(A); ys\\<in>list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "tokens_append";
-Addsimps [tokens_append];
-
-(*????????????????List.thy*)
-Goal "l\\<in>list(A) ==> \\<forall>n\\<in>nat. length(take(n, l))=min(n, length(l))";
-by (induct_tac "l" 1);
-by Safe_tac;
-by (ALLGOALS(Asm_simp_tac));
-by (etac natE 1);
-by (ALLGOALS(Asm_simp_tac));
-qed "length_take";
-
-(** bag_of **)
-
-Goal "l\\<in>list(A) ==>bag_of(l)\\<in>Mult(A)";
-by (induct_tac "l" 1);
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
-qed "bag_of_type";
-AddTCs [bag_of_type];
-Addsimps [bag_of_type];
-
-Goal "l\\<in>list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A";
-by (dtac bag_of_type 1);
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
-qed "bag_of_multiset";
-
-Goal "[| xs\\<in>list(A); ys\\<in>list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)";
-by (induct_tac "xs" 1);
-by (auto_tac (claset(), simpset()
- addsimps [bag_of_multiset, munion_assoc]));
-qed "bag_of_append";
-Addsimps [bag_of_append];
-
-Goal "xs\\<in>list(A) ==> \\<forall>ys\\<in>list(A). <xs, ys>\\<in>prefix(A) \
-\ --> <bag_of(xs), bag_of(ys)>\\<in>MultLe(A, r)";
-by (induct_tac "xs" 1);
-by (ALLGOALS(Clarify_tac));
-by (ftac bag_of_multiset 1);
-by (forw_inst_tac [("l", "ys")] bag_of_multiset 2);
-by (auto_tac (claset() addIs [empty_le_MultLe],
- simpset() addsimps [prefix_def]));
-by (rtac munion_mono 1);
-by (force_tac (claset(), simpset() addsimps
- [MultLe_def, Mult_iff_multiset]) 1);
-by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 1);
-qed_spec_mp "bag_of_mono_aux";
-
-Goal "[| <xs, ys>\\<in>prefix(A); xs\\<in>list(A); ys\\<in>list(A) |] ==> \
-\ <bag_of(xs), bag_of(ys)>\\<in>MultLe(A, r)";
-by (blast_tac (claset() addIs [bag_of_mono_aux]) 1);
-qed "bag_of_mono";
-AddIs [bag_of_mono];
-
-Goalw [mono1_def]
- "mono1(list(A), prefix(A), Mult(A), MultLe(A,r), bag_of)";
-by (auto_tac (claset(), simpset() addsimps [bag_of_type]));
-qed "mono_bag_of";
-Addsimps [mono_bag_of];
-
-
-(** msetsum **)
-
-bind_thm("nat_into_Fin", eqpoll_refl RSN (2,thm"Fin_lemma"));
-
-Goal "l \\<in> list(A) ==> C Int length(l) \\<in> Fin(length(l))";
-by (dtac length_type 1);
-by (rtac Fin_subset 1);
-by (rtac Int_lower2 1);
-by (etac nat_into_Fin 1);
-qed "list_Int_length_Fin";
-
-
-
-Goal "[|xs \\<in> list(A); k \\<in> C \\<inter> length(xs)|] ==> k < length(xs)";
-by (asm_full_simp_tac (simpset() addsimps [ltI]) 1);
-qed "mem_Int_imp_lt_length";
-
-
-Goal "[|C \\<subseteq> nat; x \\<in> A; xs \\<in> list(A)|] \
-\ ==> msetsum(\\<lambda>i. {#nth(i, xs @ [x])#}, C \\<inter> succ(length(xs)), A) = \
-\ (if length(xs) \\<in> C then \
-\ {#x#} +# msetsum(\\<lambda>x. {#nth(x, xs)#}, C \\<inter> length(xs), A) \
-\ else msetsum(\\<lambda>x. {#nth(x, xs)#}, C \\<inter> length(xs), A))";
-by (asm_full_simp_tac (simpset() addsimps [subsetD, nth_append, lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Int_succ_right]) 1);
-by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1);
-by (Clarify_tac 1);
-by (stac msetsum_cons 1);
-by (rtac succI1 3);
-by (blast_tac (claset() addIs [list_Int_length_Fin, subset_succI RS Fin_mono RS subsetD]) 1);
-by (asm_full_simp_tac (simpset() addsimps [mem_not_refl]) 1);
-by (asm_full_simp_tac (simpset() addsimps [nth_type, lt_not_refl]) 1);
-by (blast_tac (claset() addIs [nat_into_Ord, ltI, length_type]) 1);
-by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1);
-qed "bag_of_sublist_lemma";
-
-Goal "l\\<in>list(A) ==> \
-\ C <= nat ==> \
-\ bag_of(sublist(l, C)) = \
-\ msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
-by (etac list_append_induct 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [sublist_append, nth_append,
- bag_of_sublist_lemma, munion_commute, bag_of_sublist_lemma,
- msetsum_multiset, munion_0]) 1);
-qed "bag_of_sublist_lemma2";
-
-
-Goal "l \\<in> list(A) ==> nat \\<inter> length(l) = length(l)";
-by (rtac Int_absorb1 1);
-by (rtac OrdmemD 1);
-by Auto_tac;
-qed "nat_Int_length_eq";
-
-(*eliminating the assumption C<=nat*)
-Goal "l\\<in>list(A) ==> \
-\ bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
-by (subgoal_tac
- " bag_of(sublist(l, C Int nat)) = \
-\ msetsum(%i. {#nth(i, l)#}, C Int length(l), A)" 1);
-by (asm_full_simp_tac (simpset() addsimps [sublist_Int_eq]) 1);
-by (asm_full_simp_tac (simpset() addsimps [bag_of_sublist_lemma2, Int_lower2, Int_assoc, nat_Int_length_eq]) 1);
-qed "bag_of_sublist";
-
-Goal
-"l\\<in>list(A) ==> \
-\ bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) = \
-\ bag_of(sublist(l, B)) +# bag_of(sublist(l, C))";
-by (subgoal_tac
- "B Int C Int length(l) = \
-\ (B Int length(l)) Int (C Int length(l))" 1);
-by (Blast_tac 2);
-by (asm_simp_tac (simpset() addsimps [bag_of_sublist,
- Int_Un_distrib2, msetsum_Un_Int]) 1);
-by (resolve_tac [msetsum_Un_Int] 1);
-by (REPEAT (etac list_Int_length_Fin 1));
- by (asm_full_simp_tac (simpset() addsimps [ltI, nth_type]) 1);
-qed "bag_of_sublist_Un_Int";
-
-
-Goal "[| l\\<in>list(A); B Int C = 0 |]\
-\ ==> bag_of(sublist(l, B Un C)) = \
-\ bag_of(sublist(l, B)) +# bag_of(sublist(l, C))";
-by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym,
- sublist_type, bag_of_multiset]) 1);
-qed "bag_of_sublist_Un_disjoint";
-
-Goal "[|Finite(I); \\<forall>i\\<in>I. \\<forall>j\\<in>I. i\\<noteq>j --> A(i) \\<inter> A(j) = 0; \
-\ l\\<in>list(B) |] \
-\ ==> bag_of(sublist(l, \\<Union>i\\<in>I. A(i))) = \
-\ (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) ";
-by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
- addsimps [bag_of_sublist]) 1);
-by (stac (inst "A" "length(l)" msetsum_UN_disjoint) 1);
-by (dresolve_tac [Finite_into_Fin] 1);
-by (assume_tac 1);
-by (Force_tac 3);
-by (auto_tac (claset() addSIs [Fin_IntI2, Finite_into_Fin],
- simpset() addsimps [ltI, nth_type, length_type, nat_into_Finite]));
-qed_spec_mp "bag_of_sublist_UN_disjoint";
-
-
-Goalw [part_ord_def, Lt_def, irrefl_def, trans_on_def]
- "part_ord(nat, Lt)";
-by (auto_tac (claset() addIs [lt_trans], simpset()));
-qed "part_ord_Lt";
-Addsimps [part_ord_Lt];
-
-
-(** all_distinct **)
-
-Goalw [all_distinct_def] "all_distinct(Nil)";
-by Auto_tac;
-qed "all_distinct_Nil";
-
-Goalw [all_distinct_def]
-"all_distinct(Cons(a, l)) <-> \
-\ (a\\<in>set_of_list(l) --> False) & (a \\<notin> set_of_list(l) --> all_distinct(l))";
-by (auto_tac (claset() addEs [list.elim], simpset()));
-qed "all_distinct_Cons";
-Addsimps [all_distinct_Nil, all_distinct_Cons];
-
-(** state_of **)
-Goalw [state_of_def] "s\\<in>state ==> state_of(s)=s";
-by Auto_tac;
-qed "state_of_state";
-Addsimps [state_of_state];
-
-
-Goalw [state_of_def] "state_of(state_of(s))=state_of(s)";
-by Auto_tac;
-qed "state_of_idem";
-Addsimps [state_of_idem];
-
-
-Goalw [state_of_def] "state_of(s)\\<in>state";
-by Auto_tac;
-qed "state_of_type";
-Addsimps [state_of_type];
-AddTCs [state_of_type];
-
-Goalw [lift_def] "lift(x, s)=s`x";
-by (Simp_tac 1);
-qed "lift_apply";
-Addsimps [lift_apply];
-
-(** Used in ClientImp **)
-
-Goalw [Increasing_def]
-"Increasing(A, r, %s. f(state_of(s))) = \
-\ Increasing(A, r, f)";
-by Auto_tac;
-qed "gen_Increains_state_of_eq";
-bind_thm("Increasing_state_ofD1",
-gen_Increains_state_of_eq RS equalityD1 RS subsetD);
-bind_thm("Increasing_state_ofD2",
-gen_Increains_state_of_eq RS equalityD2 RS subsetD);
-
-Goalw [Follows_def, Increasing_def]
-"Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) = \
-\ Follows(A, r, f, g)";
-by Auto_tac;
-qed "Follows_state_of_eq";
-bind_thm("Follows_state_ofD1", Follows_state_of_eq RS equalityD1 RS subsetD);
-bind_thm("Follows_state_ofD2", Follows_state_of_eq RS equalityD2 RS subsetD);
-
-(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
-fun list_of_Int th = list_of_Int_aux (Drule.freeze_all th)
-and list_of_Int_aux th =
- (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
- handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
- handle THM _ => (list_of_Int (th RS InterD))
- handle THM _ => (list_of_Int (th RS bspec))
- handle THM _ => [th];
-
-(*Used just once, for Alloc_Increasing*)
-
-fun normalize th =
- normalize (th RS spec
- handle THM _ => th RS bspec
- handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
- handle THM _ => th;
-
-Goal "n\\<in>nat ==> nat_list_inj(n)\\<in>list(nat)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "nat_list_inj_type";
-
-Goal "n\\<in>nat ==> length(nat_list_inj(n)) = n";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "length_nat_list_inj";
-
-Goalw [nat_var_inj_def]
- "(\\<lambda>x\\<in>nat. nat_var_inj(x))\\<in>inj(nat, var)";
-by (res_inst_tac [("d", "var_inj")] lam_injective 1);
-by (asm_simp_tac (simpset() addsimps [length_nat_list_inj]) 2);
-by (auto_tac (claset(), simpset() addsimps var.intrs@[nat_list_inj_type]));
-qed "var_infinite_lemma";
-
-Goalw [lepoll_def] "nat lepoll var";
-by (res_inst_tac [("x", "(\\<lambda>x\\<in>nat. nat_var_inj(x))")] exI 1);
-by (rtac var_infinite_lemma 1);
-qed "nat_lepoll_var";
-
-Goalw [Finite_def] "~Finite(var)";
-by Auto_tac;
-by (dtac eqpoll_imp_lepoll 1);
-by (cut_facts_tac [nat_lepoll_var] 1);
-by (subgoal_tac "nat lepoll x" 1);
-by (blast_tac (claset() addIs [lepoll_trans]) 2);
-by (dres_inst_tac [("i", "x"), ("A", "nat")] lepoll_cardinal_le 1);
-by Auto_tac;
-by (subgoal_tac "Card(nat)" 1);
-by (rewrite_goal_tac [Card_def] 1);
-by (dtac sym 1);
-by Auto_tac;
-by (dtac le_imp_subset 1);
-by (dtac subsetD 1);
-by (auto_tac (claset(), simpset() addsimps [Card_nat]));
-by (blast_tac (claset() addEs [mem_irrefl]) 1);
-qed "var_not_Finite";
-
-Goal "~Finite(A) ==> \\<exists>x. x\\<in>A";
-by (etac swap 1);
-by Auto_tac;
-by (subgoal_tac "A=0" 1);
-by (auto_tac (claset(), simpset() addsimps [Finite_0]));
-qed "not_Finite_imp_exist";
-
-Goal "Finite(A) ==> b\\<in>(Inter(RepFun(var-A, B))) <-> (\\<forall>x\\<in>var-A. b\\<in>B(x))";
-by (subgoal_tac "\\<exists>x. x\\<in>var-A" 1);
-by Auto_tac;
-by (subgoal_tac "~Finite(var-A)" 1);
-by (dtac not_Finite_imp_exist 1);
-by Auto_tac;
-by (cut_facts_tac [var_not_Finite] 1);
-by (etac swap 1);
-by (res_inst_tac [("B", "A")] Diff_Finite 1);
-by Auto_tac;
-qed "Inter_Diff_var_iff";
-
-Goal "[| b\\<in>Inter(RepFun(var-A, B)); Finite(A); x\\<in>var-A |] ==> b\\<in>B(x)";
-by (rotate_tac 1 1);
-by (asm_full_simp_tac (simpset() addsimps [Inter_Diff_var_iff]) 1);
-qed "Inter_var_DiffD";
-
-(* [| Finite(A); (\\<forall>x\\<in>var-A. b\\<in>B(x)) |] ==> b\\<in>Inter(RepFun(var-A, B)) *)
-bind_thm("Inter_var_DiffI", Inter_Diff_var_iff RS iffD2);
-
-AddSIs [Inter_var_DiffI];
-Addsimps [Finite_0, Finite_cons];
-
-Goal "Acts(F)<= A \\<inter> Pow(state*state) <-> Acts(F)<=A";
-by (cut_facts_tac [inst "F" "F" Acts_type] 1);
-by Auto_tac;
-qed "Acts_subset_Int_Pow_simp";
-Addsimps [Acts_subset_Int_Pow_simp];
-
-(*for main zf?????*)
-Goal "cons(x, A \\<inter> B) = cons(x, A) \\<inter> cons(x, B)";
-by Auto_tac;
-qed "cons_Int_distrib";
-
-
-(* Currently not used, but of potential interest *)
-Goal
-"[| Finite(A); \\<forall>x\\<in>A. g(x)\\<in>nat |] ==> \
-\ setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)";
-by (etac Finite_induct 1);
-by (auto_tac (claset(), simpset() addsimps [int_of_add]));
-qed "setsum_nsetsum_eq";
-
-Goal
-"[| A=B; \\<forall>x\\<in>A. f(x)=g(x); \\<forall>x\\<in>A. g(x)\\<in>nat; \
-\ Finite(A) |] ==> nsetsum(f, A) = nsetsum(g, B)";
-by (subgoal_tac "$# nsetsum(f, A) = $# nsetsum(g, B)" 1);
-by (rtac trans 2);
-by (rtac setsum_nsetsum_eq 3);
-by (rtac trans 2);
-by (rtac (setsum_nsetsum_eq RS sym) 2);
-by Auto_tac;
-by (rtac setsum_cong 1);
-by Auto_tac;
-qed "nsetsum_cong";
-
-
-
-
--- a/src/ZF/UNITY/AllocBase.thy Thu Jun 26 18:20:00 2003 +0200
+++ b/src/ZF/UNITY/AllocBase.thy Fri Jun 27 13:15:40 2003 +0200
@@ -3,65 +3,65 @@
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
-Common declarations for Chandy and Charpentier's Allocator
*)
-AllocBase = Follows + MultisetSum + Guar +
+header{*Common declarations for Chandy and Charpentier's Allocator*}
+
+theory AllocBase = Follows + MultisetSum + Guar:
consts
tokbag :: i (* tokbags could be multisets...or any ordered type?*)
NbT :: i (* Number of tokens in system *)
Nclients :: i (* Number of clients *)
-translations
-"tokbag" => "nat"
-rules
- NbT_pos "NbT:nat-{0}"
- Nclients_pos "Nclients:nat-{0}"
+
+translations "tokbag" => "nat"
+
+axioms
+ NbT_pos: "NbT \<in> nat-{0}"
+ Nclients_pos: "Nclients \<in> nat-{0}"
-(*This function merely sums the elements of a list*)
-consts tokens :: i =>i
+text{*This function merely sums the elements of a list*}
+consts tokens :: "i =>i"
item :: i (* Items to be merged/distributed *)
primrec
"tokens(Nil) = 0"
"tokens (Cons(x,xs)) = x #+ tokens(xs)"
consts
- bag_of :: i => i
+ bag_of :: "i => i"
primrec
"bag_of(Nil) = 0"
"bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"
-(* definitions needed in Client.thy *)
-consts
- all_distinct0:: i=>i
- all_distinct:: i=>o
-
-primrec
+
+text{*Definitions needed in Client.thy. We define a recursive predicate
+using 0 and 1 to code the truth values.*}
+consts all_distinct0 :: "i=>i"
+ primrec
"all_distinct0(Nil) = 1"
"all_distinct0(Cons(a, l)) =
- (if a:set_of_list(l) then 0 else all_distinct0(l))"
+ (if a \<in> set_of_list(l) then 0 else all_distinct0(l))"
-defs
-all_distinct_def
- "all_distinct(l) == all_distinct0(l)=1"
+constdefs
+ all_distinct :: "i=>o"
+ "all_distinct(l) == all_distinct0(l)=1"
constdefs
- (* coersion from anyting to state *)
- state_of :: i =>i
- "state_of(s) == if s:state then s else st0"
+ state_of :: "i =>i" --{* coersion from anyting to state *}
+ "state_of(s) == if s \<in> state then s else st0"
- (* simplifies the expression of programs *)
+ lift :: "i =>(i=>i)" --{* simplifies the expression of programs*}
+ "lift(x) == %s. s`x"
- lift :: "i =>(i=>i)"
- "lift(x) == %s. s`x"
+text{* function to show that the set of variables is infinite *}
+consts
+ nat_list_inj :: "i=>i"
+ nat_var_inj :: "i=>i"
+ var_inj :: "i=>i"
-consts (* to show that the set of variables is infinite *)
- nat_list_inj :: i=>i
- nat_var_inj :: i=>i
- var_inj :: i=>i
defs
- nat_var_inj_def "nat_var_inj(n) == Var(nat_list_inj(n))"
+ nat_var_inj_def: "nat_var_inj(n) == Var(nat_list_inj(n))"
primrec
"nat_list_inj(0) = Nil"
"nat_list_inj(succ(n)) = Cons(n, nat_list_inj(n))"
@@ -69,4 +69,343 @@
primrec
"var_inj(Var(l)) = length(l)"
+
+subsection{*Various simple lemmas*}
+
+lemma Nclients_NbT_gt_0 [simp]: "0 < Nclients & 0 < NbT"
+apply (cut_tac Nclients_pos NbT_pos)
+apply (auto intro: Ord_0_lt)
+done
+
+lemma Nclients_NbT_not_0 [simp]: "Nclients \<noteq> 0 & NbT \<noteq> 0"
+by (cut_tac Nclients_pos NbT_pos, auto)
+
+lemma Nclients_type [simp,TC]: "Nclients\<in>nat"
+by (cut_tac Nclients_pos NbT_pos, auto)
+
+lemma NbT_type [simp,TC]: "NbT\<in>nat"
+by (cut_tac Nclients_pos NbT_pos, auto)
+
+lemma INT_Nclient_iff [iff]:
+ "b\<in>Inter(RepFun(Nclients, B)) <-> (\<forall>x\<in>Nclients. b\<in>B(x))"
+apply (auto simp add: INT_iff)
+apply (rule_tac x = 0 in exI)
+apply (rule ltD, auto)
+done
+
+lemma setsum_fun_mono [rule_format]:
+ "n\<in>nat ==>
+ (\<forall>i\<in>nat. i<n --> f(i) $<= g(i)) -->
+ setsum(f, n) $<= setsum(g,n)"
+apply (induct_tac "n", simp_all)
+apply (subgoal_tac "Finite(x) & x\<notin>x")
+ prefer 2 apply (simp add: nat_into_Finite mem_not_refl, clarify)
+apply (simp (no_asm_simp) add: succ_def)
+apply (subgoal_tac "\<forall>i\<in>nat. i<x--> f(i) $<= g(i) ")
+ prefer 2 apply (force dest: leI)
+apply (rule zadd_zle_mono, simp_all)
+done
+
+lemma tokens_type [simp,TC]: "l\<in>list(A) ==> tokens(l)\<in>nat"
+by (erule list.induct, auto)
+
+lemma tokens_mono_aux [rule_format]:
+ "xs\<in>list(A) ==> \<forall>ys\<in>list(A). <xs, ys>\<in>prefix(A)
+ --> tokens(xs) \<le> tokens(ys)"
+apply (induct_tac "xs")
+apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: prefix_def)
+done
+
+lemma tokens_mono: "<xs, ys>\<in>prefix(A) ==> tokens(xs) \<le> tokens(ys)"
+apply (cut_tac prefix_type)
+apply (blast intro: tokens_mono_aux)
+done
+
+lemma mono_tokens [iff]: "mono1(list(A), prefix(A), nat, Le,tokens)"
+apply (unfold mono1_def)
+apply (auto intro: tokens_mono simp add: Le_def)
+done
+
+lemma tokens_append [simp]:
+"[| xs\<in>list(A); ys\<in>list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)"
+apply (induct_tac "xs", auto)
+done
+
+subsection{*The function @{term bag_of}*}
+
+lemma bag_of_type [simp,TC]: "l\<in>list(A) ==>bag_of(l)\<in>Mult(A)"
+apply (induct_tac "l")
+apply (auto simp add: Mult_iff_multiset)
+done
+
+lemma bag_of_multiset:
+ "l\<in>list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A"
+apply (drule bag_of_type)
+apply (auto simp add: Mult_iff_multiset)
+done
+
+lemma bag_of_append [simp]:
+ "[| xs\<in>list(A); ys\<in>list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)"
+apply (induct_tac "xs")
+apply (auto simp add: bag_of_multiset munion_assoc)
+done
+
+lemma bag_of_mono_aux [rule_format]:
+ "xs\<in>list(A) ==> \<forall>ys\<in>list(A). <xs, ys>\<in>prefix(A)
+ --> <bag_of(xs), bag_of(ys)>\<in>MultLe(A, r)"
+apply (induct_tac "xs", simp_all, clarify)
+apply (frule_tac l = ys in bag_of_multiset)
+apply (auto intro: empty_le_MultLe simp add: prefix_def)
+apply (rule munion_mono)
+apply (force simp add: MultLe_def Mult_iff_multiset)
+apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
+done
+
+lemma bag_of_mono [intro]:
+ "[| <xs, ys>\<in>prefix(A); xs\<in>list(A); ys\<in>list(A) |]
+ ==> <bag_of(xs), bag_of(ys)>\<in>MultLe(A, r)"
+apply (blast intro: bag_of_mono_aux)
+done
+
+lemma mono_bag_of [simp]:
+ "mono1(list(A), prefix(A), Mult(A), MultLe(A,r), bag_of)"
+by (auto simp add: mono1_def bag_of_type)
+
+
+subsection{*The function @{term msetsum}*}
+
+lemmas nat_into_Fin = eqpoll_refl [THEN [2] Fin_lemma]
+
+lemma list_Int_length_Fin: "l \<in> list(A) ==> C Int length(l) \<in> Fin(length(l))"
+apply (drule length_type)
+apply (rule Fin_subset)
+apply (rule Int_lower2)
+apply (erule nat_into_Fin)
+done
+
+
+
+lemma mem_Int_imp_lt_length:
+ "[|xs \<in> list(A); k \<in> C \<inter> length(xs)|] ==> k < length(xs)"
+apply (simp add: ltI)
+done
+
+
+lemma bag_of_sublist_lemma:
+ "[|C \<subseteq> nat; x \<in> A; xs \<in> list(A)|]
+ ==> msetsum(\<lambda>i. {#nth(i, xs @ [x])#}, C \<inter> succ(length(xs)), A) =
+ (if length(xs) \<in> C then
+ {#x#} +# msetsum(\<lambda>x. {#nth(x, xs)#}, C \<inter> length(xs), A)
+ else msetsum(\<lambda>x. {#nth(x, xs)#}, C \<inter> length(xs), A))"
+apply (simp add: subsetD nth_append lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong)
+apply (simp add: Int_succ_right)
+apply (simp add: lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong, clarify)
+apply (subst msetsum_cons)
+apply (rule_tac [3] succI1)
+apply (blast intro: list_Int_length_Fin subset_succI [THEN Fin_mono, THEN subsetD])
+apply (simp add: mem_not_refl)
+apply (simp add: nth_type lt_not_refl)
+apply (blast intro: nat_into_Ord ltI length_type)
+apply (simp add: lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong)
+done
+
+lemma bag_of_sublist_lemma2:
+ "l\<in>list(A) ==>
+ C <= nat ==>
+ bag_of(sublist(l, C)) =
+ msetsum(%i. {#nth(i, l)#}, C Int length(l), A)"
+apply (erule list_append_induct)
+apply (simp (no_asm))
+apply (simp (no_asm_simp) add: sublist_append nth_append bag_of_sublist_lemma munion_commute bag_of_sublist_lemma msetsum_multiset munion_0)
+done
+
+
+lemma nat_Int_length_eq: "l \<in> list(A) ==> nat \<inter> length(l) = length(l)"
+apply (rule Int_absorb1)
+apply (rule OrdmemD, auto)
+done
+
+(*eliminating the assumption C<=nat*)
+lemma bag_of_sublist:
+ "l\<in>list(A) ==>
+ bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)"
+apply (subgoal_tac " bag_of (sublist (l, C Int nat)) = msetsum (%i. {#nth (i, l) #}, C Int length (l), A) ")
+apply (simp add: sublist_Int_eq)
+apply (simp add: bag_of_sublist_lemma2 Int_lower2 Int_assoc nat_Int_length_eq)
+done
+
+lemma bag_of_sublist_Un_Int:
+"l\<in>list(A) ==>
+ bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) =
+ bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"
+apply (subgoal_tac "B Int C Int length (l) = (B Int length (l)) Int (C Int length (l))")
+prefer 2 apply blast
+apply (simp (no_asm_simp) add: bag_of_sublist Int_Un_distrib2 msetsum_Un_Int)
+apply (rule msetsum_Un_Int)
+apply (erule list_Int_length_Fin)+
+ apply (simp add: ltI nth_type)
+done
+
+
+lemma bag_of_sublist_Un_disjoint:
+ "[| l\<in>list(A); B Int C = 0 |]
+ ==> bag_of(sublist(l, B Un C)) =
+ bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"
+by (simp add: bag_of_sublist_Un_Int [symmetric] bag_of_multiset)
+
+
+lemma bag_of_sublist_UN_disjoint [rule_format]:
+ "[|Finite(I); \<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j --> A(i) \<inter> A(j) = 0;
+ l\<in>list(B) |]
+ ==> bag_of(sublist(l, \<Union>i\<in>I. A(i))) =
+ (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) "
+apply (simp (no_asm_simp) del: UN_simps
+ add: UN_simps [symmetric] bag_of_sublist)
+apply (subst msetsum_UN_disjoint [of _ _ _ "length (l)"])
+apply (drule Finite_into_Fin, assumption)
+prefer 3 apply force
+apply (auto intro!: Fin_IntI2 Finite_into_Fin simp add: ltI nth_type length_type nat_into_Finite)
+done
+
+
+lemma part_ord_Lt [simp]: "part_ord(nat, Lt)"
+apply (unfold part_ord_def Lt_def irrefl_def trans_on_def)
+apply (auto intro: lt_trans)
+done
+
+subsubsection{*The function @{term all_distinct}*}
+
+lemma all_distinct_Nil [simp]: "all_distinct(Nil)"
+by (unfold all_distinct_def, auto)
+
+lemma all_distinct_Cons [simp]:
+ "all_distinct(Cons(a,l)) <->
+ (a\<in>set_of_list(l) --> False) & (a \<notin> set_of_list(l) --> all_distinct(l))"
+apply (unfold all_distinct_def)
+apply (auto elim: list.cases)
+done
+
+subsubsection{*The function @{term state_of}*}
+
+lemma state_of_state: "s\<in>state ==> state_of(s)=s"
+by (unfold state_of_def, auto)
+declare state_of_state [simp]
+
+
+lemma state_of_idem: "state_of(state_of(s))=state_of(s)"
+
+apply (unfold state_of_def, auto)
+done
+declare state_of_idem [simp]
+
+
+lemma state_of_type [simp,TC]: "state_of(s)\<in>state"
+by (unfold state_of_def, auto)
+
+lemma lift_apply [simp]: "lift(x, s)=s`x"
+by (simp add: lift_def)
+
+
+(** Used in ClientImp **)
+
+lemma gen_Increains_state_of_eq:
+ "Increasing(A, r, %s. f(state_of(s))) = Increasing(A, r, f)"
+apply (unfold Increasing_def, auto)
+done
+
+lemmas Increasing_state_ofD1 =
+ gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD, standard]
+lemmas Increasing_state_ofD2 =
+ gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD, standard]
+
+lemma Follows_state_of_eq:
+ "Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) =
+ Follows(A, r, f, g)"
+apply (unfold Follows_def Increasing_def, auto)
+done
+
+lemmas Follows_state_ofD1 =
+ Follows_state_of_eq [THEN equalityD1, THEN subsetD, standard]
+lemmas Follows_state_ofD2 =
+ Follows_state_of_eq [THEN equalityD2, THEN subsetD, standard]
+
+lemma nat_list_inj_type: "n\<in>nat ==> nat_list_inj(n)\<in>list(nat)"
+by (induct_tac "n", auto)
+
+lemma length_nat_list_inj: "n\<in>nat ==> length(nat_list_inj(n)) = n"
+by (induct_tac "n", auto)
+
+lemma var_infinite_lemma:
+ "(\<lambda>x\<in>nat. nat_var_inj(x))\<in>inj(nat, var)"
+apply (unfold nat_var_inj_def)
+apply (rule_tac d = var_inj in lam_injective)
+apply (auto simp add: var.intros nat_list_inj_type)
+apply (simp add: length_nat_list_inj)
+done
+
+lemma nat_lepoll_var: "nat lepoll var"
+apply (unfold lepoll_def)
+apply (rule_tac x = " (\<lambda>x\<in>nat. nat_var_inj (x))" in exI)
+apply (rule var_infinite_lemma)
+done
+
+(*Surely a simpler proof uses lepoll_Finite and the following lemma:*)
+
+ (*????Cardinal*)
+ lemma nat_not_Finite: "~Finite(nat)"
+ apply (unfold Finite_def, clarify)
+ apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp)
+ apply (insert Card_nat)
+ apply (simp add: Card_def)
+ apply (drule le_imp_subset)
+ apply (blast elim: mem_irrefl)
+ done
+
+lemma var_not_Finite: "~Finite(var)"
+apply (insert nat_not_Finite)
+apply (blast intro: lepoll_Finite [OF nat_lepoll_var])
+done
+
+lemma not_Finite_imp_exist: "~Finite(A) ==> \<exists>x. x\<in>A"
+apply (subgoal_tac "A\<noteq>0")
+apply (auto simp add: Finite_0)
+done
+
+lemma Inter_Diff_var_iff:
+ "Finite(A) ==> b\<in>(Inter(RepFun(var-A, B))) <-> (\<forall>x\<in>var-A. b\<in>B(x))"
+apply (subgoal_tac "\<exists>x. x\<in>var-A", auto)
+apply (subgoal_tac "~Finite (var-A) ")
+apply (drule not_Finite_imp_exist, auto)
+apply (cut_tac var_not_Finite)
+apply (erule swap)
+apply (rule_tac B = A in Diff_Finite, auto)
+done
+
+lemma Inter_var_DiffD:
+ "[| b\<in>Inter(RepFun(var-A, B)); Finite(A); x\<in>var-A |] ==> b\<in>B(x)"
+by (simp add: Inter_Diff_var_iff)
+
+(* [| Finite(A); (\<forall>x\<in>var-A. b\<in>B(x)) |] ==> b\<in>Inter(RepFun(var-A, B)) *)
+lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2, standard]
+
+declare Inter_var_DiffI [intro!]
+
+lemma Acts_subset_Int_Pow_simp [simp]:
+ "Acts(F)<= A \<inter> Pow(state*state) <-> Acts(F)<=A"
+by (insert Acts_type [of F], auto)
+
+lemma setsum_nsetsum_eq:
+ "[| Finite(A); \<forall>x\<in>A. g(x)\<in>nat |]
+ ==> setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)"
+apply (erule Finite_induct)
+apply (auto simp add: int_of_add)
+done
+
+lemma nsetsum_cong:
+ "[| A=B; \<forall>x\<in>A. f(x)=g(x); \<forall>x\<in>A. g(x)\<in>nat; Finite(A) |]
+ ==> nsetsum(f, A) = nsetsum(g, B)"
+apply (subgoal_tac "$# nsetsum (f, A) = $# nsetsum (g, B)", simp)
+apply (simp add: setsum_nsetsum_eq [symmetric] cong: setsum_cong)
+done
+
end
--- a/src/ZF/UNITY/AllocImpl.thy Thu Jun 26 18:20:00 2003 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy Fri Jun 27 13:15:40 2003 +0200
@@ -394,10 +394,11 @@
apply (simp_all add: refl_prefix Le_def comp_def length_type)
done
-(* Lemma 51, page 29.
+
+text{*Lemma 51, page 29.
This theorem states as invariant that if the number of
tokens given does not exceed the number returned, then the upper limit
- (NbT) does not exceed the number currently available.*)
+ (@{term NbT}) does not exceed the number currently available.*}
lemma alloc_prog_Always_lemma:
"[| G \<in> program; alloc_prog ok G;
alloc_prog \<squnion> G \<in> Incr(lift(ask));
@@ -405,22 +406,24 @@
==> alloc_prog \<squnion> 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 \<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))}) ")
+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))})")
apply (rule_tac [2] AlwaysI)
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))")
-apply (simp (no_asm_simp))
-apply (rule nat_diff_split [THEN iffD2], auto)
-apply (drule_tac j = "tokens(x ` giv)" in lt_trans2)
-apply assumption
-apply auto
+apply (simp add: );
+apply (auto split add: nat_diff_split dest: lt_trans2)
done
+
+
subsubsection{* Main lemmas towards proving property (31)*}
lemma LeadsTo_strength_R:
--- a/src/ZF/UNITY/Guar.ML Thu Jun 26 18:20:00 2003 +0200
+++ b/src/ZF/UNITY/Guar.ML Fri Jun 27 13:15:40 2003 +0200
@@ -34,7 +34,7 @@
by (ALLGOALS(asm_full_simp_tac
(simpset() addsimps [OK_cons_iff])));
(* Auto_tac proves the goal in one step *)
-by Safe_tac;
+by (safe_tac (claset() addSEs [not_emptyE]));
by (ALLGOALS(Asm_full_simp_tac));
by (Fast_tac 1);
qed_spec_mp "ex1";
--- a/src/ZF/UNITY/Merge.thy Thu Jun 26 18:20:00 2003 +0200
+++ b/src/ZF/UNITY/Merge.thy Fri Jun 27 13:15:40 2003 +0200
@@ -87,14 +87,12 @@
lemma (in merge) Out_value_type [TC,simp]: "s \<in> state ==> s`Out \<in> list(A)"
apply (unfold state_def)
-apply (drule_tac a = "Out" in apply_type)
-apply auto
+apply (drule_tac a = Out in apply_type, auto)
done
lemma (in merge) iOut_value_type [TC,simp]: "s \<in> state ==> s`iOut \<in> list(nat)"
apply (unfold state_def)
-apply (drule_tac a = "iOut" in apply_type)
-apply auto
+apply (drule_tac a = iOut in apply_type, auto)
done
lemma (in merge) M_in_program [intro,simp]: "M \<in> program"
@@ -123,7 +121,7 @@
==> M \<squnion> G \<in> Always({s \<in> state. length(s`Out)=length(s`iOut)})"
apply (frule preserves_type [THEN subsetD])
apply (subgoal_tac "G \<in> program")
- prefer 2 apply (assumption)
+ prefer 2 apply assumption
apply (frule M_ok_iff)
apply (cut_tac merge_spec)
apply (force dest: guaranteesD simp add: merge_spec_def merge_eq_Out_def)
@@ -148,8 +146,7 @@
Nclients, A) = bag_of(s`Out)})"
apply (rule Always_Diff_Un_eq [THEN iffD1])
apply (rule_tac [2] state_AlwaysI [THEN Always_weaken])
-apply (rule Always_Int_I [OF merge_Always_Out_eq_iOut merge_Bounded])
-apply auto
+apply (rule Always_Int_I [OF merge_Always_Out_eq_iOut merge_Bounded], auto)
apply (subst bag_of_sublist_UN_disjoint [symmetric])
apply (auto simp add: nat_into_Finite set_of_list_conv_nth [OF iOut_value_type])
apply (subgoal_tac " (\<Union>i \<in> Nclients. {k \<in> nat. k < length (x`iOut) & nth (k, x`iOut) = i}) = length (x`iOut) ")
@@ -158,10 +155,9 @@
take_all [OF _ Out_value_type]
length_type [OF iOut_value_type])
apply (rule equalityI)
-apply (blast dest: ltD)
-apply clarify
+apply (blast dest: ltD, clarify)
apply (subgoal_tac "length (x ` iOut) \<in> nat")
- prefer 2 apply (simp add: length_type [OF iOut_value_type]);
+ prefer 2 apply (simp add: length_type [OF iOut_value_type])
apply (subgoal_tac "xa \<in> nat")
apply (simp_all add: Ord_mem_iff_lt)
prefer 2 apply (blast intro: lt_trans)
@@ -177,19 +173,15 @@
(%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)"
apply (cut_tac merge_spec)
apply (rule merge_bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI])
- apply (simp_all add: M_ok_iff)
-apply clarify
+ apply (simp_all add: M_ok_iff, clarify)
apply (rule Follows_state_ofD1 [OF Follows_msetsum_UN])
apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
-apply (simp add: INT_iff merge_spec_def merge_follows_def)
-apply clarify
+apply (simp add: INT_iff merge_spec_def merge_follows_def, clarify)
apply (cut_tac merge_spec)
apply (subgoal_tac "M ok G")
prefer 2 apply (force intro: M_ok_iff [THEN iffD2])
-apply (drule guaranteesD)
-apply assumption
- apply (simp add: merge_spec_def merge_follows_def)
- apply blast
+apply (drule guaranteesD, assumption)
+ apply (simp add: merge_spec_def merge_follows_def, blast)
apply (simp cong add: Follows_cong
add: refl_prefix
mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
--- a/src/ZF/UNITY/Union.ML Thu Jun 26 18:20:00 2003 +0200
+++ b/src/ZF/UNITY/Union.ML Fri Jun 27 13:15:40 2003 +0200
@@ -164,12 +164,11 @@
by Auto_tac;
qed "JN_empty";
AddIffs [JN_empty];
-AddSEs [not_emptyE];
Addsimps [Inter_0];
Goal "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))";
by (simp_tac (simpset() addsimps [JOIN_def]) 1);
-by (auto_tac (claset(), simpset() addsimps [INT_Int_distrib]));
+by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [INT_Int_distrib]));
qed "Init_JN";
Goalw [JOIN_def]
@@ -183,7 +182,7 @@
"AllowedActs(JN i:I. F(i)) = (if I=0 then Pow(state*state) else (INT i:I. AllowedActs(F(i))))";
by Auto_tac;
by (rtac equalityI 1);
-by (auto_tac (claset() addDs [AllowedActs_type RS subsetD], simpset()));
+by (auto_tac (claset() addSEs [not_emptyE] addDs [AllowedActs_type RS subsetD], simpset()));
qed "AllowedActs_JN";
AddIffs [Init_JN, Acts_JN, AllowedActs_JN];
@@ -225,22 +224,21 @@
Goal "(JN i:I. F(i) Join G(i)) = (JN i:I. F(i)) Join (JN i:I. G(i))";
by (rtac program_equalityI 1);
by (ALLGOALS(simp_tac (simpset() addsimps [Int_absorb])));
-by Safe_tac;
+by (safe_tac (claset() addSEs [not_emptyE]));
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps
[INT_Int_distrib, Int_absorb])));
by (Force_tac 1);
qed "JN_Join_distrib";
Goal "(JN i:I. F(i) Join G) = ((JN i:I. F(i) Join G))";
-by (asm_simp_tac (simpset()
- addsimps [JN_Join_distrib, JN_constant]) 1);
+by (asm_simp_tac (simpset() addsimps [JN_Join_distrib, JN_constant]) 1);
qed "JN_Join_miniscope";
(*Used to prove guarantees_JN_I*)
Goal "i:I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)";
by (rtac program_equalityI 1);
-by Auto_tac;
+by (auto_tac (claset() addSEs [not_emptyE], simpset()));
qed "JN_Join_diff";
(*** Safety: co, stable, FP ***)
@@ -309,9 +307,7 @@
val [major, minor] = Goalw [initially_def]
"[| (!!i. i:I ==>F(i):initially(A)); i:I |] ==> (JN i:I. F(i)):initially(A)";
by (cut_facts_tac [minor] 1);
-by (Asm_full_simp_tac 1);
-by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps [Inter_iff]) 1);
+by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [Inter_iff]));
by (forw_inst_tac [("i", "x")] major 1);
by Auto_tac;
qed "initially_JN_I";
@@ -500,13 +496,13 @@
qed "ok_Join_commute_I";
Goal "F ok JOIN(I,G) <-> (ALL i:I. F ok G(i))";
-by (auto_tac (claset(), simpset() addsimps [ok_def]));
+by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [ok_def]));
by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
qed "ok_JN_iff1";
Goal "JOIN(I,G) ok F <-> (ALL i:I. G(i) ok F)";
-by (auto_tac (claset(), simpset() addsimps [ok_def]));
+by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [ok_def]));
by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
qed "ok_JN_iff2";
AddIffs [ok_JN_iff1, ok_JN_iff2];
--- a/src/ZF/ZF.thy Thu Jun 26 18:20:00 2003 +0200
+++ b/src/ZF/ZF.thy Fri Jun 27 13:15:40 2003 +0200
@@ -2,41 +2,43 @@
ID: $Id$
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
Copyright 1993 University of Cambridge
+*)
-Zermelo-Fraenkel Set Theory
-*)
+header{*Zermelo-Fraenkel Set Theory*}
theory ZF = FOL:
global
-typedecl
- i
-
-arities
- i :: "term"
+typedecl i
+arities i :: "term"
consts
- "0" :: "i" ("0") (*the empty set*)
- Pow :: "i => i" (*power sets*)
- Inf :: "i" (*infinite set*)
+ "0" :: "i" ("0") --{*the empty set*}
+ Pow :: "i => i" --{*power sets*}
+ Inf :: "i" --{*infinite set*}
- (* Bounded Quantifiers *)
+text {*Bounded Quantifiers *}
+consts
Ball :: "[i, i => o] => o"
Bex :: "[i, i => o] => o"
- (* General Union and Intersection *)
+text {*General Union and Intersection *}
+consts
Union :: "i => i"
Inter :: "i => i"
- (* Variations on Replacement *)
+text {*Variations on Replacement *}
+consts
PrimReplace :: "[i, [i, i] => o] => i"
Replace :: "[i, [i, i] => o] => i"
RepFun :: "[i, i => i] => i"
Collect :: "[i, i => o] => i"
- (* Descriptions *)
+
+text {*Descriptions *}
+consts
The :: "(i => o) => i" (binder "THE " 10)
If :: "[o, i, i] => i" ("(if (_)/ then (_)/ else (_))" [10] 10)
@@ -47,46 +49,49 @@
"if(P,a,b)" => "If(P,a,b)"
+
+text {*Finite Sets *}
consts
-
- (* Finite Sets *)
Upair :: "[i, i] => i"
cons :: "[i, i] => i"
succ :: "i => i"
- (* Ordered Pairing *)
+text {*Ordered Pairing *}
+consts
Pair :: "[i, i] => i"
fst :: "i => i"
snd :: "i => i"
- split :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*)
+ split :: "[[i, i] => 'a, i] => 'a::logic" --{*for pattern-matching*}
- (* Sigma and Pi Operators *)
+text {*Sigma and Pi Operators *}
+consts
Sigma :: "[i, i => i] => i"
Pi :: "[i, i => i] => i"
- (* Relations and Functions *)
-
- "domain" :: "i => i"
+text {*Relations and Functions *}
+consts
+ "domain" :: "i => i"
range :: "i => i"
field :: "i => i"
converse :: "i => i"
- relation :: "i => o" (*recognizes sets of pairs*)
- function :: "i => o" (*recognizes functions; can have non-pairs*)
+ relation :: "i => o" --{*recognizes sets of pairs*}
+ function :: "i => o" --{*recognizes functions; can have non-pairs*}
Lambda :: "[i, i => i] => i"
restrict :: "[i, i] => i"
- (* Infixes in order of decreasing precedence *)
+text {*Infixes in order of decreasing precedence *}
+consts
- "``" :: "[i, i] => i" (infixl 90) (*image*)
- "-``" :: "[i, i] => i" (infixl 90) (*inverse image*)
- "`" :: "[i, i] => i" (infixl 90) (*function application*)
+ "``" :: "[i, i] => i" (infixl 90) --{*image*}
+ "-``" :: "[i, i] => i" (infixl 90) --{*inverse image*}
+ "`" :: "[i, i] => i" (infixl 90) --{*function application*}
(*"*" :: "[i, i] => i" (infixr 80) [virtual] Cartesian product*)
- "Int" :: "[i, i] => i" (infixl 70) (*binary intersection*)
- "Un" :: "[i, i] => i" (infixl 65) (*binary union*)
- "-" :: "[i, i] => i" (infixl 65) (*set difference*)
+ "Int" :: "[i, i] => i" (infixl 70) --{*binary intersection*}
+ "Un" :: "[i, i] => i" (infixl 65) --{*binary union*}
+ "-" :: "[i, i] => i" (infixl 65) --{*set difference*}
(*"->" :: "[i, i] => i" (infixr 60) [virtual] function spac\<epsilon>*)
- "<=" :: "[i, i] => o" (infixl 50) (*subset relation*)
- ":" :: "[i, i] => o" (infixl 50) (*membership relation*)
+ "<=" :: "[i, i] => o" (infixl 50) --{*subset relation*}
+ ":" :: "[i, i] => o" (infixl 50) --{*membership relation*}
(*"~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)*)
--- a/src/ZF/equalities.thy Thu Jun 26 18:20:00 2003 +0200
+++ b/src/ZF/equalities.thy Fri Jun 27 13:15:40 2003 +0200
@@ -238,6 +238,9 @@
"A Int cons(a, B) = (if a : A then cons(a, A Int B) else A Int B)"
by auto
+lemma cons_Int_distrib: "cons(x, A \<inter> B) = cons(x, A) \<inter> cons(x, B)"
+by auto
+
subsection{*Binary Union*}
(** Union is the least upper bound of two sets *)