# HG changeset patch # User paulson # Date 1033471570 -7200 # Node ID 449a70d88b38584a4c6b20730691f975469a0361 # Parent 0b91269c0b13be62d9b718aaf26607e56aada902 Numerous cosmetic changes, prompted by the new simplifier diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/ArithSimp.thy --- a/src/ZF/ArithSimp.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/ArithSimp.thy Tue Oct 01 13:26:10 2002 +0200 @@ -514,14 +514,13 @@ (P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))" apply (case_tac "a < b") apply (force simp add: nat_lt_imp_diff_eq_0) -apply (rule iffI, simp_all) - apply clarify - apply (rotate_tac -1) - apply simp +apply (rule iffI, force) +apply simp apply (drule_tac x="a#-b" in bspec) apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse) done + ML {* val diff_self_eq_0 = thm "diff_self_eq_0"; diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Cardinal.thy Tue Oct 01 13:26:10 2002 +0200 @@ -917,8 +917,7 @@ apply (erule Finite_induct, auto) apply (case_tac "x:A") apply (subgoal_tac [2] "A-cons (x, B) = A - B") -apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}") -apply (rotate_tac -1, simp) +apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp) apply (drule Diff_sing_Finite, auto) done diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/CardinalArith.thy Tue Oct 01 13:26:10 2002 +0200 @@ -30,7 +30,7 @@ be a cardinal*) jump_cardinal :: "i=>i" "jump_cardinal(K) == - UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" + \X\Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" (*needed because jump_cardinal(K) might not be the successor of K*) csucc :: "i=>i" @@ -55,11 +55,11 @@ done lemma Card_UN: - "(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" + "(!!x. x:A ==> Card(K(x))) ==> Card(\x\A. K(x))" by (blast intro: Card_Union) lemma Card_OUN [simp,intro,TC]: - "(!!x. x:A ==> Card(K(x))) ==> Card(UN x Card(K(x))) ==> Card(\x nat ==> n \ nat" @@ -850,16 +850,15 @@ lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1" apply (rule succ_inject) apply (rule_tac b = "|A|" in trans) -apply (simp add: Finite_imp_succ_cardinal_Diff) + apply (simp add: Finite_imp_succ_cardinal_Diff) apply (subgoal_tac "1 \ A") prefer 2 apply (blast intro: not_0_is_lepoll_1) apply (frule Finite_imp_well_ord, clarify) -apply (rotate_tac -1) apply (drule well_ord_lepoll_imp_Card_le) -apply (auto simp add: cardinal_1) + apply (auto simp add: cardinal_1) apply (rule trans) -apply (rule_tac [2] diff_succ) -apply (auto simp add: Finite_cardinal_in_nat) + apply (rule_tac [2] diff_succ) + apply (auto simp add: Finite_cardinal_in_nat) done lemma cardinal_lt_imp_Diff_not_0 [rule_format]: diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Cardinal_AC.thy --- a/src/ZF/Cardinal_AC.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Cardinal_AC.thy Tue Oct 01 13:26:10 2002 +0200 @@ -28,10 +28,10 @@ lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y" by (blast intro: cardinal_cong cardinal_eqE) -lemma cardinal_disjoint_Un: "[| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==> - |A Un C| = |B Un D|" -apply (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un) -done +lemma cardinal_disjoint_Un: + "[| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] + ==> |A Un C| = |B Un D|" +by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un) lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|" apply (rule AC_well_ord [THEN exE]) @@ -85,7 +85,8 @@ apply (erule CollectE) apply (rule_tac A1 = "Y" and B1 = "%y. f-``{y}" in AC_Pi [THEN exE]) apply (fast elim!: apply_Pair) -apply (blast dest: apply_type Pi_memberD intro: apply_equality Pi_type f_imp_injective) +apply (blast dest: apply_type Pi_memberD + intro: apply_equality Pi_type f_imp_injective) done (*Kunen's Lemma 10.20*) @@ -97,7 +98,8 @@ done (*Kunen's Lemma 10.21*) -lemma cardinal_UN_le: "[| InfCard(K); ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K" +lemma cardinal_UN_le: + "[| InfCard(K); ALL i:K. |X(i)| le K |] ==> |\i\K. X(i)| le K" apply (simp add: InfCard_is_Card le_Card_iff) apply (rule lepoll_trans) prefer 2 @@ -108,7 +110,8 @@ apply (erule AC_ball_Pi [THEN exE]) apply (rule exI) (*Lemma needed in both subgoals, for a fixed z*) -apply (subgoal_tac "ALL z: (UN i:K. X (i)). z: X (LEAST i. z:X (i)) & (LEAST i. z:X (i)) : K") +apply (subgoal_tac "ALL z: (\i\K. X (i)). z: X (LEAST i. z:X (i)) & + (LEAST i. z:X (i)) : K") prefer 2 apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI elim!: LeastI Ord_in_Ord) @@ -121,15 +124,14 @@ (*The same again, using csucc*) lemma cardinal_UN_lt_csucc: "[| InfCard(K); ALL i:K. |X(i)| < csucc(K) |] - ==> |UN i:K. X(i)| < csucc(K)" -apply (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal) -done + ==> |\i\K. X(i)| < csucc(K)" +by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal) (*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i), the least ordinal j such that i:Vfrom(A,j). *) lemma cardinal_UN_Ord_lt_csucc: "[| InfCard(K); ALL i:K. j(i) < csucc(K) |] - ==> (UN i:K. j(i)) < csucc(K)" + ==> (\i\K. j(i)) < csucc(K)" apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption) apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE) apply (blast intro!: Ord_UN elim: ltE) @@ -144,7 +146,7 @@ (*Work backwards along the injection from W into K, given that W~=0.*) lemma inj_UN_subset: "[| f: inj(A,B); a:A |] ==> - (UN x:A. C(x)) <= (UN y:B. C(if y: range(f) then converse(f)`y else a))" + (\x\A. C(x)) <= (\y\B. C(if y: range(f) then converse(f)`y else a))" apply (rule UN_least) apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper]) apply (simp add: inj_is_fun [THEN apply_rangeI]) @@ -155,7 +157,7 @@ be weaker.*) lemma le_UN_Ord_lt_csucc: "[| InfCard(K); |W| le K; ALL w:W. j(w) < csucc(K) |] - ==> (UN w:W. j(w)) < csucc(K)" + ==> (\w\W. j(w)) < csucc(K)" apply (case_tac "W=0") (*solve the easy 0 case*) apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc] diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Constructible/AC_in_L.thy --- a/src/ZF/Constructible/AC_in_L.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Constructible/AC_in_L.thy Tue Oct 01 13:26:10 2002 +0200 @@ -240,7 +240,6 @@ apply safe apply (subgoal_tac "Ord(y)") prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord) - apply (rotate_tac -1) apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def Ord_mem_iff_lt) apply (blast intro: lt_trans) diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Tue Oct 01 13:26:10 2002 +0200 @@ -683,10 +683,8 @@ Ord(i); M(i); M(z); \x[M]. \g[M]. function(g) --> M(H(x,g))|] ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" -apply (rotate_tac 2) -apply (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def +by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel) -done theorem (in M_eclose) transrec_closed: @@ -694,10 +692,9 @@ Ord(i); M(i); \x[M]. \g[M]. function(g) --> M(H(x,g))|] ==> M(transrec(i,H))" -apply (rotate_tac 2) -apply (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def - transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel) -done +by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def + transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel) + text{*Helps to prove instances of @{term transrec_replacement}*} lemma (in M_eclose) transrec_replacementI: diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Tue Oct 01 13:26:10 2002 +0200 @@ -1203,7 +1203,6 @@ lemma (in M_basic) restriction_is_function: "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] ==> function(z)" -apply (rotate_tac 1) apply (simp add: restriction_def ball_iff_equiv) apply (unfold function_def, blast) done diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Tue Oct 01 13:26:10 2002 +0200 @@ -225,7 +225,6 @@ lemma (in M_trancl) wellfounded_trancl: "[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)" -apply (rotate_tac -1) apply (simp add: wellfounded_iff_wellfounded_on_field) apply (rule wellfounded_on_subset_A, erule wellfounded_on_trancl) apply blast diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Constructible/WFrec.thy --- a/src/ZF/Constructible/WFrec.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Constructible/WFrec.thy Tue Oct 01 13:26:10 2002 +0200 @@ -143,7 +143,7 @@ apply (drule equalityD1 [THEN subsetD], assumption) apply (blast dest: pair_components_in_M) apply (blast elim!: equalityE dest: pair_components_in_M) - apply (frule transM, assumption, rotate_tac -1) + apply (frule transM, assumption) apply simp apply blast apply (subgoal_tac "is_function(M,f)") @@ -187,7 +187,6 @@ apply (frule pair_components_in_M, assumption, clarify) apply (rule iffI) apply (frule_tac y="" in transM, assumption) - apply (rotate_tac -1) apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff] apply_recfun is_recfun_cut) txt{*Opposite inclusion: something in f, show in Y*} @@ -320,9 +319,7 @@ relativize2(M,MH,H); M(r)|] ==> strong_replacement(M, \x z. \y[M]. pair(M,x,y,z) & (\g[M]. is_recfun(r,x,H,g) & y = H(x,g)))" -apply (rotate_tac 1) -apply (simp add: wfrec_replacement_def is_wfrec_abs) -done +by (simp add: wfrec_replacement_def is_wfrec_abs) lemma wfrec_replacement_cong [cong]: "[| !!x y z. [| M(x); M(y); M(z) |] ==> MH(x,y,z) <-> MH'(x,y,z); diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Constructible/Wellorderings.thy --- a/src/ZF/Constructible/Wellorderings.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Constructible/Wellorderings.thy Tue Oct 01 13:26:10 2002 +0200 @@ -381,7 +381,7 @@ apply (rule iffI) prefer 2 apply blast apply (rule equalityI) - apply (clarify, frule transM, assumption, rotate_tac -1, simp) + apply (clarify, frule transM, assumption, simp) apply (clarify, frule transM, assumption, force) done @@ -392,7 +392,6 @@ ==> z \ f <-> (\a\A. \x[M]. \g[M]. z = & Ord(x) & g \ ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))" -apply (rotate_tac 1) apply (simp add: omap_def Memrel_closed pred_closed) apply (rule iffI) apply (drule_tac [2] x=z in rspec) @@ -432,7 +431,6 @@ lemma (in M_basic) Ord_otype: "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)" -apply (rotate_tac 1) apply (rule OrdI) prefer 2 apply (simp add: Ord_def otype_def omap_def) @@ -454,7 +452,6 @@ lemma (in M_basic) domain_omap: "[| omap(M,A,r,f); obase(M,A,r,B); M(A); M(r); M(B); M(f) |] ==> domain(f) = B" -apply (rotate_tac 2) apply (simp add: domain_closed obase_iff) apply (rule equality_iffI) apply (simp add: domain_iff omap_iff, blast) @@ -463,7 +460,7 @@ lemma (in M_basic) omap_subset: "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); M(A); M(r); M(f); M(B); M(i) |] ==> f \ B * i" -apply (rotate_tac 3, clarify) +apply clarify apply (simp add: omap_iff obase_iff) apply (force simp add: otype_iff) done @@ -471,7 +468,6 @@ lemma (in M_basic) omap_funtype: "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); M(A); M(r); M(f); M(B); M(i) |] ==> f \ B -> i" -apply (rotate_tac 3) apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) done @@ -519,7 +515,6 @@ apply (rule OrdI) prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast) txt{*Hard part is to show that the image is a transitive set.*} -apply (rotate_tac 3) apply (simp add: Transset_def, clarify) apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f B i]]) apply (rename_tac c j, clarify) @@ -552,7 +547,6 @@ lemma (in M_basic) obase_equals: "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); M(A); M(r); M(f); M(B); M(i) |] ==> B = A" -apply (rotate_tac 4) apply (rule equalityI, force simp add: obase_iff, clarify) apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp) apply (frule wellordered_is_wellfounded_on, assumption) diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Epsilon.thy --- a/src/ZF/Epsilon.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Epsilon.thy Tue Oct 01 13:26:10 2002 +0200 @@ -11,13 +11,13 @@ constdefs eclose :: "i=>i" - "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))" + "eclose(A) == \n\nat. nat_rec(n, A, %m r. Union(r))" transrec :: "[i, [i,i]=>i] =>i" "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" rank :: "i=>i" - "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))" + "rank(a) == transrec(a, %x f. \y\x. succ(f`y))" transrec2 :: "[i, i, [i,i]=>i] =>i" "transrec2(k, a, b) == @@ -25,7 +25,7 @@ %i r. if(i=0, a, if(EX j. i=succ(j), b(THE j. i=succ(j), r`(THE j. i=succ(j))), - UN jji, i]=>i" "recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))" @@ -216,7 +216,7 @@ subsection{*Rank*} (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*) -lemma rank: "rank(a) = (UN y:a. succ(rank(y)))" +lemma rank: "rank(a) = (\y\a. succ(rank(y)))" by (subst rank_def [THEN def_transrec], simp) lemma Ord_rank [simp]: "Ord(rank(a))" @@ -268,7 +268,7 @@ apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset]) done -lemma rank_Union: "rank(Union(A)) = (UN x:A. rank(x))" +lemma rank_Union: "rank(Union(A)) = (\x\A. rank(x))" apply (rule equalityI) apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least]) apply (erule_tac [2] Union_upper) @@ -350,7 +350,7 @@ done lemma transrec2_Limit: - "Limit(i) ==> transrec2(i,a,b) = (UN j transrec2(i,a,b) = (\j f(0) = a & f(succ(i)) = b(i, f(i)) & - (Limit(K) --> f(K) = (UN j f(K) = (\j B") prefer 2 apply (blast intro: restrict_type2) diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/InfDatatype.thy --- a/src/ZF/InfDatatype.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/InfDatatype.thy Tue Oct 01 13:26:10 2002 +0200 @@ -15,7 +15,7 @@ lemma fun_Vcsucc_lemma: "[| f: D -> Vfrom(A,csucc(K)); |D| le K; InfCard(K) |] ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)" -apply (rule_tac x = "UN d:D. LEAST i. f`d : Vfrom (A,i) " in exI) +apply (rule_tac x = "\d\D. LEAST i. f`d : Vfrom (A,i) " in exI) apply (rule conjI) apply (rule_tac [2] le_UN_Ord_lt_csucc) apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all) diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Integ/EquivClass.thy --- a/src/ZF/Integ/EquivClass.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Integ/EquivClass.thy Tue Oct 01 13:26:10 2002 +0200 @@ -149,18 +149,15 @@ ==> X=Y" apply (unfold quotient_def, safe) apply (rule equiv_class_eq, assumption) -apply (rotate_tac -2) apply (simp add: UN_equiv_class [of A r b]) done subsection{*Defining Binary Operations upon Equivalence Classes*} - lemma congruent2_implies_congruent: "[| equiv(A,r); congruent2(r,b); a: A |] ==> congruent(r,b(a))" -apply (unfold congruent_def congruent2_def equiv_def refl_def, blast) -done +by (unfold congruent_def congruent2_def equiv_def refl_def, blast) lemma congruent2_implies_congruent_UN: "[| equiv(A,r); congruent2(r,b); a: A |] ==> diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Integ/IntDiv.thy --- a/src/ZF/Integ/IntDiv.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Integ/IntDiv.thy Tue Oct 01 13:26:10 2002 +0200 @@ -658,18 +658,16 @@ (*the case a=0*) lemma quorem_0: "[|b \ #0; b \ int|] ==> quorem (<#0,b>, <#0,#0>)" -apply (rotate_tac -1) -apply (auto simp add: quorem_def neq_iff_zless) -done +by (force simp add: quorem_def neq_iff_zless) lemma posDivAlg_zero_divisor: "posDivAlg() = <#0,a>" apply (subst posDivAlg_unfold) -apply (simp (no_asm)) +apply simp done lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>" apply (subst posDivAlg_unfold) -apply (simp (no_asm) add: not_zle_iff_zless) +apply (simp add: not_zle_iff_zless) done @@ -710,7 +708,6 @@ lemma divAlg_correct: "[|b \ #0; a \ int; b \ int|] ==> quorem (, divAlg())" -apply (rotate_tac 1) apply (auto simp add: quorem_0 divAlg_def) apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct posDivAlg_type negDivAlg_type) @@ -810,7 +807,6 @@ "[|b \ #0; a \ int; b \ int |] ==> quorem (, )" apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) -apply (rotate_tac 1) apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound) done diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/List.thy --- a/src/ZF/List.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/List.thy Tue Oct 01 13:26:10 2002 +0200 @@ -721,8 +721,7 @@ apply (induct_tac "m", auto) apply (erule_tac a = xs in list.cases) apply (auto simp add: take_Nil) -apply (rotate_tac 1) -apply (erule natE) +apply (erule_tac n=n in natE) apply (auto intro: take_0 take_type) done diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/OrdQuant.thy Tue Oct 01 13:26:10 2002 +0200 @@ -20,7 +20,7 @@ (* Ordinal Union *) OUnion :: "[i, i => i] => i" - "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}" + "OUnion(i,B) == {z: \x\i. B(x). Ord(i)}" syntax "@oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10) @@ -77,31 +77,31 @@ apply (auto simp add: lt_def) done -lemma Limit_OUN_eq: "Limit(i) ==> (UN x (\xi\nat.i)=nat *) lemma OUN_least: - "(!!x. x B(x) \ C) ==> (UN x C" + "(!!x. x B(x) \ C) ==> (\x C" by (simp add: OUnion_def UN_least ltI) -(* No < version; consider (UN i:nat.i)=nat *) +(* No < version; consider (\i\nat.i)=nat *) lemma OUN_least_le: - "[| Ord(i); !!x. x b(x) \ i |] ==> (UN x i" + "[| Ord(i); !!x. x b(x) \ i |] ==> (\x i" by (simp add: OUnion_def UN_least_le ltI Ord_0_le) lemma le_implies_OUN_le_OUN: - "[| !!x. x c(x) \ d(x) |] ==> (UN x (UN x c(x) \ d(x) |] ==> (\x (\x Ord(B(x))) - ==> (UN z < (UN x:A. B(x)). C(z)) = (UN x:A. UN z < B(x). C(z))" + ==> (\z < (\x\A. B(x)). C(z)) = (\x\A. \z < B(x). C(z))" by (simp add: OUnion_def) lemma OUN_Union_eq: "(!!x. x:X ==> Ord(x)) - ==> (UN z < Union(X). C(z)) = (UN x:X. UN z < x. C(z))" + ==> (\z < Union(X). C(z)) = (\x\X. \z < x. C(z))" by (simp add: OUnion_def) (*So that rule_format will get rid of ALL x b: (UN z b: (\z R |] ==> R" + "[| b : (\z R |] ==> R" apply (unfold OUnion_def lt_def, blast) done -lemma OUN_iff: "b : (UN x (EX xx (EX x C(x)=D(x) |] ==> (UN x C(x)=D(x) |] ==> (\xxi" (*Construction for linearity theorem*) "ord_iso_map(A,r,B,s) == - UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {}" + \x\A. \y\B. \f \ ord_iso(pred(A,x,r), r, pred(B,y,s), s). {}" first :: "[i, i, i] => o" "first(u, X, R) == u:X & (ALL v:X. v~=u --> : R)" diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/OrderType.thy --- a/src/ZF/OrderType.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/OrderType.thy Tue Oct 01 13:26:10 2002 +0200 @@ -567,7 +567,7 @@ apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+ done -lemma oadd_unfold: "[| Ord(i); Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})" +lemma oadd_unfold: "[| Ord(i); Ord(j) |] ==> i++j = i Un (\k\j. {i++k})" apply (rule subsetI [THEN equalityI]) apply (erule ltI [THEN lt_oadd_disj, THEN disjE]) apply (blast intro: Ord_oadd) @@ -592,12 +592,12 @@ lemma oadd_UN: "[| !!x. x:A ==> Ord(j(x)); a:A |] - ==> i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))" + ==> i ++ (\x\A. j(x)) = (\x\A. i++j(x))" by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD] oadd_lt_mono2 [THEN ltD] elim!: ltE dest!: ltI [THEN lt_oadd_disj]) -lemma oadd_Limit: "Limit(j) ==> i++j = (UN k:j. i++k)" +lemma oadd_Limit: "Limit(j) ==> i++j = (\k\j. i++k)" apply (frule Limit_has_0 [THEN ltD]) apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] Union_eq_UN [symmetric] Limit_Union_eq) @@ -818,7 +818,7 @@ done lemma omult_unfold: - "[| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})" + "[| Ord(i); Ord(j) |] ==> j**i = (\j'\j. \i'\i. {j**i' ++ j'})" apply (rule subsetI [THEN equalityI]) apply (rule lt_omult [THEN exE]) apply (erule_tac [3] ltI) @@ -901,10 +901,10 @@ lemma omult_UN: "[| Ord(i); !!x. x:A ==> Ord(j(x)) |] - ==> i ** (UN x:A. j(x)) = (UN x:A. i**j(x))" + ==> i ** (\x\A. j(x)) = (\x\A. i**j(x))" by (simp (no_asm_simp) add: Ord_UN omult_unfold, blast) -lemma omult_Limit: "[| Ord(i); Limit(j) |] ==> i**j = (UN k:j. i**k)" +lemma omult_Limit: "[| Ord(i); Limit(j) |] ==> i**j = (\k\j. i**k)" by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric] Union_eq_UN [symmetric] Limit_Union_eq) diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Ordinal.thy --- a/src/ZF/Ordinal.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Ordinal.thy Tue Oct 01 13:26:10 2002 +0200 @@ -102,11 +102,11 @@ by (unfold Inter_def Transset_def, blast) lemma Transset_UN: - "(!!x. x \ A ==> Transset(B(x))) ==> Transset (UN x:A. B(x))" + "(!!x. x \ A ==> Transset(B(x))) ==> Transset (\x\A. B(x))" by (rule Transset_Union_family, auto) lemma Transset_INT: - "(!!x. x \ A ==> Transset(B(x))) ==> Transset (INT x:A. B(x))" + "(!!x. x \ A ==> Transset(B(x))) ==> Transset (\x\A. B(x))" by (rule Transset_Inter_family, auto) @@ -555,7 +555,7 @@ done lemma Ord_UN [intro,simp,TC]: - "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))" + "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\x\A. B(x))" by (rule Ord_Union, blast) lemma Ord_Inter [intro,simp,TC]: @@ -567,19 +567,19 @@ done lemma Ord_INT [intro,simp,TC]: - "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))" + "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\x\A. B(x))" by (rule Ord_Inter, blast) -(* No < version; consider (UN i:nat.i)=nat *) +(* No < version; consider (\i\nat.i)=nat *) lemma UN_least_le: - "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i" + "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (\x\A. b(x)) le i" apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le]) apply (blast intro: Ord_UN elim: ltE)+ done lemma UN_succ_least_lt: - "[| j b(x) (UN x:A. succ(b(x))) < i" + "[| j b(x) (\x\A. succ(b(x))) < i" apply (rule ltE, assumption) apply (rule UN_least_le [THEN lt_trans2]) apply (blast intro: succ_leI)+ @@ -590,7 +590,7 @@ by (unfold lt_def, blast) lemma UN_upper_le: - "[| a: A; i le b(a); Ord(UN x:A. b(x)) |] ==> i le (UN x:A. b(x))" + "[| a: A; i le b(a); Ord(\x\A. b(x)) |] ==> i le (\x\A. b(x))" apply (frule ltD) apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le]) apply (blast intro: lt_Ord UN_upper)+ @@ -606,13 +606,13 @@ done lemma le_implies_UN_le_UN: - "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))" + "[| !!x. x:A ==> c(x) le d(x) |] ==> (\x\A. c(x)) le (\x\A. d(x))" apply (rule UN_least_le) apply (rule_tac [2] UN_upper_le) apply (blast intro: Ord_UN le_Ord2)+ done -lemma Ord_equality: "Ord(i) ==> (UN y:i. succ(y)) = i" +lemma Ord_equality: "Ord(i) ==> (\y\i. succ(y)) = i" by (blast intro: Ord_trans) (*Holds for all transitive sets, not just ordinals*) diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/QPair.thy --- a/src/ZF/QPair.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/QPair.thy Tue Oct 01 13:26:10 2002 +0200 @@ -38,7 +38,7 @@ "qconverse(r) == {z. w:r, EX x y. w= & z=}" QSigma :: "[i, i => i] => i" - "QSigma(A,B) == UN x:A. UN y:B(x). {}" + "QSigma(A,B) == \x\A. \y\B(x). {}" syntax "@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10) diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/QUniv.thy --- a/src/ZF/QUniv.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/QUniv.thy Tue Oct 01 13:26:10 2002 +0200 @@ -189,7 +189,7 @@ subset_trans [OF Transset_0 [THEN QPair_Int_Vfrom_subset] QPair_mono] lemma QPair_Int_Vset_subset_UN: - "Ord(i) ==> Int Vset(i) <= (UN j:i. )" + "Ord(i) ==> Int Vset(i) <= (\j\i. )" apply (erule Ord_cases) (*0 case*) apply (simp add: Vfrom_0) diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/equalities.thy --- a/src/ZF/equalities.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/equalities.thy Tue Oct 01 13:26:10 2002 +0200 @@ -62,10 +62,10 @@ lemma bex_Un: "(\x \ A\B. P(x)) <-> (\x \ A. P(x)) | (\x \ B. P(x))"; by blast -lemma ball_UN: "(\z \ (UN x:A. B(x)). P(z)) <-> (\x\A. \z \ B(x). P(z))" +lemma ball_UN: "(\z \ (\x\A. B(x)). P(z)) <-> (\x\A. \z \ B(x). P(z))" by blast -lemma bex_UN: "(\z \ (UN x:A. B(x)). P(z)) <-> (\x\A. \z\B(x). P(z))" +lemma bex_UN: "(\z \ (\x\A. B(x)). P(z)) <-> (\x\A. \z\B(x). P(z))" by blast subsection{*Converse of a Relation*} @@ -136,7 +136,7 @@ lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B" by blast -lemma equal_singleton [rule_format]: "[| a: C; ALL y:C. y=b |] ==> C = {b}" +lemma equal_singleton [rule_format]: "[| a: C; \y\C. y=b |] ==> C = {b}" by blast lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)" @@ -354,7 +354,7 @@ (** Big Union is the least upper bound of a set **) -lemma Union_subset_iff: "Union(A) <= C <-> (ALL 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)" @@ -372,15 +372,15 @@ lemma Union_Int_subset: "Union(A Int B) <= Union(A) Int Union(B)" by blast -lemma Union_disjoint: "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)" +lemma Union_disjoint: "Union(C) Int A = 0 <-> (\B\C. B Int A = 0)" by (blast elim!: equalityE) -lemma Union_empty_iff: "Union(A) = 0 <-> (ALL B:A. B=0)" +lemma Union_empty_iff: "Union(A) = 0 <-> (\B\A. B=0)" by blast (** Big Intersection is the greatest lower bound of a nonempty set **) -lemma Inter_subset_iff: "a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)" +lemma Inter_subset_iff: "a: A ==> C <= Inter(A) <-> (\x\A. C <= x)" by blast lemma Inter_lower: "B:A ==> Inter(A) <= B" @@ -391,11 +391,11 @@ (** Intersection of a family of sets **) -lemma INT_lower: "x:A ==> (INT 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 <= (INT x:A. B(x))" + "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (\x\A. B(x))" by blast lemma Inter_0: "Inter(0) = 0" @@ -422,80 +422,80 @@ subsection{*Unions and Intersections of Families*} -lemma subset_UN_iff_eq: "A <= (UN i:I. B(i)) <-> A = (UN 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: "(UN x:A. B(x)) <= C <-> (ALL 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) <= (UN 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 |] ==> (UN 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) = (UN x:A. x)" +lemma Union_eq_UN: "Union(A) = (\x\A. x)" by blast -lemma Inter_eq_INT: "Inter(A) = (INT x:A. x)" +lemma Inter_eq_INT: "Inter(A) = (\x\A. x)" by (unfold Inter_def, blast) -lemma UN_0 [simp]: "(UN i:0. A(i)) = 0" +lemma UN_0 [simp]: "(\i\0. A(i)) = 0" by blast -lemma UN_singleton: "(UN x:A. {x}) = A" +lemma UN_singleton: "(\x\A. {x}) = A" by blast -lemma UN_Un: "(UN i: A Un B. C(i)) = (UN i: A. C(i)) Un (UN i:B. C(i))" +lemma UN_Un: "(\i\ A Un B. C(i)) = (\i\ A. C(i)) Un (\i\B. C(i))" by blast -lemma INT_Un: "(INT i:I Un J. A(i)) = (if I=0 then INT j:J. A(j) - else if J=0 then INT i:I. A(i) - else ((INT i:I. A(i)) Int (INT j:J. A(j))))" +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 UN_UN_flatten: "(UN x : (UN y:A. B(y)). C(x)) = (UN y:A. UN x: B(y). C(x))" +lemma UN_UN_flatten: "(\x \ (\y\A. B(y)). C(x)) = (\y\A. \x\ B(y). C(x))" by blast (*Halmos, Naive Set Theory, page 35.*) -lemma Int_UN_distrib: "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))" +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 (INT i:I. A(i)) = (INT i:I. B Un A(i))" +lemma Un_INT_distrib: "i:I ==> B Un (\i\I. A(i)) = (\i\I. B Un A(i))" by blast lemma Int_UN_distrib2: - "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))" + "(\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 |] ==> - (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))" + (\i\I. A(i)) Un (\j\J. B(j)) = (\i\I. \j\J. A(i) Un B(j))" by blast -lemma UN_constant: "a: A ==> (UN y:A. c) = c" +lemma UN_constant: "a: A ==> (\y\A. c) = c" by blast -lemma INT_constant: "a: A ==> (INT y:A. c) = c" +lemma INT_constant: "a: A ==> (\y\A. c) = c" by blast -lemma UN_RepFun [simp]: "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))" +lemma UN_RepFun [simp]: "(\y\ RepFun(A,f). B(y)) = (\x\A. B(f(x)))" by blast -lemma INT_RepFun [simp]: "(INT x:RepFun(A,f). B(x)) = (INT a:A. B(f(a)))" +lemma INT_RepFun [simp]: "(\x\RepFun(A,f). B(x)) = (\a\A. B(f(a)))" by (auto simp add: Inter_def) lemma INT_Union_eq: - "0 ~: A ==> (INT x: Union(A). B(x)) = (INT y:A. INT x:y. B(x))" -apply (simp add: Inter_def) -apply (subgoal_tac "ALL x:A. x~=0") -prefer 2 apply blast -apply (tactic "first_best_tac (claset() addss' simpset()) 1") + "0 ~: A ==> (\x\ Union(A). B(x)) = (\y\A. \x\y. B(x))" +apply (subgoal_tac "\x\A. x~=0") + prefer 2 apply blast +apply (force simp add: Inter_def ball_conj_distrib) done -lemma INT_UN_eq: "(ALL x:A. B(x) ~= 0) - ==> (INT z: (UN x:A. B(x)). C(z)) = (INT x:A. INT z: B(x). C(z))" +lemma INT_UN_eq: + "(\x\A. B(x) ~= 0) + ==> (\z\ (\x\A. B(x)). C(z)) = (\x\A. \z\ B(x). C(z))" apply (subst INT_Union_eq, blast) apply (simp add: Inter_def) done @@ -505,23 +505,23 @@ Union of a family of unions **) lemma UN_Un_distrib: - "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))" + "(\i\I. A(i) Un B(i)) = (\i\I. A(i)) Un (\i\I. B(i))" by blast lemma INT_Int_distrib: - "i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))" + "i:I ==> (\i\I. A(i) Int B(i)) = (\i\I. A(i)) Int (\i\I. B(i))" by blast lemma UN_Int_subset: - "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))" + "(\z\I Int J. A(z)) <= (\z\I. A(z)) Int (\z\J. A(z))" by blast (** Devlin, page 12, exercise 5: Complements **) -lemma Diff_UN: "i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))" +lemma Diff_UN: "i:I ==> B - (\i\I. A(i)) = (\i\I. B - A(i))" by blast -lemma Diff_INT: "i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))" +lemma Diff_INT: "i:I ==> B - (\i\I. A(i)) = (\i\I. B - A(i))" by blast (** Unions and Intersections with General Sum **) @@ -541,11 +541,11 @@ by blast lemma SUM_UN_distrib1: - "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))" + "(SUM x:(\y\A. C(y)). B(x)) = (\y\A. SUM x:C(y). B(x))" by blast lemma SUM_UN_distrib2: - "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))" + "(SUM i:I. \j\J. C(i,j)) = (\j\J. SUM i:I. C(i,j))" by blast lemma SUM_Un_distrib1: @@ -573,7 +573,7 @@ by (rule SUM_Int_distrib2) (*Cf Aczel, Non-Well-Founded Sets, page 115*) -lemma SUM_eq_UN: "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))" +lemma SUM_eq_UN: "(SUM i:I. A(i)) = (\i\I. {i} * A(i))" by blast lemma times_subset_iff: @@ -617,10 +617,10 @@ lemma domain_Diff_subset: "domain(A) - domain(B) <= domain(A - B)" by blast -lemma domain_UN: "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))" +lemma domain_UN: "domain(\x\A. B(x)) = (\x\A. domain(B(x)))" by blast -lemma domain_Union: "domain(Union(A)) = (UN x:A. domain(x))" +lemma domain_Union: "domain(Union(A)) = (\x\A. domain(x))" by blast @@ -728,7 +728,7 @@ by blast (** The Union of a set of relations is a relation -- Lemma for fun_Union **) -lemma rel_Union: "(ALL x:S. EX A B. x <= A*B) ==> +lemma rel_Union: "(\x\S. EX A B. x <= A*B) ==> Union(S) <= domain(Union(S)) * range(Union(S))" by blast @@ -745,7 +745,7 @@ subsection{*Image of a Set under a Function or Relation*} -lemma image_iff: "b : r``A <-> (EX x:A. :r)" +lemma image_iff: "b : r``A <-> (\x\A. :r)" by (unfold image_def, blast) lemma image_singleton_iff: "b : r``{a} <-> :r" @@ -791,7 +791,7 @@ subsection{*Inverse Image of a Set under a Function or Relation*} lemma vimage_iff: - "a : r-``B <-> (EX y:B. :r)" + "a : r-``B <-> (\y\B. :r)" by (unfold vimage_def image_def converse_def, blast) lemma vimage_singleton_iff: "a : r-``{b} <-> :r" @@ -820,7 +820,7 @@ by blast (*NOT suitable for rewriting*) -lemma vimage_eq_UN: "f -``B = (UN y:B. f-``{y})" +lemma vimage_eq_UN: "f -``B = (\y\B. f-``{y})" by blast lemma function_vimage_Int: @@ -863,12 +863,12 @@ lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)" by blast -lemma converse_UN [simp]: "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))" +lemma converse_UN [simp]: "converse(\x\A. B(x)) = (\x\A. converse(B(x)))" by blast (*Unfolding Inter avoids using excluded middle on A=0*) lemma converse_INT [simp]: - "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))" + "converse(\x\A. B(x)) = (\x\A. converse(B(x)))" apply (unfold Inter_def, blast) done @@ -887,7 +887,7 @@ lemma Un_Pow_subset: "Pow(A) Un Pow(B) <= Pow(A Un B)" by blast -lemma UN_Pow_subset: "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))" +lemma UN_Pow_subset: "(\x\A. Pow(B(x))) <= Pow(\x\A. B(x))" by blast lemma subset_Pow_Union: "A <= Pow(Union(A))" @@ -899,7 +899,7 @@ lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)" by blast -lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))" +lemma Pow_INT_eq: "x:A ==> Pow(\x\A. B(x)) = (\x\A. Pow(B(x)))" by blast diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/ex/Limit.thy --- a/src/ZF/ex/Limit.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/ex/Limit.thy Tue Oct 01 13:26:10 2002 +0200 @@ -1139,11 +1139,8 @@ apply (assumption | rule cpoI poI)+ apply (simp add: subcpo_rel_eq) apply (assumption | rule cpo_refl subcpo_subset [THEN subsetD])+ -apply (rotate_tac -3) apply (simp add: subcpo_rel_eq) apply (blast intro: subcpo_subset [THEN subsetD] cpo_trans) -(* Changing the order of the assumptions, otherwise simp doesn't work. *) -apply (rotate_tac -2) apply (simp add: subcpo_rel_eq) apply (blast intro: cpo_antisym subcpo_subset [THEN subsetD]) apply (fast intro: islub_subcpo) diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/func.thy --- a/src/ZF/func.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/func.thy Tue Oct 01 13:26:10 2002 +0200 @@ -261,7 +261,7 @@ done (*For this lemma and the next, the right-hand side could equivalently - be written UN x:C. {f`x} *) + be written \x\C. {f`x} *) lemma image_function: "[| function(f); C <= domain(f) |] ==> f``C = {f`x. x:C}"; by (simp add: Repfun_function_if) @@ -505,7 +505,7 @@ by blast lemma UN_mono: - "[| A<=C; !!x. x:A ==> B(x)<=D(x) |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))" + "[| A<=C; !!x. x:A ==> B(x)<=D(x) |] ==> (\x\A. B(x)) <= (\x\C. D(x))" by blast (*Intersection is ANTI-monotonic. There are TWO premises! *)