# HG changeset patch
# User traytel
# Date 1387292217 -3600
# Node ID e279c2ceb54c81489b300cb45198ed48a4c9fcd4
# Parent  c99f0fdb08863fa47f024aec2a4fee6a860ec467
reduced cardinals dependencies of (co)datatypes

diff -r c99f0fdb0886 -r e279c2ceb54c src/HOL/BNF/Tools/bnf_lfp_util.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_util.ML	Tue Dec 17 15:44:10 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_util.ML	Tue Dec 17 15:56:57 2013 +0100
@@ -12,7 +12,6 @@
 
   val mk_bij_betw: term -> term -> term -> term
   val mk_cardSuc: term -> term
-  val mk_cpow: term -> term
   val mk_inver: term -> term -> term -> term
   val mk_not_empty: term -> term
   val mk_not_eq: term -> term -> term
@@ -49,10 +48,6 @@
   let val T = fst (dest_relT (fastype_of r));
   in Const (@{const_name cardSuc}, mk_relT (T, T) --> mk_relT (`I (HOLogic.mk_setT T))) $ r end;
 
-fun mk_cpow r =
-  let val T = fst (dest_relT (fastype_of r));
-  in Const (@{const_name cpow}, mk_relT (T, T) --> mk_relT (`I (HOLogic.mk_setT T))) $ r end;
-
 fun mk_bij_betw f A B =
  Const (@{const_name bij_betw},
    fastype_of f --> fastype_of A --> fastype_of B --> HOLogic.boolT) $ f $ A $ B;
diff -r c99f0fdb0886 -r e279c2ceb54c src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Tue Dec 17 15:44:10 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Tue Dec 17 15:56:57 2013 +0100
@@ -172,8 +172,43 @@
 unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field)
 
 
+lemma card_order_cexp:
+  assumes "card_order r1" "card_order r2"
+  shows "card_order (r1 ^c r2)"
+proof -
+  have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto
+  thus ?thesis unfolding cexp_def Func_def by (simp add: card_of_card_order_on)
+qed
+
+lemma Cinfinite_ordLess_cexp:
+  assumes r: "Cinfinite r"
+  shows "r <o r ^c r"
+proof -
+  have "r <o ctwo ^c r" using r by (simp only: ordLess_ctwo_cexp)
+  also have "ctwo ^c r \<le>o r ^c r"
+    by (rule cexp_mono1[OF ctwo_ordLeq_Cinfinite]) (auto simp: r ctwo_not_czero Card_order_ctwo)
+  finally show ?thesis .
+qed
+
+lemma infinite_ordLeq_cexp:
+  assumes "Cinfinite r"
+  shows "r \<le>o r ^c r"
+by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]])
+
+
 subsection {* Powerset *}
 
+definition cpow where "cpow r = |Pow (Field r)|"
+
+lemma card_order_cpow: "card_order r \<Longrightarrow> card_order (cpow r)"
+by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on)
+
+lemma cpow_greater_eq: "Card_order r \<Longrightarrow> r \<le>o cpow r"
+by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow)
+
+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)
+
 lemma Card_order_cpow: "Card_order (cpow r)"
 unfolding cpow_def by (rule card_of_Card_order)
 
diff -r c99f0fdb0886 -r e279c2ceb54c src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy	Tue Dec 17 15:44:10 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy	Tue Dec 17 15:56:57 2013 +0100
@@ -700,29 +700,6 @@
   finally show ?thesis .
 qed
 
-lemma card_order_cexp:
-  assumes "card_order r1" "card_order r2"
-  shows "card_order (r1 ^c r2)"
-proof -
-  have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto
-  thus ?thesis unfolding cexp_def Func_def by (simp add: card_of_card_order_on)
-qed
-
-lemma Cinfinite_ordLess_cexp:
-  assumes r: "Cinfinite r"
-  shows "r <o r ^c r"
-proof -
-  have "r <o ctwo ^c r" using r by (simp only: ordLess_ctwo_cexp)
-  also have "ctwo ^c r \<le>o r ^c r"
-    by (rule cexp_mono1[OF ctwo_ordLeq_Cinfinite]) (auto simp: r ctwo_not_czero Card_order_ctwo)
-  finally show ?thesis .
-qed
-
-lemma infinite_ordLeq_cexp:
-  assumes "Cinfinite r"
-  shows "r \<le>o r ^c r"
-by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]])
-
 (* cardSuc *)
 
 lemma Cinfinite_cardSuc: "Cinfinite r \<Longrightarrow> Cinfinite (cardSuc r)"
@@ -733,17 +710,4 @@
   shows "EX i : Field (cardSuc r). B \<le> As i"
 using cardSuc_UNION assms unfolding cinfinite_def by blast
 
-subsection {* Powerset *}
-
-definition cpow where "cpow r = |Pow (Field r)|"
-
-lemma card_order_cpow: "card_order r \<Longrightarrow> card_order (cpow r)"
-by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on)
-
-lemma cpow_greater_eq: "Card_order r \<Longrightarrow> r \<le>o cpow r"
-by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow)
-
-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)
-
 end
diff -r c99f0fdb0886 -r e279c2ceb54c src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Dec 17 15:44:10 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Dec 17 15:56:57 2013 +0100
@@ -1369,6 +1369,14 @@
 shows "|B| \<le>o |f -` B|"
 by (metis assms card_of_vimage subset_UNIV)
 
+lemma infinite_Pow:
+assumes "\<not> finite A"
+shows "\<not> finite (Pow A)"
+proof-
+  have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
+  thus ?thesis by (metis assms finite_Pow_iff)
+qed
+
 (* bounded powerset *)
 definition Bpow where
 "Bpow r A \<equiv> {X . X \<subseteq> A \<and> |X| \<le>o r}"
diff -r c99f0fdb0886 -r e279c2ceb54c src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Tue Dec 17 15:44:10 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Tue Dec 17 15:56:57 2013 +0100
@@ -486,15 +486,6 @@
 using card_of_Pow card_of_Field_ordIso ordIso_ordLess_trans ordIso_symmetric by blast
 
 
-lemma infinite_Pow:
-assumes "\<not> finite A"
-shows "\<not> finite (Pow A)"
-proof-
-  have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
-  thus ?thesis by (metis assms finite_Pow_iff)
-qed
-
-
 lemma card_of_Plus1: "|A| \<le>o |A <+> B|"
 proof-
   have "Inl ` A \<le> A <+> B" by auto