author blanchet Mon Jan 20 22:24:48 2014 +0100 (2014-01-20) changeset 55087 252c7fec4119 parent 55086 500ef036117b child 55088 57c82e01022b
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
```     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)
```