# Theory Gauss

Up to index of Isabelle/HOL/NumberTheory

theory Gauss
imports Euler
begin

    (*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
        ID:         $Id: Gauss.thy,v 1.9 2005/07/12 15:56:04 avigad Exp $
        Authors:    Jeremy Avigad, David Gray, and Adam Kramer)
    *)

    header {* Gauss' Lemma *}

    theory Gauss imports Euler begin;

    locale GAUSS =
      fixes p :: "int"
      fixes a :: "int"
      fixes A :: "int set"
      fixes B :: "int set"
      fixes C :: "int set"
      fixes D :: "int set"
      fixes E :: "int set"
      fixes F :: "int set"

      assumes p_prime: "zprime p"
      assumes p_g_2: "2 < p"
      assumes p_a_relprime: "~[a = 0](mod p)"
      assumes a_nonzero:    "0 < a"

      defines A_def: "A == {(x::int). 0 < x & x ≤ ((p - 1) div 2)}"
      defines B_def: "B == (%x. x * a) ` A"
      defines C_def: "C == (StandardRes p) ` B"
      defines D_def: "D == C ∩ {x. x ≤ ((p - 1) div 2)}"
      defines E_def: "E == C ∩ {x. ((p - 1) div 2) < x}"
      defines F_def: "F == (%x. (p - x)) ` E";

    subsection {* Basic properties of p *}

    lemma (in GAUSS) p_odd: "p ∈ zOdd";
      by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)

    lemma (in GAUSS) p_g_0: "0 < p";
      by (insert p_g_2, auto)

    lemma (in GAUSS) int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2";
      by (insert p_g_2, auto simp add: pos_imp_zdiv_nonneg_iff)

    lemma (in GAUSS) p_minus_one_l: "(p - 1) div 2 < p";
      proof -;
        have "p - 1 = (p - 1) div 1" by auto
        then have "(p - 1) div 2 ≤ p - 1"
          apply (rule ssubst) back;
          apply (rule zdiv_mono2)
          by (auto simp add: p_g_0)
        then have "(p - 1) div 2 ≤ p - 1";
          by auto
        then show ?thesis by simp
    qed;

    lemma (in GAUSS) p_eq: "p = (2 * (p - 1) div 2) + 1";
      apply (insert zdiv_zmult_self2 [of 2 "p - 1"])
    by auto

    lemma zodd_imp_zdiv_eq: "x ∈ zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)";
      apply (frule odd_minus_one_even)
      apply (simp add: zEven_def)
      apply (subgoal_tac "2 ≠ 0")
      apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)
    by (auto simp add: even_div_2_prop2)

    lemma (in GAUSS) p_eq2: "p = (2 * ((p - 1) div 2)) + 1";
      apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
    by (frule zodd_imp_zdiv_eq, auto)

    subsection {* Basic Properties of the Gauss Sets *}

    lemma (in GAUSS) finite_A: "finite (A)";
      apply (auto simp add: A_def)
    thm bdd_int_set_l_finite;
      apply (subgoal_tac "{x. 0 < x & x ≤ (p - 1) div 2} ⊆ {x. 0 ≤ x & x < 1 + (p - 1) div 2}");
    by (auto simp add: bdd_int_set_l_finite finite_subset)

    lemma (in GAUSS) finite_B: "finite (B)";
      by (auto simp add: B_def finite_A finite_imageI)

    lemma (in GAUSS) finite_C: "finite (C)";
      by (auto simp add: C_def finite_B finite_imageI)

    lemma (in GAUSS) finite_D: "finite (D)";
      by (auto simp add: D_def finite_Int finite_C)

    lemma (in GAUSS) finite_E: "finite (E)";
      by (auto simp add: E_def finite_Int finite_C)

    lemma (in GAUSS) finite_F: "finite (F)";
      by (auto simp add: F_def finite_E finite_imageI)

    lemma (in GAUSS) C_eq: "C = D ∪ E";
      by (auto simp add: C_def D_def E_def)

    lemma (in GAUSS) A_card_eq: "card A = nat ((p - 1) div 2)";
      apply (auto simp add: A_def)
      apply (insert int_nat)
      apply (erule subst)
      by (auto simp add: card_bdd_int_set_l_le)

    lemma (in GAUSS) inj_on_xa_A: "inj_on (%x. x * a) A";
      apply (insert a_nonzero)
    by (simp add: A_def inj_on_def)

    lemma (in GAUSS) A_res: "ResSet p A";
      apply (auto simp add: A_def ResSet_def)
      apply (rule_tac m = p in zcong_less_eq)
      apply (insert p_g_2, auto)
      apply (subgoal_tac [1-2] "(p - 1) div 2 < p");
    by (auto, auto simp add: p_minus_one_l)

    lemma (in GAUSS) B_res: "ResSet p B";
      apply (insert p_g_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)
      proof -;
        fix x fix y
        assume a: "[x * a = y * a] (mod p)"
        assume b: "0 < x"
        assume c: "x ≤ (p - 1) div 2"
        assume d: "0 < y"
        assume e: "y ≤ (p - 1) div 2"
        from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
            have "[x = y](mod p)";
          by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
        with zcong_less_eq [of x y p] p_minus_one_l
             order_le_less_trans [of x "(p - 1) div 2" p]
             order_le_less_trans [of y "(p - 1) div 2" p] show "x = y";
          by (simp add: prems p_minus_one_l p_g_0)
    qed;

    lemma (in GAUSS) SR_B_inj: "inj_on (StandardRes p) B";
      apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems)
      proof -;
        fix x fix y
        assume a: "x * a mod p = y * a mod p"
        assume b: "0 < x"
        assume c: "x ≤ (p - 1) div 2"
        assume d: "0 < y"
        assume e: "y ≤ (p - 1) div 2"
        assume f: "x ≠ y"
        from a have "[x * a = y * a](mod p)";
          by (simp add: zcong_zmod_eq p_g_0)
        with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
            have "[x = y](mod p)";
          by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
        with zcong_less_eq [of x y p] p_minus_one_l
             order_le_less_trans [of x "(p - 1) div 2" p]
             order_le_less_trans [of y "(p - 1) div 2" p] have "x = y";
          by (simp add: prems p_minus_one_l p_g_0)
        then have False;
          by (simp add: f)
        then show "a = 0";
          by simp
    qed;

    lemma (in GAUSS) inj_on_pminusx_E: "inj_on (%x. p - x) E";
      apply (auto simp add: E_def C_def B_def A_def)
      apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI);
    by auto

    lemma (in GAUSS) A_ncong_p: "x ∈ A ==> ~[x = 0](mod p)";
      apply (auto simp add: A_def)
      apply (frule_tac m = p in zcong_not_zero)
      apply (insert p_minus_one_l)
    by auto

    lemma (in GAUSS) A_greater_zero: "x ∈ A ==> 0 < x";
      by (auto simp add: A_def)

    lemma (in GAUSS) B_ncong_p: "x ∈ B ==> ~[x = 0](mod p)";
      apply (auto simp add: B_def)
      apply (frule A_ncong_p)
      apply (insert p_a_relprime p_prime a_nonzero)
      apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra)
    by (auto simp add: A_greater_zero)

    lemma (in GAUSS) B_greater_zero: "x ∈ B ==> 0 < x";
      apply (insert a_nonzero)
    by (auto simp add: B_def mult_pos_pos A_greater_zero)

    lemma (in GAUSS) C_ncong_p: "x ∈ C ==>  ~[x = 0](mod p)";
      apply (auto simp add: C_def)
      apply (frule B_ncong_p)
      apply (subgoal_tac "[x = StandardRes p x](mod p)");
      defer; apply (simp add: StandardRes_prop1)
      apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans)
    by auto

    lemma (in GAUSS) C_greater_zero: "y ∈ C ==> 0 < y";
      apply (auto simp add: C_def)
      proof -;
        fix x;
        assume a: "x ∈ B";
        from p_g_0 have "0 ≤ StandardRes p x";
          by (simp add: StandardRes_lbound)
        moreover have "~[x = 0] (mod p)";
          by (simp add: a B_ncong_p)
        then have "StandardRes p x ≠ 0";
          by (simp add: StandardRes_prop3)
        ultimately show "0 < StandardRes p x";
          by (simp add: order_le_less)
    qed;

    lemma (in GAUSS) D_ncong_p: "x ∈ D ==> ~[x = 0](mod p)";
      by (auto simp add: D_def C_ncong_p)

    lemma (in GAUSS) E_ncong_p: "x ∈ E ==> ~[x = 0](mod p)";
      by (auto simp add: E_def C_ncong_p)

    lemma (in GAUSS) F_ncong_p: "x ∈ F ==> ~[x = 0](mod p)";
      apply (auto simp add: F_def)
      proof -;
        fix x assume a: "x ∈ E" assume b: "[p - x = 0] (mod p)"
        from E_ncong_p have "~[x = 0] (mod p)";
          by (simp add: a)
        moreover from a have "0 < x";
          by (simp add: a E_def C_greater_zero)
        moreover from a have "x < p";
          by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
        ultimately have "~[p - x = 0] (mod p)";
          by (simp add: zcong_not_zero)
        from this show False by (simp add: b)
    qed;

    lemma (in GAUSS) F_subset: "F ⊆ {x. 0 < x & x ≤ ((p - 1) div 2)}";
      apply (auto simp add: F_def E_def)
      apply (insert p_g_0)
      apply (frule_tac x = xa in StandardRes_ubound)
      apply (frule_tac x = x in StandardRes_ubound)
      apply (subgoal_tac "xa = StandardRes p xa")
      apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1)
      proof -;
        from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have
            "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)";
          by simp
        with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x ∈ B |]
             ==> p - StandardRes p x ≤ (p - 1) div 2";
          by simp
    qed;

    lemma (in GAUSS) D_subset: "D ⊆ {x. 0 < x & x ≤ ((p - 1) div 2)}";
      by (auto simp add: D_def C_greater_zero)

    lemma (in GAUSS) F_eq: "F = {x. ∃y ∈ A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}";
      by (auto simp add: F_def E_def D_def C_def B_def A_def)

    lemma (in GAUSS) D_eq: "D = {x. ∃y ∈ A. ( x = StandardRes p (y*a) & StandardRes p (y*a) ≤ (p - 1) div 2)}";
      by (auto simp add: D_def C_def B_def A_def)

    lemma (in GAUSS) D_leq: "x ∈ D ==> x ≤ (p - 1) div 2";
      by (auto simp add: D_eq)

    lemma (in GAUSS) F_ge: "x ∈ F ==> x ≤ (p - 1) div 2";
      apply (auto simp add: F_eq A_def)
      proof -;
        fix y;
        assume "(p - 1) div 2 < StandardRes p (y * a)";
        then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)";
          by arith
        also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)";
          by (rule subst, auto)
        also; have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1";
          by arith
        finally show "p - StandardRes p (y * a) ≤ (p - 1) div 2";
          by (insert zless_add1_eq [of "p - StandardRes p (y * a)"
              "(p - 1) div 2"],auto);
    qed;

    lemma (in GAUSS) all_A_relprime: "∀x ∈ A. zgcd(x,p) = 1";
      apply (insert p_prime p_minus_one_l)
    by (auto simp add: A_def zless_zprime_imp_zrelprime)

    lemma (in GAUSS) A_prod_relprime: "zgcd((setprod id A),p) = 1";
      by (insert all_A_relprime finite_A, simp add: all_relprime_prod_relprime)

    subsection {* Relationships Between Gauss Sets *}

    lemma (in GAUSS) B_card_eq_A: "card B = card A";
      apply (insert finite_A)
    by (simp add: finite_A B_def inj_on_xa_A card_image)

    lemma (in GAUSS) B_card_eq: "card B = nat ((p - 1) div 2)";
      by (auto simp add: B_card_eq_A A_card_eq)

    lemma (in GAUSS) F_card_eq_E: "card F = card E";
      apply (insert finite_E)
    by (simp add: F_def inj_on_pminusx_E card_image)

    lemma (in GAUSS) C_card_eq_B: "card C = card B";
      apply (insert finite_B)
      apply (subgoal_tac "inj_on (StandardRes p) B");
      apply (simp add: B_def C_def card_image)
      apply (rule StandardRes_inj_on_ResSet)
    by (simp add: B_res)

    lemma (in GAUSS) D_E_disj: "D ∩ E = {}";
      by (auto simp add: D_def E_def)

    lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E";
      by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)

    lemma (in GAUSS) C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C";
      apply (insert D_E_disj finite_D finite_E C_eq)
      apply (frule setprod_Un_disjoint [of D E id])
    by auto

    lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)";
      apply (auto simp add: C_def)
      apply (insert finite_B SR_B_inj)
      apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id[THEN sym], auto)
      apply (rule setprod_same_function_zcong)
    by (auto simp add: StandardRes_prop1 zcong_sym p_g_0)

    lemma (in GAUSS) F_Un_D_subset: "(F ∪ D) ⊆ A";
      apply (rule Un_least)
    by (auto simp add: A_def F_subset D_subset)

    lemma two_eq: "2 * (x::int) = x + x";
      by arith

    lemma (in GAUSS) F_D_disj: "(F ∩ D) = {}";
      apply (simp add: F_eq D_eq)
      apply (auto simp add: F_eq D_eq)
      proof -;
        fix y; fix ya;
        assume "p - StandardRes p (y * a) = StandardRes p (ya * a)";
        then have "p = StandardRes p (y * a) + StandardRes p (ya * a)";
          by arith
        moreover have "p dvd p";
          by auto
        ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))";
          by auto
        then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)";
          by (auto simp add: zcong_def)
        have "[y * a = StandardRes p (y * a)] (mod p)";
          by (simp only: zcong_sym StandardRes_prop1)
        moreover have "[ya * a = StandardRes p (ya * a)] (mod p)";
          by (simp only: zcong_sym StandardRes_prop1)
        ultimately have "[y * a + ya * a =
            StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)";
          by (rule zcong_zadd)
        with a have "[y * a + ya * a = 0] (mod p)";
          apply (elim zcong_trans)
          by (simp only: zcong_refl)
        also have "y * a + ya * a = a * (y + ya)";
          by (simp add: zadd_zmult_distrib2 zmult_commute)
        finally have "[a * (y + ya) = 0] (mod p)";.;
        with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
            p_a_relprime
            have a: "[y + ya = 0] (mod p)";
          by auto
        assume b: "y ∈ A" and c: "ya: A";
        with A_def have "0 < y + ya";
          by auto
        moreover from b c A_def have "y + ya ≤ (p - 1) div 2 + (p - 1) div 2";
          by auto
        moreover from b c p_eq2 A_def have "y + ya < p";
          by auto
        ultimately show False;
          apply simp
          apply (frule_tac m = p in zcong_not_zero)
          by (auto simp add: a)
    qed;

    lemma (in GAUSS) F_Un_D_card: "card (F ∪ D) = nat ((p - 1) div 2)";
      apply (insert F_D_disj finite_F finite_D)
      proof -;
        have "card (F ∪ D) = card E + card D";
          by (auto simp add: finite_F finite_D F_D_disj
                             card_Un_disjoint F_card_eq_E)
        then have "card (F ∪ D) = card C";
          by (simp add: C_card_eq_D_plus_E)
        from this show "card (F ∪ D) = nat ((p - 1) div 2)";
          by (simp add: C_card_eq_B B_card_eq)
    qed;

    lemma (in GAUSS) F_Un_D_eq_A: "F ∪ D = A";
      apply (insert finite_A F_Un_D_subset A_card_eq F_Un_D_card)
    by (auto simp add: card_seteq)

    lemma (in GAUSS) prod_D_F_eq_prod_A:
        "(setprod id D) * (setprod id F) = setprod id A";
      apply (insert F_D_disj finite_D finite_F)
      apply (frule setprod_Un_disjoint [of F D id])
    by (auto simp add: F_Un_D_eq_A)

    lemma (in GAUSS) prod_F_zcong:
        "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
      proof -
        have "setprod id F = setprod id (op - p ` E)"
          by (auto simp add: F_def)
        then have "setprod id F = setprod (op - p) E"
          apply simp
          apply (insert finite_E inj_on_pminusx_E)
          by (frule_tac f = "op - p" in setprod_reindex_id, auto)
        then have one:
          "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
          apply simp
          apply (insert p_g_0 finite_E)
          by (auto simp add: StandardRes_prod)
        moreover have a: "∀x ∈ E. [p - x = 0 - x] (mod p)"
          apply clarify
          apply (insert zcong_id [of p])
          by (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
        moreover have b: "∀x ∈ E. [StandardRes p (p - x) = p - x](mod p)"
          apply clarify
          by (simp add: StandardRes_prop1 zcong_sym)
        moreover have "∀x ∈ E. [StandardRes p (p - x) = - x](mod p)"
          apply clarify
          apply (insert a b)
          by (rule_tac b = "p - x" in zcong_trans, auto)
        ultimately have c:
          "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
          apply simp
          apply (insert finite_E p_g_0)
          by (rule setprod_same_function_zcong [of E "StandardRes p o (op - p)"
                                                         uminus p], auto)
        then have two: "[setprod id F = setprod (uminus) E](mod p)"
          apply (insert one c)
          by (rule zcong_trans [of "setprod id F"
                                   "setprod (StandardRes p o op - p) E" p
                                   "setprod uminus E"], auto)
        also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
          apply (insert finite_E)
          by (induct set: Finites, auto)
        then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
          by (simp add: zmult_commute)
        with two show ?thesis
          by simp
    qed

    subsection {* Gauss' Lemma *}

    lemma (in GAUSS) aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
      by (auto simp add: finite_E neg_one_special)

    theorem (in GAUSS) pre_gauss_lemma:
        "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
      proof -
        have "[setprod id A = setprod id F * setprod id D](mod p)"
          by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
        then have "[setprod id A = ((-1)^(card E) * setprod id E) *
            setprod id D] (mod p)"
          apply (rule zcong_trans)
          by (auto simp add: prod_F_zcong zcong_scalar)
        then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
          apply (rule zcong_trans)
          apply (insert C_prod_eq_D_times_E, erule subst)
          by (subst zmult_assoc, auto)
        then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
          apply (rule zcong_trans)
          by (simp add: C_B_zcong_prod zcong_scalar2)
        then have "[setprod id A = ((-1)^(card E) *
            (setprod id ((%x. x * a) ` A)))] (mod p)"
          by (simp add: B_def)
        then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
            (mod p)"
          by(simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
        moreover have "setprod (%x. x * a) A =
            setprod (%x. a) A * setprod id A"
          by (insert finite_A, induct set: Finites, auto)
        ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
            setprod id A))] (mod p)"
          by simp
        then have "[setprod id A = ((-1)^(card E) * a^(card A) *
            setprod id A)](mod p)"
          apply (rule zcong_trans)
          by (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant
            zmult_assoc)
        then have a: "[setprod id A * (-1)^(card E) =
            ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
          by (rule zcong_scalar)
        then have "[setprod id A * (-1)^(card E) = setprod id A *
            (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
          apply (rule zcong_trans)
          by (simp add: a mult_commute mult_left_commute)
        then have "[setprod id A * (-1)^(card E) = setprod id A *
            a^(card A)](mod p)"
          apply (rule zcong_trans)
          by (simp add: aux)
        with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
             p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
           by (simp add: order_less_imp_le)
        from this show ?thesis
          by (simp add: A_card_eq zcong_sym)
    qed

    theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
    proof -
      from Euler_Criterion p_prime p_g_2 have
        "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
        by auto
      moreover note pre_gauss_lemma
      ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
        by (rule zcong_trans)
      moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
        by (auto simp add: Legendre_def)
      moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
        by (rule neg_one_power)
      ultimately show ?thesis
        by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
    qed

    end

### Basic properties of p

lemma p_odd:

      GAUSS p a ==> p ∈ zOdd

lemma p_g_0:

      GAUSS p a ==> 0 < p

lemma int_nat:

      GAUSS p a ==> int (nat ((p - 1) div 2)) = (p - 1) div 2

lemma p_minus_one_l:

      GAUSS p a ==> (p - 1) div 2 < p

lemma p_eq:

      GAUSS p a ==> p = 2 * (p - 1) div 2 + 1

lemma zodd_imp_zdiv_eq:

      x ∈ zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)

lemma p_eq2:

      GAUSS p a ==> p = 2 * ((p - 1) div 2) + 1

### Basic Properties of the Gauss Sets

lemma finite_A:

      GAUSS p a ==> finite {x. 0 < x ∧ x ≤ (p - 1) div 2}

lemma finite_B:

      GAUSS p a ==> finite ((%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2})

lemma finite_C:

      GAUSS p a
      ==> finite (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2})

lemma finite_D:

      GAUSS p a
      ==> finite
           (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
            {x. x ≤ (p - 1) div 2})

lemma finite_E:

      GAUSS p a
      ==> finite
           (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
            {x. (p - 1) div 2 < x})

lemma finite_F:

      GAUSS p a
      ==> finite
           (op - p `
            (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
             {x. (p - 1) div 2 < x}))

lemma C_eq:

      GAUSS p a
      ==> StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} =
          StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
          {x. x ≤ (p - 1) div 2} ∪
          StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
          {x. (p - 1) div 2 < x}

lemma A_card_eq:

      GAUSS p a ==> card {x. 0 < x ∧ x ≤ (p - 1) div 2} = nat ((p - 1) div 2)

lemma inj_on_xa_A:

      GAUSS p a ==> inj_on (%x. x * a) {x. 0 < x ∧ x ≤ (p - 1) div 2}

lemma A_res:

      GAUSS p a ==> ResSet p {x. 0 < x ∧ x ≤ (p - 1) div 2}

lemma B_res:

      GAUSS p a ==> ResSet p ((%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2})

lemma SR_B_inj:

      GAUSS p a
      ==> inj_on (StandardRes p) ((%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2})

lemma inj_on_pminusx_E:

      GAUSS p a
      ==> inj_on (op - p)
           (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
            {x. (p - 1) div 2 < x})

lemma A_ncong_p:

      [| GAUSS p a; x ∈ {x. 0 < x ∧ x ≤ (p - 1) div 2} |] ==> ¬ [x = 0] (mod p)

lemma A_greater_zero:

      [| GAUSS p a; x ∈ {x. 0 < x ∧ x ≤ (p - 1) div 2} |] ==> 0 < x

lemma B_ncong_p:

      [| GAUSS p a; x ∈ (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} |]
      ==> ¬ [x = 0] (mod p)

lemma B_greater_zero:

      [| GAUSS p a; x ∈ (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} |] ==> 0 < x

lemma C_ncong_p:

      [| GAUSS p a;
         x ∈ StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} |]
      ==> ¬ [x = 0] (mod p)

