diff -r 87201c60ae7d -r 521cc9bf2958 src/HOL/Number_Theory/Primes.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/Primes.thy	Tue Sep 01 15:39:33 2009 +0200
@@ -0,0 +1,423 @@
+(*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
+                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
+
+
+This file deals with properties of primes. Definitions and lemmas are
+proved uniformly for the natural numbers and integers.
+
+This file combines and revises a number of prior developments.
+
+The original theories "GCD" and "Primes" were by Christophe Tabacznyj
+and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
+gcd, lcm, and prime for the natural numbers.
+
+The original theory "IntPrimes" was by Thomas M. Rasmussen, and
+extended gcd, lcm, primes to the integers. Amine Chaieb provided
+another extension of the notions to the integers, and added a number
+of results to "Primes" and "GCD". IntPrimes also defined and developed
+the congruence relations on the integers. The notion was extended to
+the natural numbers by Chiaeb.
+
+Jeremy Avigad combined all of these, made everything uniform for the
+natural numbers and the integers, and added a number of new theorems.
+
+Tobias Nipkow cleaned up a lot.
+*)
+
+
+header {* Primes *}
+
+theory Primes
+imports GCD
+begin
+
+declare One_nat_def [simp del]
+
+class prime = one +
+
+fixes
+  prime :: "'a \<Rightarrow> bool"
+
+instantiation nat :: prime
+
+begin
+
+definition
+  prime_nat :: "nat \<Rightarrow> bool"
+where
+  [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+
+instance proof qed
+
+end
+
+instantiation int :: prime
+
+begin
+
+definition
+  prime_int :: "int \<Rightarrow> bool"
+where
+  [code del]: "prime_int p = prime (nat p)"
+
+instance proof qed
+
+end
+
+
+subsection {* Set up Transfer *}
+
+
+lemma transfer_nat_int_prime:
+  "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
+  unfolding gcd_int_def lcm_int_def prime_int_def
+  by auto
+
+declare TransferMorphism_nat_int[transfer add return:
+    transfer_nat_int_prime]
+
+lemma transfer_int_nat_prime:
+  "prime (int x) = prime x"
+  by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
+
+declare TransferMorphism_int_nat[transfer add return:
+    transfer_int_nat_prime]
+
+
+subsection {* Primes *}
+
+lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
+  unfolding prime_nat_def
+  apply (subst even_mult_two_ex)
+  apply clarify
+  apply (drule_tac x = 2 in spec)
+  apply auto
+done
+
+lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
+  unfolding prime_int_def
+  apply (frule prime_odd_nat)
+  apply (auto simp add: even_nat_def)
+done
+
+(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
+
+lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
+  by (unfold prime_nat_def, auto)
+
+lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
+  by (unfold prime_nat_def, auto)
+
+lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
+  by (unfold prime_nat_def, auto)
+
+lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
+  by (unfold prime_nat_def, auto)
+
+lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
+  by (unfold prime_nat_def, auto)
+
+lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
+  by (unfold prime_nat_def, auto)
+
+lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
+  by (unfold prime_nat_def, auto)
+
+lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
+  by (unfold prime_int_def prime_nat_def) auto
+
+lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
+  by (unfold prime_int_def prime_nat_def, auto)
+
+lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
+  by (unfold prime_int_def prime_nat_def, auto)
+
+lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
+  by (unfold prime_int_def prime_nat_def, auto)
+
+lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
+  by (unfold prime_int_def prime_nat_def, auto)
+
+
+lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
+    m = 1 \<or> m = p))"
+  using prime_nat_def [transferred]
+    apply (case_tac "p >= 0")
+    by (blast, auto simp add: prime_ge_0_int)
+
+lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
+  apply (unfold prime_nat_def)
+  apply (metis gcd_dvd1_nat gcd_dvd2_nat)
+  done
+
+lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
+  apply (unfold prime_int_altdef)
+  apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
+  done
+
+lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
+  by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
+
+lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
+  by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
+
+lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
+    p dvd m * n = (p dvd m \<or> p dvd n)"
+  by (rule iffI, rule prime_dvd_mult_nat, auto)
+
+lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
+    p dvd m * n = (p dvd m \<or> p dvd n)"
+  by (rule iffI, rule prime_dvd_mult_int, auto)
+
+lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
+    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
+  unfolding prime_nat_def dvd_def apply auto
+  by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
+
+lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
+    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
+  unfolding prime_int_altdef dvd_def
+  apply auto
+  by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
+
+lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
+    n > 0 --> (p dvd x^n --> p dvd x)"
+  by (induct n rule: nat_induct, auto)
+
+lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
+    n > 0 --> (p dvd x^n --> p dvd x)"
+  apply (induct n rule: nat_induct, auto)
+  apply (frule prime_ge_0_int)
+  apply auto
+done
+
+subsubsection{* Make prime naively executable *}
+
+lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
+  by (simp add: prime_nat_def)
+
+lemma zero_not_prime_int [simp]: "~prime (0::int)"
+  by (simp add: prime_int_def)
+
+lemma one_not_prime_nat [simp]: "~prime (1::nat)"
+  by (simp add: prime_nat_def)
+
+lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
+  by (simp add: prime_nat_def One_nat_def)
+
+lemma one_not_prime_int [simp]: "~prime (1::int)"
+  by (simp add: prime_int_def)
+
+lemma prime_nat_code[code]:
+ "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
+apply(simp add: Ball_def)
+apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
+done
+
+lemma prime_nat_simp:
+ "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
+apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
+apply(simp add:nat_number One_nat_def)
+done
+
+lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard]
+
+lemma prime_int_code[code]:
+  "prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R")
+proof
+  assume "?L" thus "?R"
+    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
+next
+    assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
+qed
+
+lemma prime_int_simp:
+  "prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))"
+apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto)
+apply simp
+done
+
+lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
+
+lemma two_is_prime_nat [simp]: "prime (2::nat)"
+by simp
+
+lemma two_is_prime_int [simp]: "prime (2::int)"
+by simp
+
+text{* A bit of regression testing: *}
+
+lemma "prime(97::nat)"
+by simp
+
+lemma "prime(97::int)"
+by simp
+
+lemma "prime(997::nat)"
+by eval
+
+lemma "prime(997::int)"
+by eval
+
+
+lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
+  apply (rule coprime_exp_nat)
+  apply (subst gcd_commute_nat)
+  apply (erule (1) prime_imp_coprime_nat)
+done
+
+lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
+  apply (rule coprime_exp_int)
+  apply (subst gcd_commute_int)
+  apply (erule (1) prime_imp_coprime_int)
+done
+
+lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+  apply (rule prime_imp_coprime_nat, assumption)
+  apply (unfold prime_nat_def, auto)
+done
+
+lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+  apply (rule prime_imp_coprime_int, assumption)
+  apply (unfold prime_int_altdef, clarify)
+  apply (drule_tac x = q in spec)
+  apply (drule_tac x = p in spec)
+  apply auto
+done
+
+lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
+  by (rule coprime_exp2_nat, rule primes_coprime_nat)
+
+lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
+  by (rule coprime_exp2_int, rule primes_coprime_int)
+
+lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
+  apply (induct n rule: nat_less_induct)
+  apply (case_tac "n = 0")
+  using two_is_prime_nat apply blast
+  apply (case_tac "prime n")
+  apply blast
+  apply (subgoal_tac "n > 1")
+  apply (frule (1) not_prime_eq_prod_nat)
+  apply (auto intro: dvd_mult dvd_mult2)
+done
+
+(* An Isar version:
+
+lemma prime_factor_b_nat:
+  fixes n :: nat
+  assumes "n \<noteq> 1"
+  shows "\<exists>p. prime p \<and> p dvd n"
+
+using `n ~= 1`
+proof (induct n rule: less_induct_nat)
+  fix n :: nat
+  assume "n ~= 1" and
+    ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
+  thus "\<exists>p. prime p \<and> p dvd n"
+  proof -
+  {
+    assume "n = 0"
+    moreover note two_is_prime_nat
+    ultimately have ?thesis
+      by (auto simp del: two_is_prime_nat)
+  }
+  moreover
+  {
+    assume "prime n"
+    hence ?thesis by auto
+  }
+  moreover
+  {
+    assume "n ~= 0" and "~ prime n"
+    with `n ~= 1` have "n > 1" by auto
+    with `~ prime n` and not_prime_eq_prod_nat obtain m k where
+      "n = m * k" and "1 < m" and "m < n" by blast
+    with ih obtain p where "prime p" and "p dvd m" by blast
+    with `n = m * k` have ?thesis by auto
+  }
+  ultimately show ?thesis by blast
+  qed
+qed
+
+*)
+
+text {* One property of coprimality is easier to prove via prime factors. *}
+
+lemma prime_divprod_pow_nat:
+  assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
+  shows "p^n dvd a \<or> p^n dvd b"
+proof-
+  {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
+      apply (cases "n=0", simp_all)
+      apply (cases "a=1", simp_all) done}
+  moreover
+  {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
+    then obtain m where m: "n = Suc m" by (cases n, auto)
+    from n have "p dvd p^n" by (intro dvd_power, auto)
+    also note pab
+    finally have pab': "p dvd a * b".
+    from prime_dvd_mult_nat[OF p pab']
+    have "p dvd a \<or> p dvd b" .
+    moreover
+    {assume pa: "p dvd a"
+      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
+      from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
+      with p have "coprime b p"
+        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
+      hence pnb: "coprime (p^n) b"
+        by (subst gcd_commute_nat, rule coprime_exp_nat)
+      from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
+    moreover
+    {assume pb: "p dvd b"
+      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
+      from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
+        by auto
+      with p have "coprime a p"
+        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
+      hence pna: "coprime (p^n) a"
+        by (subst gcd_commute_nat, rule coprime_exp_nat)
+      from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
+    ultimately have ?thesis by blast}
+  ultimately show ?thesis by blast
+qed
+
+subsection {* Infinitely many primes *}
+
+lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
+proof-
+  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
+  from prime_factor_nat [OF f1]
+      obtain p where "prime p" and "p dvd fact n + 1" by auto
+  hence "p \<le> fact n + 1" 
+    by (intro dvd_imp_le, auto)
+  {assume "p \<le> n"
+    from `prime p` have "p \<ge> 1" 
+      by (cases p, simp_all)
+    with `p <= n` have "p dvd fact n" 
+      by (intro dvd_fact_nat)
+    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
+      by (rule dvd_diff_nat)
+    hence "p dvd 1" by simp
+    hence "p <= 1" by auto
+    moreover from `prime p` have "p > 1" by auto
+    ultimately have False by auto}
+  hence "n < p" by arith
+  with `prime p` and `p <= fact n + 1` show ?thesis by auto
+qed
+
+lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
+using next_prime_bound by auto
+
+lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
+proof
+  assume "finite {(p::nat). prime p}"
+  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
+    by auto
+  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
+    by auto
+  with bigger_prime [of b] show False by auto
+qed
+
+
+end