Up to index of Isabelle/HOL/SumSquares
theory FourSquares(* Title: FourSquares.thy
Author: Roelof Oosterhuis
2007 Rijksuniversiteit Groningen
*)
header {* Lagrange's four-square theorem *}
theory FourSquares
imports IntNatAux InfDesc
"~~/src/HOL/NumberTheory/Quadratic_Reciprocity"
begin
text {* Shows that all nonnegative integers can be written as the sum of four squares. The proof consists of the following steps:
\begin{itemize}\item For every prime $p=2n+1$ the two sets of residue classes $$\{x^2 \bmod p\mid 0\le x\le n\} ~{\rm and}~ \{-1-y^2 \bmod p \mid 0 \le y \le n\}$$ both contain $n+1$ different elements and therefore they must have at least one element in common.
\item Hence there exist $x,y$ such that $x^2+y^2+1^2+0^2$ is a multiple of $p$.
\item The next step is to show, by an infinite descent, that $p$ itself can be written as the sum of four squares.
\item Finally, using the multiplicity of this form, the same holds for all positive numbers.
\end{itemize} *}
constdefs
sum4sq :: "int × int × int × int => int"
"sum4sq == λ(a,b,c,d). a^2+b^2+c^2+d^2"
is_sum4sq :: "int => bool"
"is_sum4sq x == ∃ a b c d. sum4sq(a,b,c,d) = x"
lemma mult_sum4sq: "sum4sq(a,b,c,d) * sum4sq(p,q,r,s) =
sum4sq(a*p+b*q+c*r+d*s, a*q-b*p-c*s+d*r,
a*r+b*s-c*p-d*q, a*s-b*r+c*q-d*p)"
by (unfold sum4sq_def, simp add: nat_number ring_simps)
lemma is_mult_sum4sq: "is_sum4sq x ==> is_sum4sq y ==> is_sum4sq (x*y)"
by (unfold is_sum4sq_def, auto simp only: mult_sum4sq, blast)
lemma mult_oddprime_is_sum4sq: "[| zprime p; p ∈ zOdd |] ==>
∃ t. 0<t ∧ t<p ∧ is_sum4sq (p*t)"
proof -
assume p1: "zprime p"
hence p0: "p > 1" by (simp add: zprime_def)
assume p2: "p ∈ zOdd"
then obtain n where n: "p = 2*n+1" by (auto simp add: zOdd_def)
with p1 have n0: "n > 0" by (auto simp add: zprime_def)
let ?C = "{y. 0 ≤ y ∧ y < p}"
let ?D = "{y. 0 ≤ y ∧ y ≤ n}"
let ?f = "%x. x^2 mod p"
let ?g = "%x. (-1-x^2) mod p"
let ?A = "?f ` ?D"
let ?B = "?g ` ?D"
have finC: "finite ?C" by (rule bdd_int_set_l_finite)
have finD: "finite ?D" by (rule bdd_int_set_le_finite)
from p0 have AsubC: "?A ⊆ ?C" and BsubC: "?B ⊆ ?C"
by (auto simp add: pos_mod_conj)
with finC have finA: "finite ?A" and finB: "finite ?B"
by (auto simp add: finite_subset)
from AsubC BsubC have AunBsubC: "?A ∪ ?B ⊆ ?C" by (rule Un_least)
from p0 have cardC: "card ?C = nat p" by (simp only: card_bdd_int_set_l)
from n0 have cardD: "card ?D = 1+ nat n" by (simp only: card_bdd_int_set_le)
have cardA: "card ?A = card ?D"
proof -
have "inj_on ?f ?D"
proof (unfold inj_on_def, auto)
fix x fix y
assume x0: "0 ≤ x" and xn: "x ≤ n" and y0: "0 ≤ y" and yn: " y ≤ n"
and xyp: "x^2 mod p = y^2 mod p"
with p0 have "[x^2 = y^2] (mod p)" by (simp only: zcong_zmod_eq)
hence "p dvd x^2-y^2" by (simp only: zcong_def)
hence "p dvd (x+y)*(x-y)" by (simp only: zspecial_product)
with p1 have "p dvd x+y ∨ p dvd x-y" by (simp only: zprime_zdvd_zmult_general)
moreover
{ assume "p dvd x+y"
moreover from xn yn n have "x+y < p" by auto
ultimately have "¬ x+y > 0" by (auto simp add: zdvd_not_zless)
with x0 y0 have "x = y" by auto } -- "both are zero"
moreover
{ assume ass: "p dvd x-y"
have "x = y"
proof (rule ccontr, case_tac "x-y ≥ 0", auto)
assume "x-y ≥ 0" and "x ≠ y" hence "x-y > 0" by auto
with ass have "¬ x-y < p" by (auto simp add: zdvd_not_zless)
with xn y0 n p0 show "False" by auto
next
assume "¬ 0 ≤ x-y" hence "y-x > 0" by auto
moreover from x0 yn n p0 have "y-x < p" by auto
ultimately have "¬ p dvd y-x" by (auto simp add: zdvd_not_zless)
moreover from ass have "p dvd -(x-y)" by (simp only: zdvd_zminus_iff)
ultimately show "False" by auto
qed }
ultimately show "x=y" by auto
qed
with finD show ?thesis by (simp only: inj_on_iff_eq_card)
qed
have cardB: "card ?B = card ?D"
proof -
have "inj_on ?g ?D"
proof (unfold inj_on_def, auto)
fix x fix y
assume x0: "0 ≤ x" and xn: "x ≤ n" and y0: "0 ≤ y" and yn: " y ≤ n"
and xyp: "(-1-x^2) mod p = (-1-y^2) mod p"
with p0 have "[-1-y^2 = -1-x^2] (mod p)" by (simp only: zcong_zmod_eq)
hence "p dvd (-1-y^2) - (-1-x^2)" by (simp only: zcong_def)
moreover have "-1-y^2 - (-1-x^2) = x^2 - y^2" by arith
ultimately have "p dvd x^2-y^2" by simp
hence "p dvd (x+y)*(x-y)" by (simp only: zspecial_product)
with p1 have "p dvd x+y ∨ p dvd x-y" by (simp only: zprime_zdvd_zmult_general)
moreover
{ assume "p dvd x+y"
moreover from xn yn n have "x+y < p" by auto
ultimately have "¬ x+y > 0" by (auto simp add: zdvd_not_zless)
with x0 y0 have "x = y" by auto } -- "both are zero"
moreover
{ assume ass: "p dvd x-y"
have "x = y"
proof (rule ccontr, case_tac "x-y ≥ 0", auto)
assume "x-y ≥ 0" and "x ≠ y" hence "x-y > 0" by auto
with ass have "¬ x-y < p" by (auto simp add: zdvd_not_zless)
with xn y0 n p0 show "False" by auto
next
assume "¬ 0 ≤ x-y" hence "y-x > 0" by auto
moreover from x0 yn n p0 have "y-x < p" by auto
ultimately have "¬ p dvd y-x" by (auto simp add: zdvd_not_zless)
moreover from ass have "p dvd -(x-y)" by (simp only: zdvd_zminus_iff)
ultimately show "False" by auto
qed }
ultimately show "x=y" by auto
qed
with finD show ?thesis by (simp only: inj_on_iff_eq_card)
qed
have "?A ∩ ?B ≠ {}"
proof (rule ccontr, auto)
assume ABdisj: "?A ∩ ?B = {}"
from cardA cardB cardD have "2 + 2*(nat n) = card ?A + card ?B" by auto
also with finA finB ABdisj have "… = card (?A ∪ ?B)"
by (simp only: card_Un_disjoint)
also with finC AunBsubC have "… ≤ card ?C" by (simp only: card_mono)
also with cardC have "… = nat p" by simp
finally have "2 + 2*(nat n) ≤ nat p" by simp
with n show "False" by arith
qed
then obtain z where "z ∈ ?A ∧ z ∈ ?B" by auto
then obtain x y where xy: "x ∈ ?D ∧ y ∈ ?D ∧ z = x^2 mod p ∧
z = (-1-y^2) mod p" by auto
with p0 have "[x^2=-1-y^2](mod p)" by (simp add: zcong_zmod_eq)
hence "p dvd x^2-(-1-y^2)" by (simp only: zcong_def)
moreover have "x^2-(-1-y^2)=x^2+y^2+1" by arith
ultimately have "p dvd sum4sq(x,y,1,0)" by (auto simp add: sum4sq_def)
then obtain t where t: "sum4sq(x,y,1,0) = p*t" by (auto simp add: dvd_def)
hence "is_sum4sq (p*t)" by (unfold is_sum4sq_def, auto)
moreover have "t > 0 ∧ t < p"
proof
have "x^2 ≥ 0 ∧ y^2 ≥ 0" by (simp add: zero_le_power2)
hence "x^2+y^2+1 > 0" by arith
with t have "p*t > 0" by (unfold sum4sq_def, auto)
moreover
{ assume "t < 0" with p0 have "p*t < p*0" by (simp only: zmult_zless_mono2)
hence "p*t < 0" by simp }
moreover
{ assume "t = 0" hence "p*t = 0" by simp }
ultimately have "¬ t < 0 ∧ t ≠ 0" by auto
thus "t > 0" by simp
from xy have "x^2 ≤ n^2 ∧ y^2 ≤ n^2" by (auto simp add: power_mono)
hence "x^2+y^2+1 ≤ 2*n^2 + 1" by auto
with t have contr: "p*t ≤ 2*n^2+1" by (simp add: sum4sq_def)
moreover
{ assume "t > n+1"
with p0 have "p*(n+1) < p*t" by (simp only: zmult_zless_mono2)
with n have "p*t > (2*n+1)*n + (2*n+1)*1" by (simp only: zadd_zmult_distrib2)
hence "p*t > 2*n*n + n + 2*n + 1" by (simp only: zadd_zmult_distrib zmult_1)
with n0 have "p*t > 2*n^2 + 1" by (simp add: power2_eq_square) }
ultimately have "¬ t > n+1" by auto
with n0 n show "t < p" by auto
qed
ultimately show ?thesis by blast
qed
lemma zprime_is_sum4sq: "zprime p ==> is_sum4sq p"
proof (cases)
assume p2: "p=2"
hence "p = sum4sq(1,1,0,0)" by (auto simp add: sum4sq_def)
thus ?thesis by (auto simp add: is_sum4sq_def)
next
assume "¬ p =2" and prp: "zprime p"
hence "2 < p" by (simp add: zprime_def)
with prp have "p ∈ zOdd" by (simp only: zprime_zOdd_eq_grt_2)
with prp have "∃ t. 0<t ∧ t<p ∧ is_sum4sq (p*t)"
by (rule mult_oddprime_is_sum4sq)
then obtain a b c d t where pt_sol: "0<t ∧ t<p ∧ sum4sq(a,b,c,d)=p*t"
by (unfold is_sum4sq_def, blast)
hence Qt: "0<t ∧ t<p ∧ (∃ a1 a2 a3 a4. sum4sq(a1,a2,a3,a4)=p*t)"
(is "?Q t") by blast
have "?Q 1"
proof (rule ccontr)
assume nQ1: "¬ ?Q 1"
have "¬ ?Q t"
proof (rule_tac x=t and V="λx. (nat x)- 1" in val_infinite_descent, clarify)
fix x a b c d
assume "nat x - 1 = 0" and "x > 0" and s: "sum4sq(a,b,c,d)=p*x" and "x < p"
moreover hence "x = 1" by arith
ultimately have "?Q 1" by auto
with nQ1 show False by auto
next
fix x
assume "0 < nat x - 1" and "¬ ¬ ?Q x"
then obtain a1 a2 a3 a4 where ass: "1<x ∧ x<p ∧ sum4sq(a1,a2,a3,a4)=p*x"
by auto
have "∃ y. nat y - 1 < nat x - 1 ∧ ?Q y"
proof (cases)
assume evx: "x ∈ zEven"
hence "x*p ∈ zEven" by (rule even_times_either)
with ass have ev1234: "a1^2+a2^2 + a3^2+a4^2 ∈ zEven"
by (auto simp add: sum4sq_def mult_ac)
have "∃ b1 b2 b3 b4. sum4sq(b1,b2,b3,b4)=p*x ∧
b1+b2 ∈ zEven ∧ b3+b4 ∈ zEven"
proof (cases)
assume ev12: "a1^2+a2^2 ∈ zEven"
moreover have "2*a1*a2 ∈ zEven" by (auto simp add: zEven_def)
ultimately have"a1^2+a2^2+2*a1*a2 ∈ zEven" by (rule even_plus_even)
hence "(a1+a2)^2 ∈ zEven" by (auto simp add: zadd_power2 add_ac)
hence tmp: "a1+a2 ∈ zEven" by (auto simp add: power_preserves_even)
from ev12 ev1234 have "a1^2+a2^2+a3^2+a4^2-(a1^2+a2^2) ∈ zEven"
by (simp only: even_minus_even)
hence "a3^2+a4^2 ∈ zEven" by auto
moreover have "2*a3*a4 ∈ zEven" by (auto simp add: zEven_def)
ultimately have"a3^2+a4^2+2*a3*a4 ∈ zEven" by (rule even_plus_even)
hence "(a3+a4)^2 ∈ zEven" by (auto simp add: zadd_power2 add_ac)
hence "a3+a4 ∈ zEven" by (auto simp add: power_preserves_even)
with tmp ass show ?thesis by blast
next
assume "¬ a1^2+a2^2 ∈ zEven"
hence odd12: "a1^2+a2^2 ∈ zOdd" by (simp add: odd_iff_not_even)
with ev1234 have "a1^2+a2^2+a3^2+a4^2-(a1^2+a2^2) ∈ zOdd"
by (simp only: even_minus_odd)
hence odd34: "a3^2+a4^2 ∈ zOdd" by auto
show ?thesis
proof (cases)
assume ev1: "a1^2 ∈ zEven"
with odd12 have odd2: "a2^2 ∈ zOdd" by (rule even_plus_odd_prop2)
show ?thesis
proof (cases)
assume ev3: "a3^2 ∈ zEven"
with odd34 have "a4^2 ∈ zOdd" by (rule even_plus_odd_prop2)
with odd2 have "a2 ∈ zOdd ∧ a4 ∈ zOdd"
by (auto simp add: power_preserves_odd)
hence tmp: "a2+a4 ∈ zEven" by (simp only: odd_plus_odd)
from ev3 ev1 have "a1 ∈ zEven ∧ a3 ∈ zEven"
by (auto simp add: power_preserves_even)
hence tmp2: "a1+a3 ∈ zEven" by (simp only: even_plus_even)
from ass have "sum4sq(a1,a3,a2,a4)=p*x"
by (auto simp add: sum4sq_def)
with tmp tmp2 show ?thesis by blast
next
assume "¬ a3^2 ∈ zEven"
hence odd3: "a3^2 ∈ zOdd" by (simp add: odd_iff_not_even)
with odd34 have "a4^2 ∈ zEven" by (rule even_plus_odd_prop1)
with ev1 have "a1 ∈ zEven ∧ a4 ∈ zEven"
by (auto simp add: power_preserves_even)
hence tmp: "a1+a4 ∈ zEven" by (simp only: even_plus_even)
from odd2 odd3 have "a2 ∈ zOdd ∧ a3 ∈ zOdd"
by (auto simp add: power_preserves_odd)
hence tmp2: "a2+a3 ∈ zEven" by (simp only: odd_plus_odd)
from ass have "sum4sq(a1,a4,a2,a3)=p*x"
by (auto simp add: sum4sq_def)
with tmp tmp2 show ?thesis by blast
qed
next
assume "¬ a1^2 ∈ zEven"
hence odd1: "a1^2 ∈ zOdd" by (simp add: odd_iff_not_even)
with odd12 have ev2: "a2^2 ∈ zEven" by (rule even_plus_odd_prop1)
show ?thesis
proof (cases)
assume ev3: "a3^2 ∈ zEven"
with odd34 have "a4^2 ∈ zOdd" by (rule even_plus_odd_prop2)
with odd1 have "a1 ∈ zOdd ∧ a4 ∈ zOdd"
by (auto simp add: power_preserves_odd)
hence tmp: "a1+a4 ∈ zEven" by (simp only: odd_plus_odd)
from ev3 ev2 have "a2 ∈ zEven ∧ a3 ∈ zEven"
by (auto simp add: power_preserves_even)
hence tmp2: "a2+a3 ∈ zEven" by (simp only: even_plus_even)
from ass have "sum4sq(a1,a4,a2,a3)=p*x"
by (auto simp add: sum4sq_def)
with tmp tmp2 show ?thesis by blast
next
assume "¬ a3^2 ∈ zEven"
hence odd3: "a3^2 ∈ zOdd" by (simp add: odd_iff_not_even)
with odd34 have "a4^2 ∈ zEven" by (rule even_plus_odd_prop1)
with ev2 have "a2 ∈ zEven ∧ a4 ∈ zEven"
by (auto simp add: power_preserves_even)
hence tmp: "a2+a4 ∈ zEven" by (simp only: even_plus_even)
from odd1 odd3 have "a1 ∈ zOdd ∧ a3 ∈ zOdd"
by (auto simp add: power_preserves_odd)
hence tmp2: "a1+a3 ∈ zEven" by (simp only: odd_plus_odd)
from ass have "sum4sq(a1,a3,a2,a4)=p*x"
by (auto simp add: sum4sq_def)
with tmp tmp2 show ?thesis by blast
qed
qed
qed
then obtain b1 b2 b3 b4 where b: "sum4sq(b1,b2,b3,b4)=p*x ∧
b1+b2 ∈ zEven ∧ b3+b4 ∈ zEven" by auto
then obtain c1 c3 where c13: "b1+b2 = 2*c1 ∧ b3+b4 = 2*c3"
by (auto simp add: zEven_def)
have "2*b2 ∈ zEven ∧ 2*b4 ∈ zEven" by (auto simp add: zEven_def)
with b have "b1+b2 - 2*b2 ∈ zEven ∧ b3+b4 - 2*b4 ∈ zEven"
by (auto simp only: even_minus_even)
moreover have "b1+b2 - 2*b2 = b1-b2 ∧ b3+b4 - 2*b4 = b3-b4" by auto
ultimately have "b1-b2 ∈ zEven ∧ b3-b4 ∈ zEven" by simp
then obtain c2 c4 where c24: "b1-b2 = 2*c2 ∧ b3-b4 = 2*c4"
by (auto simp add: zEven_def)
from evx obtain y where y: "x = 2*y" by (auto simp add: zEven_def)
hence "4*(p*y) = 2*(p*x)" by (simp add: mult_ac)
also from b have "… = 2*b1^2 + 2*b2^2 + 2*b3^2 + 2*b4^2"
by (auto simp only: sum4sq_def)
also have "… = (b1 + b2)^2 + (b1 - b2)^2 + (b3 + b4)^2 + (b3 - b4)^2"
by (auto simp add: zadd_power2 zdiff_power2)
also with c13 c24 have "… = 4*(c1^2 + c2^2 + c3^2 + c4^2)"
by (auto simp add: power_mult_distrib)
finally have "sum4sq(c1,c2,c3,c4) = p*y" by (auto simp add: sum4sq_def)
moreover from y ass have "0 < y ∧ y < p ∧ (nat y) - 1 < (nat x) - 1" by arith
ultimately show ?thesis by blast
next
assume "¬ x ∈ zEven"
hence xodd: "x ∈ zOdd" by (simp add: odd_iff_not_even)
with ass have "∃ c1 c2 c3 c4. 2*¦a1-c1*x¦<x ∧ 2*¦a2-c2*x¦<x
∧ 2*¦a3-c3*x¦<x ∧ 2*¦a4-c4*x¦<x"
by (simp add: best_odd_division_abs)
then obtain b1 c1 b2 c2 b3 c3 b4 c4 where
bc_def: "b1 = a1-c1*x ∧ b2 = a2-c2*x ∧ b3 = a3-c3*x ∧ b4 = a4-c4*x"
and bc_abs: "2*¦b1¦<x ∧ 2*¦b2¦<x ∧ 2*¦b3¦<x ∧ 2*¦b4¦<x"
by blast
let ?B = "b1^2 + b2^2 + b3^2 + b4^2"
let ?C = "c1^2 + c2^2 + c3^2 + c4^2"
have "x dvd ?B"
proof
from bc_def ass have
"?B = p*x - 2*(a1*c1+a2*c2+a3*c3+a4*c4)*x + ?C*x^2"
by (auto simp add: zdiff_power2 sum4sq_def
zadd_zmult_distrib power_mult_distrib)
thus "?B = x*(p - 2*(a1*c1+a2*c2+a3*c3+a4*c4) + ?C*x)"
by (auto simp add: mult_ac power2_eq_square
zadd_zmult_distrib2 zdiff_zmult_distrib2)
qed
then obtain y where y: "?B = x * y" by (auto simp add: dvd_def)
let ?A1 = "a1*b1 + a2*b2 + a3*b3 + a4*b4"
let ?A2 = "a1*b2 - a2*b1 - a3*b4 + a4*b3"
let ?A3 = "a1*b3 + a2*b4 - a3*b1 - a4*b2"
let ?A4 = "a1*b4 - a2*b3 + a3*b2 - a4*b1"
let ?A = "sum4sq(?A1,?A2,?A3,?A4)"
have "x dvd ?A1 ∧ x dvd ?A2 ∧ x dvd ?A3 ∧ x dvd ?A4"
proof (safe)
from bc_def have
"?A1 = (b1+c1*x)*b1 + (b2+c2*x)*b2 + (b3+c3*x)*b3 + (b4+c4*x)*b4"
by simp
also with y have "… = x*(y + c1*b1 + c2*b2 + c3*b3 + c4*b4)"
by (auto simp add: zadd_zmult_distrib2 power2_eq_square mult_ac)
finally show "x dvd ?A1" by auto
from bc_def have
"?A2 = (b1+c1*x)*b2 - (b2+c2*x)*b1 - (b3+c3*x)*b4 + (b4+c4*x)*b3"
by simp
also have "… = x*(c1*b2 - c2*b1 - c3*b4 + c4*b3)"
by (auto simp add: zadd_zmult_distrib2 zdiff_zmult_distrib2 mult_ac)
finally show "x dvd ?A2" by auto
from bc_def have
"?A3 = (b1+c1*x)*b3 + (b2+c2*x)*b4 - (b3+c3*x)*b1 - (b4+c4*x)*b2"
by simp
also have "… = x*(c1*b3 + c2*b4 - c3*b1 - c4*b2)"
by (auto simp add: zadd_zmult_distrib2 zdiff_zmult_distrib2 mult_ac)
finally show "x dvd ?A3" by auto
from bc_def have
"?A4 = (b1+c1*x)*b4 - (b2+c2*x)*b3 + (b3+c3*x)*b2 - (b4+c4*x)*b1"
by simp
also have "… = x*(c1*b4 - c2*b3 + c3*b2 - c4*b1)"
by (auto simp add: zadd_zmult_distrib2 zdiff_zmult_distrib2 mult_ac)
finally show "x dvd ?A4" by auto
qed
then obtain d1 d2 d3 d4 where d:
"?A1=x*d1 ∧ ?A2=x*d2 ∧ ?A3=x*d3 ∧ ?A4=x*d4"
by (auto simp add: dvd_def)
let ?D = "sum4sq(d1,d2,d3,d4)"
from d have "x^2*?D = ?A"
by (auto simp only: sum4sq_def power_mult_distrib zadd_zmult_distrib2)
also have "… = sum4sq(a1,a2,a3,a4)*sum4sq(b1,b2,b3,b4)"
by (simp only: mult_sum4sq)
also with y ass have "… = (p*x)*(x*y)" by (auto simp add: sum4sq_def)
also have "… = x^2*(p*y)" by (simp only: power2_eq_square mult_ac)
finally have "x^2*(?D - p*y) = 0" by (auto simp add: zdiff_zmult_distrib2)
with ass have "?D = p*y" by auto
moreover have y_l_x: "y < x"
proof -
have "4*b1^2 = (2*¦b1¦)^2 ∧ 4*b2^2 = (2*¦b2¦)^2 ∧
4*b3^2 = (2*¦b3¦)^2 ∧ 4*b4^2 = (2*¦b4¦)^2"
by (auto simp add: power_mult_distrib abs_mult power2_abs)
with bc_abs have "4*b1^2<x^2 ∧ 4*b2^2<x^2 ∧ 4*b3^2<x^2 ∧ 4*b4^2<x^2"
by (auto simp add: power_strict_mono)
hence "?B < x^2" by auto
with y have "x*(x-y) > 0"
by (auto simp add: power2_eq_square zdiff_zmult_distrib2)
moreover from ass have "x > 0" by simp
ultimately show ?thesis by (auto dest: pos_zmult_pos)
qed
moreover have "y > 0"
proof -
have b2pos: "b1^2 ≥ 0 ∧ b2^2 ≥ 0 ∧ b3^2 ≥ 0 ∧ b4^2 ≥ 0"
by (auto simp add: zero_le_power2)
hence "?B = 0 ∨ ?B > 0" by arith
moreover
{ assume "?B = 0"
moreover from b2pos have
"?B-b1^2 ≥ 0 ∧ ?B-b2^2 ≥ 0 ∧ ?B-b3^2 ≥ 0 ∧ ?B-b4^2 ≥ 0" by arith
ultimately have "b1^2 ≤ 0 ∧ b2^2 ≤ 0 ∧ b3^2 ≤ 0 ∧ b4^2 ≤ 0" by auto
with b2pos have "b1^2 = 0 ∧ b2^2 = 0 ∧ b3^2 = 0 ∧ b4^2 = 0" by arith
hence "b1 = 0 ∧ b2 = 0 ∧ b3 = 0 ∧ b4 = 0" by auto
with bc_def have "x dvd a1 ∧ x dvd a2 ∧ x dvd a3 ∧ x dvd a4"
by (auto simp add: zdvd_triv_right)
hence "x^2 dvd a1^2 ∧ x^2 dvd a2^2 ∧ x^2 dvd a3^2 ∧ x^2 dvd a4^2"
by (auto simp only: zpower_zdvd_mono)
hence "x^2 dvd a1^2+a2^2+a3^2+a4^2" by (simp only: zdvd_zadd)
with ass have "x^2 dvd p*x" by (auto simp only: sum4sq_def)
hence "x*x dvd x*p" by (simp only: power2_eq_square mult_ac)
with ass have "x dvd p" by (auto dest: zdvd_mult_cancel)
moreover from ass prp have "x ≥ 0 ∧ x ≠ 1 ∧ x ≠ p ∧ zprime p" by simp
ultimately have "False" by (unfold zprime_def, auto) }
moreover
{ assume "?B > 0"
with y have "x*y > 0" by simp
moreover from ass have "x > 0" by simp
ultimately have ?thesis by (auto dest: pos_zmult_pos) }
ultimately show ?thesis by auto
qed
moreover with y_l_x have "(nat y) - 1 < (nat x) - 1" by arith
moreover from y_l_x ass have "y < p" by auto
ultimately show ?thesis by blast
qed
thus "∃ y. nat y - 1 < nat x - 1 ∧ ¬ ¬ ?Q y" by blast
qed
with Qt show "False" by simp
qed
thus "is_sum4sq p" by (auto simp add: is_sum4sq_def)
qed
theorem four_squares: "(n::int) ≥ 0 ==> ∃ a b c d. a^2 + b^2 + c^2 + d^2 = n"
proof -
assume "n ≥ 0"
hence "n = 0 ∨ n > 0" by auto
moreover
{ assume "n = 0"
hence "n = sum4sq(0,0,0,0)" by (auto simp add: sum4sq_def)
hence "is_sum4sq n" by (auto simp add: is_sum4sq_def) }
moreover
{ assume npos: "n > 0"
hence "nat n ≠ 0" by simp
then obtain ps where ps: "primel ps ∧ prod ps = nat n"
by (frule_tac a="nat n" in factor_exists_general, auto)
have "primel ps ==> is_sum4sq (int (prod ps))"
proof (induct ps, auto)
have "sum4sq(1,0,0,0) = 1" by (auto simp add: sum4sq_def)
thus "is_sum4sq 1" by (auto simp add: is_sum4sq_def)
next
fix p ps
let ?X = "int (prod ps)"
assume "primel ps ==> is_sum4sq ?X" and "primel (p#ps)"
hence "prime p" and x: "is_sum4sq ?X" by (auto simp add: primel_hd_tl)
hence "zprime (int p)" by (simp only: prime_impl_zprime_int)
hence "is_sum4sq (int p)" by (rule zprime_is_sum4sq)
with x have "is_sum4sq((int p)*?X)" by (simp add: is_mult_sum4sq)
thus "is_sum4sq (int (p*prod ps))" by (auto simp only: int_mult)
qed
with ps npos have "is_sum4sq n" by auto }
ultimately have "is_sum4sq n" by auto
thus ?thesis by (auto simp only: is_sum4sq_def sum4sq_def)
qed
end
lemma mult_sum4sq:
sum4sq (a, b, c, d) * sum4sq (p, q, r, s) =
sum4sq
(a * p + b * q + c * r + d * s, a * q - b * p - c * s + d * r,
a * r + b * s - c * p - d * q, a * s - b * r + c * q - d * p)
lemma is_mult_sum4sq:
[| is_sum4sq x; is_sum4sq y |] ==> is_sum4sq (x * y)
lemma mult_oddprime_is_sum4sq:
[| zprime p; p ∈ zOdd |] ==> ∃t>0. t < p ∧ is_sum4sq (p * t)
lemma zprime_is_sum4sq:
zprime p ==> is_sum4sq p
theorem four_squares:
0 ≤ n ==> ∃a b c d. a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n