lemma C_greater_zero:

      [| GAUSS p a;
         y ∈ StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} |]
      ==> 0 < y

lemma D_ncong_p:

      [| GAUSS p a;
         x ∈ StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
             {x. x ≤ (p - 1) div 2} |]
      ==> ¬ [x = 0] (mod p)

lemma E_ncong_p:

      [| GAUSS p a;
         x ∈ StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
             {x. (p - 1) div 2 < x} |]
      ==> ¬ [x = 0] (mod p)

lemma F_ncong_p:

      [| GAUSS p a;
         x ∈ op - p `
             (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
              {x. (p - 1) div 2 < x}) |]
      ==> ¬ [x = 0] (mod p)

lemma F_subset:

      GAUSS p a
      ==> op - p `
          (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
           {x. (p - 1) div 2 < x})
          ⊆ {x. 0 < x ∧ x ≤ (p - 1) div 2}

lemma D_subset:

      GAUSS p a
      ==> StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
          {x. x ≤ (p - 1) div 2}
          ⊆ {x. 0 < x ∧ x ≤ (p - 1) div 2}

lemma F_eq:

      GAUSS p a
      ==> op - p `
          (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
           {x. (p - 1) div 2 < x}) =
          {x. ∃y∈{x. 0 < x ∧ x ≤ (p - 1) div 2}.
                 x = p - StandardRes p (y * a) ∧
                 (p - 1) div 2 < StandardRes p (y * a)}

lemma D_eq:

      GAUSS p a
      ==> StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
          {x. x ≤ (p - 1) div 2} =
          {x. ∃y∈{x. 0 < x ∧ x ≤ (p - 1) div 2}.
                 x = StandardRes p (y * a) ∧ StandardRes p (y * a) ≤ (p - 1) div 2}

lemma D_leq:

      [| GAUSS p a;
         x ∈ StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
             {x. x ≤ (p - 1) div 2} |]
      ==> x ≤ (p - 1) div 2

lemma F_ge:

      [| GAUSS p a;
         x ∈ op - p `
             (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
              {x. (p - 1) div 2 < x}) |]
      ==> x ≤ (p - 1) div 2

