author  paulson <lp15@cam.ac.uk> 
Sun, 02 Feb 2014 19:15:25 +0000  
changeset 55242  413ec965f95d 
parent 55238  7ddb889e23bd 
child 55337  5d45fb978d5a 
permissions  rwrr 
32479  1 
(* Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 
31798  2 
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow 
31706  3 

4 

32479  5 
This file deals with properties of primes. Definitions and lemmas are 
6 
proved uniformly for the natural numbers and integers. 

31706  7 

8 
This file combines and revises a number of prior developments. 

9 

10 
The original theories "GCD" and "Primes" were by Christophe Tabacznyj 

11 
and Lawrence C. Paulson, based on \cite{davenport92}. They introduced 

12 
gcd, lcm, and prime for the natural numbers. 

13 

14 
The original theory "IntPrimes" was by Thomas M. Rasmussen, and 

15 
extended gcd, lcm, primes to the integers. Amine Chaieb provided 

16 
another extension of the notions to the integers, and added a number 

17 
of results to "Primes" and "GCD". IntPrimes also defined and developed 

18 
the congruence relations on the integers. The notion was extended to 

33718  19 
the natural numbers by Chaieb. 
31706  20 

32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

21 
Jeremy Avigad combined all of these, made everything uniform for the 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

22 
natural numbers and the integers, and added a number of new theorems. 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

23 

31798  24 
Tobias Nipkow cleaned up a lot. 
21256  25 
*) 
26 

31706  27 

32479  28 
header {* Primes *} 
21256  29 

32479  30 
theory Primes 
37294
a2a8216999a2
absolute import  must work with Main.thy / HOLProofs
haftmann
parents:
35644
diff
changeset

31 
imports "~~/src/HOL/GCD" 
31706  32 
begin 
33 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

34 
declare One_nat_def [simp] 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

35 
declare [[coercion int]] 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

36 
declare [[coercion_enabled]] 
31706  37 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

38 
definition prime :: "nat \<Rightarrow> bool" 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

39 
where "prime p = (1 < p \<and> (\<forall>m. m dvd p > m = 1 \<or> m = p))" 
31706  40 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

41 
lemmas prime_nat_def = prime_def 
31798  42 

21256  43 

32479  44 
subsection {* Primes *} 
31706  45 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

46 
lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p" 
54228  47 
apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0) 
48 
apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral) 

49 
done 

31706  50 

31992  51 
(* FIXME Is there a better way to handle these, rather than making them elim rules? *) 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

52 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

53 
lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0" 
44872  54 
unfolding prime_nat_def by auto 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

55 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

56 
lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1" 
44872  57 
unfolding prime_nat_def by auto 
22367  58 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

59 
lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1" 
44872  60 
unfolding prime_nat_def by auto 
31706  61 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

62 
lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0" 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

63 
unfolding prime_nat_def by auto 
31706  64 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

65 
lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0" 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

66 
unfolding prime_nat_def by auto 
31706  67 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

68 
lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2" 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

69 
unfolding prime_nat_def by auto 
31706  70 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

71 
lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n" 
31706  72 
apply (unfold prime_nat_def) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

73 
apply (metis gcd_dvd1_nat gcd_dvd2_nat) 
31706  74 
done 
75 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

76 
lemma prime_int_altdef: 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

77 
"prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow> 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

78 
m = 1 \<or> m = p))" 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

79 
apply (simp add: prime_def) 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

80 
apply (auto simp add: ) 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

81 
apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff) 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

82 
apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff) 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

83 
done 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

84 

413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

85 
lemma prime_imp_coprime_int: 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

86 
fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n" 
31706  87 
apply (unfold prime_int_altdef) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

88 
apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

89 
done 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

90 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

91 
lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

92 
by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat) 
31706  93 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

94 
lemma prime_dvd_mult_int: 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

95 
fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

96 
by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int) 
31706  97 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

98 
lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow> 
31706  99 
p dvd m * n = (p dvd m \<or> p dvd n)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

100 
by (rule iffI, rule prime_dvd_mult_nat, auto) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

101 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

102 
lemma prime_dvd_mult_eq_int [simp]: 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

103 
fixes n::int 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

104 
shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

105 
by (rule iffI, rule prime_dvd_mult_int, auto) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

106 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

107 
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow> 
31706  108 
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" 
109 
unfolding prime_nat_def dvd_def apply auto 

