# HG changeset patch
# User traytel
# Date 1385383680 -3600
# Node ID 1502a1f707d9113c4682567c6551e05d280c0bc4
# Parent  7b9336176a1cba27fd784a87208a9ecb86688426
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports

diff -r 7b9336176a1c -r 1502a1f707d9 src/HOL/BNF/BNF_Def.thy
--- 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"
 
diff -r 7b9336176a1c -r 1502a1f707d9 src/HOL/BNF/BNF_GFP.thy
--- 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
diff -r 7b9336176a1c -r 1502a1f707d9 src/HOL/BNF/BNF_Util.thy
--- 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
diff -r 7b9336176a1c -r 1502a1f707d9 src/HOL/BNF/Basic_BNFs.thy
--- 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
 
diff -r 7b9336176a1c -r 1502a1f707d9 src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- 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
diff -r 7b9336176a1c -r 1502a1f707d9 src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy
--- 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
diff -r 7b9336176a1c -r 1502a1f707d9 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- 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|"
diff -r 7b9336176a1c -r 1502a1f707d9 src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy
--- 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
 
 
diff -r 7b9336176a1c -r 1502a1f707d9 src/HOL/Cardinals/Fun_More.thy
--- 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)"
diff -r 7b9336176a1c -r 1502a1f707d9 src/HOL/Cardinals/Fun_More_FP.thy
--- 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