1.1 --- a/src/HOL/BNF/BNF_Def.thy Mon Nov 25 12:27:03 2013 +0100
1.2 +++ b/src/HOL/BNF/BNF_Def.thy Mon Nov 25 13:48:00 2013 +0100
1.3 @@ -9,6 +9,8 @@
1.4
1.5 theory BNF_Def
1.6 imports BNF_Util
1.7 + (*FIXME: register fundef_cong attribute in an interpretation to remove this dependency*)
1.8 + FunDef
1.9 keywords
1.10 "print_bnfs" :: diag and
1.11 "bnf" :: thy_goal
1.12 @@ -196,6 +198,10 @@
1.13 lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
1.14 unfolding vimage2p_def convol_def by auto
1.15
1.16 +(*FIXME: duplicates lemma from Record.thy*)
1.17 +lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
1.18 + by clarsimp
1.19 +
1.20 ML_file "Tools/bnf_def_tactics.ML"
1.21 ML_file "Tools/bnf_def.ML"
1.22
2.1 --- a/src/HOL/BNF/BNF_GFP.thy Mon Nov 25 12:27:03 2013 +0100
2.2 +++ b/src/HOL/BNF/BNF_GFP.thy Mon Nov 25 13:48:00 2013 +0100
2.3 @@ -8,7 +8,7 @@
2.4 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
2.5
2.6 theory BNF_GFP
2.7 -imports BNF_FP_Base Equiv_Relations_More
2.8 +imports BNF_FP_Base Equiv_Relations_More List_Prefix
2.9 keywords
2.10 "codatatype" :: thy_decl and
2.11 "primcorecursive" :: thy_goal and
2.12 @@ -166,6 +166,8 @@
2.13
2.14 (*Extended Sublist*)
2.15
2.16 +definition clists where "clists r = |lists (Field r)|"
2.17 +
2.18 definition prefCl where
2.19 "prefCl Kl = (\<forall> kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
2.20 definition PrefCl where
3.1 --- a/src/HOL/BNF/BNF_Util.thy Mon Nov 25 12:27:03 2013 +0100
3.2 +++ b/src/HOL/BNF/BNF_Util.thy Mon Nov 25 13:48:00 2013 +0100
3.3 @@ -10,6 +10,8 @@
3.4
3.5 theory BNF_Util
3.6 imports "../Cardinals/Cardinal_Arithmetic_FP"
3.7 + (*FIXME: define fun_rel here, reuse in Transfer once this theory is in HOL*)
3.8 + Transfer
3.9 begin
3.10
3.11 definition collect where
4.1 --- a/src/HOL/BNF/Basic_BNFs.thy Mon Nov 25 12:27:03 2013 +0100
4.2 +++ b/src/HOL/BNF/Basic_BNFs.thy Mon Nov 25 13:48:00 2013 +0100
4.3 @@ -11,13 +11,12 @@
4.4
4.5 theory Basic_BNFs
4.6 imports BNF_Def
4.7 + (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
4.8 + Lifting_Sum
4.9 + Lifting_Product
4.10 + Main
4.11 begin
4.12
4.13 -lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
4.14 -
4.15 -lemma natLeq_cinfinite: "cinfinite natLeq"
4.16 -unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
4.17 -
4.18 lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2"
4.19 unfolding wpull_def Grp_def by auto
4.20
5.1 --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Nov 25 12:27:03 2013 +0100
5.2 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Nov 25 13:48:00 2013 +0100
5.3 @@ -183,22 +183,4 @@
5.4 lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r"
5.5 unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
5.6
5.7 -
5.8 -subsection {* Lists *}
5.9 -
5.10 -text {*
5.11 - The following collection of lemmas should be seen as an user interface to the HOL theory
5.12 - of cardinals. It is not expected to be complete in any sense, since its
5.13 - development was driven by demand arising from the development of the (co)datatype package.
5.14 -*}
5.15 -
5.16 -lemma clists_Cinfinite: "Cinfinite r \<Longrightarrow> clists r =o r"
5.17 -unfolding cinfinite_def clists_def by (blast intro: Card_order_lists_infinite)
5.18 -
5.19 -lemma Card_order_clists: "Card_order (clists r)"
5.20 -unfolding clists_def by (rule card_of_Card_order)
5.21 -
5.22 -lemma Cnotzero_clists: "Cnotzero (clists r)"
5.23 -by (simp add: clists_def card_of_ordIso_czero_iff_empty lists_not_empty)
5.24 -
5.25 end
6.1 --- a/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy Mon Nov 25 12:27:03 2013 +0100
6.2 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy Mon Nov 25 13:48:00 2013 +0100
6.3 @@ -136,6 +136,11 @@
6.4 unfolding cfinite_def cinfinite_def
6.5 by (metis card_order_on_well_order_on finite_ordLess_infinite)
6.6
6.7 +lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
6.8 +
6.9 +lemma natLeq_cinfinite: "cinfinite natLeq"
6.10 +unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
6.11 +
6.12 lemma natLeq_ordLeq_cinfinite:
6.13 assumes inf: "Cinfinite r"
6.14 shows "natLeq \<le>o r"
6.15 @@ -583,7 +588,8 @@
6.16 by (simp add: cinfinite_cexp Card_order_cexp)
6.17
6.18 lemma ctwo_ordLess_natLeq: "ctwo <o natLeq"
6.19 -unfolding ctwo_def using finite_iff_ordLess_natLeq finite_UNIV by fast
6.20 +unfolding ctwo_def using finite_UNIV natLeq_cinfinite natLeq_Card_order
6.21 +by (intro Cfinite_ordLess_Cinfinite) (auto simp: cfinite_def card_of_Card_order)
6.22
6.23 lemma ctwo_ordLess_Cinfinite: "Cinfinite r \<Longrightarrow> ctwo <o r"
6.24 by (metis ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite ordLess_ordLeq_trans)
6.25 @@ -740,8 +746,4 @@
6.26 lemma Cinfinite_cpow: "Cinfinite r \<Longrightarrow> Cinfinite (cpow r)"
6.27 unfolding cpow_def cinfinite_def by (metis Field_card_of card_of_Card_order infinite_Pow)
6.28
6.29 -subsection {* Lists *}
6.30 -
6.31 -definition clists where "clists r = |lists (Field r)|"
6.32 -
6.33 end
7.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Nov 25 12:27:03 2013 +0100
7.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Nov 25 13:48:00 2013 +0100
7.3 @@ -1024,6 +1024,27 @@
7.4 lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
7.5 using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
7.6
7.7 +lemma closed_nat_set_iff:
7.8 +assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
7.9 +shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
7.10 +proof-
7.11 + {assume "A \<noteq> UNIV" hence "\<exists>n. n \<notin> A" by blast
7.12 + moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast
7.13 + ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)"
7.14 + using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce
7.15 + have "A = {0 ..< n}"
7.16 + proof(auto simp add: 1)
7.17 + fix m assume *: "m \<in> A"
7.18 + {assume "n \<le> m" with assms * have "n \<in> A" by blast
7.19 + hence False using 1 by auto
7.20 + }
7.21 + thus "m < n" by fastforce
7.22 + qed
7.23 + hence "\<exists>n. A = {0 ..< n}" by blast
7.24 + }
7.25 + thus ?thesis by blast
7.26 +qed
7.27 +
7.28 lemma natLeq_ofilter_iff:
7.29 "ofilter natLeq A = (A = UNIV \<or> (\<exists>n. A = {0 ..< n}))"
7.30 proof(rule iffI)
7.31 @@ -1040,6 +1061,27 @@
7.32 lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
7.33 unfolding rel.under_def by auto
7.34
7.35 +lemma natLeq_on_ofilter_less_eq:
7.36 +"n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
7.37 +apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
7.38 +apply (simp add: Field_natLeq_on)
7.39 +by (auto simp add: rel.under_def)
7.40 +
7.41 +lemma natLeq_on_ofilter_iff:
7.42 +"wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
7.43 +proof(rule iffI)
7.44 + assume *: "wo_rel.ofilter (natLeq_on m) A"
7.45 + hence 1: "A \<le> {0..<m}"
7.46 + by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on)
7.47 + hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
7.48 + using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def)
7.49 + hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
7.50 + thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
7.51 +next
7.52 + assume "(\<exists>n\<le>m. A = {0 ..< n})"
7.53 + thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq)
7.54 +qed
7.55 +
7.56 corollary natLeq_on_ofilter:
7.57 "ofilter(natLeq_on n) {0 ..< n}"
7.58 by (auto simp add: natLeq_on_ofilter_less_eq)
7.59 @@ -1057,15 +1099,16 @@
7.60 lemma natLeq_on_injective:
7.61 "natLeq_on m = natLeq_on n \<Longrightarrow> m = n"
7.62 using Field_natLeq_on[of m] Field_natLeq_on[of n]
7.63 - atLeastLessThan_injective[of m n] by auto
7.64 + atLeastLessThan_injective[of m n, unfolded atLeastLessThan_def] by blast
7.65
7.66 lemma natLeq_on_injective_ordIso:
7.67 "(natLeq_on m =o natLeq_on n) = (m = n)"
7.68 proof(auto simp add: natLeq_on_Well_order ordIso_reflexive)
7.69 assume "natLeq_on m =o natLeq_on n"
7.70 - then obtain f where "bij_betw f {0..<m} {0..<n}"
7.71 + then obtain f where "bij_betw f {x. x<m} {x. x<n}"
7.72 using Field_natLeq_on assms unfolding ordIso_def iso_def[abs_def] by auto
7.73 - thus "m = n" using atLeastLessThan_injective2 by blast
7.74 + thus "m = n" using atLeastLessThan_injective2[of f m n]
7.75 + unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
7.76 qed
7.77
7.78
7.79 @@ -1079,6 +1122,61 @@
7.80 "natLeq =o |A| \<Longrightarrow> \<not>finite A"
7.81 using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
7.82
7.83 +
7.84 +lemma ordIso_natLeq_on_imp_finite:
7.85 +"|A| =o natLeq_on n \<Longrightarrow> finite A"
7.86 +unfolding ordIso_def iso_def[abs_def]
7.87 +by (auto simp: Field_natLeq_on bij_betw_finite)
7.88 +
7.89 +
7.90 +lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
7.91 +proof(unfold card_order_on_def,
7.92 + auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
7.93 + fix r assume "well_order_on {x. x < n} r"
7.94 + thus "natLeq_on n \<le>o r"
7.95 + using finite_atLeastLessThan natLeq_on_well_order_on
7.96 + finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
7.97 +qed
7.98 +
7.99 +
7.100 +corollary card_of_Field_natLeq_on:
7.101 +"|Field (natLeq_on n)| =o natLeq_on n"
7.102 +using Field_natLeq_on natLeq_on_Card_order
7.103 + Card_order_iff_ordIso_card_of[of "natLeq_on n"]
7.104 + ordIso_symmetric[of "natLeq_on n"] by blast
7.105 +
7.106 +
7.107 +corollary card_of_less:
7.108 +"|{0 ..< n}| =o natLeq_on n"
7.109 +using Field_natLeq_on card_of_Field_natLeq_on
7.110 +unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by auto
7.111 +
7.112 +
7.113 +lemma natLeq_on_ordLeq_less_eq:
7.114 +"((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
7.115 +proof
7.116 + assume "natLeq_on m \<le>o natLeq_on n"
7.117 + then obtain f where "inj_on f {x. x < m} \<and> f ` {x. x < m} \<le> {x. x < n}"
7.118 + unfolding ordLeq_def using
7.119 + embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
7.120 + embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
7.121 + thus "m \<le> n" using atLeastLessThan_less_eq2
7.122 + unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
7.123 +next
7.124 + assume "m \<le> n"
7.125 + hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto
7.126 + hence "|{0..<m}| \<le>o |{0..<n}|" using card_of_ordLeq by blast
7.127 + thus "natLeq_on m \<le>o natLeq_on n"
7.128 + using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
7.129 +qed
7.130 +
7.131 +
7.132 +lemma natLeq_on_ordLeq_less:
7.133 +"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
7.134 +using not_ordLeq_iff_ordLess[of "natLeq_on m" "natLeq_on n"]
7.135 + natLeq_on_Well_order natLeq_on_ordLeq_less_eq
7.136 +by fastforce
7.137 +
7.138 lemma ordLeq_natLeq_on_imp_finite:
7.139 assumes "|A| \<le>o natLeq_on n"
7.140 shows "finite A"
7.141 @@ -1091,6 +1189,26 @@
7.142
7.143 subsubsection {* "Backward compatibility" with the numeric cardinal operator for finite sets *}
7.144
7.145 +lemma finite_card_of_iff_card2:
7.146 +assumes FIN: "finite A" and FIN': "finite B"
7.147 +shows "( |A| \<le>o |B| ) = (card A \<le> card B)"
7.148 +using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast
7.149 +
7.150 +lemma finite_imp_card_of_natLeq_on:
7.151 +assumes "finite A"
7.152 +shows "|A| =o natLeq_on (card A)"
7.153 +proof-
7.154 + obtain h where "bij_betw h A {0 ..< card A}"
7.155 + using assms ex_bij_betw_finite_nat by blast
7.156 + thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast
7.157 +qed
7.158 +
7.159 +lemma finite_iff_card_of_natLeq_on:
7.160 +"finite A = (\<exists>n. |A| =o natLeq_on n)"
7.161 +using finite_imp_card_of_natLeq_on[of A]
7.162 +by(auto simp add: ordIso_natLeq_on_imp_finite)
7.163 +
7.164 +
7.165 lemma finite_card_of_iff_card:
7.166 assumes FIN: "finite A" and FIN': "finite B"
7.167 shows "( |A| =o |B| ) = (card A = card B)"
7.168 @@ -1145,6 +1263,54 @@
7.169 using cardSuc_mono_ordLeq[of r' r] assms by blast
7.170 qed
7.171
7.172 +lemma cardSuc_natLeq_on_Suc:
7.173 +"cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
7.174 +proof-
7.175 + obtain r r' p where r_def: "r = natLeq_on n" and
7.176 + r'_def: "r' = cardSuc(natLeq_on n)" and
7.177 + p_def: "p = natLeq_on(Suc n)" by blast
7.178 + (* Preliminary facts: *)
7.179 + have CARD: "Card_order r \<and> Card_order r' \<and> Card_order p" unfolding r_def r'_def p_def
7.180 + using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
7.181 + hence WELL: "Well_order r \<and> Well_order r' \<and> Well_order p"
7.182 + unfolding card_order_on_def by force
7.183 + have FIELD: "Field r = {0..<n} \<and> Field p = {0..<(Suc n)}"
7.184 + unfolding r_def p_def Field_natLeq_on atLeast_0 atLeastLessThan_def lessThan_def by simp
7.185 + hence FIN: "finite (Field r)" by force
7.186 + have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast
7.187 + hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
7.188 + hence LESS: "|Field r| <o |Field r'|"
7.189 + using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
7.190 + (* Main proof: *)
7.191 + have "r' \<le>o p" using CARD unfolding r_def r'_def p_def
7.192 + using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
7.193 + moreover have "p \<le>o r'"
7.194 + proof-
7.195 + {assume "r' <o p"
7.196 + then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
7.197 + let ?q = "Restr p (f ` Field r')"
7.198 + have 1: "embed r' p f" using 0 unfolding embedS_def by force
7.199 + hence 2: "f ` Field r' < {0..<(Suc n)}"
7.200 + using WELL FIELD 0 by (auto simp add: embedS_iff)
7.201 + have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
7.202 + then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}"
7.203 + unfolding p_def by (auto simp add: natLeq_on_ofilter_iff)
7.204 + hence 4: "m \<le> n" using 2 by force
7.205 + (* *)
7.206 + have "bij_betw f (Field r') (f ` (Field r'))"
7.207 + using 1 WELL embed_inj_on unfolding bij_betw_def by force
7.208 + moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
7.209 + ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
7.210 + using bij_betw_same_card bij_betw_finite by metis
7.211 + hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force
7.212 + hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
7.213 + hence False using LESS not_ordLess_ordLeq by auto
7.214 + }
7.215 + thus ?thesis using WELL CARD by fastforce
7.216 + qed
7.217 + ultimately show ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast
7.218 +qed
7.219 +
7.220 lemma card_of_Plus_ordLeq_infinite[simp]:
7.221 assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
7.222 shows "|A <+> B| \<le>o |C|"
8.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Mon Nov 25 12:27:03 2013 +0100
8.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Mon Nov 25 13:48:00 2013 +0100
8.3 @@ -1337,37 +1337,15 @@
8.4 using natLeq_Linear_order wf_less natLeq_natLess_Id by auto
8.5
8.6
8.7 -lemma closed_nat_set_iff:
8.8 -assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
8.9 -shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
8.10 -proof-
8.11 - {assume "A \<noteq> UNIV" hence "\<exists>n. n \<notin> A" by blast
8.12 - moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast
8.13 - ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)"
8.14 - using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce
8.15 - have "A = {0 ..< n}"
8.16 - proof(auto simp add: 1)
8.17 - fix m assume *: "m \<in> A"
8.18 - {assume "n \<le> m" with assms * have "n \<in> A" by blast
8.19 - hence False using 1 by auto
8.20 - }
8.21 - thus "m < n" by fastforce
8.22 - qed
8.23 - hence "\<exists>n. A = {0 ..< n}" by blast
8.24 - }
8.25 - thus ?thesis by blast
8.26 -qed
8.27 -
8.28 -
8.29 -lemma Field_natLeq_on: "Field (natLeq_on n) = {0 ..< n}"
8.30 +lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"
8.31 unfolding Field_def by auto
8.32
8.33
8.34 -lemma natLeq_underS_less: "rel.underS natLeq n = {0 ..< n}"
8.35 +lemma natLeq_underS_less: "rel.underS natLeq n = {x. x < n}"
8.36 unfolding rel.underS_def by auto
8.37
8.38
8.39 -lemma Restr_natLeq: "Restr natLeq {0 ..< n} = natLeq_on n"
8.40 +lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
8.41 by force
8.42
8.43
8.44 @@ -1378,10 +1356,10 @@
8.45
8.46 lemma natLeq_on_Well_order: "Well_order(natLeq_on n)"
8.47 using Restr_natLeq[of n] natLeq_Well_order
8.48 - Well_order_Restr[of natLeq "{0..<n}"] by auto
8.49 + Well_order_Restr[of natLeq "{x. x < n}"] by auto
8.50
8.51
8.52 -corollary natLeq_on_well_order_on: "well_order_on {0 ..< n} (natLeq_on n)"
8.53 +corollary natLeq_on_well_order_on: "well_order_on {x. x < n} (natLeq_on n)"
8.54 using natLeq_on_Well_order Field_natLeq_on by auto
8.55
8.56
8.57 @@ -1389,28 +1367,6 @@
8.58 unfolding wo_rel_def using natLeq_on_Well_order .
8.59
8.60
8.61 -lemma natLeq_on_ofilter_less_eq:
8.62 -"n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
8.63 -apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
8.64 -apply (simp add: Field_natLeq_on)
8.65 -by (auto simp add: rel.under_def)
8.66 -
8.67 -lemma natLeq_on_ofilter_iff:
8.68 -"wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
8.69 -proof(rule iffI)
8.70 - assume *: "wo_rel.ofilter (natLeq_on m) A"
8.71 - hence 1: "A \<le> {0..<m}"
8.72 - by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on)
8.73 - hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
8.74 - using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def)
8.75 - hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
8.76 - thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
8.77 -next
8.78 - assume "(\<exists>n\<le>m. A = {0 ..< n})"
8.79 - thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq)
8.80 -qed
8.81 -
8.82 -
8.83
8.84 subsubsection {* Then as cardinals *}
8.85
8.86 @@ -1418,8 +1374,7 @@
8.87 lemma natLeq_Card_order: "Card_order natLeq"
8.88 proof(auto simp add: natLeq_Well_order
8.89 Card_order_iff_Restr_underS Restr_natLeq2, simp add: Field_natLeq)
8.90 - fix n have "finite(Field (natLeq_on n))"
8.91 - unfolding Field_natLeq_on by auto
8.92 + fix n have "finite(Field (natLeq_on n))" by (auto simp: Field_def)
8.93 moreover have "\<not>finite(UNIV::nat set)" by auto
8.94 ultimately show "natLeq_on n <o |UNIV::nat set|"
8.95 using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
8.96 @@ -1444,91 +1399,10 @@
8.97 using infinite_iff_card_of_nat[of A] card_of_nat
8.98 ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
8.99
8.100 -
8.101 corollary finite_iff_ordLess_natLeq:
8.102 "finite A = ( |A| <o natLeq)"
8.103 using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
8.104 - card_of_Well_order natLeq_Well_order
8.105 -by auto
8.106 -
8.107 -lemma ordIso_natLeq_on_imp_finite:
8.108 -"|A| =o natLeq_on n \<Longrightarrow> finite A"
8.109 -unfolding ordIso_def iso_def[abs_def]
8.110 -by (auto simp: Field_natLeq_on bij_betw_finite Field_card_of)
8.111 -
8.112 -
8.113 -lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
8.114 -proof(unfold card_order_on_def,
8.115 - auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
8.116 - fix r assume "well_order_on {0..<n} r"
8.117 - thus "natLeq_on n \<le>o r"
8.118 - using finite_atLeastLessThan natLeq_on_well_order_on
8.119 - finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
8.120 -qed
8.121 -
8.122 -
8.123 -corollary card_of_Field_natLeq_on:
8.124 -"|Field (natLeq_on n)| =o natLeq_on n"
8.125 -using Field_natLeq_on natLeq_on_Card_order
8.126 - Card_order_iff_ordIso_card_of[of "natLeq_on n"]
8.127 - ordIso_symmetric[of "natLeq_on n"] by blast
8.128 -
8.129 -
8.130 -corollary card_of_less:
8.131 -"|{0 ..< n}| =o natLeq_on n"
8.132 -using Field_natLeq_on card_of_Field_natLeq_on by auto
8.133 -
8.134 -
8.135 -lemma natLeq_on_ordLeq_less_eq:
8.136 -"((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
8.137 -proof
8.138 - assume "natLeq_on m \<le>o natLeq_on n"
8.139 - then obtain f where "inj_on f {0..<m} \<and> f ` {0..<m} \<le> {0..<n}"
8.140 - unfolding ordLeq_def using
8.141 - embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
8.142 - embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
8.143 - thus "m \<le> n" using atLeastLessThan_less_eq2 by blast
8.144 -next
8.145 - assume "m \<le> n"
8.146 - hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto
8.147 - hence "|{0..<m}| \<le>o |{0..<n}|" using card_of_ordLeq by blast
8.148 - thus "natLeq_on m \<le>o natLeq_on n"
8.149 - using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
8.150 -qed
8.151 -
8.152 -
8.153 -lemma natLeq_on_ordLeq_less:
8.154 -"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
8.155 -using not_ordLeq_iff_ordLess[of "natLeq_on m" "natLeq_on n"]
8.156 - natLeq_on_Well_order natLeq_on_ordLeq_less_eq
8.157 -by fastforce
8.158 -
8.159 -
8.160 -
8.161 -subsubsection {* "Backward compatibility" with the numeric cardinal operator for finite sets *}
8.162 -
8.163 -
8.164 -lemma finite_card_of_iff_card2:
8.165 -assumes FIN: "finite A" and FIN': "finite B"
8.166 -shows "( |A| \<le>o |B| ) = (card A \<le> card B)"
8.167 -using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast
8.168 -
8.169 -
8.170 -lemma finite_imp_card_of_natLeq_on:
8.171 -assumes "finite A"
8.172 -shows "|A| =o natLeq_on (card A)"
8.173 -proof-
8.174 - obtain h where "bij_betw h A {0 ..< card A}"
8.175 - using assms ex_bij_betw_finite_nat by blast
8.176 - thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast
8.177 -qed
8.178 -
8.179 -
8.180 -lemma finite_iff_card_of_natLeq_on:
8.181 -"finite A = (\<exists>n. |A| =o natLeq_on n)"
8.182 -using finite_imp_card_of_natLeq_on[of A]
8.183 -by(auto simp add: ordIso_natLeq_on_imp_finite)
8.184 -
8.185 + card_of_Well_order natLeq_Well_order by metis
8.186
8.187
8.188 subsection {* The successor of a cardinal *}
8.189 @@ -1667,55 +1541,6 @@
8.190 qed
8.191
8.192
8.193 -lemma cardSuc_natLeq_on_Suc:
8.194 -"cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
8.195 -proof-
8.196 - obtain r r' p where r_def: "r = natLeq_on n" and
8.197 - r'_def: "r' = cardSuc(natLeq_on n)" and
8.198 - p_def: "p = natLeq_on(Suc n)" by blast
8.199 - (* Preliminary facts: *)
8.200 - have CARD: "Card_order r \<and> Card_order r' \<and> Card_order p" unfolding r_def r'_def p_def
8.201 - using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
8.202 - hence WELL: "Well_order r \<and> Well_order r' \<and> Well_order p"
8.203 - unfolding card_order_on_def by force
8.204 - have FIELD: "Field r = {0..<n} \<and> Field p = {0..<(Suc n)}"
8.205 - unfolding r_def p_def Field_natLeq_on by simp
8.206 - hence FIN: "finite (Field r)" by force
8.207 - have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast
8.208 - hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
8.209 - hence LESS: "|Field r| <o |Field r'|"
8.210 - using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
8.211 - (* Main proof: *)
8.212 - have "r' \<le>o p" using CARD unfolding r_def r'_def p_def
8.213 - using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
8.214 - moreover have "p \<le>o r'"
8.215 - proof-
8.216 - {assume "r' <o p"
8.217 - then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
8.218 - let ?q = "Restr p (f ` Field r')"
8.219 - have 1: "embed r' p f" using 0 unfolding embedS_def by force
8.220 - hence 2: "f ` Field r' < {0..<(Suc n)}"
8.221 - using WELL FIELD 0 by (auto simp add: embedS_iff)
8.222 - have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
8.223 - then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}"
8.224 - unfolding p_def by (auto simp add: natLeq_on_ofilter_iff)
8.225 - hence 4: "m \<le> n" using 2 by force
8.226 - (* *)
8.227 - have "bij_betw f (Field r') (f ` (Field r'))"
8.228 - using 1 WELL embed_inj_on unfolding bij_betw_def by force
8.229 - moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
8.230 - ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
8.231 - using bij_betw_same_card bij_betw_finite by metis
8.232 - hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force
8.233 - hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
8.234 - hence False using LESS not_ordLess_ordLeq by auto
8.235 - }
8.236 - thus ?thesis using WELL CARD by (fastforce simp: not_ordLess_iff_ordLeq)
8.237 - qed
8.238 - ultimately show ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast
8.239 -qed
8.240 -
8.241 -
8.242 lemma card_of_cardSuc_finite:
8.243 "finite(Field(cardSuc |A| )) = finite A"
8.244 proof
8.245 @@ -1728,18 +1553,12 @@
8.246 thus "finite A" using * card_of_ordLeq_finite by blast
8.247 next
8.248 assume "finite A"
8.249 - then obtain n where "|A| =o natLeq_on n" using finite_iff_card_of_natLeq_on by blast
8.250 - hence "cardSuc |A| =o cardSuc(natLeq_on n)"
8.251 - using card_of_Card_order cardSuc_invar_ordIso natLeq_on_Card_order by blast
8.252 - hence "cardSuc |A| =o natLeq_on(Suc n)"
8.253 - using cardSuc_natLeq_on_Suc ordIso_transitive by blast
8.254 - hence "cardSuc |A| =o |{0..<(Suc n)}|" using card_of_less ordIso_equivalence by blast
8.255 - moreover have "|Field (cardSuc |A| ) | =o cardSuc |A|"
8.256 - using card_of_Field_ordIso cardSuc_Card_order card_of_Card_order by blast
8.257 - ultimately have "|Field (cardSuc |A| ) | =o |{0..<(Suc n)}|"
8.258 - using ordIso_equivalence by blast
8.259 - thus "finite (Field (cardSuc |A| ))"
8.260 - using card_of_ordIso_finite finite_atLeastLessThan by blast
8.261 + then have "finite ( Field |Pow A| )" unfolding Field_card_of by simp
8.262 + then show "finite (Field (cardSuc |A| ))"
8.263 + proof (rule card_of_ordLeq_finite[OF card_of_mono2, rotated])
8.264 + show "cardSuc |A| \<le>o |Pow A|"
8.265 + by (metis cardSuc_ordLess_ordLeq card_of_Card_order card_of_Pow)
8.266 + qed
8.267 qed
8.268
8.269
9.1 --- a/src/HOL/Cardinals/Fun_More.thy Mon Nov 25 12:27:03 2013 +0100
9.2 +++ b/src/HOL/Cardinals/Fun_More.thy Mon Nov 25 13:48:00 2013 +0100
9.3 @@ -8,7 +8,7 @@
9.4 header {* More on Injections, Bijections and Inverses *}
9.5
9.6 theory Fun_More
9.7 -imports Fun_More_FP
9.8 +imports Fun_More_FP Main
9.9 begin
9.10
9.11
9.12 @@ -170,6 +170,20 @@
9.13 card_atLeastLessThan[of m] card_atLeastLessThan[of n]
9.14 bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto
9.15
9.16 +
9.17 +(*2*)lemma atLeastLessThan_less_eq:
9.18 +"({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)"
9.19 +unfolding ivl_subset by arith
9.20 +
9.21 +
9.22 +(*2*)lemma atLeastLessThan_less_eq2:
9.23 +assumes "inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}"
9.24 +shows "m \<le> n"
9.25 +using assms
9.26 +using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
9.27 + card_atLeastLessThan[of m] card_atLeastLessThan[of n]
9.28 + card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce
9.29 +
9.30 (* unused *)
9.31 (*2*)lemma atLeastLessThan_less_eq3:
9.32 "(\<exists>f. inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}) = (m \<le> n)"
10.1 --- a/src/HOL/Cardinals/Fun_More_FP.thy Mon Nov 25 12:27:03 2013 +0100
10.2 +++ b/src/HOL/Cardinals/Fun_More_FP.thy Mon Nov 25 13:48:00 2013 +0100
10.3 @@ -8,7 +8,7 @@
10.4 header {* More on Injections, Bijections and Inverses (FP) *}
10.5
10.6 theory Fun_More_FP
10.7 -imports Main
10.8 +imports Hilbert_Choice
10.9 begin
10.10
10.11
10.12 @@ -219,22 +219,5 @@
10.13 by (auto intro: inj_on_inv_into)
10.14
10.15
10.16 -subsection {* Other facts *}
10.17 -
10.18 -
10.19 -(*2*)lemma atLeastLessThan_less_eq:
10.20 -"({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)"
10.21 -unfolding ivl_subset by arith
10.22 -
10.23 -
10.24 -(*2*)lemma atLeastLessThan_less_eq2:
10.25 -assumes "inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}"
10.26 -shows "m \<le> n"
10.27 -using assms
10.28 -using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
10.29 - card_atLeastLessThan[of m] card_atLeastLessThan[of n]
10.30 - card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce
10.31 -
10.32 -
10.33
10.34 end