# HG changeset patch
# User blanchet
# Date 1384794285 -3600
# Node ID 57e781b711b55d6438a35f2387c01ff422356cef
# Parent  af1ea7ca741792d52c5b28facaf08275fd06c98f
no need for 3-way split with GFP for a handful of theorems

diff -r af1ea7ca7417 -r 57e781b711b5 src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Nov 18 18:04:45 2013 +0100
@@ -8,7 +8,7 @@
 header {* Cardinal Arithmetic  *}
 
 theory Cardinal_Arithmetic
-imports Cardinal_Arithmetic_GFP Cardinal_Order_Relation
+imports Cardinal_Arithmetic_LFP Cardinal_Order_Relation
 begin
 
 
diff -r af1ea7ca7417 -r 57e781b711b5 src/HOL/Cardinals/Cardinal_Arithmetic_GFP.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic_GFP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-(*  Title:      HOL/Cardinals/Cardinal_Arithmetic_GFP.thy
-    Author:     Dmitriy Traytel, TU Muenchen
-    Copyright   2012
-
-Cardinal arithmetic (GFP).
-*)
-
-header {* Cardinal Arithmetic (GFP) *}
-
-theory Cardinal_Arithmetic_GFP
-imports Cardinal_Arithmetic_LFP
-begin
-
-
-subsection {* Binary sum *}
-
-lemma Cinfinite_csum:
-  "Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
-unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
-
-lemma Cinfinite_csum_strong:
-  "\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
-by (metis Cinfinite_csum)
-
-
-subsection {* Exponentiation *}
-
-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]])
-
-end
diff -r af1ea7ca7417 -r 57e781b711b5 src/HOL/Cardinals/Cardinal_Arithmetic_LFP.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic_LFP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic_LFP.thy	Mon Nov 18 18:04:45 2013 +0100
@@ -187,6 +187,14 @@
   "Cinfinite r1 \<Longrightarrow> Cinfinite (r1 +c r2)"
 unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
 
+lemma Cinfinite_csum:
+  "Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
+unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
+
+lemma Cinfinite_csum_strong:
+  "\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
+by (metis Cinfinite_csum)
+
 lemma csum_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 +c p2 =o r1 +c r2"
 by (simp only: csum_def ordIso_Plus_cong)
 
@@ -682,6 +690,28 @@
   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 *)