# HG changeset patch
# User haftmann
# Date 1275485714 -7200
# Node ID 2b1c6dd4899593bd99e6e1807ea2ddbc4bca6938
# Parent  9834c21c4ba1c8ac55c51483c6e8c2d480583a4f
removed dependency of Euclid on Old_Number_Theory

diff -r 9834c21c4ba1 -r 2b1c6dd48995 src/HOL/Extraction/Euclid.thy
--- a/src/HOL/Extraction/Euclid.thy	Wed Jun 02 15:35:13 2010 +0200
+++ b/src/HOL/Extraction/Euclid.thy	Wed Jun 02 15:35:14 2010 +0200
@@ -7,16 +7,43 @@
 header {* Euclid's theorem *}
 
 theory Euclid
-imports "~~/src/HOL/Old_Number_Theory/Factorization" Util Efficient_Nat
+imports "~~/src/HOL/Number_Theory/UniqueFactorization" Util Efficient_Nat
 begin
 
+lemma list_nonempty_induct [consumes 1, case_names single cons]:
+  assumes "xs \<noteq> []"
+  assumes single: "\<And>x. P [x]"
+  assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"
+  shows "P xs"
+using `xs \<noteq> []` proof (induct xs)
+  case Nil then show ?case by simp
+next
+  case (Cons x xs) show ?case proof (cases xs)
+    case Nil with single show ?thesis by simp
+  next
+    case Cons then have "xs \<noteq> []" by simp
+    moreover with Cons.hyps have "P xs" .
+    ultimately show ?thesis by (rule cons)
+  qed
+qed
+
 text {*
 A constructive version of the proof of Euclid's theorem by
 Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}.
 *}
 
-lemma prime_eq: "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
-  apply (simp add: prime_def)
+lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
+  by (induct m) auto
+
+lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k"
+  by (induct k) auto
+
+lemma prod_mn_less_k:
+  "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"
+  by (induct m) auto
+
+lemma prime_eq: "prime (p::nat) = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
+  apply (simp add: prime_nat_def)
   apply (rule iffI)
   apply blast
   apply (erule conjE)
@@ -33,15 +60,9 @@
   apply simp
   done
 
-lemma prime_eq': "prime p = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
+lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
   by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps)
 
-lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
-  by (induct m) auto
-
-lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k"
-  by (induct k) auto
-
 lemma not_prime_ex_mk:
   assumes n: "Suc 0 < n"
   shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
@@ -96,7 +117,55 @@
   qed
 qed
 
-lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)"
+lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact (n::nat)"
+proof (induct n rule: nat_induct)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  from `m \<le> Suc n` show ?case
+  proof (rule le_SucE)
+    assume "m \<le> n"
+    with `0 < m` have "m dvd fact n" by (rule Suc)
+    then have "m dvd (fact n * Suc n)" by (rule dvd_mult2)
+    then show ?thesis by (simp add: mult_commute)
+  next
+    assume "m = Suc n"
+    then have "m dvd (fact n * Suc n)"
+      by (auto intro: dvdI simp: mult_ac)
+    then show ?thesis by (simp add: mult_commute)
+  qed
+qed
+
+lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#multiset_of (n # ns). m)"
+  by (simp add: msetprod_Un msetprod_singleton)
+
+abbreviation (input) "primel ps \<equiv> (\<forall>(p::nat)\<in>set ps. prime p)"
+
+lemma prime_primel: "prime n \<Longrightarrow> primel [n]"
+  by simp
+
+lemma split_primel:
+  assumes "primel ms" and "primel ns"
+  shows "\<exists>qs. primel qs \<and> (PROD m\<Colon>nat:#multiset_of qs. m) =
+    (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
+proof -
+  from assms have "primel (ms @ ns)"
+    unfolding set_append ball_Un by iprover
+  moreover from assms have "(PROD m\<Colon>nat:#multiset_of (ms @ ns). m) =
+    (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)"
+    by (simp add: msetprod_Un)
+  ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
+  then show ?thesis ..
+qed
+
+lemma primel_nempty_g_one:
+  assumes "primel ps" and "ps \<noteq> []"
+  shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)"
+  using `ps \<noteq> []` `primel ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
+    (simp_all add: msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
+
+lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = n)"
 proof (induct n rule: nat_wf_ind)
   case (1 n)
   from `Suc 0 < n`
@@ -107,51 +176,22 @@
     assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
     then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
       and kn: "k < n" and nmk: "n = m * k" by iprover
-    from mn and m have "\<exists>l. primel l \<and> prod l = m" by (rule 1)
-    then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "prod l1 = m"
+    from mn and m have "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = m" by (rule 1)
+    then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "(PROD m\<Colon>nat:#multiset_of l1. m) = m"
       by iprover
-    from kn and k have "\<exists>l. primel l \<and> prod l = k" by (rule 1)
-    then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "prod l2 = k"
+    from kn and k have "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = k" by (rule 1)
+    then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "(PROD m\<Colon>nat:#multiset_of l2. m) = k"
       by iprover
     from primel_l1 primel_l2
-    have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2"
+    have "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) =
+      (PROD m\<Colon>nat:#multiset_of l1. m) * (PROD m\<Colon>nat:#multiset_of l2. m)"
       by (rule split_primel)
     with prod_l1_m prod_l2_k nmk show ?thesis by simp
   next
-    assume "prime n"
-    hence "primel [n] \<and> prod [n] = n" by (rule prime_primel)
-    thus ?thesis ..
-  qed
-qed
-
-lemma dvd_prod [iff]: "n dvd prod (n # ns)"
-  by simp
-
-primrec fact :: "nat \<Rightarrow> nat"    ("(_!)" [1000] 999)
-where
-    "0! = 1"
-  | "(Suc n)! = n! * Suc n"
-
-lemma fact_greater_0 [iff]: "0 < n!"
-  by (induct n) simp_all
-
-lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd n!"
-proof (induct n)
-  case 0
-  then show ?case by simp
-next
-  case (Suc n)
-  from `m \<le> Suc n` show ?case
-  proof (rule le_SucE)
-    assume "m \<le> n"
-    with `0 < m` have "m dvd n!" by (rule Suc)
-    then have "m dvd (n! * Suc n)" by (rule dvd_mult2)
-    then show ?thesis by simp
-  next
-    assume "m = Suc n"
-    then have "m dvd (n! * Suc n)"
-      by (auto intro: dvdI simp: mult_ac)
-    then show ?thesis by simp
+    assume "prime n" then have "primel [n]" by (rule prime_primel)
+    moreover have "(PROD m\<Colon>nat:#multiset_of [n]. m) = n" by (simp add: msetprod_singleton)
+    ultimately have "primel [n] \<and> (PROD m\<Colon>nat:#multiset_of [n]. m) = n" ..
+    then show ?thesis ..
   qed
 qed
 
@@ -160,13 +200,14 @@
   shows "\<exists>p. prime p \<and> p dvd n"
 proof -
   from N obtain l where primel_l: "primel l"
-    and prod_l: "n = prod l" using factor_exists
+    and prod_l: "n = (PROD m\<Colon>nat:#multiset_of l. m)" using factor_exists
     by simp iprover
-  from prems have "l \<noteq> []"
-    by (auto simp add: primel_nempty_g_one)
+  with N have "l \<noteq> []"
+    by (auto simp add: primel_nempty_g_one msetprod_empty)
   then obtain x xs where l: "l = x # xs"
     by (cases l) simp
-  from primel_l l have "prime x" by (simp add: primel_hd_tl)
+  then have "x \<in> set l" by (simp only: insert_def set.simps) (iprover intro: UnI1 CollectI)
+  with primel_l have "prime x" ..
   moreover from primel_l l prod_l
   have "x dvd n" by (simp only: dvd_prod)
   ultimately show ?thesis by iprover
@@ -176,21 +217,21 @@
 Euclid's theorem: there are infinitely many primes.
 *}
 
-lemma Euclid: "\<exists>p. prime p \<and> n < p"
+lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
 proof -
-  let ?k = "n! + 1"
-  have "1 < n! + 1" by simp
+  let ?k = "fact n + 1"
+  have "1 < fact n + 1" by simp
   then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover
   have "n < p"
   proof -
     have "\<not> p \<le> n"
     proof
       assume pn: "p \<le> n"
-      from `prime p` have "0 < p" by (rule prime_g_zero)
-      then have "p dvd n!" using pn by (rule dvd_factorial)
-      with dvd have "p dvd ?k - n!" by (rule dvd_diff_nat)
+      from `prime p` have "0 < p" by (rule prime_gt_0_nat)
+      then have "p dvd fact n" using pn by (rule dvd_factorial)
+      with dvd have "p dvd ?k - fact n" by (rule dvd_diff_nat)
       then have "p dvd 1" by simp
-      with prime show False using prime_nd_one by auto
+      with prime show False by auto
     qed
     then show ?thesis by simp
   qed
@@ -224,29 +265,26 @@
 
 end
 
+primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
+  "iterate 0 f x = []"
+  | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
+
+lemma "factor_exists 1007 = [53, 19]" by eval
+lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
+lemma "factor_exists 345 = [23, 5, 3]" by eval
+lemma "factor_exists 999 = [37, 3, 3, 3]" by eval
+lemma "factor_exists 876 = [73, 3, 2, 2]" by eval
+
+lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval
+
 consts_code
   default ("(error \"default\")")
 
 lemma "factor_exists 1007 = [53, 19]" by evaluation
-lemma "factor_exists 1007 = [53, 19]" by eval
-
 lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by evaluation
-lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
-
 lemma "factor_exists 345 = [23, 5, 3]" by evaluation
-lemma "factor_exists 345 = [23, 5, 3]" by eval
-
 lemma "factor_exists 999 = [37, 3, 3, 3]" by evaluation
-lemma "factor_exists 999 = [37, 3, 3, 3]" by eval
-
 lemma "factor_exists 876 = [73, 3, 2, 2]" by evaluation
-lemma "factor_exists 876 = [73, 3, 2, 2]" by eval
-
-primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
-  "iterate 0 f x = []"
-  | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
-
 lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by evaluation
-lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval
 
 end
diff -r 9834c21c4ba1 -r 2b1c6dd48995 src/HOL/Extraction/ROOT.ML
--- a/src/HOL/Extraction/ROOT.ML	Wed Jun 02 15:35:13 2010 +0200
+++ b/src/HOL/Extraction/ROOT.ML	Wed Jun 02 15:35:14 2010 +0200
@@ -2,5 +2,5 @@
 
 Proofterm.proofs := 2;
 
-no_document use_thys ["Efficient_Nat", "~~/src/HOL/Old_Number_Theory/Factorization"];
+no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"];
 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];