--- 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;
--- 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)
--- 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
--- 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}"
--- 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