# HG changeset patch
# User paulson
# Date 864732402 -7200
# Node ID 88cd6a2c6ebed602775a690e12f9749439630855
# Parent  13f1df323daf6d024701579398a69d96ebc9dd72
New theorems suggested by Florian Kammueller

diff -r 13f1df323daf -r 88cd6a2c6ebe src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Tue May 27 13:26:11 1997 +0200
+++ b/src/HOL/ex/Primes.ML	Tue May 27 13:26:42 1997 +0200
@@ -37,6 +37,35 @@
                      addss (!simpset addsimps [mult_assoc, mult_eq_1_iff])) 1);
 qed "dvd_anti_sym";
 
+goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)";
+by (blast_tac (!claset addIs [add_mult_distrib2 RS sym]) 1);
+qed "dvd_add";
+
+goalw thy [dvd_def] "!!k. k dvd m ==> k dvd (q * m)";
+by (blast_tac (!claset addIs [mult_left_commute]) 1);
+qed "dvd_mult";
+
+(*Based on a theorem of F. Kammüller's.  Doesn't really belong here...*)
+goal Primes.thy "!!C. finite C ==> finite (Union C) --> \
+\          (! c : C. k dvd card c) -->  \
+\          (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \
+\          --> k dvd card(Union C)";
+by (etac finite_induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (strip_tac 1);
+by (REPEAT (etac conjE 1));
+by (stac card_Un_disjoint 1);
+by (ALLGOALS
+    (asm_full_simp_tac (!simpset
+			 addsimps [dvd_add, disjoint_eq_subset_Compl])));
+by (thin_tac "?PP-->?QQ" 1);
+by (thin_tac "!c:F. ?PP(c)" 1);
+by (thin_tac "!c:F. ?PP(c) & ?QQ(c)" 1);
+by (Step_tac 1);
+by (ball_tac 1);
+by (Blast_tac 1);
+qed "dvd_partition";
+
 
 (************************************************)
 (** Greatest Common Divisor                    **)
@@ -71,14 +100,6 @@
 by (Simp_tac 1);
 qed "gcd_0_dvd_0";
 
-goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)";
-by (blast_tac (!claset addIs [add_mult_distrib2 RS sym]) 1);
-qed "dvd_add";
-
-goalw thy [dvd_def] "!!k. k dvd m ==> k dvd (q * m)";
-by (blast_tac (!claset addIs [mult_left_commute]) 1);
-qed "dvd_mult";
-
 goal thy "!!k. [| k dvd (m mod n); k dvd n; n~=0 |] ==> k dvd m";
 by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
 by (asm_simp_tac (!simpset addsimps [dvd_add, dvd_mult]) 2);