# HG changeset patch # User paulson # Date 1057850081 -7200 # Node ID a1ba833d6b61d61f1573bb10cbd4b254f5816eab # Parent 33147ecac5f90906bb09461902f15fc090db48bb Changed many Intersection rules from i:I to I~=0 to avoid introducing a new variable diff -r 33147ecac5f9 -r a1ba833d6b61 src/ZF/Integ/EquivClass.thy --- a/src/ZF/Integ/EquivClass.thy Wed Jul 09 12:41:47 2003 +0200 +++ b/src/ZF/Integ/EquivClass.thy Thu Jul 10 17:14:41 2003 +0200 @@ -125,9 +125,9 @@ (*Conversion rule*) lemma UN_equiv_class: "[| equiv(A,r); congruent(r,b); a: A |] ==> (UN x:r``{a}. b(x)) = b(a)" -apply (rule trans [OF refl [THEN UN_cong] UN_constant]) -apply (erule_tac [2] equiv_class_self) -prefer 2 apply assumption +apply (subgoal_tac "\x \ r``{a}. b(x) = b(a)") + apply simp + apply (blast intro: equiv_class_self) apply (unfold equiv_def sym_def congruent_def, blast) done diff -r 33147ecac5f9 -r a1ba833d6b61 src/ZF/UNITY/AllocBase.thy --- a/src/ZF/UNITY/AllocBase.thy Wed Jul 09 12:41:47 2003 +0200 +++ b/src/ZF/UNITY/AllocBase.thy Thu Jul 10 17:14:41 2003 +0200 @@ -88,10 +88,7 @@ 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 +by (force simp add: INT_iff) lemma setsum_fun_mono [rule_format]: "n\nat ==> diff -r 33147ecac5f9 -r a1ba833d6b61 src/ZF/UNITY/AllocImpl.thy --- a/src/ZF/UNITY/AllocImpl.thy Wed Jul 09 12:41:47 2003 +0200 +++ b/src/ZF/UNITY/AllocImpl.thy Thu Jul 10 17:14:41 2003 +0200 @@ -575,7 +575,7 @@ n < length(s`giv)}" apply (rule LeadsTo_weaken_R) apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify) -apply (simp add: INT_iff, clarify) +apply (simp add: INT_iff) apply (drule_tac x = "length(x ` giv)" and P = "%x. ?f (x) \ NbT" in bspec) apply simp apply (blast intro: le_trans) @@ -656,10 +656,11 @@ {s\state. \ prefix(tokbag)} LeadsTo {s\state. \ prefix(tokbag)})" apply (rule guaranteesI) -apply (rule INT_I [OF _ list.Nil]) +apply (rule INT_I) apply (rule alloc_progress.final) -apply (simp_all add: alloc_progress_def) +apply (auto simp add: alloc_progress_def) done + end diff -r 33147ecac5f9 -r a1ba833d6b61 src/ZF/UNITY/Distributor.thy --- a/src/ZF/UNITY/Distributor.thy Wed Jul 09 12:41:47 2003 +0200 +++ b/src/ZF/UNITY/Distributor.thy Thu Jul 10 17:14:41 2003 +0200 @@ -81,8 +81,6 @@ apply (cut_tac distr_spec) apply (auto simp add: INT_iff distr_spec_def distr_allowed_acts_def Allowed_def ok_iff_Allowed) -apply (drule_tac [2] x = G and P = "%y. x \ Acts(y)" in bspec) -apply auto apply (drule safety_prop_Acts_iff [THEN [2] rev_iffD1]) apply (auto intro: safety_prop_Inter) done diff -r 33147ecac5f9 -r a1ba833d6b61 src/ZF/UNITY/Follows.thy --- a/src/ZF/UNITY/Follows.thy Wed Jul 09 12:41:47 2003 +0200 +++ b/src/ZF/UNITY/Follows.thy Thu Jul 10 17:14:41 2003 +0200 @@ -274,26 +274,33 @@ \x \ state. g(x):A |] ==> F \ Follows(A, r, g, h)" apply (unfold Follows_def Increasing_def Stable_def) apply (simp add: INT_iff, auto) -apply (rule_tac [3] C = "{s \ state. f (s) =g (s) }" and A = "{s \ state. \ r}" and A' = "{s \ state. \ r}" in Always_LeadsTo_weaken) -apply (erule_tac A = "{s \ state. \ r}" and A' = "{s \ state. \ r}" in Always_Constrains_weaken) +apply (rule_tac [3] C = "{s \ state. f(s)=g(s)}" + and A = "{s \ state. \ r}" + and A' = "{s \ state. \ r}" in Always_LeadsTo_weaken) +apply (erule_tac A = "{s \ state. \ r}" + and A' = "{s \ state. \ r}" in Always_Constrains_weaken) apply auto apply (drule Always_Int_I, assumption) -apply (erule_tac A = "{s \ state . f (s) = g (s) } \ {s \ state . \f (s), h (s) \ \ r}" in Always_weaken) +apply (erule_tac A = "{s \ state. f(s)=g(s)} \ {s \ state. \ r}" + in Always_weaken) apply auto done + lemma Always_Follows2: "[| F \ Always({s \ state. g(s) = h(s)}); F \ Follows(A, r, f, g); \x \ state. h(x):A |] ==> F \ Follows(A, r, f, h)" apply (unfold Follows_def Increasing_def Stable_def) -apply (simp (no_asm_use) add: INT_iff) -apply auto -apply (erule_tac [3] V = "k \ A" in thin_rl) -apply (rule_tac [3] C = "{s \ state. g (s) =h (s) }" and A = "{s \ state. \ r}" and A' = "{s \ state. \ r}" in Always_LeadsTo_weaken) -apply (erule_tac A = "{s \ state. \ r}" and A' = "{s \ state. \ r}" in Always_Constrains_weaken) +apply (simp add: INT_iff, auto) +apply (rule_tac [3] C = "{s \ state. g (s) =h (s) }" + and A = "{s \ state. \ r}" + and A' = "{s \ state. \ r}" in Always_LeadsTo_weaken) +apply (erule_tac A = "{s \ state. \ r}" + and A' = "{s \ state. \ r}" in Always_Constrains_weaken) apply auto apply (drule Always_Int_I, assumption) -apply (erule_tac A = "{s \ state . g (s) = h (s) } \ {s \ state . \f (s), g (s) \ \ r}" in Always_weaken) +apply (erule_tac A = "{s \ state. g(s)=h(s)} \ {s \ state. \ r}" + in Always_weaken) apply auto done diff -r 33147ecac5f9 -r a1ba833d6b61 src/ZF/UNITY/ROOT.ML --- a/src/ZF/UNITY/ROOT.ML Wed Jul 09 12:41:47 2003 +0200 +++ b/src/ZF/UNITY/ROOT.ML Thu Jul 10 17:14:41 2003 +0200 @@ -14,9 +14,7 @@ (*Basic meta-theory*) time_use_thy "Guar"; -(* Prefix relation; part of the Allocator example *) -time_use_thy "GenPrefix"; - +(* Prefix relation; the Allocator example *) time_use_thy "Distributor"; time_use_thy "Merge"; time_use_thy "ClientImpl"; diff -r 33147ecac5f9 -r a1ba833d6b61 src/ZF/UNITY/Union.thy --- a/src/ZF/UNITY/Union.thy Wed Jul 09 12:41:47 2003 +0200 +++ b/src/ZF/UNITY/Union.thy Thu Jul 10 17:14:41 2003 +0200 @@ -13,8 +13,6 @@ theory Union = SubstAx + FP: -declare Inter_0 [simp] - constdefs (*FIXME: conjoin Init(F) Int Init(G) \ 0 *) @@ -160,9 +158,7 @@ lemma Init_JN [simp]: "Init(\i \ I. F(i)) = (if I=0 then state else (\i \ I. Init(F(i))))" -apply (simp add: JOIN_def) -apply (auto elim!: not_emptyE simp add: INT_extend_simps simp del: INT_simps) -done +by (simp add: JOIN_def INT_extend_simps del: INT_simps) lemma Acts_JN [simp]: "Acts(JOIN(I,F)) = cons(id(state), \i \ I. Acts(F(i)))" @@ -208,9 +204,7 @@ lemma JN_Join_distrib: "(\i \ I. F(i) Join G(i)) = (\i \ I. F(i)) Join (\i \ I. G(i))" apply (rule program_equalityI) -apply (simp_all add: Int_absorb) -apply (safe elim!: not_emptyE) -apply (simp_all add: INT_Int_distrib Int_absorb, force) +apply (simp_all add: INT_Int_distrib, blast) done lemma JN_Join_miniscope: "(\i \ I. F(i) Join G) = ((\i \ I. F(i) Join G))" diff -r 33147ecac5f9 -r a1ba833d6b61 src/ZF/ZF.thy --- a/src/ZF/ZF.thy Wed Jul 09 12:41:47 2003 +0200 +++ b/src/ZF/ZF.thy Thu Jul 10 17:14:41 2003 +0200 @@ -538,49 +538,6 @@ the search space.*) -subsection{*Rules for Inter*} - -(*Not obviously useful for proving InterI, InterD, InterE*) -lemma Inter_iff: - "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)" -by (simp add: Inter_def Ball_def, blast) - -(* Intersection is well-behaved only if the family is non-empty! *) -lemma InterI [intro!]: - "[| !!x. x: C ==> A: x; EX c. c:C |] ==> A : Inter(C)" -by (simp add: Inter_iff) - -(*A "destruct" rule -- every B in C contains A as an element, but - A:B can hold when B:C does not! This rule is analogous to "spec". *) -lemma InterD [elim]: "[| A : Inter(C); B : C |] ==> A : B" -by (unfold Inter_def, blast) - -(*"Classical" elimination rule -- does not require exhibiting B:C *) -lemma InterE [elim]: - "[| A : Inter(C); B~:C ==> R; A:B ==> R |] ==> R" -by (simp add: Inter_def, blast) - - -subsection{*Rules for Intersections of families*} -(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *) - -lemma INT_iff: "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)" -by (simp add: Inter_def, best) - -lemma INT_I: - "[| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x))" -by blast - -lemma INT_E: "[| b : (INT x:A. B(x)); a: A |] ==> b : B(a)" -by blast - -lemma INT_cong: - "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A. C(x)) = (INT x:B. D(x))" -by simp - -(*No "Addcongs [INT_cong]" because INT is a combination of constants*) - - subsection{*Rules for the empty set*} (*The set {x:0.False} is empty; by foundation it equals 0 @@ -611,6 +568,48 @@ by blast +subsection{*Rules for Inter*} + +(*Not obviously useful for proving InterI, InterD, InterE*) +lemma Inter_iff: "A : Inter(C) <-> (ALL x:C. A: x) & C\0" +by (simp add: Inter_def Ball_def, blast) + +(* Intersection is well-behaved only if the family is non-empty! *) +lemma InterI [intro!]: + "[| !!x. x: C ==> A: x; C\0 |] ==> A : Inter(C)" +by (simp add: Inter_iff) + +(*A "destruct" rule -- every B in C contains A as an element, but + A:B can hold when B:C does not! This rule is analogous to "spec". *) +lemma InterD [elim]: "[| A : Inter(C); B : C |] ==> A : B" +by (unfold Inter_def, blast) + +(*"Classical" elimination rule -- does not require exhibiting B:C *) +lemma InterE [elim]: + "[| A : Inter(C); B~:C ==> R; A:B ==> R |] ==> R" +by (simp add: Inter_def, blast) + + +subsection{*Rules for Intersections of families*} + +(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *) + +lemma INT_iff: "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & A\0" +by (force simp add: Inter_def) + +lemma INT_I: "[| !!x. x: A ==> b: B(x); A\0 |] ==> b: (INT x:A. B(x))" +by blast + +lemma INT_E: "[| b : (INT x:A. B(x)); a: A |] ==> b : B(a)" +by blast + +lemma INT_cong: + "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A. C(x)) = (INT x:B. D(x))" +by simp + +(*No "Addcongs [INT_cong]" because INT is a combination of constants*) + + subsection{*Rules for Powersets*} lemma PowI: "A <= B ==> A : Pow(B)" diff -r 33147ecac5f9 -r a1ba833d6b61 src/ZF/equalities.thy --- a/src/ZF/equalities.thy Wed Jul 09 12:41:47 2003 +0200 +++ b/src/ZF/equalities.thy Thu Jul 10 17:14:41 2003 +0200 @@ -12,7 +12,7 @@ text{*These cover union, intersection, converse, domain, range, etc. Philippe de Groote proved many of the inclusions.*} -lemma in_mono: "A<=B ==> x:A --> x:B" +lemma in_mono: "A\B ==> x\A --> x\B" by blast lemma the_eq_0 [simp]: "(THE x. False) = 0" @@ -38,25 +38,25 @@ subsection{*Converse of a Relation*} -lemma converse_iff [simp]: ": converse(r) <-> :r" +lemma converse_iff [simp]: "\ converse(r) <-> \r" by (unfold converse_def, blast) -lemma converseI [intro!]: ":r ==> :converse(r)" +lemma converseI [intro!]: "\r ==> \converse(r)" by (unfold converse_def, blast) -lemma converseD: " : converse(r) ==> : r" +lemma converseD: " \ converse(r) ==> \ r" by (unfold converse_def, blast) lemma converseE [elim!]: - "[| yx : converse(r); - !!x y. [| yx=; :r |] ==> P |] + "[| yx \ converse(r); + !!x y. [| yx=; \r |] ==> P |] ==> P" by (unfold converse_def, blast) -lemma converse_converse: "r<=Sigma(A,B) ==> converse(converse(r)) = r" +lemma converse_converse: "r\Sigma(A,B) ==> converse(converse(r)) = r" by blast -lemma converse_type: "r<=A*B ==> converse(r)<=B*A" +lemma converse_type: "r\A*B ==> converse(r)\B*A" by blast lemma converse_prod [simp]: "converse(A*B) = B*A" @@ -66,29 +66,29 @@ by blast lemma converse_subset_iff: - "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B" + "A \ Sigma(X,Y) ==> converse(A) \ converse(B) <-> A \ B" by blast subsection{*Finite Set Constructions Using @{term cons}*} -lemma cons_subsetI: "[| a:C; B<=C |] ==> cons(a,B) <= C" +lemma cons_subsetI: "[| a\C; B\C |] ==> cons(a,B) \ C" by blast -lemma subset_consI: "B <= cons(a,B)" +lemma subset_consI: "B \ cons(a,B)" by blast -lemma cons_subset_iff [iff]: "cons(a,B)<=C <-> a:C & B<=C" +lemma cons_subset_iff [iff]: "cons(a,B)\C <-> a\C & B\C" by blast (*A safe special case of subset elimination, adding no new variables - [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *) + [| cons(a,B) \ C; [| a \ C; B \ C |] ==> R |] ==> R *) lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard] -lemma subset_empty_iff: "A<=0 <-> A=0" +lemma subset_empty_iff: "A\0 <-> A=0" by blast -lemma subset_cons_iff: "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)" +lemma subset_cons_iff: "C\cons(a,B) <-> C\B | (a\C & C-{a} \ B)" by blast (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*) @@ -115,28 +115,28 @@ (** singletons **) -lemma singleton_subsetI: "a:C ==> {a} <= C" +lemma singleton_subsetI: "a\C ==> {a} \ C" by blast -lemma singleton_subsetD: "{a} <= C ==> a:C" +lemma singleton_subsetD: "{a} \ C ==> a\C" by blast (** succ **) -lemma subset_succI: "i <= succ(i)" +lemma subset_succI: "i \ succ(i)" by blast -(*But if j is an ordinal or is transitive, then i:j implies i<=j! +(*But if j is an ordinal or is transitive, then i\j implies i\j! See ordinal/Ord_succ_subsetI*) -lemma succ_subsetI: "[| i:j; i<=j |] ==> succ(i)<=j" +lemma succ_subsetI: "[| i\j; i\j |] ==> succ(i)\j" by (unfold succ_def, blast) lemma succ_subsetE: - "[| succ(i) <= j; [| i:j; i<=j |] ==> P |] ==> P" + "[| succ(i) \ j; [| i\j; i\j |] ==> P |] ==> P" by (unfold succ_def, blast) -lemma succ_subset_iff: "succ(a) <= B <-> (a <= B & a : B)" +lemma succ_subset_iff: "succ(a) \ B <-> (a \ B & a \ B)" by (unfold succ_def, blast) @@ -144,19 +144,19 @@ (** Intersection is the greatest lower bound of two sets **) -lemma Int_subset_iff: "C <= A Int B <-> C <= A & C <= B" +lemma Int_subset_iff: "C \ A Int B <-> C \ A & C \ B" by blast -lemma Int_lower1: "A Int B <= A" +lemma Int_lower1: "A Int B \ A" by blast -lemma Int_lower2: "A Int B <= B" +lemma Int_lower2: "A Int B \ B" by blast -lemma Int_greatest: "[| C<=A; C<=B |] ==> C <= A Int B" +lemma Int_greatest: "[| C\A; C\B |] ==> C \ A Int B" by blast -lemma Int_cons: "cons(a,B) Int C <= cons(a, B Int C)" +lemma Int_cons: "cons(a,B) Int C \ cons(a, B Int C)" by blast lemma Int_absorb [simp]: "A Int A = A" @@ -189,21 +189,21 @@ lemma Int_Un_distrib2: "(B Un C) Int A = (B Int A) Un (C Int A)" by blast -lemma subset_Int_iff: "A<=B <-> A Int B = A" +lemma subset_Int_iff: "A\B <-> A Int B = A" by (blast elim!: equalityE) -lemma subset_Int_iff2: "A<=B <-> B Int A = A" +lemma subset_Int_iff2: "A\B <-> B Int A = A" by (blast elim!: equalityE) -lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B" +lemma Int_Diff_eq: "C\A ==> (A-B) Int C = C-B" by blast lemma Int_cons_left: - "cons(a,A) Int B = (if a : B then cons(a, A Int B) else A Int B)" + "cons(a,A) Int B = (if a \ B then cons(a, A Int B) else A Int B)" by auto lemma Int_cons_right: - "A Int cons(a, B) = (if a : A then cons(a, A Int B) else A Int B)" + "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)" @@ -213,16 +213,16 @@ (** Union is the least upper bound of two sets *) -lemma Un_subset_iff: "A Un B <= C <-> A <= C & B <= C" +lemma Un_subset_iff: "A Un B \ C <-> A \ C & B \ C" by blast -lemma Un_upper1: "A <= A Un B" +lemma Un_upper1: "A \ A Un B" by blast -lemma Un_upper2: "B <= A Un B" +lemma Un_upper2: "B \ A Un B" by blast -lemma Un_least: "[| A<=C; B<=C |] ==> A Un B <= C" +lemma Un_least: "[| A\C; B\C |] ==> A Un B \ C" by blast lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)" @@ -255,10 +255,10 @@ lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)" by blast -lemma subset_Un_iff: "A<=B <-> A Un B = B" +lemma subset_Un_iff: "A\B <-> A Un B = B" by (blast elim!: equalityE) -lemma subset_Un_iff2: "A<=B <-> B Un A = B" +lemma subset_Un_iff2: "A\B <-> B Un A = B" by (blast elim!: equalityE) lemma Un_empty [iff]: "(A Un B = 0) <-> (A = 0 & B = 0)" @@ -269,13 +269,13 @@ subsection{*Set Difference*} -lemma Diff_subset: "A-B <= A" +lemma Diff_subset: "A-B \ A" by blast -lemma Diff_contains: "[| C<=A; C Int B = 0 |] ==> C <= A-B" +lemma Diff_contains: "[| C\A; C Int B = 0 |] ==> C \ A-B" by blast -lemma subset_Diff_cons_iff: "B <= A - cons(c,C) <-> B<=A-C & c ~: B" +lemma subset_Diff_cons_iff: "B \ A - cons(c,C) <-> B\A-C & c ~: B" by blast lemma Diff_cancel: "A - A = 0" @@ -290,7 +290,7 @@ lemma Diff_0 [simp]: "A - 0 = A" by blast -lemma Diff_eq_0_iff: "A - B = 0 <-> A <= B" +lemma Diff_eq_0_iff: "A - B = 0 <-> A \ B" by (blast elim: equalityE) (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) @@ -304,13 +304,13 @@ lemma Diff_disjoint: "A Int (B-A) = 0" by blast -lemma Diff_partition: "A<=B ==> A Un (B-A) = B" +lemma Diff_partition: "A\B ==> A Un (B-A) = B" by blast -lemma subset_Un_Diff: "A <= B Un (A - B)" +lemma subset_Un_Diff: "A \ B Un (A - B)" by blast -lemma double_complement: "[| A<=B; B<=C |] ==> B-(C-A) = A" +lemma double_complement: "[| A\B; B\C |] ==> B-(C-A) = A" by blast lemma double_complement_Un: "(A Un B) - (B-A) = A" @@ -340,7 +340,7 @@ by blast (*Halmos, Naive Set Theory, page 16.*) -lemma Un_Int_assoc_iff: "(A Int B) Un C = A Int (B Un C) <-> C<=A" +lemma Un_Int_assoc_iff: "(A Int B) Un C = A Int (B Un C) <-> C\A" by (blast elim!: equalityE) @@ -348,13 +348,13 @@ (** Big Union is the least upper bound of a set **) -lemma Union_subset_iff: "Union(A) <= C <-> (\x\A. x <= C)" +lemma Union_subset_iff: "Union(A) \ C <-> (\x\A. x \ C)" by blast -lemma Union_upper: "B:A ==> B <= Union(A)" +lemma Union_upper: "B\A ==> B \ Union(A)" by blast -lemma Union_least: "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C" +lemma Union_least: "[| !!x. x\A ==> x\C |] ==> Union(A) \ C" by blast lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)" @@ -363,7 +363,7 @@ lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)" by blast -lemma Union_Int_subset: "Union(A Int B) <= Union(A) Int Union(B)" +lemma Union_Int_subset: "Union(A Int B) \ Union(A) Int Union(B)" by blast lemma Union_disjoint: "Union(C) Int A = 0 <-> (\B\C. B Int A = 0)" @@ -372,39 +372,38 @@ lemma Union_empty_iff: "Union(A) = 0 <-> (\B\A. B=0)" by blast -lemma Int_Union2: "Union(B) Int A = (UN C:B. C Int A)" +lemma Int_Union2: "Union(B) Int A = (\C\B. C Int A)" by blast (** Big Intersection is the greatest lower bound of a nonempty set **) -lemma Inter_subset_iff: "a: A ==> C <= Inter(A) <-> (\x\A. C <= x)" +lemma Inter_subset_iff: "A\0 ==> C \ Inter(A) <-> (\x\A. C \ x)" by blast -lemma Inter_lower: "B:A ==> Inter(A) <= B" +lemma Inter_lower: "B\A ==> Inter(A) \ B" by blast -lemma Inter_greatest: "[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)" +lemma Inter_greatest: "[| A\0; !!x. x\A ==> C\x |] ==> C \ Inter(A)" by blast (** Intersection of a family of sets **) -lemma INT_lower: "x:A ==> (\x\A. B(x)) <= B(x)" +lemma INT_lower: "x\A ==> (\x\A. B(x)) \ B(x)" by blast -lemma INT_greatest: - "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (\x\A. B(x))" -by blast +lemma INT_greatest: "[| A\0; !!x. x\A ==> C\B(x) |] ==> C \ (\x\A. B(x))" +by force -lemma Inter_0: "Inter(0) = 0" +lemma Inter_0 [simp]: "Inter(0) = 0" by (unfold Inter_def, blast) lemma Inter_Un_subset: - "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)" + "[| z\A; z\B |] ==> Inter(A) Un Inter(B) \ Inter(A Int B)" by blast (* A good challenge: Inter is ill-behaved on the empty set *) lemma Inter_Un_distrib: - "[| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)" + "[| A\0; B\0 |] ==> Inter(A Un B) = Inter(A) Int Inter(B)" by blast lemma Union_singleton: "Union({b}) = b" @@ -419,16 +418,16 @@ subsection{*Unions and Intersections of Families*} -lemma subset_UN_iff_eq: "A <= (\i\I. B(i)) <-> A = (\i\I. A Int B(i))" +lemma subset_UN_iff_eq: "A \ (\i\I. B(i)) <-> A = (\i\I. A Int B(i))" by (blast elim!: equalityE) -lemma UN_subset_iff: "(\x\A. B(x)) <= C <-> (\x\A. B(x) <= C)" +lemma UN_subset_iff: "(\x\A. B(x)) \ C <-> (\x\A. B(x) \ C)" by blast -lemma UN_upper: "x:A ==> B(x) <= (\x\A. B(x))" +lemma UN_upper: "x\A ==> B(x) \ (\x\A. B(x))" by (erule RepFunI [THEN Union_upper]) -lemma UN_least: "[| !!x. x:A ==> B(x)<=C |] ==> (\x\A. B(x)) <= C" +lemma UN_least: "[| !!x. x\A ==> B(x)\C |] ==> (\x\A. B(x)) \ C" by blast lemma Union_eq_UN: "Union(A) = (\x\A. x)" @@ -446,12 +445,11 @@ lemma UN_Un: "(\i\ A Un B. C(i)) = (\i\ A. C(i)) Un (\i\B. C(i))" by blast -lemma INT_Un: "(\i\I Un J. A(i)) = (if I=0 then \j\J. A(j) - else if J=0 then \i\I. A(i) - else ((\i\I. A(i)) Int (\j\J. A(j))))" -apply simp -apply (blast intro!: equalityI) -done +lemma INT_Un: "(\i\I Un J. A(i)) = + (if I=0 then \j\J. A(j) + else if J=0 then \i\I. A(i) + else ((\i\I. A(i)) Int (\j\J. A(j))))" +by (simp, blast intro!: equalityI) lemma UN_UN_flatten: "(\x \ (\y\A. B(y)). C(x)) = (\y\A. \x\ B(y). C(x))" by blast @@ -460,22 +458,22 @@ lemma Int_UN_distrib: "B Int (\i\I. A(i)) = (\i\I. B Int A(i))" by blast -lemma Un_INT_distrib: "i:I ==> B Un (\i\I. A(i)) = (\i\I. B Un A(i))" -by blast +lemma Un_INT_distrib: "I\0 ==> B Un (\i\I. A(i)) = (\i\I. B Un A(i))" +by auto lemma Int_UN_distrib2: "(\i\I. A(i)) Int (\j\J. B(j)) = (\i\I. \j\J. A(i) Int B(j))" by blast -lemma Un_INT_distrib2: "[| i:I; j:J |] ==> +lemma Un_INT_distrib2: "[| I\0; J\0 |] ==> (\i\I. A(i)) Un (\j\J. B(j)) = (\i\I. \j\J. A(i) Un B(j))" -by blast +by auto -lemma UN_constant: "a: A ==> (\y\A. c) = c" -by blast +lemma UN_constant [simp]: "(\y\A. c) = (if A=0 then 0 else c)" +by force -lemma INT_constant: "a: A ==> (\y\A. c) = c" -by blast +lemma INT_constant [simp]: "(\y\A. c) = (if A=0 then 0 else c)" +by force lemma UN_RepFun [simp]: "(\y\ RepFun(A,f). B(y)) = (\x\A. B(f(x)))" by blast @@ -506,20 +504,21 @@ by blast lemma INT_Int_distrib: - "i:I ==> (\i\I. A(i) Int B(i)) = (\i\I. A(i)) Int (\i\I. B(i))" -by blast + "I\0 ==> (\i\I. A(i) Int B(i)) = (\i\I. A(i)) Int (\i\I. B(i))" +by (blast elim!: not_emptyE) lemma UN_Int_subset: - "(\z\I Int J. A(z)) <= (\z\I. A(z)) Int (\z\