--- a/src/HOL/Number_Theory/Gauss.thy Thu Apr 06 16:08:48 2017 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy Thu Apr 06 21:01:39 2017 +0200
@@ -1,33 +1,33 @@
-(* Authors: Jeremy Avigad, David Gray, and Adam Kramer
+(* Title: HOL/Number_Theory/Quadratic_Reciprocity.thy
+ Authors: Jeremy Avigad, David Gray, and Adam Kramer
-Ported by lcp but unfinished
+Ported by lcp but unfinished.
*)
section \<open>Gauss' Lemma\<close>
theory Gauss
-imports Euler_Criterion
+ imports Euler_Criterion
begin
-lemma cong_prime_prod_zero_nat:
- fixes a::nat
- shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
+lemma cong_prime_prod_zero_nat:
+ "[a * b = 0] (mod p) \<Longrightarrow> prime p \<Longrightarrow> [a = 0] (mod p) \<or> [b = 0] (mod p)"
+ for a :: nat
by (auto simp add: cong_altdef_nat prime_dvd_mult_iff)
-lemma cong_prime_prod_zero_int:
- fixes a::int
- shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
+lemma cong_prime_prod_zero_int:
+ "[a * b = 0] (mod p) \<Longrightarrow> prime p \<Longrightarrow> [a = 0] (mod p) \<or> [b = 0] (mod p)"
+ for a :: int
by (auto simp add: cong_altdef_int prime_dvd_mult_iff)
locale GAUSS =
fixes p :: "nat"
fixes a :: "int"
-
assumes p_prime: "prime p"
assumes p_ge_2: "2 < p"
assumes p_a_relprime: "[a \<noteq> 0](mod p)"
- assumes a_nonzero: "0 < a"
+ assumes a_nonzero: "0 < a"
begin
definition "A = {0::int <.. ((int p - 1) div 2)}"
@@ -41,47 +41,51 @@
subsection \<open>Basic properties of p\<close>
lemma odd_p: "odd p"
-by (metis p_prime p_ge_2 prime_odd_nat)
+ by (metis p_prime p_ge_2 prime_odd_nat)
lemma p_minus_one_l: "(int p - 1) div 2 < p"
proof -
have "(p - 1) div 2 \<le> (p - 1) div 1"
by (metis div_by_1 div_le_dividend)
also have "\<dots> = p - 1" by simp
- finally show ?thesis using p_ge_2 by arith
+ finally show ?thesis
+ using p_ge_2 by arith
qed
lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
- using odd_p p_ge_2 nonzero_mult_div_cancel_left [of 2 "p - 1"]
- by simp
+ using odd_p p_ge_2 nonzero_mult_div_cancel_left [of 2 "p - 1"] by simp
-lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
- using odd_p p_ge_2
- by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2)
+lemma p_odd_int: obtains z :: int where "int p = 2 * z + 1" "0 < z"
+proof
+ let ?z = "(int p - 1) div 2"
+ show "int p = 2 * ?z + 1" by (rule p_eq2)
+ show "0 < ?z"
+ using p_ge_2 by linarith
+qed
subsection \<open>Basic Properties of the Gauss Sets\<close>
-lemma finite_A: "finite (A)"
-by (auto simp add: A_def)
+lemma finite_A: "finite A"
+ by (auto simp add: A_def)
-lemma finite_B: "finite (B)"
-by (auto simp add: B_def finite_A)
+lemma finite_B: "finite B"
+ by (auto simp add: B_def finite_A)
-lemma finite_C: "finite (C)"
-by (auto simp add: C_def finite_B)
+lemma finite_C: "finite C"
+ by (auto simp add: C_def finite_B)
-lemma finite_D: "finite (D)"
-by (auto simp add: D_def finite_C)
+lemma finite_D: "finite D"
+ by (auto simp add: D_def finite_C)
-lemma finite_E: "finite (E)"
-by (auto simp add: E_def finite_C)
+lemma finite_E: "finite E"
+ by (auto simp add: E_def finite_C)
-lemma finite_F: "finite (F)"
-by (auto simp add: F_def finite_E)
+lemma finite_F: "finite F"
+ by (auto simp add: F_def finite_E)
lemma C_eq: "C = D \<union> E"
-by (auto simp add: C_def D_def E_def)
+ by (auto simp add: C_def D_def E_def)
lemma A_card_eq: "card A = nat ((int p - 1) div 2)"
by (auto simp add: A_def)
@@ -89,83 +93,86 @@
lemma inj_on_xa_A: "inj_on (\<lambda>x. x * a) A"
using a_nonzero by (simp add: A_def inj_on_def)
-definition ResSet :: "int => int set => bool"
- where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
+definition ResSet :: "int \<Rightarrow> int set \<Rightarrow> bool"
+ where "ResSet m X \<longleftrightarrow> (\<forall>y1 y2. y1 \<in> X \<and> y2 \<in> X \<and> [y1 = y2] (mod m) \<longrightarrow> y1 = y2)"
lemma ResSet_image:
- "\<lbrakk> 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) \<rbrakk> \<Longrightarrow>
- ResSet m (f ` A)"
+ "0 < m \<Longrightarrow> ResSet m A \<Longrightarrow> \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) \<longrightarrow> x = y) \<Longrightarrow> ResSet m (f ` A)"
by (auto simp add: ResSet_def)
lemma A_res: "ResSet p A"
- using p_ge_2
- by (auto simp add: A_def ResSet_def intro!: cong_less_imp_eq_int)
+ using p_ge_2 by (auto simp add: A_def ResSet_def intro!: cong_less_imp_eq_int)
lemma B_res: "ResSet p B"
proof -
- {fix x fix y
- assume a: "[x * a = y * a] (mod p)"
- assume b: "0 < x"
- assume c: "x \<le> (int p - 1) div 2"
- assume d: "0 < y"
- assume e: "y \<le> (int p - 1) div 2"
- from p_a_relprime have "\<not>p dvd a"
+ have *: "x = y"
+ if a: "[x * a = y * a] (mod p)"
+ and b: "0 < x"
+ and c: "x \<le> (int p - 1) div 2"
+ and d: "0 < y"
+ and e: "y \<le> (int p - 1) div 2"
+ for x y
+ proof -
+ from p_a_relprime have "\<not> p dvd a"
by (simp add: cong_altdef_int)
- with p_prime have "coprime a (int p)"
- by (subst gcd.commute, intro prime_imp_coprime) auto
- with a cong_mult_rcancel_int [of a "int p" x y]
- have "[x = y] (mod p)" by simp
+ with p_prime have "coprime a (int p)"
+ by (subst gcd.commute, intro prime_imp_coprime) auto
+ with a cong_mult_rcancel_int [of a "int p" x y] have "[x = y] (mod p)"
+ by simp
with cong_less_imp_eq_int [of x y p] p_minus_one_l
- order_le_less_trans [of x "(int p - 1) div 2" p]
- order_le_less_trans [of y "(int p - 1) div 2" p]
- have "x = y"
+ order_le_less_trans [of x "(int p - 1) div 2" p]
+ order_le_less_trans [of y "(int p - 1) div 2" p]
+ show ?thesis
by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
- } note xy = this
+ qed
show ?thesis
apply (insert p_ge_2 p_a_relprime p_minus_one_l)
apply (auto simp add: B_def)
apply (rule ResSet_image)
- apply (auto simp add: A_res)
- apply (auto simp add: A_def xy)
+ apply (auto simp add: A_res)
+ apply (auto simp add: A_def *)
done
- qed
+qed
lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B"
proof -
-{ fix x fix y
- assume a: "x * a mod p = y * a mod p"
- assume b: "0 < x"
- assume c: "x \<le> (int p - 1) div 2"
- assume d: "0 < y"
- assume e: "y \<le> (int p - 1) div 2"
- assume f: "x \<noteq> y"
- from a have a': "[x * a = y * a](mod p)"
- by (metis cong_int_def)
- from p_a_relprime have "\<not>p dvd a"
- by (simp add: cong_altdef_int)
- with p_prime have "coprime a (int p)"
- by (subst gcd.commute, intro prime_imp_coprime) auto
- with a' cong_mult_rcancel_int [of a "int p" x y]
+ have False
+ if a: "x * a mod p = y * a mod p"
+ and b: "0 < x"
+ and c: "x \<le> (int p - 1) div 2"
+ and d: "0 < y"
+ and e: "y \<le> (int p - 1) div 2"
+ and f: "x \<noteq> y"
+ for x y
+ proof -
+ from a have a': "[x * a = y * a](mod p)"
+ by (metis cong_int_def)
+ from p_a_relprime have "\<not>p dvd a"
+ by (simp add: cong_altdef_int)
+ with p_prime have "coprime a (int p)"
+ by (subst gcd.commute, intro prime_imp_coprime) auto
+ with a' cong_mult_rcancel_int [of a "int p" x y]
have "[x = y] (mod p)" by simp
- with cong_less_imp_eq_int [of x y p] p_minus_one_l
- order_le_less_trans [of x "(int p - 1) div 2" p]
- order_le_less_trans [of y "(int p - 1) div 2" p]
- have "x = y"
- by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
- then have False
- by (simp add: f)}
+ with cong_less_imp_eq_int [of x y p] p_minus_one_l
+ order_le_less_trans [of x "(int p - 1) div 2" p]
+ order_le_less_trans [of y "(int p - 1) div 2" p]
+ have "x = y"
+ by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
+ then show ?thesis
+ by (simp add: f)
+ qed
then show ?thesis
by (auto simp add: B_def inj_on_def A_def) metis
qed
lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E"
apply (auto simp add: E_def C_def B_def A_def)
- apply (rule_tac g = "(op - (int p))" in inj_on_inverseI)
+ apply (rule inj_on_inverseI [where g = "op - (int p)"])
apply auto
done
-lemma nonzero_mod_p:
- fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)"
+lemma nonzero_mod_p: "0 < x \<Longrightarrow> x < int p \<Longrightarrow> [x \<noteq> 0](mod p)"
+ for x :: int
by (simp add: cong_int_def)
lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
@@ -175,7 +182,7 @@
by (auto simp add: A_def)
lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)"
- by (auto simp: B_def p_prime p_a_relprime A_ncong_p dest: cong_prime_prod_zero_int)
+ by (auto simp: B_def p_prime p_a_relprime A_ncong_p dest: cong_prime_prod_zero_int)
lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
using a_nonzero by (auto simp add: B_def A_greater_zero)
@@ -183,29 +190,33 @@
lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
proof (auto simp add: C_def)
fix x :: int
- assume a1: "x \<in> B"
- have f2: "\<And>x\<^sub>1. int x\<^sub>1 = 0 \<or> 0 < int x\<^sub>1" by linarith
- have "x mod int p \<noteq> 0" using a1 B_ncong_p cong_int_def by simp
- thus "0 < x mod int p" using a1 f2
+ assume x: "x \<in> B"
+ moreover from x have "x mod int p \<noteq> 0"
+ using B_ncong_p cong_int_def by simp
+ moreover have "int y = 0 \<or> 0 < int y" for y
+ by linarith
+ ultimately show "0 < x mod int p"
by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int)
qed
-lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((int p - 1) div 2)}"
+lemma F_subset: "F \<subseteq> {x. 0 < x \<and> x \<le> ((int p - 1) div 2)}"
apply (auto simp add: F_def E_def C_def)
- apply (metis p_ge_2 Divides.pos_mod_bound less_diff_eq nat_int plus_int_code(2) zless_nat_conj)
+ apply (metis p_ge_2 Divides.pos_mod_bound nat_int zless_nat_conj)
apply (auto intro: p_odd_int)
done
-lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
+lemma D_subset: "D \<subseteq> {x. 0 < x \<and> x \<le> ((p - 1) div 2)}"
by (auto simp add: D_def C_greater_zero)
-lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - ((y*a) mod p) & (int p - 1) div 2 < (y*a) mod p)}"
+lemma F_eq: "F = {x. \<exists>y \<in> A. (x = p - ((y * a) mod p) \<and> (int p - 1) div 2 < (y * a) mod p)}"
by (auto simp add: F_def E_def D_def C_def B_def A_def)
-lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = (y*a) mod p & (y*a) mod p \<le> (int p - 1) div 2)}"
+lemma D_eq: "D = {x. \<exists>y \<in> A. (x = (y * a) mod p \<and> (y * a) mod p \<le> (int p - 1) div 2)}"
by (auto simp add: D_def C_def B_def A_def)
-lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
+lemma all_A_relprime:
+ assumes "x \<in> A"
+ shows "gcd x p = 1"
using p_prime A_ncong_p [OF assms]
by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
@@ -215,7 +226,7 @@
subsection \<open>Relationships Between Gauss Sets\<close>
-lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)"
+lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> inj_on (\<lambda>b. b mod m) X"
by (auto simp add: ResSet_def inj_on_def cong_int_def)
lemma B_card_eq_A: "card B = card A"
@@ -225,13 +236,12 @@
by (simp add: B_card_eq_A A_card_eq)
lemma F_card_eq_E: "card F = card E"
- using finite_E
- by (simp add: F_def inj_on_pminusx_E card_image)
+ using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
lemma C_card_eq_B: "card C = card B"
proof -
have "inj_on (\<lambda>x. x mod p) B"
- by (metis SR_B_inj)
+ by (metis SR_B_inj)
then show ?thesis
by (metis C_def card_image)
qed
@@ -255,28 +265,25 @@
done
lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
- apply (intro Un_least subset_trans [OF F_subset] subset_trans [OF D_subset])
- apply (auto simp add: A_def)
- done
+ by (intro Un_least subset_trans [OF F_subset] subset_trans [OF D_subset]) (auto simp: A_def)
lemma F_D_disj: "(F \<inter> D) = {}"
proof (auto simp add: F_eq D_eq)
- fix y::int and z::int
- assume "p - (y*a) mod p = (z*a) mod p"
- then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)"
+ fix y z :: int
+ assume "p - (y * a) mod p = (z * a) mod p"
+ then have "[(y * a) mod p + (z * a) mod p = 0] (mod p)"
by (metis add.commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
- moreover have "[y * a = (y*a) mod p] (mod p)"
+ moreover have "[y * a = (y * a) mod p] (mod p)"
by (metis cong_int_def mod_mod_trivial)
ultimately have "[a * (y + z) = 0] (mod p)"
by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
- with p_prime a_nonzero p_a_relprime
- have a: "[y + z = 0] (mod p)"
+ with p_prime a_nonzero p_a_relprime have a: "[y + z = 0] (mod p)"
by (auto dest!: cong_prime_prod_zero_int)
assume b: "y \<in> A" and c: "z \<in> A"
- with A_def have "0 < y + z"
- by auto
- moreover from b c p_eq2 A_def have "y + z < p"
- by auto
+ then have "0 < y + z"
+ by (auto simp: A_def)
+ moreover from b c p_eq2 have "y + z < p"
+ by (auto simp: A_def)
ultimately show False
by (metis a nonzero_mod_p)
qed
@@ -292,28 +299,27 @@
qed
lemma F_Un_D_eq_A: "F \<union> D = A"
- using finite_A F_Un_D_subset A_card_eq F_Un_D_card
- by (auto simp add: card_seteq)
+ using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq)
-lemma prod_D_F_eq_prod_A: "(prod id D) * (prod id F) = prod id A"
+lemma prod_D_F_eq_prod_A: "prod id D * prod id F = prod id A"
by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F prod.union_disjoint)
-lemma prod_F_zcong: "[prod id F = ((-1) ^ (card E)) * (prod id E)] (mod p)"
+lemma prod_F_zcong: "[prod id F = ((-1) ^ (card E)) * prod id E] (mod p)"
proof -
have FE: "prod id F = prod (op - p) E"
apply (auto simp add: F_def)
apply (insert finite_E inj_on_pminusx_E)
- apply (drule prod.reindex, auto)
+ apply (drule prod.reindex)
+ apply auto
done
then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
then have "[prod ((\<lambda>x. x mod p) o (op - p)) E = prod (uminus) E](mod p)"
- using finite_E p_ge_2
- cong_prod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
+ using finite_E p_ge_2 cong_prod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
by auto
then have two: "[prod id F = prod (uminus) E](mod p)"
by (metis FE cong_cong_mod_int cong_refl_int cong_prod_int minus_mod_self1)
- have "prod uminus E = (-1) ^ (card E) * (prod id E)"
+ have "prod uminus E = (-1) ^ card E * prod id E"
using finite_E by (induct set: finite) auto
with two show ?thesis
by simp
@@ -323,68 +329,56 @@
subsection \<open>Gauss' Lemma\<close>
lemma aux: "prod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = prod id A * a ^ card A"
-by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
+ by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
-theorem pre_gauss_lemma:
- "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
+theorem pre_gauss_lemma: "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
have "[prod id A = prod id F * prod id D](mod p)"
- by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: prod.strong_cong)
+ by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.strong_cong)
then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
- apply (rule cong_trans_int)
- apply (metis cong_scalar_int prod_F_zcong)
- done
+ by (rule cong_trans_int) (metis cong_scalar_int prod_F_zcong)
then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
by (metis C_prod_eq_D_times_E mult.commute mult.left_commute)
then have "[prod id A = ((-1)^(card E) * prod id B)] (mod p)"
by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
- then have "[prod id A = ((-1)^(card E) *
- (prod id ((\<lambda>x. x * a) ` A)))] (mod p)"
+ then have "[prod id A = ((-1)^(card E) * prod id ((\<lambda>x. x * a) ` A))] (mod p)"
by (simp add: B_def)
- then have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. x * a) A))]
- (mod p)"
+ then have "[prod id A = ((-1)^(card E) * prod (\<lambda>x. x * a) A)] (mod p)"
by (simp add: inj_on_xa_A prod.reindex)
- moreover have "prod (\<lambda>x. x * a) A =
- prod (\<lambda>x. a) A * prod id A"
+ moreover have "prod (\<lambda>x. x * a) A = prod (\<lambda>x. a) A * prod id A"
using finite_A by (induct set: finite) auto
- ultimately have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. a) A *
- prod id A))] (mod p)"
+ ultimately have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. a) A * prod id A))] (mod p)"
by simp
- then have "[prod id A = ((-1)^(card E) * a^(card A) *
- prod id A)](mod p)"
- apply (rule cong_trans_int)
- apply (simp add: cong_scalar2_int cong_scalar_int finite_A prod_constant mult.assoc)
- done
+ then have "[prod id A = ((-1)^(card E) * a^(card A) * prod id A)](mod p)"
+ by (rule cong_trans_int)
+ (simp add: cong_scalar2_int cong_scalar_int finite_A prod_constant mult.assoc)
then have a: "[prod id A * (-1)^(card E) =
((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
by (rule cong_scalar_int)
then have "[prod id A * (-1)^(card E) = prod id A *
(-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
- apply (rule cong_trans_int)
- apply (simp add: a mult.commute mult.left_commute)
- done
+ by (rule cong_trans_int) (simp add: a mult.commute mult.left_commute)
then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
- apply (rule cong_trans_int)
- apply (simp add: aux cong del: prod.strong_cong)
- done
+ by (rule cong_trans_int) (simp add: aux cong del: prod.strong_cong)
with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
by (metis cong_mult_lcancel_int)
then show ?thesis
by (simp add: A_card_eq cong_sym_int)
qed
-theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
+theorem gauss_lemma: "Legendre a p = (-1) ^ (card E)"
proof -
- from euler_criterion p_prime p_ge_2 have
- "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
+ from euler_criterion p_prime p_ge_2 have "[Legendre a p = a^(nat (((p) - 1) div 2))] (mod p)"
by auto
- moreover have "int ((p - 1) div 2) =(int p - 1) div 2" using p_eq2 by linarith
- hence "[a ^ nat (int ((p - 1) div 2)) = a ^ nat ((int p - 1) div 2)] (mod int p)" by force
- moreover note pre_gauss_lemma
- ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)" using cong_trans_int by blast
- moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
+ moreover have "int ((p - 1) div 2) = (int p - 1) div 2"
+ using p_eq2 by linarith
+ then have "[a ^ nat (int ((p - 1) div 2)) = a ^ nat ((int p - 1) div 2)] (mod int p)"
+ by force
+ ultimately have "[Legendre a p = (-1) ^ (card E)] (mod p)"
+ using pre_gauss_lemma cong_trans_int by blast
+ moreover from p_a_relprime have "Legendre a p = 1 \<or> Legendre a p = -1"
by (auto simp add: Legendre_def)
- moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
+ moreover have "(-1::int) ^ (card E) = 1 \<or> (-1::int) ^ (card E) = -1"
using neg_one_even_power neg_one_odd_power by blast
moreover have "[1 \<noteq> - 1] (mod int p)"
using cong_altdef_int nonzero_mod_p[of 2] p_odd_int by fastforce
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Thu Apr 06 16:08:48 2017 +0200
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Thu Apr 06 21:01:39 2017 +0200
@@ -1,15 +1,19 @@
-(* Author: Jaime Mendizabal Roche *)
+(* Title: HOL/Number_Theory/Quadratic_Reciprocity.thy
+ Author: Jaime Mendizabal Roche
+*)
theory Quadratic_Reciprocity
imports Gauss
begin
-text \<open>The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close>
+text \<open>
+ The proof is based on Gauss's fifth proof, which can be found at
+ \<^url>\<open>http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close>.
+\<close>
locale QR =
fixes p :: "nat"
fixes q :: "nat"
-
assumes p_prime: "prime p"
assumes p_ge_2: "2 < p"
assumes q_prime: "prime q"
@@ -17,20 +21,26 @@
assumes pq_neq: "p \<noteq> q"
begin
-lemma odd_p: "odd p" using p_ge_2 p_prime prime_odd_nat by blast
+lemma odd_p: "odd p"
+ using p_ge_2 p_prime prime_odd_nat by blast
lemma p_ge_0: "0 < int p"
using p_prime not_prime_0[where 'a = nat] by fastforce+
-lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1" using odd_p by simp
+lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
+ using odd_p by simp
-lemma odd_q: "odd q" using q_ge_2 q_prime prime_odd_nat by blast
+lemma odd_q: "odd q"
+ using q_ge_2 q_prime prime_odd_nat by blast
-lemma q_ge_0: "0 < int q" using q_prime not_prime_0[where 'a = nat] by fastforce+
+lemma q_ge_0: "0 < int q"
+ using q_prime not_prime_0[where 'a = nat] by fastforce+
-lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1" using odd_q by simp
+lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1"
+ using odd_q by simp
-lemma pq_eq2: "int p * int q = (2 * ((int p * int q - 1) div 2)) + 1" using odd_p odd_q by simp
+lemma pq_eq2: "int p * int q = (2 * ((int p * int q - 1) div 2)) + 1"
+ using odd_p odd_q by simp
lemma pq_coprime: "coprime p q"
using pq_neq p_prime primes_coprime_nat q_prime by blast
@@ -38,27 +48,31 @@
lemma pq_coprime_int: "coprime (int p) (int q)"
using pq_coprime transfer_int_nat_gcd(1) by presburger
-lemma qp_ineq: "(int p * k \<le> (int p * int q - 1) div 2) = (k \<le> (int q - 1) div 2)"
+lemma qp_ineq: "int p * k \<le> (int p * int q - 1) div 2 \<longleftrightarrow> k \<le> (int q - 1) div 2"
proof -
- have "(2 * int p * k \<le> int p * int q - 1) = (2 * k \<le> int q - 1)" using p_ge_0 by auto
- thus ?thesis by auto
+ have "2 * int p * k \<le> int p * int q - 1 \<longleftrightarrow> 2 * k \<le> int q - 1"
+ using p_ge_0 by auto
+ then show ?thesis by auto
qed
-lemma QRqp: "QR q p" using QR_def QR_axioms by simp
-
-lemma pq_commute: "int p * int q = int q * int p" by simp
+lemma QRqp: "QR q p"
+ using QR_def QR_axioms by simp
-lemma pq_ge_0: "int p * int q > 0" using p_ge_0 q_ge_0 mult_pos_pos by blast
+lemma pq_commute: "int p * int q = int q * int p"
+ by simp
-definition "r = ((p - 1) div 2)*((q - 1) div 2)"
+lemma pq_ge_0: "int p * int q > 0"
+ using p_ge_0 q_ge_0 mult_pos_pos by blast
+
+definition "r = ((p - 1) div 2) * ((q - 1) div 2)"
definition "m = card (GAUSS.E p q)"
definition "n = card (GAUSS.E q p)"
-abbreviation "Res (k::int) \<equiv> {0 .. k - 1}"
-abbreviation "Res_ge_0 (k::int) \<equiv> {0 <.. k - 1}"
-abbreviation "Res_0 (k::int) \<equiv> {0::int}"
-abbreviation "Res_l (k::int) \<equiv> {0 <.. (k - 1) div 2}"
-abbreviation "Res_h (k::int) \<equiv> {(k - 1) div 2 <.. k - 1}"
+abbreviation "Res k \<equiv> {0 .. k - 1}" for k :: int
+abbreviation "Res_ge_0 k \<equiv> {0 <.. k - 1}" for k :: int
+abbreviation "Res_0 k \<equiv> {0::int}" for k :: int
+abbreviation "Res_l k \<equiv> {0 <.. (k - 1) div 2}" for k :: int
+abbreviation "Res_h k \<equiv> {(k - 1) div 2 <.. k - 1}" for k :: int
abbreviation "Sets_pq r0 r1 r2 \<equiv>
{(x::int). x \<in> r0 (int p * int q) \<and> x mod p \<in> r1 (int p) \<and> x mod q \<in> r2 (int q)}"
@@ -77,311 +91,376 @@
definition "e = card E"
definition "f = card F"
-lemma Gpq: "GAUSS p q" unfolding GAUSS_def
+lemma Gpq: "GAUSS p q"
using p_prime pq_neq p_ge_2 q_prime
- by (auto simp: cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq)
+ by (auto simp: GAUSS_def cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq)
-lemma Gqp: "GAUSS q p" using QRqp QR.Gpq by simp
+lemma Gqp: "GAUSS q p"
+ by (simp add: QRqp QR.Gpq)
lemma QR_lemma_01: "(\<lambda>x. x mod q) ` E = GAUSS.E q p"
proof
- {
- fix x
- assume a1: "x \<in> E"
- then obtain k where k: "x = int p * k" unfolding E_def by blast
- have "x \<in> Res_l (int p * int q)" using a1 E_def by blast
- hence "k \<in> GAUSS.A q" using Gqp GAUSS.A_def k qp_ineq by (simp add: zero_less_mult_iff)
- hence "x mod q \<in> GAUSS.E q p"
- using GAUSS.C_def[of q p] Gqp k GAUSS.B_def[of q p] a1 GAUSS.E_def[of q p]
- unfolding E_def by force
- hence "x \<in> E \<longrightarrow> x mod int q \<in> GAUSS.E q p" by auto
- }
- thus "(\<lambda>x. x mod int q) ` E \<subseteq> GAUSS.E q p" by auto
-next
+ have "x \<in> E \<longrightarrow> x mod int q \<in> GAUSS.E q p" if "x \<in> E" for x
+ proof -
+ from that obtain k where k: "x = int p * k"
+ unfolding E_def by blast
+ from that E_def have "x \<in> Res_l (int p * int q)"
+ by blast
+ then have "k \<in> GAUSS.A q"
+ using Gqp GAUSS.A_def k qp_ineq by (simp add: zero_less_mult_iff)
+ then have "x mod q \<in> GAUSS.E q p"
+ 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 "(\<lambda>x. x mod int q) ` E \<subseteq> GAUSS.E q p"
+ by auto
show "GAUSS.E q p \<subseteq> (\<lambda>x. x mod q) ` E"
proof
fix x
- assume a1: "x \<in> GAUSS.E q p"
+ assume x: "x \<in> GAUSS.E q p"
then obtain ka where ka: "ka \<in> GAUSS.A q" "x = (ka * p) mod q"
- using Gqp GAUSS.B_def GAUSS.C_def GAUSS.E_def by auto
- hence "ka * p \<in> Res_l (int p * int q)"
- using GAUSS.A_def Gqp p_ge_0 qp_ineq by (simp add: Groups.mult_ac(2))
- thus "x \<in> (\<lambda>x. x mod q) ` E" unfolding E_def using ka a1 Gqp GAUSS.E_def q_ge_0 by force
+ by (auto simp: Gqp GAUSS.B_def GAUSS.C_def GAUSS.E_def)
+ then have "ka * p \<in> Res_l (int p * int q)"
+ using Gqp p_ge_0 qp_ineq by (simp add: GAUSS.A_def Groups.mult_ac(2))
+ then show "x \<in> (\<lambda>x. x mod q) ` E"
+ using ka x Gqp q_ge_0 by (force simp: E_def GAUSS.E_def)
qed
qed
-lemma QR_lemma_02: "e= n"
+lemma QR_lemma_02: "e = n"
proof -
- {
- fix x y
- assume a: "x \<in> E" "y \<in> E" "x mod q = y mod q"
+ have "x = y" if x: "x \<in> E" and y: "y \<in> E" and mod: "x mod q = y mod q" for x y
+ proof -
obtain p_inv where p_inv: "[int p * p_inv = 1] (mod int q)"
using pq_coprime_int cong_solve_coprime_int by blast
- obtain kx ky where k: "x = int p * kx" "y = int p * ky" using a E_def dvd_def[of p x] by blast
- hence "0 < x" "int p * kx \<le> (int p * int q - 1) div 2"
+ from x y E_def obtain kx ky where k: "x = int p * kx" "y = int p * ky"
+ using dvd_def[of p x] by blast
+ with x y E_def have "0 < x" "int p * kx \<le> (int p * int q - 1) div 2"
"0 < y" "int p * ky \<le> (int p * int q - 1) div 2"
- using E_def a greaterThanAtMost_iff mem_Collect_eq by blast+
- hence "0 \<le> kx" "kx < q" "0 \<le> ky" "ky < q" using qp_ineq k by (simp add: zero_less_mult_iff)+
- moreover have "(p_inv * (p * kx)) mod q = (p_inv * (p * ky)) mod q"
- using a(3) mod_mult_cong k by blast
- hence "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q" by (simp add:algebra_simps)
- hence "kx mod q = ky mod q"
- using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] cong_int_def by auto
- hence "[kx = ky] (mod q)" using cong_int_def by blast
- ultimately have "x = y" using cong_less_imp_eq_int k by blast
- }
- hence "inj_on (\<lambda>x. x mod q) E" unfolding inj_on_def by auto
- thus ?thesis using QR_lemma_01 card_image e_def n_def by fastforce
+ using greaterThanAtMost_iff mem_Collect_eq by blast+
+ with k have "0 \<le> kx" "kx < q" "0 \<le> ky" "ky < q"
+ using qp_ineq by (simp_all add: zero_less_mult_iff)
+ moreover from mod k have "(p_inv * (p * kx)) mod q = (p_inv * (p * ky)) mod q"
+ using mod_mult_cong by blast
+ then have "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q"
+ by (simp add: algebra_simps)
+ then have "kx mod q = ky mod q"
+ using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] by (auto simp: cong_int_def)
+ then have "[kx = ky] (mod q)"
+ unfolding cong_int_def by blast
+ ultimately show ?thesis
+ using cong_less_imp_eq_int k by blast
+ qed
+ then have "inj_on (\<lambda>x. x mod q) E"
+ 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: "f = m"
proof -
- have "F = QR.E q p" unfolding F_def pq_commute using QRqp QR.E_def[of q p] by fastforce
- hence "f = QR.e q p" unfolding f_def using QRqp QR.e_def[of q p] by presburger
- thus ?thesis using QRqp QR.QR_lemma_02 m_def QRqp QR.n_def by presburger
+ have "F = QR.E q p"
+ unfolding F_def pq_commute using QRqp QR.E_def[of q p] by fastforce
+ then have "f = QR.e q p"
+ 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 :: "int \<Rightarrow> int \<times> int" where
- "f_1 x = ((x mod p), (x mod q))"
+definition f_1 :: "int \<Rightarrow> int \<times> int"
+ where "f_1 x = ((x mod p), (x mod q))"
-definition P_1 :: "int \<times> int \<Rightarrow> int \<Rightarrow> bool" where
- "P_1 res x \<longleftrightarrow> x mod p = fst res & x mod q = snd res & x \<in> Res (int p * int q)"
+definition P_1 :: "int \<times> int \<Rightarrow> int \<Rightarrow> bool"
+ where "P_1 res x \<longleftrightarrow> x mod p = fst res \<and> x mod q = snd res \<and> x \<in> Res (int p * int q)"
-definition g_1 :: "int \<times> int \<Rightarrow> int" where
- "g_1 res = (THE x. P_1 res x)"
+definition g_1 :: "int \<times> int \<Rightarrow> int"
+ where "g_1 res = (THE x. P_1 res x)"
-lemma P_1_lemma: assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
- shows "\<exists>! x. P_1 res x"
+lemma P_1_lemma:
+ assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
+ shows "\<exists>!x. P_1 res x"
proof -
obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q"
using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce
- have h1: "[y = fst res] (mod p)" "[y = snd res] (mod q)"
+ have *: "[y = fst res] (mod p)" "[y = snd res] (mod q)"
using yk(1) assms(1) cong_iff_lin_int[of "fst res"] cong_sym_int apply simp
using yk(2) assms(3) cong_iff_lin_int[of "snd res"] cong_sym_int by simp
have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res"
- using h1(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp
- using h1(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp
- then obtain x where "P_1 res x" unfolding P_1_def
+ using *(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp
+ using *(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp
+ then obtain x where "P_1 res x"
+ unfolding P_1_def
using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce
- moreover {
- fix a b
- assume a: "P_1 res a" "P_1 res b"
- hence "int p * int q dvd a - b"
+ moreover have "a = b" if "P_1 res a" "P_1 res b" for a b
+ proof -
+ from that have "int p * int q dvd a - b"
using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int mod_eq_dvd_iff [of a _ b]
unfolding P_1_def by force
- hence "a = b" using dvd_imp_le_int[of "a - b"] a unfolding P_1_def by fastforce
- }
+ with that show ?thesis
+ using dvd_imp_le_int[of "a - b"] unfolding P_1_def by fastforce
+ qed
ultimately show ?thesis by auto
qed
-lemma g_1_lemma: assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
- shows "P_1 res (g_1 res)" using assms P_1_lemma theI'[of "P_1 res"] g_1_def by presburger
+lemma g_1_lemma:
+ assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
+ shows "P_1 res (g_1 res)"
+ using assms P_1_lemma theI'[of "P_1 res"] g_1_def by presburger
definition "BuC = Sets_pq Res_ge_0 Res_h Res_l"
-lemma QR_lemma_04: "card BuC = card ((Res_h p) \<times> (Res_l q))"
- using card_bij_eq[of f_1 "BuC" "(Res_h p) \<times> (Res_l q)" g_1]
+lemma QR_lemma_04: "card BuC = card (Res_h p \<times> Res_l q)"
+ using card_bij_eq[of f_1 "BuC" "Res_h p \<times> Res_l q" g_1]
proof
- {
+ show "inj_on f_1 BuC"
+ proof
fix x y
- assume a: "x \<in> BuC" "y \<in> BuC" "f_1 x = f_1 y"
- hence "int p * int q dvd x - y"
- using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"]
- mod_eq_dvd_iff[of x _ y] by auto
- hence "x = y"
- using dvd_imp_le_int[of "x - y" "int p * int q"] a unfolding BuC_def by force
- }
- thus "inj_on f_1 BuC" unfolding inj_on_def by auto
-next
- {
+ assume *: "x \<in> BuC" "y \<in> BuC" "f_1 x = f_1 y"
+ then have "int p * int q dvd x - y"
+ using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"]
+ mod_eq_dvd_iff[of x _ y]
+ by auto
+ with * show "x = y"
+ using dvd_imp_le_int[of "x - y" "int p * int q"] unfolding BuC_def by force
+ qed
+ show "inj_on g_1 (Res_h p \<times> Res_l q)"
+ proof
fix x y
- assume a: "x \<in> (Res_h p) \<times> (Res_l q)" "y \<in> (Res_h p) \<times> (Res_l q)" "g_1 x = g_1 y"
- hence "0 \<le> fst x" "fst x < p" "0 \<le> snd x" "snd x < q"
+ assume *: "x \<in> Res_h p \<times> Res_l q" "y \<in> Res_h p \<times> Res_l q" "g_1 x = g_1 y"
+ then have "0 \<le> fst x" "fst x < p" "0 \<le> snd x" "snd x < q"
"0 \<le> fst y" "fst y < p" "0 \<le> snd y" "snd y < q"
using mem_Sigma_iff prod.collapse by fastforce+
- hence "x = y" using g_1_lemma[of x] g_1_lemma[of y] a P_1_def by fastforce
- }
- thus "inj_on g_1 ((Res_h p) \<times> (Res_l q))" unfolding inj_on_def by auto
-next
- show "g_1 ` ((Res_h p) \<times> (Res_l q)) \<subseteq> BuC"
+ with * show "x = y"
+ using g_1_lemma[of x] g_1_lemma[of y] P_1_def by fastforce
+ qed
+ show "g_1 ` (Res_h p \<times> Res_l q) \<subseteq> BuC"
proof
fix y
- assume "y \<in> g_1 ` ((Res_h p) \<times> (Res_l q))"
- then obtain x where x: "y = g_1 x" "x \<in> ((Res_h p) \<times> (Res_l q))" by blast
- hence "P_1 x y" using g_1_lemma by fastforce
- thus "y \<in> BuC" unfolding P_1_def BuC_def mem_Collect_eq using x SigmaE prod.sel by fastforce
+ assume "y \<in> g_1 ` (Res_h p \<times> Res_l q)"
+ then obtain x where x: "y = g_1 x" "x \<in> Res_h p \<times> Res_l q"
+ by blast
+ then have "P_1 x y"
+ using g_1_lemma by fastforce
+ with x show "y \<in> BuC"
+ unfolding P_1_def BuC_def mem_Collect_eq using SigmaE prod.sel by fastforce
qed
qed (auto simp: BuC_def finite_subset f_1_def)
-lemma QR_lemma_05: "card ((Res_h p) \<times> (Res_l q)) = r"
+lemma QR_lemma_05: "card (Res_h p \<times> Res_l q) = r"
proof -
- have "card (Res_l q) = (q - 1) div 2" "card (Res_h p) = (p - 1) div 2" using p_eq2 by force+
- thus ?thesis unfolding r_def using card_cartesian_product[of "Res_h p" "Res_l q"] by presburger
+ have "card (Res_l q) = (q - 1) div 2" "card (Res_h p) = (p - 1) div 2"
+ using p_eq2 by force+
+ then show ?thesis
+ unfolding r_def using card_cartesian_product[of "Res_h p" "Res_l q"] by presburger
qed
lemma QR_lemma_06: "b + c = r"
proof -
- have "B \<inter> C = {}" "finite B" "finite C" "B \<union> C = BuC" unfolding B_def C_def BuC_def by fastforce+
- thus ?thesis
+ have "B \<inter> C = {}" "finite B" "finite C" "B \<union> C = BuC"
+ 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:: "int \<Rightarrow> int" where
- "f_2 x = (int p * int q) - x"
+definition f_2:: "int \<Rightarrow> int"
+ where "f_2 x = (int p * int q) - x"
-lemma f_2_lemma_1: "\<And>x. f_2 (f_2 x) = x" unfolding f_2_def by simp
+lemma f_2_lemma_1: "f_2 (f_2 x) = x"
+ by (simp add: f_2_def)
-lemma f_2_lemma_2: "[f_2 x = int p - x] (mod p)" unfolding f_2_def using cong_altdef_int by simp
+lemma f_2_lemma_2: "[f_2 x = int p - x] (mod p)"
+ by (simp add: f_2_def cong_altdef_int)
lemma f_2_lemma_3: "f_2 x \<in> S \<Longrightarrow> x \<in> f_2 ` S"
using f_2_lemma_1[of x] image_eqI[of x f_2 "f_2 x" S] by presburger
-lemma QR_lemma_07: "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)"
- "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)"
+lemma QR_lemma_07:
+ "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)"
+ "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)"
proof -
- have h1: "f_2 ` Res_l (int p * int q) \<subseteq> Res_h (int p * int q)" using f_2_def by force
- have h2: "f_2 ` Res_h (int p * int q) \<subseteq> Res_l (int p * int q)" using f_2_def pq_eq2 by fastforce
- have h3: "Res_h (int p * int q) \<subseteq> f_2 ` Res_l (int p * int q)" using h2 f_2_lemma_3 by blast
- have h4: "Res_l (int p * int q) \<subseteq> f_2 ` Res_h (int p * int q)" using h1 f_2_lemma_3 by blast
- show "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)" using h1 h3 by blast
- show "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)" using h2 h4 by blast
+ have 1: "f_2 ` Res_l (int p * int q) \<subseteq> Res_h (int p * int q)"
+ by (force simp: f_2_def)
+ have 2: "f_2 ` Res_h (int p * int q) \<subseteq> Res_l (int p * int q)"
+ using pq_eq2 by (fastforce simp: f_2_def)
+ from 2 have 3: "Res_h (int p * int q) \<subseteq> f_2 ` Res_l (int p * int q)"
+ using f_2_lemma_3 by blast
+ from 1 have 4: "Res_l (int p * int q) \<subseteq> f_2 ` Res_h (int p * int q)"
+ using f_2_lemma_3 by blast
+ from 1 3 show "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)"
+ by blast
+ from 2 4 show "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)"
+ by blast
qed
-lemma QR_lemma_08: "(f_2 x mod p \<in> Res_l p) = (x mod p \<in> Res_h p)"
- "(f_2 x mod p \<in> Res_h p) = (x mod p \<in> Res_l p)"
+lemma QR_lemma_08:
+ "f_2 x mod p \<in> Res_l p \<longleftrightarrow> x mod p \<in> Res_h p"
+ "f_2 x mod p \<in> Res_h p \<longleftrightarrow> x mod p \<in> Res_l p"
using f_2_lemma_2[of x] cong_int_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p]
- zmod_zminus1_eq_if[of x p] p_eq2 by auto
+ zmod_zminus1_eq_if[of x p] p_eq2
+ by auto
-lemma QR_lemma_09: "(f_2 x mod q \<in> Res_l q) = (x mod q \<in> Res_h q)"
- "(f_2 x mod q \<in> Res_h q) = (x mod q \<in> Res_l q)"
- using QRqp QR.QR_lemma_08 f_2_def QR.f_2_def pq_commute by auto+
+lemma QR_lemma_09:
+ "f_2 x mod q \<in> Res_l q \<longleftrightarrow> x mod q \<in> Res_h q"
+ "f_2 x mod q \<in> Res_h q \<longleftrightarrow> x mod q \<in> Res_l q"
+ using QRqp QR.QR_lemma_08 f_2_def QR.f_2_def pq_commute by auto
-lemma QR_lemma_10: "a = c" unfolding a_def c_def apply (rule card_bij_eq[of f_2 A C f_2])
+lemma QR_lemma_10: "a = c"
+ 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)+
- by fastforce+
+ using QR_lemma_07 QR_lemma_08 QR_lemma_09 apply ((simp add: inj_on_def f_2_def), blast)+
+ apply fastforce+
+ done
definition "BuD = Sets_pq Res_l Res_h Res_ge_0"
definition "BuDuF = Sets_pq Res_l Res_h Res"
-definition f_3 :: "int \<Rightarrow> int \<times> int" where
- "f_3 x = (x mod p, x div p + 1)"
+definition f_3 :: "int \<Rightarrow> int \<times> int"
+ where "f_3 x = (x mod p, x div p + 1)"
-definition g_3 :: "int \<times> int \<Rightarrow> int" where
- "g_3 x = fst x + (snd x - 1) * p"
+definition g_3 :: "int \<times> int \<Rightarrow> int"
+ where "g_3 x = fst x + (snd x - 1) * p"
-lemma QR_lemma_11: "card BuDuF = card ((Res_h p) \<times> (Res_l q))"
- using card_bij_eq[of f_3 BuDuF "(Res_h p) \<times> (Res_l q)" g_3]
+lemma QR_lemma_11: "card BuDuF = card (Res_h p \<times> Res_l q)"
+ using card_bij_eq[of f_3 BuDuF "Res_h p \<times> Res_l q" g_3]
proof
- show "f_3 ` BuDuF \<subseteq> (Res_h p) \<times> (Res_l q)"
+ show "f_3 ` BuDuF \<subseteq> Res_h p \<times> Res_l q"
proof
fix y
assume "y \<in> f_3 ` BuDuF"
- then obtain x where x: "y = f_3 x" "x \<in> BuDuF" by blast
- hence "x \<le> int p * (int q - 1) div 2 + (int p - 1) div 2"
+ then obtain x where x: "y = f_3 x" "x \<in> BuDuF"
+ by blast
+ then have "x \<le> int p * (int q - 1) div 2 + (int p - 1) div 2"
unfolding BuDuF_def using p_eq2 int_distrib(4) by auto
- moreover have "(int p - 1) div 2 \<le> - 1 + x mod p" using x BuDuF_def by auto
+ moreover from x have "(int p - 1) div 2 \<le> - 1 + x mod p"
+ by (auto simp: BuDuF_def)
moreover have "int p * (int q - 1) div 2 = int p * ((int q - 1) div 2)"
using zdiv_zmult1_eq odd_q by auto
- hence "p * (int q - 1) div 2 = p * ((int q + 1) div 2 - 1)" by fastforce
- ultimately have "x \<le> p * ((int q + 1) div 2 - 1) - 1 + x mod p" by linarith
- hence "x div p < (int q + 1) div 2 - 1"
+ then have "p * (int q - 1) div 2 = p * ((int q + 1) div 2 - 1)"
+ by fastforce
+ ultimately have "x \<le> p * ((int q + 1) div 2 - 1) - 1 + x mod p"
+ by linarith
+ then have "x div p < (int q + 1) div 2 - 1"
using mult.commute[of "int p" "x div p"] p_ge_0 div_mult_mod_eq[of x p]
- mult_less_cancel_left_pos[of p "x div p" "(int q + 1) div 2 - 1"] by linarith
- moreover have "0 < x div p + 1"
- using pos_imp_zdiv_neg_iff[of p x] p_ge_0 x mem_Collect_eq BuDuF_def by auto
- ultimately show "y \<in> (Res_h p) \<times> (Res_l q)" using x BuDuF_def f_3_def by auto
+ and mult_less_cancel_left_pos[of p "x div p" "(int q + 1) div 2 - 1"]
+ by linarith
+ moreover from x have "0 < x div p + 1"
+ using pos_imp_zdiv_neg_iff[of p x] p_ge_0 by (auto simp: BuDuF_def)
+ ultimately show "y \<in> Res_h p \<times> Res_l q"
+ using x by (auto simp: BuDuF_def f_3_def)
qed
-next
- have h1: "\<And>x. x \<in> ((Res_h p) \<times> (Res_l q)) \<Longrightarrow> f_3 (g_3 x) = x"
- proof -
- fix x
- assume a: "x \<in> ((Res_h p) \<times> (Res_l q))"
- moreover have h: "(fst x + (snd x - 1) * int p) mod int p = fst x" using a by force
- ultimately have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x"
- by (auto simp: semiring_numeral_div_class.div_less)
- with h show "f_3 (g_3 x) = x" unfolding f_3_def g_3_def by simp
+ show "inj_on g_3 (Res_h p \<times> Res_l q)"
+ proof
+ have *: "f_3 (g_3 x) = x" if "x \<in> Res_h p \<times> Res_l q" for x
+ proof -
+ from that have *: "(fst x + (snd x - 1) * int p) mod int p = fst x"
+ by force
+ from that have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x"
+ by (auto simp: semiring_numeral_div_class.div_less)
+ with * show "f_3 (g_3 x) = x"
+ by (simp add: f_3_def g_3_def)
+ qed
+ fix x y
+ assume "x \<in> Res_h p \<times> Res_l q" "y \<in> Res_h p \<times> Res_l q" "g_3 x = g_3 y"
+ from this *[of x] *[of y] show "x = y"
+ by presburger
qed
- show "inj_on g_3 ((Res_h p) \<times> (Res_l q))" apply (rule inj_onI[of "(Res_h p) \<times> (Res_l q)" g_3])
- proof -
- fix x y
- assume "x \<in> ((Res_h p) \<times> (Res_l q))" "y \<in> ((Res_h p) \<times> (Res_l q))" "g_3 x = g_3 y"
- thus "x = y" using h1[of x] h1[of y] by presburger
- qed
-next
- show "g_3 ` ((Res_h p) \<times> (Res_l q)) \<subseteq> BuDuF"
+ show "g_3 ` (Res_h p \<times> Res_l q) \<subseteq> BuDuF"
proof
fix y
- assume "y \<in> g_3 ` ((Res_h p) \<times> (Res_l q))"
- then obtain x where x: "y = g_3 x" "x \<in> (Res_h p) \<times> (Res_l q)" by blast
- hence "snd x \<le> (int q - 1) div 2" by force
+ assume "y \<in> g_3 ` (Res_h p \<times> Res_l q)"
+ then obtain x where x: "x \<in> Res_h p \<times> Res_l q" and y: "y = g_3 x"
+ by blast
+ then have "snd x \<le> (int q - 1) div 2"
+ by force
moreover have "int p * ((int q - 1) div 2) = (int p * int q - int p) div 2"
using int_distrib(4) zdiv_zmult1_eq[of "int p" "int q - 1" 2] odd_q by fastforce
ultimately have "(snd x) * int p \<le> (int q * int p - int p) div 2"
using mult_right_mono[of "snd x" "(int q - 1) div 2" p] mult.commute[of "(int q - 1) div 2" p]
- pq_commute by presburger
- hence "(snd x - 1) * int p \<le> (int q * int p - 1) div 2 - int p"
+ pq_commute
+ by presburger
+ then have "(snd x - 1) * int p \<le> (int q * int p - 1) div 2 - int p"
using p_ge_0 int_distrib(3) by auto
- moreover have "fst x \<le> int p - 1" using x by force
+ moreover from x have "fst x \<le> int p - 1" by force
ultimately have "fst x + (snd x - 1) * int p \<le> (int p * int q - 1) div 2"
using pq_commute by linarith
- moreover have "0 < fst x" "0 \<le> (snd x - 1) * p" using x(2) by fastforce+
- ultimately show "y \<in> BuDuF" unfolding BuDuF_def using q_ge_0 x g_3_def x(1) by auto
+ moreover from x have "0 < fst x" "0 \<le> (snd x - 1) * p"
+ by fastforce+
+ ultimately show "y \<in> BuDuF"
+ unfolding BuDuF_def using q_ge_0 x g_3_def y by auto
qed
-next
show "finite BuDuF" 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: "b + d + m = r"
proof -
- have "B \<inter> D = {}" "finite B" "finite D" "B \<union> D = BuD" unfolding B_def D_def BuD_def by fastforce+
- hence "b + d = card BuD" unfolding b_def d_def using card_Un_Int by fastforce
- moreover have "BuD \<inter> F = {}" "finite BuD" "finite F" unfolding BuD_def F_def by fastforce+
- moreover have "BuD \<union> F = BuDuF" unfolding BuD_def F_def BuDuF_def
+ have "B \<inter> D = {}" "finite B" "finite D" "B \<union> D = BuD"
+ unfolding B_def D_def BuD_def by fastforce+
+ then have "b + d = card BuD"
+ unfolding b_def d_def using card_Un_Int by fastforce
+ moreover have "BuD \<inter> F = {}" "finite BuD" "finite F"
+ unfolding BuD_def F_def by fastforce+
+ moreover have "BuD \<union> F = BuDuF"
+ unfolding BuD_def F_def BuDuF_def
using q_ge_0 ivl_disj_un_singleton(5)[of 0 "int q - 1"] 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
+ 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: "a + d + n = r"
proof -
- have "A = QR.B q p" unfolding A_def pq_commute using QRqp QR.B_def[of q p] by blast
- hence "a = QR.b q p" using a_def QRqp QR.b_def[of q p] by presburger
- moreover have "D = QR.D q p" unfolding D_def pq_commute using QRqp QR.D_def[of q p] by blast
- hence "d = QR.d q p" using d_def QRqp QR.d_def[of q p] by presburger
- moreover have "n = QR.m q p" using n_def QRqp QR.m_def[of q p] by presburger
- moreover have "r = QR.r q p" unfolding r_def using QRqp QR.r_def[of q p] by auto
- ultimately show ?thesis using QRqp QR.QR_lemma_12 by presburger
+ have "A = QR.B q p"
+ unfolding A_def pq_commute using QRqp QR.B_def[of q p] by blast
+ then have "a = QR.b q p"
+ using a_def QRqp QR.b_def[of q p] by presburger
+ moreover have "D = QR.D q p"
+ unfolding D_def pq_commute using QRqp QR.D_def[of q p] by blast
+ then have "d = QR.d q p"
+ using d_def QRqp QR.d_def[of q p] by presburger
+ moreover have "n = QR.m q p"
+ using n_def QRqp QR.m_def[of q p] by presburger
+ moreover have "r = QR.r q p"
+ 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: "(-1::int) ^ (m + n) = (-1) ^ r"
proof -
- have "m + n + 2 * d = r" using QR_lemma_06 QR_lemma_10 QR_lemma_12 QR_lemma_13 by auto
- thus ?thesis using power_add[of "-1::int" "m + n" "2 * d"] by fastforce
+ have "m + n + 2 * d = r"
+ using QR_lemma_06 QR_lemma_10 QR_lemma_12 QR_lemma_13 by auto
+ then show ?thesis
+ using power_add[of "-1::int" "m + n" "2 * d"] by fastforce
qed
lemma Quadratic_Reciprocity:
- "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))"
+ "Legendre p q * Legendre q p = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))"
using Gpq Gqp GAUSS.gauss_lemma power_add[of "-1::int" m n] QR_lemma_14
unfolding r_def m_def n_def by auto
end
-theorem Quadratic_Reciprocity: assumes "prime p" "2 < p" "prime q" "2 < q" "p \<noteq> q"
- shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))"
+theorem Quadratic_Reciprocity:
+ assumes "prime p" "2 < p" "prime q" "2 < q" "p \<noteq> q"
+ shows "Legendre p q * Legendre q p = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))"
using QR.Quadratic_Reciprocity QR_def assms by blast
-theorem Quadratic_Reciprocity_int: assumes "prime (nat p)" "2 < p" "prime (nat q)" "2 < q" "p \<noteq> q"
- shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ (nat ((p - 1) div 2 * ((q - 1) div 2)))"
+theorem Quadratic_Reciprocity_int:
+ assumes "prime (nat p)" "2 < p" "prime (nat q)" "2 < q" "p \<noteq> q"
+ shows "Legendre p q * Legendre q p = (-1::int) ^ (nat ((p - 1) div 2 * ((q - 1) div 2)))"
proof -
- have "0 \<le> (p - 1) div 2" using assms by simp
+ from assms have "0 \<le> (p - 1) div 2" by simp
moreover have "(nat p - 1) div 2 = nat ((p - 1) div 2)" "(nat q - 1) div 2 = nat ((q - 1) div 2)"
by fastforce+
ultimately have "(nat p - 1) div 2 * ((nat q - 1) div 2) = nat ((p - 1) div 2 * ((q - 1) div 2))"
using nat_mult_distrib by presburger
moreover have "2 < nat p" "2 < nat q" "nat p \<noteq> nat q" "int (nat p) = p" "int (nat q) = q"
using assms by linarith+
- ultimately show ?thesis using Quadratic_Reciprocity[of "nat p" "nat q"] assms by presburger
+ ultimately show ?thesis
+ using Quadratic_Reciprocity[of "nat p" "nat q"] assms by presburger
qed
end