# HG changeset patch # User blanchet # Date 1390253088 -3600 # Node ID 252c7fec41198f26ff8cfe67734f80719346ac7e # Parent 500ef036117ba64fe2f8c896bde32ba8b1cf23ec renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test) diff -r 500ef036117b -r 252c7fec4119 src/HOL/BNF_Cardinal_Order_Relation.thy --- a/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Jan 20 21:45:08 2014 +0100 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Jan 20 22:24:48 2014 +0100 @@ -1504,16 +1504,16 @@ "cofinal A r \ ALL a : Field r. EX b : A. a \ b \ (a,b) : r" -definition regular where -"regular r \ +definition regularCard where +"regularCard r \ ALL K. K \ Field r \ cofinal K r \ |K| =o r" definition relChain where "relChain r As \ ALL i j. (i,j) \ r \ As i \ As j" -lemma regular_UNION: -assumes r: "Card_order r" "regular r" +lemma regularCard_UNION: +assumes r: "Card_order r" "regularCard r" and As: "relChain r As" and Bsub: "B \ (UN i : Field r. As i)" and cardB: "|B| b\B. i \ f b \ (i, f b) \ r" by blast qed moreover have "?K \ Field r" using f by blast - ultimately have "|?K| =o r" using 2 r unfolding regular_def by blast + ultimately have "|?K| =o r" using 2 r unfolding regularCard_def by blast moreover { have "|?K| <=o |B|" using card_of_image . @@ -1548,16 +1548,16 @@ thus ?thesis by blast qed -lemma infinite_cardSuc_regular: +lemma infinite_cardSuc_regularCard: assumes r_inf: "\finite (Field r)" and r_card: "Card_order r" -shows "regular (cardSuc r)" +shows "regularCard (cardSuc r)" proof- let ?r' = "cardSuc r" have r': "Card_order ?r'" "!! p. Card_order p \ (p \o r) = (p Field ?r'" and 2: "cofinal K ?r'" hence "|K| \o |Field ?r'|" by (simp only: card_of_mono1) also have 22: "|Field ?r'| =o ?r'" @@ -1610,10 +1610,10 @@ have "Card_order ?r' \ |B| \ tr'. subtr UNIV tr' tr \ tr' = f (root tr')" definition "regular tr \ \ f. reg f tr" diff -r 500ef036117b -r 252c7fec4119 src/HOL/Cardinals/Cardinal_Order_Relation.thy --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Jan 20 21:45:08 2014 +0100 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Jan 20 22:24:48 2014 +0100 @@ -1623,8 +1623,8 @@ lemma refl_init_seg_of[intro, simp]: "refl init_seg_of" unfolding refl_on_def Field_def by auto -lemma regular_all_ex: -assumes r: "Card_order r" "regular r" +lemma regularCard_all_ex: +assumes r: "Card_order r" "regularCard r" and As: "\ i j b. b \ B \ (i,j) \ r \ P i b \ P j b" and Bsub: "\ b \ B. \ i \ Field r. P i b" and cardB: "|B| ?As i" - apply(rule regular_UNION) using assms unfolding relChain_def by auto + apply(rule regularCard_UNION) using assms unfolding relChain_def by auto thus ?thesis by auto qed @@ -1692,8 +1692,8 @@ |A| (\a \ A. |F a| |SIGMA a : A. F a| finite (Field r)" and reg: "regular r" +lemma regularCard_stable: +assumes cr: "Card_order r" and ir: "\finite (Field r)" and reg: "regularCard r" shows "stable r" unfolding stable_def proof safe fix A :: "'a set" and F :: "'a \ 'a set" assume A: "|A| a\A. |F a| cofinal (f ` L) r" using reg fL unfolding regular_def by (metis not_ordLess_ordIso) + hence "\ cofinal (f ` L) r" using reg fL unfolding regularCard_def by (metis not_ordLess_ordIso) then obtain k where k: "k \ Field r" and "\ l \ L. \ (f l \ k \ (k, f l) \ r)" unfolding cofinal_def image_def by auto hence "\ k \ Field r. \ l \ L. (f l, k) \ r" using r by (metis fL image_subset_iff wo_rel.in_notinI) @@ -1734,7 +1734,7 @@ partial_order_on_def antisym_def by auto ultimately show "\j\g ` A. i \ j \ (i, j) \ r" using a by auto qed - ultimately have "|g ` A| =o r" using reg unfolding regular_def by auto + ultimately have "|g ` A| =o r" using reg unfolding regularCard_def by auto moreover have "|g ` A| \o |A|" by (metis card_of_image) ultimately have False using A by (metis not_ordLess_ordIso ordLeq_ordLess_trans) } @@ -1742,10 +1742,10 @@ using cr not_ordLess_iff_ordLeq by (metis card_of_Well_order card_order_on_well_order_on) qed -lemma stable_regular: +lemma stable_regularCard: assumes cr: "Card_order r" and ir: "\finite (Field r)" and st: "stable r" -shows "regular r" -unfolding regular_def proof safe +shows "regularCard r" +unfolding regularCard_def proof safe fix K assume K: "K \ Field r" and cof: "cofinal K r" have "|K| \o r" using K by (metis card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans) moreover @@ -1807,13 +1807,13 @@ by (auto simp add: finite_iff_ordLess_natLeq) qed -corollary regular_natLeq: "regular natLeq" -using stable_regular[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp +corollary regularCard_natLeq: "regularCard natLeq" +using stable_regularCard[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp lemma stable_cardSuc: assumes CARD: "Card_order r" and INF: "\finite (Field r)" shows "stable(cardSuc r)" -using infinite_cardSuc_regular regular_stable +using infinite_cardSuc_regularCard regularCard_stable by (metis CARD INF cardSuc_Card_order cardSuc_finite) lemma stable_UNION: @@ -1900,10 +1900,10 @@ thus ?thesis using CARD card_of_UNIV2 ordLeq_ordLess_trans by blast qed -corollary infinite_regular_exists: +corollary infinite_regularCard_exists: assumes CARD: "\r \ R. Card_order (r::'a rel)" shows "\(A :: (nat + 'a set)set). - \finite A \ regular |A| \ (\r \ R. r finite A \ regularCard |A| \ (\r \ R. r o" 50) and ordLess2 (infix "") and top ("\") and @@ -33,6 +28,11 @@ cexp (infixr "^c" 90) and convol ("<_ , _>") +hide_const (open) + image2 image2p vimage2p Gr Grp collect fsts snds setl setr + convol pick_middlep fstOp sndOp csquare inver relImage relInvImage + prefCl PrefCl Succ Shift shift proj + no_syntax (xsymbols) "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)