# HG changeset patch # User paulson # Date 1056712540 -7200 # Node ID 5cfc8b9fb880d4682583d5c4007e641120acbfa3 # Parent ab2e26ae90e349200997d65d646e3ae7be14d884 Conversion of AllocBase to new-style diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/Cardinal.thy --- 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"; diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/IsaMakefile --- 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\ diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/List.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\list(A) ==> \n\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*} diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/UNITY/AllocBase.ML --- 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 \\ 0 & NbT \\ 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\\nat & NbT\\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\\Inter(RepFun(Nclients, B)) <-> (\\x\\Nclients. b\\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\\nat ==> \ -\ (\\i\\nat. i 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\\x" 1); -by (Clarify_tac 1); -by (Asm_simp_tac 1); -by (subgoal_tac "\\i\\nat. i 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\\list(A) ==> tokens(l)\\nat"; -by (etac list.induct 1); -by Auto_tac; -qed "tokens_type"; -AddTCs [tokens_type]; -Addsimps [tokens_type]; - -Goal "xs\\list(A) ==> \\ys\\list(A). \\prefix(A) \ -\ --> tokens(xs) \\ 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 "\\prefix(A) ==> tokens(xs) \\ 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\\list(A); ys\\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\\list(A) ==> \\n\\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\\list(A) ==>bag_of(l)\\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\\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\\list(A); ys\\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\\list(A) ==> \\ys\\list(A). \\prefix(A) \ -\ --> \\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 "[| \\prefix(A); xs\\list(A); ys\\list(A) |] ==> \ -\ \\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 \\ list(A) ==> C Int length(l) \\ 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 \\ list(A); k \\ C \\ length(xs)|] ==> k < length(xs)"; -by (asm_full_simp_tac (simpset() addsimps [ltI]) 1); -qed "mem_Int_imp_lt_length"; - - -Goal "[|C \\ nat; x \\ A; xs \\ list(A)|] \ -\ ==> msetsum(\\i. {#nth(i, xs @ [x])#}, C \\ succ(length(xs)), A) = \ -\ (if length(xs) \\ C then \ -\ {#x#} +# msetsum(\\x. {#nth(x, xs)#}, C \\ length(xs), A) \ -\ else msetsum(\\x. {#nth(x, xs)#}, C \\ 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\\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 \\ list(A) ==> nat \\ 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\\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\\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\\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); \\i\\I. \\j\\I. i\\j --> A(i) \\ A(j) = 0; \ -\ l\\list(B) |] \ -\ ==> bag_of(sublist(l, \\i\\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\\set_of_list(l) --> False) & (a \\ 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\\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)\\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\\nat ==> nat_list_inj(n)\\list(nat)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "nat_list_inj_type"; - -Goal "n\\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] - "(\\x\\nat. nat_var_inj(x))\\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", "(\\x\\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) ==> \\x. x\\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\\(Inter(RepFun(var-A, B))) <-> (\\x\\var-A. b\\B(x))"; -by (subgoal_tac "\\x. x\\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\\Inter(RepFun(var-A, B)); Finite(A); x\\var-A |] ==> b\\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); (\\x\\var-A. b\\B(x)) |] ==> b\\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 \\ 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 \\ B) = cons(x, A) \\ cons(x, B)"; -by Auto_tac; -qed "cons_Int_distrib"; - - -(* Currently not used, but of potential interest *) -Goal -"[| Finite(A); \\x\\A. g(x)\\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; \\x\\A. f(x)=g(x); \\x\\A. g(x)\\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"; - - - - diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/UNITY/AllocBase.thy --- 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 \ nat-{0}" + Nclients_pos: "Nclients \ 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 \ 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 \ 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 \ 0 & NbT \ 0" +by (cut_tac Nclients_pos NbT_pos, auto) + +lemma Nclients_type [simp,TC]: "Nclients\nat" +by (cut_tac Nclients_pos NbT_pos, auto) + +lemma NbT_type [simp,TC]: "NbT\nat" +by (cut_tac Nclients_pos NbT_pos, auto) + +lemma INT_Nclient_iff [iff]: + "b\Inter(RepFun(Nclients, B)) <-> (\x\Nclients. b\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\nat ==> + (\i\nat. i f(i) $<= g(i)) --> + setsum(f, n) $<= setsum(g,n)" +apply (induct_tac "n", simp_all) +apply (subgoal_tac "Finite(x) & x\x") + prefer 2 apply (simp add: nat_into_Finite mem_not_refl, clarify) +apply (simp (no_asm_simp) add: succ_def) +apply (subgoal_tac "\i\nat. i f(i) $<= g(i) ") + prefer 2 apply (force dest: leI) +apply (rule zadd_zle_mono, simp_all) +done + +lemma tokens_type [simp,TC]: "l\list(A) ==> tokens(l)\nat" +by (erule list.induct, auto) + +lemma tokens_mono_aux [rule_format]: + "xs\list(A) ==> \ys\list(A). \prefix(A) + --> tokens(xs) \ tokens(ys)" +apply (induct_tac "xs") +apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: prefix_def) +done + +lemma tokens_mono: "\prefix(A) ==> tokens(xs) \ 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\list(A); ys\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\list(A) ==>bag_of(l)\Mult(A)" +apply (induct_tac "l") +apply (auto simp add: Mult_iff_multiset) +done + +lemma bag_of_multiset: + "l\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\list(A); ys\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\list(A) ==> \ys\list(A). \prefix(A) + --> \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]: + "[| \prefix(A); xs\list(A); ys\list(A) |] + ==> \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 \ list(A) ==> C Int length(l) \ 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 \ list(A); k \ C \ length(xs)|] ==> k < length(xs)" +apply (simp add: ltI) +done + + +lemma bag_of_sublist_lemma: + "[|C \ nat; x \ A; xs \ list(A)|] + ==> msetsum(\i. {#nth(i, xs @ [x])#}, C \ succ(length(xs)), A) = + (if length(xs) \ C then + {#x#} +# msetsum(\x. {#nth(x, xs)#}, C \ length(xs), A) + else msetsum(\x. {#nth(x, xs)#}, C \ 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\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 \ list(A) ==> nat \ length(l) = length(l)" +apply (rule Int_absorb1) +apply (rule OrdmemD, auto) +done + +(*eliminating the assumption C<=nat*) +lemma bag_of_sublist: + "l\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\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\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); \i\I. \j\I. i\j --> A(i) \ A(j) = 0; + l\list(B) |] + ==> bag_of(sublist(l, \i\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\set_of_list(l) --> False) & (a \ 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\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)\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\nat ==> nat_list_inj(n)\list(nat)" +by (induct_tac "n", auto) + +lemma length_nat_list_inj: "n\nat ==> length(nat_list_inj(n)) = n" +by (induct_tac "n", auto) + +lemma var_infinite_lemma: + "(\x\nat. nat_var_inj(x))\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 = " (\x\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) ==> \x. x\A" +apply (subgoal_tac "A\0") +apply (auto simp add: Finite_0) +done + +lemma Inter_Diff_var_iff: + "Finite(A) ==> b\(Inter(RepFun(var-A, B))) <-> (\x\var-A. b\B(x))" +apply (subgoal_tac "\x. x\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\Inter(RepFun(var-A, B)); Finite(A); x\var-A |] ==> b\B(x)" +by (simp add: Inter_Diff_var_iff) + +(* [| Finite(A); (\x\var-A. b\B(x)) |] ==> b\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 \ Pow(state*state) <-> Acts(F)<=A" +by (insert Acts_type [of F], auto) + +lemma setsum_nsetsum_eq: + "[| Finite(A); \x\A. g(x)\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; \x\A. f(x)=g(x); \x\A. g(x)\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 diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/UNITY/AllocImpl.thy --- 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 \ program; alloc_prog ok G; alloc_prog \ G \ Incr(lift(ask)); @@ -405,22 +406,24 @@ ==> alloc_prog \ G \ Always({s\state. tokens(s`giv) \ tokens(take(s`NbR, s`rel)) --> NbT \ s`available_tok})" -apply (subgoal_tac "alloc_prog \ G \ Always ({s\state. s`NbR \ length(s`rel) } \ {s\state. s`available_tok #+ tokens(s`giv) = NbT #+ tokens(take (s`NbR, s`rel))}) ") +apply (subgoal_tac + "alloc_prog \ G + \ Always ({s\state. s`NbR \ length(s`rel) } \ + {s\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 \ 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: diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/UNITY/Guar.ML --- 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"; diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/UNITY/Merge.thy --- 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 \ state ==> s`Out \ 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 \ state ==> s`iOut \ 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 \ program" @@ -123,7 +121,7 @@ ==> M \ G \ Always({s \ state. length(s`Out)=length(s`iOut)})" apply (frule preserves_type [THEN subsetD]) apply (subgoal_tac "G \ 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 " (\i \ Nclients. {k \ 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) \ 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 \ 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]) diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/UNITY/Union.ML --- 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]; diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/ZF.thy --- 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\*) - "<=" :: "[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*)*) diff -r ab2e26ae90e3 -r 5cfc8b9fb880 src/ZF/equalities.thy --- 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 \ B) = cons(x, A) \ cons(x, B)" +by auto + subsection{*Binary Union*} (** Union is the least upper bound of two sets *)