Theory Primes
section‹The Divides Relation and Euclid's algorithm for the GCD›
theory Primes imports ZF begin
definition
divides :: "[i,i]⇒o" (infixl ‹dvd› 50) where
"m dvd n ≡ m ∈ nat ∧ n ∈ nat ∧ (∃k ∈ nat. n = m#*k)"
definition
is_gcd :: "[i,i,i]⇒o" where
"is_gcd(p,m,n) ≡ ((p dvd m) ∧ (p dvd n)) ∧
(∀d∈nat. (d dvd m) ∧ (d dvd n) ⟶ d dvd p)"
definition
gcd :: "[i,i]⇒i" where
"gcd(m,n) ≡ transrec(natify(n),
λn f. λm ∈ nat.
if n=0 then m else f`(m mod n)`n) ` natify(m)"
definition
coprime :: "[i,i]⇒o" where
"coprime(m,n) ≡ gcd(m,n) = 1"
definition
prime :: i where
"prime ≡ {p ∈ nat. 1<p ∧ (∀m ∈ nat. m dvd p ⟶ m=1 | m=p)}"
subsection‹The Divides Relation›
lemma dvdD: "m dvd n ⟹ m ∈ nat ∧ n ∈ nat ∧ (∃k ∈ nat. n = m#*k)"
by (unfold divides_def, assumption)
lemma dvdE:
"⟦m dvd n; ⋀k. ⟦m ∈ nat; n ∈ nat; k ∈ nat; n = m#*k⟧ ⟹ P⟧ ⟹ P"
by (blast dest!: dvdD)
lemmas dvd_imp_nat1 = dvdD [THEN conjunct1]
lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1]
lemma dvd_0_right [simp]: "m ∈ nat ⟹ m dvd 0"
apply (simp add: divides_def)
apply (fast intro: nat_0I mult_0_right [symmetric])
done
lemma dvd_0_left: "0 dvd m ⟹ m = 0"
by (simp add: divides_def)
lemma dvd_refl [simp]: "m ∈ nat ⟹ m dvd m"
apply (simp add: divides_def)
apply (fast intro: nat_1I mult_1_right [symmetric])
done
lemma dvd_trans: "⟦m dvd n; n dvd p⟧ ⟹ m dvd p"
by (auto simp add: divides_def intro: mult_assoc mult_type)
lemma dvd_anti_sym: "⟦m dvd n; n dvd m⟧ ⟹ m=n"
apply (simp add: divides_def)
apply (force dest: mult_eq_self_implies_10
simp add: mult_assoc mult_eq_1_iff)
done
lemma dvd_mult_left: "⟦(i#*j) dvd k; i ∈ nat⟧ ⟹ i dvd k"
by (auto simp add: divides_def mult_assoc)
lemma dvd_mult_right: "⟦(i#*j) dvd k; j ∈ nat⟧ ⟹ j dvd k"
apply (simp add: divides_def, clarify)
apply (rule_tac x = "i#*ka" in bexI)
apply (simp add: mult_ac)
apply (rule mult_type)
done
subsection‹Euclid's Algorithm for the GCD›
lemma gcd_0 [simp]: "gcd(m,0) = natify(m)"
apply (simp add: gcd_def)
apply (subst transrec, simp)
done
lemma gcd_natify1 [simp]: "gcd(natify(m),n) = gcd(m,n)"
by (simp add: gcd_def)
lemma gcd_natify2 [simp]: "gcd(m, natify(n)) = gcd(m,n)"
by (simp add: gcd_def)
lemma gcd_non_0_raw:
"⟦0<n; n ∈ nat⟧ ⟹ gcd(m,n) = gcd(n, m mod n)"
apply (simp add: gcd_def)
apply (rule_tac P = "λz. left (z) = right" for left right in transrec [THEN ssubst])
apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym]
mod_less_divisor [THEN ltD])
done
lemma gcd_non_0: "0 < natify(n) ⟹ gcd(m,n) = gcd(n, m mod n)"
apply (cut_tac m = m and n = "natify (n) " in gcd_non_0_raw)
apply auto
done
lemma gcd_1 [simp]: "gcd(m,1) = 1"
by (simp (no_asm_simp) add: gcd_non_0)
lemma dvd_add: "⟦k dvd a; k dvd b⟧ ⟹ k dvd (a #+ b)"
apply (simp add: divides_def)
apply (fast intro: add_mult_distrib_left [symmetric] add_type)
done
lemma dvd_mult: "k dvd n ⟹ k dvd (m #* n)"
apply (simp add: divides_def)
apply (fast intro: mult_left_commute mult_type)
done
lemma dvd_mult2: "k dvd m ⟹ k dvd (m #* n)"
apply (subst mult_commute)
apply (blast intro: dvd_mult)
done
lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult]
lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2]
lemma dvd_mod_imp_dvd_raw:
"⟦a ∈ nat; b ∈ nat; k dvd b; k dvd (a mod b)⟧ ⟹ k dvd a"
apply (case_tac "b=0")
apply (simp add: DIVISION_BY_ZERO_MOD)
apply (blast intro: mod_div_equality [THEN subst]
elim: dvdE
intro!: dvd_add dvd_mult mult_type mod_type div_type)
done
lemma dvd_mod_imp_dvd: "⟦k dvd (a mod b); k dvd b; a ∈ nat⟧ ⟹ k dvd a"
apply (cut_tac b = "natify (b)" in dvd_mod_imp_dvd_raw)
apply auto
apply (simp add: divides_def)
done
lemma gcd_induct_lemma [rule_format (no_asm)]: "⟦n ∈ nat;
∀m ∈ nat. P(m,0);
∀m ∈ nat. ∀n ∈ nat. 0<n ⟶ P(n, m mod n) ⟶ P(m,n)⟧
⟹ ∀m ∈ nat. P (m,n)"
apply (erule_tac i = n in complete_induct)
apply (case_tac "x=0")
apply (simp (no_asm_simp))
apply clarify
apply (drule_tac x1 = m and x = x in bspec [THEN bspec])
apply (simp_all add: Ord_0_lt_iff)
apply (blast intro: mod_less_divisor [THEN ltD])
done
lemma gcd_induct: "⋀P. ⟦m ∈ nat; n ∈ nat;
⋀m. m ∈ nat ⟹ P(m,0);
⋀m n. ⟦m ∈ nat; n ∈ nat; 0<n; P(n, m mod n)⟧ ⟹ P(m,n)⟧
⟹ P (m,n)"
by (blast intro: gcd_induct_lemma)
subsection‹Basic Properties of \<^term>‹gcd››
text‹type of gcd›
lemma gcd_type [simp,TC]: "gcd(m, n) ∈ nat"
apply (subgoal_tac "gcd (natify (m), natify (n)) ∈ nat")
apply simp
apply (rule_tac m = "natify (m)" and n = "natify (n)" in gcd_induct)
apply auto
apply (simp add: gcd_non_0)
done
text‹Property 1: gcd(a,b) divides a and b›
lemma gcd_dvd_both:
"⟦m ∈ nat; n ∈ nat⟧ ⟹ gcd (m, n) dvd m ∧ gcd (m, n) dvd n"
apply (rule_tac m = m and n = n in gcd_induct)
apply (simp_all add: gcd_non_0)
apply (blast intro: dvd_mod_imp_dvd_raw nat_into_Ord [THEN Ord_0_lt])
done
lemma gcd_dvd1 [simp]: "m ∈ nat ⟹ gcd(m,n) dvd m"
apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both)
apply auto
done
lemma gcd_dvd2 [simp]: "n ∈ nat ⟹ gcd(m,n) dvd n"
apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both)
apply auto
done
text‹if f divides a and b then f divides gcd(a,b)›
lemma dvd_mod: "⟦f dvd a; f dvd b⟧ ⟹ f dvd (a mod b)"
apply (simp add: divides_def)
apply (case_tac "b=0")
apply (simp add: DIVISION_BY_ZERO_MOD, auto)
apply (blast intro: mod_mult_distrib2 [symmetric])
done
text‹Property 2: for all a,b,f naturals,
if f divides a and f divides b then f divides gcd(a,b)›
lemma gcd_greatest_raw [rule_format]:
"⟦m ∈ nat; n ∈ nat; f ∈ nat⟧
⟹ (f dvd m) ⟶ (f dvd n) ⟶ f dvd gcd(m,n)"
apply (rule_tac m = m and n = n in gcd_induct)
apply (simp_all add: gcd_non_0 dvd_mod)
done
lemma gcd_greatest: "⟦f dvd m; f dvd n; f ∈ nat⟧ ⟹ f dvd gcd(m,n)"
apply (rule gcd_greatest_raw)
apply (auto simp add: divides_def)
done
lemma gcd_greatest_iff [simp]: "⟦k ∈ nat; m ∈ nat; n ∈ nat⟧
⟹ (k dvd gcd (m, n)) ⟷ (k dvd m ∧ k dvd n)"
by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans)
subsection‹The Greatest Common Divisor›
text‹The GCD exists and function gcd computes it.›
lemma is_gcd: "⟦m ∈ nat; n ∈ nat⟧ ⟹ is_gcd(gcd(m,n), m, n)"
by (simp add: is_gcd_def)
text‹The GCD is unique›
lemma is_gcd_unique: "⟦is_gcd(m,a,b); is_gcd(n,a,b); m∈nat; n∈nat⟧ ⟹ m=n"
apply (simp add: is_gcd_def)
apply (blast intro: dvd_anti_sym)
done
lemma is_gcd_commute: "is_gcd(k,m,n) ⟷ is_gcd(k,n,m)"
by (simp add: is_gcd_def, blast)
lemma gcd_commute_raw: "⟦m ∈ nat; n ∈ nat⟧ ⟹ gcd(m,n) = gcd(n,m)"
apply (rule is_gcd_unique)
apply (rule is_gcd)
apply (rule_tac [3] is_gcd_commute [THEN iffD1])
apply (rule_tac [3] is_gcd, auto)
done
lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_commute_raw)
apply auto
done
lemma gcd_assoc_raw: "⟦k ∈ nat; m ∈ nat; n ∈ nat⟧
⟹ gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
apply (rule is_gcd_unique)
apply (rule is_gcd)
apply (simp_all add: is_gcd_def)
apply (blast intro: gcd_dvd1 gcd_dvd2 gcd_type intro: dvd_trans)
done
lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) "
in gcd_assoc_raw)
apply auto
done
lemma gcd_0_left [simp]: "gcd (0, m) = natify(m)"
by (simp add: gcd_commute [of 0])
lemma gcd_1_left [simp]: "gcd (1, m) = 1"
by (simp add: gcd_commute [of 1])
subsection‹Addition laws›
lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)"
apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))")
apply simp
apply (case_tac "natify (n) = 0")
apply (auto simp add: Ord_0_lt_iff gcd_non_0)
done
lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)"
apply (rule gcd_commute [THEN trans])
apply (subst add_commute, simp)
apply (rule gcd_commute)
done
lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)"
by (subst add_commute, rule gcd_add2)
lemma gcd_add_mult_raw: "k ∈ nat ⟹ gcd (m, k #* m #+ n) = gcd (m, n)"
apply (erule nat_induct)
apply (auto simp add: gcd_add2 add_assoc)
done
lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)"
apply (cut_tac k = "natify (k)" in gcd_add_mult_raw)
apply auto
done
subsection‹Multiplication Laws›
lemma gcd_mult_distrib2_raw:
"⟦k ∈ nat; m ∈ nat; n ∈ nat⟧
⟹ k #* gcd (m, n) = gcd (k #* m, k #* n)"
apply (erule_tac m = m and n = n in gcd_induct, assumption)
apply simp
apply (case_tac "k = 0", simp)
apply (simp add: mod_geq gcd_non_0 mod_mult_distrib2 Ord_0_lt_iff)
done
lemma gcd_mult_distrib2: "k #* gcd (m, n) = gcd (k #* m, k #* n)"
apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) "
in gcd_mult_distrib2_raw)
apply auto
done
lemma gcd_mult [simp]: "gcd (k, k #* n) = natify(k)"
by (cut_tac k = k and m = 1 and n = n in gcd_mult_distrib2, auto)
lemma gcd_self [simp]: "gcd (k, k) = natify(k)"
by (cut_tac k = k and n = 1 in gcd_mult, auto)
lemma relprime_dvd_mult:
"⟦gcd (k,n) = 1; k dvd (m #* n); m ∈ nat⟧ ⟹ k dvd m"
apply (cut_tac k = m and m = k and n = n in gcd_mult_distrib2, auto)
apply (erule_tac b = m in ssubst)
apply (simp add: dvd_imp_nat1)
done
lemma relprime_dvd_mult_iff:
"⟦gcd (k,n) = 1; m ∈ nat⟧ ⟹ k dvd (m #* n) ⟷ k dvd m"
by (blast intro: dvdI2 relprime_dvd_mult dvd_trans)
lemma prime_imp_relprime:
"⟦p ∈ prime; ¬ (p dvd n); n ∈ nat⟧ ⟹ gcd (p, n) = 1"
apply (simp add: prime_def, clarify)
apply (drule_tac x = "gcd (p,n)" in bspec)
apply auto
apply (cut_tac m = p and n = n in gcd_dvd2, auto)
done
lemma prime_into_nat: "p ∈ prime ⟹ p ∈ nat"
by (simp add: prime_def)
lemma prime_nonzero: "p ∈ prime ⟹ p≠0"
by (auto simp add: prime_def)
text‹This theorem leads immediately to a proof of the uniqueness of
factorization. If \<^term>‹p› divides a product of primes then it is
one of those primes.›
lemma prime_dvd_mult:
"⟦p dvd m #* n; p ∈ prime; m ∈ nat; n ∈ nat⟧ ⟹ p dvd m ∨ p dvd n"
by (blast intro: relprime_dvd_mult prime_imp_relprime prime_into_nat)
lemma gcd_mult_cancel_raw:
"⟦gcd (k,n) = 1; m ∈ nat; n ∈ nat⟧ ⟹ gcd (k #* m, n) = gcd (m, n)"
apply (rule dvd_anti_sym)
apply (rule gcd_greatest)
apply (rule relprime_dvd_mult [of _ k])
apply (simp add: gcd_assoc)
apply (simp add: gcd_commute)
apply (simp_all add: mult_commute)
apply (blast intro: dvdI1 gcd_dvd1 dvd_trans)
done
lemma gcd_mult_cancel: "gcd (k,n) = 1 ⟹ gcd (k #* m, n) = gcd (m, n)"
apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_mult_cancel_raw)
apply auto
done
subsection‹The Square Root of a Prime is Irrational: Key Lemma›
lemma prime_dvd_other_side:
"⟦n#*n = p#*(k#*k); p ∈ prime; n ∈ nat⟧ ⟹ p dvd n"
apply (subgoal_tac "p dvd n#*n")
apply (blast dest: prime_dvd_mult)
apply (rule_tac j = "k#*k" in dvd_mult_left)
apply (auto simp add: prime_def)
done
lemma reduction:
"⟦k#*k = p#*(j#*j); p ∈ prime; 0 < k; j ∈ nat; k ∈ nat⟧
⟹ k < p#*j ∧ 0 < j"
apply (rule ccontr)
apply (simp add: not_lt_iff_le prime_into_nat)
apply (erule disjE)
apply (frule mult_le_mono, assumption+)
apply (simp add: mult_ac)
apply (auto dest!: natify_eqE
simp add: not_lt_iff_le prime_into_nat mult_le_cancel_le1)
apply (simp add: prime_def)
apply (blast dest: lt_trans1)
done
lemma rearrange: "j #* (p#*j) = k#*k ⟹ k#*k = p#*(j#*j)"
by (simp add: mult_ac)
lemma prime_not_square:
"⟦m ∈ nat; p ∈ prime⟧ ⟹ ∀k ∈ nat. 0<k ⟶ m#*m ≠ p#*(k#*k)"
apply (erule complete_induct, clarify)
apply (frule prime_dvd_other_side, assumption)
apply assumption
apply (erule dvdE)
apply (simp add: mult_assoc mult_cancel1 prime_nonzero prime_into_nat)
apply (blast dest: rearrange reduction ltD)
done
end