lemma all_A_relprime:

      GAUSS p a ==> ∀x∈{x. 0 < x ∧ x ≤ (p - 1) div 2}. zgcd (x, p) = 1

lemma A_prod_relprime:

      GAUSS p a ==> zgcd (setprod id {x. 0 < x ∧ x ≤ (p - 1) div 2}, p) = 1

### Relationships Between Gauss Sets

lemma B_card_eq_A:

      GAUSS p a
      ==> card ((%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2}) =
          card {x. 0 < x ∧ x ≤ (p - 1) div 2}

lemma B_card_eq:

      GAUSS p a
      ==> card ((%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2}) = nat ((p - 1) div 2)

lemma F_card_eq_E:

      GAUSS p a
      ==> card (op - p `
                (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                 {x. (p - 1) div 2 < x})) =
          card (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                {x. (p - 1) div 2 < x})

lemma C_card_eq_B:

      GAUSS p a
      ==> card (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2}) =
          card ((%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2})

lemma D_E_disj:

      GAUSS p a
      ==> StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
          {x. x ≤ (p - 1) div 2} ∩
          (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
           {x. (p - 1) div 2 < x}) =
          {}

lemma C_card_eq_D_plus_E:

      GAUSS p a
      ==> card (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2}) =
          card (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                {x. x ≤ (p - 1) div 2}) +
          card (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                {x. (p - 1) div 2 < x})

lemma C_prod_eq_D_times_E:

      GAUSS p a
      ==> setprod id
           (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
            {x. (p - 1) div 2 < x}) *
          setprod id
           (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
            {x. x ≤ (p - 1) div 2}) =
          setprod id (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2})

lemma C_B_zcong_prod:

      GAUSS p a
      ==> [setprod id
            (StandardRes p `
             (%x. x * a) `
             {x. 0 < x ∧
                 x ≤ (p - 1) div
                     2}) = setprod id
                            ((%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2})] (mod p)

lemma F_Un_D_subset:

      GAUSS p a
      ==> op - p `
          (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
           {x. (p - 1) div 2 < x}) ∪
          StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
          {x. x ≤ (p - 1) div 2}
          ⊆ {x. 0 < x ∧ x ≤ (p - 1) div 2}

lemma two_eq:

      2 * x = x + x

lemma F_D_disj:

      GAUSS p a
      ==> op - p `
          (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
           {x. (p - 1) div 2 < x}) ∩
          (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
           {x. x ≤ (p - 1) div 2}) =
          {}

lemma F_Un_D_card:

      GAUSS p a
      ==> card (op - p `
                (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                 {x. (p - 1) div 2 < x}) ∪
                StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                {x. x ≤ (p - 1) div 2}) =
          nat ((p - 1) div 2)

