imports Gauss

imports Gauss
begin

text

locale QR =
fixes p ::
fixes q ::
assumes p_prime:
assumes p_ge_2:
assumes q_prime:
assumes q_ge_2:
assumes pq_neq:
begin

lemma odd_p:
using p_ge_2 p_prime prime_odd_nat by blast

lemma p_ge_0:

lemma p_eq2:
using odd_p by simp

lemma odd_q:
using q_ge_2 q_prime prime_odd_nat by blast

lemma q_ge_0:

lemma q_eq2:
using odd_q by simp

lemma pq_eq2:
using odd_p odd_q by simp

lemma pq_coprime:
using pq_neq p_prime primes_coprime_nat q_prime by blast

lemma pq_coprime_int:

lemma qp_ineq:
proof -
have
using p_ge_0 by auto
then show ?thesis by auto
qed

lemma QRqp:
using QR_def QR_axioms by simp

lemma pq_commute:
by simp

lemma pq_ge_0:
using p_ge_0 q_ge_0 mult_pos_pos by blast

definition
definition
definition

abbreviation  for k :: int
abbreviation  for k :: int
abbreviation  for k :: int
abbreviation  for k :: int
abbreviation  for k :: int

abbreviation

definition
definition
definition
definition
definition
definition

definition
definition
definition
definition
definition
definition

lemma Gpq:
using p_prime pq_neq p_ge_2 q_prime
by (auto simp: GAUSS_def cong_altdef_int dest: primes_dvd_imp_eq)

lemma Gqp:

lemma QR_lemma_01:
proof
have  if  for x
proof -
from that obtain k where k:
unfolding E_def by blast
from that E_def have
by blast
then have
using Gqp GAUSS.A_def k qp_ineq by (simp add: zero_less_mult_iff)
then have
using GAUSS.C_def[of q p] Gqp k GAUSS.B_def[of q p] that GAUSS.E_def[of q p]
by (force simp: E_def)
then show ?thesis by auto
qed
then show
by auto
show
proof
fix x
assume x:
then obtain ka where ka:
by (auto simp: Gqp GAUSS.B_def GAUSS.C_def GAUSS.E_def)
then have
using Gqp p_ge_0 qp_ineq by (simp add: GAUSS.A_def Groups.mult_ac(2))
then show
using ka x Gqp q_ge_0 by (force simp: E_def GAUSS.E_def)
qed
qed

lemma QR_lemma_02:
proof -
have  if x:  and y:  and mod:  for x y
proof -
obtain p_inv where p_inv:
using pq_coprime_int cong_solve_coprime_int by blast
from x y E_def obtain kx ky where k:
using dvd_def[of p x] by blast
with x y E_def have

using greaterThanAtMost_iff mem_Collect_eq by blast+
with k have
using qp_ineq by (simp_all add: zero_less_mult_iff)
moreover from mod k have
using mod_mult_cong by blast
then have
then have
using p_inv mod_mult_cong[of   ]
by (auto simp: cong_def)
then have
unfolding cong_def by blast
ultimately show ?thesis
using cong_less_imp_eq_int k by blast
qed
then have
by (auto simp: inj_on_def)
then show ?thesis
using QR_lemma_01 card_image e_def n_def by fastforce
qed

lemma QR_lemma_03:
proof -
have
unfolding F_def pq_commute using QRqp QR.E_def[of q p] by fastforce
then have
unfolding f_def using QRqp QR.e_def[of q p] by presburger
then show ?thesis
using QRqp QR.QR_lemma_02 m_def QRqp QR.n_def by presburger
qed

definition f_1 ::
where

definition P_1 ::
where

definition g_1 ::
where

lemma P_1_lemma:
fixes res ::
assumes
shows
proof -
obtain y k1 k2 where yk:
using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce
have
using  yk(1) by simp
moreover have
using  yk(2) by simp
ultimately have res:
have y:
using yk by simp_all
from y have *:
by (auto simp add: res cong_le_nat intro: exI [of _ k1] exI [of _ k2])
from * have
using y apply (auto simp add: res of_nat_mult [symmetric] of_nat_mod [symmetric] mod_mod_cancel simp del: of_nat_mult)
apply (metis  assms(1) assms(2) cong_def mod_pos_pos_trivial nat_int of_nat_mod)
apply (metis  assms(3) assms(4) cong_def mod_pos_pos_trivial nat_int of_nat_mod)
done
then obtain x where
unfolding P_1_def
using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce
moreover have  if   for a b
proof -
from that have
using divides_mult[of   ] pq_coprime_int mod_eq_dvd_iff [of a _ b]
unfolding P_1_def by force
with that show ?thesis
using dvd_imp_le_int[of ] unfolding P_1_def by fastforce
qed
ultimately show ?thesis by auto
qed

lemma g_1_lemma:
fixes res ::
assumes
shows
using assms P_1_lemma [of res] theI' [of ] g_1_def
by auto

definition

lemma finite_BuC [simp]:

proof -
{
fix p q :: nat
have
by simp
then have
by (auto intro: rev_finite_subset)
}
then show ?thesis
qed

lemma QR_lemma_04:
using card_bij_eq[of f_1   g_1]
proof
show
proof
fix x y
assume *:
then have
using f_1_def pq_coprime_int divides_mult[of   ]
mod_eq_dvd_iff[of x _ y]
by auto
with * show
using dvd_imp_le_int[of  ] unfolding BuC_def by force
qed
show
proof
fix x y
assume *:
then have