44872  110 
by (metis mult_commute linorder_neq_iff linorder_not_le mult_1 
111 
n_less_n_mult_m one_le_mult_iff less_imp_le_nat) 

27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

112 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

113 
lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x" 
53598
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

114 
by (induct n) auto 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

115 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

116 
lemma prime_dvd_power_int: 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

117 
fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x" 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

118 
by (induct n) auto 
31706  119 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

120 
lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow> 
53598
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

121 
p dvd x^n \<longleftrightarrow> p dvd x" 
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

122 
by (cases n) (auto elim: prime_dvd_power_nat) 
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

123 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

124 
lemma prime_dvd_power_int_iff: 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

125 
fixes x::int 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

126 
shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x" 
53598
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

127 
by (cases n) (auto elim: prime_dvd_power_int) 
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

128 

2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

129 

44872  130 
subsubsection {* Make prime naively executable *} 
32007  131 

132 
lemma zero_not_prime_nat [simp]: "~prime (0::nat)" 

133 
by (simp add: prime_nat_def) 

134 

135 
lemma one_not_prime_nat [simp]: "~prime (1::nat)" 

136 
by (simp add: prime_nat_def) 

137 

138 
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)" 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

139 
by (simp add: prime_nat_def) 
32007  140 

37607  141 
lemma prime_nat_code [code]: 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

142 
"prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" 
44872  143 
apply (simp add: Ball_def) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

144 
apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat) 
44872  145 
done 
32007  146 

147 
lemma prime_nat_simp: 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

148 
"prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)" 
44872  149 
by (auto simp add: prime_nat_code) 
32007  150 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset

151 
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m 
32007  152 

153 
lemma two_is_prime_nat [simp]: "prime (2::nat)" 

44872  154 
by simp 
32007  155 

32111  156 
text{* A bit of regression testing: *} 
157 

44872  158 
lemma "prime(97::nat)" by simp 
159 
lemma "prime(997::nat)" by eval 

32111  160 

32007  161 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

162 
lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

163 
by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

164 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

165 
lemma prime_imp_power_coprime_int: 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

166 
fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

167 
by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

168 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

169 
lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

170 
by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

171 

44872  172 
lemma primes_imp_powers_coprime_nat: 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

173 
"prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

174 
by (rule coprime_exp2_nat, rule primes_coprime_nat) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

175 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

176 
lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n" 
31706  177 
apply (induct n rule: nat_less_induct) 
178 
apply (case_tac "n = 0") 

44872  179 
using two_is_prime_nat 
180 
apply blast 

181 
apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat 

182 
nat_dvd_not_less neq0_conv prime_nat_def) 

183 
done 

23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

184 

31706  185 
text {* One property of coprimality is easier to prove via prime factors. *} 
186 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

187 
lemma prime_divprod_pow_nat: 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

188 
assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b" 
31706  189 
shows "p^n dvd a \<or> p^n dvd b" 
190 
proof 

44872  191 
{ assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis 
31706  192 
apply (cases "n=0", simp_all) 
44872  193 
apply (cases "a=1", simp_all) 
194 
done } 

