(* File: Miller_Rabin.thy Authors: Daniel Stüwe Some facts about Quadratic Residues that are missing from the library *) section ‹Additional Material on Quadratic Residues› theory QuadRes imports Jacobi_Symbol Algebraic_Auxiliaries begin text ‹Proofs are inspired by \<^cite>‹"Quadratic_Residues"›.› lemma inj_on_QuadRes: fixes p :: int assumes "prime p" shows "inj_on (λx. x^2 mod p) {0..(p-1) div 2}" proof fix x y :: int assume elem: "x ∈ {0..(p-1) div 2}" "y ∈ {0..(p-1) div 2}" have * : "abs(a) < p ⟹ p dvd a ⟹ a = 0" for a :: int using dvd_imp_le_int by force assume "x⇧^{2}mod p = y⇧^{2}mod p" hence "[x⇧^{2}= y⇧^{2}] (mod p)" unfolding cong_def . hence "p dvd (x⇧^{2}- y⇧^{2})" by (simp add: cong_iff_dvd_diff) hence "p dvd (x + y) * (x - y)" by (simp add: power2_eq_square square_diff_square_factored) hence "p dvd (x + y) ∨ p dvd (x - y)" using ‹prime p› by (simp add: prime_dvd_mult_iff) moreover have "p dvd x + y ⟹ x + y = 0" "p dvd x - y ⟹ x - y = 0" and "0 ≤ x" "0 ≤ y" using elem by (fastforce intro!: * )+ ultimately show "x = y" by auto qed lemma QuadRes_set_prime: assumes "prime p" and "odd p" shows "{x . QuadRes p x ∧ x ∈ {0..<p}} = {x^2 mod p | x . x ∈ {0..(p-1) div 2}}" proof(safe, goal_cases) case (1 x) then obtain y where "[y⇧^{2}= x] (mod p)" unfolding QuadRes_def by blast then have A: "[(y mod p)⇧^{2}= x] (mod p)" unfolding cong_def by (simp add: power_mod) then have "[(-(y mod p))⇧^{2}= x] (mod p)" by simp then have B: "[(p - (y mod p))⇧^{2}= x] (mod p)" unfolding cong_def using minus_mod_self1 by (metis power_mod) have "p = 1 + ((p - 1) div 2) * 2" using prime_gt_0_int[OF ‹prime p›] ‹odd p› by simp then have C: "(p - (y mod p)) ∈ {0..(p - 1) div 2} ∨ y mod p ∈ {0..(p - 1) div 2}" using prime_gt_0_int[OF ‹prime p›] by (clarsimp, auto simp: le_less) then show ?case proof show ?thesis if "p - y mod p ∈ {0..(p - 1) div 2}" using that B unfolding cong_def using ‹x ∈ {0..<p}› by auto show ?thesis if "y mod p ∈ {0..(p - 1) div 2}" using that A unfolding cong_def using ‹x ∈ {0..<p}› by auto qed qed (auto simp: QuadRes_def cong_def) corollary QuadRes_iff: assumes "prime p" and "odd p" shows "(QuadRes p x ∧ x ∈ {0..<p}) ⟷ (∃ a ∈ {0..(p-1) div 2}. a^2 mod p = x)" proof - have "(QuadRes p x ∧ x ∈ {0..<p}) ⟷ x ∈ {x. QuadRes p x ∧ x ∈ {0..<p}}" by auto also note QuadRes_set_prime[OF assms] also have "(x ∈ {x⇧^{2}mod p |x. x ∈ {0..(p - 1) div 2}}) = (∃a∈{0..(p - 1) div 2}. a⇧^{2}mod p = x)" by blast finally show ?thesis . qed corollary card_QuadRes_set_prime: fixes p :: int assumes "prime p" and "odd p" shows "card {x. QuadRes p x ∧ x ∈ {0..<p}} = nat (p+1) div 2" proof - have "card {x. QuadRes p x ∧ x ∈ {0..<p}} = card {x⇧^{2}mod p | x . x ∈ {0..(p-1) div 2}}" unfolding QuadRes_set_prime[OF assms] .. also have "{x⇧^{2}mod p | x . x ∈ {0..(p-1) div 2}} = (λx. x⇧^{2}mod p) ` {0..(p-1) div 2}" by auto also have "card ... = card {0..(p-1) div 2}" using inj_on_QuadRes[OF ‹prime p›] by (rule card_image) also have "... = nat (p+1) div 2" by simp finally show ?thesis . qed corollary card_not_QuadRes_set_prime: fixes p :: int assumes "prime p" and "odd p" shows "card {x. ¬QuadRes p x ∧ x ∈ {0..<p}} = nat (p-1) div 2" proof - have "{0..<p} ∩ {x. QuadRes p x ∧ x ∈ {0..<p}} = {x. QuadRes p x ∧ x ∈ {0..<p}}" by blast moreover have "nat p - nat (p + 1) div 2 = nat (p - 1) div 2" using ‹odd p› prime_gt_0_int[OF ‹prime p›] by (auto elim!: oddE simp: nat_add_distrib nat_mult_distrib) ultimately have "card {0..<p} - card ({0..<p} ∩ {x. QuadRes p x ∧ x ∈ {0..<p}}) = nat (p - 1) div 2" using card_QuadRes_set_prime[OF assms] and card_atLeastZeroLessThan_int by presburger moreover have "{x. ¬QuadRes p x ∧ x ∈ {0..<p}} = {0..<p} - {x. QuadRes p x ∧ x ∈ {0..<p}}" by blast ultimately show ?thesis by (auto simp add: card_Diff_subset_Int) qed lemma not_QuadRes_ex_if_prime: assumes "prime p" and "odd p" shows "∃ x. ¬QuadRes p x" proof - have "2 < p" using odd_prime_gt_2_int assms by blast then have False if "{x . ¬QuadRes p x ∧ x ∈ {0..<p}} = {}" using card_not_QuadRes_set_prime[OF assms] unfolding that by simp thus ?thesis by blast qed lemma not_QuadRes_ex: "1 < p ⟹ odd p ⟹ ∃x. ¬QuadRes p x" proof (induction p rule: prime_divisors_induct) case (factor p x) then show ?case by (meson not_QuadRes_ex_if_prime QuadRes_def cong_iff_dvd_diff dvd_mult_left even_mult_iff) qed simp_all end