author paulson Wed, 09 Jun 2004 11:18:51 +0200 changeset 14889 d7711d6b9014 parent 14888 99ac3eb0f84e child 14890 51f28df21c8b
moved some cardinality results into main HOL
 src/HOL/Algebra/Exponent.thy file | annotate | diff | comparison | revisions src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions
```--- 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 @@

-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)```
```--- 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 *}
```