# HG changeset patch # User paulson # Date 1606773623 0 # Node ID 402afc68f2f9ac645b9f556218d1f0a0f109cd1e # Parent d39a32cff5d7f2e08a25f86caf94e09a737fe79a A bunch of suggestions from Pedro Sánchez Terraf diff -r d39a32cff5d7 -r 402afc68f2f9 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Mon Nov 30 19:33:07 2020 +0000 +++ b/src/ZF/Cardinal.thy Mon Nov 30 22:00:23 2020 +0000 @@ -329,7 +329,7 @@ lemma Least_cong: "(!!y. P(y) \ Q(y)) ==> (\ x. P(x)) = (\ x. Q(x))" by simp -(*Need AC to get @{term"X \ Y ==> |X| \ |Y|"}; see well_ord_lepoll_imp_Card_le +(*Need AC to get @{term"X \ Y ==> |X| \ |Y|"}; see well_ord_lepoll_imp_cardinal_le Converse also requires AC, but see well_ord_cardinal_eqE*) lemma cardinal_cong: "X \ Y ==> |X| = |Y|" apply (unfold eqpoll_def cardinal_def) @@ -507,7 +507,7 @@ by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym]) (*Can use AC or finiteness to discharge first premise*) -lemma well_ord_lepoll_imp_Card_le: +lemma well_ord_lepoll_imp_cardinal_le: assumes wB: "well_ord(B,r)" and AB: "A \ B" shows "|A| \ |B|" using Ord_cardinal [of A] Ord_cardinal [of B] @@ -528,7 +528,7 @@ lemma lepoll_cardinal_le: "[| A \ i; Ord(i) |] ==> |A| \ i" apply (rule le_trans) -apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption) +apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_cardinal_le], assumption) apply (erule Ord_cardinal_le) done diff -r d39a32cff5d7 -r 402afc68f2f9 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Mon Nov 30 19:33:07 2020 +0000 +++ b/src/ZF/CardinalArith.thy Mon Nov 30 22:00:23 2020 +0000 @@ -151,7 +151,7 @@ have "K \ |K|" by (rule Card_cardinal_le [OF K]) moreover have "|K| \ |K + L|" using K L - by (blast intro: well_ord_lepoll_imp_Card_le sum_lepoll_self + by (blast intro: well_ord_lepoll_imp_cardinal_le sum_lepoll_self well_ord_radd well_ord_Memrel Card_is_Ord) ultimately show "K \ |K + L|" by (blast intro: le_trans) @@ -173,7 +173,7 @@ "[| K' \ K; L' \ L |] ==> (K' \ L') \ (K \ L)" apply (unfold cadd_def) apply (safe dest!: le_subset_iff [THEN iffD1]) -apply (rule well_ord_lepoll_imp_Card_le) +apply (rule well_ord_lepoll_imp_cardinal_le) apply (blast intro: well_ord_radd well_ord_Memrel) apply (blast intro: sum_lepoll_mono subset_imp_lepoll) done @@ -308,7 +308,7 @@ lemma cmult_square_le: "Card(K) ==> K \ K \ K" apply (unfold cmult_def) apply (rule le_trans) -apply (rule_tac [2] well_ord_lepoll_imp_Card_le) +apply (rule_tac [2] well_ord_lepoll_imp_cardinal_le) apply (rule_tac [3] prod_square_lepoll) apply (simp add: le_refl Card_is_Ord Card_cardinal_eq) apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) @@ -325,7 +325,7 @@ lemma cmult_le_self: "[| Card(K); Ord(L); 0 K \ (K \ L)" apply (unfold cmult_def) -apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le]) +apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_cardinal_le]) apply assumption apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) apply (blast intro: prod_lepoll_self ltD) @@ -347,7 +347,7 @@ "[| K' \ K; L' \ L |] ==> (K' \ L') \ (K \ L)" apply (unfold cmult_def) apply (safe dest!: le_subset_iff [THEN iffD1]) -apply (rule well_ord_lepoll_imp_Card_le) +apply (rule well_ord_lepoll_imp_cardinal_le) apply (blast intro: well_ord_rmult well_ord_Memrel) apply (blast intro: prod_lepoll_mono subset_imp_lepoll) done @@ -548,7 +548,7 @@ assumes K: "Limit(K)" and x: "x succ(x \ y)" shows "|ordermap(K \ K, csquare_rel(K)) ` \x,y\| \ |succ(z)| \ |succ(z)|" -proof (unfold cmult_def, rule well_ord_lepoll_imp_Card_le) +proof (unfold cmult_def, rule well_ord_lepoll_imp_cardinal_le) show "well_ord(|succ(z)| \ |succ(z)|, rmult(|succ(z)|, Memrel(|succ(z)|), |succ(z)|, Memrel(|succ(z)|)))" by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult) @@ -627,10 +627,10 @@ (*Main result: Kunen's Theorem 10.12*) lemma InfCard_csquare_eq: - assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \ K = K" + assumes IK: "InfCard(K)" shows "K \ K = K" proof - have OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) - show "InfCard(K) ==> K \ K = K" using OK + show "K \ K = K" using OK IK proof (induct rule: trans_induct) case (step i) show "i \ i = i" @@ -935,6 +935,6 @@ qed lemma Ord_nat_subset_into_Card: "[| Ord(i); i \ nat |] ==> Card(i)" -by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) + by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) end diff -r d39a32cff5d7 -r 402afc68f2f9 src/ZF/Cardinal_AC.thy --- a/src/ZF/Cardinal_AC.thy Mon Nov 30 19:33:07 2020 +0000 +++ b/src/ZF/Cardinal_AC.thy Mon Nov 30 22:00:23 2020 +0000 @@ -33,9 +33,9 @@ ==> |A \ C| = |B \ D|" by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un) -lemma lepoll_imp_Card_le: "A \ B ==> |A| \ |B|" +lemma lepoll_imp_cardinal_le: "A \ B ==> |A| \ |B|" apply (rule AC_well_ord [THEN exE]) -apply (erule well_ord_lepoll_imp_Card_le, assumption) +apply (erule well_ord_lepoll_imp_cardinal_le, assumption) done lemma cadd_assoc: "(i \ j) \ k = i \ (j \ k)" @@ -82,7 +82,7 @@ lemma le_Card_iff: "Card(K) ==> |A| \ K \ A \ K" apply (erule Card_cardinal_eq [THEN subst], rule iffI, erule Card_le_imp_lepoll) -apply (erule lepoll_imp_Card_le) +apply (erule lepoll_imp_cardinal_le) done lemma cardinal_0_iff_0 [simp]: "|A| = 0 \ A = 0" @@ -132,7 +132,7 @@ text\Kunen's Lemma 10.20\ lemma surj_implies_cardinal_le: assumes f: "f \ surj(X,Y)" shows "|Y| \ |X|" -proof (rule lepoll_imp_Card_le) +proof (rule lepoll_imp_cardinal_le) from f [THEN surj_implies_inj] obtain g where "g \ inj(Y,X)" .. thus "Y \ X" by (auto simp add: lepoll_def) diff -r d39a32cff5d7 -r 402afc68f2f9 src/ZF/Constructible/Formula.thy --- a/src/ZF/Constructible/Formula.thy Mon Nov 30 19:33:07 2020 +0000 +++ b/src/ZF/Constructible/Formula.thy Mon Nov 30 22:00:23 2020 +0000 @@ -80,21 +80,19 @@ (\env \ list(A). bool_of_o (\x\A. satisfies(A,p) ` (Cons(x,env)) = 1))" -lemma "p \ formula ==> satisfies(A,p) \ list(A) -> bool" +lemma satisfies_type: "p \ formula \ satisfies(A,p) \ list(A) -> bool" by (induct set: formula) simp_all abbreviation sats :: "[i,i,i] => o" where "sats(A,p,env) == satisfies(A,p)`env = 1" -lemma [simp]: - "env \ list(A) - ==> sats(A, Member(x,y), env) \ nth(x,env) \ nth(y,env)" +lemma sats_Member_iff [simp]: + "env \ list(A) \ sats(A, Member(x,y), env) \ nth(x,env) \ nth(y,env)" by simp -lemma [simp]: - "env \ list(A) - ==> sats(A, Equal(x,y), env) \ nth(x,env) = nth(y,env)" +lemma sats_Equal_iff [simp]: + "env \ list(A) \ sats(A, Equal(x,y), env) \ nth(x,env) = nth(y,env)" by simp lemma sats_Nand_iff [simp]: diff -r d39a32cff5d7 -r 402afc68f2f9 src/ZF/Constructible/Rank.thy --- a/src/ZF/Constructible/Rank.thy Mon Nov 30 19:33:07 2020 +0000 +++ b/src/ZF/Constructible/Rank.thy Mon Nov 30 22:00:23 2020 +0000 @@ -397,7 +397,7 @@ text\(b) Order types are absolute\ -theorem (in M_ordertype) +theorem (in M_ordertype) ordertypes_are_absolute: "[| wellordered(M,A,r); f \ ord_iso(A, r, i, Memrel(i)); M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)" by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso diff -r d39a32cff5d7 -r 402afc68f2f9 src/ZF/Constructible/Wellorderings.thy --- a/src/ZF/Constructible/Wellorderings.thy Mon Nov 30 19:33:07 2020 +0000 +++ b/src/ZF/Constructible/Wellorderings.thy Mon Nov 30 22:00:23 2020 +0000 @@ -137,8 +137,8 @@ by (unfold transitive_rel_def trans_on_def, blast) lemma (in M_basic) wf_on_imp_relativized: - "wf[A](r) ==> wellfounded_on(M,A,r)" -apply (simp add: wellfounded_on_def wf_def wf_on_def, clarify) + "wf[A](r) \ wellfounded_on(M,A,r)" +apply (clarsimp simp: wellfounded_on_def wf_def wf_on_def) apply (drule_tac x=x in spec, blast) done @@ -164,17 +164,15 @@ ==> order_isomorphism(M,A,r,B,s,f) \ f \ ord_iso(A,r,B,s)" by (simp add: order_isomorphism_def ord_iso_def) -lemma (in M_basic) pred_set_abs [simp]: +lemma (in M_trans) pred_set_abs [simp]: "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) \ B = Order.pred(A,x,r)" apply (simp add: pred_set_def Order.pred_def) apply (blast dest: transM) done lemma (in M_basic) pred_closed [intro,simp]: - "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))" -apply (simp add: Order.pred_def) -apply (insert pred_separation [of r x], simp) -done + "\M(A); M(r); M(x)\ \ M(Order.pred(A, x, r))" + using pred_separation [of r x] by (simp add: Order.pred_def) lemma (in M_basic) membership_abs [simp]: "[| M(r); M(A) |] ==> membership(M,A,r) \ r = Memrel(A)" @@ -190,17 +188,12 @@ done lemma (in M_basic) M_Memrel_iff: - "M(A) ==> - Memrel(A) = {z \ A*A. \x[M]. \y[M]. z = \x,y\ & x \ y}" -apply (simp add: Memrel_def) -apply (blast dest: transM) -done + "M(A) \ Memrel(A) = {z \ A*A. \x[M]. \y[M]. z = \x,y\ & x \ y}" +unfolding Memrel_def by (blast dest: transM) lemma (in M_basic) Memrel_closed [intro,simp]: - "M(A) ==> M(Memrel(A))" -apply (simp add: M_Memrel_iff) -apply (insert Memrel_separation, simp) -done + "M(A) \ M(Memrel(A))" + using Memrel_separation by (simp add: M_Memrel_iff) subsection \Main results of Kunen, Chapter 1 section 6\ @@ -208,19 +201,19 @@ text\Subset properties-- proved outside the locale\ lemma linear_rel_subset: - "[| linear_rel(M,A,r); B<=A |] ==> linear_rel(M,B,r)" + "\linear_rel(M, A, r); B \ A\ \ linear_rel(M, B, r)" by (unfold linear_rel_def, blast) lemma transitive_rel_subset: - "[| transitive_rel(M,A,r); B<=A |] ==> transitive_rel(M,B,r)" + "\transitive_rel(M, A, r); B \ A\ \ transitive_rel(M, B, r)" by (unfold transitive_rel_def, blast) lemma wellfounded_on_subset: - "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)" + "\wellfounded_on(M, A, r); B \ A\ \ wellfounded_on(M, B, r)" by (unfold wellfounded_on_def subset_def, blast) lemma wellordered_subset: - "[| wellordered(M,A,r); B<=A |] ==> wellordered(M,B,r)" + "\wellordered(M, A, r); B \ A\ \ wellordered(M, B, r)" apply (unfold wellordered_def) apply (blast intro: linear_rel_subset transitive_rel_subset wellfounded_on_subset) diff -r d39a32cff5d7 -r 402afc68f2f9 src/ZF/InfDatatype.thy --- a/src/ZF/InfDatatype.thy Mon Nov 30 19:33:07 2020 +0000 +++ b/src/ZF/InfDatatype.thy Mon Nov 30 22:00:23 2020 +0000 @@ -103,7 +103,7 @@ lemmas le_nat_Un_cardinal = Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]] -lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_Card_le] +lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_cardinal_le] (*The new version of Data_Arg.intrs, declared in Datatype.ML*) lemmas Data_Arg_intros =