# HG changeset patch
# User paulson
# Date 1086772731 -7200
# Node ID d7711d6b901448f9bf256e1d648f4ca5a7fe414d
# Parent  99ac3eb0f84ee7e5313a4272293225d98ceabd98
moved some cardinality results into main HOL

diff -r 99ac3eb0f84e -r d7711d6b9014 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Tue Jun 08 19:25:27 2004 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Wed Jun 09 11:18:51 2004 +0200
@@ -34,29 +34,6 @@
 by (force simp add: prime_iff)
 
 
-lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
-apply (rule_tac P = "%x. x <= b * c" in subst)
-apply (rule mult_1_right)
-apply (rule mult_le_mono, auto)
-done
-
-lemma insert_partition:
-     "[| x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 --> c1 \<inter> c2 = {}|] 
-      ==> x \<inter> \<Union> F = {}"
-by auto
-
-(* main cardinality theorem *)
-lemma card_partition [rule_format]:
-     "finite C ==>  
-        finite (\<Union> C) -->  
-        (\<forall>c\<in>C. card c = k) -->   
-        (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
-        k * card(C) = card (\<Union> C)"
-apply (erule finite_induct, simp)
-apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
-       finite_subset [of _ "\<Union> (insert x F)"])
-done
-
 lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
 by (rule ccontr, simp)
 
@@ -221,6 +198,12 @@
 
 subsection{*Lemmas for the Main Combinatorial Argument*}
 
+lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
+apply (rule_tac P = "%x. x <= b * c" in subst)
+apply (rule mult_1_right)
+apply (rule mult_le_mono, auto)
+done
+
 lemma p_fac_forw_lemma:
      "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
 apply (rule notnotD)
diff -r 99ac3eb0f84e -r d7711d6b9014 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jun 08 19:25:27 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jun 09 11:18:51 2004 +0200
@@ -496,6 +496,23 @@
 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
 by (erule psubsetI, blast)
 
+lemma insert_partition:
+     "[| x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 --> c1 \<inter> c2 = {}|] 
+      ==> x \<inter> \<Union> F = {}"
+by auto
+
+(* main cardinality theorem *)
+lemma card_partition [rule_format]:
+     "finite C ==>  
+        finite (\<Union> C) -->  
+        (\<forall>c\<in>C. card c = k) -->   
+        (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
+        k * card(C) = card (\<Union> C)"
+apply (erule finite_induct, simp)
+apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
+       finite_subset [of _ "\<Union> (insert x F)"])
+done
+
 
 subsubsection {* Cardinality of image *}