# 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 \<equiv>
  ALL a : Field r. EX b : A. a \<noteq> b \<and> (a,b) : r"
 
-definition regular where
-"regular r \<equiv>
+definition regularCard where
+"regularCard r \<equiv>
  ALL K. K \<le> Field r \<and> cofinal K r \<longrightarrow> |K| =o r"
 
 definition relChain where
 "relChain r As \<equiv>
  ALL i j. (i,j) \<in> r \<longrightarrow> As i \<le> 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 \<le> (UN i : Field r. As i)"
 and cardB: "|B| <o r"
@@ -1537,7 +1537,7 @@
      with b show "\<exists>b\<in>B. i \<noteq> f b \<and> (i, f b) \<in> r" by blast
    qed
    moreover have "?K \<le> 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: "\<not>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 \<longrightarrow> (p \<le>o r) = (p <o ?r')"
   using r_card by (auto simp: cardSuc_Card_order cardSuc_ordLeq_ordLess)
   show ?thesis
-  unfolding regular_def proof auto
+  unfolding regularCard_def proof auto
     fix K assume 1: "K \<le> Field ?r'" and 2: "cofinal K ?r'"
     hence "|K| \<le>o |Field ?r'|" by (simp only: card_of_mono1)
     also have 22: "|Field ?r'| =o ?r'"
@@ -1610,10 +1610,10 @@
   have "Card_order ?r' \<and> |B| <o ?r'"
   using r cardB cardSuc_ordLeq_ordLess cardSuc_Card_order
   card_of_Card_order by blast
-  moreover have "regular ?r'"
-  using assms by(simp add: infinite_cardSuc_regular)
+  moreover have "regularCard ?r'"
+  using assms by(simp add: infinite_cardSuc_regularCard)
   ultimately show ?thesis
-  using As Bsub cardB regular_UNION by blast
+  using As Bsub cardB regularCard_UNION by blast
 qed
 
 
diff -r 500ef036117b -r 252c7fec4119 src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy
--- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 21:45:08 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 22:24:48 2014 +0100
@@ -681,8 +681,6 @@
 
 subsection{* Regular Trees *}
 
-hide_const regular
-
 definition "reg f tr \<equiv> \<forall> tr'. subtr UNIV tr' tr \<longrightarrow> tr' = f (root tr')"
 definition "regular tr \<equiv> \<exists> 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: "\<And> i j b. b \<in> B \<Longrightarrow> (i,j) \<in> r \<Longrightarrow> P i b \<Longrightarrow> P j b"
 and Bsub: "\<forall> b \<in> B. \<exists> i \<in> Field r. P i b"
 and cardB: "|B| <o r"
@@ -1632,7 +1632,7 @@
 proof-
   let ?As = "\<lambda>i. {b \<in> B. P i b}"
   have "EX i : Field r. B \<le> ?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| <o r \<and> (\<forall>a \<in> A. |F a| <o r)
                \<longrightarrow> |SIGMA a : A. F a| <o r"
 
-lemma regular_stable:
-assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regular r"
+lemma regularCard_stable:
+assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regularCard r"
 shows "stable r"
 unfolding stable_def proof safe
   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"
@@ -1710,7 +1710,7 @@
     apply(rule exI[of _ snd]) unfolding bij_betw_def inj_on_def by (auto simp: image_def)
     hence "|L| <o r" using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
     hence "|f ` L| <o r" using ordLeq_ordLess_trans[OF card_of_image, of "L"] unfolding L_def by auto
-    hence "\<not> cofinal (f ` L) r" using reg fL unfolding regular_def by (metis not_ordLess_ordIso)
+    hence "\<not> cofinal (f ` L) r" using reg fL unfolding regularCard_def by (metis not_ordLess_ordIso)
     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)"
     unfolding cofinal_def image_def by auto
     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)
@@ -1734,7 +1734,7 @@
      partial_order_on_def antisym_def by auto
      ultimately show "\<exists>j\<in>g ` A. i \<noteq> j \<and> (i, j) \<in> 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| \<le>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: "\<not>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 \<subseteq> Field r" and cof: "cofinal K r"
   have "|K| \<le>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: "\<not>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: "\<forall>r \<in> R. Card_order (r::'a rel)"
 shows "\<exists>(A :: (nat + 'a set)set).
-          \<not>finite A \<and> regular |A| \<and> (\<forall>r \<in> R. r <o |A| )"
-using infinite_stable_exists[OF CARD] stable_regular by (metis Field_card_of card_of_card_order_on)
+          \<not>finite A \<and> regularCard |A| \<and> (\<forall>r \<in> R. r <o |A| )"
+using infinite_stable_exists[OF CARD] stable_regularCard by (metis Field_card_of card_of_card_order_on)
 
 end
diff -r 500ef036117b -r 252c7fec4119 src/HOL/Library/Cardinal_Notations.thy
--- a/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 21:45:08 2014 +0100
+++ b/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 22:24:48 2014 +0100
@@ -16,7 +16,7 @@
   ordLeq3 (infix "\<le>o" 50) and
   ordLess2 (infix "<o" 50) and
   ordIso2 (infix "=o" 50) and
-  card_of ("|_|" ) and
+  card_of ("|_|") and
   csum (infixr "+c" 65) and
   cprod (infixr "*c" 80) and
   cexp (infixr "^c" 90)
diff -r 500ef036117b -r 252c7fec4119 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jan 20 21:45:08 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 22:24:48 2014 +0100
@@ -11,11 +11,6 @@
 
 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
 
-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_notation
   bot ("\<bottom>") and
   top ("\<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 \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)