31706  195 
moreover 
44872  196 
{ assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1" 
197 
then obtain m where m: "n = Suc m" by (cases n) auto 

198 
from n have "p dvd p^n" apply (intro dvd_power) apply auto done 

31706  199 
also note pab 
200 
finally have pab': "p dvd a * b". 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

201 
from prime_dvd_mult_nat[OF p pab'] 
31706  202 
have "p dvd a \<or> p dvd b" . 
203 
moreover 

33946  204 
{ assume pa: "p dvd a" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

205 
from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto 
31706  206 
with p have "coprime b p" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

207 
by (subst gcd_commute_nat, intro prime_imp_coprime_nat) 
44872  208 
then have pnb: "coprime (p^n) b" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

209 
by (subst gcd_commute_nat, rule coprime_exp_nat) 
33946  210 
from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast } 
31706  211 
moreover 
33946  212 
{ assume pb: "p dvd b" 
31706  213 
have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

214 
from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a" 
31706  215 
by auto 
216 
with p have "coprime a p" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

217 
by (subst gcd_commute_nat, intro prime_imp_coprime_nat) 
44872  218 
then have pna: "coprime (p^n) a" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

219 
by (subst gcd_commute_nat, rule coprime_exp_nat) 
33946  220 
from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast } 
44872  221 
ultimately have ?thesis by blast } 
31706  222 
ultimately show ?thesis by blast 
23983  223 
qed 
224 

44872  225 

32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

226 
subsection {* Infinitely many primes *} 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

227 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset

228 
lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1" 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

229 
proof 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

230 
have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

231 
from prime_factor_nat [OF f1] 
44872  232 
obtain p where "prime p" and "p dvd fact n + 1" by auto 
233 
then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done 

234 
{ assume "p \<le> n" 

32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

235 
from `prime p` have "p \<ge> 1" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

236 
by (cases p, simp_all) 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

237 
with `p <= n` have "p dvd fact n" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

238 
by (intro dvd_fact_nat) 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

239 
with `p dvd fact n + 1` have "p dvd fact n + 1  fact n" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

240 
by (rule dvd_diff_nat) 
44872  241 
then have "p dvd 1" by simp 
242 
then have "p <= 1" by auto 

32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

243 
moreover from `prime p` have "p > 1" by auto 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

244 
ultimately have False by auto} 
44872  245 
then have "n < p" by presburger 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

246 
with `prime p` and `p <= fact n + 1` show ?thesis by auto 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

247 
qed 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

248 

8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

249 
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
44872  250 
using next_prime_bound by auto 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

251 

8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

252 
lemma primes_infinite: "\<not> (finite {(p::nat). prime p})" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

253 
proof 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

254 
assume "finite {(p::nat). prime p}" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

255 
with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

256 
by auto 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

257 
then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

258 
by auto 
44872  259 
with bigger_prime [of b] show False 
260 
by auto 

32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

261 
qed 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

262 

55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

263 
subsection{*Powers of Primes*} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

264 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

265 
text{*Versions for type nat only*} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

266 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

267 
lemma prime_product: 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

268 
fixes p::nat 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

269 
assumes "prime (p * q)" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

270 
shows "p = 1 \<or> q = 1" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

271 
proof  
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

272 
from assms have 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

273 
"1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

274 
unfolding prime_nat_def by auto 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

275 
from `1 < p * q` have "p \<noteq> 0" by (cases p) auto 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

276 
then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

277 
have "p dvd p * q" by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

278 
then have "p = 1 \<or> p = p * q" by (rule P) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

279 
then show ?thesis by (simp add: Q) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

280 
qed 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

281 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

282 
lemma prime_exp: 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

283 
fixes p::nat 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

284 
shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

285 
proof(induct n) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

286 
case 0 thus ?case by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

287 
next 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

288 
case (Suc n) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

289 
{assume "p = 0" hence ?case by simp} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

290 
moreover 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

291 
{assume "p=1" hence ?case by simp} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

292 
moreover 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

293 
{assume p: "p \<noteq> 0" "p\<noteq>1" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

294 
{assume pp: "prime (p^Suc n)" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

295 
hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

296 
with p have n: "n = 0" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

297 
by (metis One_nat_def nat_power_eq_Suc_0_iff) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

298 
with pp have "prime p \<and> Suc n = 1" by simp} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

299 
moreover 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

300 
{assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

301 
ultimately have ?case by blast} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

302 
ultimately show ?case by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

303 
qed 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

304 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

305 
lemma prime_power_mult: 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

306 
fixes p::nat 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

307 
assumes p: "prime p" and xy: "x * y = p ^ k" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

308 
shows "\<exists>i j. x = p ^i \<and> y = p^ j" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

309 
using xy 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

310 
proof(induct k arbitrary: x y) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

311 
case 0 thus ?case apply simp by (rule exI[where x="0"], simp) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

312 
next 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

313 
case (Suc k x y) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

314 
from Suc.prems have pxy: "p dvd x*y" by auto 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

315 
from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" . 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

316 
from p have p0: "p \<noteq> 0" by  (rule ccontr, simp) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

317 
{assume px: "p dvd x" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

318 
then obtain d where d: "x = p*d" unfolding dvd_def by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

319 
from Suc.prems d have "p*d*y = p^Suc k" by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

320 
hence th: "d*y = p^k" using p0 by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

321 
from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

322 
with d have "x = p^Suc i" by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

323 
with ij(2) have ?case by blast} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

324 
moreover 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

325 
{assume px: "p dvd y" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

326 
then obtain d where d: "y = p*d" unfolding dvd_def by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

327 
from Suc.prems d have "p*d*x = p^Suc k" by (simp add: mult_commute) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

328 
hence th: "d*x = p^k" using p0 by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

329 
from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

330 
with d have "y = p^Suc i" by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

331 
with ij(2) have ?case by blast} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

332 
ultimately show ?case using pxyc by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

333 
qed 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

334 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

335 
lemma prime_power_exp: 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

336 
fixes p::nat 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

337 
assumes p: "prime p" and n: "n \<noteq> 0" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

338 
and xn: "x^n = p^k" shows "\<exists>i. x = p^i" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

339 
using n xn 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

340 
proof(induct n arbitrary: k) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

341 
case 0 thus ?case by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

342 
next 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

343 
case (Suc n k) hence th: "x*x^n = p^k" by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

344 
{assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

345 
moreover 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

346 
{assume n: "n \<noteq> 0" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

347 
from prime_power_mult[OF p th] 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

348 
obtain i j where ij: "x = p^i" "x^n = p^j"by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

349 
from Suc.hyps[OF n ij(2)] have ?case .} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

350 
ultimately show ?case by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

351 
qed 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

352 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

353 
lemma divides_primepow: 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

354 
fixes p::nat 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

355 
assumes p: "prime p" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

356 
shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

357 
proof 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

358 
assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

359 
unfolding dvd_def apply (auto simp add: mult_commute) by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

360 
from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

361 
from e ij have "p^(i + j) = p^k" by (simp add: power_add) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

362 
hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

363 
hence "i \<le> k" by arith 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

364 
with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

365 
next 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

366 
{fix i assume H: "i \<le> k" "d = p^i" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

367 
then obtain j where j: "k = i + j" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

368 
by (metis le_add_diff_inverse) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

369 
hence "p^k = p^j*d" using H(2) by (simp add: power_add) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

370 
hence "d dvd p^k" unfolding dvd_def by auto} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

371 
thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

372 
qed 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

373 

55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

374 
subsection {*Chinese Remainder Theorem Variants*} 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

375 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

376 
lemma bezout_gcd_nat: 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

377 
fixes a::nat shows "\<exists>x y. a * x  b * y = gcd a b \<or> b * x  a * y = gcd a b" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

378 
using bezout_nat[of a b] 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

379 
by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

380 
gcd_nat.right_neutral mult_0) 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

381 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

382 
lemma gcd_bezout_sum_nat: 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

383 
fixes a::nat 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

384 
assumes "a * x + b * y = d" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

385 
shows "gcd a b dvd d" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

386 
proof 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

387 
let ?g = "gcd a b" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

388 
have dv: "?g dvd a*x" "?g dvd b * y" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

389 
by simp_all 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

390 
from dvd_add[OF dv] assms 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

391 
show ?thesis by auto 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

392 
qed 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

393 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

394 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

395 
text {* A binary form of the Chinese Remainder Theorem. *} 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

396 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

397 
lemma chinese_remainder: 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

398 
fixes a::nat assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

399 
shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

400 
proof 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

401 
from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a] 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

402 
obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

403 
and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

404 
then have d12: "d1 = 1" "d2 =1" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

405 
by (metis ab coprime_nat)+ 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

406 
let ?x = "v * a * x1 + u * b * x2" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

407 
let ?q1 = "v * x1 + u * y2" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

408 
let ?q2 = "v * y1 + u * x2" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

409 
from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

410 
have "?x = u + ?q1 * a" "?x = v + ?q2 * b" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

411 
apply (auto simp add: algebra_simps) 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

412 
apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+ 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

413 
done 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

414 
thus ?thesis by blast 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

415 
qed 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

416 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

417 
text {* Primality *} 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

418 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

419 
lemma coprime_bezout_strong: 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

420 
fixes a::nat assumes "coprime a b" "b \<noteq> 1" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

421 
shows "\<exists>x y. a * x = b * y + 1" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

422 
by (metis assms bezout_nat gcd_nat.left_neutral) 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

423 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

424 
lemma bezout_prime: 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

425 
assumes p: "prime p" and pa: "\<not> p dvd a" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

426 
shows "\<exists>x y. a*x = Suc (p*y)" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

427 
proof 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

428 
have ap: "coprime a p" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

429 
by (metis gcd_nat.commute p pa prime_imp_coprime_nat) 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

430 
from coprime_bezout_strong[OF ap] show ?thesis 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

431 
by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa) 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

432 
qed 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

433 

21256  434 
end 