```(*
File:     Miller_Rabin.thy
Authors:  Daniel Stüwe

Some facts about Quadratic Residues that are missing from the library
*)
imports
Jacobi_Symbol
Algebraic_Auxiliaries
begin

text ‹Proofs are inspired by \<^cite>‹"Quadratic_Residues"›.›

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

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)

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

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

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

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}} = {}"
unfolding that
by simp

thus ?thesis by blast
qed