author  haftmann 
Sun, 09 Nov 2014 10:03:18 +0100  
changeset 58954  18750e86d5b8 
parent 58898  1ebf0a1f12a4 
child 59667  651ea265d568 
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 

58623  11 
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced 
31706  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 

58889  28 
section {* 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 

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

34 
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

35 
declare [[coercion_enabled]] 
31706  36 

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

37 
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

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

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

40 
lemmas prime_nat_def = prime_def 
31798  41 

21256  42 

32479  43 
subsection {* Primes *} 
31706  44 

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

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

54228  48 
done 
31706  49 

31992  50 
(* 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

51 

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

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

54 

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

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

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

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

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

61 
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

62 
unfolding prime_nat_def by auto 
31706  63 

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

64 
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

65 
unfolding prime_nat_def by auto 
31706  66 

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

67 
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

68 
unfolding prime_nat_def by auto 
31706  69 

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

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

72 
apply (metis gcd_dvd1_nat gcd_dvd2_nat) 
31706  73 
done 
74 

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

75 
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

76 
"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

77 
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

78 
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

79 
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

80 
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

81 
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

82 
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

83 

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 
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

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

87 
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

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

89 

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

90 
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

91 
by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat) 
31706  92 

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

93 
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

94 
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

95 
by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int) 
31706  96 

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

97 
lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow> 
31706  98 
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

99 
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

100 

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

101 
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

102 
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

103 
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

104 
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

105 

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

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55337
diff
changeset

109 
by (metis mult.commute linorder_neq_iff linorder_not_le mult_1 
44872  110 
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

111 

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

112 
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

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

114 

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

115 
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

116 
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

117 
by (induct n) auto 
31706  118 

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

119 
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

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

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

122 

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

123 
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

124 
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

125 
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

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

127 

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

128 

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

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

132 
by (simp add: prime_nat_def) 

133 

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

135 
by (simp add: prime_nat_def) 

136 

137 
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

138 
by (simp add: prime_nat_def) 
32007  139 

37607  140 
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

141 
"prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" 
44872  142 
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

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

146 
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

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

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

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

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

44872  153 
by simp 
32007  154 

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

58954
18750e86d5b8
reverted 1ebf0a1f12a4 after successful retuning of simp rules for divisibility
haftmann
parents:
58898
diff
changeset

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

32007  160 

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

161 
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

162 
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

163 

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

164 
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

165 
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

166 
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

167 

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

168 
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

169 
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

170 

44872  171 
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

172 
"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

173 
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

174 

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

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

44872  178 
using two_is_prime_nat 
179 
apply blast 

180 
apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat 

181 
nat_dvd_not_less neq0_conv prime_nat_def) 

182 
done 

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

183 

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

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

186 
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

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

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

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

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

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

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

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

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

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

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

208 
by (subst gcd_commute_nat, rule coprime_exp_nat) 
33946  209 
from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast } 
31706  210 
moreover 
33946  211 
{ assume pb: "p dvd b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55337
diff
changeset

212 
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

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

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

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

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

44872  224 

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

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

226 

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

227 
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

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

229 
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

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

233 
{ assume "p \<le> n" 

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

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

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

236 
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

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

238 
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

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

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

242 
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

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

245 
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

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

247 

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

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

250 

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

251 
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

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

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

254 
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

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

256 
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

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

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

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

261 

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

262 
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

263 

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

264 
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

265 

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

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

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

268 
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

269 
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

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

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

272 
"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

273 
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

274 
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

275 
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

276 
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

277 
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

278 
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

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

280 

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

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

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

283 
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

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

285 
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

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

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

288 
{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

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

290 
{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

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

292 
{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

293 
{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

294 
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

295 
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

296 
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

297 
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

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

299 
{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

300 
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

301 
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

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

303 

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

304 
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

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

306 
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

307 
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

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

309 
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

310 
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

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

312 
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

313 
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

314 
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

315 
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

316 
{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

317 
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

318 
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

319 
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

320 
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

321 
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

322 
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

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

324 
{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

325 
then obtain d where d: "y = p*d" unfolding dvd_def by blast 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55337
diff
changeset

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

327 
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

328 
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

329 
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

330 
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

331 
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

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

333 

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

334 
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

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

336 
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

337 
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

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

339 
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

340 
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

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

342 
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

343 
{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

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

345 
{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

346 
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

347 
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

348 
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

349 
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

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

351 

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

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

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

354 
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

355 
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

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

357 
assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55337
diff
changeset

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

359 
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

360 
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

361 
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

362 
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

363 
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

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

365 
{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

366 
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

367 
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

368 
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

369 
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

370 
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

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

372 

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

373 
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

374 

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

375 
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

376 
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

377 
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

378 
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

379 
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

380 

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

381 
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

382 
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

383 
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

384 
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

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

386 
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

387 
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

388 
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

389 
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

390 
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

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

392 

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 
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

395 

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

396 
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

397 
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

398 
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

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

400 
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

401 
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

402 
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

403 
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

404 
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

405 
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

406 
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

407 
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

408 
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

409 
have "?x = u + ?q1 * a" "?x = v + ?q2 * b" 
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

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

411 
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

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

413 

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

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

415 

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

416 
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

417 
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

418 
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

419 
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

420 

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

421 
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

422 
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

423 
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

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

425 
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

426 
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

427 
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

428 
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

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

430 

21256  431 
end 