using mem_Sigma_iff prod.collapse by fastforce+
with * show
using g_1_lemma[of x] g_1_lemma[of y] P_1_def by fastforce
qed
show
proof
fix y
assume
then obtain x where x:
by blast
then have
using g_1_lemma by fastforce
with x show
unfolding P_1_def BuC_def mem_Collect_eq using SigmaE prod.sel by fastforce
qed
qed (auto simp: finite_subset f_1_def, simp_all add: BuC_def)

lemma QR_lemma_05:
proof -
have
using p_eq2 by force+
then show ?thesis
unfolding r_def using card_cartesian_product[of  ] by presburger
qed

lemma QR_lemma_06:
proof -
have
unfolding B_def C_def BuC_def by fastforce+
then show ?thesis
unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce
qed

definition f_2::
where

lemma f_2_lemma_1:

lemma f_2_lemma_2:

lemma f_2_lemma_3:
using f_2_lemma_1[of x] image_eqI[of x f_2  S] by presburger

lemma QR_lemma_07:

proof -
have 1:
by (force simp: f_2_def)
have 2:
using pq_eq2 by (fastforce simp: f_2_def)
from 2 have 3:
using f_2_lemma_3 by blast
from 1 have 4:
using f_2_lemma_3 by blast
from 1 3 show
by blast
from 2 4 show
by blast
qed

lemma QR_lemma_08:

using f_2_lemma_2[of x] cong_def[of   p] minus_mod_self2[of x p]
zmod_zminus1_eq_if[of x p] p_eq2
by auto

lemma QR_lemma_09:

using QRqp QR.QR_lemma_08 f_2_def QR.f_2_def pq_commute by auto

lemma QR_lemma_10:
unfolding a_def c_def
apply (rule card_bij_eq[of f_2 A C f_2])
unfolding A_def C_def
using QR_lemma_07 QR_lemma_08 QR_lemma_09 apply ((simp add: inj_on_def f_2_def), blast)+
apply fastforce+
done

definition
definition

definition f_3 ::
where

definition g_3 ::
where

lemma QR_lemma_11:
using card_bij_eq[of f_3 BuDuF  g_3]
proof
show
proof
fix y
assume
then obtain x where x:
by blast
then have
unfolding BuDuF_def using p_eq2 int_distrib(4) by auto
moreover from x have
by (auto simp: BuDuF_def)
moreover have
by (subst div_mult1_eq) (simp add: odd_q)
then have
by fastforce
ultimately have
by linarith
then have
using mult.commute[of  ] p_ge_0 div_mult_mod_eq[of x p]
and mult_less_cancel_left_pos[of p  ]
by linarith
moreover from x have
using pos_imp_zdiv_neg_iff[of p x] p_ge_0 by (auto simp: BuDuF_def)
ultimately show
using x by (auto simp: BuDuF_def f_3_def)
qed
show
proof
have *:  if  for x
proof -
from that have *:
by force
from that have
by auto
with * show
qed
fix x y
assume
from this *[of x] *[of y] show
by presburger
qed
show
proof
fix y
assume
then obtain x where x:  and y:
by blast
then have
by force
moreover have
using int_distrib(4) div_mult1_eq[of   2] odd_q by fastforce
ultimately have
using mult_right_mono[of   p] mult.commute[of  p]
pq_commute
by presburger
then have
using p_ge_0 int_distrib(3) by auto
moreover from x have  by force
ultimately have
using pq_commute by linarith
moreover from x have
by fastforce+
ultimately show
unfolding BuDuF_def using q_ge_0 x g_3_def y by auto
qed
show  unfolding BuDuF_def by fastforce
qed (simp add: inj_on_inverseI[of BuDuF g_3] f_3_def g_3_def QR_lemma_05)+

lemma QR_lemma_12:
proof -
have
unfolding B_def D_def BuD_def by fastforce+
then have
unfolding b_def d_def using card_Un_Int by fastforce
moreover have
unfolding BuD_def F_def by fastforce+
moreover have
unfolding BuD_def F_def BuDuF_def
using q_ge_0 ivl_disj_un_singleton(5)[of 0 ] by auto
ultimately show ?thesis
using QR_lemma_03 QR_lemma_05 QR_lemma_11 card_Un_disjoint[of BuD F]
unfolding b_def d_def f_def
by presburger
qed

lemma QR_lemma_13:
proof -
have
unfolding A_def pq_commute using QRqp QR.B_def[of q p] by blast
then have
using a_def QRqp QR.b_def[of q p] by presburger
moreover have
unfolding D_def pq_commute using QRqp QR.D_def[of q p] by blast
then have
using d_def  QRqp QR.d_def[of q p] by presburger
moreover have
using n_def QRqp QR.m_def[of q p] by presburger
moreover have
unfolding r_def using QRqp QR.r_def[of q p] by auto
ultimately show ?thesis
using QRqp QR.QR_lemma_12 by presburger
qed

lemma QR_lemma_14:
proof -
have
using QR_lemma_06 QR_lemma_10 QR_lemma_12 QR_lemma_13 by auto
then show ?thesis
qed

using Gpq Gqp GAUSS.gauss_lemma power_add[of  m n] QR_lemma_14
unfolding r_def m_def n_def by auto

end

assumes
shows
using QR.Quadratic_Reciprocity QR_def assms by blast

assumes
shows
proof -
from assms have  by simp
moreover have
by fastforce+
ultimately have
using nat_mult_distrib by presburger
moreover have
using assms by linarith+
ultimately show ?thesis
using Quadratic_Reciprocity[of  ] assms by presburger
qed

end