src/HOL/Number_Theory/Gauss.thy

setprod -> prod

(*  Authors:    Jeremy Avigad, David Gray, and Adam Kramer

Ported by lcp but unfinished
*)

section \<open>Gauss' Lemma\<close>

theory Gauss
imports Residues
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)"
  by (auto simp add: cong_altdef_nat)

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)"
  by (auto simp add: cong_altdef_int)


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"
begin

definition "A = {0::int <.. ((int p - 1) div 2)}"
definition "B = (\<lambda>x. x * a) ` A"
definition "C = (\<lambda>x. x mod p) ` B"
definition "D = C \<inter> {.. (int p - 1) div 2}"
definition "E = C \<inter> {(int p - 1) div 2 <..}"
definition "F = (\<lambda>x. (int p - x)) ` E"


subsection \<open>Basic properties of p\<close>

lemma odd_p: "odd p"
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
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

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)


subsection \<open>Basic Properties of the Gauss Sets\<close>

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_C: "finite (C)"
by (auto simp add: C_def finite_B)

lemma finite_D: "finite (D)"