src/HOL/Number_Theory/Gauss.thy
author haftmann
Sun, 09 Nov 2014 10:03:18 +0100
changeset 58954 18750e86d5b8
parent 58889 5b7a9633cfa8
child 59545 12a6088ed195
permissions -rw-r--r--
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     1
(*  Authors:    Jeremy Avigad, David Gray, and Adam Kramer
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     2
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     3
Ported by lcp but unfinished
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     4
*)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     5
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 58834
diff changeset
     6
section {* Gauss' Lemma *}
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     7
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     8
theory Gauss
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     9
imports Residues
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    10
begin
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    11
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    12
lemma cong_prime_prod_zero_nat: 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    13
  fixes a::nat
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    14
  shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    15
  by (auto simp add: cong_altdef_nat)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    16
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    17
lemma cong_prime_prod_zero_int: 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    18
  fixes a::int
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    19
  shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    20
  by (auto simp add: cong_altdef_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    21
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    22
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    23
locale GAUSS =
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    24
  fixes p :: "nat"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    25
  fixes a :: "int"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    26
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    27
  assumes p_prime: "prime p"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    28
  assumes p_ge_2: "2 < p"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    29
  assumes p_a_relprime: "[a \<noteq> 0](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    30
  assumes a_nonzero:    "0 < a"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    31
begin
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    32
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    33
definition "A = {0::int <.. ((int p - 1) div 2)}"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    34
definition "B = (\<lambda>x. x * a) ` A"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    35
definition "C = (\<lambda>x. x mod p) ` B"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    36
definition "D = C \<inter> {.. (int p - 1) div 2}"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    37
definition "E = C \<inter> {(int p - 1) div 2 <..}"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    38
definition "F = (\<lambda>x. (int p - x)) ` E"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    39
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    40
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    41
subsection {* Basic properties of p *}
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    42
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    43
lemma odd_p: "odd p"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    44
by (metis p_prime p_ge_2 prime_odd_nat)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    45
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    46
lemma p_minus_one_l: "(int p - 1) div 2 < p"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    47
proof -
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    48
  have "(p - 1) div 2 \<le> (p - 1) div 1"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    49
    by (metis div_by_1 div_le_dividend)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    50
  also have "\<dots> = p - 1" by simp
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    51
  finally show ?thesis using p_ge_2 by arith
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    52
qed
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    53
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    54
lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    55
  using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]   
58834
773b378d9313 more simp rules concerning dvd and even/odd
haftmann
parents: 58645
diff changeset
    56
  by simp
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    57
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    58
lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    59
  using odd_p p_ge_2
58645
94bef115c08f more foundational definition for predicate even
haftmann
parents: 58410
diff changeset
    60
  by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    61
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    62
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    63
subsection {* Basic Properties of the Gauss Sets *}
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    64
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    65
lemma finite_A: "finite (A)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    66
by (auto simp add: A_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    67
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    68
lemma finite_B: "finite (B)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    69
by (auto simp add: B_def finite_A)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    70
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    71
lemma finite_C: "finite (C)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    72
by (auto simp add: C_def finite_B)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    73
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    74
lemma finite_D: "finite (D)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    75
by (auto simp add: D_def finite_C)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    76
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    77
lemma finite_E: "finite (E)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    78
by (auto simp add: E_def finite_C)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    79
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    80
lemma finite_F: "finite (F)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    81
by (auto simp add: F_def finite_E)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    82
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    83
lemma C_eq: "C = D \<union> E"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    84
by (auto simp add: C_def D_def E_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    85
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    86
lemma A_card_eq: "card A = nat ((int p - 1) div 2)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    87
  by (auto simp add: A_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    88
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    89
lemma inj_on_xa_A: "inj_on (\<lambda>x. x * a) A"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    90
  using a_nonzero by (simp add: A_def inj_on_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    91
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    92
definition ResSet :: "int => int set => bool"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    93
  where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    94
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    95
lemma ResSet_image:
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    96
  "\<lbrakk> 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) \<rbrakk> \<Longrightarrow>
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    97
    ResSet m (f ` A)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    98
  by (auto simp add: ResSet_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    99
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   100
lemma A_res: "ResSet p A"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   101
  using p_ge_2
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   102
  by (auto simp add: A_def ResSet_def intro!: cong_less_imp_eq_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   103
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   104
lemma B_res: "ResSet p B"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   105
proof -
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   106
  {fix x fix y
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   107
    assume a: "[x * a = y * a] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   108
    assume b: "0 < x"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   109
    assume c: "x \<le> (int p - 1) div 2"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   110
    assume d: "0 < y"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   111
    assume e: "y \<le> (int p - 1) div 2"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   112
    from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y]
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   113
    have "[x = y](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   114
      by (metis comm_monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   115
                cong_mult_self_int gcd_int.commute prime_imp_coprime_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   116
    with cong_less_imp_eq_int [of x y p] p_minus_one_l
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   117
        order_le_less_trans [of x "(int p - 1) div 2" p]
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   118
        order_le_less_trans [of y "(int p - 1) div 2" p] 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   119
    have "x = y"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   120
      by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   121
    } note xy = this
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   122
  show ?thesis
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   123
    apply (insert p_ge_2 p_a_relprime p_minus_one_l)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   124
    apply (auto simp add: B_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   125
    apply (rule ResSet_image)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   126
    apply (auto simp add: A_res)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   127
    apply (auto simp add: A_def xy)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   128
    done
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   129
  qed
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   130
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   131
lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   132
proof -
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   133
{ fix x fix y
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   134
  assume a: "x * a mod p = y * a mod p"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   135
  assume b: "0 < x"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   136
  assume c: "x \<le> (int p - 1) div 2"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   137
  assume d: "0 < y"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   138
  assume e: "y \<le> (int p - 1) div 2"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   139
  assume f: "x \<noteq> y"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   140
  from a have "[x * a = y * a](mod p)" 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   141
    by (metis cong_int_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   142
  with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y]
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   143
  have "[x = y](mod p)" 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   144
    by (metis cong_mult_self_int dvd_div_mult_self gcd_commute_int prime_imp_coprime_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   145
  with cong_less_imp_eq_int [of x y p] p_minus_one_l
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   146
    order_le_less_trans [of x "(int p - 1) div 2" p]
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   147
    order_le_less_trans [of y "(int p - 1) div 2" p] 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   148
  have "x = y"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   149
    by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   150
  then have False
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   151
    by (simp add: f)}
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   152
  then show ?thesis
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   153
    by (auto simp add: B_def inj_on_def A_def) metis
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   154
qed
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   155
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   156
lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   157
  apply (auto simp add: E_def C_def B_def A_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   158
  apply (rule_tac g = "(op - (int p))" in inj_on_inverseI)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   159
  apply auto
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   160
  done
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   161
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   162
lemma nonzero_mod_p:
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   163
  fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   164
by (metis Nat_Transfer.transfer_nat_int_function_closures(9) cong_less_imp_eq_int 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   165
     inf.semilattice_strict_iff_order int_less_0_conv le_numeral_extra(3) zero_less_imp_eq_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   166
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   167
lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   168
  by (rule nonzero_mod_p) (auto simp add: A_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   169
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   170
lemma A_greater_zero: "x \<in> A \<Longrightarrow> 0 < x"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   171
  by (auto simp add: A_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   172
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   173
lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   174
  by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   175
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   176
lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
56544
b60d5d119489 made mult_pos_pos a simp rule
nipkow
parents: 55730
diff changeset
   177
  using a_nonzero by (auto simp add: B_def A_greater_zero)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   178
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   179
lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   180
proof (auto simp add: C_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   181
  fix x :: int
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   182
  assume a1: "x \<in> B"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   183
  have f2: "\<And>x\<^sub>1. int x\<^sub>1 = 0 \<or> 0 < int x\<^sub>1" by linarith
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   184
  have "x mod int p \<noteq> 0" using a1 B_ncong_p cong_int_def by simp
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   185
  thus "0 < x mod int p" using a1 f2 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   186
    by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   187
qed
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   188
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   189
lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((int p - 1) div 2)}"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   190
  apply (auto simp add: F_def E_def C_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   191
  apply (metis p_ge_2 Divides.pos_mod_bound less_diff_eq nat_int plus_int_code(2) zless_nat_conj)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   192
  apply (auto intro: p_odd_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   193
  done
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   194
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   195
lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   196
  by (auto simp add: D_def C_greater_zero)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   197
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   198
lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - ((y*a) mod p) & (int p - 1) div 2 < (y*a) mod p)}"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   199
  by (auto simp add: F_def E_def D_def C_def B_def A_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   200
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   201
lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = (y*a) mod p & (y*a) mod p \<le> (int p - 1) div 2)}"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   202
  by (auto simp add: D_def C_def B_def A_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   203
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   204
lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   205
  using p_prime A_ncong_p [OF assms]
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   206
  by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   207
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   208
lemma A_prod_relprime: "gcd (setprod id A) p = 1"
58288
87b59745dd6d avoid internal fact
blanchet
parents: 57512
diff changeset
   209
  by (metis id_def all_A_relprime setprod_coprime_int)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   210
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   211
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   212
subsection {* Relationships Between Gauss Sets *}
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   213
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   214
lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   215
  by (auto simp add: ResSet_def inj_on_def cong_int_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   216
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   217
lemma B_card_eq_A: "card B = card A"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   218
  using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   219
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   220
lemma B_card_eq: "card B = nat ((int p - 1) div 2)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   221
  by (simp add: B_card_eq_A A_card_eq)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   222
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   223
lemma F_card_eq_E: "card F = card E"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   224
  using finite_E 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   225
  by (simp add: F_def inj_on_pminusx_E card_image)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   226
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   227
lemma C_card_eq_B: "card C = card B"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   228
proof -
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   229
  have "inj_on (\<lambda>x. x mod p) B"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   230
    by (metis SR_B_inj) 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   231
  then show ?thesis
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   232
    by (metis C_def card_image)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   233
qed
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   234
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   235
lemma D_E_disj: "D \<inter> E = {}"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   236
  by (auto simp add: D_def E_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   237
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   238
lemma C_card_eq_D_plus_E: "card C = card D + card E"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   239
  by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   240
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   241
lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   242
  by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod.union_disjoint sup_commute)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   243
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   244
lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   245
  apply (auto simp add: C_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   246
  apply (insert finite_B SR_B_inj)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   247
  apply (drule setprod.reindex [of "\<lambda>x. x mod int p" B id])
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   248
  apply auto
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   249
  apply (rule cong_setprod_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   250
  apply (auto simp add: cong_int_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   251
  done
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   252
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   253
lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   254
  apply (intro Un_least subset_trans [OF F_subset] subset_trans [OF D_subset])
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   255
  apply (auto simp add: A_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   256
  done
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   257
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   258
lemma F_D_disj: "(F \<inter> D) = {}"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   259
proof (auto simp add: F_eq D_eq)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   260
  fix y::int and z::int
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   261
  assume "p - (y*a) mod p = (z*a) mod p"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   262
  then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   263
    by (metis add.commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   264
  moreover have "[y * a = (y*a) mod p] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   265
    by (metis cong_int_def mod_mod_trivial)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   266
  ultimately have "[a * (y + z) = 0] (mod p)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   267
    by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   268
  with p_prime a_nonzero p_a_relprime
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   269
  have a: "[y + z = 0] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   270
    by (metis cong_prime_prod_zero_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   271
  assume b: "y \<in> A" and c: "z \<in> A"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   272
  with A_def have "0 < y + z"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   273
    by auto
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   274
  moreover from b c p_eq2 A_def have "y + z < p"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   275
    by auto
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   276
  ultimately show False
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   277
    by (metis a nonzero_mod_p)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   278
qed
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   279
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   280
lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   281
proof -
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   282
  have "card (F \<union> D) = card E + card D"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   283
    by (auto simp add: finite_F finite_D F_D_disj card_Un_disjoint F_card_eq_E)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   284
  then have "card (F \<union> D) = card C"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   285
    by (simp add: C_card_eq_D_plus_E)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   286
  then show "card (F \<union> D) = nat ((p - 1) div 2)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   287
    by (simp add: C_card_eq_B B_card_eq)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   288
qed
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   289
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   290
lemma F_Un_D_eq_A: "F \<union> D = A"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   291
  using finite_A F_Un_D_subset A_card_eq F_Un_D_card 
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   292
  by (auto simp add: card_seteq)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   293
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   294
lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   295
  by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod.union_disjoint)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   296
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   297
lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   298
proof -
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   299
  have FE: "setprod id F = setprod (op - p) E"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   300
    apply (auto simp add: F_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   301
    apply (insert finite_E inj_on_pminusx_E)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   302
    apply (drule setprod.reindex, auto)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   303
    done
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   304
  then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   305
    by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   306
  then have "[setprod ((\<lambda>x. x mod p) o (op - p)) E = setprod (uminus) E](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   307
    using finite_E p_ge_2
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   308
          cong_setprod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   309
    by auto
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   310
  then have two: "[setprod id F = setprod (uminus) E](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   311
    by (metis FE cong_cong_mod_int cong_refl_int cong_setprod_int minus_mod_self1)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   312
  have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   313
    using finite_E by (induct set: finite) auto
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   314
  with two show ?thesis
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   315
    by simp
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   316
qed
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   317
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   318
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   319
subsection {* Gauss' Lemma *}
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   320
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 58288
diff changeset
   321
lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   322
by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   323
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   324
theorem pre_gauss_lemma:
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   325
  "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   326
proof -
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   327
  have "[setprod id A = setprod id F * setprod id D](mod p)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   328
    by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   329
  then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   330
    apply (rule cong_trans_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   331
    apply (metis cong_scalar_int prod_F_zcong)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   332
    done
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   333
  then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   334
    by (metis C_prod_eq_D_times_E mult.commute mult.left_commute)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   335
  then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   336
    by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   337
  then have "[setprod id A = ((-1)^(card E) *
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   338
    (setprod id ((\<lambda>x. x * a) ` A)))] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   339
    by (simp add: B_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   340
  then have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. x * a) A))]
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   341
    (mod p)"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   342
    by (simp add: inj_on_xa_A setprod.reindex)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   343
  moreover have "setprod (\<lambda>x. x * a) A =
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   344
    setprod (\<lambda>x. a) A * setprod id A"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   345
    using finite_A by (induct set: finite) auto
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   346
  ultimately have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. a) A *
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   347
    setprod id A))] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   348
    by simp
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   349
  then have "[setprod id A = ((-1)^(card E) * a^(card A) *
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   350
      setprod id A)](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   351
    apply (rule cong_trans_int)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   352
    apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult.assoc)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   353
    done
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   354
  then have a: "[setprod id A * (-1)^(card E) =
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   355
      ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   356
    by (rule cong_scalar_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   357
  then have "[setprod id A * (-1)^(card E) = setprod id A *
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   358
      (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   359
    apply (rule cong_trans_int)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   360
    apply (simp add: a mult.commute mult.left_commute)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   361
    done
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   362
  then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   363
    apply (rule cong_trans_int)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   364
    apply (simp add: aux cong del:setprod.cong)
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   365
    done
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 58288
diff changeset
   366
  with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
55730
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   367
    by (metis cong_mult_lcancel_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   368
  then show ?thesis
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   369
    by (simp add: A_card_eq cong_sym_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   370
qed
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   371
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   372
(*NOT WORKING. Old_Number_Theory/Euler.thy needs to be translated, but it's
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   373
quite a mess and should better be completely redone.
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   374
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   375
theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   376
proof -
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   377
  from Euler_Criterion p_prime p_ge_2 have
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   378
      "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   379
    by auto
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   380
  moreover note pre_gauss_lemma
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   381
  ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   382
    by (rule cong_trans_int)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   383
  moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   384
    by (auto simp add: Legendre_def)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   385
  moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   386
    by (rule neg_one_power)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   387
  ultimately show ?thesis
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   388
    by (auto simp add: p_ge_2 one_not_neg_one_mod_m zcong_sym)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   389
qed
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   390
*)
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   391
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   392
end
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   393
97ff9276e12d Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   394
end