renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
authorblanchet
Mon Jan 20 22:24:48 2014 +0100 (2014-01-20)
changeset 55087252c7fec4119
parent 55086 500ef036117b
child 55088 57c82e01022b
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy
src/HOL/Cardinals/Cardinal_Order_Relation.thy
src/HOL/Library/Cardinal_Notations.thy
src/HOL/Main.thy
     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  
     2.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 21:45:08 2014 +0100
     2.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 22:24:48 2014 +0100
     2.3 @@ -681,8 +681,6 @@
     2.4  
     2.5  subsection{* Regular Trees *}
     2.6  
     2.7 -hide_const regular
     2.8 -
     2.9  definition "reg f tr \<equiv> \<forall> tr'. subtr UNIV tr' tr \<longrightarrow> tr' = f (root tr')"
    2.10  definition "regular tr \<equiv> \<exists> f. reg f tr"
    2.11  
     3.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Jan 20 21:45:08 2014 +0100
     3.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Jan 20 22:24:48 2014 +0100
     3.3 @@ -1623,8 +1623,8 @@
     3.4  lemma refl_init_seg_of[intro, simp]: "refl init_seg_of"
     3.5  unfolding refl_on_def Field_def by auto
     3.6  
     3.7 -lemma regular_all_ex:
     3.8 -assumes r: "Card_order r"   "regular r"
     3.9 +lemma regularCard_all_ex:
    3.10 +assumes r: "Card_order r"   "regularCard r"
    3.11  and As: "\<And> i j b. b \<in> B \<Longrightarrow> (i,j) \<in> r \<Longrightarrow> P i b \<Longrightarrow> P j b"
    3.12  and Bsub: "\<forall> b \<in> B. \<exists> i \<in> Field r. P i b"
    3.13  and cardB: "|B| <o r"
    3.14 @@ -1632,7 +1632,7 @@
    3.15  proof-
    3.16    let ?As = "\<lambda>i. {b \<in> B. P i b}"
    3.17    have "EX i : Field r. B \<le> ?As i"
    3.18 -  apply(rule regular_UNION) using assms unfolding relChain_def by auto
    3.19 +  apply(rule regularCard_UNION) using assms unfolding relChain_def by auto
    3.20    thus ?thesis by auto
    3.21  qed
    3.22  
    3.23 @@ -1692,8 +1692,8 @@
    3.24                 |A| <o r \<and> (\<forall>a \<in> A. |F a| <o r)
    3.25                 \<longrightarrow> |SIGMA a : A. F a| <o r"
    3.26  
    3.27 -lemma regular_stable:
    3.28 -assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regular r"
    3.29 +lemma regularCard_stable:
    3.30 +assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regularCard r"
    3.31  shows "stable r"
    3.32  unfolding stable_def proof safe
    3.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"
    3.34 @@ -1710,7 +1710,7 @@
    3.35      apply(rule exI[of _ snd]) unfolding bij_betw_def inj_on_def by (auto simp: image_def)
    3.36      hence "|L| <o r" using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
    3.37      hence "|f ` L| <o r" using ordLeq_ordLess_trans[OF card_of_image, of "L"] unfolding L_def by auto
    3.38 -    hence "\<not> cofinal (f ` L) r" using reg fL unfolding regular_def by (metis not_ordLess_ordIso)
    3.39 +    hence "\<not> cofinal (f ` L) r" using reg fL unfolding regularCard_def by (metis not_ordLess_ordIso)
    3.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)"
    3.41      unfolding cofinal_def image_def by auto
    3.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)
    3.43 @@ -1734,7 +1734,7 @@
    3.44       partial_order_on_def antisym_def by auto
    3.45       ultimately show "\<exists>j\<in>g ` A. i \<noteq> j \<and> (i, j) \<in> r" using a by auto
    3.46     qed
    3.47 -   ultimately have "|g ` A| =o r" using reg unfolding regular_def by auto
    3.48 +   ultimately have "|g ` A| =o r" using reg unfolding regularCard_def by auto
    3.49     moreover have "|g ` A| \<le>o |A|" by (metis card_of_image)
    3.50     ultimately have False using A by (metis not_ordLess_ordIso ordLeq_ordLess_trans)
    3.51    }
    3.52 @@ -1742,10 +1742,10 @@
    3.53    using cr not_ordLess_iff_ordLeq by (metis card_of_Well_order card_order_on_well_order_on)
    3.54  qed
    3.55  
    3.56 -lemma stable_regular:
    3.57 +lemma stable_regularCard:
    3.58  assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and st: "stable r"
    3.59 -shows "regular r"
    3.60 -unfolding regular_def proof safe
    3.61 +shows "regularCard r"
    3.62 +unfolding regularCard_def proof safe
    3.63    fix K assume K: "K \<subseteq> Field r" and cof: "cofinal K r"
    3.64    have "|K| \<le>o r" using K by (metis card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans)
    3.65    moreover
    3.66 @@ -1807,13 +1807,13 @@
    3.67    by (auto simp add: finite_iff_ordLess_natLeq)
    3.68  qed
    3.69  
    3.70 -corollary regular_natLeq: "regular natLeq"
    3.71 -using stable_regular[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
    3.72 +corollary regularCard_natLeq: "regularCard natLeq"
    3.73 +using stable_regularCard[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
    3.74  
    3.75  lemma stable_cardSuc:
    3.76  assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
    3.77  shows "stable(cardSuc r)"
    3.78 -using infinite_cardSuc_regular regular_stable
    3.79 +using infinite_cardSuc_regularCard regularCard_stable
    3.80  by (metis CARD INF cardSuc_Card_order cardSuc_finite)
    3.81  
    3.82  lemma stable_UNION:
    3.83 @@ -1900,10 +1900,10 @@
    3.84    thus ?thesis using CARD card_of_UNIV2 ordLeq_ordLess_trans by blast
    3.85  qed
    3.86  
    3.87 -corollary infinite_regular_exists:
    3.88 +corollary infinite_regularCard_exists:
    3.89  assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
    3.90  shows "\<exists>(A :: (nat + 'a set)set).
    3.91 -          \<not>finite A \<and> regular |A| \<and> (\<forall>r \<in> R. r <o |A| )"
    3.92 -using infinite_stable_exists[OF CARD] stable_regular by (metis Field_card_of card_of_card_order_on)
    3.93 +          \<not>finite A \<and> regularCard |A| \<and> (\<forall>r \<in> R. r <o |A| )"
    3.94 +using infinite_stable_exists[OF CARD] stable_regularCard by (metis Field_card_of card_of_card_order_on)
    3.95  
    3.96  end
     4.1 --- a/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 21:45:08 2014 +0100
     4.2 +++ b/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 22:24:48 2014 +0100
     4.3 @@ -16,7 +16,7 @@
     4.4    ordLeq3 (infix "\<le>o" 50) and
     4.5    ordLess2 (infix "<o" 50) and
     4.6    ordIso2 (infix "=o" 50) and
     4.7 -  card_of ("|_|" ) and
     4.8 +  card_of ("|_|") and
     4.9    csum (infixr "+c" 65) and
    4.10    cprod (infixr "*c" 80) and
    4.11    cexp (infixr "^c" 90)
     5.1 --- a/src/HOL/Main.thy	Mon Jan 20 21:45:08 2014 +0100
     5.2 +++ b/src/HOL/Main.thy	Mon Jan 20 22:24:48 2014 +0100
     5.3 @@ -11,11 +11,6 @@
     5.4  
     5.5  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
     5.6  
     5.7 -hide_const (open)
     5.8 -  image2 image2p vimage2p Gr Grp collect fsts snds setl setr
     5.9 -  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
    5.10 -  prefCl PrefCl Succ Shift shift proj
    5.11 -
    5.12  no_notation
    5.13    bot ("\<bottom>") and
    5.14    top ("\<top>") and
    5.15 @@ -33,6 +28,11 @@
    5.16    cexp (infixr "^c" 90) and
    5.17    convol ("<_ , _>")
    5.18  
    5.19 +hide_const (open)
    5.20 +  image2 image2p vimage2p Gr Grp collect fsts snds setl setr
    5.21 +  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
    5.22 +  prefCl PrefCl Succ Shift shift proj
    5.23 +
    5.24  no_syntax (xsymbols)
    5.25    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    5.26    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)