lemma F_Un_D_eq_A:

      GAUSS p a
      ==> op - p `
          (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
           {x. (p - 1) div 2 < x}) ∪
          StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
          {x. x ≤ (p - 1) div 2} =
          {x. 0 < x ∧ x ≤ (p - 1) div 2}

lemma prod_D_F_eq_prod_A:

      GAUSS p a
      ==> setprod id
           (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
            {x. x ≤ (p - 1) div 2}) *
          setprod id
           (op - p `
            (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
             {x. (p - 1) div 2 < x})) =
          setprod id {x. 0 < x ∧ x ≤ (p - 1) div 2}

lemma prod_F_zcong:

      GAUSS p a
      ==> [setprod id
            (op - p `
             (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
              {x. (p - 1) div 2
                  < x})) = -1 ^
                           card (StandardRes p `
                                 (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                                 {x. (p - 1) div 2 < x}) *
                           setprod id
                            (StandardRes p `
                             (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                             {x. (p - 1) div 2 < x})] (mod p)

### Gauss' Lemma

lemma aux:

      GAUSS p a
      ==> setprod id {x. 0 < x ∧ x ≤ (p - 1) div 2} *
          -1 ^
          card (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                {x. (p - 1) div 2 < x}) *
          a ^ card {x. 0 < x ∧ x ≤ (p - 1) div 2} *
          -1 ^
          card (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                {x. (p - 1) div 2 < x}) =
          setprod id {x. 0 < x ∧ x ≤ (p - 1) div 2} *
          a ^ card {x. 0 < x ∧ x ≤ (p - 1) div 2}

theorem pre_gauss_lemma:

      GAUSS p a
      ==> [a ^ nat ((p - 1) div
                    2) = -1 ^
                         card (StandardRes p `
                               (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                               {x. (p - 1) div 2 < x})] (mod p)

theorem gauss_lemma:

      GAUSS p a
      ==> Legendre a p =
          -1 ^
          card (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
                {x. (p - 1) div 2 < x})