Up to index of Isabelle/HOL/Fermat3_4
theory QuadForm(* Title: QuadForm.thy
Author: Roelof Oosterhuis
2007 Rijksuniversiteit Groningen
*)
header {* The quadratic form $x^2 + Ny^2$ *}
theory QuadForm
imports
"~~/src/HOL/NumberTheory/Quadratic_Reciprocity"
IntNatAux InfDesc
begin
text {* Shows some properties of the quadratic form $x^2+Ny^2$, such as how to multiply and divide them. The second part focuses on the case $N=3$ and is used in the proof of the case $n=3$ of Fermat's last theorem. The last part -- not used for FLT3 -- shows which primes can be written as $x^2 + 3y^2$. *}
subsection {* Definitions and auxiliary results *}
constdefs
is_qfN :: "int => int => bool"
"is_qfN A N == ∃ x y. A = x^2 + N*y^2"
is_cube_form :: "int => int => bool"
"is_cube_form a b == ∃ p q. a = p^3 - 9*p*q^2 ∧ b = 3*p^2*q - 3*q^3"
lemma abs_eq_impl_unitfactor: "¦a::int¦ = ¦b¦ ==> ∃ u. a = u*b ∧ ¦u¦=1"
proof -
assume "¦a¦ = ¦b¦"
hence "a = 1*b ∨ a = (-1)*b" by arith
then obtain u where "a = u*b ∧ (u=1 ∨ u=-1)" by blast
thus ?thesis by auto
qed
lemma zprime_3: "zprime 3"
proof (auto simp add: zprime_def)
fix m::int assume m0: "m ≥ 0" and mdvd3: "m dvd 3" and mn3: "m ≠ 3"
hence "m ≤ 3" by (auto simp only: zdvd_imp_le)
with mn3 have "m < 3" by simp
moreover from mdvd3 have "m ≠ 0" by auto
moreover with m0 have "m > 0" by simp
ultimately have "m = 1 ∨ m = 2" by auto
moreover from mdvd3 have "m = 2 ==> False" by arith
ultimately show "m = 1" by auto
qed
(*lemma zgcd_not_1_impl_common_primedivisor:
"zgcd(a,b) ≠ 1 ==> ∃ p. zprime p ∧ p dvd a ∧ p dvd b"
by (auto simp add: zgcd1_iff_no_common_primedivisor)
*)
subsection {* Basic facts if $N \ge 1$ *}
lemma qfN_pos: "[| N ≥ 1; is_qfN A N |] ==> A ≥ 0"
proof -
assume N: "N ≥ 1" and "is_qfN A N"
then obtain a b where ab: "A = a^2 + N*b^2" by (auto simp add: is_qfN_def)
have "N*b^2 ≥ 0"
proof (cases)
assume "b = 0" thus ?thesis by auto
next
assume "¬ b = 0" hence " b^2 > 0" by (simp add: zero_less_power2)
moreover from N have "N>0" by simp
ultimately have "N*b^2 > N*0" by (auto simp only: zmult_zless_mono2)
thus ?thesis by auto
qed
with ab have "A ≥ a^2" by auto
moreover have "a^2 ≥ 0" by (rule zero_le_power2)
ultimately show ?thesis by arith
qed
lemma qfN_zero: "[| (N::int) ≥ 1; a^2 + N*b^2 = 0 |] ==> (a = 0 ∧ b = 0)"
proof -
assume N: "N ≥ 1" and abN: "a^2 + N*b^2 = 0"
show ?thesis
proof (rule ccontr, auto)
assume "a ≠ 0" hence "a^2 > 0" by (simp add: zero_less_power2)
moreover have "N*b^2 ≥ 0"
proof (cases)
assume "b = 0" thus ?thesis by auto
next
assume "¬ b = 0" hence " b^2 > 0" by (simp add: zero_less_power2)
moreover from N have "N>0" by simp
ultimately have "N*b^2 > N*0" by (auto simp only: zmult_zless_mono2)
thus ?thesis by auto
qed
ultimately have "a^2 + N*b^2 > 0" by arith
with abN show False by auto
next
assume "b ≠ 0" hence "b^2>0" by (simp add: zero_less_power2)
moreover from N have "N>0" by simp
ultimately have "N*b^2>N*0" by (auto simp only: zmult_zless_mono2)
hence "N*b^2 > 0" by simp
moreover have "a^2 ≥ 0" by (rule zero_le_power2)
ultimately have "a^2 + N*b^2 > 0" by arith
with abN show False by auto
qed
qed
subsection {* Multiplication and division *}
lemma qfN_mult1: "((a::int)^2 + N*b^2)*(c^2 + N*d^2)
= (a*c+N*b*d)^2 + N*(a*d-b*c)^2"
by (simp add: nat_number ring_simps)
lemma qfN_mult2: "((a::int)^2 + N*b^2)*(c^2 + N*d^2)
= (a*c-N*b*d)^2 + N*(a*d+b*c)^2"
by (simp add: nat_number ring_simps)
corollary is_qfN_mult: "is_qfN A N ==> is_qfN B N ==> is_qfN (A*B) N"
by (unfold is_qfN_def, auto, auto simp only: qfN_mult1)
corollary is_qfN_power: "(n::nat) > 0 ==> is_qfN A N ==> is_qfN (A^n) N"
by (induct n, auto, case_tac "n=0", auto simp add: is_qfN_mult)
lemma qfN_div_prime:
assumes ass: "zprime (p^2+N*q^2) ∧ (p^2+N*q^2) dvd (a^2+N*b^2)"
shows "∃ u v. a^2+N*b^2 = (u^2+N*v^2)*(p^2+N*q^2)
∧ (∃ e. a = p*u+e*N*q*v ∧ b = p*v - e*q*u ∧ ¦e¦=1)"
proof -
let ?P = "p^2+N*q^2"
let ?A = "a^2+N*b^2"
from ass obtain U where U: "?A = ?P*U" by (auto simp only: dvd_def)
have "∃ e. ?P dvd b*p + e*a*q ∧ ¦e¦ = 1"
proof -
have "?P dvd (b*p + a*q)*(b*p - a*q)"
proof -
have "(b*p + a*q)*(b*p - a*q)= b^2*?P - q^2*?A"
by (simp add: nat_number ring_simps)
also from U have "… = (b^2 - q^2*U)*?P" by (simp add: ring_simps)
finally show ?thesis by simp
qed
with ass have "?P dvd (b*p + a*q) ∨ ?P dvd (b*p - a*q)"
by (simp only: zprime_zdvd_zmult_general)
moreover
{ assume "?P dvd b*p + a*q"
hence "?P dvd b*p + 1*a*q ∧ ¦1¦ = (1::int)" by simp }
moreover
{ assume "?P dvd b*p - a*q"
hence "?P dvd b*p + (-1)*a*q ∧ ¦-1¦ = (1::int)" by simp }
ultimately show ?thesis by blast
qed
then obtain v e where v: "b*p + e*a*q = ?P*v" and e: "¦e¦ = 1"
by (auto simp only: dvd_def)
have "?P dvd a*p - e*N*b*q"
proof (cases)
assume e1: "e = 1"
from U have "U * ?P^2 = ?A * ?P" by (simp add: power2_eq_square)
also with e1 have "… = (a*p-e*N*b*q)^2 + N*(b*p+e*a*q)^2"
by (simp only: qfN_mult2 add_commute zmult_1)
also with v have "… = (a*p-e*N*b*q)^2 + N*v^2*?P^2"
by (simp only: power_mult_distrib mult_ac)
finally have "(a*p-e*N*b*q)^2 = ?P^2*(U-N*v^2)"
by (simp add: mult_ac zdiff_zmult_distrib)
hence "?P^2 dvd (a*p - e*N*b*q)^2" by (rule dvdI)
thus ?thesis by (simp only: zpower_zdvd_mono)
next
assume "¬ e=1" with e have e1: "e=-1" by auto
from U have "U * ?P^2 = ?A * ?P" by (simp add: power2_eq_square)
also with e1 have "… = (a*p-e*N*b*q)^2 + N*( -(b*p+e*a*q))^2"
by (simp add: qfN_mult1)
also have "… = (a*p-e*N*b*q)^2 + N*(b*p+e*a*q)^2"
by (simp only: power2_minus)
also with v have "… = (a*p-e*N*b*q)^2 + N*v^2*?P^2"
by (simp only: power_mult_distrib mult_ac)
finally have "(a*p-e*N*b*q)^2 = ?P^2*(U-N*v^2)"
by (simp add: mult_ac zdiff_zmult_distrib)
hence "?P^2 dvd (a*p-e*N*b*q)^2" by (rule dvdI)
thus ?thesis by (simp only: zpower_zdvd_mono)
qed
then obtain u where u: "a*p - e*N*b*q = ?P*u" by (auto simp only: dvd_def)
from e have e2_1: "e*e = 1" by auto
have a: "a = p*u + e*N*q*v"
proof -
have "(p*u + e*N*q*v)*?P = p*(?P*u) + (e*N*q)*(?P*v)"
by (simp only: zadd_zmult_distrib mult_ac)
also with v u have "… = p*(a*p - e*N*b*q) + (e*N*q)*(b*p + e*a*q)"
by simp
also have "… = a*(p^2 + e*e*N*q^2)"
by (simp add: power2_eq_square zadd_zmult_distrib2 mult_ac zdiff_zmult_distrib2)
also with e2_1 have "… = a*?P" by simp
finally have "(a-(p*u+e*N*q*v))*?P = 0" by auto
moreover from ass have "?P ≠ 0" by (unfold zprime_def, auto)
ultimately show ?thesis by simp
qed
moreover have b: "b = p*v-e*q*u"
proof -
have "(p*v-e*q*u)*?P = p*(?P*v) - (e*q)*(?P*u)"
by (simp only: zdiff_zmult_distrib mult_ac)
also with v u have "… = p*(b*p+e*a*q) - e*q*(a*p-e*N*b*q)" by simp
also have "… = b*(p^2 + e*e*N*q^2)"
by (simp add: power2_eq_square zadd_zmult_distrib2 mult_ac zdiff_zmult_distrib2)
also with e2_1 have "… = b * ?P" by simp
finally have "(b-(p*v-e*q*u))*?P = 0" by auto
moreover from ass have "?P ≠ 0" by (unfold zprime_def, auto)
ultimately show ?thesis by simp
qed
moreover have "?A = (u^2 + N*v^2)*?P"
proof (cases)
assume "e=1"
with a and b show ?thesis by (simp add: qfN_mult1 zmult_1 mult_ac)
next
assume "¬ e=1" with e have "e=-1" by simp
with a and b show ?thesis by (simp add: qfN_mult2 zmult_1 mult_ac)
qed
moreover from e have "¦e¦ = 1" ..
ultimately show ?thesis by blast
qed
corollary qfN_div_prime_weak:
"[| zprime (p^2+N*q^2); (p^2+N*q^2) dvd (a^2+N*b^2) |]
==> ∃ u v. a^2+N*b^2 = (u^2+N*v^2)*(p^2+N*q^2)"
apply (subgoal_tac "∃ u v. a^2+N*b^2 = (u^2+N*v^2)*(p^2+N*q^2)
∧ (∃ e. a = p*u+e*N*q*v ∧ b = p*v - e*q*u ∧ ¦e¦=1)", blast)
apply (rule qfN_div_prime, auto)
done
corollary qfN_div_prime_general: "[| zprime P; P dvd A; is_qfN A N; is_qfN P N |]
==> ∃ Q. A = Q*P ∧ is_qfN Q N"
apply (subgoal_tac "∃ u v. A = (u^2+N*v^2)*P")
apply (unfold is_qfN_def, auto)
apply (simp only: qfN_div_prime_weak)
done
lemma qfN_power_div_prime:
assumes ass: "zprime P ∧ P ∈ zOdd ∧ P dvd A ∧ P^n = p^2+N*q^2
∧ A^n = a^2+N*b^2 ∧ zgcd(a,b)=1 ∧ zgcd(p,N*q)=1 ∧ n>0"
shows "∃ u v. a^2+N*b^2 = (u^2 + N*v^2)*(p^2+N*q^2) ∧ zgcd(u,v)=1
∧ (∃ e. a = p*u+e*N*q*v ∧ b = p*v-e*q*u ∧ ¦e¦ = 1)"
proof -
from ass have "P dvd A ∧ n>0" by simp
hence "P^n dvd A^n" by (simp add: zpower_zdvd_mono)
then obtain U where U: "A^n = U*P^n" by (auto simp only: dvd_def mult_ac)
have "∃ e. P^n dvd b*p + e*a*q ∧ ¦e¦ = 1"
proof -
have Pn_dvd_prod: "P^n dvd (b*p + a*q)*(b*p - a*q)"
proof -
have "(b*p + a*q)*(b*p - a*q) = (b*p)^2 - (a*q)^2" by (rule zspecial_product)
also have "… = b^2 * p^2 + b^2*N*q^2 - b^2*N*q^2 - a^2*q^2"
by (simp add: power_mult_distrib)
also with ass have "… = b^2*P^n - q^2*A^n"
by (simp only: mult_ac zadd_zmult_distrib zadd_zmult_distrib2)
also with U have "… = (b^2-q^2*U)*P^n" by (simp only: zdiff_zmult_distrib)
finally show ?thesis by (simp add: mult_ac)
qed
have "P^n dvd (b*p + a*q) ∨ P^n dvd (b*p - a*q)"
proof -
have PdvdPn: "P dvd P^n"
proof -
from ass have "∃ m. n = Suc m" by (simp add: not0_implies_Suc)
then obtain m where "n = Suc m" by auto
hence "P^n = P*(P^m)" by auto
thus ?thesis by auto
qed
have "¬ P dvd b*p+a*q ∨ ¬ P dvd b*p-a*q"
proof (rule ccontr, simp)
assume "P dvd b*p+a*q ∧ P dvd b*p-a*q"
hence "P dvd (b*p+a*q)+(b*p-a*q) ∧ P dvd (b*p+a*q)-(b*p-a*q)"
by (simp only: zdvd_zadd, simp only: zdvd_zdiff)
hence "P dvd 2*(b*p) ∧ P dvd 2*(a*q)" by (simp only: mult_2, auto)
with ass have "(P dvd 2 ∨ P dvd b*p) ∧ (P dvd 2 ∨ P dvd a*q)"
by (simp add: zprime_zdvd_zmult_general)
hence "P dvd 2 ∨ (P dvd b*p ∧ P dvd a*q)" by auto
moreover have "¬ P dvd 2"
proof (rule ccontr, simp)
assume pdvd2: "P dvd 2"
have "P ≤ 2"
proof (rule ccontr)
assume "¬ P ≤ 2" hence Pl2: "P > 2" by simp
with pdvd2 show False by (simp add: zdvd_not_zless)
qed
moreover from ass have "P > 1" by (simp only: zprime_def)
ultimately have "P=2" by auto
with ass have "2 ∈ zOdd" by simp
moreover have "2 ∈ zEven" by (simp add: zEven_def)
ultimately show False by (simp add: odd_iff_not_even)
qed
ultimately have "P dvd b*p ∧ P dvd a*q" by auto
with ass have "(P dvd b ∨ P dvd p) ∧ (P dvd a ∨ P dvd q)"
by (auto simp only: zprime_zdvd_zmult_general)
moreover have "¬ P dvd p ∧ ¬ P dvd q"
proof (auto dest: ccontr)
assume Pdvdp: "P dvd p"
hence "P dvd p^2" by (simp only: zdvd_zmult power2_eq_square)
with PdvdPn have "P dvd P^n-p^2" by (simp only: zdvd_zdiff)
with ass have "P dvd N*(q*q)" by (simp add: power2_eq_square)
with ass have "P dvd N ∨ P dvd q" by (auto dest: zprime_zdvd_zmult_general)
hence "P dvd N*q" by (auto simp add: zdvd_zmult zdvd_zmult2)
with Pdvdp have "P dvd zgcd(p,N*q)" by (simp add: zgcd_greatest_iff)
with ass show False by (auto simp add: zprime_def)
next
assume "P dvd q"
hence PdvdNq: "P dvd N*q" by (simp add: zdvd_zmult)
hence "P dvd N*q*q" by (simp add: zdvd_zmult2)
hence "P dvd N*q^2" by (simp add: power2_eq_square mult_ac)
with PdvdPn have "P dvd P^n-N*q^2" by (simp only: zdvd_zdiff)
with ass have "P dvd p*p" by (simp add: power2_eq_square)
with ass have "P dvd p" by (auto dest: zprime_zdvd_zmult_general)
with PdvdNq have "P dvd zgcd(p,N*q)" by (simp add: zgcd_greatest_iff)
with ass show False by (auto simp add: zprime_def)
qed
ultimately have "P dvd a ∧ P dvd b" by auto
hence "P dvd zgcd(a,b)" by (simp add: zgcd_greatest_iff)
with ass show False by (auto simp add: zprime_def)
qed
moreover
{ assume "¬ P dvd b*p+a*q"
with Pn_dvd_prod and ass have "P^n dvd b*p-a*q"
by (rule_tac a="b*p+a*q" in zprime_power_zdvd_cancel_left, simp) }
moreover
{ assume "¬ P dvd b*p-a*q"
with Pn_dvd_prod and ass have "P^n dvd b*p+a*q"
by (rule_tac a="b*p+a*q" in zprime_power_zdvd_cancel_right, simp) }
ultimately show ?thesis by auto
qed
moreover
{ assume "P^n dvd b*p + a*q"
hence "P^n dvd b*p + 1*a*q ∧ ¦1¦ = (1::int)" by simp }
moreover
{ assume "P^n dvd b*p - a*q"
hence "P^n dvd b*p + (-1)*a*q ∧ ¦-1¦ = (1::int)" by simp }
ultimately show ?thesis by blast
qed
then obtain v e where v: "b*p + e*a*q = P^n*v" and e: "¦e¦ = 1"
by (auto simp only: dvd_def)
have "P^n dvd a*p - e*N*b*q"
proof (cases)
assume e1: "e = 1"
from U have "(P^n)^2*U = A^n*P^n" by (simp add: power2_eq_square mult_ac)
also with e1 ass have "… = (a*p-e*N*b*q)^2 + N*(b*p+e*a*q)^2"
by (simp only: qfN_mult2 add_commute zmult_1)
also with v have "… = (a*p-e*N*b*q)^2 + (P^n)^2*(N*v^2)"
by (simp only: power_mult_distrib mult_ac)
finally have "(a*p-e*N*b*q)^2 = (P^n)^2*U - (P^n)^2*N*v^2" by simp
also have "… = (P^n)^2 * (U - N*v^2)" by (simp only: zdiff_zmult_distrib2)
finally have "(P^n)^2 dvd (a*p - e*N*b*q)^2" by (rule dvdI)
thus ?thesis by (simp only: zpower_zdvd_mono)
next
assume "¬ e=1" with e have e1: "e=-1" by auto
from U have "(P^n)^2 * U = A^n * P^n" by (simp add: power2_eq_square)
also with e1 ass have "… = (a*p-e*N*b*q)^2 + N*( -(b*p+e*a*q))^2"
by (simp add: qfN_mult1)
also have "… = (a*p-e*N*b*q)^2 + N*(b*p+e*a*q)^2"
by (simp only: power2_minus)
also with v and ass have "… = (a*p-e*N*b*q)^2 + N*v^2*(P^n)^2"
by (simp only: power_mult_distrib mult_ac)
finally have "(a*p-e*N*b*q)^2 = (P^n)^2*U-(P^n)^2*N*v^2" by simp
also have "… = (P^n)^2 * (U - N*v^2)" by (simp only: zdiff_zmult_distrib2)
finally have "(P^n)^2 dvd (a*p-e*N*b*q)^2" by (rule dvdI)
thus ?thesis by (simp only: zpower_zdvd_mono)
qed
then obtain u where u: "a*p - e*N*b*q = P^n*u" by (auto simp only: dvd_def)
from e have e2_1: "e*e = 1" by auto
have a: "a = p*u + e*N*q*v"
proof -
from ass have "(p*u + e*N*q*v)*P^n = p*(P^n*u) + (e*N*q)*(P^n*v)"
by (simp only: zadd_zmult_distrib mult_ac)
also with v and u have "… = p*(a*p - e*N*b*q) + (e*N*q)*(b*p + e*a*q)"
by simp
also have "… = a*(p^2 + e*e*N*q^2)"
by (simp add: power2_eq_square zadd_zmult_distrib2 mult_ac zdiff_zmult_distrib2)
also with e2_1 and ass have "… = a*P^n" by simp
finally have "(a-(p*u+e*N*q*v))*P^n = 0" by auto
moreover from ass have "P^n ≠ 0"
by (unfold zprime_def, auto simp add: power_eq_0_iff)
ultimately show ?thesis by auto
qed
moreover have b: "b = p*v-e*q*u"
proof -
from ass have "(p*v-e*q*u)*P^n = p*(P^n*v) - (e*q)*(P^n*u)"
by (simp only: zdiff_zmult_distrib mult_ac)
also with v u have "… = p*(b*p+e*a*q) - e*q*(a*p-e*N*b*q)" by simp
also have "… = b*(p^2 + e*e*N*q^2)"
by (simp add: power2_eq_square zadd_zmult_distrib2 mult_ac zdiff_zmult_distrib2)
also with e2_1 and ass have "… = b * P^n" by simp
finally have "(b-(p*v-e*q*u))*P^n = 0" by auto
moreover from ass have "P^n ≠ 0"
by (unfold zprime_def, auto simp add: power_eq_0_iff)
ultimately show ?thesis by auto
qed
moreover have "A^n = (u^2 + N*v^2)*P^n"
proof (cases)
assume "e=1"
with a and b and ass show ?thesis by (simp add: qfN_mult1 zmult_1 mult_ac)
next
assume "¬ e=1" with e have "e=-1" by simp
with a and b and ass show ?thesis by (simp add: qfN_mult2 zmult_1 mult_ac)
qed
moreover have "zgcd(u,v)=1"
proof -
let ?g = "zgcd(u,v)"
have "?g dvd u ∧ ?g dvd v" by auto
hence "?g dvd u*p + v*(e*N*q) ∧ ?g dvd v*p - u*(e*q)"
by (simp add: zdvd_zmult2 zdvd_zadd zdvd_zdiff)
with a and b have "?g dvd a ∧ ?g dvd b" by (auto simp only: mult_ac)
hence "?g dvd zgcd(a,b)" by (simp add: zgcd_greatest_iff)
with ass have "?g = 1 ∨ ?g = -1" by simp
moreover have "?g ≥ 0" by (rule zgcd_geq_zero)
ultimately show ?thesis by auto
qed
moreover from e and ass have
"¦e¦ = 1 ∧ A^n = a^2+N*b^2 ∧ P^n = p^2+N*q^2" by simp
ultimately show ?thesis by auto
qed
lemma qfN_primedivisor_not:
assumes ass: "zprime P ∧ Q > 0 ∧ is_qfN (P*Q) N ∧ ¬ is_qfN P N"
shows "∃ R. (zprime R ∧ R dvd Q ∧ ¬ is_qfN R N)"
proof (rule ccontr, auto)
assume ass2: "∀ R. R dvd Q --> zprime R --> is_qfN R N"
have "∃ ps. primel ps ∧ int (prod ps) = Q"
proof -
from ass have "Q=1 ∨ nat(Q) > Suc 0" by auto
moreover
{ assume "Q=1" hence "primel [] ∧ int (prod []) = Q" by (simp add: primel_def)
hence ?thesis by auto }
moreover
{ assume "nat(Q) > Suc 0"
then have "∃ ps. primel ps ∧ prod ps = nat(Q)" by (simp only: factor_exists)
with ass have ?thesis by auto }
ultimately show ?thesis by blast
qed
then obtain ps where ps: "primel ps ∧ int(prod ps) = Q" by auto
have ps_lemma: "(primel ps ∧ is_qfN (P*int(prod ps)) N
∧ (∀R. (zprime R ∧ R dvd int(prod ps)) --> is_qfN R N)) ==> False"
(is "?B ps ==> False")
proof (induct ps)
case Nil hence "is_qfN P N" by simp
with ass show False by simp
next
case (Cons p ps)
hence ass3: "?B ps ==> False"
and IH: "?B (p#ps)" by simp
hence p: "zprime (int p)" and "int p dvd int(prod(p#ps))"
by (auto simp add: primel_def prime_impl_zprime_int int_mult)
moreover with IH have pqfN: "is_qfN (int p) N"
and "int p dvd P*int(prod(p#ps))" and "is_qfN (P*int(prod(p#ps))) N"
by (auto simp add: zdvd_zmult)
ultimately obtain S where S: "P*int(prod(p#ps)) = S*(int p) ∧ is_qfN S N"
by (auto dest: qfN_div_prime_general)
hence "(int p)*(P* int(prod ps) - S) = 0" by (auto simp add: int_mult)
with p S have "is_qfN (P*int(prod ps)) N" by (auto simp add: zprime_def)
moreover from IH have "primel ps" by (simp add: primel_def)
moreover from IH have "∀ R. zprime R ∧ R dvd int(prod ps) --> is_qfN R N"
by (auto simp add: int_mult zdvd_zmult)
ultimately have "?B ps" by simp
with ass3 show False by simp
qed
with ps ass2 ass show False by auto
qed
lemma qfN_oddprime_cube:
"[| zprime (p^2+N*q^2); (p^2+N*q^2) ∈ zOdd; p ≠ 0; N ≥ 1 |]
==> ∃ a b. (p^2+N*q^2)^3 = a^2 + N*b^2 ∧ zgcd(a, N*b)=1"
proof -
let ?P = "p^2+N*q^2"
assume P: "zprime ?P" and Podd: "?P ∈ zOdd" and p0: "p ≠ 0" and N1: "N ≥ 1"
have suc23: "3 = Suc 2" by simp
let ?a = "p*(p^2 - 3*N*q^2)"
let ?b = "q*(3*p^2 - N*q^2)"
have abP: "?P^3 = ?a^2 + N*?b^2" by (simp add: nat_number ring_simps)
have "zgcd(?b,?a) ≠ 1 ==> ?P dvd p"
proof -
let ?h = "zgcd(?b,?a)"
assume h1: "?h ≠ 1"
have "?h ≥ 0" by (rule zgcd_geq_zero)
hence "?h = 0 ∨ ?h = 1 ∨ ?h > 1" by auto
with h1 have "?h =0 ∨ ?h >1" by auto
moreover
{ assume "?h = 0" hence "nat¦?b¦ = 0 ∧ nat¦?a¦ = 0"
by (unfold zgcd_def, auto simp add: gcd_zero)
hence "?a = 0 ∧ ?b = 0" by arith
with abP have "?P^3 = 0" by auto
with P have False by (unfold zprime_def, auto)
hence ?thesis by simp }
moreover
{ assume "?h > 1" hence "∃ g. zprime g ∧ g dvd ?h" by (rule zprime_factor_exists)
then obtain g where g: "zprime g ∧ g dvd ?h" by blast
hence "g dvd ?b ∧ g dvd ?a" by (simp add: zgcd_greatest_iff)
with g have g1: "g dvd q ∨ g dvd 3*p^2-N*q^2"
and g2: "g dvd p ∨ g dvd p^2 - 3*N*q^2"
by (auto simp add: zprime_zdvd_zmult_general)
from g have gpos: "g ≥ 0" by (auto simp only: zprime_def)
have "g dvd ?P"
proof (cases)
assume "g dvd q"
hence gNq: "g dvd N*q^2" by (auto simp add: dvd_def power2_eq_square)
show ?thesis
proof (cases)
assume gp: "g dvd p"
hence "g dvd p^2" by (auto simp add: dvd_def power2_eq_square)
with gNq show ?thesis by (auto simp add: zdvd_zadd)
next
assume "¬ g dvd p" with g2 have "g dvd p^2 - 3*N*q^2" by auto
moreover from gNq have "g dvd 4*(N*q^2)" by (rule zdvd_zmult)
ultimately have "g dvd p^2 - 3*(N*q^2) + 4*(N*q^2)"
by (simp only: zdvd_zadd mult_ac)
moreover have "p^2 - 3*(N*q^2)+4*(N*q^2) = p^2 + N*q^2" by arith
ultimately show ?thesis by simp
qed
next
assume "¬ g dvd q" with g1 have gpq: "g dvd 3*p^2-N*q^2" by simp
show ?thesis
proof (cases)
assume "g dvd p"
hence "g dvd 4*p^2" by (auto simp add: dvd_def power2_eq_square)
with gpq have " g dvd 4*p^2 - (3*p^2 - N*q^2)" by (simp only: zdvd_zdiff)
moreover have "4*p^2 - (3*p^2 - N*q^2) = p^2 + N*q^2" by arith
ultimately show ?thesis by simp
next
assume "¬ g dvd p" with g2 have "g dvd p^2 - 3*N*q^2" by auto
with gpq have "g dvd 3*p^2-N*q^2 - (p^2 - 3*N*q^2)"
by (simp only: zdvd_zdiff)
moreover have "3*p^2-N*q^2 - (p^2 - 3*N*q^2) = 2*?P" by auto
ultimately have "g dvd 2*?P" by simp
with g have "g dvd 2 ∨ g dvd ?P" by (simp only: zprime_zdvd_zmult)
moreover have "¬ g dvd 2"
proof (rule ccontr, simp)
assume gdvd2: "g dvd 2"
have "g ≤ 2"
proof (rule ccontr)
assume "¬ g ≤ 2" hence "g > 2" by simp
moreover have "(0::int) < 2" by auto
ultimately have "¬ g dvd 2" by (auto simp only: zdvd_not_zless)
with gdvd2 show False by simp
qed
moreover from g have "g ≥ 2" by (simp add: zprime_def)
ultimately have "g = 2" by auto
with g have "2 dvd ?a ∧ 2 dvd ?b" by (auto simp add: zgcd_greatest_iff)
hence "2 dvd ?a^2 ∧ 2 dvd N*?b^2"
by (auto simp only: power2_eq_square zdvd_zmult)
with abP have "2 dvd ?P^3" by (simp only: zdvd_zadd)
hence "?P^3 ∈ zEven" by (auto simp add: dvd_def zEven_def)
moreover have "?P^3 ∈ zOdd"
proof -
from Podd have "?P*?P^2 ∈ zOdd"
by (simp only: odd_times_odd power2_eq_square)
thus ?thesis by (simp only: cube_square)
qed
ultimately show False by (auto simp only: odd_iff_not_even)
qed
ultimately show ?thesis by simp
qed
qed
with P gpos have "g = 1 ∨ g = ?P" by (auto simp only: zprime_def)
with g have "g = ?P" by (simp add: zprime_def)
with g have Pab: "?P dvd ?a ∧ ?P dvd ?b" by (auto simp add: zgcd_greatest_iff)
have ?thesis
proof -
from Pab P have "?P dvd p ∨ ?P dvd p^2- 3*N*q^2"
by (auto simp add: zprime_zdvd_zmult_general)
moreover
{ assume "?P dvd p^2 - 3*N*q^2"
moreover have "?P dvd 3*(p^2 + N*q^2)"
by (auto simp only: zdvd_refl zdvd_zmult)
ultimately have "?P dvd p^2- 3*N*q^2 + 3*(p^2+N*q^2)"
by (simp only: zdvd_zadd)
hence "?P dvd 4*p^2" by auto
with P have "?P dvd 4 ∨ ?P dvd p^2"
by (simp only: zprime_zdvd_zmult_general)
moreover have "¬ ?P dvd 4"
proof (rule ccontr, simp)
assume Pdvd4: "?P dvd 4"
have "?P ≤ 4"
proof (rule ccontr)
assume "¬ ?P ≤ 4" hence "?P > 4" by simp
moreover have "(0::int) < 4" by auto
ultimately have "¬ ?P dvd 4" by (auto simp only: zdvd_not_zless)
with Pdvd4 show False by simp
qed
moreover from P have "?P ≥ 2" by (auto simp add: zprime_def)
moreover have "?P ≠ 2 ∧ ?P ≠ 4"
proof (rule ccontr, simp)
assume "?P = 2 ∨ ?P = 4" hence "?P ∈ zEven"
by (auto simp add: zEven_def)
with Podd show False by (simp add: odd_iff_not_even)
qed
ultimately have "?P = 3" by auto
with Pdvd4 have "(3::int) dvd 4" by simp
thus False by arith
qed
ultimately have "?P dvd p*p" by (simp add: power2_eq_square)
with P have ?thesis by (auto dest: zprime_zdvd_zmult_general) }
ultimately show ?thesis by auto
qed }
ultimately show ?thesis by blast
qed
moreover have "zgcd(N,?a) ≠ 1 ==> ?P dvd p"
proof -
let ?h = "zgcd(N,?a)"
assume h1: "?h ≠ 1"
have "?h ≥ 0" by (rule zgcd_geq_zero)
hence "?h = 0 ∨ ?h = 1 ∨ ?h > 1" by auto
with h1 have "?h =0 ∨ ?h >1" by auto
moreover
{ assume "?h = 0" hence "nat¦N¦ = 0 ∧ nat¦?a¦ = 0"
by (unfold zgcd_def, auto simp add: gcd_zero)
hence "N = 0" by arith
with N1 have False by auto
hence ?thesis by simp }
moreover
{ assume "?h > 1" hence "∃ g. zprime g ∧ g dvd ?h" by (rule zprime_factor_exists)
then obtain g where g: "zprime g ∧ g dvd ?h" by blast
hence gN: "g dvd N" and "g dvd ?a" by (auto simp add: zgcd_greatest_iff)
hence "g dvd p*p^2 - N*(3*p*q^2)"
by (auto simp only: zdiff_zmult_distrib2 mult_ac)
with gN have "g dvd p*p^2 - N*(3*p*q^2) + N*(3*p*q^2)"
by (simp only: zdvd_zadd zdvd_zmult2)
hence "g dvd p*p^2" by simp
with g have "g dvd p ∨ g dvd p*p"
by (simp add: zprime_zdvd_zmult_general power2_eq_square)
with g have gp: "g dvd p" by (auto dest: zprime_zdvd_zmult_general)
hence "g dvd p^2" by (simp add: zdvd_zmult power2_eq_square)
with gN have gP: "g dvd ?P" by (auto simp add: zdvd_zmult2 zdvd_zadd)
from g have "g ≥ 0" by (simp add: zprime_def)
with gP P have "g = 1 ∨ g = ?P" by (auto simp only: zprime_def)
with g have "g = ?P" by (auto simp only: zprime_def)
with gp have ?thesis by simp }
ultimately show ?thesis by auto
qed
moreover have "¬ ?P dvd p"
proof (rule ccontr, clarsimp)
assume Pdvdp: "?P dvd p"
have "p^2 ≥ ?P^2"
proof (rule ccontr)
assume "¬ p^2 ≥ ?P^2" hence pP: "p^2 < ?P^2" by simp
moreover with p0 have "p^2 > 0" by (simp add: zero_less_power2)
ultimately have "¬ ?P^2 dvd p^2" by (simp add: zdvd_not_zless)
with Pdvdp show False by (simp add: zpower_zdvd_mono)
qed
moreover with P have "?P*1 < ?P*?P"
by (unfold zprime_def, auto simp only: zmult_zless_mono2)
ultimately have "p^2 > ?P" by (auto simp add: power2_eq_square)
hence neg: "N*q^2 < 0" by auto
show False
proof -
have "is_qfN (0^2 + N*q^2) N" by (auto simp only: is_qfN_def)
with N1 have "0^2 +N*q^2 ≥ 0" by (rule qfN_pos)
with neg show False by simp
qed
qed
ultimately have "zgcd(?b,?a)=1 ∧ zgcd(N,?a)=1" by auto
hence "zgcd(N*?b,?a) = 1" by (simp only: zgcd_zmult_cancel)
with abP show ?thesis by (auto simp only: zgcd_commute)
qed
subsection {* Uniqueness ($N>1$)*}
lemma qfN_prime_unique:
"[| zprime (a^2+N*b^2); N > 1; a^2+N*b^2 = c^2+N*d^2 |]
==> (¦a¦ = ¦c¦ ∧ ¦b¦ = ¦d¦)"
proof -
let ?P = "a^2+N*b^2"
assume P: "zprime ?P" and N: "N > 1" and abcdN: "?P = c^2 + N*d^2"
have mult: "(a*d+b*c)*(a*d-b*c) = ?P*(d^2-b^2)"
proof -
have "(a*d+b*c)*(a*d-b*c) = (a^2 + N*b^2)*d^2 - b^2*(c^2 + N*d^2)"
by (simp add: nat_number ring_simps)
with abcdN show ?thesis by (simp add: ring_simps)
qed
have "?P dvd a*d+b*c ∨ ?P dvd a*d-b*c"
proof -
from mult have "?P dvd (a*d+b*c)*(a*d-b*c)" by simp
with P show ?thesis by (simp add: zprime_zdvd_zmult_general)
qed
moreover
{ assume "?P dvd a*d+b*c"
then obtain Q where Q: "a*d+b*c = ?P*Q" by (auto simp add: dvd_def)
from abcdN have "?P^2 = (a^2 + N*b^2) * (c^2 + N*d^2)"
by (simp add: power2_eq_square)
also have "… = (a*c-N*b*d)^2 + N*(a*d+b*c)^2" by (rule qfN_mult2)
also with Q have "… = (a*c-N*b*d)^2 + N*Q^2*?P^2"
by (simp add: mult_ac power_mult_distrib)
also have "… ≥ N*Q^2*?P^2" by (simp add: zero_le_power2)
finally have pos: "?P^2 ≥ ?P^2*(Q^2*N)" by (simp add: mult_ac)
have "b^2 = d^2"
proof (rule ccontr)
assume "b^2 ≠ d^2"
with P mult Q have "Q ≠ 0" by (unfold zprime_def, auto)
hence "Q^2 > 0" by (simp add: zero_less_power2)
moreover with N have "Q^2*N > Q^2*1" by (simp only: zmult_zless_mono2)
ultimately have "Q^2*N > 1" by arith
moreover with P have "?P^2 > 0" by (simp add: zprime_def zero_less_power2)
ultimately have "?P^2*1 < ?P^2*(Q^2*N)" by (simp only: zmult_zless_mono2)
with pos show False by simp
qed }
moreover
{ assume "?P dvd a*d-b*c"
then obtain Q where Q: "a*d-b*c = ?P*Q" by (auto simp add: dvd_def)
from abcdN have "?P^2 = (a^2 + N*b^2) * (c^2 + N*d^2)"
by (simp add: power2_eq_square)
also have "… = (a*c+N*b*d)^2 + N*(a*d-b*c)^2" by (rule qfN_mult1)
also with Q have "… = (a*c+N*b*d)^2 + N*Q^2*?P^2"
by (simp add: mult_ac power_mult_distrib)
also have "… ≥ N*Q^2*?P^2" by (simp add: zero_le_power2)
finally have pos: "?P^2 ≥ ?P^2*(Q^2*N)" by (simp add: mult_ac)
have "b^2 = d^2"
proof (rule ccontr)
assume "b^2 ≠ d^2"
with P mult Q have "Q ≠ 0" by (unfold zprime_def, auto)
hence "Q^2 > 0" by (simp add: zero_less_power2)
moreover with N have "Q^2*N > Q^2*1" by (simp only: zmult_zless_mono2)
ultimately have "Q^2*N > 1" by arith
moreover with P have "?P^2 > 0" by (simp add: zprime_def zero_less_power2)
ultimately have "?P^2*1 < ?P^2 * (Q^2*N)" by (simp only: zmult_zless_mono2)
with pos show False by simp
qed }
ultimately have bd: "b^2 = d^2" by blast
moreover with abcdN have "a^2 = c^2" by auto
ultimately show ?thesis by (auto simp only: power2_eq_iff_abs_eq)
qed
lemma qfN_square_prime:
assumes ass:
"zprime (p^2+N*q^2) ∧ N>1 ∧ (p^2+N*q^2)^2 = r^2+N*s^2 ∧ zgcd(r,s)=1"
shows "¦r¦ = ¦p^2-N*q^2¦ ∧ ¦s¦ = ¦2*p*q¦"
proof -
let ?P = "p^2 + N*q^2"
let ?A = "r^2 + N*s^2"
from ass have P1: "?P > 1" by (simp add: zprime_def)
from ass have APP: "?A = ?P*?P" by (simp only: power2_eq_square)
with ass have "zprime ?P ∧ ?P dvd ?A" by (simp add: dvdI)
then obtain u v e where uve:
"?A = (u^2+N*v^2)*?P ∧ r = p*u+e*N*q*v ∧ s = p*v - e*q*u ∧ ¦e¦=1"
by (frule_tac p="p" in qfN_div_prime, auto)
with APP P1 ass have "zprime (u^2+N*v^2) ∧ N>1 ∧ u^2 + N*v^2 = ?P"
by auto
hence "¦u¦ = ¦p¦ ∧ ¦v¦ = ¦q¦" by (auto dest: qfN_prime_unique)
then obtain f g where f: "u = f*p ∧ ¦f¦ = 1" and g: "v = g*q ∧ ¦g¦ = 1"
by (blast dest: abs_eq_impl_unitfactor)
with uve have "r = f*p*p + (e*g)*N*q*q ∧ s = g*p*q - (e*f)*p*q" by simp
hence rs: "r = f*p^2 + (e*g)*N*q^2 ∧ s = (g - e*f)*p*q"
by (auto simp only: power2_eq_square zdiff_zmult_distrib)
moreover have "s ≠ 0"
proof (rule ccontr, simp)
assume s0: "s=0"
hence "zgcd(r,s) = ¦r¦" by (simp only: zgcd_0)
with ass have "¦r¦ = 1" by simp
hence "r^2 = 1" by (auto simp add: abs_power2_distrib)
with s0 have "?A = 1" by simp
moreover have "?P^2 > 1"
proof -
from P1 have "1 < ?P ∧ (0::int) ≤ 1 ∧ (0::nat) < 2" by auto
hence "?P^2 > 1^2" by (simp only: power_strict_mono)
thus ?thesis by auto
qed
moreover from ass have "?A = ?P^2" by simp
ultimately show False by auto
qed
ultimately have "g ≠ e*f" by auto
moreover from f g uve have "¦g¦ = ¦e*f¦" by auto
ultimately have "g = -(e*f)" by arith
with rs uve have "r = f*(p^2 - N*q^2) ∧ s = (-e*f)*2*p*q"
by (auto simp add: power2_eq_square zdiff_zmult_distrib2)
hence "¦r¦ = ¦f¦ * ¦p^2-N*q^2¦
∧ ¦s¦ = ¦e¦*¦f¦*¦2*p*q¦"
by (auto simp add: abs_mult)
with uve f g show ?thesis by (auto simp only: zmult_1)
qed
lemma qfN_cube_prime:
assumes ass: "zprime (p^2 + N*q^2) ∧ N > 1
∧ (p^2 + N*q^2)^3 = a^2 + N*b^2 ∧ zgcd(a, b)=1"
shows "¦a¦ = ¦p^3- 3*N*p*q^2¦ ∧ ¦b¦ = ¦3*p^2*q-N*q^3¦"
proof -
let ?P = "p^2 + N*q^2"
let ?A = "a^2 + N*b^2"
from ass have P1: "?P > 1" by (simp add: zprime_def)
with ass have APP: "?A = ?P*?P^2" by (auto simp only: cube_square)
with ass have "zprime ?P ∧ ?P dvd ?A" by (simp add: dvdI)
then obtain u v e where uve:
"?A = (u^2+N*v^2)*?P ∧ a = p*u+e*N*q*v ∧ b = p*v-e*q*u ∧ ¦e¦=1"
by (frule_tac p="p" in qfN_div_prime, auto)
have "zgcd(u,v)=1"
proof -
let ?g = "zgcd(u,v)"
have "?g dvd u ∧ ?g dvd v" by (auto simp add: zgcd_greatest_iff)
with uve have "?g dvd a ∧ ?g dvd b"
by (auto simp add: zdvd_zmult zdvd_zadd zdvd_zdiff)
hence "?g dvd zgcd(a,b)" by (auto simp add: zgcd_greatest_iff)
with ass have "?g dvd 1" by simp
moreover have "?g ≥ 0" by (rule zgcd_geq_zero)
ultimately show ?thesis by auto
qed
with P1 uve APP ass have "zprime ?P ∧ N > 1 ∧ ?P^2 = u^2+N*v^2
∧ zgcd(u,v)=1" by (auto simp add: mult_ac)
hence "¦u¦ = ¦p^2-N*q^2¦ ∧ ¦v¦ = ¦2*p*q¦" by (rule qfN_square_prime)
then obtain f g where f: "u = f*(p^2-N*q^2) ∧ ¦f¦ = 1"
and g: "v = g*(2*p*q) ∧ ¦g¦ = 1" by (blast dest: abs_eq_impl_unitfactor)
with uve have "a = p*f*(p^2-N*q^2) + e*N*q*g*2*p*q
∧ b = p*g*2*p*q -e*q*f*(p^2-N*q^2)" by auto
hence ab: "a = f*p*p^2 + -f*N*p*q^2 + 2*e*g*N*p*q^2
∧ b = 2*g*p^2*q - e*f*p^2*q + e*f*N*q*q^2"
by (auto simp add: mult_ac zdiff_zmult_distrib2 power2_eq_square)
from f have f2: "f^2 = 1" by (auto simp add: abs_power2_distrib)
from g have g2: "g^2 = 1" by (auto simp add: abs_power2_distrib)
have "e ≠ f*g"
proof (rule ccontr, simp)
assume efg: "e = f*g"
with ab g have "a = f*p*p^2+f*N*p*q^2" by (auto simp add: power2_eq_square)
hence "a = (f*p)*?P" by (auto simp add: zadd_zmult_distrib2 mult_ac)
hence Pa: "?P dvd a" by auto
from efg f ab have "b = g*p^2*q+g*N*q*q^2" by (auto simp add: power2_eq_square)
hence "b = (g*q)*?P" by (auto simp add: zadd_zmult_distrib2 mult_ac)
hence "?P dvd b" by auto
with Pa have "?P dvd zgcd(a,b)" by (simp add: zgcd_greatest_iff)
with ass have "?P dvd 1" by auto
with P1 show False by auto
qed
moreover from f g uve have "¦e¦ = ¦f*g¦" by auto
ultimately have "e = -(f*g)" by arith
with ab f g have "a = f*p*p^2 - 3*f*N*p*q^2 ∧ b = 3*g*p^2*q - g*N*q*q^2"
by (auto simp add: power2_eq_square)
hence "a = f*(p^3 - 3*N*p*q^2) ∧ b = g*( 3*p^2*q - N*q^3 )"
by (auto simp only: zdiff_zmult_distrib2 mult_ac cube_square)
with f g show ?thesis by (auto simp add: zmult_1 abs_mult)
qed
subsection {* The case $N=3$ *}
lemma qf3_even: "a^2+3*b^2 ∈ zEven ==> ∃ B. a^2+3*b^2 = 4*B ∧ is_qfN B 3"
proof -
let ?A = "a^2+3*b^2"
assume even: "?A ∈ zEven"
have "(a ∈ zOdd ∧ b ∈ zOdd) ∨ (a ∈ zEven ∧ b ∈ zEven)"
proof (rule ccontr, auto dest: not_odd_impl_even)
assume "a ∉ zOdd" and "b ∉ zEven"
hence "a ∈ zEven ∧ b ∈ zOdd" by (auto simp only: odd_iff_not_even)
hence "a^2 ∈ zEven ∧ b^2 ∈ zOdd"
by (auto simp only: power2_eq_square odd_times_odd even_times_either)
moreover have "3 ∈ zOdd" by (unfold zOdd_def, auto)
ultimately have "?A ∈ zOdd" by (auto simp add: odd_times_odd even_plus_odd)
with even show False by (simp add: odd_iff_not_even)
next
assume "a ∉ zEven" and "b ∉ zOdd"
hence "a ∈ zOdd ∧ b ∈ zEven" by (auto simp only: odd_iff_not_even)
hence "a^2 ∈ zOdd ∧ b^2 ∈ zEven"
by (auto simp only: power2_eq_square odd_times_odd even_times_either)
moreover hence "b^2*3 ∈ zEven" by (simp only: even_times_either)
ultimately have "b^2*3+a^2 ∈ zOdd" by (auto simp add: even_plus_odd)
hence "?A ∈ zOdd" by (simp only: mult_ac add_ac)
with even show False by (simp add: odd_iff_not_even)
qed
moreover
{ assume "a ∈ zEven ∧ b ∈ zEven"
then obtain c d where abcd: "a = 2*c ∧ b = 2*d" by (unfold zEven_def, auto)
hence "?A = 4*(c^2 + 3*d^2)" by (simp add: power_mult_distrib)
moreover have "is_qfN (c^2+3*d^2) 3" by (unfold is_qfN_def, auto)
ultimately have ?thesis by blast }
moreover
{ assume "a ∈ zOdd ∧ b ∈ zOdd"
then obtain c d where abcd: "a = 2*c+1 ∧ b = 2*d+1"
by (unfold zOdd_def, auto)
have "c-d ∈ zOdd ∨ c-d ∈ zEven" by (rule_tac x="c-d" in even_odd_disj)
moreover
{ assume "c-d ∈ zEven"
then obtain e where "c-d = 2*e" by (auto simp add: zEven_def)
with abcd have e1: "a-b = 4*e" by arith
hence e2: "a+3*b = 4*(e+b)" by auto
have "4*?A = (a+3*b)^2 + 3*(a-b)^2"
by (simp add: nat_number ring_simps)
also with e1 e2 have "… = (4*(e+b))^2+3*(4*e)^2" by (simp(no_asm_simp))
finally have "?A = 4*((e+b)^2 + 3*e^2)" by (simp add: nat_number ring_simps)
moreover have "is_qfN ((e+b)^2 + 3*e^2) 3" by (unfold is_qfN_def, auto)
ultimately have ?thesis by blast }
moreover
{ assume "c-d ∈ zOdd"
then obtain e where "c-d = 2*e+1" by (auto simp add: zOdd_def)
with abcd have e1: "a+b = 4*(e+d+1)" by auto
hence e2: "a- 3*b = 4*(e+d-b+1)" by auto
have "4*?A = (a- 3*b)^2 + 3*(a+b)^2"
by (simp add: nat_number ring_simps)
also with e1 e2 have "… = (4*(e+d-b+1))^2 +3*(4*(e+d+1))^2"
by (simp (no_asm_simp))
finally have "?A = 4*((e+d-b+1)^2+3*(e+d+1)^2)"
by (simp add: nat_number ring_simps)
moreover have "is_qfN ((e+d-b+1)^2 + 3*(e+d+1)^2) 3"
by (unfold is_qfN_def, auto)
ultimately have ?thesis by blast }
ultimately have ?thesis by auto }
ultimately show ?thesis by auto
qed
lemma qf3_even_general: "[| is_qfN A 3; A ∈ zEven |]
==> ∃ B. A = 4*B ∧ is_qfN B 3"
proof -
assume "A ∈ zEven" and "is_qfN A 3"
then obtain a b where "A = a^2 + 3*b^2"
and "a^2 + 3*b^2 ∈ zEven" by (unfold is_qfN_def, auto)
thus ?thesis by (auto simp add: qf3_even)
qed
lemma qf3_oddprimedivisor_not:
assumes ass: "zprime P ∧ P ∈ zOdd ∧ Q>0 ∧ is_qfN (P*Q) 3 ∧ ¬ is_qfN P 3"
shows "∃ R. zprime R ∧ R ∈ zOdd ∧ R dvd Q ∧ ¬ is_qfN R 3"
proof (rule ccontr, simp)
assume ass2: "∀ R. R dvd Q --> R ∈ zOdd --> zprime R --> is_qfN R 3"
(is "?A Q")
obtain n::nat where "n = nat Q" by auto
with ass have n: "Q = int n" by auto
have "(n > 0 ∧ is_qfN (P*int n) 3 ∧ ?A(int n)) ==> False" (is "?B n ==> False")
proof (induct n rule: less_induct)
case (less n)
hence IH: "!!m. m<n ∧ ?B m ==> False"
and Bn: "?B n" by auto
show False
proof (cases)
assume odd: "(int n) ∈ zOdd"
from Bn ass have "zprime P ∧ int n > 0 ∧ is_qfN (P*int n) 3 ∧ ¬ is_qfN P 3"
by simp
hence "∃ R. zprime R ∧ R dvd int n ∧ ¬ is_qfN R 3"
by (rule qfN_primedivisor_not)
then obtain R where R: "zprime R ∧ R dvd int n ∧ ¬ is_qfN R 3" by auto
moreover with odd have "R ∈ zOdd"
proof -
from R obtain U where "int n = R*U" by (auto simp add: dvd_def)
with odd show ?thesis by (auto dest: odd_mult_odd_prop)
qed
moreover from Bn have "?A (int n)" by simp
ultimately show False by auto
next
assume "¬ (int n) ∈ zOdd"
hence even: "int n ∈ zEven" by (rule not_odd_impl_even)
hence "(int n)*P ∈ zEven" by (rule even_times_either)
with Bn have "P*int n ∈ zEven ∧ is_qfN (P*int n) 3" by (simp add: mult_ac)
hence "∃ B. P*(int n) = 4*B ∧ is_qfN B 3" by (simp only: qf3_even_general)
then obtain B where B: "P*(int n) = 4*B ∧ is_qfN B 3" by auto
hence "2^2 dvd (int n)*P" by (simp add: mult_ac)
moreover have "¬ 2 dvd P"
proof (rule ccontr, simp)
assume "2 dvd P"
with ass have "P ∈ zOdd ∧ P ∈ zEven" by (simp add: dvd_def zEven_def)
thus False by (simp only: even_odd_conj)
qed
moreover have "zprime 2" by (rule zprime_2)
ultimately have "2^2 dvd int n"
by (rule_tac p="2" in zprime_power_zdvd_cancel_right)
then obtain im::int where "int n = 4*im" by (auto simp add: dvd_def)
moreover obtain m::nat where "m = nat im" by auto
ultimately have m: "n = 4*m" by arith
with B have "is_qfN (P*int m) 3" by (auto simp add: int_mult)
moreover from m Bn have "m > 0" by auto
moreover from m Bn have "?A (int m)"
by (auto simp add: zdvd_zmult int_mult)
ultimately have Bm: "?B m" by simp
from Bn m have "m < n" by arith
with IH Bm show False by auto
qed
qed
with ass ass2 n show False by auto
qed
lemma qf3_oddprimedivisor:
"[| zprime P; P ∈ zOdd; zgcd(a,b)=1; P dvd (a^2+3*b^2) |]
==> is_qfN P 3"
proof -
have lem: "∀a b. (zprime P ∧ P ∈ zOdd ∧ zgcd(a,b)=1 ∧ P dvd (a^2+3*b^2))
--> is_qfN P 3" (is "?B P")
proof (rule_tac x="P" and V="λP. nat¦P¦" in val_infinite_descent)
fix x
assume "nat¦x¦ = 0"
hence "x = 0" by arith
thus "?B x" by (simp add: zprime_def)
next
fix x
assume "nat¦x¦ > 0" and "¬ ?B x"
then obtain a b where abx: "zprime x ∧ x ∈ zOdd ∧ zgcd(a,b)=1
∧ x dvd (a^2+3*b^2) ∧ ¬ is_qfN x 3" by auto
then obtain M where M: "a^2+3*b^2 = x*M" by (auto simp add: dvd_def)
let ?A = "a^2 + 3*b^2"
from abx have x0: "x > 0 ∧ x ∈ zOdd" by (simp add: zprime_def)
then obtain m where "2*¦a-m*x¦<x" by (auto dest: best_odd_division_abs)
then obtain c where cm: "c = a-m*x ∧ 2*¦c¦ < x" by auto
from x0 obtain n where "2*¦b-n*x¦<x" by (auto dest: best_odd_division_abs)
then obtain d where dn: "d = b-n*x ∧ 2*¦d¦ < x" by auto
let ?C = "c^2+3*d^2"
have C3: "is_qfN ?C 3" by (unfold is_qfN_def, auto)
have C0: "?C > 0"
proof -
have hlp: "(3::int) ≥ 1" by simp
with C3 have "?C ≥ 0" by (simp only: qfN_pos)
hence "?C = 0 ∨ ?C > 0" by auto
moreover
{ assume "?C = 0"
with hlp have "c=0 ∧ d=0" by (rule qfN_zero)
with cm dn have "a = m*x ∧ b = n*x" by simp
hence "x dvd a ∧ x dvd b" by simp
hence "x dvd zgcd(a,b)" by (simp add: zgcd_greatest_iff)
with abx have False by (auto simp add: zprime_def) }
ultimately show ?thesis by blast
qed
have "x dvd ?C"
proof
have "?C = ¦c¦^2 + 3*¦d¦^2" by (simp only: power2_abs)
also with cm dn have "… = (a-m*x)^2 + 3*(b-n*x)^2" by simp
also have "… =
a^2 - 2*a*(m*x) + (m*x)^2 + 3*(b^2 - 2*b*(n*x) + (n*x)^2)"
by (simp only: zdiff_power2)
also with abx M have "… =
x*M - x*(2*a*m + 3*2*b*n) + x^2*(m^2 + 3*n^2)"
by (simp only: power_mult_distrib zadd_zmult_distrib2 mult_ac, auto)
finally show "?C = x*(M - (2*a*m + 3*2*b*n) + x*(m^2 + 3*n^2))"
by (simp add: power2_eq_square zadd_zmult_distrib2 zdiff_zmult_distrib2)
qed
then obtain y where y: "?C = x*y" by (auto simp add: dvd_def)
have yx: "y < x"
proof (rule ccontr)
assume "¬ y < x" hence xy: "x-y ≤ 0" by simp
have hlp: "2*¦c¦ ≥ 0 ∧ 2*¦d¦ ≥ 0 ∧ (3::nat) > 0" by simp
from y have "4*x*y = 2^2*c^2 + 3*2^2*d^2" by simp
hence "4*x*y = (2*¦c¦)^2 + 3*(2*¦d¦)^2"
by (auto simp add: power2_abs power_mult_distrib)
with cm dn hlp have "4*x*y < x^2 + 3*(2*¦d¦)^2"
and "(3::int) > 0 ∧ (2*¦d¦)^2 < x^2"
by (auto simp add: power_strict_mono)
hence "x*4*y < x^2 + 3*x^2" by (auto)
also have "… = x*4*x" by (simp add: power2_eq_square)
finally have contr: "(x-y)*(4*x) > 0" by (auto simp add: zdiff_zmult_distrib2)
show False
proof (cases)
assume "x-y = 0" with contr show False by auto
next
assume "¬ x-y =0" with xy have "x-y < 0" by simp
moreover from x0 have "4*x > 0" by simp
ultimately have "4*x*(x-y) < 4*x*0" by (simp only: zmult_zless_mono2)
with contr show False by auto
qed
qed
have y0: "y > 0"
proof (rule ccontr)
assume "¬ y > 0"
hence "y ≤ 0" by simp
moreover have "y ≠ 0"
proof (rule ccontr)
assume "¬ y≠0" hence "y=0" by simp
with y and C0 show False by auto
qed
ultimately have "y < 0" by simp
with x0 have "x*y < x*0" by (simp only: zmult_zless_mono2)
with C0 y show False by simp
qed
let ?g = "zgcd(c,d)"
have "c ≠ 0 ∨ d ≠ 0"
proof (rule ccontr)
assume "¬ (c≠0 ∨ d≠0)" hence "c=0 ∧ d=0" by simp
with C0 show False by simp
qed
then obtain e f where ef: "c = ?g*e ∧ d = ?g * f ∧ zgcd(e,f)=1"
by (frule_tac a="c" in make_zrelprime, auto)
have g2nonzero: "?g^2 ≠ 0"
proof (rule ccontr, clarsimp)
assume "?g =0"
hence "nat¦c¦=0 ∧ nat¦d¦=0"
by (unfold zgcd_def, auto simp add: gcd_zero)
hence "c=0 ∧ d=0" by arith
with C0 show False by simp
qed
let ?E = "e^2 + 3*f^2"
have E3: "is_qfN ?E 3" by (unfold is_qfN_def, auto)
have CgE: "?C = ?g^2 * ?E"
proof -
have "?g^2 * ?E = (?g*e)^2 + 3*(?g*f)^2"
by (simp add: zadd_zmult_distrib2 power_mult_distrib)
with ef show ?thesis by simp
qed
hence "?g^2 dvd ?C" by (simp add: dvd_def)
with y have g2dvdxy: "?g^2 dvd y*x" by (simp add: mult_ac)
moreover have "zgcd(x, ?g^2) = 1"
proof -
let ?h = "zgcd(?g, x)"
have "?h dvd ?g" and "?g dvd c" by auto
hence hc: "?h dvd c" by (rule zdvd_trans)
have "?h dvd ?g" and "?g dvd d" by auto
hence hd: "?h dvd d" by (rule zdvd_trans)
have hx: "?h dvd x" by simp
hence "?h dvd m*x" by (rule zdvd_zmult)
with hc have "?h dvd c+m*x" by (rule zdvd_zadd)
with cm have ha: "?h dvd a" by simp
from hx have "?h dvd n*x" by (rule zdvd_zmult)
with hd have "?h dvd d+n*x" by (rule zdvd_zadd)
with dn have hb: "?h dvd b" by simp
with ha have "?h dvd zgcd(a,b)" by (simp add: zgcd_greatest_iff)
with abx have "?h dvd 1" by simp
hence "?h = 1" by (simp add: zgcd_geq_zero)
hence "zgcd(?g^2,x)=1" by (rule zgcd_1_power_left_distrib)
thus ?thesis by (simp only: zgcd_commute)
qed
ultimately have "?g^2 dvd y" by (auto dest: zrelprime_zdvd_zmult)
then obtain w where w: "y = ?g^2 * w" by (auto simp add: dvd_def)
with CgE y g2nonzero have Ewx: "?E = x*w" by auto
have w0: "w>0"
proof (rule ccontr)
assume "¬ w>0" hence "w ≤ 0" by auto
hence "w=0 ∨ w<0" by auto
moreover
{ assume "w=0" with w y0 have False by auto }
moreover
{ assume wneg: "w<0"
have "?g^2 ≥ 0" by (rule zero_le_power2)
with g2nonzero have "?g^2 > 0" by arith
with wneg have "?g^2*w < ?g^2*0" by (simp only: zmult_zless_mono2)
with w y0 have False by auto }
ultimately show False by blast
qed
have w_le_y: "w ≤ y"
proof (rule ccontr)
assume "¬ w ≤ y"
hence wy: "w > y" by simp
have "?g^2 = 1 ∨ ?g^2 > 1"
proof -
have "?g^2 ≥ 0" by (rule zero_le_power2)
hence "?g^2 =0 ∨ ?g^2 > 0" by auto
with g2nonzero show ?thesis by arith
qed
moreover
{ assume "?g^2 =1" with w wy have False by simp }
moreover
{ assume g1: "?g^2 >1"
with w0 have "w*1 < w*?g^2" by (auto dest: zmult_zless_mono2)
with w have "w < y" by (simp add: zmult_1 mult_ac)
with wy have False by auto }
ultimately show False by blast
qed
from Ewx E3 abx w0 have
"zprime x ∧ x ∈ zOdd ∧ w > 0 ∧ is_qfN (x*w) 3 ∧ ¬ is_qfN x 3" by simp
then obtain z where z: "zprime z ∧ z ∈ zOdd ∧ z dvd w ∧ ¬ is_qfN z 3"
by (frule_tac P="x" in qf3_oddprimedivisor_not, auto)
from Ewx have "w dvd ?E" by simp
with z have "z dvd ?E" by (auto dest: zdvd_trans)
with z ef have "zprime z ∧ z ∈ zOdd ∧ zgcd(e,f)=1 ∧ z dvd ?E ∧ ¬ is_qfN z 3"
by auto
moreover have "nat¦z¦ < nat¦x¦"
proof -
have "z ≤ w"
proof (rule ccontr)
assume "¬ z ≤ w" hence "w < z" by auto
with w0 have "¬ z dvd w" by (rule zdvd_not_zless)
with z show False by simp
qed
with w_le_y yx have "z < x" by simp
with z have "¦z¦ < ¦x¦" by (simp add: zprime_def)
thus ?thesis by auto
qed
ultimately show "∃ z. nat¦z¦ < nat¦x¦ ∧ ¬ ?B z" by auto
qed
assume "zprime P" and "P ∈ zOdd" and "zgcd(a,b)=1" and "P dvd a^2+3*b^2"
with lem show ?thesis by blast
qed
lemma qf3_cube_prime_impl_cube_form:
assumes ab_relprime: "zgcd(a,b)=1" and abP: "P^3 = a^2 + 3*b^2"
and P: "zprime P ∧ P ∈ zOdd"
shows "is_cube_form a b"
proof -
from abP have qfP3: "is_qfN (P^3) 3" by (auto simp only: is_qfN_def)
have PvdP3: "P dvd P^3" by (simp add: nat_number)
with abP ab_relprime P have qfP: "is_qfN P 3" by (simp only: qf3_oddprimedivisor)
then obtain p q where pq: "P = p^2 + 3*q^2" by (auto simp only: is_qfN_def)
with P abP ab_relprime have "zprime (p^2 + 3*q^2) ∧ (3::int) > 1
∧ (p^2+3*q^2)^3 = a^2+3*b^2 ∧ zgcd(a,b)=1" by auto
hence ab: "¦a¦ = ¦p^3 - 3*3*p*q^2¦ ∧ ¦b¦ = ¦3*p^2*q - 3*q^3¦"
by (rule qfN_cube_prime)
hence a: "a = p^3 - 9*p*q^2 ∨ a = -(p^3) + 9*p*q^2" by arith
from ab have b: "b = 3*p^2*q - 3*q^3 ∨ b = -(3*p^2*q) + 3*q^3" by arith
obtain r s where r: "r = -p" and s: "s = -q" by simp
show ?thesis
proof (cases)
assume a1: "a = p^3- 9*p*q^2"
show ?thesis
proof (cases)
assume b1: "b = 3*p^2*q - 3*q^3"
with a1 show ?thesis by (unfold is_cube_form_def, auto)
next
assume "¬ b = 3*p^2*q - 3*q^3"
with b have "b = - 3*p^2*q + 3*q^3" by simp
with s have "b = 3*p^2*s - 3*s^3" by (simp add: power3_minus)
moreover from a s have "a = p^3 - 9*p*s^2" by (simp add: power2_minus)
ultimately show ?thesis by (unfold is_cube_form_def, auto)
qed
next
assume "¬ a = p^3 - 9*p*q^2"
with a have "a = -(p^3) + 9*p*q^2" by simp
with r have ar: "a = r^3 - 9*r*q^2" by (simp add: power3_minus)
show ?thesis
proof (cases)
assume b1: "b = 3*p^2*q - 3*q^3"
with r have "b = 3*r^2*q - 3*q^3" by (simp add: power2_minus)
with ar show ?thesis by (unfold is_cube_form_def, auto)
next
assume "¬ b = 3*p^2*q - 3*q^3"
with b have "b = - 3*p^2*q + 3*q^3" by simp
with r s have "b = 3*r^2*s - 3*s^3"
by (simp add: power2_minus power3_minus)
moreover from ar s have "a = r^3 - 9*r*s^2" by (simp add: power2_minus)
ultimately show ?thesis by (unfold is_cube_form_def, auto)
qed
qed
qed
lemma cube_form_mult: "[| is_cube_form a b; is_cube_form c d; ¦e¦ = 1 |]
==> is_cube_form (a*c+e*3*b*d) (a*d-e*b*c)"
proof -
assume ab: "is_cube_form a b" and c_d: "is_cube_form c d" and e: "¦e¦ = 1"
from ab obtain p q where pq: "a = p^3 - 9*p*q^2 ∧ b = 3*p^2*q - 3*q^3"
by (auto simp only: is_cube_form_def)
from c_d obtain r s where rs: "c = r^3 - 9*r*s^2 ∧ d = 3*r^2*s - 3*s^3"
by (auto simp only: is_cube_form_def)
let ?t = "p*r + e*3*q*s"
let ?u = "p*s - e*r*q"
have e2: "e^2=1"
proof -
from e have "e=1 ∨ e=-1" by simp
moreover
{ assume "e=1" hence ?thesis by auto }
moreover
{ assume "e=-1" hence ?thesis by (simp add: power2_minus) }
ultimately show ?thesis by blast
qed
hence "e*e^2 = e" by simp
hence e3: "e*1 = e^3" by (simp only: cube_square)
have "a*c+e*3*b*d = ?t^3 - 9*?t*?u^2"
proof -
have "?t^3 - 9*?t*?u^2 = p^3*r^3 + e*9*p^2*q*r^2*s + e^2*27*p*q^2*r*s^2
+ e^3*27*q^3*s^3 - 9*p*p^2*r*s^2 + e*18*p^2*q*r^2*s - e^2*9*p*q^2*(r*r^2)
- e*27*p^2*q*(s*s^2) + e^2*54*p*q^2*r*s^2 - e*e^2*27*(q*q^2)*r^2*s"
by (simp add: nat_number ring_simps)
also with e2 e3 have "… =
p^3*r^3 + e*27*p^2*q*r^2*s + 81*p*q^2*r*s^2 + e*27*q^3*s^3
- 9*p^3*r*s^2 - 9*p*q^2*r^3 - e*27*p^2*q*s^3 - e*27*q^3*r^2*s"
by (simp add: cube_square zmult_1)
also with pq rs have "… = a*c + e*3*b*d"
by (simp only: zdiff_zmult_distrib zdiff_zmult_distrib2 mult_ac)
finally show ?thesis by auto
qed
moreover have "a*d-e*b*c = 3*?t^2*?u - 3*?u^3"
proof -
have "3*?t^2*?u - 3*?u^3 =
3*(p*p^2)*r^2*s - e*3*p^2*q*(r*r^2) + e*18*p^2*q*r*s^2
- e^2*18*p*q^2*r^2*s + e^2*27*p*q^2*(s*s^2) - e*e^2*27*(q*q^2)*r*s^2
- 3*p^3*s^3 + e*9*p^2*q*r*s^2 - e^2*9*p*q^2*r^2*s + e^3*3*r^3*q^3"
by (simp add: nat_number ring_simps)
also with e2 e3 have "… = 3*p^3*r^2*s - e*3*p^2*q*r^3 + e*18*p^2*q*r*s^2
- 18*p*q^2*r^2*s + 27*p*q^2*s^3 - e*27*q^3*r*s^2 - 3*p^3*s^3
+ e*9*p^2*q*r*s^2 - 9*p*q^2*r^2*s + e*3*r^3*q^3"
by (simp add: cube_square zmult_1)
also with pq rs have "… = a*d-e*b*c"
by (simp only: zdiff_zmult_distrib zdiff_zmult_distrib2 mult_ac)
finally show ?thesis by auto
qed
ultimately show ?thesis by (auto simp only: is_cube_form_def)
qed
lemma qf3_cube_primelist_impl_cube_form: "[| primel ps; int (prod ps) ∈ zOdd |] ==>
(!! a b. zgcd(a,b)=1 ==> a^2 + 3*b^2 = (int(prod ps))^3 ==> is_cube_form a b)"
proof (induct ps)
case Nil hence ab1: "a^2 + 3*b^2 = 1" by simp
have b0: "b=0"
proof (rule ccontr)
assume "b≠0"
hence "b^2>0" by (simp add: zero_less_power2)
hence "3*b^2 > 1" by arith
with ab1 have "a^2 < 0" by arith
moreover have "a^2 ≥ 0" by (rule zero_le_power2)
ultimately show False by auto
qed
with ab1 have a1: "(a=1 ∨ a=-1)" by (auto simp add: power2_eq_square zmult_eq_1_iff)
then obtain p and q where "p=a" and "q=(0::int)" by simp
with a1 and b0 have "a = p^3 - 9*p*q^2 ∧ b = 3*p^2*q - 3*q^3" by auto
thus "is_cube_form a b" by (auto simp only: is_cube_form_def)
next
case (Cons p ps) hence ass: "zgcd(a,b)=1 ∧ int(prod (p#ps)) ∈ zOdd
∧ a^2+3*b^2 = int(prod (p#ps))^3 ∧ primel ps ∧ zprime (int p)"
and IH: "!! u v. zgcd(u,v)=1 ∧ u^2+3*v^2 = int(prod ps)^3
∧ int(prod ps) ∈ zOdd ==> is_cube_form u v"
by (auto simp add: primel_def prime_impl_zprime_int)
let ?w = "int (prod (p#ps))"
let ?X = "int (prod ps)"
let ?p = "int p"
have ge3_1: "(3::int) ≥ 1" by auto
have pw: "?w = ?p * ?X ∧ ?p ∈ zOdd ∧ ?X ∈ zOdd"
proof (safe)
have "prod (p#ps) = p * prod ps" by simp
thus wpx: "?w = ?p * ?X" by (auto simp only: zmult_int)
with ass show "?p ∈ zOdd" by (auto dest: odd_mult_odd_prop)
from wpx have "?w = ?X*?p" by simp
with ass show "?X ∈ zOdd" by (auto dest: odd_mult_odd_prop)
qed
have "is_qfN ?p 3"
proof -
from ass have "a^2+3*b^2 = (?p*?X)^3" by (simp add: zmult_int)
hence "?p dvd a^2+3*b^2" by (simp add: nat_number ring_simps)
moreover from ass have "zprime ?p" and "zgcd(a,b)=1" by simp
moreover from pw have "?p ∈ zOdd" by simp
ultimately show ?thesis by (simp only: qf3_oddprimedivisor)
qed
then obtain α β where alphabeta: "?p = α^2 + 3*β^2"
by (auto simp add: is_qfN_def)
have "α ≠ 0"
proof (rule ccontr, simp)
assume "α = 0" with alphabeta have "3 dvd ?p" by auto
with pw have w3: "3 dvd ?w" by (simp only: zdvd_zmult2)
then obtain v where "?w = 3*v" by (auto simp add: dvd_def)
with ass have vab: "27*v^3 = a^2 + 3*b^2" by (simp add: power_mult_distrib)
hence "a^2 = 3*(9*v^3 - b^2)" by auto
hence "3 dvd a^2" by (unfold dvd_def, blast)
moreover have "zprime 3" by (rule zprime_3)
ultimately have a3: "3 dvd a" by (rule_tac p="3" in zprime_zdvd_power)
then obtain c where c: "a = 3*c" by (auto simp add: dvd_def)
with vab have "27*v^3 = 9*c^2 + 3*b^2" by (simp add: power_mult_distrib)
hence "b^2 = 3*(3*v^3 - c^2)" by auto
hence "3 dvd b^2" by (unfold dvd_def, blast)
moreover have "zprime 3" by (rule zprime_3)
ultimately have "3 dvd b" by (rule_tac p="3" in zprime_zdvd_power)
with a3 have "3 dvd zgcd(a,b)" by (simp add: zgcd_greatest_iff)
with ass show False by simp
qed
moreover from alphabeta pw ass have
"zprime (α^2 + 3*β^2) ∧ α^2+3*β^2 ∈ zOdd ∧ (3::int) ≥ 1" by auto
ultimately obtain c d where cdp:
"(α^2+3*β^2)^3 = c^2+3*d^2 ∧ zgcd(c, 3*d)=1"
by (blast dest: qfN_oddprime_cube)
with ass pw alphabeta have "∃ u v. a^2+3*b^2 = (u^2 + 3*v^2)*(c^2+3*d^2)
∧ zgcd(u,v)=1 ∧ (∃ e. a = c*u+e*3*d*v ∧ b = c*v-e*d*u ∧ ¦e¦ = 1)"
by (rule_tac A="?w" and n="3" in qfN_power_div_prime, auto)
then obtain u v e where uve: "a^2+3*b^2 = (u^2+3*v^2)*(c^2+3*d^2)
∧ zgcd(u,v)=1 ∧ a = c*u+e*3*d*v ∧ b = c*v-e*d*u ∧ ¦e¦ = 1" by blast
moreover have "is_cube_form u v"
proof -
have uvX: "u^2+3*v^2 = ?X^3"
proof -
from ass have p0: "?p ≠ 0" by (simp add: zprime_def)
from pw have "?p^3*?X^3 = ?w^3" by (simp add: power_mult_distrib)
also with ass have "… = a^2+3*b^2" by simp
also with uve have "… = (u^2+3*v^2)*(c^2+3*d^2)" by auto
also with cdp alphabeta have "… = ?p^3 * (u^2+3*v^2)" by (simp only: mult_ac)
finally have "?p^3*(u^2+3*v^2-?X^3) = 0" by auto
with p0 show ?thesis by auto
qed
with pw IH uve show ?thesis by simp
qed
moreover have "is_cube_form c d"
proof -
have "zgcd(c,d) = 1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix h::int assume "h dvd c" and "h dvd d" and h: "zprime h"
hence "h dvd c*u + d*(e*3*v) ∧ h dvd c*v-d*(e*u)"
by (simp add: zdvd_zmult2 zdvd_zadd zdvd_zdiff)
with uve have "h dvd a ∧ h dvd b" by (auto simp only: mult_ac)
with ass h show False by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
with pw cdp ass alphabeta show ?thesis
by (rule_tac P="?p" in qf3_cube_prime_impl_cube_form, auto)
qed
ultimately show "is_cube_form a b" by (simp only: cube_form_mult)
qed
lemma qf3_cube_impl_cube_form:
assumes ass: "zgcd(a,b)=1 ∧ a^2 + 3*b^2 = w^3 ∧ w ∈ zOdd"
shows "is_cube_form a b"
proof -
have "∃ ps. primel ps ∧ int (prod ps) = w"
proof -
have wpos: "w ≥ 1"
proof -
have "b^2 ≥ 0" by (rule zero_le_power2)
hence "3*b^2 ≥ 0" by arith
moreover have "a^2≥0" by (rule zero_le_power2)
ultimately have "a^2 + 3*b^2 ≥ 0" by arith
with ass have w3pos: "w^3 ≥ 0" by simp
have "w≥0"
proof (rule ccontr)
assume "¬ w≥0" hence "-w > 0" by auto
hence "(-1 * w)^3 > 0" by (auto simp only: zero_less_power)
hence "(-1)^3* (w^3) > 0" by (simp only: power_mult_distrib)
hence "w^3 < 0" by (simp add: neg_one_odd_power)
with w3pos show False by auto
qed
moreover have "w ≠ 0"
proof (rule ccontr)
assume "¬w≠0" with ass have "0 ∈ zOdd" by simp
moreover have "0 ∈ zEven" by (simp add: zEven_def)
ultimately show False by (auto simp add: odd_iff_not_even)
qed
ultimately show ?thesis by (auto)
qed
hence "w=1 ∨ Suc 0 < nat w" by auto
moreover
{ assume "w=1"
hence "primel [] ∧ int (prod []) = w" by (auto simp add: primel_def)
hence ?thesis by (simp only: exI) }
moreover
{ assume "Suc 0 < nat w"
hence "∃ l. primel l ∧ prod l = nat w" by (rule factor_exists)
then obtain ps where ps: "primel ps ∧ prod ps = nat w" by auto
with wpos have ?thesis by auto }
ultimately show ?thesis by blast
qed
with ass show ?thesis by (auto dest: qf3_cube_primelist_impl_cube_form)
qed
subsection {* Existence ($N=3$) *}
text {* This part contains the proof that all prime numbers $\equiv 1 \bmod 6$ can be written as $x^2 + 3y^2$. *}
text {* First show $(\frac{a}{p})(\frac{b}{p}) = (\frac{ab}{p})$, where $p$ is an odd prime. *}
lemma Legendre_zmult: "[| p > 2; zprime p |]
==> (Legendre (a*b) p) = (Legendre a p)*(Legendre b p)"
proof -
assume p2: "p > 2" and prp: "zprime p"
let ?p12 = "nat(((p) - 1) div 2)"
let ?Labp = "Legendre (a*b) p"
let ?Lap = "Legendre a p"
let ?Lbp = "Legendre b p"
from p2 prp have "[?Labp = (a*b)^?p12] (mod p)"
by (simp only: Euler_Criterion)
hence "[a^?p12 * b^?p12 = ?Labp] (mod p)"
by (simp only: power_mult_distrib zcong_sym)
moreover from p2 prp have "[?Lap * ?Lbp = a^?p12*b^?p12] (mod p)"
by (simp only: Euler_Criterion zcong_zmult)
ultimately have "[?Lap * ?Lbp = ?Labp] (mod p)"
by (rule_tac b="a^?p12 * b^?p12" in zcong_trans)
then obtain k where k: "?Labp = (?Lap*?Lbp) + p * k"
by (auto simp add: zcong_iff_lin)
have "k=0"
proof (rule ccontr)
assume "k ≠ 0" hence "¦k¦ = 1 ∨ ¦k¦ > 1" by arith
moreover
{ assume "¦k¦= 1"
with p2 have "¦k¦*p > 2" by auto }
moreover
{ assume k1: "¦k¦ > 1"
with p2 have "¦k¦*2 < ¦k¦*p"
by (simp only: zmult_zless_mono2)
with k1 have "¦k¦*p > 2" by auto }
ultimately have "¦k¦*p > 2" by auto
moreover from p2 have "¦p¦ = p" by auto
ultimately have "¦k*p¦ > 2" by (auto simp only: abs_mult)
moreover from k have "?Labp - ?Lap*?Lbp = k*p" by auto
ultimately have "¦?Labp - ?Lap*?Lbp¦ > 2" by auto
moreover have "?Labp = 1 ∨ ?Labp = 0 ∨ ?Labp = -1"
by (simp add: Legendre_def)
moreover have "?Lap*?Lbp = 1 ∨ ?Lap*?Lbp = 0 ∨ ?Lap*?Lbp = -1"
by (auto simp add: Legendre_def)
ultimately show False by auto
qed
with k show ?thesis by auto
qed
text {* Now show $(\frac{-3}{p}) = +1$ for primes $p \equiv 1 \bmod 6$. *}
lemma Legendre_1mod6: "zprime (6*m+1) ==> Legendre (-3) (6*m+1) = 1"
proof -
let ?p = "6*m+1"
let ?L = "Legendre (-3) ?p"
let ?L1 = "Legendre (-1) ?p"
let ?L3 = "Legendre 3 ?p"
assume p: "zprime ?p"
have neg1cube: "(-1::int)^3 = -1" by (simp add: power3_minus)
have m1: "m ≥ 1"
proof (rule ccontr)
assume "¬ m ≥ 1" hence "m ≤ 0" by simp
with p show False by (auto simp add: zprime_def)
qed
hence pn3: "?p ≠ 3" and p2: "?p > 2" by auto
with p have "?L = (Legendre (-1) ?p) * (Legendre 3 ?p)"
by (frule_tac a="-1" and b="3" in Legendre_zmult, auto)
moreover have "[Legendre (-1) ?p = (-1)^nat m] (mod ?p)"
proof -
from p p2 have "[?L1 = (-1)^(nat(((?p) - 1) div 2))] (mod ?p)"
by (simp only: Euler_Criterion)
moreover have "nat ((?p - 1) div 2) = 3* nat m"
proof -
have "(?p - 1) div 2 = 3*m" by auto
hence "nat((?p - 1) div 2) = nat (3*m)" by simp
moreover have "(3::int) ≥ 0" by simp
ultimately show ?thesis by (simp add: nat_mult_distrib)
qed
moreover with neg1cube have "(-1::int)^(3*nat m) = (-1)^nat m"
by (simp only: power_mult)
ultimately show ?thesis by auto
qed
moreover have "?L3 = (-1)^nat m"
proof -
have "?L3 * (Legendre ?p 3) = (-1)^nat m"
proof -
have "3 ∈ zOdd ∧ ?p ∈ zOdd" by (unfold zOdd_def, auto)
with p pn3 have "?L3 * (Legendre ?p 3) = (-1::int)^(3*nat m)"
by (simp add: zprime_3 Quadratic_Reciprocity nat_mult_distrib)
with neg1cube show ?thesis by (simp add: power_mult)
qed
moreover have "Legendre ?p 3 = 1"
proof -
have "[1^2 = ?p] (mod 3)" by (unfold zcong_def dvd_def, auto)
hence "QuadRes 3 ?p" by (unfold QuadRes_def, blast)
moreover have "¬ [?p = 0] (mod 3)"
proof (rule ccontr, simp)
assume "[?p = 0] (mod 3)"
hence "3 dvd ?p" by (simp add: zcong_def)
moreover have "3 dvd 6*m" by (auto simp add: dvd_def)
ultimately have "3 dvd ?p- 6*m" by (simp only: zdvd_zdiff)
hence "(3::int) dvd 1" by simp
thus False by auto
qed
ultimately show ?thesis by (unfold Legendre_def, auto)
qed
ultimately show ?thesis by auto
qed
ultimately have "[?L = (-1)^(nat m)*(-1)^(nat m)] (mod ?p)"
by (auto dest: zcong_scalar)
hence "[?L = (-1)^((nat m)+(nat m))] (mod ?p)" by (simp only: power_add)
moreover have "(nat m)+(nat m) = 2*(nat m)" by auto
ultimately have "[?L = (-1)^(2*(nat m))] (mod ?p)" by simp
hence "[?L = ((-1)^2)^(nat m)] (mod ?p)" by (simp only: power_mult)
hence "[1 = ?L] (mod ?p)" by (auto simp add: zcong_sym)
hence "?p dvd 1 - ?L" by (simp only: zcong_def)
moreover have "?L = -1 ∨ ?L = 0 ∨ ?L = 1" by (simp add: Legendre_def)
ultimately have "?p dvd 2 ∨ ?p dvd 1 ∨ ?L = 1" by auto
moreover
{ assume "?p dvd 2 ∨ ?p dvd 1"
with p2 have False by (auto simp add: zdvd_not_zless) }
ultimately show ?thesis by auto
qed
text {* Use this to prove that such primes can be written as $x^2 + 3y^2$. *}
lemma qf3_prime_exists: "zprime (6*m+1) ==> ∃ x y. 6*m+1 = x^2 + 3*y^2"
proof -
let ?p = "6*m+1"
assume p: "zprime ?p"
hence "Legendre (-3) ?p = 1" by (rule Legendre_1mod6)
moreover
{ assume "¬ QuadRes ?p (-3)"
hence "Legendre (-3) ?p ≠ 1" by (unfold Legendre_def, auto) }
ultimately have "QuadRes ?p (-3)" by auto
then obtain s where s: "[s^2 = -3] (mod ?p)" by (auto simp add: QuadRes_def)
hence "?p dvd s^2 - (-3::int)" by (unfold zcong_def, simp)
moreover have "s^2 -(-3::int) = s^2 + 3" by arith
ultimately have "?p dvd s^2 + 3*1^2" by auto
moreover have "zgcd(s,1) = 1" by (unfold zgcd_def, auto)
moreover have "?p ∈ zOdd"
proof -
have "?p = 2*(3*m)+1" by simp
thus ?thesis by (unfold zOdd_def, blast)
qed
moreover from p have "zprime ?p" by simp
ultimately have "is_qfN ?p 3" by (simp only: qf3_oddprimedivisor)
thus ?thesis by (unfold is_qfN_def, auto)
qed
end
lemma abs_eq_impl_unitfactor:
¦a¦ = ¦b¦ ==> ∃u. a = u * b ∧ ¦u¦ = 1
lemma zprime_3:
zprime 3
lemma qfN_pos:
[| 1 ≤ N; is_qfN A N |] ==> 0 ≤ A
lemma qfN_zero:
[| 1 ≤ N; a ^ 2 + N * b ^ 2 = 0 |] ==> a = 0 ∧ b = 0
lemma qfN_mult1:
(a ^ 2 + N * b ^ 2) * (c ^ 2 + N * d ^ 2) =
(a * c + N * b * d) ^ 2 + N * (a * d - b * c) ^ 2
lemma qfN_mult2:
(a ^ 2 + N * b ^ 2) * (c ^ 2 + N * d ^ 2) =
(a * c - N * b * d) ^ 2 + N * (a * d + b * c) ^ 2
corollary is_qfN_mult:
[| is_qfN A N; is_qfN B N |] ==> is_qfN (A * B) N
corollary is_qfN_power:
[| 0 < n; is_qfN A N |] ==> is_qfN (A ^ n) N
lemma qfN_div_prime:
zprime (p ^ 2 + N * q ^ 2) ∧ p ^ 2 + N * q ^ 2 dvd a ^ 2 + N * b ^ 2
==> ∃u v. a ^ 2 + N * b ^ 2 = (u ^ 2 + N * v ^ 2) * (p ^ 2 + N * q ^ 2) ∧
(∃e. a = p * u + e * N * q * v ∧ b = p * v - e * q * u ∧ ¦e¦ = 1)
corollary qfN_div_prime_weak:
[| zprime (p ^ 2 + N * q ^ 2); p ^ 2 + N * q ^ 2 dvd a ^ 2 + N * b ^ 2 |]
==> ∃u v. a ^ 2 + N * b ^ 2 = (u ^ 2 + N * v ^ 2) * (p ^ 2 + N * q ^ 2)
corollary qfN_div_prime_general:
[| zprime P; P dvd A; is_qfN A N; is_qfN P N |] ==> ∃Q. A = Q * P ∧ is_qfN Q N
lemma qfN_power_div_prime:
zprime P ∧
P ∈ zOdd ∧
P dvd A ∧
P ^ n = p ^ 2 + N * q ^ 2 ∧
A ^ n = a ^ 2 + N * b ^ 2 ∧ zgcd (a, b) = 1 ∧ zgcd (p, N * q) = 1 ∧ 0 < n
==> ∃u v. a ^ 2 + N * b ^ 2 = (u ^ 2 + N * v ^ 2) * (p ^ 2 + N * q ^ 2) ∧
zgcd (u, v) = 1 ∧
(∃e. a = p * u + e * N * q * v ∧ b = p * v - e * q * u ∧ ¦e¦ = 1)
lemma qfN_primedivisor_not:
zprime P ∧ 0 < Q ∧ is_qfN (P * Q) N ∧ ¬ is_qfN P N
==> ∃R. zprime R ∧ R dvd Q ∧ ¬ is_qfN R N
lemma qfN_oddprime_cube:
[| zprime (p ^ 2 + N * q ^ 2); p ^ 2 + N * q ^ 2 ∈ zOdd; p ≠ 0; 1 ≤ N |]
==> ∃a b. (p ^ 2 + N * q ^ 2) ^ 3 = a ^ 2 + N * b ^ 2 ∧ zgcd (a, N * b) = 1
lemma qfN_prime_unique:
[| zprime (a ^ 2 + N * b ^ 2); 1 < N; a ^ 2 + N * b ^ 2 = c ^ 2 + N * d ^ 2 |]
==> ¦a¦ = ¦c¦ ∧ ¦b¦ = ¦d¦
lemma qfN_square_prime:
zprime (p ^ 2 + N * q ^ 2) ∧
1 < N ∧ (p ^ 2 + N * q ^ 2) ^ 2 = r ^ 2 + N * s ^ 2 ∧ zgcd (r, s) = 1
==> ¦r¦ = ¦p ^ 2 - N * q ^ 2¦ ∧ ¦s¦ = ¦2 * p * q¦
lemma qfN_cube_prime:
zprime (p ^ 2 + N * q ^ 2) ∧
1 < N ∧ (p ^ 2 + N * q ^ 2) ^ 3 = a ^ 2 + N * b ^ 2 ∧ zgcd (a, b) = 1
==> ¦a¦ = ¦p ^ 3 - 3 * N * p * q ^ 2¦ ∧ ¦b¦ = ¦3 * p ^ 2 * q - N * q ^ 3¦
lemma qf3_even:
a ^ 2 + 3 * b ^ 2 ∈ zEven ==> ∃B. a ^ 2 + 3 * b ^ 2 = 4 * B ∧ is_qfN B 3
lemma qf3_even_general:
[| is_qfN A 3; A ∈ zEven |] ==> ∃B. A = 4 * B ∧ is_qfN B 3
lemma qf3_oddprimedivisor_not:
zprime P ∧ P ∈ zOdd ∧ 0 < Q ∧ is_qfN (P * Q) 3 ∧ ¬ is_qfN P 3
==> ∃R. zprime R ∧ R ∈ zOdd ∧ R dvd Q ∧ ¬ is_qfN R 3
lemma qf3_oddprimedivisor:
[| zprime P; P ∈ zOdd; zgcd (a, b) = 1; P dvd a ^ 2 + 3 * b ^ 2 |]
==> is_qfN P 3
lemma qf3_cube_prime_impl_cube_form:
[| zgcd (a, b) = 1; P ^ 3 = a ^ 2 + 3 * b ^ 2; zprime P ∧ P ∈ zOdd |]
==> is_cube_form a b
lemma cube_form_mult:
[| is_cube_form a b; is_cube_form c d; ¦e¦ = 1 |]
==> is_cube_form (a * c + e * 3 * b * d) (a * d - e * b * c)
lemma qf3_cube_primelist_impl_cube_form:
[| primel ps; int_of_nat (prod ps) ∈ zOdd; zgcd (a, b) = 1;
a ^ 2 + 3 * b ^ 2 = int_of_nat (prod ps) ^ 3 |]
==> is_cube_form a b
lemma qf3_cube_impl_cube_form:
zgcd (a, b) = 1 ∧ a ^ 2 + 3 * b ^ 2 = w ^ 3 ∧ w ∈ zOdd ==> is_cube_form a b
lemma Legendre_zmult:
[| 2 < p; zprime p |] ==> Legendre (a * b) p = Legendre a p * Legendre b p
lemma Legendre_1mod6:
zprime (6 * m + 1) ==> Legendre -3 (6 * m + 1) = 1
lemma qf3_prime_exists:
zprime (6 * m + 1) ==> ∃x y. 6 * m + 1 = x ^ 2 + 3 * y ^ 2