src/HOL/Cardinals/Cardinal_Order_Relation.thy
changeset 55087 252c7fec4119
parent 55056 b5c94200d081
child 55102 761e40ce91bc
     1.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Jan 20 21:45:08 2014 +0100
     1.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Jan 20 22:24:48 2014 +0100
     1.3 @@ -1623,8 +1623,8 @@
     1.4  lemma refl_init_seg_of[intro, simp]: "refl init_seg_of"
     1.5  unfolding refl_on_def Field_def by auto
     1.6  
     1.7 -lemma regular_all_ex:
     1.8 -assumes r: "Card_order r"   "regular r"
     1.9 +lemma regularCard_all_ex:
    1.10 +assumes r: "Card_order r"   "regularCard r"
    1.11  and As: "\<And> i j b. b \<in> B \<Longrightarrow> (i,j) \<in> r \<Longrightarrow> P i b \<Longrightarrow> P j b"
    1.12  and Bsub: "\<forall> b \<in> B. \<exists> i \<in> Field r. P i b"
    1.13  and cardB: "|B| <o r"
    1.14 @@ -1632,7 +1632,7 @@
    1.15  proof-
    1.16    let ?As = "\<lambda>i. {b \<in> B. P i b}"
    1.17    have "EX i : Field r. B \<le> ?As i"
    1.18 -  apply(rule regular_UNION) using assms unfolding relChain_def by auto
    1.19 +  apply(rule regularCard_UNION) using assms unfolding relChain_def by auto
    1.20    thus ?thesis by auto
    1.21  qed
    1.22  
    1.23 @@ -1692,8 +1692,8 @@
    1.24                 |A| <o r \<and> (\<forall>a \<in> A. |F a| <o r)
    1.25                 \<longrightarrow> |SIGMA a : A. F a| <o r"
    1.26  
    1.27 -lemma regular_stable:
    1.28 -assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regular r"
    1.29 +lemma regularCard_stable:
    1.30 +assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regularCard r"
    1.31  shows "stable r"
    1.32  unfolding stable_def proof safe
    1.33    fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set" assume A: "|A| <o r" and F: "\<forall>a\<in>A. |F a| <o r"
    1.34 @@ -1710,7 +1710,7 @@
    1.35      apply(rule exI[of _ snd]) unfolding bij_betw_def inj_on_def by (auto simp: image_def)
    1.36      hence "|L| <o r" using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
    1.37      hence "|f ` L| <o r" using ordLeq_ordLess_trans[OF card_of_image, of "L"] unfolding L_def by auto
    1.38 -    hence "\<not> cofinal (f ` L) r" using reg fL unfolding regular_def by (metis not_ordLess_ordIso)
    1.39 +    hence "\<not> cofinal (f ` L) r" using reg fL unfolding regularCard_def by (metis not_ordLess_ordIso)
    1.40      then obtain k where k: "k \<in> Field r" and "\<forall> l \<in> L. \<not> (f l \<noteq> k \<and> (k, f l) \<in> r)"
    1.41      unfolding cofinal_def image_def by auto
    1.42      hence "\<exists> k \<in> Field r. \<forall> l \<in> L. (f l, k) \<in> r" using r by (metis fL image_subset_iff wo_rel.in_notinI)
    1.43 @@ -1734,7 +1734,7 @@
    1.44       partial_order_on_def antisym_def by auto
    1.45       ultimately show "\<exists>j\<in>g ` A. i \<noteq> j \<and> (i, j) \<in> r" using a by auto
    1.46     qed
    1.47 -   ultimately have "|g ` A| =o r" using reg unfolding regular_def by auto
    1.48 +   ultimately have "|g ` A| =o r" using reg unfolding regularCard_def by auto
    1.49     moreover have "|g ` A| \<le>o |A|" by (metis card_of_image)
    1.50     ultimately have False using A by (metis not_ordLess_ordIso ordLeq_ordLess_trans)
    1.51    }
    1.52 @@ -1742,10 +1742,10 @@
    1.53    using cr not_ordLess_iff_ordLeq by (metis card_of_Well_order card_order_on_well_order_on)
    1.54  qed
    1.55  
    1.56 -lemma stable_regular:
    1.57 +lemma stable_regularCard:
    1.58  assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and st: "stable r"
    1.59 -shows "regular r"
    1.60 -unfolding regular_def proof safe
    1.61 +shows "regularCard r"
    1.62 +unfolding regularCard_def proof safe
    1.63    fix K assume K: "K \<subseteq> Field r" and cof: "cofinal K r"
    1.64    have "|K| \<le>o r" using K by (metis card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans)
    1.65    moreover
    1.66 @@ -1807,13 +1807,13 @@
    1.67    by (auto simp add: finite_iff_ordLess_natLeq)
    1.68  qed
    1.69  
    1.70 -corollary regular_natLeq: "regular natLeq"
    1.71 -using stable_regular[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
    1.72 +corollary regularCard_natLeq: "regularCard natLeq"
    1.73 +using stable_regularCard[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
    1.74  
    1.75  lemma stable_cardSuc:
    1.76  assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
    1.77  shows "stable(cardSuc r)"
    1.78 -using infinite_cardSuc_regular regular_stable
    1.79 +using infinite_cardSuc_regularCard regularCard_stable
    1.80  by (metis CARD INF cardSuc_Card_order cardSuc_finite)
    1.81  
    1.82  lemma stable_UNION:
    1.83 @@ -1900,10 +1900,10 @@
    1.84    thus ?thesis using CARD card_of_UNIV2 ordLeq_ordLess_trans by blast
    1.85  qed
    1.86  
    1.87 -corollary infinite_regular_exists:
    1.88 +corollary infinite_regularCard_exists:
    1.89  assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
    1.90  shows "\<exists>(A :: (nat + 'a set)set).
    1.91 -          \<not>finite A \<and> regular |A| \<and> (\<forall>r \<in> R. r <o |A| )"
    1.92 -using infinite_stable_exists[OF CARD] stable_regular by (metis Field_card_of card_of_card_order_on)
    1.93 +          \<not>finite A \<and> regularCard |A| \<and> (\<forall>r \<in> R. r <o |A| )"
    1.94 +using infinite_stable_exists[OF CARD] stable_regularCard by (metis Field_card_of card_of_card_order_on)
    1.95  
    1.96  end