src/HOL/BNF_Cardinal_Order_Relation.thy
 changeset 55087 252c7fec4119 parent 55059 ef2e0fb783c6 child 55101 57c875e488bd
```     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Jan 20 21:45:08 2014 +0100
1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Jan 20 22:24:48 2014 +0100
1.3 @@ -1504,16 +1504,16 @@
1.4  "cofinal A r \<equiv>
1.5   ALL a : Field r. EX b : A. a \<noteq> b \<and> (a,b) : r"
1.6
1.7 -definition regular where
1.8 -"regular r \<equiv>
1.9 +definition regularCard where
1.10 +"regularCard r \<equiv>
1.11   ALL K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"
1.12
1.13  definition relChain where
1.14  "relChain r As \<equiv>
1.15   ALL i j. (i,j) \<in> r \<longrightarrow> As i \<le> As j"
1.16
1.17 -lemma regular_UNION:
1.18 -assumes r: "Card_order r"   "regular r"
1.19 +lemma regularCard_UNION:
1.20 +assumes r: "Card_order r"   "regularCard r"
1.21  and As: "relChain r As"
1.22  and Bsub: "B \<le> (UN i : Field r. As i)"
1.23  and cardB: "|B| <o r"
1.24 @@ -1537,7 +1537,7 @@
1.25       with b show "\<exists>b\<in>B. i \<noteq> f b \<and> (i, f b) \<in> r" by blast
1.26     qed
1.27     moreover have "?K \<le> Field r" using f by blast
1.28 -   ultimately have "|?K| =o r" using 2 r unfolding regular_def by blast
1.29 +   ultimately have "|?K| =o r" using 2 r unfolding regularCard_def by blast
1.30     moreover
1.31     {
1.32      have "|?K| <=o |B|" using card_of_image .
1.33 @@ -1548,16 +1548,16 @@
1.34    thus ?thesis by blast
1.35  qed
1.36
1.37 -lemma infinite_cardSuc_regular:
1.38 +lemma infinite_cardSuc_regularCard:
1.39  assumes r_inf: "\<not>finite (Field r)" and r_card: "Card_order r"
1.40 -shows "regular (cardSuc r)"
1.41 +shows "regularCard (cardSuc r)"
1.42  proof-
1.43    let ?r' = "cardSuc r"
1.44    have r': "Card_order ?r'"
1.45    "!! p. Card_order p \<longrightarrow> (p \<le>o r) = (p <o ?r')"
1.46    using r_card by (auto simp: cardSuc_Card_order cardSuc_ordLeq_ordLess)
1.47    show ?thesis
1.48 -  unfolding regular_def proof auto
1.49 +  unfolding regularCard_def proof auto
1.50      fix K assume 1: "K \<le> Field ?r'" and 2: "cofinal K ?r'"
1.51      hence "|K| \<le>o |Field ?r'|" by (simp only: card_of_mono1)
1.52      also have 22: "|Field ?r'| =o ?r'"
1.53 @@ -1610,10 +1610,10 @@
1.54    have "Card_order ?r' \<and> |B| <o ?r'"
1.55    using r cardB cardSuc_ordLeq_ordLess cardSuc_Card_order
1.56    card_of_Card_order by blast
1.57 -  moreover have "regular ?r'"
1.58 -  using assms by(simp add: infinite_cardSuc_regular)
1.59 +  moreover have "regularCard ?r'"
1.60 +  using assms by(simp add: infinite_cardSuc_regularCard)
1.61    ultimately show ?thesis
1.62 -  using As Bsub cardB regular_UNION by blast
1.63 +  using As Bsub cardB regularCard_UNION by blast
1.64  qed
1.65
1.66
```