--- a/src/HOL/BNF/BNF_Def.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/BNF/BNF_Def.thy Mon Nov 25 13:48:00 2013 +0100
@@ -9,6 +9,8 @@
theory BNF_Def
imports BNF_Util
+ (*FIXME: register fundef_cong attribute in an interpretation to remove this dependency*)
+ FunDef
keywords
"print_bnfs" :: diag and
"bnf" :: thy_goal
@@ -196,6 +198,10 @@
lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
unfolding vimage2p_def convol_def by auto
+(*FIXME: duplicates lemma from Record.thy*)
+lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
+ by clarsimp
+
ML_file "Tools/bnf_def_tactics.ML"
ML_file "Tools/bnf_def.ML"
--- a/src/HOL/BNF/BNF_GFP.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/BNF/BNF_GFP.thy Mon Nov 25 13:48:00 2013 +0100
@@ -8,7 +8,7 @@
header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
theory BNF_GFP
-imports BNF_FP_Base Equiv_Relations_More
+imports BNF_FP_Base Equiv_Relations_More List_Prefix
keywords
"codatatype" :: thy_decl and
"primcorecursive" :: thy_goal and
@@ -166,6 +166,8 @@
(*Extended Sublist*)
+definition clists where "clists r = |lists (Field r)|"
+
definition prefCl where
"prefCl Kl = (\<forall> kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
definition PrefCl where
--- a/src/HOL/BNF/BNF_Util.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/BNF/BNF_Util.thy Mon Nov 25 13:48:00 2013 +0100
@@ -10,6 +10,8 @@
theory BNF_Util
imports "../Cardinals/Cardinal_Arithmetic_FP"
+ (*FIXME: define fun_rel here, reuse in Transfer once this theory is in HOL*)
+ Transfer
begin
definition collect where
--- a/src/HOL/BNF/Basic_BNFs.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/BNF/Basic_BNFs.thy Mon Nov 25 13:48:00 2013 +0100
@@ -11,13 +11,12 @@
theory Basic_BNFs
imports BNF_Def
+ (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
+ Lifting_Sum
+ Lifting_Product
+ Main
begin
-lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
-
-lemma natLeq_cinfinite: "cinfinite natLeq"
-unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
-
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"
unfolding wpull_def Grp_def by auto
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Nov 25 13:48:00 2013 +0100
@@ -183,22 +183,4 @@
lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r"
unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
-
-subsection {* Lists *}
-
-text {*
- The following collection of lemmas should be seen as an user interface to the HOL theory
- of cardinals. It is not expected to be complete in any sense, since its
- development was driven by demand arising from the development of the (co)datatype package.
-*}
-
-lemma clists_Cinfinite: "Cinfinite r \<Longrightarrow> clists r =o r"
-unfolding cinfinite_def clists_def by (blast intro: Card_order_lists_infinite)
-
-lemma Card_order_clists: "Card_order (clists r)"
-unfolding clists_def by (rule card_of_Card_order)
-
-lemma Cnotzero_clists: "Cnotzero (clists r)"
-by (simp add: clists_def card_of_ordIso_czero_iff_empty lists_not_empty)
-
end
--- a/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy Mon Nov 25 13:48:00 2013 +0100
@@ -136,6 +136,11 @@
unfolding cfinite_def cinfinite_def
by (metis card_order_on_well_order_on finite_ordLess_infinite)
+lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
+
+lemma natLeq_cinfinite: "cinfinite natLeq"
+unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
+
lemma natLeq_ordLeq_cinfinite:
assumes inf: "Cinfinite r"
shows "natLeq \<le>o r"
@@ -583,7 +588,8 @@
by (simp add: cinfinite_cexp Card_order_cexp)
lemma ctwo_ordLess_natLeq: "ctwo <o natLeq"
-unfolding ctwo_def using finite_iff_ordLess_natLeq finite_UNIV by fast
+unfolding ctwo_def using finite_UNIV natLeq_cinfinite natLeq_Card_order
+by (intro Cfinite_ordLess_Cinfinite) (auto simp: cfinite_def card_of_Card_order)
lemma ctwo_ordLess_Cinfinite: "Cinfinite r \<Longrightarrow> ctwo <o r"
by (metis ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite ordLess_ordLeq_trans)
@@ -740,8 +746,4 @@
lemma Cinfinite_cpow: "Cinfinite r \<Longrightarrow> Cinfinite (cpow r)"
unfolding cpow_def cinfinite_def by (metis Field_card_of card_of_Card_order infinite_Pow)
-subsection {* Lists *}
-
-definition clists where "clists r = |lists (Field r)|"
-
end
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Nov 25 13:48:00 2013 +0100
@@ -1024,6 +1024,27 @@
lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
+lemma closed_nat_set_iff:
+assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
+shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
+proof-
+ {assume "A \<noteq> UNIV" hence "\<exists>n. n \<notin> A" by blast
+ moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast
+ ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)"
+ using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce
+ have "A = {0 ..< n}"
+ proof(auto simp add: 1)
+ fix m assume *: "m \<in> A"
+ {assume "n \<le> m" with assms * have "n \<in> A" by blast
+ hence False using 1 by auto
+ }
+ thus "m < n" by fastforce
+ qed
+ hence "\<exists>n. A = {0 ..< n}" by blast
+ }
+ thus ?thesis by blast
+qed
+
lemma natLeq_ofilter_iff:
"ofilter natLeq A = (A = UNIV \<or> (\<exists>n. A = {0 ..< n}))"
proof(rule iffI)
@@ -1040,6 +1061,27 @@
lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
unfolding rel.under_def by auto
+lemma natLeq_on_ofilter_less_eq:
+"n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
+apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
+apply (simp add: Field_natLeq_on)
+by (auto simp add: rel.under_def)
+
+lemma natLeq_on_ofilter_iff:
+"wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
+proof(rule iffI)
+ assume *: "wo_rel.ofilter (natLeq_on m) A"
+ hence 1: "A \<le> {0..<m}"
+ by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on)
+ hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
+ using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def)
+ hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
+ thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
+next
+ assume "(\<exists>n\<le>m. A = {0 ..< n})"
+ thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq)
+qed
+
corollary natLeq_on_ofilter:
"ofilter(natLeq_on n) {0 ..< n}"
by (auto simp add: natLeq_on_ofilter_less_eq)
@@ -1057,15 +1099,16 @@
lemma natLeq_on_injective:
"natLeq_on m = natLeq_on n \<Longrightarrow> m = n"
using Field_natLeq_on[of m] Field_natLeq_on[of n]
- atLeastLessThan_injective[of m n] by auto
+ atLeastLessThan_injective[of m n, unfolded atLeastLessThan_def] by blast
lemma natLeq_on_injective_ordIso:
"(natLeq_on m =o natLeq_on n) = (m = n)"
proof(auto simp add: natLeq_on_Well_order ordIso_reflexive)
assume "natLeq_on m =o natLeq_on n"
- then obtain f where "bij_betw f {0..<m} {0..<n}"
+ then obtain f where "bij_betw f {x. x<m} {x. x<n}"
using Field_natLeq_on assms unfolding ordIso_def iso_def[abs_def] by auto
- thus "m = n" using atLeastLessThan_injective2 by blast
+ thus "m = n" using atLeastLessThan_injective2[of f m n]
+ unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
qed
@@ -1079,6 +1122,61 @@
"natLeq =o |A| \<Longrightarrow> \<not>finite A"
using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
+
+lemma ordIso_natLeq_on_imp_finite:
+"|A| =o natLeq_on n \<Longrightarrow> finite A"
+unfolding ordIso_def iso_def[abs_def]
+by (auto simp: Field_natLeq_on bij_betw_finite)
+
+
+lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
+proof(unfold card_order_on_def,
+ auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
+ fix r assume "well_order_on {x. x < n} r"
+ thus "natLeq_on n \<le>o r"
+ using finite_atLeastLessThan natLeq_on_well_order_on
+ finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
+qed
+
+
+corollary card_of_Field_natLeq_on:
+"|Field (natLeq_on n)| =o natLeq_on n"
+using Field_natLeq_on natLeq_on_Card_order
+ Card_order_iff_ordIso_card_of[of "natLeq_on n"]
+ ordIso_symmetric[of "natLeq_on n"] by blast
+
+
+corollary card_of_less:
+"|{0 ..< n}| =o natLeq_on n"
+using Field_natLeq_on card_of_Field_natLeq_on
+unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by auto
+
+
+lemma natLeq_on_ordLeq_less_eq:
+"((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
+proof
+ assume "natLeq_on m \<le>o natLeq_on n"
+ then obtain f where "inj_on f {x. x < m} \<and> f ` {x. x < m} \<le> {x. x < n}"
+ unfolding ordLeq_def using
+ embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
+ embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
+ thus "m \<le> n" using atLeastLessThan_less_eq2
+ unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
+next
+ assume "m \<le> n"
+ hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto
+ hence "|{0..<m}| \<le>o |{0..<n}|" using card_of_ordLeq by blast
+ thus "natLeq_on m \<le>o natLeq_on n"
+ using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
+qed
+
+
+lemma natLeq_on_ordLeq_less:
+"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
+using not_ordLeq_iff_ordLess[of "natLeq_on m" "natLeq_on n"]
+ natLeq_on_Well_order natLeq_on_ordLeq_less_eq
+by fastforce
+
lemma ordLeq_natLeq_on_imp_finite:
assumes "|A| \<le>o natLeq_on n"
shows "finite A"
@@ -1091,6 +1189,26 @@
subsubsection {* "Backward compatibility" with the numeric cardinal operator for finite sets *}
+lemma finite_card_of_iff_card2:
+assumes FIN: "finite A" and FIN': "finite B"
+shows "( |A| \<le>o |B| ) = (card A \<le> card B)"
+using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast
+
+lemma finite_imp_card_of_natLeq_on:
+assumes "finite A"
+shows "|A| =o natLeq_on (card A)"
+proof-
+ obtain h where "bij_betw h A {0 ..< card A}"
+ using assms ex_bij_betw_finite_nat by blast
+ thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast
+qed
+
+lemma finite_iff_card_of_natLeq_on:
+"finite A = (\<exists>n. |A| =o natLeq_on n)"
+using finite_imp_card_of_natLeq_on[of A]
+by(auto simp add: ordIso_natLeq_on_imp_finite)
+
+
lemma finite_card_of_iff_card:
assumes FIN: "finite A" and FIN': "finite B"
shows "( |A| =o |B| ) = (card A = card B)"
@@ -1145,6 +1263,54 @@
using cardSuc_mono_ordLeq[of r' r] assms by blast
qed
+lemma cardSuc_natLeq_on_Suc:
+"cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
+proof-
+ obtain r r' p where r_def: "r = natLeq_on n" and
+ r'_def: "r' = cardSuc(natLeq_on n)" and
+ p_def: "p = natLeq_on(Suc n)" by blast
+ (* Preliminary facts: *)
+ have CARD: "Card_order r \<and> Card_order r' \<and> Card_order p" unfolding r_def r'_def p_def
+ using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
+ hence WELL: "Well_order r \<and> Well_order r' \<and> Well_order p"
+ unfolding card_order_on_def by force
+ have FIELD: "Field r = {0..<n} \<and> Field p = {0..<(Suc n)}"
+ unfolding r_def p_def Field_natLeq_on atLeast_0 atLeastLessThan_def lessThan_def by simp
+ hence FIN: "finite (Field r)" by force
+ have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast
+ hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
+ hence LESS: "|Field r| <o |Field r'|"
+ using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
+ (* Main proof: *)
+ have "r' \<le>o p" using CARD unfolding r_def r'_def p_def
+ using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
+ moreover have "p \<le>o r'"
+ proof-
+ {assume "r' <o p"
+ then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
+ let ?q = "Restr p (f ` Field r')"
+ have 1: "embed r' p f" using 0 unfolding embedS_def by force
+ hence 2: "f ` Field r' < {0..<(Suc n)}"
+ using WELL FIELD 0 by (auto simp add: embedS_iff)
+ have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
+ then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}"
+ unfolding p_def by (auto simp add: natLeq_on_ofilter_iff)
+ hence 4: "m \<le> n" using 2 by force
+ (* *)
+ have "bij_betw f (Field r') (f ` (Field r'))"
+ using 1 WELL embed_inj_on unfolding bij_betw_def by force
+ moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
+ ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
+ using bij_betw_same_card bij_betw_finite by metis
+ hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force
+ hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
+ hence False using LESS not_ordLess_ordLeq by auto
+ }
+ thus ?thesis using WELL CARD by fastforce
+ qed
+ ultimately show ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast
+qed
+
lemma card_of_Plus_ordLeq_infinite[simp]:
assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
shows "|A <+> B| \<le>o |C|"
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Mon Nov 25 13:48:00 2013 +0100
@@ -1337,37 +1337,15 @@
using natLeq_Linear_order wf_less natLeq_natLess_Id by auto
-lemma closed_nat_set_iff:
-assumes "\<forall>(m::nat) n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
-shows "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
-proof-
- {assume "A \<noteq> UNIV" hence "\<exists>n. n \<notin> A" by blast
- moreover obtain n where n_def: "n = (LEAST n. n \<notin> A)" by blast
- ultimately have 1: "n \<notin> A \<and> (\<forall>m. m < n \<longrightarrow> m \<in> A)"
- using LeastI_ex[of "\<lambda> n. n \<notin> A"] n_def Least_le[of "\<lambda> n. n \<notin> A"] by fastforce
- have "A = {0 ..< n}"
- proof(auto simp add: 1)
- fix m assume *: "m \<in> A"
- {assume "n \<le> m" with assms * have "n \<in> A" by blast
- hence False using 1 by auto
- }
- thus "m < n" by fastforce
- qed
- hence "\<exists>n. A = {0 ..< n}" by blast
- }
- thus ?thesis by blast
-qed
-
-
-lemma Field_natLeq_on: "Field (natLeq_on n) = {0 ..< n}"
+lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"
unfolding Field_def by auto
-lemma natLeq_underS_less: "rel.underS natLeq n = {0 ..< n}"
+lemma natLeq_underS_less: "rel.underS natLeq n = {x. x < n}"
unfolding rel.underS_def by auto
-lemma Restr_natLeq: "Restr natLeq {0 ..< n} = natLeq_on n"
+lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
by force
@@ -1378,10 +1356,10 @@
lemma natLeq_on_Well_order: "Well_order(natLeq_on n)"
using Restr_natLeq[of n] natLeq_Well_order
- Well_order_Restr[of natLeq "{0..<n}"] by auto
+ Well_order_Restr[of natLeq "{x. x < n}"] by auto
-corollary natLeq_on_well_order_on: "well_order_on {0 ..< n} (natLeq_on n)"
+corollary natLeq_on_well_order_on: "well_order_on {x. x < n} (natLeq_on n)"
using natLeq_on_Well_order Field_natLeq_on by auto
@@ -1389,28 +1367,6 @@
unfolding wo_rel_def using natLeq_on_Well_order .
-lemma natLeq_on_ofilter_less_eq:
-"n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
-apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
-apply (simp add: Field_natLeq_on)
-by (auto simp add: rel.under_def)
-
-lemma natLeq_on_ofilter_iff:
-"wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
-proof(rule iffI)
- assume *: "wo_rel.ofilter (natLeq_on m) A"
- hence 1: "A \<le> {0..<m}"
- by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on)
- hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
- using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def)
- hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
- thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
-next
- assume "(\<exists>n\<le>m. A = {0 ..< n})"
- thus "wo_rel.ofilter (natLeq_on m) A" by (auto simp add: natLeq_on_ofilter_less_eq)
-qed
-
-
subsubsection {* Then as cardinals *}
@@ -1418,8 +1374,7 @@
lemma natLeq_Card_order: "Card_order natLeq"
proof(auto simp add: natLeq_Well_order
Card_order_iff_Restr_underS Restr_natLeq2, simp add: Field_natLeq)
- fix n have "finite(Field (natLeq_on n))"
- unfolding Field_natLeq_on by auto
+ fix n have "finite(Field (natLeq_on n))" by (auto simp: Field_def)
moreover have "\<not>finite(UNIV::nat set)" by auto
ultimately show "natLeq_on n <o |UNIV::nat set|"
using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
@@ -1444,91 +1399,10 @@
using infinite_iff_card_of_nat[of A] card_of_nat
ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
-
corollary finite_iff_ordLess_natLeq:
"finite A = ( |A| <o natLeq)"
using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
- card_of_Well_order natLeq_Well_order
-by auto
-
-lemma ordIso_natLeq_on_imp_finite:
-"|A| =o natLeq_on n \<Longrightarrow> finite A"
-unfolding ordIso_def iso_def[abs_def]
-by (auto simp: Field_natLeq_on bij_betw_finite Field_card_of)
-
-
-lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
-proof(unfold card_order_on_def,
- auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
- fix r assume "well_order_on {0..<n} r"
- thus "natLeq_on n \<le>o r"
- using finite_atLeastLessThan natLeq_on_well_order_on
- finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
-qed
-
-
-corollary card_of_Field_natLeq_on:
-"|Field (natLeq_on n)| =o natLeq_on n"
-using Field_natLeq_on natLeq_on_Card_order
- Card_order_iff_ordIso_card_of[of "natLeq_on n"]
- ordIso_symmetric[of "natLeq_on n"] by blast
-
-
-corollary card_of_less:
-"|{0 ..< n}| =o natLeq_on n"
-using Field_natLeq_on card_of_Field_natLeq_on by auto
-
-
-lemma natLeq_on_ordLeq_less_eq:
-"((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
-proof
- assume "natLeq_on m \<le>o natLeq_on n"
- then obtain f where "inj_on f {0..<m} \<and> f ` {0..<m} \<le> {0..<n}"
- unfolding ordLeq_def using
- embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
- embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
- thus "m \<le> n" using atLeastLessThan_less_eq2 by blast
-next
- assume "m \<le> n"
- hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto
- hence "|{0..<m}| \<le>o |{0..<n}|" using card_of_ordLeq by blast
- thus "natLeq_on m \<le>o natLeq_on n"
- using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
-qed
-
-
-lemma natLeq_on_ordLeq_less:
-"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
-using not_ordLeq_iff_ordLess[of "natLeq_on m" "natLeq_on n"]
- natLeq_on_Well_order natLeq_on_ordLeq_less_eq
-by fastforce
-
-
-
-subsubsection {* "Backward compatibility" with the numeric cardinal operator for finite sets *}
-
-
-lemma finite_card_of_iff_card2:
-assumes FIN: "finite A" and FIN': "finite B"
-shows "( |A| \<le>o |B| ) = (card A \<le> card B)"
-using assms card_of_ordLeq[of A B] inj_on_iff_card_le[of A B] by blast
-
-
-lemma finite_imp_card_of_natLeq_on:
-assumes "finite A"
-shows "|A| =o natLeq_on (card A)"
-proof-
- obtain h where "bij_betw h A {0 ..< card A}"
- using assms ex_bij_betw_finite_nat by blast
- thus ?thesis using card_of_ordIso card_of_less ordIso_equivalence by blast
-qed
-
-
-lemma finite_iff_card_of_natLeq_on:
-"finite A = (\<exists>n. |A| =o natLeq_on n)"
-using finite_imp_card_of_natLeq_on[of A]
-by(auto simp add: ordIso_natLeq_on_imp_finite)
-
+ card_of_Well_order natLeq_Well_order by metis
subsection {* The successor of a cardinal *}
@@ -1667,55 +1541,6 @@
qed
-lemma cardSuc_natLeq_on_Suc:
-"cardSuc(natLeq_on n) =o natLeq_on(Suc n)"
-proof-
- obtain r r' p where r_def: "r = natLeq_on n" and
- r'_def: "r' = cardSuc(natLeq_on n)" and
- p_def: "p = natLeq_on(Suc n)" by blast
- (* Preliminary facts: *)
- have CARD: "Card_order r \<and> Card_order r' \<and> Card_order p" unfolding r_def r'_def p_def
- using cardSuc_ordLess_ordLeq natLeq_on_Card_order cardSuc_Card_order by blast
- hence WELL: "Well_order r \<and> Well_order r' \<and> Well_order p"
- unfolding card_order_on_def by force
- have FIELD: "Field r = {0..<n} \<and> Field p = {0..<(Suc n)}"
- unfolding r_def p_def Field_natLeq_on by simp
- hence FIN: "finite (Field r)" by force
- have "r <o r'" using CARD unfolding r_def r'_def using cardSuc_greater by blast
- hence "|Field r| <o r'" using CARD card_of_Field_ordIso ordIso_ordLess_trans by blast
- hence LESS: "|Field r| <o |Field r'|"
- using CARD card_of_Field_ordIso ordLess_ordIso_trans ordIso_symmetric by blast
- (* Main proof: *)
- have "r' \<le>o p" using CARD unfolding r_def r'_def p_def
- using natLeq_on_ordLeq_less cardSuc_ordLess_ordLeq by blast
- moreover have "p \<le>o r'"
- proof-
- {assume "r' <o p"
- then obtain f where 0: "embedS r' p f" unfolding ordLess_def by force
- let ?q = "Restr p (f ` Field r')"
- have 1: "embed r' p f" using 0 unfolding embedS_def by force
- hence 2: "f ` Field r' < {0..<(Suc n)}"
- using WELL FIELD 0 by (auto simp add: embedS_iff)
- have "wo_rel.ofilter p (f ` Field r')" using embed_Field_ofilter 1 WELL by blast
- then obtain m where "m \<le> Suc n" and 3: "f ` (Field r') = {0..<m}"
- unfolding p_def by (auto simp add: natLeq_on_ofilter_iff)
- hence 4: "m \<le> n" using 2 by force
- (* *)
- have "bij_betw f (Field r') (f ` (Field r'))"
- using 1 WELL embed_inj_on unfolding bij_betw_def by force
- moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
- ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
- using bij_betw_same_card bij_betw_finite by metis
- hence "card(Field r') \<le> card(Field r)" using 3 4 FIELD by force
- hence "|Field r'| \<le>o |Field r|" using FIN 5 finite_card_of_iff_card2 by blast
- hence False using LESS not_ordLess_ordLeq by auto
- }
- thus ?thesis using WELL CARD by (fastforce simp: not_ordLess_iff_ordLeq)
- qed
- ultimately show ?thesis using ordIso_iff_ordLeq unfolding r'_def p_def by blast
-qed
-
-
lemma card_of_cardSuc_finite:
"finite(Field(cardSuc |A| )) = finite A"
proof
@@ -1728,18 +1553,12 @@
thus "finite A" using * card_of_ordLeq_finite by blast
next
assume "finite A"
- then obtain n where "|A| =o natLeq_on n" using finite_iff_card_of_natLeq_on by blast
- hence "cardSuc |A| =o cardSuc(natLeq_on n)"
- using card_of_Card_order cardSuc_invar_ordIso natLeq_on_Card_order by blast
- hence "cardSuc |A| =o natLeq_on(Suc n)"
- using cardSuc_natLeq_on_Suc ordIso_transitive by blast
- hence "cardSuc |A| =o |{0..<(Suc n)}|" using card_of_less ordIso_equivalence by blast
- moreover have "|Field (cardSuc |A| ) | =o cardSuc |A|"
- using card_of_Field_ordIso cardSuc_Card_order card_of_Card_order by blast
- ultimately have "|Field (cardSuc |A| ) | =o |{0..<(Suc n)}|"
- using ordIso_equivalence by blast
- thus "finite (Field (cardSuc |A| ))"
- using card_of_ordIso_finite finite_atLeastLessThan by blast
+ then have "finite ( Field |Pow A| )" unfolding Field_card_of by simp
+ then show "finite (Field (cardSuc |A| ))"
+ proof (rule card_of_ordLeq_finite[OF card_of_mono2, rotated])
+ show "cardSuc |A| \<le>o |Pow A|"
+ by (metis cardSuc_ordLess_ordLeq card_of_Card_order card_of_Pow)
+ qed
qed
--- a/src/HOL/Cardinals/Fun_More.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/Cardinals/Fun_More.thy Mon Nov 25 13:48:00 2013 +0100
@@ -8,7 +8,7 @@
header {* More on Injections, Bijections and Inverses *}
theory Fun_More
-imports Fun_More_FP
+imports Fun_More_FP Main
begin
@@ -170,6 +170,20 @@
card_atLeastLessThan[of m] card_atLeastLessThan[of n]
bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto
+
+(*2*)lemma atLeastLessThan_less_eq:
+"({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)"
+unfolding ivl_subset by arith
+
+
+(*2*)lemma atLeastLessThan_less_eq2:
+assumes "inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}"
+shows "m \<le> n"
+using assms
+using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
+ card_atLeastLessThan[of m] card_atLeastLessThan[of n]
+ card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce
+
(* unused *)
(*2*)lemma atLeastLessThan_less_eq3:
"(\<exists>f. inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}) = (m \<le> n)"
--- a/src/HOL/Cardinals/Fun_More_FP.thy Mon Nov 25 12:27:03 2013 +0100
+++ b/src/HOL/Cardinals/Fun_More_FP.thy Mon Nov 25 13:48:00 2013 +0100
@@ -8,7 +8,7 @@
header {* More on Injections, Bijections and Inverses (FP) *}
theory Fun_More_FP
-imports Main
+imports Hilbert_Choice
begin
@@ -219,22 +219,5 @@
by (auto intro: inj_on_inv_into)
-subsection {* Other facts *}
-
-
-(*2*)lemma atLeastLessThan_less_eq:
-"({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)"
-unfolding ivl_subset by arith
-
-
-(*2*)lemma atLeastLessThan_less_eq2:
-assumes "inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}"
-shows "m \<le> n"
-using assms
-using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
- card_atLeastLessThan[of m] card_atLeastLessThan[of n]
- card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce
-
-
end