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